Add sums, vectors and arithmetic encodings.

Also define pretty printing of terms.

13 files changed, 859 insertions, 46 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index ca7325c..c2a0fbb 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -7,10 +7,15 @@ options = "--total"
 depends = contrib
 
 modules
-  = Encoded.Bool
+  = Encoded.Arith
+  , Encoded.Bool
+  , Encoded.Fin
   , Encoded.Pair
+  , Encoded.Sum
   , Encoded.Union
+  , Encoded.Vect
   , Term
+  , Term.Pretty
   , Term.Semantics
   , Term.Syntax
   , Thinned
diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr
new file mode 100644
index 0000000..d2f83bc
--- /dev/null
+++ b/src/Encoded/Arith.idr
@@ -0,0 +1,81 @@
+module Encoded.Arith
+
+import Encoded.Bool
+import Encoded.Pair
+import Term.Syntax
+
+export
+rec : {ty : Ty} -> Term (N ~> ty ~> (N * ty ~> ty) ~> ty) ctx
+rec = Abs $ Abs $ Abs $
+  let n = Var $ There $ There Here in
+  let z = Var $ There Here in
+  let s = Var Here in
+  let 
+    p : Term (N * ty) (ctx :< N :< ty :< (N * ty ~> ty))
+    p = Rec n
+      (App pair [<Zero, z])
+      (Abs' (\p =>
+        App pair
+          [<Suc (App fst [<p])
+          , App (shift s) [<p]]))
+  in
+  App snd [<p]
+
+export
+plus : Term (N ~> N ~> N) ctx
+plus = Abs' (\n => Rec n Id (Abs' (Abs' Suc .)))
+
+export
+pred : Term (N ~> N) ctx
+-- pred = Abs' (\n => App rec [<n, Zero, fst])
+pred = Abs'
+  (\n => App
+    (Rec n
+      (Const Zero)
+      (Abs' (\f =>
+        Rec (App f [<Zero])
+          (Abs' (\k => Rec k (Suc Zero) (Const Zero)))
+          (Const $ Abs' (\k => Rec k (Suc Zero) (Abs' Suc . shift f))))))
+    [<Lit 1])
+
+export
+minus : Term (N ~> N ~> N) ctx
+minus = Abs $ Abs $
+  let m = Var $ There Here in
+  let n = Var Here in
+  Rec n m pred
+
+export
+mult : Term (N ~> N ~> N) ctx
+mult = Abs' (\n =>
+  Rec n
+    (Const Zero)
+    (Abs $ Abs $
+      let f = Var $ There Here in
+      let m = Var Here in
+      App plus [<m, App f [<m]]))
+
+export
+lte : Term (N ~> N ~> B) ctx
+lte = Abs' (\m => isZero . App minus [<m])
+
+export
+equal : Term (N ~> N ~> B) ctx
+equal = Abs $ Abs $
+  let m = Var $ There Here in
+  let n = Var Here in
+  App and [<App lte [<m, n], App lte [<n, m]]
+
+export
+divmod : Term (N ~> N ~> N * N) ctx
+divmod = Abs $ Abs $
+  let n = Var (There Here) in
+  let d = Var Here in
+  Rec
+    n
+    (App pair [<Zero, Zero])
+    (Abs' (\p =>
+      App if'
+        [<App lte [<shift d, App snd [<p]]
+        , App pair [<Suc (App fst [<p]), Zero]
+        , App mapSnd [<Abs' Suc, p]]))
diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
index d185856..11bb894 100644
--- a/src/Encoded/Bool.idr
+++ b/src/Encoded/Bool.idr
@@ -1,5 +1,6 @@
 module Encoded.Bool
 
+import Term.Semantics
 import Term.Syntax
 
 export
@@ -7,6 +8,15 @@ B : Ty
 B = N
 
 export
+Show (TypeOf B) where
+  show 0 = "true"
+  show (S k) = "false"
+
+export
+toBool : TypeOf B -> Bool
+toBool = (== 0)
+
+export
 True : Term B ctx
 True = Lit 0
   
@@ -20,3 +30,19 @@ if' = Abs' (\b =>
   Rec b
     (Abs $ Const $ Var Here)
     (Const $ Const $ Abs $ Var Here))
+
+export
+and : Term (B ~> B ~> B) ctx
+and = Abs' (\b => App if' [<b, Id, Const False])
+
+export
+or : Term (B ~> B ~> B) ctx
+or = Abs' (\b => App if' [<b, Const True, Id])
+
+export
+not : Term (B ~> B) ctx
+not = Abs' (\b => App if' [<b, False, True])
+
+export
+isZero : Term (N ~> B) ctx
+isZero = Id
diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr
new file mode 100644
index 0000000..901c612
--- /dev/null
+++ b/src/Encoded/Fin.idr
@@ -0,0 +1,48 @@
+module Encoded.Fin
+
+import public Data.Nat
+
+import Data.Stream
+import Encoded.Arith
+import Encoded.Pair
+import Term.Semantics
+import Term.Syntax
+
+export
+Fin : Nat -> Ty
+Fin k = N
+
+oldShow : Nat -> String
+oldShow = show
+
+export
+zero : Term (Fin (S k)) ctx
+zero = Zero
+
+export
+suc : Term (Fin k ~> Fin (S k)) ctx
+suc = Abs' Suc
+
+export
+inject : Term (Fin k ~> Fin (S k)) ctx
+inject = Id
+
+export
+absurd : {ty : Ty} -> Term (Fin 0 ~> ty) ctx
+absurd = Arb
+
+export
+induct : {ty : Ty} -> Term (Fin (S k) ~> ty ~> (Fin k * ty ~> ty) ~> ty) ctx
+induct = rec
+
+export
+forget : Term (Fin k ~> N) ctx
+forget = Id
+
+export
+allSem : (k : Nat) -> List (TypeOf (Fin k))
+allSem k = take k nats
+
+export
+divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx
+divmod' k = Abs' (\n => App divmod [<n, Lit k])
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index b2a95ab..32bb06c 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -2,6 +2,7 @@ module Encoded.Pair
 
 import Encoded.Bool
 import Encoded.Union
