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?