Add more built-in functions.

4 files changed, 82 insertions, 182 deletions

diff --git a/src/Term/Compile.idr b/src/Term/Compile.idr
index c7b5e9b..b29a6e9 100644
--- a/src/Term/Compile.idr
+++ b/src/Term/Compile.idr
@@ -9,12 +9,13 @@ import Data.Stream
 import Data.String
 
 import Term
+import Term.Pretty
 import Term.Syntax
 
 %prefix_record_projections off
 
 rec_ : Doc ann
-rec_ = "my-rec"
+rec_ = "squid-rec"
 
 underscore : Doc ann
 underscore = "_"
@@ -28,25 +29,15 @@ lambda = "lambda"
 lit : Nat -> Doc ann
 lit = pretty
 
-getSucs : FullTerm ty ctx -> (Nat, Maybe (FullTerm ty ctx))
-getSucs (Lit n) = (n, 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)
-
-extend : sx `Thins` sy -> Len sz -> sx ++ sz `Thins` sy ++ sz
-extend thin Z = thin
-extend thin (S k) = Keep (extend thin k)
+compileOp : Operator tys ty -> Doc ann
+compileOp (Lit n) = lit n
+compileOp Suc = "1+"
+compileOp Plus = "squid-plus"
+compileOp Mult = "squid-mult"
+compileOp Pred = "1-" -- Confusing name, but correct
+compileOp Minus = "squid-minus"
+compileOp Div = "squid-div"
+compileOp Mod = "squid-mod"
 
 parameters (names : Stream String)
   compileFullTerm : (len : Len ctx) => FullTerm ty ctx' -> ctx' `Thins` ctx -> Doc ann
@@ -64,15 +55,7 @@ parameters (names : Stream String)
     parens $ group $ align $
       compileFullTerm t (thin . thin1) <+> line <+>
       compileFullTerm u (thin . thin2)
-  compileFullTerm (Lit n) thin = lit n
-  compileFullTerm t'@(Suc t) thin =
-    let (n, t) = getSucs t in
-    case t of
-      Just t =>
-        parens $ group $ align $
-          plus <++> lit (S n) <+> softline <+>
-          compileFullTerm (assert_smaller t' t) thin
-      Nothing => lit (S n)
+  compileFullTerm (Op op) thin = compileOp op
   compileFullTerm
     (Rec (MakePair
       (t `Over` thin1)
@@ -117,41 +100,43 @@ name k =
     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 . reverse . name) nats
-
 public export
 data ProfileMode = Run | Profile
 
-builtin_rec : String
-builtin_rec = """
-  (define (my-rec n z s)
+builtins : String
+builtins = """
+  (define (squid-rec n z s)
     (let loop ((k 0) (acc z))
       (if (= k n)
         acc
         (loop (1+ k) (s acc)))))
+
+  (define (squid-plus m) (lambda (n) (+ m n)))
+  (define (squid-mult m) (lambda (n) (* m n)))
+  (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)))
   """
 
 wrap_main : Len ctx => Term ty ctx -> Doc ann
 wrap_main t =
   parens $ group $ hang 2 $
-    "define (my-main)" <+> line <+>
+    "define (squid-main)" <+> line <+>
       compileFullTerm canonicalNames t.value t.thin
 
 run_main : ProfileMode -> String
 run_main Run = """
-  (display (my-main))
+  (display (squid-main))
   (newline)
   """
 run_main Profile = """
   (use-modules (statprof))
