-
Notifications
You must be signed in to change notification settings - Fork 36
/
GluedEval.hs
137 lines (104 loc) · 4.55 KB
/
GluedEval.hs
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
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
{-# language Strict, LambdaCase, BlockArguments #-}
{-# options_ghc -Wincomplete-patterns #-}
{-
Minimal demo of "glued" evaluation in the style of Olle Fredriksson:
https://github.com/ollef/sixty
The main idea is that during elaboration, we need different evaluation
strategies for different tasks; here in particular we have a distinction
between top and local scope, and we want to have control over unfolding
of top-level definitions.
- For generating terms (for error displaying, serialization, metavariable
solutions), we want to avoid unfolding as much as possible, to avoid size
blowups.
- For conversion checking, we want to have an efficient, preferably call-by-need
evaluator which unfolds everything.
We want evaluation to be as fast as possible, and we also want to avoid
duplicating computation between the two unfolding modes which could be shared.
The solution here is to use normalization-by-evaluation extended with
lazy non-deterministic choice in the semantic domain. We extend values with
... | VTop Name Spine ~Val
where Name and Spine constitute a neutral expression whose head is a top-level
definition name, and ~Val is the lazy result of evaluating the same netural
expression, but with the top definition unfolded.
Hence, when we hit VTop during processing Val-s, we can choose between
unfolding and not unfolding.
We also have to implement the semantic action of projections and eliminations
on VTop. In our case, we only have function application:
vapp :: Val -> Val -> Val
vapp (VLam _ t) ~u = t u
vapp (VLoc x sp) ~u = VLoc x (SApp sp u)
vapp (VTop x sp t) ~u = VTop x (SApp sp u) (vapp t u)
vapp acts on both branches of VTop. The neutral part is eagerly computed,
since the computation there is trivial, delaying it would be more costly
than just performing it. In contrast, the "vapp t u" can be arbitrarily costly,
so it is delayed.
Note that "u" is duplicated in "VTop x (SApp sp u) (vapp t u)". This means
that "u" is computed at most once regardless of which evaluation branch we
compute (of course, we can compute both too).
-}
import Data.Maybe
type Name = String
data Tm
= Loc Name -- local var
| Top Name -- top-level var
| App Tm Tm
| Let Name Tm Tm
| Lam Name Tm
deriving Show
data Spine = SNil | SApp Spine ~Val
data Val = VLam Name (Val -> Val) | VLoc Name Spine | VTop Name Spine ~Val
type TopEnv = [(Name, Val)]
type LocalEnv = [(Name, Val)]
eval :: TopEnv -> LocalEnv -> Tm -> Val
eval top loc = \case
Loc x -> fromJust $ lookup x loc
Top x -> VTop x SNil (fromJust $ lookup x top)
App t u -> vapp (eval top loc t) (eval top loc u)
Let x t u -> eval top ((x, eval top loc t) : loc) u
Lam x t -> VLam x \u -> eval top ((x, u):loc) t
vapp :: Val -> Val -> Val
vapp (VLam _ t) ~u = t u
vapp (VLoc x sp) ~u = VLoc x (SApp sp u)
vapp (VTop x sp t) ~u = VTop x (SApp sp u) (vapp t u)
fresh :: LocalEnv -> Name -> Name
fresh env x = case lookup x env of
Nothing -> x
Just{} -> fresh env (x ++ "'")
type UnfoldTop = Bool
quoteSp :: LocalEnv -> UnfoldTop -> Tm -> Spine -> Tm
quoteSp loc unf h = \case
SNil -> h
SApp sp u -> App (quoteSp loc unf h sp) (quote loc unf u)
quote :: LocalEnv -> UnfoldTop -> Val -> Tm
quote loc unf = \case
VLoc x sp -> quoteSp loc unf (Loc x) sp
VLam x t -> let x' = fresh loc x
v = VLoc x' SNil
in Lam x' (quote ((x, v):loc) unf (t v))
VTop x sp t -> if unf then quote loc unf t
else quoteSp loc unf (Top x) sp
evalTop :: [(Name, Tm)] -> Tm -> Val
evalTop top t = eval topvals [] t where
topvals = foldl (\top (x, t) -> (x, eval top [] t) : top) [] top
nfTop :: UnfoldTop -> [(Name, Tm)] -> Tm -> Tm
nfTop unf top t = quote [] unf (evalTop top t)
------------------------------------------------------------
($$) = App
infixl 8 $$
top :: [(Name, Tm)]
top = [
("zero", Lam "s" $ Lam "z" $ Loc "z")
, ("suc", Lam "n" $ Lam "s" $ Lam "z" $
Loc "s" $$ (Loc "n" $$ Loc "s" $$ Loc "z"))
, ("add", Lam "a" $ Lam "b" $ Lam "s" $ Lam "z" $
Loc "a" $$ Loc "s" $$ (Loc "b" $$ Loc "s" $$ Loc "z"))
, ("mul", Lam "a" $ Lam "b" $ Lam "s" $ Lam "z" $
Loc "a" $$ (Loc "b" $$ Loc "s") $$ Loc "s" $$ Loc "z")
, ("5", Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$
(Top "suc" $$ Top "zero")))))
, ("10", Top "add" $$ Top "5" $$ Top "5")
, ("100", Top "mul" $$ Top "10" $$ Top "10")
]
tm = Let "five" (Top "suc" $$ (Top "suc" $$ (Top "suc" $$ (Top "suc" $$
(Top "suc" $$ Top "zero"))))) $
Top "mul" $$ Loc "five" $$ Top "5"