Project

General

Profile

Download (16.4 KB) Statistics
| Branch: | Tag: | Revision:
1 2863281f ploc
open Lustre_types
2
open Machine_code_types
3 75c459f4 Lélio Brun
open Spec_types
4 2863281f ploc
open Corelang
5 6cbbe1c1 Lélio Brun
open Utils.Format
6
7 2863281f ploc
let print_statelocaltag = true
8
9 c35de73b ploc
let is_memory m id =
10 70be4acf ploc
  (List.exists (fun o -> o.var_id = id.var_id) m.mmemory) 
11 c35de73b ploc
12 6d1693b9 Lélio Brun
let is_reset_flag id =
13
  id.var_id = "_reset"
14
15
let pp_vdecl fmt v =
16
  pp_print_string fmt v.var_id
17
18 c35de73b ploc
let rec pp_val m fmt v =
19
  let pp_val = pp_val m in
20 2863281f ploc
  match v.value_desc with
21 c35de73b ploc
  | Cst c         -> Printers.pp_const fmt c 
22
  | Var v    ->
23 6d1693b9 Lélio Brun
    if is_memory m v then
24
      if print_statelocaltag then
25
        fprintf fmt "{%s}" v.var_id
26
      else
27
        pp_print_string fmt v.var_id
28
    else
29
    if print_statelocaltag then
30
      fprintf fmt "%s" v.var_id
31
    else
32
      pp_vdecl fmt v
33
  | Array vl      -> pp_print_bracketed pp_val fmt vl
34 6cbbe1c1 Lélio Brun
  | Access (t, i) -> fprintf fmt "%a[%a]" pp_val t pp_val i
35
  | Power (v, n)  -> fprintf fmt "(%a^%a)" pp_val v pp_val n
36 6d1693b9 Lélio Brun
  | Fun (n, vl)   -> fprintf fmt "%s%a" n (pp_print_parenthesized pp_val) vl
37 c4780a6a Lélio Brun
  | ResetFlag     -> fprintf fmt "RESET"
38 6d1693b9 Lélio Brun
39
module PrintSpec = struct
40
41
  let pp_reg fmt = function
42
    | ResetFlag -> pp_print_string fmt "{RESET}"
43
    | StateVar v -> fprintf fmt "{OUT:%a}" pp_vdecl v
44
45
  let pp_expr: type a. machine_t -> formatter -> (value_t, a) expression_t -> unit =
46
    fun m fmt -> function
47
      | Val v -> pp_val m fmt v
48
      | Tag t -> pp_print_string fmt t
49
      | Var v -> pp_vdecl fmt v
50
      | Memory r -> pp_reg fmt r
51
52
  let pp_predicate m fmt p =
53
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
54
      fun fmt e -> pp_expr m fmt e
55
    in
56
    match p with
57 aaa8e454 Lélio Brun
    | Transition (f, inst, i, inputs, locals, outputs, _r, _mems) ->
58 6d1693b9 Lélio Brun
      fprintf fmt "Transition_%a<%a>%a%a"
59
        pp_print_string f
60
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
61
           pp_print_string) inst
62
        (pp_print_option pp_print_int) i
63
        (pp_print_parenthesized pp_expr) (inputs @ locals @ outputs)
64 aaa8e454 Lélio Brun
    | Reset (f, inst, r) ->
65
      fprintf fmt "Reset_%a<%a> on %a"
66
        pp_print_string f
67
        pp_print_string inst
68
        (pp_val m) r
69 6d1693b9 Lélio Brun
    | MemoryPack (f, inst, i) ->
70
      fprintf fmt "MemoryPack_%a<%a>%a"
71
        pp_print_string f
72
        (pp_print_option ~none:(fun fmt () -> pp_print_string fmt "SELF")
73
           pp_print_string) inst
74
        (pp_print_option pp_print_int) i
75
    | ResetCleared f ->
76
      fprintf fmt "ResetCleared_%a" pp_print_string f
77
    | Initialization -> ()
78
79
  let pp_spec m =
80
    let pp_expr: type a. formatter -> (value_t, a) expression_t -> unit =
81
      fun fmt e -> pp_expr m fmt e
82
    in
83
    let rec pp_spec fmt f =
84
      match f with
85
      | True -> pp_print_string fmt "true"
86
      | False -> pp_print_string fmt "false"
87
      | Equal (a, b) ->
88
        fprintf fmt "%a == %a" pp_expr a pp_expr b
