blob: 7029893ad217f97fd4c84e524e5bbbbec640d47d (
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
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
|
module CC.Term.Eval
import CC.Name
import CC.Term
import CC.Thinning
import Data.SnocList.Elem
-- Evaluation ------------------------------------------------------------------
export
app : (n : Name) -> Env local global -> Term (local :< n) -> Lazy (Value global) -> Value global
export
eval : Env local global -> Term local -> Value global
app n env t v = eval (env :< (n, v)) t
eval env (Var k n prf) = index env k prf
eval env (Let n ty val t) = eval (env :< (n, eval env val)) t
eval env Set = VSet
eval env (Pi Nothing t u) = VFunc env t u
eval env (Pi (Just n) t u) = VPi n (eval env t) env u
eval env (Abs n t) = VAbs env n t
eval env (App t u) =
case eval env t of
Ntrl n => Ntrl $ VApp n (eval env u)
VAbs env' n t => assert_total $ app n env' t (eval env u)
_ => assert_total $ idris_crash "eval invariant broken"
-- Quoting ---------------------------------------------------------------------
export
quote : {ctx : _} -> Value ctx -> Term ctx
quoteNtrl : {ctx : _} -> Neutral ctx -> Term ctx
quote (Ntrl n) = quoteNtrl n
quote VSet = Set
quote (VPi n t env u) =
Pi (Just n)
(quote t)
(assert_total $ quote $ eval (liftEnv [<n] env) u)
quote (VFunc env t u) =
Pi Nothing
(assert_total $ quote $ eval env t)
(assert_total $ quote $ eval env u)
quote (VAbs env n t) =
Abs n $ assert_total $ quote $ app n (wknEnv env (drop id)) t (Ntrl $ VVar 0 _ $ fromElem Here)
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
-- Conversion ------------------------------------------------------------------
export
convert : {ctx : Context} -> Value ctx -> Value ctx -> Bool
convertNtrl : {ctx : Context} -> Neutral ctx -> Neutral ctx -> Bool
convert VSet VSet = True
convert (VFunc env t u) (VFunc env' t' u') =
assert_total $
convert (eval env t) (eval env' t') &&
convert (eval env u) (eval env' u')
convert (VFunc env t u) (VPi m t' env' u') =
assert_total $
convert (eval env t) t' &&
convert (eval (wknEnv env (drop id)) u) (eval (liftEnv [<m] env') u')
convert (VPi n t env u) (VFunc env' t' u') =
assert_total $
convert t (eval env' t') &&
convert (eval (liftEnv [<n] env) u) (eval (wknEnv env' (drop id)) u')
convert (VPi n t env u) (VPi m t' env' u') =
convert t t' &&
(assert_total $ convert (eval (liftEnv [<n] env) u) (eval (liftEnv [<n] env') $ renTerm Refl u'))
convert (VAbs env n t) (VAbs env' m u) =
assert_total $
convert (eval (liftEnv [<n] env) t) (eval (liftEnv [<n] env') $ renTerm Refl u)
convert (VAbs env n t) (Ntrl m) =
assert_total $
convert
(eval (liftEnv [<n] env) t)
(Ntrl (VApp (wknNtrl m (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here)))
convert (Ntrl n) (VAbs env m t) =
assert_total $
convert
(Ntrl (VApp (wknNtrl n (drop id)) (Ntrl $ VVar 0 _ $ fromElem Here)))
(eval (liftEnv [<m] env) t)
convert (Ntrl n) (Ntrl m) = convertNtrl n m
convert _ _ = False
convertNtrl (VVar k _ _) (VVar j _ _) = k == j
convertNtrl (VApp n v) (VApp m u) = convertNtrl n m && convert v u
convertNtrl _ _ = False
|
