blob: 0ad36c9102b3bf518e4349835b962299f6cf7a69 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
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"
|
