Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

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