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
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Cost semantics %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
grammar
heap :: 'Heap_' ::= {{ com Values on the heap }}
| cl :: :: HeapClosure {{ com Closure }}
| K args :: :: HeapConstructor {{ com Data constructor }}
| x :: :: HeapIndirection {{ com Indirection }}
cost :: 'cost_' ::=
| alloc K :: :: AllocateCon
| alloc cl :: :: AllocateClosure
| alloc PAP :: :: AllocatePAP
t {{ tex \theta }} :: 't_' ::=
| {} :: :: empty
| { ccs |-> cost } :: :: inject
| t <> t' :: :: append
G {{ tex \Gamma }}, D {{ tex \Delta }}, T {{ tex \Theta }} :: 'G_' ::= {{ com Heap }}
| G [ Gp ] :: :: vn {{ com Heap with assignment }}
Gp :: 'Gp_' ::= {{ com Heap assignment }}
| x |- ccs -> heap :: :: prod
{{ tex [[x]] \overset{[[ccs]]}{\mapsto} [[heap]] }}
formula :: 'formula_' ::=
| judgement :: :: judgement
% all the random extra stuff we didn't want to gunk up the inductive
% types with...
| alt' = alt :: :: Galt
| ccs' /= ccs :: :: Gccsneq
| Gp in G :: :: Gin
| x fresh :: :: Gfresh
v :: 'v_' ::=
| cl :: :: HClosureReentrant
| K args :: :: HConstructor
ret :: 'ret_' ::= {{ com Return values }}
| a :: :: Return {{ com Normal return }}
| { x args } :: :: LetNoEscape {{ com Jump to let-no-escape }}
subrules
v <:: heap
defns
Jcost :: '' ::=
defn
ccs , G : e >- t -> D : ret , ccs' :: :: cost :: ''
{{tex [[ccs]] [[,]] [[G]] [[:]] [[e]]\ \Downarrow_{[[t]]}\ [[D]] [[:]] [[ret]] [[,]] [[ccs']] }}
by
--------------------------------------- :: Lit
ccs, G : lit >-{}-> G : lit, ccs
x |- ccs0 -> v in G
--------------------------------------- :: Whnf
ccs, G : x nil >-{}-> G : x, ccs
ccs0, G : e >-t-> D : z, ccs'
--------------------------------------- :: Thunk
ccs, G [ x |- ccs0 -> \ u _ nil . e ] : x nil >-t-> D [ x |- ccs0 -> z ] : z, ccs'
f |- ccs0 -> \ r ccs1 </ yi // i /> </ xj // j /> . e in G
z fresh
--------------------------------------- :: AppUnder
ccs, G : f </ ai // i /> >- { ccs |-> alloc PAP } -> G [ z |- ccs -> \ r _ </ xj // j /> . f </ ai // i /> </ xj // j /> ] : z, ccs
% NB: PAPs not charged!
ccs ^ ccs0, G : e >-t-> D : z, ccs'
------------------------------------------------- :: App
ccs, G [ f |- ccs0 -> \ r CCCS </ xi // i /> . e ] : f </ ai // i /> >-t-> D : z, ccs'
ccs, G : e >-t-> D : z, ccs'
ccs1 /= CCCS
------------------------------------------------- :: AppTop
ccs, G [ f |- _ -> \ r ccs1 </ xi // i /> . e ] : f </ ai // i /> >-t-> D : z, ccs'
ccs, G : f </ ai // i /> >-t-> D : f', ccs'
ccs, D : f' </ bj // j /> >-t'-> T : z, ccs''
---------------------------------------- :: AppOver
ccs, G : f </ ai // i /> </ bj // j /> >-t <> t'-> T : z, ccs''
z fresh
---------------------------------------- :: ConApp
ccs, G : K </ ai // i /> >- { ccs |-> alloc K } -> G [ z |- ccs -> K </ ai // i /> ] : z, ccs
altj = Kk </ xi // i /> -> e'
ccs, G : e >- t -> D [ y |- _ -> Kk </ ai // i /> ] : y, ccs'
ccs, D [ y |- _ -> Kk </ ai // i /> ] : e' [ y / x ] </ [ ai / xi ] // i /> >- t' -> T : z, ccs''
--------------------------------------------------------------- :: Case
ccs, G : case e as x of </ altj // j /> >- t <> t' -> T : z, ccs''
y fresh
ccs, G [ y |- ccs -> cl ] : e [ x / y ] >- t -> D : z, ccs'
------------------------------------------------------------ :: LetClosure
ccs, G : let x = cl in e >- { ccs |-> alloc cl } <> t -> D : z, ccs'
y fresh
ccs, G [ y |- ccs -> K </ ai // i /> ] : e [ x / y ] >- t -> D : z, ccs'
------------------------------------------------------------ :: LetCon
ccs, G : let x = K CCCS </ ai // i /> in e >- { ccs |-> alloc K } <> t -> D : z, ccs'
ccs, G : e >- t -> D : { f </ ai // i /> } , ccs'
ccs, D : e' </ [ ai / xi ] // i /> >- t' -> T : z, ccs''
------------------------------------------------------------ :: LneClosure
ccs, G : lne f = \ upd _ </ x // i /> . e' in e >- t <> t' -> T : z, ccs''
ccs, G : e >- t -> D : x , ccs'
ccs, D : K </ ai // i /> >- t' -> T : z, ccs''
--------------------------------------------------------------- :: LneCon
ccs, G : lne x = K _ </ ai // i /> in e >- t <> t' -> T : z, ccs''
ccs # cc, G : e >- t -> D : z, ccs'
--------------------------------------- :: SCC
ccs, G : scc cc e >- t -> D : z, ccs'
|