89
      | And fs ->
90
        pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∧ ")
91
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs
92
      | Or fs ->
93
        pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ∨ ")
94
          (fun fmt spec -> fprintf fmt "@[%a@]" pp_spec spec) fmt fs
95
      | Imply (a, b) ->
96
        fprintf fmt "%a@ -> %a" pp_spec a pp_spec b
97
      | Exists (xs, a) ->
98
        fprintf fmt "@[<hv 2>∃ @[<h>%a,@]@ %a@]"
99
          (pp_comma_list Printers.pp_var) xs pp_spec a
100
      | Forall (xs, a) ->
101
        fprintf fmt "@[<hv 2>∀ @[<h>%a,@]@ %a@]"
102
          (pp_comma_list Printers.pp_var) xs pp_spec a
103
      | Ternary (e, a, b) ->
104
        fprintf fmt "If %a Then (@[<hov>%a@]) Else (@[<hov>%a@])"
105
          pp_expr e pp_spec a pp_spec b
106
      | Predicate p ->
107
        pp_predicate m fmt p
108
      | StateVarPack r ->
109
        fprintf fmt "StateVarPack<%a>" pp_reg r
110 aaa8e454 Lélio Brun
      | ExistsMem (_f, a, b) ->
111
        fprintf fmt "@[<hv 2>∃ MEM,@ %a@]" pp_spec (And [a; b])
112 6d1693b9 Lélio Brun
    in
113
    pp_spec
114
115
end
116
117
let pp_spec m =
118
  pp_print_list
119
    ~pp_open_box:pp_open_vbox0
120
    ~pp_prologue:pp_print_cut
121
    (fun fmt -> fprintf fmt "@[<h>--%@ %a@]" (PrintSpec.pp_spec m))
122
123
let rec pp_instr m fmt i =
124
  let pp_val = pp_val m in
125
  let pp_branch = pp_branch m in
126
  begin match i.instr_desc with
127 6cbbe1c1 Lélio Brun
    | MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v
128
    | MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v
129 c4780a6a Lélio Brun
    | MResetAssign b     -> fprintf fmt "RESET := %a" pp_print_bool b
130 6d1693b9 Lélio Brun
    | MSetReset i        -> fprintf fmt "set_reset %s" i
131
    | MClearReset        -> fprintf fmt "clear_reset %s" m.mname.node_id
132 6cbbe1c1 Lélio Brun
    | MNoReset i         -> fprintf fmt "noreset %s" i
133 2863281f ploc
    | MStep (il, i, vl)  ->
134 6d1693b9 Lélio Brun
      fprintf fmt "%a := %s%a"
135
        (pp_comma_list pp_vdecl) il
136
        i
137
        (pp_print_parenthesized pp_val) vl
138 2863281f ploc
    | MBranch (g,hl)     ->
139 6d1693b9 Lélio Brun
      fprintf fmt "@[<v 2>case(%a) {@,%a@]@,}"
140
        pp_val g
141
        (pp_print_list ~pp_open_box:pp_open_vbox0 pp_branch) hl
142 6cbbe1c1 Lélio Brun
    | MComment s -> pp_print_string fmt s
143
    | MSpec s -> pp_print_string fmt ("@" ^ s)
144 6d1693b9 Lélio Brun
145
  end;
146 2863281f ploc
  (* Annotation *)
147
  (* let _ = *)
148 6cbbe1c1 Lélio Brun
  (*   match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
149 2863281f ploc
  (* in *)
150 6cbbe1c1 Lélio Brun
  begin match i.lustre_eq with
151
  | None -> ()
152 6d1693b9 Lélio Brun
  | Some eq -> fprintf fmt " @[<h>-- original eq: %a@]" Printers.pp_node_eq eq
153 6cbbe1c1 Lélio Brun
  end;
154 6d1693b9 Lélio Brun
  pp_spec m fmt i.instr_spec
155 6cbbe1c1 Lélio Brun
156
157 c35de73b ploc
and pp_branch m fmt (t, h) =
158 6cbbe1c1 Lélio Brun
  fprintf fmt "@[<v 2>%s:@,%a@]" t
159
    (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)) h
160 2863281f ploc
161 6cbbe1c1 Lélio Brun
let pp_instrs m =
162
  pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
163 2863281f ploc
164
165
(* merge log: get_node_def was in c0f8 *)
166
(* Returns the node/machine associated to id in m calls *)
167
let get_node_def id m =
168
  try
