Add sums, vectors and arithmetic encodings.

Also define pretty printing of terms.

3 files changed, 414 insertions, 28 deletions

diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr
new file mode 100644
index 0000000..ed2dd45
--- /dev/null
+++ b/src/Term/Pretty.idr
@@ -0,0 +1,246 @@
+module Term.Pretty
+
+import public Text.PrettyPrint.Prettyprinter
+import public Text.PrettyPrint.Prettyprinter.Render.Terminal
+
+import Data.Fin
+import Data.Fin.Extra
+import Data.Nat
+import Data.Stream
+import Data.String
+
+import Term
+import Term.Syntax
+
+%prefix_record_projections off
+
+data Syntax = Bound | Keyword | Symbol | Literal
+
+symbol : Doc Syntax -> Doc Syntax
+symbol = annotate Symbol
+
+keyword : Doc Syntax -> Doc Syntax
+keyword = annotate Keyword
+
+bound : Doc Syntax -> Doc Syntax
+bound = annotate Bound
+
+literal : Doc Syntax -> Doc Syntax
+literal = annotate Literal
+
+rec_ : Doc Syntax
+rec_ = keyword "rec"
+
+underscore : Doc Syntax
+underscore = bound "_"
+
+plus : Doc Syntax
+plus = symbol "+"
+
+arrow : Doc Syntax
+arrow = symbol "=>"
+
+backslash : Doc Syntax
+backslash = symbol Symbols.backslash
+
+lit : Nat -> Doc Syntax
+lit = literal . pretty
+
+public export
+interface Renderable (0 a : Type) where
+  fromSyntax : Syntax -> a
+
+export
+Renderable AnsiStyle where
+  fromSyntax Bound = italic
+  fromSyntax Keyword  = color Blue
+  fromSyntax Symbol = color BrightWhite
+  fromSyntax Literal = color Green
+
+startPrec, leftAppPrec, appPrec : Prec
+startPrec = Open
+leftAppPrec = Equal
+appPrec = App
+
+data StrictThins : SnocList a -> SnocList a -> Type where
+  Empty : [<] `StrictThins` [<]
+  Drop : sx `StrictThins` sy -> sx `StrictThins` sy :< y
+  Keep : sx `StrictThins` sy -> sx :< z `StrictThins` sy :< z
+
+%name StrictThins thin
+
+record IsBound (ty : Ty) (ctx : SnocList Ty) (t : FullTerm ty' ctx') where
+  constructor MkBound
+  {0 bound : SnocList Ty}
+  {0 used : SnocList Ty}
+  thin : used `StrictThins` bound
+  0 prfTy : ty = bound ~>* ty'
+  0 prfCtx : ctx' = ctx ++ used
+
+%name IsBound isBound
+
+record Binding (ty : Ty) (ctx : SnocList Ty) where
+  constructor MkBinding
+  {0 ty' : Ty}
+  {0 ctx' : SnocList Ty}
+  term : FullTerm ty' ctx'
+  isBound : IsBound ty ctx term
+
+%name Binding bound
+
+getBinding : (t : FullTerm ty' ctx') -> IsBound ty ctx t -> Binding ty ctx
+getBinding (Const t) isBound =
+  getBinding t (MkBound (Drop isBound.thin) isBound.prfTy isBound.prfCtx)
+getBinding (Abs {ty} t) isBound =
+  getBinding t (MkBound (Keep isBound.thin) isBound.prfTy (cong (:< ty) isBound.prfCtx))
+getBinding t isBound = MkBinding t isBound
+
+isBoundRefl : (0 t : FullTerm ty ctx) -> IsBound ty ctx t
+isBoundRefl t = MkBound {bound = [<]} Empty Refl Refl
+
+record Spline (ty : Ty) (ctx : SnocList Ty) where
+  constructor MkSpline
+  {0 tys : SnocList Ty}
+  head : Term (tys ~>* ty) ctx
+  args : All (flip Term ctx) tys
+
+%name Spline spline
+
+wkn : Spline ty ctx -> ctx `Thins` ctx' -> Spline ty ctx'
+wkn spline thin = MkSpline (wkn spline.head thin) (mapProperty (flip wkn thin) spline.args)
+
+getSpline : FullTerm ty ctx -> Spline ty ctx
+getSpline (App (MakePair (t `Over` thin) u _)) =
+  let rec = wkn (getSpline t) thin in
+  MkSpline rec.head (rec.args :< u)
+getSpline t = MkSpline (t `Over` Id) [<]
+
+getSucs : FullTerm ty ctx -> (Nat, Maybe (FullTerm ty ctx))
+getSucs Zero = (0, Nothing)
+getSucs (Suc t) = mapFst S (getSucs t)
+getSucs t = (0, Just t)
+
+public export
+data Len : SnocList a -> Type where
+  Z : Len [<]
+  S : Len sx -> Len (sx :< a)
+
+%name Len k
+
+lenToNat : Len sx -> Nat
+lenToNat Z = 0
+lenToNat (S k) = S (lenToNat k)
+
+lenSrc : sx `StrictThins` sy -> Len sx
+lenSrc Empty = Z
+lenSrc (Drop thin) = lenSrc thin
+lenSrc (Keep thin) = S (lenSrc thin)
+
+strictSrc : Len sz -> sx `StrictThins` sy  -> Len (sz ++ sx)
+strictSrc k Empty = k
+strictSrc k (Drop thin) = strictSrc k thin
+strictSrc k (Keep thin) = S (strictSrc k thin)
+
+extend : sx `Thins` sy -> Len sz -> sx ++ sz `Thins` sy ++ sz
+extend thin Z = thin
+extend thin (S k) = Keep (extend thin k)
+
+parameters (names : Stream String)
+  prettyTerm' : (len : Len ctx) => Prec -> Term ty ctx -> Doc Syntax
+  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
+
+  prettyFullTerm d Var thin =
+    bound (pretty $ index (minus (lenToNat len) (S $ elemToNat $ index thin Here)) names)
+  prettyFullTerm d t@(Const _) thin =
+    prettyBinding d (assert_smaller t $ getBinding t $ isBoundRefl t) thin
+  prettyFullTerm d t@(Abs _) thin =
+    prettyBinding d (assert_smaller t $ getBinding t $ isBoundRefl t) thin
+  prettyFullTerm d t@(App _) thin =
+    prettySpline d (assert_smaller t $ wkn (getSpline t) thin)
+  prettyFullTerm d Zero thin = lit 0
+  prettyFullTerm d (Suc t) thin =
+    let (n, t') = getSucs t in
+    case t' of
+      Just t' =>
+        parenthesise (d >= appPrec) $ group $
+          lit (S n) <++> plus <++> prettyFullTerm leftAppPrec (assert_smaller t t') thin
+      Nothing => lit (S n)
+  prettyFullTerm d t@(Rec _) thin =
+    prettySpline d (assert_smaller t $ wkn (getSpline t) thin)
+
+  prettyBinding d (MkBinding t {ctx' = ctx'_} (MkBound thin' _ prfCtx)) thin =
+    parenthesise (d > startPrec) $ group $ align $ hang 2 $
+      Pretty.backslash <+> snd (prettyThin (lenToNat len) thin') <++> arrow <+> line <+>
+        prettyFullTerm @{strictSrc len thin'} Open t
+          (rewrite prfCtx in extend thin $ lenSrc thin')
+    where
+    prettyThin : Nat -> sx `StrictThins` sy -> (Nat, Doc Syntax)
+    prettyThin n Empty = (n, neutral)
+    prettyThin n (Drop Empty) = (n, underscore)
+    prettyThin n (Keep Empty) = (S n, bound (pretty $ index n names))
+    prettyThin n (Drop thin) =
+      let (k, doc) = prettyThin n thin in
+      (k, doc <+> comma <++> underscore)
+    prettyThin n (Keep thin) =
+      let (k, doc) = prettyThin n thin in
+      (S k, doc <+> comma <++> bound (pretty $ index k names))
+
+  prettySpline d
+    s@(MkSpline (Rec (MakePair t (MakePair u v _ `Over` thin2) _) `Over` thin1) args) =
+      parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+        (rec_ <++> prettyTerm' appPrec (assert_smaller s $ wkn t thin1)) <+> line <+>
+        vsep
+          ([prettyTerm' appPrec (assert_smaller s $ wkn u (thin1 . thin2))
+          , prettyTerm' appPrec (assert_smaller s $ wkn v (thin1 . thin2))] ++
+            toList (forget $ mapProperty (assert_total $ prettyTerm' appPrec) args))
+  prettySpline d s@(MkSpline t args) =
+    parenthesise (d >= appPrec) $ group $ align $ hang 2 $
+      prettyTerm' leftAppPrec t <+> line <+>
+      vsep (toList $ forget $ mapProperty (assert_total $ prettyTerm' appPrec) args)
+
+finToChar : Fin 26 -> Char
+finToChar 0 = 'x'
+finToChar 1 = 'y'
+finToChar 2 = 'z'
+finToChar 3 = 'a'
+finToChar 4 = 'b'
+finToChar 5 = 'c'
+finToChar 6 = 'd'
+finToChar 7 = 'e'
+finToChar 8 = 'f'
+finToChar 9 = 'g'
+finToChar 10 = 'h'
+finToChar 11 = 'i'
+finToChar 12 = 'j'
+finToChar 13 = 'k'
+finToChar 14 = 'l'
+finToChar 15 = 'm'
+finToChar 16 = 'n'
+finToChar 17 = 'o'
+finToChar 18 = 'p'
+finToChar 19 = 'q'
+finToChar 20 = 'r'
+finToChar 21 = 's'
+finToChar 22 = 't'
+finToChar 23 = 'u'
+finToChar 24 = 'v'
+finToChar 25 = 'w'
+
+name : Nat -> List Char
+name k =
+  case divMod k 26 of
+    Fraction k 26 0 r prf => [finToChar r]
+    Fraction k 26 (S q) r prf => finToChar r :: name (assert_smaller k q)
+
+export
+canonicalNames : Stream String
+canonicalNames = map (fastPack . name) nats
+
+export
+prettyTerm : Renderable ann => (len : Len ctx) => Term ty ctx -> Doc ann
+prettyTerm t = map fromSyntax (prettyTerm' canonicalNames Open t)
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index eeb2210..2e61040 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -1,6 +1,8 @@
 module Term.Semantics
 
+import Control.Monad.Identity
 import Term
+
 import public Data.SnocList.Quantifiers
 
 public export
@@ -12,27 +14,55 @@ rec : Nat -> a -> (a -> a) -> a
 rec 0 x f = x
 rec (S k) x f = f (rec k x f)
 
-fullSem : FullTerm ty ctx -> ctx `Thins` ctx' -> All TypeOf ctx' -> TypeOf ty
-fullSem Var thin ctx = indexAll (index thin Here) ctx
-fullSem (Const t) thin ctx = const (fullSem t thin ctx)
-fullSem (Abs t) thin ctx = \v => fullSem t (Keep thin) (ctx :< v)
-fullSem (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin ctx =
-  fullSem t (thin . thin1) ctx (fullSem u (thin . thin2) ctx)
-fullSem Zero thin ctx = 0
-fullSem (Suc t) thin ctx = S (fullSem t thin ctx)
-fullSem
-  (Rec (MakePair
-    (t `Over` thin1)
-    (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin')
-    _))
-  thin
-  ctx =
-  let thin' = thin . thin' in
-  rec
-    (fullSem t (thin . thin1) ctx)
-    (fullSem u (thin' . thin2) ctx)
-    (fullSem v (thin' . thin3) ctx)
+%inline
+init : All p (sx :< x) -> All p sx
+init (psx :< px) = psx
+
+%inline
+mapInit : (All p sx -> All p sy) -> All p (sx :< z) -> All p (sy :< z)
+mapInit f (psx :< px) = f psx :< px
+
+restrict : Applicative m => sx `Thins` sy -> m (All p sy -> All p sx)
+restrict Id = pure id
+restrict Empty = pure (const [<])
+restrict (Drop thin) = [| restrict thin . [| init |] |]
+restrict (Keep thin) = [| mapInit (restrict thin) |]
+
+%inline
+indexVar : All p [<x] -> p x
+indexVar [<px] = px
+
+%inline
+sem' : Monad m => Term ty ctx -> m (All TypeOf ctx -> TypeOf ty)
+fullSem' : Monad m => FullTerm ty ctx -> m (All TypeOf ctx -> TypeOf ty)
+
+sem' (t `Over` thin) = [| fullSem' t . restrict thin |]
+
+fullSem' Var = pure indexVar
+fullSem' (Const t) = do
+  t <- fullSem' t
+  pure (const . t)
+fullSem' (Abs t) = do
+  t <- fullSem' t
+  pure (t .: (:<))
+fullSem' (App (MakePair t u _)) = do
+  t <- sem' t
+  u <- sem' u
+  pure (\ctx => t ctx (u ctx))
+fullSem' Zero = pure (const 0)
+fullSem' (Suc t) = do
+  t <- fullSem' t
+  pure (S . t)
+fullSem' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) = do
+  t <- sem' t
+  u <- sem' u
+  v <- sem' v
+  f <- restrict thin
+  pure
+    (\ctx =>
+      let ctx' = f ctx in
+      rec (t ctx) (u ctx') (v ctx'))
 
 export
 sem : Term ty ctx -> All TypeOf ctx -> TypeOf ty
-sem (t `Over` thin) ctx = fullSem t thin ctx
+sem t = runIdentity (sem' t)
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index a990600..6a05271 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -3,6 +3,8 @@ module Term.Syntax
 import public Data.SnocList
 import public Term
 
+%prefix_record_projections off
+
 -- Combinators
 
 export
@@ -32,16 +34,124 @@ Abs' : (Term ty (ctx :< ty) -> Term ty' (ctx :< ty)) -> Term (ty ~> ty') ctx
 Abs' f = Abs (f $ Var Here)
 
 export
-App' : {ty : Ty} -> Term (ty ~> ty') ctx -> Term ty ctx -> Term ty' ctx
-App' (Const t `Over` thin) u = t `Over` thin
-App' (Abs t `Over` thin) u = subst (t `Over` Keep thin) (Base Id :< u)
-App' t u = App t u
-
-export
 App : {sty : SnocList Ty} -> Term (sty ~>* ty) ctx -> All (flip Term ctx) sty -> Term ty ctx
 App t [<] = t
-App t (us :< u) = App' (App t us) u
+App t (us :< u) = App (App t us) u
 
 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]])
+
+-- Incomplete Evaluation
+
+data IsFunc : FullTerm (ty ~> ty') ctx -> Type where
+  ConstFunc : (t : FullTerm ty' ctx) -> IsFunc (Const t)
+  AbsFunc : (t : FullTerm ty' (ctx :< ty)) -> IsFunc (Abs t)
+
+isFunc : (t : FullTerm (ty ~> ty') ctx) -> Maybe (IsFunc t)
+isFunc Var = Nothing
+isFunc (Const t) = Just (ConstFunc t)
+isFunc (Abs t) = Just (AbsFunc t)
+isFunc (App x) = Nothing
+isFunc (Rec x) = Nothing
+
+app :
+  (ratio : Double) ->
+  {ty : Ty} ->
+  (t : Term (ty ~> ty') ctx) ->
+  {auto 0 ok : IsFunc t.value} ->
+  Term ty ctx ->
+  Maybe (Term ty' ctx)
+app ratio (Const t `Over` thin) u = Just (t `Over` thin)
+app ratio (Abs t `Over` thin) u =
+  let uses = countUses (t `Over` Id) Here in
+  let sizeU = size u in
+  if cast (sizeU * uses) <= cast (S (sizeU + uses)) * ratio
+  then
+    Just (subst (t `Over` Keep thin) (Base Id :< u))
+  else
+    Nothing
+
+App' :
+  {ty : Ty} ->
+  (ratio : Double) ->
+  Term (ty ~> ty') ctx ->
+  Term ty ctx ->
+  Maybe (Term ty' ctx)
+App' ratio
+  (Rec (MakePair
+    t
+    (MakePair (u `Over` thin2) (Const v `Over` thin3) _ `Over` thin')
+    _) `Over` thin)
+  arg =
+  case (isFunc u, isFunc v) of
+    (Just ok1, Just ok2) =>
+      let thinA = thin . thin' . thin2 in
+      let thinB = thin . thin' . thin3 in
+      case (app ratio (u `Over` thinA) arg , app ratio (v `Over` thinB) arg)
+      of
+        (Just u, Just v) => Just (Rec (wkn t thin) u (Const v))
+        (Just u, Nothing) => Just (Rec (wkn t thin) u (Const $ App (v `Over` thinB) arg))
+        (Nothing, Just v) => Just (Rec (wkn t thin) (App (u `Over` thinA) arg) (Const v))
+        (Nothing, Nothing) =>
+          Just (Rec (wkn t thin) (App (u `Over` thinA) arg) (Const $ App (v `Over` thinB) arg))
+    _ => Nothing
+App' ratio t arg =
+  case isFunc t.value of
+    Just _ => app ratio t arg
+    Nothing => Nothing
+
+Rec' :
+  {ty : Ty} ->
+  FullTerm N ctx' ->
+  ctx' `Thins` ctx ->
+  Term ty ctx ->
+  Term (ty ~> ty) ctx ->
+  Maybe (Term ty ctx)
+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 u v = Nothing
+
+eval' : {ty : Ty} -> (fuel : Nat) -> (ratio : Double) -> Term ty ctx -> (Nat, Term ty ctx)
+fullEval' : {ty : Ty} -> (fuel : Nat) -> (ratio : Double) -> FullTerm ty ctx -> (Nat, Term ty ctx)
+
+eval' fuel r (t `Over` thin) = mapSnd (flip wkn thin) (fullEval' fuel r t)
+
+fullEval' 0 r t = (0, t `Over` Id)
+fullEval' fuel@(S f) r Var = (fuel, Var `Over` Id)
+fullEval' fuel@(S f) r (Const t) = mapSnd Const (fullEval' fuel r t)
+fullEval' fuel@(S f) r (Abs t) = mapSnd Abs (fullEval' fuel r t)
+fullEval' fuel@(S f) r (App (MakePair t u _)) =
+  case App' r t u of
+    Just t => (f, t)
+    Nothing =>
+      let (fuel', t) = eval' f r t in
+      let (fuel', u) = eval' (assert_smaller fuel fuel') r u in
+      (fuel', App t u)
+fullEval' fuel@(S f) r Zero = (fuel, Zero `Over` Id)
+fullEval' fuel@(S f) r (Suc t) = mapSnd Suc (fullEval' fuel r t)
+fullEval' fuel@(S f) r (Rec (MakePair t (MakePair u v _ `Over` thin) _)) =
+  case Rec' t.value t.thin (wkn u thin) (wkn v thin) of
+    Just t => (f, t)
+    Nothing =>
+      let (fuel', t) = eval' f r t in
+      let (fuel', u) = eval' (assert_smaller fuel fuel') r u in
+      let (fuel', v) = eval' (assert_smaller fuel fuel') r v in
+      (fuel', Rec t (wkn u thin) (wkn v thin))
+
+export
+eval :
+  {ty : Ty} ->
+  {default 1.5 ratio : Double} ->
+  {default 20000 fuel : Nat} ->
+  Term ty ctx ->
+  Term ty ctx
+eval t = loop fuel t
+  where
+  loop : Nat -> Term ty ctx -> Term ty ctx
+  loop fuel t =
+    case eval' fuel ratio t of
+      (0, t) => t
+      (S f, t) => loop (assert_smaller fuel f) t