blob: 89d55681ba1e8a9123841e559c03c47ae4d08f1c (
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
61
62
63
64
|
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 : Stack ty -> Stack r) -> 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 : (Stack ty -> Stack r) -> Stack ds -> Stack ((F ty r) :: ds)
quote f = PushFn f
dup : Stack (x :: ds) -> Stack (x :: x :: ds)
dup (PushVal x s) = (push x . push x) s
dup (PushFn x s) = (quote x . quote x) s
call : Stack ((F f r) :: f) -> (Stack r)
call (PushFn g y) = g y
pop : Stack (x :: d) -> Stack d
pop (PushVal x s) = s
pop (PushFn x s) = s
-- compose : (n : Nat) -> {0 s : Vect n Discrim} -> Stack ((F f r) :: (F f' 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)) -> Stack (r ++ r)
-- both (PushFn g s) = append (g (takeN n s)) (append (g (takeN n (popN n s))) (popN n (popN n s)))
-- both (PushFn g s) = append (takeN n' (?hole1 (takeN n s))) (?hole2 (takeN n (popN n s)))
both (PushFn g s) = append (g (takeN n s)) (append (g (takeN n (popN n s))) (popN n (popN n s)))
add : Stack ([V Nat, V Nat] ++ r) -> Stack ([V Nat] ++ r)
add (PushVal x z) = case z of (PushVal y st) => PushVal (x + y) st
-- specialCompose : (Stack x -> Stack y) -> (Stack x' -> y') -> (Stack ?x -> Stack ?y)
-- sum3 : ?
-- sum3 = add . add
main : IO ()
main = putStrLn "a"
|
