Make unions a pseudo-built-in type.

10 files changed, 89 insertions, 50 deletions

diff --git a/church-eval.ipkg b/church-eval.ipkg
index 80fc5f5..1e7ccd1 100644
--- a/church-eval.ipkg
+++ b/church-eval.ipkg
@@ -13,7 +13,6 @@ modules
   , Encoded.Fin
   , Encoded.Pair
   , Encoded.Sum
-  , Encoded.Union
   , Encoded.Vect
   , Term
   , Term.Compile
diff --git a/src/Encoded/Pair.idr b/src/Encoded/Pair.idr
index 42adde5..5873e40 100644
--- a/src/Encoded/Pair.idr
+++ b/src/Encoded/Pair.idr
@@ -1,7 +1,6 @@
 module Encoded.Pair
 
 import Encoded.Bool
-import Encoded.Union
 import Term.Syntax
 
 export
diff --git a/src/Encoded/Sum.idr b/src/Encoded/Sum.idr
index 6c6da6a..fd0543a 100644
--- a/src/Encoded/Sum.idr
+++ b/src/Encoded/Sum.idr
@@ -4,7 +4,6 @@ import public Data.SnocList.Operations
 
 import Encoded.Bool
 import Encoded.Pair
-import Encoded.Union
 import Term.Syntax
 
 -- Binary Sums -----------------------------------------------------------------
diff --git a/src/Encoded/Union.idr b/src/Encoded/Union.idr
deleted file mode 100644
index 00b07e7..0000000
--- a/src/Encoded/Union.idr
+++ /dev/null
@@ -1,42 +0,0 @@
-module Encoded.Union
-
-import Term.Syntax
-
--- Binary Union ----------------------------------------------------------------
-
-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 96a0cb5..f6fecbb 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -23,6 +23,11 @@ data Operator : List Ty -> Ty -> Type where
   Minus : Operator [N, N] N
   Div : Operator [N, N] N
   Mod : Operator [N, N] N
