Project

General

Profile

Revision ae08b9fc

View differences:

src/corelang.ml
1408 1408
    | _ -> assert false (* no array, array access, power or merge/when yet *)
1409 1409
  in
1410 1410
  mkexpr e.expr_loc desc
1411
   
1411

  
1412

  
1413
        
1414
let mk_eq l e1 e2 =
1415
  mkpredef_call l "=" [e1; e2]
1416
      
1412 1417
    (* Local Variables: *)
1413 1418
    (* compile-command:"make -C .." *)
1414 1419
    (* End: *)
src/corelang.mli
200 200
val push_negations: ?neg:bool -> expr -> expr
201 201

  
202 202
val add_pre_expr: ident list -> expr -> expr
203
                                            (* Local Variables: *)
203

  
204
val mk_eq: Location.t -> expr -> expr -> expr 
205
(* Local Variables: *)
204 206
(* compile-command:"make -C .." *)
205 207
(* End: *)
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 =
src/tools/seal/seal_utils.ml
63 63
                        | Some gl ->
64 64
                           Format.fprintf fmt "[@[%a@]] -> (%a)@ "
65 65
                             Printers.pp_expr gl pp_up up) sw
66
                  
66
let pp_all_defs =
67
  (Utils.fprintf_list ~sep:",@ "
68
     (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a]@]"
69
                             id
70
                             (pp_mdefs pp_elem) gel))              
67 71
module UpMap =
68
  struct
69
    include Map.Make (
70
                struct
71
                  type t = (ident * expr) list
72
                  let compare l1 l2 =
73
                    let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in
74
                    compare (proj l1) (proj l2) 
75
                end)
76
    let pp = pp_up 
77
  end
72
      struct
73
        include Map.Make (
74
                    struct
75
                      type t = (ident * expr) list
76
                      let compare l1 l2 =
77
                        let proj l = List.map (fun (s,e) -> s, e.expr_tag) l in
78
                        compare (proj l1) (proj l2) 
79
                    end)
80
        let pp = pp_up 
81
      end
78 82
    
79 83
module Guards = struct
80 84
  include Set.Make (
......
88 92
  let pp_long fmt s = pp_gl Printers.pp_expr fmt (elements s)
89 93
end
90 94
                  
91
                  
92

  
95
        
src/tools/zustre/zustre_common.ml
54 54

  
55 55
let get_const_sort = Hashtbl.find const_sorts 
56 56
let get_sort_elems = Hashtbl.find sort_elems
57
let get_tag_sort = Hashtbl.find const_tags
57
let get_tag_sort id = try Hashtbl.find const_tags id with _ -> Format.eprintf "Unable to find sort for tag=%s@." id; assert false
58 58
  
59 59

  
60 60
  
src/types.ml
168 168
    fprintf fmt "_%s" (name_of_type ty.tid)
169 169
  | Tbasic t -> pp_basic fmt t
170 170
  | Tclock t ->
171
    fprintf fmt "%a clock" print_ty t
171
    fprintf fmt "%a%s" print_ty t (if !Options.kind2_print then "" else " clock")
172 172
  | Tstatic (d, t) ->
173 173
    fprintf fmt "(%a:%a)" Dimension.pp_dimension d print_ty t
174 174
  | Tconst t ->
......
204 204
  end
205 205
  | Tbasic t -> BasicT.pp fmt t
206 206
  | Tclock t ->
207
    fprintf fmt "%a clock" print_node_ty t
207
    fprintf fmt "%a%s" print_node_ty t (if !Options.kind2_print then "" else " clock")
208 208
  | Tstatic (_, t) ->
209 209
    fprintf fmt "%a" print_node_ty t
210 210
  | Tconst t ->

Also available in: Unified diff