169
    let (decl, _) = List.assoc id m.mcalls in
170
    Corelang.node_of_top decl
171
  with Not_found -> ( 
172 6cbbe1c1 Lélio Brun
    (* eprintf "Unable to find node %s in list [%a]@.@?" *)
173 2863281f ploc
    (*   id *)
174 6cbbe1c1 Lélio Brun
    (*   (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n)) m.mcalls *)
175 2863281f ploc
    (* ; *)
176
    raise Not_found
177
  )
178
    
179
(* merge log: machine_vars was in 44686 *)
180
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
181
182 c35de73b ploc
let pp_step m fmt s =
183 6d1693b9 Lélio Brun
  fprintf fmt
184
    "@[<v>\
185
     inputs : %a@ \
186
     outputs: %a@ \
187
     locals : %a@ \
188
     checks : %a@ \
189
     instrs : @[%a@]@ \
190
     asserts : @[%a@]@]@ "
191
    (pp_comma_list Printers.pp_var) s.step_inputs
192
    (pp_comma_list Printers.pp_var) s.step_outputs
193
    (pp_comma_list Printers.pp_var) s.step_locals
194
    (pp_comma_list (fun fmt (_, c) -> pp_val m fmt c))
195 6cbbe1c1 Lélio Brun
    s.step_checks
196
    (pp_instrs m) s.step_instrs
197 6d1693b9 Lélio Brun
    (pp_comma_list (pp_val m)) s.step_asserts
198 2863281f ploc
199
let pp_static_call fmt (node, args) =
200 6d1693b9 Lélio Brun
  fprintf fmt "%s<%a>"
201
    (node_name node)
202
    (pp_comma_list Dimension.pp_dimension) args
203
204
let pp_instance fmt (o1, o2) =
205
  fprintf fmt "(%s, %a)"
206
    o1
207
    pp_static_call o2
208
209
let pp_memory_pack m fmt mp =
210
  fprintf fmt
211
    "@[<v 2>MemoryPack_%a<SELF>%a =@ %a@]"
212
    pp_print_string mp.mpname.node_id
213
    (pp_print_option pp_print_int) mp.mpindex
214
    (PrintSpec.pp_spec m) mp.mpformula
215
216
let pp_memory_packs m fmt =
217
  fprintf fmt
218
    "@[<v 2>memory_packs:@ %a@]"
219
    (pp_print_list (pp_memory_pack m))
220
221
let pp_transition m fmt t =
222
  fprintf fmt
223
    "@[<v 2>Transition_%a<SELF>%a%a =@ %a@]"
224
    pp_print_string t.tname.node_id
225
    (pp_print_option pp_print_int) t.tindex
226
    (pp_print_parenthesized pp_vdecl) (t.tinputs @ t.tlocals @ t.toutputs)
227
    (PrintSpec.pp_spec m) t.tformula
228
229
let pp_transitions m fmt =
230
  fprintf fmt
231
    "@[<v 2>transitions:@ %a@]"
232
    (pp_print_list (pp_transition m))
233 2863281f ploc
234
let pp_machine fmt m =
235 6cbbe1c1 Lélio Brun
  fprintf fmt
236 7ee5f69e Lélio Brun
    "@[<v 2>machine %s@ \
237
     mem      : %a@ \
238
     instances: %a@ \
239
     init     : %a@ \
240
     const    : %a@ \
241
     step     :@   \
242
     @[<v 2>%a@]@ \
243 6d1693b9 Lélio Brun
     spec     : @[<v>%t@ %a@ @ %a@]@ \
244 7ee5f69e Lélio Brun
     annot    : @[%a@]@]@ "
245 2863281f ploc
    m.mname.node_id
246 6d1693b9 Lélio Brun
    (pp_comma_list Printers.pp_var) m.mmemory
247
    (pp_comma_list pp_instance) m.minstances
248
    (pp_instrs m) m.minit
249
    (pp_instrs m) m.mconst
250 c35de73b ploc
    (pp_step m) m.mstep
251 7ee5f69e Lélio Brun
    (fun fmt -> match m.mspec.mnode_spec with
252
       | None -> ()
253 6cbbe1c1 Lélio Brun
       | Some (NodeSpec id) -> fprintf fmt "cocospec: %s" id
254 7ee5f69e Lélio Brun
       | Some (Contract spec) -> Printers.pp_spec fmt spec)
