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

Also available in: Unified diff