106 lines
2.5 KiB
Agda
106 lines
2.5 KiB
Agda
module Zoo1
|
|
|
|
-- I'm starting to translate ezoo 01-eval-closures-debruijn as a test cases.
|
|
|
|
|
|
|
|
|
|
------- Prelude stuff
|
|
|
|
data Nat : U where
|
|
Z : Nat
|
|
S : Nat -> Nat
|
|
|
|
data Unit : U where
|
|
MkUnit : Unit
|
|
|
|
data List : U -> U where
|
|
Nil : {a : U} -> List a
|
|
Cons : {a : U} -> a -> List a -> List a
|
|
|
|
data Maybe : U -> U where
|
|
Just : {a : U} -> a -> Maybe a
|
|
Nothing : {a : U} -> Maybe a
|
|
|
|
|
|
----------------------------------
|
|
|
|
-- forward declaration
|
|
Val : U
|
|
|
|
data Tm : U where
|
|
Var : Nat -> Tm
|
|
Lam : Tm -> Tm -- lam (x.t)
|
|
App : Tm -> Tm -> Tm
|
|
Let : Tm -> Tm -> Tm -- let t (x.u)
|
|
|
|
data Env : U where
|
|
ENil : Env
|
|
Define : Env -> Val -> Env
|
|
|
|
data Closure : U where
|
|
MkClosure : Env -> Tm -> Closure
|
|
|
|
data Val : U where
|
|
VVar : Nat -> Val
|
|
VApp : Val -> Val -> Val
|
|
VLam : Closure -> Val
|
|
|
|
length : Env -> Nat
|
|
length ENil = Z
|
|
length (Define env _) = S (length env)
|
|
|
|
lookup : Env -> Nat -> Maybe Val
|
|
lookup (Define env v) Z = Just v
|
|
-- If I write "Just (lookup env k)" on RHS, it's wrong, but the error message is unusable (mainly due to FC)
|
|
-- The FC is fine if I write lookup {Val} env k
|
|
lookup (Define env _) (S k) = lookup env k
|
|
lookup (ENil) x = Nothing
|
|
|
|
eval : Env -> Tm -> Val
|
|
|
|
cApp : Closure -> Val -> Val
|
|
-- If I put Closure instead of MkClosure, it reports missing case, fix that (should be bad constructor or something)
|
|
cApp (MkClosure env t) u = eval (Define env u) t
|
|
|
|
hole : Val
|
|
|
|
-- TODO need to inline solved metas somewhere, as error messages are unreadable
|
|
-- NEXT fix FC for missing case if we remove _
|
|
|
|
eval env tm = case tm of
|
|
(Var x) =>
|
|
case lookup env x of
|
|
-- case doesn't use the new code. We've got a wildcard here that
|
|
-- is forced to {Val}, but we don't have forcing/dotting
|
|
-- I guess we see what Jesper says about dotting
|
|
Just x => x
|
|
Nothing => VVar x
|
|
-- TODO no tupls yet
|
|
App t u => case eval env t of
|
|
VLam t => cApp t (eval env u)
|
|
t => VApp t (eval env u)
|
|
Lam t => VLam (MkClosure env t)
|
|
Let t u => eval (Define env (eval env t)) u
|
|
-- NEXT this is unreachable, find out how to warn about it
|
|
-- _ => hole
|
|
|
|
lvl2ix : Nat -> Nat -> Nat
|
|
lvl2ix (S k) (S j) = lvl2ix k j
|
|
lvl2ix Z (S j) = j
|
|
lvl2ix _ Z = Z -- shouldn't happen
|
|
|
|
quote : Nat -> Val -> Tm
|
|
quote l v = case v of
|
|
VVar x => Var (lvl2ix l x)
|
|
VApp t u => App (quote l t) (quote l u)
|
|
VLam t => Lam (quote (S l) (cApp t (VVar l)))
|
|
|
|
nf : Env -> Tm -> Tm
|
|
nf env t = quote (length env) (eval env t)
|
|
|
|
-- and then a parser / example
|
|
-- Are we ready to try building a parser in newt?
|
|
|
|
|