-  (statprof my-main)
+  (statprof squid-main)
   """
 
 export
 compileTerm : Len ctx => ProfileMode -> Term ty ctx -> Doc ann
 compileTerm mode t =
-  pretty builtin_rec <+> hardline <+> hardline <+>
+  pretty builtins <+> hardline <+> hardline <+>
   wrap_main t <+> hardline <+> hardline <+>
   pretty (run_main mode)
diff --git a/src/Term/Pretty.idr b/src/Term/Pretty.idr
index 907a073..cd7ed6f 100644
--- a/src/Term/Pretty.idr
+++ b/src/Term/Pretty.idr
@@ -34,9 +34,6 @@ rec_ = keyword "rec"
 underscore : Doc Syntax
 underscore = bound "_"
 
-plus : Doc Syntax
-plus = symbol "+"
-
 arrow : Doc Syntax
 arrow = symbol "=>"
 
@@ -119,11 +116,6 @@ getSpline (App (MakePair (t `Over` thin) u _)) =
   MkSpline rec.head (rec.args :< u)
 getSpline t = MkSpline (t `Over` Id) [<]
 
-getSucs : FullTerm ty ctx -> (Nat, Maybe (FullTerm ty ctx))
-getSucs (Lit n) = (n, Nothing)
-getSucs (Suc t) = mapFst S (getSucs t)
-getSucs t = (0, Just t)
-
 public export
 data Len : SnocList a -> Type where
   Z : Len [<]
@@ -131,6 +123,7 @@ data Len : SnocList a -> Type where
 
 %name Len k
 
+export
 lenToNat : Len sx -> Nat
 lenToNat Z = 0
 lenToNat (S k) = S (lenToNat k)
@@ -149,6 +142,17 @@ extend : sx `Thins` sy -> Len sz -> sx ++ sz `Thins` sy ++ sz
 extend thin Z = thin
 extend thin (S k) = Keep (extend thin k)
 
+public export
+prettyOp : Operator tys ty -> Doc Syntax
+prettyOp (Lit n) = lit n
+prettyOp Suc = keyword "suc"
+prettyOp Plus = keyword "plus"
+prettyOp Mult = keyword "mult"
+prettyOp Pred = keyword "pred"
+prettyOp Minus = keyword "minus"
+prettyOp Div = keyword "div"
+prettyOp Mod = keyword "mod"
+
 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
@@ -165,14 +169,7 @@ parameters (names : Stream String)
     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 (Lit n) thin = lit n
-  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 (Op op) thin = prettyOp op
   prettyFullTerm d t@(Rec _) thin =
     prettySpline d (assert_smaller t $ wkn (getSpline t) thin)
 
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index e8424f2..62e2be7 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -1,6 +1,7 @@
 module Term.Semantics
 
 import Control.Monad.Identity
+import Data.Nat
 import Term
 
 import public Data.SnocList.Quantifiers
@@ -33,6 +34,17 @@ indexVar : All p [<x] -> p x
 indexVar [<px] = px
 
 %inline
+opSem : Operator tys ty -> TypeOf (foldr (~>) ty tys)
+opSem (Lit n) = n
+opSem Suc = S
+opSem Plus = (+)
+opSem Mult = (*)
+opSem Pred = pred
+opSem Minus = minus
+opSem Div = div
+opSem Mod = mod
+
+%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)
 
@@ -49,10 +61,7 @@ fullSem' (App (MakePair t u _)) = do
   t <- sem' t
   u <- sem' u
   pure (\ctx => t ctx (u ctx))
-fullSem' (Lit n) = pure (const n)
-fullSem' (Suc t) = do
-  t <- fullSem' t
-  pure (S . t)
+fullSem' (Op op) = pure (const $ opSem op)
 fullSem' (Rec (MakePair t (MakePair u v _ `Over` thin) _)) = do
   t <- sem' t
   u <- sem' u
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index 10e463c..0ba09a2 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -12,13 +12,39 @@ Id : Term (ty ~> ty) ctx
 Id = Abs (Var Here)
 
 export
-Arb : {ty : Ty} -> Term ty ctx
-Arb {ty = N} = Lit 0
-Arb {ty = ty ~> ty'} = Const Arb
+Zero : Term N ctx
+Zero = Op (Lit 0)
 
 export
-Zero : Term N ctx
-Zero = Lit 0
+Suc : Term N ctx -> Term N ctx
+Suc t = App (Op Suc) t
+
+export
+Num (Term N ctx) where
+  t + u = App (App (Op Plus) t) u
+  t * u = App (App (Op Mult) t) u
+  fromInteger = Op . Lit . fromInteger
+
+export
+pred : Term N ctx -> Term N ctx
+pred t = App (Op Pred) t
+
+export
+minus : Term N ctx -> Term N ctx -> Term N ctx
+t `minus` u = App (App (Op Minus) t) u
+
+export
+div : Term N ctx -> Term N ctx -> Term N ctx
+t `div` u = App (App (Op Div) t) u
+
+export
+mod : Term N ctx -> Term N ctx -> Term N ctx
+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
 
 -- HOAS
 
@@ -58,120 +84,3 @@ export
   Term (sty ~>* ty') ctx
 (t .: u) {sty = [<]} = App t u
 (t .: u) {sty = sty :< ty''} = Abs' (\f => shift t . f) .: u
-
--- -- 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' (Lit 0) thin u v = Just u
--- Rec' (Lit (S n)) 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 (Zero `Over` thin1) (Const Zero `Over` thin2) =
---   Just (Zero `Over` Empty)
--- 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 (Lit n) = (fuel, Lit n `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