+import Term.Semantics
 import Term.Syntax
 
 export
@@ -9,6 +10,17 @@ export
 ty1 * ty2 = B ~> (ty1 <+> ty2)
 
 export
+[ShowPair]
+{ty1, ty2 : Ty} ->
+Show (TypeOf ty1) =>
+Show (TypeOf ty2) =>
+Show (TypeOf (ty1 * ty2)) where
+  show f = fastConcat
+    [ "(", show (sem prL [<] (f $ sem True [<]))
+    , ", ", show (sem prR [<] (f $ sem False [<]))
+    , ")"]
+
+export
 pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
 pair = Abs $ Abs $ Abs $
   let t = Var (There $ There Here) in
@@ -23,3 +35,32 @@ fst = Abs $ App (prL . Var Here) [<True]
 export
 snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
 snd = Abs $ App (prR . Var Here) [<False]
+
+export
+bimap :
+  {ty1, ty1', ty2, ty2' : Ty} ->
+  Term ((ty1 ~> ty1') ~> (ty2 ~> ty2') ~> ty1 * ty2 ~> ty1' * ty2') ctx
+bimap = Abs $ Abs $ Abs $ Abs $
+  let f = Var (There $ There $ There Here) in
+  let g = Var (There $ There Here) in
+  let x = Var (There $ Here) in
+  let b = Var Here in
+  App if'
+    [<b
+    , App (inL . f . prL . x) [<True]
+    , App (inR . g . prR . x) [<False]
+    ]
+
+export
+mapSnd : {ty1, ty2, ty2' : Ty} -> Term ((ty2 ~> ty2') ~> ty1 * ty2 ~> ty1 * ty2') ctx
+mapSnd = Abs $ Abs $
+  let f = Var (There Here) in
+  let x = Var Here in
+  App pair [<App fst [<x], App (f . snd) [<x]]
+
+export
+uncurry : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty2 ~> ty) ~> ty1 * ty2 ~> ty) ctx
+uncurry = Abs $ Abs $
+  let f = Var $ There Here in
+  let p = Var Here in
+  App f [<App fst [<p], App snd [<p]]
diff --git a/src/Encoded/Sum.idr b/src/Encoded/Sum.idr
new file mode 100644
index 0000000..e3729f9
--- /dev/null
+++ b/src/Encoded/Sum.idr
@@ -0,0 +1,80 @@
+module Encoded.Sum
+
+import public Data.List
+import public Data.List.Elem
+import public Data.List.Quantifiers
+
+import Encoded.Bool
+import Encoded.Pair
+import Encoded.Union
+import Term.Semantics
+import Term.Syntax
+
+-- Binary Sums -----------------------------------------------------------------
+
+export
+(+) : Ty -> Ty -> Ty
+ty1 + ty2 = B * (ty1 <+> ty2)
+
+export
+{ty1, ty2 : Ty} -> Show (TypeOf ty1) => Show (TypeOf ty2) => Show (TypeOf (ty1 + ty2)) where
+  show p =
+    if toBool (sem fst [<] p)
+    then fastConcat ["Left (", show (sem (prL . snd) [<] p), ")"]
+    else fastConcat ["Right (", show (sem (prR . snd) [<] p), ")"]
+
+export
+left : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 + ty2)) ctx
+left = Abs' (\t => App pair [<True, App inL [<t]])
+
+export
+right : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 + ty2)) ctx
+right = Abs' (\t => App pair [<False, App inR [<t]])
+
+export
+case' : {ty1, ty2, ty : Ty} -> Term ((ty1 + ty2) ~> (ty1 ~> ty) ~> (ty2 ~> ty) ~> ty) ctx
+case' = Abs' (\t =>
+  App if'
+    [<App fst [<t]
+    , Abs $ Const $ App (Var Here . prL . snd) [<shift t]
+    , Const $ Abs $ App (Var Here . prR . snd) [<shift t]
+    ])
+
+export
+either : {ty1, ty2, ty : Ty} -> Term ((ty1 ~> ty) ~> (ty2 ~> ty) ~> (ty1 + ty2) ~> ty) ctx
+either = Abs $ Abs $ Abs $
+  let f = Var $ There $ There Here in
+  let g = Var $ There Here in
+  let x = Var Here in
+  App case' [<x, f, g]
+
+-- N-ary Sums ------------------------------------------------------------------
+
+public export
+mapNonEmpty : NonEmpty xs -> NonEmpty (map f xs)
+mapNonEmpty IsNonEmpty = IsNonEmpty
+
+export
+Sum : (tys : List Ty) -> {auto 0 ok : NonEmpty tys} -> Ty
+Sum = foldr1 (+)
+
+export
+any :
+  {tys : List Ty} ->
+  {ty : Ty} ->
+  {auto 0 ok : NonEmpty tys} ->
+  All (\ty' => Term (ty' ~> ty) ctx) tys ->
+  Term (Sum tys ~> ty) ctx
+any [f] = f
+any (f :: fs@(_ :: _)) = App either [<f, any fs]
+
+export
+tag :
+  {tys : List Ty} ->
+  {ty : Ty} ->
+  {auto 0 ok : NonEmpty tys} ->
+  Elem ty tys ->
+  Term (ty ~> Sum tys) ctx
+tag {tys = [_]} Here = Id
+tag {tys = _ :: _ :: _} Here = left
+tag {tys = _ :: _ :: _} (There i) = right . tag i
diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
index 5c3b95c..00b07e7 100644
--- a/src/Encoded/Union.idr
+++ b/src/Encoded/Union.idr
@@ -2,6 +2,8 @@ module Encoded.Union
 
 import Term.Syntax
 
