4 files changed, 76 insertions, 4 deletions
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