diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/Encoded/Arith.idr | 55 | ||||
| -rw-r--r-- | src/Encoded/Bool.idr | 4 | ||||
| -rw-r--r-- | src/Encoded/Container.idr | 21 | ||||
| -rw-r--r-- | src/Encoded/Fin.idr | 2 | ||||
| -rw-r--r-- | src/Term.idr | 38 | ||||
| -rw-r--r-- | src/Term/Compile.idr | 65 | ||||
| -rw-r--r-- | src/Term/Pretty.idr | 29 | ||||
| -rw-r--r-- | src/Term/Semantics.idr | 17 | ||||
| -rw-r--r-- | src/Term/Syntax.idr | 153 |
9 files changed, 114 insertions, 270 deletions
diff --git a/src/Encoded/Arith.idr b/src/Encoded/Arith.idr index fe9bc68..4dd3e10 100644 --- a/src/Encoded/Arith.idr +++ b/src/Encoded/Arith.idr @@ -22,47 +22,8 @@ rec = Abs $ Abs $ Abs $ App snd [<p] export -plus : Term (N ~> N ~> N) ctx -plus = Abs' (\n => Rec n Id (Abs' (Abs' Suc .))) - -export -pred : Term (N ~> N) ctx --- pred = Abs' (\n => App rec [<n, Zero, fst]) -pred = Abs' - (\n => App - (Rec n - (Const Zero) - (Abs $ Abs $ - let f = Var (There Here) in - let k = Var Here in - Rec k - (Lit 1) - (Const $ - Rec (App f [<Zero]) - Zero - (Const $ Suc $ App f [<Lit 1])))) - [<Lit 1]) - -export -minus : Term (N ~> N ~> N) ctx -minus = Abs $ Abs $ - let m = Var $ There Here in - let n = Var Here in - Rec n m pred - -export -mult : Term (N ~> N ~> N) ctx -mult = Abs' (\n => - Rec n - (Const Zero) - (Abs $ Abs $ - let f = Var $ There Here in - let m = Var Here in - App plus [<m, App f [<m]])) - -export lte : Term (N ~> N ~> B) ctx -lte = Abs' (\m => isZero . App minus [<m]) +lte = Abs' (\m => isZero . App (Op Minus) [<m]) export equal : Term (N ~> N ~> B) ctx @@ -70,17 +31,3 @@ equal = Abs $ Abs $ let m = Var $ There Here in let n = Var Here in App and [<App lte [<m, n], App lte [<n, m]] - -export -divmod : Term (N ~> N ~> N * N) ctx -divmod = Abs $ Abs $ - let n = Var (There Here) in - let d = Var Here in - Rec - n - (App pair [<Zero, Zero]) - (Abs' (\p => - App if' - [<App lte [<shift d, Suc (App snd [<p])] - , App pair [<Suc (App fst [<p]), Zero] - , App mapSnd [<Abs' Suc, p]])) diff --git a/src/Encoded/Bool.idr b/src/Encoded/Bool.idr index 778f65d..731f45c 100644 --- a/src/Encoded/Bool.idr +++ b/src/Encoded/Bool.idr @@ -8,11 +8,11 @@ B = N export True : Term B ctx -True = Lit 0 +True = 0 export False : Term B ctx -False = Lit 1 +False = 1 export if' : Term (B ~> ty ~> ty ~> ty) ctx diff --git a/src/Encoded/Container.idr b/src/Encoded/Container.idr index 1334bc2..800623a 100644 --- a/src/Encoded/Container.idr +++ b/src/Encoded/Container.idr @@ -83,31 +83,28 @@ getFuel : {cont : Container} -> {c : Case} -> Term (semCase c (W cont) ~> N) ctx -getFuel {c = (tag, k)} = App foldr [<Zero, plus] . App map [<Abs' Suc . fuel] . recurse +getFuel {c = (tag, k)} = App foldr [<Zero, Op Plus] . App map [<Abs' Suc . fuel] . recurse -- Updates the base and stride for a single recursive position. -- These are multiplexed later. stepOffset : {k : Nat} -> Term (Fin k ~> (N ~> N * N) ~> (N ~> N * N)) ctx -stepOffset = Abs $ Abs $ Abs $ - let i = Var (There $ There Here) in - let f = Var (There Here) in - let x = Var Here in +stepOffset = AbsAll [<_,_,_] (\[<i, f, x] => App bimap -- Suc is for the initial tag - [<App (plus . forget . suc) [<i] . App mult [<Lit k] - , App mult [<Lit k] + [<Abs' (\n => Suc $ App forget [<shift i] + Op (Lit k) * n) + , Abs' (\n => Op (Lit k) * n) , App f [<x] - ] + ]) -- Calculates all offsets for a new W value. getOffset : {cont : Container} -> {c : Case} -> Term (semCase c (W cont) ~> N ~> N * N) ctx -getOffset {c = (tag, 0)} = Const $ Const $ App pair [<Lit 1, Zero] +getOffset {c = (tag, 0)} = Const $ Const $ App pair [<1, 0] getOffset {c = (tag, k@(S _))} = Abs' (\x => - App cons - [<App pair [<Lit 1, Zero] + App Container.cons + [<App pair [<1, 0] , Abs' (\n => let dm = App (divmod' k) [<n] in let div = App fst [<dm] in @@ -154,7 +151,7 @@ intro = gtabulate introCase calcIndex : Term (N * N ~> N ~> N) ctx -calcIndex = Abs' (\bs => App (plus . fst) [<bs] . App (mult . snd) [<bs]) +calcIndex = AbsAll [<_, _] (\[<bs, n] => App fst [<bs] + App snd [<bs] * n) fillCase : {c : Case} -> diff --git a/src/Encoded/Fin.idr b/src/Encoded/Fin.idr index 0029760..3f369cf 100644 --- a/src/Encoded/Fin.idr +++ b/src/Encoded/Fin.idr @@ -40,4 +40,4 @@ forget = Id export divmod' : (k : Nat) -> {auto 0 ok : NonZero k} -> Term (N ~> N * Fin k) ctx -divmod' k = Abs' (\n => App divmod [<n, Lit k]) +divmod' k = Abs' (\n => App pair [<n `div` Op (Lit k), n `mod` Op (Lit k)]) diff --git a/src/Term.idr b/src/Term.idr index 47586c5..96a0cb5 100644 --- a/src/Term.idr +++ b/src/Term.idr @@ -13,6 +13,19 @@ import public Type -- Definition ------------------------------------------------------------------ +public export +data Operator : List Ty -> Ty -> Type where + Lit : (n : Nat) -> Operator [] N + Suc : Operator [N] N + Plus : Operator [N, N] N + Mult : Operator [N, N] N + Pred : Operator [N] N + Minus : Operator [N, N] N + Div : Operator [N, N] N + Mod : Operator [N, N] N + +%name Operator op + ||| System T terms that use all the variables in scope. public export data FullTerm : Ty -> SnocList Ty -> Type where @@ -23,8 +36,7 @@ data FullTerm : Ty -> SnocList Ty -> Type where {ty : Ty} -> Pair (FullTerm (ty ~> ty')) (FullTerm ty) ctx -> FullTerm ty' ctx - Lit : Nat -> FullTerm N [<] - Suc : FullTerm N ctx -> FullTerm N ctx + Op : Operator tys ty -> FullTerm (foldr (~>) ty tys) [<] Rec : Pair (FullTerm N) (Pair (FullTerm ty) (FullTerm (ty ~> ty))) ctx -> FullTerm ty ctx @@ -59,12 +71,8 @@ namespace Smart App t u = map App $ MkPair t u export - Lit : Nat -> Term N ctx - Lit n = Lit n `Over` Empty - - export - Suc : Term N ctx -> Term N ctx - Suc t = map Suc t + Op : Operator tys ty -> Term (foldr (~>) ty tys) ctx + Op op = Op op `Over` Empty export Rec : Term N ctx -> Term ty ctx -> Term (ty ~> ty) ctx -> Term ty ctx @@ -96,10 +104,6 @@ namespace Smart App t1 t2 <~> App u1 u2 export - sucCong : {0 t, u : Term N ctx} -> t <~> u -> Suc t <~> Suc u - sucCong prf = mapCong Suc prf - - export recCong : {0 t1, u1 : Term N ctx} -> {0 t2, u2 : Term ty ctx} -> @@ -272,8 +276,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 (Lit n) sub = Lit n -fullSubst (Suc t) sub = Suc (fullSubst t sub) +fullSubst (Op op) sub = Op op fullSubst (Rec (MakePair (t `Over` thin1) @@ -305,8 +308,7 @@ fullSubstCong (App (MakePair (t `Over` thin1) (u `Over` thin2) _)) prf = appCong (fullSubstCong t $ compCong prf reflexive) (fullSubstCong u $ compCong prf reflexive) -fullSubstCong (Lit n) prf = irrelevantEquiv $ reflexive -fullSubstCong (Suc t) prf = sucCong (fullSubstCong t prf) +fullSubstCong (Op op) prf = irrelevantEquiv $ reflexive fullSubstCong (Rec (MakePair (t `Over` thin1) @@ -356,7 +358,6 @@ fullCountUses Var Here = 1 fullCountUses (Const t) i = fullCountUses t i fullCountUses (Abs t) i = fullCountUses t (There i) fullCountUses (App (MakePair t u _)) i = countUses t i + countUses u i -fullCountUses (Suc t) i = fullCountUses t i fullCountUses (Rec (MakePair t @@ -380,6 +381,5 @@ 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 (Lit n) = 1 -fullSize (Suc t) = S (fullSize t) +fullSize (Op op) = 1 fullSize (Rec (MakePair t (MakePair u v _ `Over` _) _)) = S (size t + size u + size v) 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 |