Define semantics and encode types up to pairs.

9 files changed, 192 insertions, 13 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index 54b7dcc..ca7325c 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -7,4 +7,12 @@ options = "--total"
 depends = contrib
 
 modules
-  = Thinning
+  = Encoded.Bool
+  , Encoded.Pair
+  , Encoded.Union
+  , Term
+  , Term.Semantics
+  , Term.Syntax
+  , Thinned
+  , Thinning
+  , Type
diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr
new file mode 100644
index 0000000..d185856
--- /dev/null
+++ b/src/Encoded/Bool.idr
@@ -0,0 +1,22 @@
+module Encoded.Bool
+
+import Term.Syntax
+
+export
+B : Ty
+B = N
+
+export
+True : Term B ctx
+True = Lit 0
+  
+export
+False : Term B ctx
+False = Lit 1
+
+export
+if' : Term (B ~> ty ~> ty ~> ty) ctx
+if' = Abs' (\b =>
+  Rec b
+    (Abs $ Const $ Var Here)
+    (Const $ Const $ Abs $ Var Here))
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
new file mode 100644
index 0000000..b2a95ab
--- /dev/null
+++ b/src/Encoded/Pair.idr
@@ -0,0 +1,25 @@
+module Encoded.Pair
+
+import Encoded.Bool
+import Encoded.Union
+import Term.Syntax
+
+export
+(*) : Ty -> Ty -> Ty
+ty1 * ty2 = B ~> (ty1 <+> ty2)
+
+export
+pair : {ty1, ty2 : Ty} -> Term (ty1 ~> ty2 ~> (ty1 * ty2)) ctx
+pair = Abs $ Abs $ Abs $
+  let t = Var (There $ There Here) in
+  let u = Var (There Here) in
+  let b = Var Here in
+  App if' [<b, App inL [<t], App inR [<u]]
+
+export
+fst : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty1) ctx
+fst = Abs $ App (prL . Var Here) [<True]
+
+export
+snd : {ty1, ty2 : Ty} -> Term ((ty1 * ty2) ~> ty2) ctx
+snd = Abs $ App (prR . Var Here) [<False]
diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
new file mode 100644
index 0000000..5c3b95c
--- /dev/null
+++ b/src/Encoded/Union.idr
@@ -0,0 +1,40 @@
+module Encoded.Union
+
+import Term.Syntax
+
+export
+(<+>) : Ty -> Ty -> Ty
+N <+> N = N
+N <+> (ty2 ~> ty2') = ty2 ~> (N <+> ty2')
+(ty1 ~> ty1') <+> N = ty1 ~> (ty1' <+> N)
+(ty1 ~> ty1') <+> (ty2 ~> ty2') = (ty1 <+> ty2) ~> (ty1' <+> ty2')
+
+export
+swap : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> (ty2 <+> ty1)) ctx
+swap {ty1 = N, ty2 = N} = Id
+swap {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\f => swap . f)
+swap {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\f => swap . f)
+swap {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\f => swap . f . swap)
+
+export
+inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx
+export
+prL : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty1) ctx
+
+inL {ty1 = N, ty2 = N} = Id
+inL {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\n => Const (App inL [<n]))
+inL {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\f => inL . f)
+inL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\f => inL . f . prL)
+
+prL {ty1 = N, ty2 = N} = Id
+prL {ty1 = N, ty2 = ty2 ~> ty2'} = Abs' (\t => App prL [<App t [<Arb]])
+prL {ty1 = ty1 ~> ty1', ty2 = N} = Abs' (\t => prL . t)
+prL {ty1 = ty1 ~> ty1', ty2 = ty2 ~> ty2'} = Abs' (\t => prL . t . inL)
+
+export
+inR : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 <+> ty2)) ctx
+inR = swap . inL
+
+export
+prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx
+prR = prL . swap
diff --git a/src/Term.idr b/src/Term.idr
index e9f6b1f..bceecfe 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -74,12 +74,15 @@ namespace Smart
 
   export
   varCong : {0 i, j : Elem ty ctx} -> i = j -> Var i <~> Var j