255 6d1693b9 Lélio Brun
    (pp_memory_packs m) m.mspec.mmemory_packs
256
    (pp_transitions m) m.mspec.mtransitions
257
    (pp_print_list Printers.pp_expr_annot) m.mannot
258 2863281f ploc
259 6d1693b9 Lélio Brun
let pp_machines =
260
  pp_print_list ~pp_open_box:pp_open_vbox0 pp_machine
261 2863281f ploc
262
let rec is_const_value v =
263
  match v.value_desc with
264
  | Cst _          -> true
265 ca7e8027 Lélio Brun
  | Fun (_, args) -> Basic_library.is_value_internal_fun v && List.for_all is_const_value args
266 2863281f ploc
  | _              -> false
267
268
(* Returns the declared stateless status and the computed one. *)
269 9d693675 Lélio Brun
let get_stateless_status_node n =
270
  (n.node_dec_stateless,
271 1fd3d002 ploc
   try
272 9d693675 Lélio Brun
     Utils.desome n.node_stateless
273
   with _ -> failwith ("stateless status of machine " ^ n.node_id ^ " not computed"))
274
275
let get_stateless_status_top_decl td = match td.top_decl_desc with
276
  | Node n -> get_stateless_status_node n
277
  | ImportedNode n -> n.nodei_stateless, false
278
  | _ -> true, false
279
280
let get_stateless_status m =
281
  get_stateless_status_node m.mname
282 2863281f ploc
283 e4edf171 ploc
let is_stateless m = m.minstances = [] && m.mmemory = []
284
285 ca7e8027 Lélio Brun
(* let is_input m id =
286
 *   List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_inputs *)
287 2863281f ploc
288
let is_output m id =
289
  List.exists (fun o -> o.var_id = id.var_id) m.mstep.step_outputs
290
291 75c459f4 Lélio Brun
let get_instr_spec i = i.instr_spec
292 2863281f ploc
293 6d1693b9 Lélio Brun
let mk_val v t =
294
  { value_desc = v;
295
    value_type = t;
296
    value_annot = None }
297
298
let vdecl_to_val vd =
299
  mk_val (Var vd) vd.var_type
300
301
let vdecls_to_vals =
302
  List.map vdecl_to_val
303
304
let id_to_tag id =
305
  let typ = (typedef_of_top (Hashtbl.find Corelang.tag_table id)).tydef_id in
306
  mk_val (Cst (Const_tag id)) (Type_predef.type_const typ)
307
308 2863281f ploc
let mk_conditional ?lustre_eq c t e =
309 75c459f4 Lélio Brun
  mkinstr ?lustre_eq
310 6cbbe1c1 Lélio Brun
    (* (Ternary (Val c,
311
     *           And (List.map get_instr_spec t),
312
     *           And (List.map get_instr_spec e))) *)
313 75c459f4 Lélio Brun
    (MBranch(c, [
314
         (tag_true, t);
315
         (tag_false, e) ]))
316
317
let mk_branch ?lustre_eq c br =
318
  mkinstr ?lustre_eq
