Add encodings for containers.

Remove useless junk.

2 files changed, 26 insertions, 3 deletions

diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr
index ed2dd45..ffa88bd 100644
--- a/src/Term/Pretty.idr
+++ b/src/Term/Pretty.idr
@@ -51,6 +51,10 @@ interface Renderable (0 a : Type) where
   fromSyntax : Syntax -> a
 
 export
+Renderable () where
+  fromSyntax _ = ()
+
+export
 Renderable AnsiStyle where
   fromSyntax Bound = italic
   fromSyntax Keyword  = color Blue
@@ -150,7 +154,6 @@ parameters (names : Stream String)
   prettyFullTerm : (len : Len ctx) => Prec -> FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc Syntax
   prettyBinding : (len : Len ctx) => Prec -> Binding ty ctx' -> ctx' `Thins` ctx -> Doc Syntax
   prettySpline : (len : Len ctx) => Prec -> Spline ty ctx -> Doc Syntax
-  prettyArg : (len : Len ctx) => Term ty ctx' -> Doc Syntax
 
   prettyTerm' d (t `Over` thin) = prettyFullTerm d t thin
 
@@ -239,7 +242,7 @@ name k =
 
 export
 canonicalNames : Stream String
-canonicalNames = map (fastPack . name) nats
+canonicalNames = map (fastPack . reverse . name) nats
 
 export
 prettyTerm : Renderable ann => (len : Len ctx) => Term ty ctx -> Doc ann
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
@@ -39,9 +39,27 @@ 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)