blob: eb5ab72ab0ac39eacb41deaeea80d2d4e0d261f9 (
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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
|
module Main
import Data.Vect
data Discrim = V Type | F (Vect n Discrim) (Vect n' Discrim)
Sig : Nat -> Type
Sig n = Vect n Discrim
data Stack : Vect n Discrim -> Type where
Bot : Stack Nil
PushVal : {0 t : Type} -> (a : t) -> (Stack d) -> Stack ((V t) :: d)
PushFn : (fn : forall n. {0 rest : Vect n Discrim} -> Stack (ty ++ rest) -> Stack (r ++ rest)) -> Stack ds -> Stack ((F ty r) :: ds)
push : {0 t : Type} -> (a : t) -> Stack d -> Stack ((V t) :: d)
push x y = PushVal x y
quote : (forall n. {0 rest : Sig n} -> Stack (ty ++ rest) -> Stack (r ++ rest)) -> Stack ds -> Stack ((F ty r) :: ds)
quote f = PushFn f
dup : Stack (x :: rest) -> Stack (x :: x :: rest)
dup (PushVal x s) = (push x . push x) s
dup (PushFn x s) = (quote x . quote x) s
call : Stack ((F f r) :: (f ++ rest)) -> (Stack (r ++ rest))
call (PushFn g y) = g y
pop : Stack (x :: rest) -> Stack rest
pop (PushVal x s) = s
pop (PushFn x s) = s
compose : Stack ((F f r) :: (F r r') :: rest) -> (Stack ((F f r') :: rest))
compose (PushFn f s) = case s of (PushFn g s') => PushFn (g . f) s'
append : Stack x -> Stack y -> Stack (x ++ y)
append Bot s' = s'
append (PushVal x s) s' = PushVal x (append s s')
append (PushFn g s) s' = PushFn g (append s s')
popN : (n : Nat) -> {0 s : Vect n Discrim} -> Stack (s ++ s') -> Stack s'
popN 0 {s = []} st = st
popN (S n) {s = _ :: _} (PushVal x st) = popN n st
popN (S n) {s = _ :: _} (PushFn x st) = popN n st
takeN : (n : Nat) -> {0 s : Vect n Discrim} -> Stack (s ++ s') -> Stack s
takeN 0 {s = []} _ = Bot
takeN (S n) {s = _ :: _} (PushVal x st) = PushVal x (takeN n st)
takeN (S n) {s = _ :: _} (PushFn x st) = PushFn x (takeN n st)
both : {n : Nat} -> {n' : Nat} -> {f : Sig n} -> {r : Sig n'} -> Stack ((F f r) :: (f ++ f ++ rest)) -> Stack (r ++ r ++ rest)
both (PushFn g s) = append (takeN n' (g s)) (g (popN n s))
add : Stack (V Nat :: V Nat :: rest) -> Stack (V Nat :: rest)
add (PushVal x z) = case z of (PushVal y st) => PushVal (x + y) st
-- sum3 : ?
-- sum3 = add . add
main : IO ()
main = putStrLn "a"
|
