Project

General

Profile

« Previous | Next » 

Revision 3e07a17b

Added by Pierre-Loïc Garoche over 2 years ago

Sorting expressions: less bugs

View differences:

src/tools/seal/seal_export.ml
28 28
  in
29 29
 *)
30 30
  
31
  let rec process_sw f_e sw =
31
  let process_sw vars f_e sw =
32 32
    let process_branch g_opt up =
33
      let el = List.map (fun (v,e) -> f_e e) up in
33
      let el = List.map (fun (v,e) -> v, f_e e) up in
34
      (* Sorting list of elements, according to vars, safety check to
35
         ensure that no variable is forgotten. *)
36
      let el, forgotten = List.fold_right (fun v (res, remaining) ->
37
                   let vid = v.var_id in
38
                   if List.mem_assoc vid remaining then
39
                     ((List.assoc vid remaining)::res),
40
                     (List.remove_assoc vid remaining)
41
                   else
42
                     assert false (* Missing variable v in list *)
43
                            ) vars ([], el)
44
      in
45
      assert (forgotten = []);
34 46
      let loc = (List.hd el).expr_loc in
35 47
      let new_e = Corelang.mkexpr loc (Expr_tuple el) in
36 48
      match g_opt with
......
46 58
         in
47 59
         Some g, new_e, loc
48 60
    in
49
    match sw with
61
    let rec process_sw f_e sw = 
62
      match sw with
50 63
    | [] -> assert false
51 64
    | [g_opt,up] -> ((* last case, no need to guard it *)
52 65
      let _, up_e, _ = process_branch g_opt up in
......
59 72
       | Some g ->
60 73
          let tl_e = process_sw f_e tl in
61 74
          Corelang.mkexpr loc (Expr_ite (g, up_e, tl_e)) 
75
    in
76
    process_sw f_e sw
62 77
  in
63 78
    
64
  let e_init = process_sw (fun x -> x) sw_init in
65
  let e_step = process_sw (Corelang.add_pre_expr vl) sw_step in
66
  let e_init_out = process_sw (fun x -> x) init_out in
67
  let e_update_out = process_sw (Corelang.add_pre_expr vl) update_out in
79
  let e_init = process_sw m.mmemory (fun x -> x) sw_init in
80
  let e_step = process_sw m.mmemory (Corelang.add_pre_expr vl) sw_step in
81
  let e_init_out = process_sw copy_nd.node_outputs (fun x -> x) init_out in
82
  let e_update_out = process_sw  copy_nd.node_outputs (Corelang.add_pre_expr vl) update_out in
68 83
  let loc = Location.dummy_loc in
69 84
  let new_nd =
70 85
    { copy_nd with
src/tools/seal/seal_extract.ml
774 774
          prefix
775 775
        :
776 776
          ((expr * bool) list * (ident * expr) list ) list =
777
  Format.eprintf "Build_switch with %a@."
778
    (Utils.fprintf_list ~sep:",@ "
779
       (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a@ ]@]"
780
                               id
781
                               pp_mdefs gel))
782
    mem_defs;
777
  if !debug then
778
    Format.eprintf "Build_switch with %a@."
779
      (Utils.fprintf_list ~sep:",@ "
780
         (fun fmt (id, gel) -> Format.fprintf fmt "%s -> [@[<v 0>%a@ ]@]"
781
                                 id
782
                                 pp_mdefs gel))
783
      mem_defs;
783 784
  (* if all mem_defs have empty guards, we are done, return prefix,
784 785
     mem_defs expr.
785 786

  
......
1157 1158

  
1158 1159
      )
1159 1160
    in
1160
    Format.eprintf "Map: %i elements@." (UpMap.cardinal map);
1161
    if !debug then Format.eprintf "Map: %i elements@." (UpMap.cardinal map);
1161 1162
    UpMap.fold (fun up (common, disj) accu ->
1162
        Format.eprintf
1163
          "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1164
          Guards.pp_short common
1165
          (fprintf_list ~sep:";@ " Guards.pp_long) disj
1166
          UpMap.pp up;
1163
        if !debug then
1164
          Format.eprintf
1165
            "Guards:@.shared: [%a]@.disj: [@[<v 0>%a@ ]@]@.Updates: %a@."
1166
            Guards.pp_short common
1167
            (fprintf_list ~sep:";@ " Guards.pp_long) disj
1168
            UpMap.pp up;
1167 1169
        let disj = clean_disj disj in
1168 1170
        let guard_expr = (gl_as_expr common)@disj in
1169 1171
        

Also available in: Unified diff