From 6385ecf96cd60885c221e3144b5a5ec63eb5c831 Mon Sep 17 00:00:00 2001
From: Chloe Brown <chloe.brown.00@outlook.com>
Date: Thu, 22 Jun 2023 17:57:48 +0100
Subject: Add encodings for containers.

Remove useless junk.
---
 src/Term/Syntax.idr | 22 +++++++++++++++++++++-
 1 file changed, 21 insertions(+), 1 deletion(-)

(limited to 'src/Term/Syntax.idr')

diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index 6a05271..211e039 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -23,7 +23,7 @@ Lit (S k) = Suc (Lit k)
 
 -- HOAS
 
-infix 4 ~>*
+infixr 4 ~>*
 
 public export
 (~>*) : SnocList Ty -> Ty -> Ty
@@ -38,10 +38,28 @@ App : {sty : SnocList Ty} -> Term (sty ~>* ty) ctx -> All (flip Term ctx) sty ->
 App t [<] = t
 App t (us :< u) = App (App t us) u
 
+export
+AbsAll :
+  (sty : SnocList Ty) ->
+  (All (flip Term (ctx ++ sty)) sty -> Term ty (ctx ++ sty)) ->
+  Term (sty ~>* ty) ctx
+AbsAll [<] f = f [<]
+AbsAll (sty :< ty') f = AbsAll sty (\vars => Abs' (\x => f (mapProperty shift vars :< x)))
+
 export
 (.) : {ty, ty' : Ty} -> Term (ty' ~> ty'') ctx -> Term (ty ~> ty') ctx -> Term (ty ~> ty'') ctx
 t . u = Abs (App (shift t) [<App (shift u) [<Var Here]])
 
+export
+(.:) :
+  {sty : SnocList Ty} ->
+  {ty : Ty} ->
+  Term (ty ~> ty') ctx ->
+  Term (sty ~>* ty) ctx ->
+  Term (sty ~>* ty') ctx
+(t .: u) {sty = [<]} = App t u
+(t .: u) {sty = sty :< ty''} = Abs' (\f => shift t . f) .: u
+
 -- Incomplete Evaluation
 
 data IsFunc : FullTerm (ty ~> ty') ctx -> Type where
@@ -112,6 +130,8 @@ Rec' Zero thin u v = Just u
 Rec' (Suc t) thin u v =
   let rec = maybe (Rec (t `Over` thin) u v) id (Rec' t thin u v) in
   Just $ maybe (App v rec) id $ (App' 1 v rec)
+Rec' t thin (Zero `Over` thin1) (Const Zero `Over` thin2) =
+  Just (Zero `Over` Empty)
 Rec' t thin u v = Nothing
 
 eval' : {ty : Ty} -> (fuel : Nat) -> (ratio : Double) -> Term ty ctx -> (Nat, Term ty ctx)
-- 
cgit v1.2.3