Project

General

Profile

Revision a0c92fa8 src/tools/seal/seal_export.ml

View differences:

src/tools/seal/seal_export.ml
62 62
       match g_opt with
63 63
       | None -> (
64 64
         Format.eprintf "SEAL issue: process_sw with %a"
65
           pp_sys sw
65
           (pp_sys Printers.pp_expr) sw
66 66
       ;
67 67
         assert false (* How could this happen anyway ? *)
68 68
       )
......
117 117
  in
118 118
  new_nd, orig_nd
119 119

  
120
    
121
let funsw_to_lustre m update_out =
122
  let orig_nd = m.mname in
123
  let copy_nd = orig_nd (*Corelang.copy_node orig_nd *) in
124
  let output_eq =
125
    let e_update_out = process_sw copy_nd.node_outputs  (fun x -> x) update_out in
126
    [ 
127
      Eq
128
        { eq_loc = Location.dummy_loc;
129
          eq_lhs = List.map (fun v -> v.var_id) copy_nd.node_outputs; 
130
          eq_rhs = e_update_out
131
        };
132
    ]
133
  in
134
  let new_nd =
135
    { copy_nd with
136
      node_id = copy_nd.node_id ^ "_seal";
137
      node_locals = [];
138
      node_stmts = output_eq;
139
    }
140
  in
141
  new_nd, orig_nd
142
  
120 143
  
121
let to_lustre basename prog m sw_init sw_step init_out update_out =
144

  
145
let to_lustre basename prog new_node orig_node =
122 146
  let loc = Location.dummy_loc in
123
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
124 147
  Global.type_env := Typing.type_node !Global.type_env new_node loc;
125 148
  Global.clock_env := Clock_calculus.clock_node !Global.clock_env loc new_node;
126 149

  
......
139 162
  let output_file_verif = !Options.dest_dir ^ "/" ^ basename ^ "_seal_verif.lus" in
140 163
  let out_verif = open_out output_file_verif in
141 164
  let fmt_verif = Format.formatter_of_out_channel out_verif in
142
  let check_nd = Lustre_utils.check_eq new_node orig_nd in
165
  let check_nd = Lustre_utils.check_eq new_node orig_node in
143 166
  let check_top =
144 167
    Corelang.mktop_decl Location.dummy_loc output_file_verif false (Node check_nd)
145 168
  in
146
  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top]);
169
  Format.fprintf fmt_verif "%a@." Printers.pp_prog  (prog@[new_top;check_top])
170
  
171
let node_to_lustre basename prog m sw_init sw_step init_out update_out =
172
  let new_node, orig_nd = sw_to_lustre m sw_init sw_step init_out update_out in
173
  to_lustre basename prog new_node orig_nd
174

  
175
let fun_to_lustre basename prog m update_out =
176
  let new_node, orig_nd = funsw_to_lustre m update_out in
177
  to_lustre basename prog new_node orig_nd
178

  

Also available in: Unified diff