319 6cbbe1c1 Lélio Brun
    (* (And (List.map (fun (l, instrs) ->
320
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
321
     *      br)) *)
322 c4780a6a Lélio Brun
    (MBranch (c, br))
323
324
let mk_branch' ?lustre_eq v =
325
  mk_branch ?lustre_eq (vdecl_to_val v)
326 75c459f4 Lélio Brun
327
let mk_assign ?lustre_eq x v =
328
  mkinstr ?lustre_eq
329 6cbbe1c1 Lélio Brun
    (* (Equal (Var x, Val v)) *)
330 75c459f4 Lélio Brun
    (MLocalAssign (x, v))
331 2863281f ploc
332
let arrow_machine =
333
  let state = "_first" in
334
  let var_state = dummy_var_decl state Type_predef.type_bool(* (Types.new_ty Types.Tbool) *) in
335
  let var_input1 = List.nth Arrow.arrow_desc.node_inputs 0 in
336
  let var_input2 = List.nth Arrow.arrow_desc.node_inputs 1 in
337
  let var_output = List.nth Arrow.arrow_desc.node_outputs 0 in
338
  let cst b = mk_val (Cst (const_of_bool b)) Type_predef.type_bool in
339 867276c9 Guillaume DAVY
  assert(var_input1.var_type = var_input2.var_type);
340
  let t_arg = var_input1.var_type in (* TODO Xavier: c'est bien la bonne def ? Guillaume: Bof preferable de reprendre le type des variables non ? *)
341 2863281f ploc
  {
342
    mname = Arrow.arrow_desc;
343
    mmemory = [var_state];
344
    mcalls = [];
345
    minstances = [];
346 6d1693b9 Lélio Brun
    minit = [mkinstr (MStateAssign(var_state, cst true))];
347 2863281f ploc
    mstatic = [];
348
    mconst = [];
349
    mstep = {
350
      step_inputs = Arrow.arrow_desc.node_inputs;
351
      step_outputs = Arrow.arrow_desc.node_outputs;
352
      step_locals = [];
353
      step_checks = [];
354 c35de73b ploc
      step_instrs = [mk_conditional (mk_val (Var var_state) Type_predef.type_bool)
355 6d1693b9 Lélio Brun
                       (List.map mkinstr
356
                          [MStateAssign(var_state, cst false);
357
                           MLocalAssign(var_output, mk_val (Var var_input1) t_arg)])
358
                       (List.map mkinstr
359
                          [MLocalAssign(var_output, mk_val (Var var_input2) t_arg)]) ];
360 2863281f ploc
      step_asserts = [];
361
    };
362 6d1693b9 Lélio Brun
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
363 2863281f ploc
    mannot = [];
364 95fb046e ploc
    msch = None
365 2863281f ploc
  }
366
367
let empty_desc =
368
  {
369
    node_id = Arrow.arrow_id;
370
    node_type = Types.bottom;
371
    node_clock = Clocks.bottom;
372
    node_inputs= [];
373
    node_outputs= [];
374
    node_locals= [];
375
    node_gencalls = [];
376
    node_checks = [];
377
    node_asserts = [];
378
    node_stmts= [];
379
    node_dec_stateless = true;
380
    node_stateless = Some true;
381
    node_spec = None;
382 f4cba4b8 ploc
    node_annot = [];
383
    node_iscontract = false;
384
}
385 2863281f ploc
386
let empty_machine =
387
  {
388
    mname = empty_desc;
389
    mmemory = [];
390
    mcalls = [];
391
    minstances = [];
392
    minit = [];
393
    mstatic = [];
394
    mconst = [];
395
    mstep = {
396
      step_inputs = [];
397
      step_outputs = [];
398
      step_locals = [];
399
      step_checks = [];
400
      step_instrs = [];
401
      step_asserts = [];
402
    };
403 6d1693b9 Lélio Brun
    mspec = { mnode_spec = None; mtransitions = []; mmemory_packs = [] };
404 2863281f ploc
    mannot = [];
405 95fb046e ploc
    msch = None
406 2863281f ploc
  }
407
408
let new_instance =
409
  let cpt = ref (-1) in
410 59020713 ploc
  fun callee tag ->
411 2863281f ploc
    begin
412
      let o =
413
	if Stateless.check_node callee then
414
	  node_name callee
415
	else
416
	  Printf.sprintf "ni_%d" (incr cpt; !cpt) in
417
      let o =
418
	if !Options.ansi && is_generic_node callee
419 59020713 ploc
	then Printf.sprintf "%s_inst_%d"
420
               o
421
               (incr cpt; !cpt)
422 2863281f ploc
	else o in
423
      o
424
    end
425
426
427 e4edf171 ploc
let get_machine_opt machines name =
428 2863281f ploc
  List.fold_left
429
    (fun res m ->
430
      match res with
431
      | Some _ -> res
432
      | None -> if m.mname.node_id = name then Some m else None)
433
    None machines
434
435 e4edf171 ploc
let get_machine machines node_name =
436
 try
437 c3b0a8c9 ploc
    Utils.desome (get_machine_opt machines node_name) 
438
 with Utils.DeSome ->
439 6cbbe1c1 Lélio Brun
   eprintf "Unable to find machine %s in machines %a@.@?"
440 c3b0a8c9 ploc
     node_name
441 6cbbe1c1 Lélio Brun
     (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines
442 c3b0a8c9 ploc
      ; assert false
443 e4edf171 ploc
     
444 2863281f ploc
let get_const_assign m id =
445
  try
446
    match get_instr_desc (List.find
447
	     (fun instr -> match get_instr_desc instr with
448
	     | MLocalAssign (v, _) -> v == id
449
	     | _ -> false)
450
	     m.mconst
451
    ) with
452
    | MLocalAssign (_, e) -> e
453
    | _                   -> assert false
454
  with Not_found -> assert false
455
456
457
let value_of_ident loc m id =
458
  (* is is a state var *)
459
  try
460
    let v = List.find (fun v -> v.var_id = id) m.mmemory
461 c35de73b ploc
    in mk_val (Var v) v.var_type 
462 2863281f ploc
  with Not_found ->
463
    try (* id is a node var *)
464
      let v = get_node_var id m.mname
465 c35de73b ploc
      in mk_val (Var v) v.var_type
466 2863281f ploc
  with Not_found ->
467
    try (* id is a constant *)
468
      let c = Corelang.var_decl_of_const (const_of_top (Hashtbl.find Corelang.consts_table id))
469 c35de73b ploc
      in mk_val (Var c) c.var_type
470 2863281f ploc
    with Not_found ->
471
      (* id is a tag *)
472
      let t = Const_tag id
473
      in mk_val (Cst t) (Typing.type_const loc t)
474
475
(* type of internal fun used in dimension expression *)
476
let type_of_value_appl f args =
477
  if List.mem f Basic_library.arith_funs
478
  then (List.hd args).value_type
479
  else Type_predef.type_bool
480
481
let rec value_of_dimension m dim =
482
  match dim.Dimension.dim_desc with
483
  | Dimension.Dbool b         ->
484 e8f55c25 ploc
     mk_val (Cst (Const_tag (if b then tag_true else tag_false))) Type_predef.type_bool
485 2863281f ploc
  | Dimension.Dint i          ->
486
     mk_val (Cst (Const_int i)) Type_predef.type_int
487
  | Dimension.Dident v        -> value_of_ident dim.Dimension.dim_loc m v
488
  | Dimension.Dappl (f, args) ->
489
     let vargs = List.map (value_of_dimension m) args
490
     in mk_val (Fun (f, vargs)) (type_of_value_appl f vargs) 
491
  | Dimension.Dite (i, t, e)  ->
492
     (match List.map (value_of_dimension m) [i; t; e] with
493
     | [vi; vt; ve] -> mk_val (Fun ("ite", [vi; vt; ve])) vt.value_type
494
     | _            -> assert false)
495
  | Dimension.Dlink dim'      -> value_of_dimension m dim'
496
  | _                         -> assert false
497
498
let rec dimension_of_value value =
499
  match value.value_desc with
500 e8f55c25 ploc
  | Cst (Const_tag t) when t = tag_true  -> Dimension.mkdim_bool  Location.dummy_loc true
501
  | Cst (Const_tag t) when t = tag_false -> Dimension.mkdim_bool  Location.dummy_loc false
502 2863281f ploc
  | Cst (Const_int i)                             -> Dimension.mkdim_int   Location.dummy_loc i
503 c35de73b ploc
  | Var v                                         -> Dimension.mkdim_ident Location.dummy_loc v.var_id
504 2863281f ploc
  | Fun (f, args)                                 -> Dimension.mkdim_appl  Location.dummy_loc f (List.map dimension_of_value args)
505
  | _                                             -> assert false
506
507
508 6d1693b9 Lélio Brun
let rec join_branches hl1 hl2 =
509 2863281f ploc
 match hl1, hl2 with
510
 | []          , _            -> hl2
511
 | _           , []           -> hl1
512
 | (t1, h1)::q1, (t2, h2)::q2 ->
513
   if t1 < t2 then (t1, h1) :: join_branches q1 hl2 else
514
   if t1 > t2 then (t2, h2) :: join_branches hl1 q2
515
   else (t1, List.fold_right join_guards h1 h2) :: join_branches q1 q2
516
517
and join_guards inst1 insts2 =
518 6d1693b9 Lélio Brun
 match get_instr_desc inst1, insts2 with
519
   | MBranch (x1, hl1),
520
     ({ instr_desc = MBranch (x2, hl2); _ } as inst2) :: insts2
521
     when x1 = x2 ->
522
     mkinstr
523
       ~instr_spec:(get_instr_spec inst1 @ get_instr_spec inst2)
524
       (* TODO on pourrait uniquement concatener les lustres de inst1 et hd(inst2) *)
525
       (MBranch (x1, join_branches (sort_handlers hl1) (sort_handlers hl2)))
526
     :: insts2
527
   | _ -> inst1 :: insts2
528 2863281f ploc
529
let join_guards_list insts =
530
 List.fold_right join_guards insts []