Revision dccec723
Added by LĂ©lio Brun over 3 years ago
src/compiler_common.ml | ||
---|---|---|
330 | 330 |
c.spec_loc |
331 | 331 |
top.top_decl_owner |
332 | 332 |
top.top_decl_itf |
333 |
(Node nd), |
|
334 |
c |
|
333 |
(Node nd) |
|
335 | 334 |
(* { nd with |
336 | 335 |
* node_dec_stateless = stateless; |
337 | 336 |
* node_stateless = Some stateless; |
... | ... | |
373 | 372 |
| Some (Contract _) -> |
374 | 373 |
(* A contract: processing it *) |
375 | 374 |
(* we bind a fresh node *) |
376 |
let new_nd, new_c = process_contract_new_node accu_contracts prog top in
|
|
375 |
let new_nd = process_contract_new_node accu_contracts prog top in |
|
377 | 376 |
(* Format.eprintf "Creating new contract node %s@." (node_name |
378 | 377 |
new_nd); *) |
379 | 378 |
let nd = |
380 |
{ nd with node_spec = Some (NodeSpec (node_name new_nd, Some new_c)) }
|
|
379 |
{ nd with node_spec = Some (NodeSpec (node_name new_nd)) } |
|
381 | 380 |
in |
382 | 381 |
( new_nd :: accu_contracts, |
383 | 382 |
{ top with top_decl_desc = Node nd } :: accu_nodes )) |
... | ... | |
392 | 391 |
| Some (Contract _) -> |
393 | 392 |
(* A contract: processing it *) |
394 | 393 |
(* we bind a fresh node *) |
395 |
let new_nd, new_c = process_contract_new_node accu_contracts prog top in
|
|
394 |
let new_nd = process_contract_new_node accu_contracts prog top in |
|
396 | 395 |
let ind = |
397 |
{ ind with nodei_spec = Some (NodeSpec (node_name new_nd, Some new_c)) }
|
|
396 |
{ ind with nodei_spec = Some (NodeSpec (node_name new_nd)) } |
|
398 | 397 |
in |
399 | 398 |
( new_nd :: accu_contracts, |
400 | 399 |
{ top with top_decl_desc = ImportedNode ind } :: accu_nodes )) |
Also available in: Unified diff
a version that almost work for the k-inuctive two_counters example