+  Inl : (ty, ty' : Ty) -> Operator [ty] (ty <+> ty')
+  Inr : (ty, ty' : Ty) -> Operator [ty'] (ty <+> ty')
+  Prl : (ty, ty' : Ty) -> Operator [ty <+> ty'] ty
+  Prr : (ty, ty' : Ty) -> Operator [ty <+> ty'] ty'
+  Arb : (ty : Ty) -> Operator [] ty
 
 %name Operator op
 
diff --git a/src/Term/Compile.idr b/src/Term/Compile.idr
index b29a6e9..2779ee3 100644
--- a/src/Term/Compile.idr
+++ b/src/Term/Compile.idr
@@ -14,9 +14,15 @@ import Term.Syntax
 
 %prefix_record_projections off
 
+const_ : Doc ann
+const_ = "const"
+
 rec_ : Doc ann
 rec_ = "squid-rec"
 
+identity_ : Doc ann
+identity_ = "squid-identity"
+
 underscore : Doc ann
 underscore = "_"
 
@@ -29,6 +35,10 @@ lambda = "lambda"
 lit : Nat -> Doc ann
 lit = pretty
 
+compileArb : Ty -> Doc ann
+compileArb N = pretty 0
+compileArb (ty ~> ty') = parens $ group $ "const" <+> softline <+> compileArb ty'
+
 compileOp : Operator tys ty -> Doc ann
 compileOp (Lit n) = lit n
 compileOp Suc = "1+"
@@ -38,6 +48,11 @@ compileOp Pred = "1-" -- Confusing name, but correct
 compileOp Minus = "squid-minus"
 compileOp Div = "squid-div"
 compileOp Mod = "squid-mod"
+compileOp (Inl _ _) = identity_
+compileOp (Inr _ _) = identity_
+compileOp (Prl _ _) = identity_
+compileOp (Prr _ _) = identity_
+compileOp (Arb ty) = compileArb ty
 
 parameters (names : Stream String)
   compileFullTerm : (len : Len ctx) => FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc ann
@@ -45,12 +60,17 @@ parameters (names : Stream String)
     pretty $ index (minus (lenToNat len) (S $ elemToNat $ index thin Here)) names
   compileFullTerm (Const t) thin =
     parens $ group $ hang 2 $
-      lambda <++> (parens $ underscore) <+> line <+>
+      const_ <+> line <+>
       compileFullTerm t thin
+  -- compileFullTerm (Abs Var) thin = identity_
   compileFullTerm (Abs t) thin =
     parens $ group $ hang 2 $
       lambda <++> (parens $ pretty $ index (lenToNat len) names) <+> line <+>
       compileFullTerm t (Keep thin)
+  -- compileFullTerm (App (MakePair (Const t `Over` thin1) (u `Over` thin2) _)) thin =
+  --   compileFullTerm t (thin . thin1)
+  -- compileFullTerm (App (MakePair (Abs Var `Over` thin1) (u `Over` thin2) _)) thin =
+  --   compileFullTerm u (thin . thin2)
   compileFullTerm (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) thin =
     parens $ group $ align $
       compileFullTerm t (thin . thin1) <+> line <+>
@@ -105,6 +125,10 @@ data ProfileMode = Run | Profile
 
 builtins : String
 builtins = """
+  (define-module (squid-module)
+    #:use-module (statprof)
+    #:declarative? #t)
+
   (define (squid-rec n z s)
     (let loop ((k 0) (acc z))
       (if (= k n)
@@ -116,6 +140,7 @@ builtins = """
   (define (squid-minus m) (lambda (n) (- m n)))
   (define (squid-div m) (lambda (n) (euclidean-quotient m n)))
   (define (squid-mod m) (lambda (n) (euclidean-remainder m n)))
+  (define (squid-identity x) x)
   """
 
 wrap_main : Len ctx => Term ty ctx -> Doc ann
@@ -130,7 +155,6 @@ run_main Run = """
   (newline)
   """
 run_main Profile = """
-  (use-modules (statprof))
   (statprof squid-main)
   """
 
diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr
index cd7ed6f..043d478 100644
--- a/src/Term/Pretty.idr
+++ b/src/Term/Pretty.idr
@@ -152,6 +152,11 @@ prettyOp Pred = keyword "pred"
 prettyOp Minus = keyword "minus"
 prettyOp Div = keyword "div"
 prettyOp Mod = keyword "mod"
+prettyOp (Inl _ _) = keyword "inl"
+prettyOp (Inr _ _) = keyword "inr"
+prettyOp (Prl _ _) = keyword "prl"
+prettyOp (Prr _ _) = keyword "prr"
+prettyOp (Arb _) = keyword "arb"
 
 parameters (names : Stream String)
   prettyTerm' : (len : Len ctx) => Prec -> Term ty ctx -> Doc Syntax
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index 62e2be7..c31a9e6 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -33,6 +33,29 @@ restrict (Keep thin) = [| mapInit (restrict thin) |]
 indexVar : All p [<x] -> p x
 indexVar [<px] = px
 
+arb : (ty : Ty) -> TypeOf ty
+arb N = 0
+arb (ty ~> ty') = const (arb ty')
+
+swap : (ty1, ty2 : Ty) -> TypeOf (ty1 <+> ty2) -> TypeOf (ty2 <+> ty1)
+swap N N = id
+swap N (ty2 ~> ty2') = (swap N ty2' .)
+swap (ty1 ~> ty1') N = (swap ty1' N .)
+swap (ty1 ~> ty1') (ty2 ~> ty2') = (swap ty1' ty2' .) . (. swap ty2 ty1)
+
+inl : (ty1, ty2 : Ty) -> TypeOf ty1 -> TypeOf (ty1 <+> ty2)
+prl : (ty1, ty2 : Ty) -> TypeOf (ty1 <+> ty2) -> TypeOf ty1
+
+inl N N = id
+inl N (ty2 ~> ty2') = const . inl N ty2'
+inl (ty1 ~> ty1') N = (inl ty1' N .)
+inl (ty1 ~> ty1') (ty2 ~> ty2') = (inl ty1' ty2' .) . (. prl ty1 ty2)
+
+prl N N = id
+prl N (ty2 ~> ty2') = prl N ty2' . ($ arb ty2)
+prl (ty1 ~> ty1') N = (prl ty1' N .)
+prl (ty1 ~> ty1') (ty2 ~> ty2') = (prl ty1' ty2' .) . (. inl ty1 ty2)
+
 %inline
 opSem : Operator tys ty -> TypeOf (foldr (~>) ty tys)
 opSem (Lit n) = n
@@ -43,6 +66,11 @@ opSem Pred = pred
 opSem Minus = minus
 opSem Div = div
 opSem Mod = mod
+opSem (Inl ty1 ty2) = inl ty1 ty2
+opSem (Inr ty1 ty2) = swap ty2 ty1 . inl ty2 ty1
+opSem (Prl ty1 ty2) = prl ty1 ty2
+opSem (Prr ty1 ty2) = prl ty2 ty1 . swap ty1 ty2
+opSem (Arb ty) = arb ty
 
 %inline
 sem' : Monad m => Term ty ctx -> m (All TypeOf ctx -> TypeOf ty)
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index 0ba09a2..d403440 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -43,8 +43,23 @@ t `mod` u = App (App (Op Mod) t) u
 
 export
 Arb : {ty : Ty} -> Term ty ctx
-Arb {ty = N} = Zero
-Arb {ty = ty ~> ty'} = Const Arb
+Arb = Op (Arb ty)
+
+export
+inL : {ty1, ty2 : Ty} -> Term (ty1 ~> (ty1 <+> ty2)) ctx
+inL = Op (Inl ty1 ty2)
+
+export
+inR : {ty1, ty2 : Ty} -> Term (ty2 ~> (ty1 <+> ty2)) ctx
+inR = Op (Inr ty1 ty2)
+
+export
+prL : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty1) ctx
+prL = Op (Prl ty1 ty2)
+
+export
+prR : {ty1, ty2 : Ty} -> Term ((ty1 <+> ty2) ~> ty2) ctx
+prR = Op (Prr ty1 ty2)
 
 -- HOAS
 
diff --git a/src/Type.idr b/src/Type.idr
index c4ab809..92de65e 100644
--- a/src/Type.idr
+++ b/src/Type.idr
@@ -1,6 +1,6 @@
 module Type
 
-infixr 4 ~>
+infixr 9 ~>
 
 public export
 data Ty : Type where
@@ -8,3 +8,10 @@ data Ty : Type where
   (~>) : Ty -> Ty -> Ty
 
 %name Ty ty
+
+public 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')