Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/corelang.ml | ||
---|---|---|
193 | 193 |
modes = []; |
194 | 194 |
imports = []; |
195 | 195 |
spec_loc = Location.dummy; |
196 |
proof = None |
|
196 | 197 |
} |
197 | 198 |
|
198 | 199 |
(* For const declaration we do as for regular lustre node. But for local flows |
... | ... | |
213 | 214 |
|
214 | 215 |
let eexpr_add_name eexpr eexpr_name = { eexpr with eexpr_name } |
215 | 216 |
|
216 |
let mk_contract_guarantees name eexpr = |
|
217 |
let mk_contract_guarantees name eexpr proof =
|
|
217 | 218 |
{ |
218 | 219 |
empty_contract with |
219 | 220 |
guarantees = [ eexpr_add_name eexpr name ]; |
220 | 221 |
spec_loc = eexpr.eexpr_loc; |
222 |
proof |
|
221 | 223 |
} |
222 | 224 |
|
223 | 225 |
let mk_contract_assume name eexpr = |
... | ... | |
242 | 244 |
spec_loc = loc; |
243 | 245 |
} |
244 | 246 |
|
247 |
let merge_proofs p1 p2 = |
|
248 |
let merge_proofs p1 p2 = match p1, p2 with |
|
249 |
| Kinduction k1, Kinduction k2 -> |
|
250 |
Kinduction (max k1 k2) |
|
251 |
in |
|
252 |
match p1, p2 with |
|
253 |
| Some p1, Some p2 -> Some (merge_proofs p1 p2) |
|
254 |
| Some p, None | None, Some p -> Some p |
|
255 |
| None, None -> None |
|
256 |
|
|
245 | 257 |
let merge_contracts ann1 ann2 = |
246 | 258 |
(* keeping the first item loc *) |
247 | 259 |
{ |
... | ... | |
253 | 265 |
modes = ann1.modes @ ann2.modes; |
254 | 266 |
imports = ann1.imports @ ann2.imports; |
255 | 267 |
spec_loc = ann1.spec_loc; |
268 |
proof = merge_proofs ann1.proof ann2.proof |
|
256 | 269 |
} |
257 | 270 |
|
258 | 271 |
let mkeexpr loc expr = |
... | ... | |
1105 | 1118 |
option_map |
1106 | 1119 |
(fun s -> |
1107 | 1120 |
match s with |
1108 |
| NodeSpec (id, oc) ->
|
|
1109 |
NodeSpec (f_node id, option_map (rename_contract f_var f_node) oc)
|
|
1121 |
| NodeSpec id ->
|
|
1122 |
NodeSpec (f_node id) |
|
1110 | 1123 |
| Contract c -> |
1111 | 1124 |
Contract (rename_contract f_var f_node c)) |
1112 | 1125 |
nd.node_spec |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example