+-- Binary Union ----------------------------------------------------------------
+
 export
 (<+>) : Ty -> Ty -> Ty
 N <+> N = N
diff --git a/src/Encoded/Vect.idr b/src/Encoded/Vect.idr
new file mode 100644
index 0000000..a427196
--- /dev/null
+++ b/src/Encoded/Vect.idr
@@ -0,0 +1,66 @@
+module Encoded.Vect
+
+import Data.String
+
+import Encoded.Bool
+import Encoded.Pair
+import Encoded.Fin
+
+import Term.Semantics
+import Term.Syntax
+
+export
+Vect : Nat -> Ty -> Ty
+Vect k ty = Fin k ~> ty
+
+export
+[ShowVect]
+{k : Nat} ->
+Show (TypeOf ty) =>
+Show (TypeOf (Vect k ty)) where
+  show f = "[" ++ joinBy ", " (map (show . f) $ allSem k) ++ "]"
+
+export
+nil : {ty : Ty} -> Term (Vect 0 ty) ctx
+nil = absurd
+
+export
+cons : {k : Nat} -> {ty : Ty} -> Term (ty ~> Vect k ty ~> Vect (S k) ty) ctx
+cons = Abs $ Abs $ Abs $
+  let x = Var $ There $ There Here in
+  let xs = Var $ There Here in
+  let i = Var Here in
+  App induct [<i, x, App uncurry [<Abs $ Const $ App (shift xs) (Var Here)]]
+
+export
+tabulate : Term ((Fin k ~> ty) ~> Vect k ty) ctx
+tabulate = Id
+
+export
+dmap :
+  {k : Nat} ->
+  {ty1, ty2 : Ty} ->
+  Term ((Fin k ~> ty1 ~> ty2) ~> Vect k ty1 ~> Vect k ty2) ctx
+dmap =
+  Abs $ Abs $ Abs $
+    let f = Var (There $ There Here) in
+    let xs = Var (There Here) in
+    let i = Var Here in
+    App f [<i, App xs i]
+
+export
+map : {k : Nat} -> {ty1, ty2 : Ty} -> Term ((ty1 ~> ty2) ~> Vect k ty1 ~> Vect k ty2) ctx
+map = Abs' (\f => App dmap (Const f))
+
+export
+index : {k : Nat} -> {ty : Ty} -> Term (Vect k ty ~> Fin k ~> ty) ctx
+index = Id
+
+export
+foldr : {k : Nat} -> {ty, ty' : Ty} -> Term (ty' ~> (ty ~> ty' ~> ty') ~> Vect k ty ~> ty') ctx
+foldr {k = 0} = Abs $ Const $ Const $ Var Here
+foldr {k = S k} = Abs $ Abs $ Abs $
+  let z = Var (There $ There Here) in
+  let c = Var (There Here) in
+  let xs = Var Here in
+  App c [<App xs [<zero], App foldr [<z, c, xs . suc]]
diff --git a/src/Term.idr b/src/Term.idr
index bceecfe..e6b7466 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -340,3 +340,46 @@ substBase :
 --   (sub1 : Subst ctx ctx') ->
 --   (sub2 : Subst ctx' ctx'') ->
 --   subst (subst t sub1) sub2 <~> subst t ?d
+
+-- Utilities -------------------------------------------------------------------
+
+export
+countUses : Term ty ctx -> Elem ty' ctx -> Nat
+fullCountUses : FullTerm ty ctx -> Elem ty' ctx -> Nat
+
+countUses (t `Over` thin) i =
+  case preimage thin i of
+    Just i => fullCountUses t i
+    Nothing => 0
+
+fullCountUses Var Here = 1
+fullCountUses (Const t) i = fullCountUses t i
+fullCountUses (Abs t) i = fullCountUses t (There i)
+fullCountUses (App (MakePair t u _)) i = countUses t i + countUses u i
+fullCountUses (Suc t) i = fullCountUses t i
+fullCountUses
+  (Rec (MakePair
+    t
+    (MakePair (u `Over` thin2) (v `Over` thin3) _ `Over` thin)
+    _))
+  i =
+  countUses t i +
+  case preimage thin i of
+    Just i =>
+      (case preimage thin2 i of Just i => fullCountUses u i; Nothing => 0) +
+      (case preimage thin3 i of Just i => fullCountUses v i; Nothing => 0)
+    Nothing => 0
+
+export
+size : Term ty ctx -> Nat
+fullSize : FullTerm ty ctx -> Nat
+
+size (t `Over` thin) = fullSize t
+
+fullSize Var = 1
+fullSize (Const t) = S (fullSize t)
+fullSize (Abs t) = S (fullSize t)
+fullSize (App (MakePair t u _)) = S (size t + size u)
+fullSize Zero = 1
+fullSize (Suc t) = S (fullSize t)
+fullSize (Rec (MakePair t (MakePair u v _ `Over` _) _)) = S (size t + size u + size v)
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
diff --git a/src/Thinning.idr b/src/Thinning.idr
index 1ba5eb0..94bb705 100644
--- a/src/Thinning.idr
+++ b/src/Thinning.idr
@@ -4,6 +4,7 @@ module Thinning
 import Control.Order
 import Control.Relation
 import Data.Either
+import Data.Maybe
 import Data.Nat
 import Syntax.PreorderReasoning
 
@@ -170,12 +171,10 @@ keepEmptyIsPoint = MkEquivalence (\Here => Refl)
 export
 (.) : sy `Thins` sz -> sx `Thins` sy -> sx `Thins` sz
 Id . thin1 = thin1
-Empty . Id = Empty
-Empty . Empty = Empty
+Empty . thin1 = rewrite thinToEmpty thin1 in Empty
 Drop thin2 . Id = Drop thin2
 Drop thin2 . Empty = Empty
-Drop thin2 . Drop thin1 = Drop (thin2 . Drop thin1)
-Drop thin2 . Keep thin1 = Drop (thin2 . Keep thin1)
+Drop thin2 . thin1 = Drop (thin2 . thin1)
 Keep thin2 . Id = Keep thin2
 Keep thin2 . Empty = Empty
 Keep thin2 . Drop thin1 = Drop (thin2 . thin1)
@@ -397,16 +396,52 @@ coprod (Keep thin1) (Keep thin2) =
     , cover = coverKeepKeep cp.cover
     }
 
--- Coproduct Equivalence -------------------------------------------------------
-
-namespace Coproduct
-  public export
-  data (<~>) :
-    {0 thin1 : sx `Thins` sa} ->
-    {0 thin2 : sy `Thins` sa} ->
-    {0 thin3 : sz `Thins` sa} ->
-    {0 thin4 : sw `Thins` sa} ->
-    Coproduct thin1 thin2 ->
-    Coproduct thin3 thin4 ->
-    Type
-    where
+-- Preimage --------------------------------------------------------------------
+
+export
+preimage : sx `Thins` sy -> Elem y sy -> Maybe (Elem y sx)
+preimage Id i = Just i
+preimage Empty i = Nothing
+preimage (Drop thin) Here = Nothing
+preimage (Drop thin) (There i) = preimage thin i
+preimage (Keep thin) Here = Just Here
+preimage (Keep thin) (There i) = There <$> preimage thin i
+
+isJustMapInv : {t : Maybe a} -> IsJust (map f t) -> IsJust t
+isJustMapInv {t = Just x} ItIsJust = ItIsJust
+
+isNothingMapInv : {t : Maybe a} -> map f t = Nothing -> t = Nothing
+isNothingMapInv {t = Nothing} Refl = Refl
+
+fromJustMap :
+  (0 f : a -> b) ->
+  (t : Maybe a) ->
+  {auto 0 ok : IsJust (map f t)} ->
+  {auto 0 ok' : IsJust t} ->
+  fromJust (map f t) @{ok} = f (fromJust t @{ok'})
+fromJustMap f (Just x) = Refl
+
+export
+preimageCorrect :
+  (thin : sx `Thins` sy) ->
+  (i : Elem y sy) ->
+  {auto 0 ok : IsJust (preimage thin i)} ->
+  index thin (fromJust (preimage thin i) @{ok}) = i
+preimageCorrect Id i = Refl
+preimageCorrect (Drop thin) (There i) = cong There $ preimageCorrect thin i
+preimageCorrect (Keep thin) Here = Refl
+preimageCorrect (Keep thin) (There i) =
+  rewrite fromJustMap There (preimage thin i) {ok} {ok' = isJustMapInv ok} in
+  cong There $ preimageCorrect thin i @{isJustMapInv ok}
+
+export
+preimageMissing :
+  (thin : sx `Thins` sy) ->
+  (i : Elem y sy) ->
+  {auto 0 ok : preimage thin i = Nothing} ->
+  (j : Elem y sx) ->
+  Not (index thin j = i)
+preimageMissing (Drop thin) (There i) j prf =
+  preimageMissing thin i j (injective prf)
+preimageMissing (Keep thin) (There i) (There j) prf =
+  preimageMissing thin i @{isNothingMapInv ok} j (injective prf)