initial commit

1 files changed, 30 insertions, 0 deletions

diff --git a/Main.idr b/Main.idr
new file mode 100644
index 0000000..0ad36c9
--- /dev/null
+++ b/Main.idr
@@ -0,0 +1,30 @@
+module Main
+
+data Discrim = V Type | F (List Discrim) Discrim
+
+Sig : Type
+Sig = List Discrim
+
+data Stack : List Discrim -> Type where
+    Bot : Stack []
+    PushVal : {t : Type} -> (a : t) -> (Stack d) -> Stack ((V t) :: d)
+    PushFn : {ty : Sig} -> {r : Discrim} -> (fn : {other : Sig} -> Stack (ty ++ other) -> Stack (r :: other)) -> (Stack ds) -> Stack ((F ty r) :: ds)
+
+push : {t : Type} -> (a : t) -> Stack d -> Stack ((V t) :: d)
+push x y = PushVal x y
+
+quote : {ty : Sig} -> {r : Discrim} -> ({d : Sig} -> Stack (ty ++ d) -> Stack (r :: d)) -> Stack ds -> Stack ((F ty r) :: ds)
+quote f = PushFn f
+
+call : {rest :Sig} -> Stack ((F f r) :: (f ++ rest)) -> (Stack (r :: rest))
+call (PushFn g y) = g y
+
+-- compose : {rest :Sig} -> Stack ((F f r) :: (F g r') :: (f ++ g ++ rest)) -> (Stack ((F ) :: rest))
+-- compose (PushFn f s) = case s of (PushFn g s') => quote {ty = ?idk} (f . g) s'
+
+
+add : {other : Sig} -> Stack (V Nat :: V Nat :: other) -> Stack (V Nat :: other)
+add (PushVal x z) = case z of (PushVal y st) =>  PushVal (x + y) st
+
+main : IO ()
+main = putStrLn "a"
\ No newline at end of file