diff options
Diffstat (limited to 'Main.idr')
| -rw-r--r-- | Main.idr | 24 |
1 files changed, 14 insertions, 10 deletions
diff --git a/Main.idr b/Main.idr index eb5ab72..89d5568 100644 --- a/Main.idr +++ b/Main.idr @@ -9,27 +9,27 @@ 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) + 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 : (forall n. {0 rest : Sig n} -> Stack (ty ++ rest) -> Stack (r ++ rest)) -> Stack ds -> Stack ((F ty r) :: ds) +quote : (Stack ty -> Stack r) -> Stack ds -> Stack ((F ty r) :: ds) quote f = PushFn f -dup : Stack (x :: rest) -> Stack (x :: x :: rest) +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 ++ rest)) -> (Stack (r ++ rest)) +call : Stack ((F f r) :: f) -> (Stack r) call (PushFn g y) = g y -pop : Stack (x :: rest) -> Stack rest +pop : Stack (x :: d) -> Stack d 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' +-- 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' @@ -46,12 +46,16 @@ 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)) +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 :: rest) -> Stack (V Nat :: rest) +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 |