1 files changed, 13 insertions, 2 deletions
diff --git a/Main.idr b/Main.idr
index 89d5568..ee7c9a5 100644
--- a/Main.idr
+++ b/Main.idr
@@ -28,6 +28,16 @@ pop : Stack (x :: d) -> Stack d
pop (PushVal x s) = s
pop (PushFn x s) = s
+swap : Stack (x :: y :: d) -> Stack (y :: x :: d)
+swap (PushFn x (PushFn y s)) = PushFn y (PushFn x s)
+swap (PushFn x (PushVal y s)) = PushVal y (PushFn x s)
+swap (PushVal x (PushVal y s)) = PushVal y (PushVal x s)
+swap (PushVal x (PushFn y s)) = PushFn y (PushVal x s)
+
+dip : Stack ((F f r) :: x :: f) -> (Stack (x :: r))
+dip (PushFn g (PushVal x y)) = PushVal x (g y)
+dip (PushFn g (PushFn x y)) = PushFn x (g y)
+
-- 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'
@@ -46,14 +56,15 @@ 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 : {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)))
+-- 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 : ?
|