+  varCong Refl = irrelevantEquiv reflexive
 
   export
   shiftVar : (i : Elem ty ctx) -> shift (Var i) <~> Var (There i)
+  shiftVar i = UpToThin (dropPoint i)
 
   export
   constCong : {0 t, u : Term ty' ctx} -> t <~> u -> Const t <~> Const u
+  constCong prf = mapCong Const prf
 
   export
   absCong : {0 t, u : Term ty' (ctx :< ty)} -> t <~> u -> Abs t <~> Abs u
@@ -94,6 +97,7 @@ namespace Smart
 
   export
   sucCong : {0 t, u : Term N ctx} -> t <~> u -> Suc t <~> Suc u
+  sucCong prf = mapCong Suc prf
 
   export
   recCong :
@@ -104,9 +108,6 @@ namespace Smart
     t2 <~> u2 ->
     t3 <~> u3 ->
     Rec t1 t2 t3 <~> Rec u1 u2 u3
-  recCong prf1 prf2 prf3 =
-    mapCong Rec
-      ?recCong_rhs_1
 
 -- Substitution Definition -----------------------------------------------------
 
@@ -333,9 +334,9 @@ substBase :
   (thin : ctx `Thins` ctx') ->
   subst t (Base thin) <~> wkn t thin
 
-export
-substHomo :
-  (t : Term ty ctx) ->
-  (sub1 : Subst ctx ctx') ->
-  (sub2 : Subst ctx' ctx'') ->
-  subst (subst t sub1) sub2 <~> subst t ?d
+-- export
+-- substHomo :
+--   (t : Term ty ctx) ->
+--   (sub1 : Subst ctx ctx') ->
+--   (sub2 : Subst ctx' ctx'') ->
+--   subst (subst t sub1) sub2 <~> subst t ?d
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
new file mode 100644
index 0000000..eeb2210
--- /dev/null
+++ b/src/Term/Semantics.idr
@@ -0,0 +1,38 @@
+module Term.Semantics
+
+import Term
+import public Data.SnocList.Quantifiers
+
+public export
+TypeOf : Ty -> Type
+TypeOf N = Nat
+TypeOf (ty ~> ty') = TypeOf ty -> TypeOf ty'
+
+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)
+
+export
+sem : Term ty ctx -> All TypeOf ctx -> TypeOf ty
+sem (t `Over` thin) ctx = fullSem t thin ctx
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
new file mode 100644
index 0000000..a990600
--- /dev/null
+++ b/src/Term/Syntax.idr
@@ -0,0 +1,47 @@
+module Term.Syntax
+
+import public Data.SnocList
+import public Term
+
+-- Combinators
+
+export
+Id : Term (ty ~> ty) ctx
+Id = Abs (Var Here)
+
+export
+Arb : {ty : Ty} -> Term ty ctx
+Arb {ty = N} = Zero
+Arb {ty = ty ~> ty'} = Const Arb
+
+export
+Lit : Nat -> Term N ctx
+Lit 0 = Zero
+Lit (S k) = Suc (Lit k)
+
+-- HOAS
+
+infix 4 ~>*
+
+public export
+(~>*) : SnocList Ty -> Ty -> Ty
+sty ~>* ty = foldr (~>) ty sty
+
+export
+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
+
+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]])
diff --git a/src/Thinned.idr b/src/Thinned.idr
index 7f5d2ac..184c44d 100644
--- a/src/Thinned.idr
+++ b/src/Thinned.idr
@@ -136,5 +136,3 @@ mkPairCong :
   v1 <~> w1 ->
   v2 <~> w2 ->
   MkPair v1 v2 <~> MkPair w1 w2
-mkPairCong (UpToThin prf1) (UpToThin prf2) =
-  ?mkPairCong_rhs_1
diff --git a/src/Type.idr b/src/Type.idr
index 12c0a74..c4ab809 100644
--- a/src/Type.idr
+++ b/src/Type.idr
@@ -1,6 +1,6 @@
 module Type
 
-infix 4 ~>
+infixr 4 ~>
 
 public export
 data Ty : Type where