From bfba7ed3c41c01ba41b2c5d61c223a17abba3e10 Mon Sep 17 00:00:00 2001
From: tzlil <tzlils@protonmail.com>
Date: Thu, 26 Oct 2023 23:53:30 +0300
Subject: implement both, rework some stuff

---
 Main.idr | 56 +++++++++++++++++++++++++++++++++++++++++++-------------
 1 file changed, 43 insertions(+), 13 deletions(-)

diff --git a/Main.idr b/Main.idr
index 0ad36c9..eb5ab72 100644
--- a/Main.idr
+++ b/Main.idr
@@ -1,30 +1,60 @@
 module Main
+import Data.Vect
 
-data Discrim = V Type | F (List Discrim) Discrim
+data Discrim = V Type | F (Vect n Discrim) (Vect n' Discrim)
 
-Sig : Type
-Sig = List Discrim
+Sig : Nat -> Type
+Sig n = Vect n Discrim
 
-data Stack : List Discrim -> Type where
-    Bot : Stack []
-    PushVal : {t : Type} -> (a : t) -> (Stack d) -> Stack ((V t) :: d)
-    PushFn : {ty : Sig} -> {r : Discrim} -> (fn : {other : Sig} -> Stack (ty ++ other) -> Stack (r :: other)) -> (Stack ds) -> Stack ((F ty r) :: ds)
+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 : {t : Type} -> (a : t) -> Stack d -> Stack ((V t) :: d)
+push : {0 t : Type} -> (a : t) -> Stack d -> Stack ((V t) :: d)
 push x y = PushVal x y
 
-quote : {ty : Sig} -> {r : Discrim} -> ({d : Sig} -> Stack (ty ++ d) -> Stack (r :: d)) -> Stack ds -> Stack ((F ty r) :: ds)
+quote : (forall n. {0 rest : Sig n} -> Stack (ty ++ rest) -> Stack (r ++ rest)) -> Stack ds -> Stack ((F ty r) :: ds)
 quote f = PushFn f
 
-call : {rest :Sig} -> Stack ((F f r) :: (f ++ rest)) -> (Stack (r :: rest))
+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
 
--- compose : {rest :Sig} -> Stack ((F f r) :: (F g r') :: (f ++ g ++ rest)) -> (Stack ((F ) :: rest))
--- compose (PushFn f s) = case s of (PushFn g s') => quote {ty = ?idk} (f . g) s'
+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)
 
-add : {other : Sig} -> Stack (V Nat :: V Nat :: other) -> Stack (V Nat :: other)
+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"
\ No newline at end of file
-- 
cgit 1.4.1