Project

General

Profile

Revision 59020713 src/normalization.ml

View differences:

src/normalization.ml
170 170
      then
171 171
	let new_aliases =
172 172
	  List.map2
173
	    (mk_fresh_var (norm_ctx.parentid, norm_ctx.vars) expr.expr_loc)
173
	    (mk_fresh_var (norm_ctx.parentid, (norm_ctx.vars@vars)) expr.expr_loc)
174 174
	    (Types.type_list_of_type expr.expr_type)
175 175
	    (Clocks.clock_list_of_clock expr.expr_clock) in
176 176
	let new_def =
177 177
	  mkeq expr.expr_loc (List.map (fun v -> v.var_id) new_aliases, expr)
178 178
	in
179 179
	(* Typing and Registering machine type *) 
180
	let _ = if Machine_types.is_active then Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr  in
180
	let _ = if Machine_types.is_active then
181
                  Machine_types.type_def (norm_ctx.parentid, norm_ctx.vars) new_aliases expr
182
        in
181 183
	(new_def::defs, new_aliases@vars), replace_expr new_aliases expr
182 184
      else
183 185
	(defs, vars), expr
......
400 402
let normalize_eq_split norm_ctx defvars eq =
401 403
  try
402 404
    let defs, vars = normalize_eq norm_ctx defvars eq in
403
  List.fold_right (fun eq (def, vars) -> 
404
    let eq_defs = Splitting.tuple_split_eq eq in
405
    if eq_defs = [eq] then
406
      eq::def, vars 
407
    else
408
      List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
409
  ) defs ([], vars)  
