-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhandlerprime.k
221 lines (193 loc) · 8.41 KB
/
handlerprime.k
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
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
requires "substitution.md"
module HANDLERPRIME-SYNTAX
imports DOMAINS-SYNTAX
imports KVAR-SYNTAX
imports ID-SYNTAX
imports INT-SYNTAX
imports BOOL-SYNTAX
// Values
//
// No values are strict as they do not compute.
syntax Val ::= // Variables
KVar [color(red)]
// Value unit
| "()" [color(red)]
// Brackets
| "(" Val ")" [bracket, color(red)]
| Int
| Bool
// Need to separate from KVar in Val due to bug
// https://github.com/kframework/k/issues/2170
// Value pairing
syntax VPair ::= "(" Val "," Val ")" [color(red), format(%1%2%3 %4%5)]
syntax Val ::= VPair
// Left sum inclusion
syntax InL ::= "inl" "(" Val ")" [color(red), format(%1%2%3%4)]
syntax Val ::= InL
// Right sum inclusion
syntax InR ::= "inr" "(" Val ")" [color(red), format(%1%2%3%4)]
syntax Val ::= InR
// Suspend a computation
syntax Thunk ::= "{" Comp "}" [color(red), format(%1%2%3)]
syntax Val ::= Thunk
// Computations
//
// Constructs which are strict in some component are also hoisting or
// computation frames. For example, in the paper we see that
//
// let x <- [] in N
//
// is a frame. Thus, let is strict in its second component.
syntax Comp ::= // Split and bind a value pair
"split" Val "with" SplitFst
[color(green), format(%1 %2 %3%i%n%4)]
// Case match on the empty value
| "void" "(" Val ")" [color(green), format(%1%2%3)]
// Case match and bind on a sum value
| "case" Val "of" "{" CaseL ";" CaseR "}"
[color(green), format(%1 %2 %3%i%n%4 %5%n%6 %7%n%8%d)]
// Force a suspended computation to continue
| Val "!" [color(green), format(%1%2)]
// Let binding
| "let" KVar "=" Comp "in" Comp
[binder, strict(2), color(green), format(%1 %2 %3 %4 %5%n%6)]
// Apply a computation to a value
| Comp Val [strict(1), color(green), format((%1 %2))]
// Project from a pair of computations
| "fst" "(" Comp ")" [strict, color(green), format(%1%2%3%4)]
| "snd" "(" Comp ")" [strict, color(green), format(%1%2%3%4)]
// Handle a computation
| "handle" Comp "with" HandlerBody
[strict(1), color(green), format(%1%i%n%2%d%n%3%i%n%4%d)]
// Brackets
| "(" Comp ")" [bracket, color(green)]
// We define canonical computations as separate sorts, and then subsort them
// to the Comp sort. These are computations which have no semantic
// transitions and no frames, and thus if they are at the head of our K cell
// they should be put back into the frame they belong to. If there is no
// parent cell, then the computation is over. This is Theorem 2 in the
// paper.
syntax Comp ::= Return
syntax Comp ::= Lambda
syntax Comp ::= CUnit
syntax Comp ::= CPair
syntax Comp ::= Op
// Effect operations
syntax Op ::= "[" Id "]" "(" Val "," OpBody ")"
[color(cyan), format(%1%2%3%4%5%6 %7%8)]
syntax OpBody ::= "\\" KVar "->" Comp
[binder, color(cyan), format(%1%2% %3%i%n%4%d%n)]
// Generic effects
syntax GenericOp ::= "@" Id "(" Val ")" [color(cyan), format(%1%2%3%4%5)]
syntax Comp ::= GenericOp
// Handler definitions
//
// A handler consists of one return matching case and then a list of
// effect operation matching cases.
syntax HandlerBody ::= "{" HandlerReturn ";" HandlerOps "}"
[color(green), format(%1 %2%n%3 %4%n%5%n)]
// Return matching case
syntax HandlerReturn ::= "return" "(" KVar ")" "->" Comp [binder, color(green)]
// List of effect operation matchings
syntax HandlerOps ::= List{HandlerOp,";"} [color(green), format(%1%2 %3)]
// Effect operation matchings
syntax HandlerOp ::= "[" Id "]" "(" HandlerOp1
[color(green), format(%1%2%3%4%5)]
syntax HandlerOp1 ::= KVar "," HandlerOp2
[binder, color(green), format(%1%2 %3)]
syntax HandlerOp2 ::= KVar ")" "->" Comp
[binder, color(green), format(%1%2 %3 %4%n)]
// Returns a value as a computation
syntax Return ::= "return" "(" Val ")" [color(cyan), format(%1%2%3%4)]
// Lambda abstraction over a computation
syntax Lambda ::= "\\" KVar "->" Comp
[binder, color(cyan), format(%1%2 %3 %4)]
// Unit type for computations
syntax CUnit ::= "<>" [color(cyan)]
// Pair of computations
syntax CPair ::= "<" Comp "," Comp ">" [color(cyan), format(%1%2%3 %4%5)]
// Canonical computations
syntax Canonical ::= Return | Lambda | CUnit | CPair | Op
// Binders for split
syntax SplitFst ::= KVar "," SplitSnd
[binder, color(green), format(%1%2 %3)]
syntax SplitSnd ::= KVar "->" Comp [binder, color(green)]
// Binders for case
syntax CaseL ::= KVar "->" Comp [binder, color(green)]
syntax CaseR ::= KVar "->" Comp [binder, color(green)]
// Integer functions
syntax IntComp ::= Val "+" Val [color(orange)]
| Val "*" Val [color(orange)]
syntax Comp ::= IntComp
// Boolean functions
syntax BoolComp ::= Val "&&" Val [color(orange)]
| Val "||" Val [color(orange)]
| "not" "(" Val ")" [color(orange), format(%1%2%3%4)]
syntax Comp ::= BoolComp
endmodule
module HANDLERPRIME
imports HANDLERPRIME-SYNTAX
imports SUBSTITUTION
imports DOMAINS
// The KResults (i.e. things which K will not rewrite and thus stops
// computation) are canonical terms since programs are computations.
syntax KResult ::= Canonical
// Programs are computations
configuration <k> $PGM:Comp </k>
// Base type functions
//
// Integers
rule V1 + V2 => return(V1 +Int V2)
rule V1 * V2 => return(V1 *Int V2)
// Booleans
rule V1 && V2 => return(V1 andBool V2)
rule V1 || V2 => return(V1 orBool V2)
rule not(V) => return(notBool V)
// Generic operations
rule [genOp]: @(OP:Id)(V:Val) => [OP](V, \!X -> return(!X)) [structural]
// Beta rule for split (\beta.\times)
rule [split]: split (V1,V2) with X1, X2 -> M => M[V1 / X1][V2 / X2]
// Beta rules for case (\beta.+)
rule [casel]: case inl(V) of { X1 -> M1 ; _ -> _ } => M1[V / X1]
rule [caser]: case inr(V) of { _ -> _ ; X2 -> M2 } => M2[V / X2]
// Beta rules for suspension and forcing (\beta.U)
rule [force]: {M:Comp}! => M
// Beta rule for let (\beta.F)
rule [let]: let X = return(V) in M => M[V / X]
// Operation hosting rule for let, an instance of (hoist.op)
rule [letOp]: let Y = [OP](V, \X -> M) in N => [OP](V, \X -> let Y = M in N)
// Beta rule for application (\beta.->)
rule [apply]: (\X -> M) V => M[V / X]
// Operation hosting rule for application, an instance of (hoist.op)
rule [applyOp]: [OP](V, \X -> M) W => [OP](V, \X -> M W)
// Beta rules for projection (\beta.&)
rule [fst]: fst(< M, _ >) => M
rule [snd]: snd(< _, M >) => M
// Operation hosting rules for projection, an instance of (hoist.op)
rule [fstOp]: fst([OP](V, \X -> M)) => [OP](V, \X -> fst(M))
rule [sndOp]: snd([OP](V, \X -> M)) => [OP](V, \X -> snd(M))
// Handling rule for values (handle.F)
rule [handleVal]: handle return(V) with {return(X) -> M; _:HandlerOps}
=> M[V / X]
// Handling rule for operations (handle.op)
//
// We use the auxilliary function getOp to find the required operation in the
// handler body, and then take the result and apply the rule.
rule [handleOp]: (handle [OP](V, \X -> M) with {RET; OPS}):Comp
=> #fun(match(P, K, N)
=> N[V / P][{\X -> handle M with {RET; OPS}} / K]
)(getOp(OP, OPS))
// Successful result of getOp
syntax OpMatch ::= match(KVar, KVar, Comp)
// getOp
syntax OpMatch ::= getOp(Id, HandlerOps) [function]
| "getOpFailure"
// If the required op matches the first case, return the match
rule getOp(OP1:Id, [OP2](X, K) -> M ; _:HandlerOps) => match(X, K, M)
requires OP1 ==K OP2
// Otherwise recurse
rule getOp(OP1:Id, [OP2](_, _) -> _ ; OPS:HandlerOps) => getOp(OP1, OPS)
requires OP1 =/=K OP2
// And fail when we run out of options
rule getOp(_:Id, .HandlerOps) => getOpFailure
endmodule