alang9

{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

module Data.Machine.Translate where

import Control.Lens
import Control.Monad
import Data.Machine

alang9

module Minesweeper

import Data.Fin
import Data.SortedMap as SM

data Tile a = Mine | NoMine a

data Board : Type -> Nat -> Nat -> Type where
  MkBoard : SortedMap (Fin r, Fin c) (Tile a) -> Board a r c

alang9

data Buffer v w x y z q i j where
  B :: Tag n1 n2 n3 n4 n5 -> !(If n1 q (:~:) m n) -> !(If n2 q (:~:) l m) -> !(If n3 q (:~:) k l) -> !(If n4 q (:~:) j k) -> !(If n5 q (:~:) i j) -> Buffer n1 n2 n3 n4 n5 q i n

pattern B0 = B Zero Refl Refl Refl Refl Refl
pattern B1 a = B One a Refl Refl Refl Refl
pattern B2 a b = B Two a b Refl Refl Refl
pattern B3 a b c = B Three a b c Refl Refl
pattern B4 a b c d = B Four a b c d Refl
pattern B5 a b c d e = B Five a b c d e

alang9

data Skippable o p q i j where
  Skip :: Skippable o F q i i
  Lou :: !(q i j) -> Skippable T T q i j

data Buffer n1 n2 n3 n4 n5 q i n where
  B :: !(Skippable T n1 q m n) -> !(Skippable n1 n2 q l m) -> !(Skippable n2 n3 q k l) -> !(Skippable n3 n4 q j k) -> !(Skippable n4 n5 q i j) -> Buffer n1 n2 n3 n4 n5 q i n

alang9

Benchmark main: RUNNING...
benchmarking pushThenPop/Cat
time                 566.5 μs   (540.5 μs .. 598.6 μs)
                     0.973 R²   (0.955 R² .. 0.985 R²)
mean                 550.2 μs   (527.5 μs .. 575.5 μs)
std dev              78.43 μs   (64.48 μs .. 107.3 μs)
variance introduced by outliers: 87% (severely inflated)

benchmarking pushThenPop/NonCat
time                 623.9 μs   (593.7 μs .. 659.3 μs)

alang9

benchmarking pushThenPop/Cat
time                 42.85 μs   (40.07 μs .. 45.80 μs)
                     0.974 R²   (0.964 R² .. 0.985 R²)
mean                 45.79 μs   (43.77 μs .. 48.19 μs)
std dev              7.540 μs   (6.223 μs .. 10.52 μs)
variance introduced by outliers: 94% (severely inflated)

benchmarking pushThenPop/Seq
time                 8.754 μs   (8.298 μs .. 9.251 μs)
                     0.981 R²   (0.973 R² .. 0.989 R²)

alang9

data Foo a b where
  F :: !Int -> Foo () ()

mkDeq :: Int -> Int -> Deque (Closed Green) (Closed Green) Foo () ()
mkDeq m n = foldr (\a d -> catenate d $ iterate (push (F a)) empty !! m) empty [1..n]

sumDeq :: Deque (Closed Green) (Closed Green) Foo () () -> Int
sumDeq = sum . unfoldr go
  where
    go :: Deque (Closed Green) (Closed Green) Foo () () -> Maybe (Int, Deque (Closed Green) (Closed Green) Foo () ())

alang9

{-# LANGUAGE RankNTypes, GADTs #-}

module Bidi where

import Control.Monad.Trans

import Data.Machine

data Pipe a' a b' b c where
    Request :: a' -> Pipe a' a b' b a