410

  
411
  with _ -> (
405
    List.fold_right (fun eq (def, vars) -> 
406
        let eq_defs = Splitting.tuple_split_eq eq in
407
        if eq_defs = [eq] then
408
          eq::def, vars 
409
        else
410
          List.fold_left (normalize_eq norm_ctx) (def, vars) eq_defs
411
      ) defs ([], vars)  
412
    
413
  with ex -> (
412 414
    Format.eprintf "Issue normalizing eq split: %a@." Printers.pp_node_eq eq;
413
    assert false
415
    raise ex
414 416
  )
415 417

  
416
let normalize_eexpr decls norm_ctx vars ee = ee (*
417
  (* New output variable *)
418
  let output_id = "spec" ^ string_of_int ee.eexpr_tag in
419
  let output_var = 
420
    mkvar_decl 
421
      ee.eexpr_loc 
422
      (output_id, 
423
       mktyp ee.eexpr_loc Tydec_any, (*TODO: Make it bool when it is spec *)
424
       mkclock ee.eexpr_loc Ckdec_any, 
425
       false (* not a constant *),
426
       None,
427
       None
428
      ) 
418
(* Projecting an eexpr to an eexpr associated to a single
419
   variable. Returns the updated ee, the bounded variable and the
420
   associated statement *)
421
let normalize_pred_eexpr decls norm_ctx (def,vars) ee =
422
  assert (ee.eexpr_quantifiers = []); (* We do not normalize quantifiers yet. This is for very far future. *)
423
  (* don't do anything is eexpr is just a variable *)
424
  let skip =
425
    match ee.eexpr_qfexpr.expr_desc with
426
    | Expr_ident _ | Expr_const _ -> true
427
    | _ -> false
429 428
  in
429
  if skip then
430
    ee, (def, vars)
431
  else (
432
    (* New output variable *)
433
    let output_id = "spec" ^ string_of_int ee.eexpr_tag in
434
    let output_var = 
435
      mkvar_decl 
436
        ee.eexpr_loc 
437
        (output_id, 
438
         mktyp ee.eexpr_loc Tydec_bool, (* It is a predicate, hence a bool *)
439
         mkclock ee.eexpr_loc Ckdec_any, 
440
         false (* not a constant *),
441
         None,
442
         None
443
        ) 
444
    in
445
    let output_expr = expr_of_vdecl output_var in
446
    (* Rebuilding an eexpr with a silly expression, just a variable *)
447
    let ee' = { ee with eexpr_qfexpr = output_expr } in
448

  
449
    (* Now processing a fresh equation output_id = eexpr_qfexpr. We
450
       inline possible calls within, normalize it and type/clock the
451
       result.  *)
452
    let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
453
    (* Inlining any calls *)
454
    let nodes = get_nodes decls in
455
    let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
456
    let vars, eqs =
457
      if calls = [] && not (eq_has_arrows eq) then
458
        vars, [eq]    
459
      else
460
        assert false (* TODO *)
461
    in
462
    
463
    (* Normalizing expr and eqs *)
464
    let defs, vars = List.fold_left (normalize_eq_split norm_ctx) (def, vars) eqs in
465
(*    let todefine =
466
      List.fold_left
467
        (fun m x-> if List.exists (fun y-> x.var_id = y.var_id) (locals) then m else ISet.add x.var_id m)
468
        (ISet.add output_id ISet.empty) vars in
469
 *)      
470

  
471
    (* Typing / Clocking *)
472
    try
473
      ignore (Typing.type_var_decl_list vars !Global.type_env vars);
474
        (*
475
    let env = Typing.type_var_decl [] !Global.type_env xxxx output_var in (* typing the variable *)
476
    (* Format.eprintf "typing var %s: %a@." output_id Types.print_ty output_var.var_type; *)
477
    let env = Typing.type_var_decl_list (vars@node.node_outputs@node.node_inputs) env (vars@node.node_outputs@node.node_inputs) in
478
    (*Format.eprintf "Env: %a@.@?" (Env.pp_env Types.print_ty) env;*)
479
    let undefined_vars = List.fold_left (Typing.type_eq (env, quant_vars@vars) false) todefine defs in
480
  (* check that table is empty *)
481
    if (not (ISet.is_empty undefined_vars)) then
482
      raise (Types.Error (ee.eexpr_loc, Types.Undefined_var undefined_vars));
483
    
484
    (*Format.eprintf "normalized eqs %a@.@?" 
485
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs;  *)
486
         *)
487

  
488
    ee', (defs, vars)
489
    
490
  with (Types.Error (loc,err)) as exc ->
491
    eprintf "Typing error for eexpr %a: %a%a%a@."
492
      Printers.pp_eexpr ee
493
      Types.pp_error err
494
      (Utils.fprintf_list ~sep:", " Printers.pp_node_eq) defs
495
      Location.pp_loc loc
496
  
497
      
498
    ;
499
    raise exc
500
                                     
501
  )
502
    
503
   (*
430 504
  
431 505
  let quant_vars = List.flatten (List.map snd ee.eexpr_quantifiers) in
432 506
  (* Calls are first inlined *)
433
  let nodes = get_nodes decls in
434
  let calls = ISet.elements (get_expr_calls nodes ee.eexpr_qfexpr) in
435
(* TODO remettre egalement, i ly a un probleme de decapsulage de nodes
436
   let calls = List.map 
437
    (fun called_nd -> List.find (fun nd2 -> nd2.node_id = called_nd) nodes) calls 
438
  in
439
*)
507
  
440 508
  (*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;  *)
441
  let eq = mkeq ee.eexpr_loc ([output_id], ee.eexpr_qfexpr) in
442
  let locals = node.node_locals @ (List.fold_left (fun accu (_, q) -> q@accu) [] ee.eexpr_quantifiers) in  
443 509
  let (new_locals, eqs) =
444 510
    if calls = [] && not (eq_has_arrows eq) then
445 511
      (locals, [eq])     
......
485 551
    raise exc
486 552
                                                 *)    
487 553
 
488
    
489
let normalize_spec decls iovars s = s (*
490
  (* Each stmt is normalized *)
491
  let orig_vars = iovars @ s.locals in
554

  
555
(* We use node local vars to make sure we are creating fresh variables *) 
556
let normalize_spec decls parentid (in_vars, out_vars, l_vars) s =  
557
  (* Original set of variables actually visible from here: iun/out and
558
     spec locals (no node locals) *)
559
  let orig_vars = in_vars @ out_vars @ s.locals in
492 560
  let not_is_orig_var v =
493 561
    List.for_all ((!=) v) orig_vars in
494
  let defs, vars = 
495
    let eqs, auts = List.fold_right (fun (el,al) s -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
496
    if auts != [] then assert false; (* Automata should be expanded by now. *)
497
    List.fold_left (normalize_eq node) ([], orig_vars) eqs
562
  let norm_ctx = {
563
      parentid = parentid;
564
      vars = in_vars @ out_vars @ l_vars;
565
      is_output = (fun _ -> false) (* no need to introduce fresh variables for outputs *);
566
    }
567
  in
568
  (* Normalizing existing stmts *)
569
  let eqs, auts = List.fold_right (fun s (el,al)  -> match s with Eq e -> e::el, al | Aut a -> el, a::al) s.stmts ([], []) in
570
  if auts != [] then assert false; (* Automata should be expanded by now. *)
571
  let defsvars = 
572
    List.fold_left (normalize_eq norm_ctx) ([], orig_vars) eqs
573
  in
574
  (* Iterate through predicates and normalize them on the go, creating
575
     fresh variables for any guarantees/assumes/require/ensure *)
576
  let process_predicates l defvars =
577
    List.fold_right (fun ee (accu, defvars) ->
578
        let ee', defvars = normalize_pred_eexpr decls norm_ctx defvars ee in
579
        ee'::accu, defvars
580
      ) l ([], defvars)
498 581
  in
499
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
500 582

  
501
  (*
583
  
584
  let assume', defsvars = process_predicates s.assume defsvars in
585
  let guarantees', defsvars = process_predicates s.guarantees defsvars in
586
  let modes', (defs, vars) =
587
    List.fold_right (
588
        fun m (accu_m, defsvars) ->
589
        let require', defsvars = process_predicates m.require defsvars in
590
        let ensure', defsvars = process_predicates m.ensure defsvars in
591
        { m with require = require'; ensure = ensure' }:: accu_m, defsvars
592
      ) s.modes ([], defsvars)
593
  in
594
  
595
  let new_locals = List.filter not_is_orig_var vars in (* removing inouts and initial locals ones *)
596
   
502 597
      
503 598
  {s with
504 599
    locals = s.locals @ new_locals;
505 600
    stmts = List.map (fun eq -> Eq eq) defs;
506
  let nee _ = () in
507
  (*normalize_eexpr decls iovars in *)
508
  List.iter nee s.assume;
509
  List.iter nee s.guarantees;
510
  List.iter (fun m -> 
511
      List.iter nee m.require;
512
    List.iter nee m.ensure
513
    ) s.modes;
514
   *)
515
  s
516
                                       *)
601
    assume = assume';
602
    guarantees = guarantees';
603
    modes = modes'
604
  }
605
(* let nee _ = () in
606
 *   (\*normalize_eexpr decls iovars in *\)
607
 *   List.iter nee s.assume;
608
 *   List.iter nee s.guarantees;
609
 *   List.iter (fun m -> 
610
 *       List.iter nee m.require;
611
 *     List.iter nee m.ensure
612
 *     ) s.modes; *)
613
   
614

  
615
                                                                     
616
  
617
  
517 618
    
518 619
(* The normalization phase introduces new local variables
519 620
   - output cannot be memories. If this happen, new local variables acting as
......
534 635
*)
535 636
let normalize_node decls node =
536 637
  reset_cpt_fresh ();
537
  let inputs_outputs = node.node_inputs@node.node_outputs in
538
  let orig_vars = inputs_outputs@node.node_locals in
638
  let orig_vars = node.node_inputs@node.node_outputs@node.node_locals in
539 639
  let not_is_orig_var v =
540 640
    List.for_all ((!=) v) orig_vars in
541 641
  let norm_ctx = {
......
636 736

  
637 737
	 Careful: we do not normalize annotations, since they can have the form
638 738
	 x = (a, b, c) *)
639
      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls inputs_outputs s) 
739
      match node.node_spec with None -> None | Some s -> Some (normalize_spec decls node.node_id (node.node_inputs, node.node_outputs, node.node_locals) s) 
640 740
    end
641 741
  in
642 742
  
......
658 758
  match nd.nodei_spec with
659 759
    None -> nd
660 760
  | Some s ->
661
     let inputs_outputs = nd.nodei_inputs@nd.nodei_outputs in
662
     let s = normalize_spec decls inputs_outputs s in
761
     let s = normalize_spec decls nd.nodei_id (nd.nodei_inputs, nd.nodei_outputs, []) s in
663 762
     { nd with nodei_spec = Some s }
664 763
  
665 764
let normalize_decl (decls: program_t) (decl: top_decl) : top_decl =

Also available in: Unified diff