Revision 949b2e1e src/normalization.ml

View differences:

src/normalization.ml
369 369
```    let norm_eq = { eq with eq_rhs = norm_rhs } in
```
370 370
```    norm_eq::defs', vars'
```
371 371

372
```(** normalize_node node returns a normalized node,
```
373
```    ie.
```
372
```let normalize_eq_split node defvars eq =
```
373
```
```
374
```  let defs, vars = normalize_eq node defvars eq in
```
375
```  List.fold_right (fun eq (def, vars) ->
```
376
```    let eq_defs = Splitting.tuple_split_eq eq in
```
377
```    if eq_defs = [eq] then
```
378
```      eq::def, vars
```
379
```    else
```
380
```      List.fold_left (normalize_eq node) (def, vars) eq_defs
```
381
```  ) defs ([], vars)
```
382

383
```let normalize_eexpr decls node vars ee =
```
384
```  (* New output variable *)
```
385
```  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
```
386
```  let output_var =
```
387
```    mkvar_decl
```
388
```      ee.eexpr_loc
```
389
```      (output_id,
```
390
```       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
```
391
```       mkclock ee.eexpr_loc Ckdec_any,
```
392
```       false (* not a constant *),
```
393
```       None,
```
394
```       None
```
395
```      )
```
396
```  in
```
397
```  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
```
398
```  (* Calls are first inlined *)
```
399
```  let nodes = get_nodes decls in
```
400
```  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
```
401
```(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
```
402
```   let calls = List.map
```
403
```    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls
```
404
```  in
```
405
```*)
```
406
```  (*Format.eprintf "eexpr %a@.calls: %a@.@?" Printers.pp_eexpr ee (Utils.fprintf_list ~sep:", " (fun fmt nd -> pp_print_string fmt nd.node_id)) calls;  *)
```
407
```  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
```
408
```  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in
```
409
```  let (new_locals, eqs) =
```
410
```    if calls = [] && not (eq_has_arrows eq) then
```
411
```      (locals, [eq])
```
412
```    else ( (* TODO remettre le code. Je l'ai enleve pour des dependances cycliques *)
```
413
```(*      let new_locals, eqs, asserts = Inliner.inline_eq ~arrows:true eq locals calls in
```
414
```      (*Format.eprintf "eqs %a@.@?"
```
415
```	(Utils.fprintf_list ~sep:", " Printers.pp_node_eq) eqs;  *)
```
416
```      (new_locals, eqs)
```
417
```*)
```
418
```           (locals, [eq])
```
419
```
```
420
```    ) in
```
421
```  (* Normalizing expr and eqs *)
```
422
```  let defs, vars = List.fold_left (normalize_eq_split node) ([], new_locals) eqs in
```
423
```  let todefine = List.fold_left
```
424
```    (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
```
425
```    (ISet.add output_id ISet.empty) vars in
```
426
```  try
```
427
```    let env = Typing.type_var_decl_list quant_vars Basic_library.type_env quant_vars in
```
428
```    let env = Typing.type_var_decl [] env output_var in (* typing the variable *)
```
429
```    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
```
430
```    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
```
431
```    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
```
432
```    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
```
433
```  (* check that table is empty *)
```
434
```    if (not (ISet.is_empty undefined_vars)) then
```
435
```      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
```
436
```
```
437
```    (*Format.eprintf "normalized eqs %a@.@?"
```
438
```      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
```
439
```    ee.eexpr_normalized <- Some (output_var, defs, vars)
```
440
```  with (Types.Error (loc,err)) as exc ->
```
441
```    eprintf "Typing error for eexpr %a: %a%a%a@."
```
442
```      Printers.pp_eexpr ee
```
443
```      Types.pp_error err
```
444
```      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
```
445
```      Location.pp_loc loc
```
446
```
```
447
```;
```
448
```    raise exc
```
449

