Project

General

Profile

Revision ae08b9fc src/tools/seal/seal_extract.ml

View differences:

src/tools/seal/seal_extract.ml
549 549
      ) ([], true) gel2
550 550
  in
551 551
  not all_invalid, l
552
     
553
(* Rewrite the expression expr, replacing any occurence of a variable
552

  
553
(* Transform the guard expressions ge = [gl1, e1; gl2, e2;...] as
554
   [gl1, e1=id; gl2, e2=id; ...]  *)
555
let mk_ge_eq_id ge id =
556
  List.map
557
    (fun (gl, g_e) ->
558
      gl,
559
      if id = "true" then
560
        g_e
561
      else
562
        match g_e with
563
        | Expr g_e ->
564
           if id = "false" then
565
             Expr (Corelang.push_negations ~neg:true g_e)
566
           else  
567
             let loc = g_e.expr_loc in
568
             Expr(Corelang.mk_eq loc
569
                    g_e
570
                    (Corelang.expr_of_ident id loc))
571
        | _ -> assert false
572
    )  ge 
573

  
574
    (* Rewrite the expression expr, replacing any occurence of a variable
554 575
   by its definition.
555
*)
576
     *)
556 577
let rec rewrite defs expr : elem_guarded_expr list =
557 578
  let rewrite = rewrite defs in
558 579
  let res =
......
578 599
       let ok_else, g_else = concatenate_ge g false e2 in
579 600
       (if ok_then then g_then else [])@
580 601
         (if ok_else then g_else else [])
581
    | Expr_merge (g, branches) ->
582
       assert false (* TODO: deal with merges *)
583
      
584
    | Expr_when (e, _, _) -> rewrite e
602
    | Expr_merge (g_id, branches) ->
603
       if Hashtbl.mem defs g_id then
604
         let g = Hashtbl.find defs g_id in
605
         (* Format.eprintf "Expr_merge %s = %a@." g_id (pp_mdefs pp_elem) g ; *)
606
         List.fold_left (fun accu (id, e) ->
607
             let g = mk_ge_eq_id g id in
608
             let e = rewrite e in
609
             let ok, g_eq_id = concatenate_ge g true e in
610
             if ok then g_eq_id@accu else accu
611
           ) [] branches
612
       else
613
         assert false (* g should be defined already *)
614
    | Expr_when (e, id, l) ->
615
       let e = rewrite e in
616
       let id_def = Hashtbl.find defs id in
617
       let clock = mk_ge_eq_id id_def l in
618
       let ok, new_ge = concatenate_ge clock true e in
619
       if ok then new_ge else []
585 620
    | Expr_arrow _ -> [[], IsInit] (* At this point the only arrow should be true -> false *)
586 621
    | Expr_tuple el ->
587 622
       (* Each expr is associated to its flatten guarded expr list *)
......
628 663
   *        pp_guard_expr) res; *)
629 664
  res
630 665
and add_def defs vid expr =
666
  (* Format.eprintf "Add_def: %s = %a@."
667
   *   vid
668
   *   Printers.pp_expr expr; *)
631 669
  let vid_defs = rewrite defs expr in
670
  (* Format.eprintf "-> @[<v 0>%a@]@."
671
   *   (Utils.fprintf_list ~sep:"@ "
672
   *      (pp_guard_expr pp_elem)) vid_defs;   *)
632 673
  (* Format.eprintf "Add_def: %s = %a@. -> @[<v 0>%a@]@."
633 674
   *     vid
634 675
   *     Printers.pp_expr expr
......
740 781
          ((expr * bool) list * (ident * expr) list ) list =
741 782
  if !seal_debug then
742 783
    report ~level:4 (fun fmt -> Format.fprintf fmt "@[<v 2>Build_switch with@ %a@]@."
743
      (Utils.fprintf_list ~sep:",@ "
744
         (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]"
745
                                 id
746
                                 (pp_mdefs pp_elem) gel))
747
      mem_defs);
784
                                  pp_all_defs
785
                                  mem_defs);
748 786
  (* if all mem_defs have empty guards, we are done, return prefix,
749 787
     mem_defs expr.
750 788

  
......
755 793
  if List.for_all (fun (m,mdefs) ->
756 794
         (* All defs are unguarded *)
757 795
         match mdefs with
758
         | [[], _] -> true
796
         | [[], _] -> true (* Regular unguarded expression *)
797
         | [] -> true (* A unbalanced definition of the memory. Here
798
                         we have m_{k+1} -> m_k *)
759 799
         | _ -> false
760 800
       ) mem_defs
761 801
  then
......
769 809
              | _ -> assert false (* No IsInit expression *)
770 810
            in
771 811
            m,e
812
         | [] -> m, Corelang.expr_of_ident m Location.dummy_loc
772 813
         | _ -> assert false
773 814
       ) mem_defs]
774 815
  else
775 816
    (* Picking a guard *)
776 817
    let elem_opt : expr option = pick_guard mem_defs in
777 818
    match elem_opt with
778
      None -> assert false (* Otherwise the first case should have matched *)
819
      None -> (
820
       Format.eprintf "Issues picking guard in mem_defs: %a@." pp_all_defs mem_defs;
821
       assert false (* Otherwise the first case should have matched *)
822
    )
779 823
    | Some elem -> (
780 824
      report ~level:4 (fun fmt -> Format.fprintf fmt "selecting guard %a@." Printers.pp_expr elem);
781 825
      let pos, neg =

Also available in: Unified diff