diff options
Diffstat (limited to 'src/Level0.idr')
| -rw-r--r-- | src/Level0.idr | 21 |
1 files changed, 16 insertions, 5 deletions
diff --git a/src/Level0.idr b/src/Level0.idr index bccaa4f..51fd236 100644 --- a/src/Level0.idr +++ b/src/Level0.idr @@ -5,8 +5,19 @@ import NormalForm import Term import Thinning -Res : Type -> Type -Res = Pair () +record Cont (a : Type) where + constructor Then + runCont : forall res. (a -> res) -> res + +Functor Cont where + map f (Then g) = Then (\k => k (g f)) + +Applicative Cont where + pure x = Then (\k => k x) + Then f <*> Then v = Then (\k => f (\j => v (k . j))) + +Monad Cont where + join (Then f) = Then (\k => f (\c => runCont c k)) public export data NormSubst : SnocList Ty -> SnocList Ty -> Type where @@ -36,11 +47,11 @@ restrict (sub :< t) (Keep thin) = restrict sub thin :< t -- Evaluates a term in a context of normal forms. partial -eval : Term ctx ty -> NormSubst ctx' ctx -> Res (Normal ctx' ty) +eval : Term ctx ty -> NormSubst ctx' ctx -> Cont (Normal ctx' ty) partial -evalSub : Subst ctx ctx'' -> NormSubst ctx' ctx -> Res (NormSubst ctx' ctx'') +evalSub : Subst ctx ctx'' -> NormSubst ctx' ctx -> Cont (NormSubst ctx' ctx'') partial -rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Res (Normal ctx ty) +rec : Normal ctx N -> Normal ctx ty -> Normal (ctx :< ty) ty -> Cont (Normal ctx ty) eval (Var i) sub = pure (index sub i) eval (Abs t) sub = [| Abs (eval t $ lift sub) |] |