Add helper function for merging finite sets

1 files changed, 41 insertions, 0 deletions

diff --git a/tiny/src/Circuit.hs b/tiny/src/Circuit.hs
new file mode 100644
index 0000000..d64e8c1
--- /dev/null
+++ b/tiny/src/Circuit.hs
@@ -0,0 +1,41 @@
+module Circuit () where
+
+import RIO
+
+import Data.Kind
+
+
+data Nat = Zero | Succ Nat | Plus Nat Nat
+
+data Env :: Nat -> Type -> Type where
+    Leaf :: Env Zero a
+    Cons :: a -> Env n a -> Env (Succ n) a
+    Node :: Env l a -> Env r a -> Env (Plus l r) a
+
+data Circuit :: Nat -> Type -> Type where
+    Con :: Int -> Circuit Zero t
+    Var :: t -> Circuit Zero t
+    Add :: Circuit m t -> Circuit n t -> Circuit (Plus m n) t
+    Let :: Circuit m t -> (t -> Circuit n t) -> Circuit (Plus m n) t
+    Fix :: (t -> Circuit n t) -> Circuit n t
+    Reg :: Circuit n t -> Circuit (Succ n) t
+
+eval :: (Circuit n Int, Env n Int) -> Int
+eval (Con i    ,        _) = i
+eval (Var x    ,        _) = x
+eval (Add e1 e2, Node l r) = eval (e1, l) + eval (e2, r)
+eval (Let e1 e2, Node l r) = eval (e2 (eval (e1, l)), r)
+eval (Fix e    ,      env) = fix (\x -> eval (e x, env))
+eval (Reg _    , Cons v _) = v
+
+step :: (Circuit n Int, Env n Int) -> Env n Int
+step (Con i    ,        _)  = Leaf
+step (Var x    ,        _)  = Leaf
+step (Add e1 e2, Node l r)  = Node (step (e1, l)) (step (e2, r))
+step (Let e1 e2, Node l r)  = Node (step (e1, l)) (step (e2 (eval (e1, l)), r))
+step (Fix e    ,      env)  = step (fix (\e' -> e (eval (e', env))), env)
+step (Reg e    , Cons _ vs) = Cons (eval (e, vs)) (step (e, vs))
+
+acc i = Fix (\x -> Reg (Add (Var x) (Var i)))
+fib = Fix (\x -> Reg (acc x))
+pipe = Reg (Reg (Reg (Reg (Reg (Reg (Con 6))))))