Add literals as primitive term.

4 files changed, 128 insertions, 128 deletions

diff --git a/src/Term.idr b/src/Term.idr
index e6b7466..47586c5 100644
--- a/src/Term.idr
+++ b/src/Term.idr
@@ -23,7 +23,7 @@ data FullTerm : Ty -> SnocList Ty -> Type where
     {ty : Ty} ->
     Pair (FullTerm (ty ~> ty')) (FullTerm ty) ctx ->
     FullTerm ty' ctx
-  Zero : FullTerm N [<]
+  Lit : Nat -> FullTerm N [<]
   Suc : FullTerm N ctx -> FullTerm N ctx
   Rec :
     Pair (FullTerm N) (Pair (FullTerm ty) (FullTerm (ty ~> ty))) ctx ->
@@ -59,8 +59,8 @@ namespace Smart
   App t u = map App $ MkPair t u
 
   export
-  Zero : Term N ctx
-  Zero = Zero `Over` Empty
+  Lit : Nat -> Term N ctx
+  Lit n = Lit n `Over` Empty
 
   export
   Suc : Term N ctx -> Term N ctx
@@ -272,7 +272,7 @@ fullSubst (Const t) sub = Const (fullSubst t sub)
 fullSubst (Abs t) sub = Abs (fullSubst t $ lift sub)
 fullSubst (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) sub =
   App (fullSubst t $ sub . thin1) (fullSubst u $ sub . thin2)
-fullSubst Zero sub = Zero
+fullSubst (Lit n) sub = Lit n
 fullSubst (Suc t) sub = Suc (fullSubst t sub)
 fullSubst
   (Rec (MakePair
@@ -305,7 +305,7 @@ fullSubstCong (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) prf =
   appCong
     (fullSubstCong t $ compCong prf reflexive)
     (fullSubstCong u $ compCong prf reflexive)
-fullSubstCong Zero prf = irrelevantEquiv $ reflexive
+fullSubstCong (Lit n) prf = irrelevantEquiv $ reflexive
 fullSubstCong (Suc t) prf = sucCong (fullSubstCong t prf)
 fullSubstCong
   (Rec (MakePair
@@ -380,6 +380,6 @@ 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 (Lit n) = 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
index ffa88bd..907a073 100644
--- a/src/Term/Pretty.idr
+++ b/src/Term/Pretty.idr
@@ -120,7 +120,7 @@ getSpline (App (MakePair (t `Over` thin) u _)) =
 getSpline t = MkSpline (t `Over` Id) [<]
 
 getSucs : FullTerm ty ctx -> (Nat, Maybe (FullTerm ty ctx))
-getSucs Zero = (0, Nothing)
+getSucs (Lit n) = (n, Nothing)
 getSucs (Suc t) = mapFst S (getSucs t)
 getSucs t = (0, Just t)
 
@@ -165,7 +165,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 Zero thin = lit 0
+  prettyFullTerm d (Lit n) thin = lit n
   prettyFullTerm d (Suc t) thin =
     let (n, t') = getSucs t in
     case t' of
diff --git a/src/Term/Semantics.idr b/src/Term/Semantics.idr
index 2e61040..e8424f2 100644
--- a/src/Term/Semantics.idr
+++ b/src/Term/Semantics.idr
@@ -49,7 +49,7 @@ fullSem' (App (MakePair t u _)) = do
   t <- sem' t
   u <- sem' u
   pure (\ctx => t ctx (u ctx))
-fullSem' Zero = pure (const 0)
+fullSem' (Lit n) = pure (const n)
 fullSem' (Suc t) = do
   t <- fullSem' t
   pure (S . t)
diff --git a/src/Term/Syntax.idr b/src/Term/Syntax.idr
index 211e039..10e463c 100644
--- a/src/Term/Syntax.idr
+++ b/src/Term/Syntax.idr
@@ -13,13 +13,12 @@ Id = Abs (Var Here)
 
 export
 Arb : {ty : Ty} -> Term ty ctx
-Arb {ty = N} = Zero
+Arb {ty = N} = Lit 0
 Arb {ty = ty ~> ty'} = Const Arb
 
 export
-Lit : Nat -> Term N ctx
-Lit 0 = Zero
-Lit (S k) = Suc (Lit k)
+Zero : Term N ctx
+Zero = Lit 0
 
 -- HOAS
 
@@ -60,118 +59,119 @@ export
 (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' 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 (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 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
+-- -- 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