blob: 311bc340e7b7efc13f5f8aa3e308a34dfb899e9d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
|
module CC.Term.Eval
import CC.Name
import CC.Term
import CC.Thinning
-- Evaluation ------------------------------------------------------------------
export
app : Closure ctx -> Lazy (Value ctx) -> Value ctx
export
eval : Env local global -> Term local -> Value global
app (Close n env t) v = assert_total $ eval (env :< (n, v)) t
eval env (Var k n prf) = index env k prf
eval env (Abs n t) = VAbs (Close n env t)
eval env (App t u) =
case eval env t of
Ntrl n => Ntrl $ VApp n (eval env u)
VAbs close => app close (eval env u)
eval env (Let n t u) = eval (env :< (n, eval env t)) u
-- Quoting ---------------------------------------------------------------------
export
quote : {ctx : _} -> Value ctx -> Term ctx
quoteNtrl : {ctx : _} -> Neutral ctx -> Term ctx
quote (Ntrl n) = quoteNtrl n
quote (VAbs close@(Close n _ _)) =
Abs n $
assert_total $
quote $
app (wknClose close (drop id)) (Ntrl $ VVar 0 n $ Here $ reflexive {rel = (~~)})
quoteNtrl (VVar k n prf) = Var k n prf
quoteNtrl (VApp n v) = App (quoteNtrl n) (quote v)
export
normalise : {global : _} -> Env local global -> Term local -> Term global
normalise env t = quote $ eval env t
|
