From 15225be21b0740db02f0841e5c8dbd5eeb8a5b69 Mon Sep 17 00:00:00 2001 From: tzlil Date: Tue, 31 Oct 2023 12:18:10 +0200 Subject: added dip --- Main.idr | 15 +++++++++++++-- 1 file 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 : ? -- cgit 1.4.1