450
```let normalize_spec decls node vars s =
```
451
```  let nee = normalize_eexpr decls node vars in
```
452
```  List.iter nee s.requires;
```
453
```  List.iter nee s.ensures;
```
454
```  List.iter (fun (_, assumes, ensures, _) ->
```
455
```      List.iter nee assumes;
```
456
```    List.iter nee ensures
```
457
```  ) s.behaviors
```
458
```
```
459
```
```
460
```(* The normalization phase introduces new local variables
```
461
```   - output cannot be memories. If this happen, new local variables acting as
```
462
```   memories are introduced.
```
463
```   - array constants, pre, arrow, fby, ite, merge, calls to node with index
```
464
```   access
```
465
```   Thoses values are shared, ie. no duplicate expressions are introduced.
```
466

467
```   Concerning specification, a similar process is applied, replacing an
```
468
```   expression by a list of local variables and definitions
```
469
```*)
```
470

471
```(** normalize_node node returns a normalized node,
```
472
```    ie.
```
374 473
```    - updated locals
```
375 474
```    - new equations
```
376 475
```    -
```
377 476
```*)
```
378
```let normalize_node node =
```
477
```let normalize_node decls node =
```
379 478
```  reset_cpt_fresh ();
```
380 479
```  let inputs_outputs = node.node_inputs@node.node_outputs in
```
480
```  let is_local v =
```
481
```    List.for_all ((<>) v) inputs_outputs in
```
381 482
```  let orig_vars = inputs_outputs@node.node_locals in
```
382 483
```  let not_is_orig_var v =
```
383 484
```    List.for_all ((!=) v) orig_vars in
```
......
465 566
```	annots
```
466 567
```    ) new_annots new_locals
```
467 568
```  in
```
569
```  if !Options.spec <> "no" then
```
570
```    begin
```
571
```      (* Update mutable fields of eexpr to perform normalization of specification/annotations *)
```
572
```      List.iter
```
573
```	(fun a ->
```
574
```	  List.iter
```
575
```	    (fun (_, ann) -> normalize_eexpr decls node inputs_outputs ann)
```
576
```	    a.annots
```
577
```	)
```
578
```	node.node_annot;
```
579
```      match node.node_spec with None -> () | Some s -> normalize_spec decls node [] s
```
580
```    end;
```
581
```
```
582
```
```
583
``` let new_locals = List.filter is_local vars in (* TODO a quoi ca sert ? *)
```
468 584
```  let node =
```
469 585
```    { node with
```
470 586
```      node_locals = all_locals;
```
......
477 593
```  )
```
478 594

479 595

480
```let normalize_decl decl =
```
596
```let normalize_decl (decls: program) (decl: top_decl) : top_decl =
```
481 597
```  match decl.top_decl_desc with
```
482 598
```  | Node nd ->
```
483
```    let decl' = {decl with top_decl_desc = Node (normalize_node nd)} in
```
599
```    let decl' = {decl with top_decl_desc = Node (normalize_node decls nd)} in
```
484 600
```    Hashtbl.replace Corelang.node_table nd.node_id decl';
```
485 601
```    decl'
```
486 602
```  | Open _ | ImportedNode _ | Const _ | TypeDef _ -> decl
```
487 603

488
```let normalize_prog ?(backend="C") decls =
```
604
```let normalize_prog ?(backend="C") decls : program =
```
489 605
```  let old_unfold_arrow_active = !unfold_arrow_active in
```
490 606
```  let old_force_alias_ite = !force_alias_ite in
```
491 607
```  let old_force_alias_internal_fun = !force_alias_internal_fun in
```
......
505 621
```  in
```
506 622

507 623
```  (* Main algorithm: iterates over nodes *)
```
508
```  let res = List.map normalize_decl decls in
```
624
```  let res = List.map (normalize_decl decls) decls in
```
509 625
```
```
510 626
```  (* Restoring previous settings *)
```
511 627
```  unfold_arrow_active := old_unfold_arrow_active;
```

Also available in: Unified diff