Project

General

Profile

« Previous | Next » 

Revision 6cbbe1c1

Added by LĂ©lio Brun 8 months ago

start again with spec representation

View differences:

include/arrow.h
23 23

  
24 24
#define _arrow_clear(self) {}
25 25

  
26
#define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y))
26
/* #define _arrow_step(x,y,output,self) ((self)->_reg._first?((self)->_reg._first=0,(*output = x)):(*output = y)) */
27 27

  
28 28
#define _arrow_reset(self) {(self)->_reg._first = 1;}
29 29

  
src/clock_calculus.ml
49 49
  match cr.carrier_desc with
50 50
  | Carry_const _
51 51
  | Carry_name ->
52
      if cr.carrier_scoped then
53
        raise (Scope_carrier cr);
54
      cr.carrier_desc <- Carry_var
52
    if cr.carrier_scoped then
53
      raise (Scope_carrier cr);
54
    cr.carrier_desc <- Carry_var
55 55
  | Carry_var -> ()
56 56
  | Carry_link cr' -> generalize_carrier cr'
57 57

  
58 58
(** Promote monomorphic clock variables to polymorphic clock variables. *)
59 59
(* Generalize by side-effects *)
60 60
let rec generalize ck =
61
    match ck.cdesc with
62
    | Carrow (ck1,ck2) ->
63
        generalize ck1; generalize ck2
64
    | Ctuple clist ->
65
        List.iter generalize clist
66
    | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
67
    | Cvar ->
68
        if ck.cscoped then
69
          raise (Scope_clock ck);
70
        ck.cdesc <- Cunivar 
71
    | Cunivar -> () 
72
    | Clink ck' ->
73
        generalize ck'
74
    | Ccarrying (cr,ck') ->
75
        generalize_carrier cr; generalize ck'
61
  match ck.cdesc with
62
  | Carrow (ck1,ck2) ->
63
    generalize ck1; generalize ck2
64
  | Ctuple clist ->
65
    List.iter generalize clist
66
  | Con (ck',cr,_) -> generalize ck'; generalize_carrier cr
67
  | Cvar ->
68
    if ck.cscoped then
69
      raise (Scope_clock ck);
70
    ck.cdesc <- Cunivar
71
  | Cunivar -> ()
72
  | Clink ck' ->
73
    generalize ck'
74
  | Ccarrying (cr,ck') ->
75
    generalize_carrier cr; generalize ck'
76 76

  
77 77
let try_generalize ck_node loc =
78 78
  try 
79 79
    generalize ck_node
80
  with (Scope_carrier cr) ->
80
  with
81
  | Scope_carrier cr ->
81 82
    raise (Error (loc, Carrier_extrusion (ck_node, cr)))
82
  | (Scope_clock ck) ->
83
  | Scope_clock ck ->
83 84
    raise (Error (loc, Clock_extrusion (ck_node, ck)))
84 85

  
85 86
(* Clocks instanciation *)
......
414 415
  let rec aux ck =
415 416
    match (repr ck).cdesc with
416 417
    | Cvar ->
417
        begin
418
          match !ck_var with
419
          | None ->
420
              ck_var:=Some ck
421
          | Some v ->
422
              (* cannot fail *)
423
              try_unify ck v loc
424
        end
418
      begin
419
        match !ck_var with
420
        | None ->
421
          ck_var := Some ck
422
        | Some v ->
423
          (* cannot fail *)
424
          try_unify ck v loc
425
      end
425 426
    | Ctuple cl ->
426
        List.iter aux cl
427
      List.iter aux cl
427 428
    | Carrow (ck1,ck2) ->
428
        aux ck1; aux ck2
429
      aux ck1; aux ck2
429 430
    | Ccarrying (_, ck1) ->
430
        aux ck1
431
      aux ck1
431 432
    | Con (ck1, _, _) -> aux ck1
432 433
    | _ -> ()
433 434
  in
......
611 612
(** [clock_eq env eq] performs the clock-calculus for equation [eq] in
612 613
    environment [env] *)
613 614
let clock_eq env eq =
614
  let expr_lhs = expr_of_expr_list eq.eq_loc (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
615
  let expr_lhs = expr_of_expr_list eq.eq_loc
616
      (List.map (fun v -> expr_of_ident v eq.eq_loc) eq.eq_lhs) in
615 617
  let ck_rhs = clock_expr env eq.eq_rhs in
616 618
  clock_subtyping_arg env expr_lhs ck_rhs
617 619

  
......
649 651
    else
650 652
 *)
651 653
      if Types.get_clock_base_type vdecl.var_type <> None
652
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
654
      then new_ck (Ccarrying (new_carrier Carry_name scoped, ck)) scoped
653 655
      else ck in
654 656
  (if vdecl.var_dec_const
655 657
   then match vdecl.var_dec_value with
......
685 687
  List.iter (clock_eq new_env) eqs;
686 688
  let ck_ins = clock_of_vlist nd.node_inputs in
687 689
  let ck_outs = clock_of_vlist nd.node_outputs in
688
  let ck_node = new_ck (Carrow (ck_ins,ck_outs)) false in
690
  let ck_node = new_ck (Carrow (ck_ins, ck_outs)) false in
689 691
  unify_imported_clock None ck_node loc;
690
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "%a@ " print_ck ck_node);
692
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Clock of %s: %a@ " nd.node_id print_ck ck_node);
691 693
  (* Local variables may contain first-order carrier variables that should be generalized.
692 694
     That's not the case for types. *)
693 695
  try_generalize ck_node loc;
......
699 701
  (*  if (is_main && is_polymorphic ck_node) then
700 702
      raise (Error (loc,(Cannot_be_polymorphic ck_node)));
701 703
  *)
702
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "%a@ " print_ck ck_node);
704
  Log.report ~level:3 (fun fmt -> Format.fprintf fmt "Generalized clock of %s: %a@ @ " nd.node_id print_ck ck_node);
703 705
  nd.node_clock <- ck_node;
704 706
  Env.add_value env nd.node_id ck_node
705 707

  
src/clocks.ml
191 191
 clock_of_clock_list (List.map (fun ck -> new_ck (Con (ck,cr,l)) true) (clock_list_of_clock ck))
192 192

  
193 193
let clock_current ck =
194
 clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with Con(ck',_,_) -> ck' | _ -> assert false) (clock_list_of_clock ck))
194
  clock_of_clock_list (List.map (fun ck -> match (repr ck).cdesc with
195
      | Con(ck',_,_) -> ck'
196
      | _ -> Format.eprintf "internal error: Clocks.clock_current %a@." print_ck_long (repr ck);
197
        assert false) (clock_list_of_clock ck))
195 198

  
196 199
let clock_of_impnode_clock ck =
197 200
  let ck = repr ck in
......
394 397
  | Factor_zero ->
395 398
    fprintf fmt "Cannot apply clock transformation with factor 0@."
396 399
  | Carrier_extrusion (ck,cr) ->
397
    fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
400
    fprintf fmt "This node has clock@.%a@.It is invalid as the carrier %a escapes its scope@."
398 401
      print_ck ck
399 402
      print_carrier cr
400 403
  | Clock_extrusion (ck_node,ck) ->
401
    fprintf fmt "This node has clock@.%a@.It is invalid as %a escapes its scope@."
404
    fprintf fmt "This node has clock@.%a@.It is invalid as the clock %a escapes its scope@."
402 405
      print_ck ck_node
403 406
      print_ck ck
404 407

  
src/corelang.ml
1009 1009
  | Node nd ->
1010 1010
    fprintf fmt "%s: " nd.node_id;
1011 1011
    Utils.reset_names ();
1012
    fprintf fmt "%a@ " Types.print_ty nd.node_type
1012
    fprintf fmt "%a" Types.print_ty nd.node_type
1013 1013
  | ImportedNode ind ->
1014 1014
    fprintf fmt "%s: " ind.nodei_id;
1015 1015
    Utils.reset_names ();
1016
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
1016
    fprintf fmt "%a" Types.print_ty ind.nodei_type
1017 1017
  | Const _ | Include _ | Open _ | TypeDef _ -> ()
1018 1018

  
1019 1019
let pp_prog_type fmt tdecl_list =
1020
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
1020
  Utils.Format.(pp_print_list
1021
                  ~pp_open_box:pp_open_vbox0
1022
                  pp_decl_type fmt tdecl_list)
1021 1023

  
1022 1024
let pp_decl_clock fmt cdecl =
1023 1025
  match cdecl.top_decl_desc with
src/machine_code.ml
165 165

  
166 166
(* Datastructure updated while visiting equations *)
167 167
type machine_ctx = {
168
  (* machine name *)
169
  id: ident;
168 170
  (* Memories *)
169 171
  m: VSet.t;
170 172
  (* Reset instructions *)
......
181 183
  t: mc_formula_t list;
182 184
}
183 185

  
184
let ctx_init = {
186
let ctx_init id = {
187
  id;
185 188
  m = VSet.empty;
186 189
  si = [];
187 190
  j = IMap.empty;
......
191 194
  t = []
192 195
}
193 196

  
197
let ctx_dummy = ctx_init ""
198

  
194 199
(****************************************************************)
195 200
(* Main function to translate equations into this machine context we
196 201
   are building *) 
197 202
(****************************************************************)
198 203

  
199
let mk_control id vs v l inst =
204
let mk_control v l inst =
200 205
  mkinstr
201
    (Imply (mk_clocked_on id vs, inst.instr_spec))
206
    True
207
    (* (Imply (mk_clocked_on id vs, inst.instr_spec)) *)
202 208
    (MBranch (v, [l, [inst]]))
203 209

  
204
let control_on_clock env ctx ck inst =
205
  let rec aux (ck_ids, vs, ctx, inst as acc) ck =
210
let control_on_clock env ctx ck spec inst =
211
  let rec aux (ck_ids, vs, ctx, spec, inst as acc) ck =
206 212
    match (Clocks.repr ck).cdesc with
207 213
    | Con (ck, cr, l) ->
208 214
      let id = Clocks.const_of_carrier cr in
......
212 218
      let ck_spec = mk_condition v l in
213 219
      aux (id :: ck_ids,
214 220
           v :: vs,
215
           { ctx
216
             with c = IMap.add id ck_spec
217
                      (IMap.add id'
218
                         (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
221
           { ctx with
222
             c = IMap.add id ck_spec
223
                 (IMap.add id' (And [ck_spec; mk_clocked_on ck_ids' vs]) ctx.c)
219 224
           },
220
           mk_control id' (v :: vs) v l inst) ck
225
           Imply (mk_clocked_on id' (v :: vs), spec),
226
           mk_control v l inst) ck
221 227
    | _ -> acc
222 228
  in
223
  let _, _, ctx, inst = aux ([], [], ctx, inst) ck in
224
  ctx, inst
229
  let _, _, ctx, spec, inst = aux ([], [], ctx, spec, inst) ck in
230
  ctx, spec, inst
225 231

  
226 232
let reset_instance env i r c =
227 233
  match r with
228 234
  | Some r ->
229
    [snd (control_on_clock env ctx_init c
230
            (mk_conditional
231
               (translate_guard env r)
232
               [mkinstr True (MReset i)]
233
               [mkinstr True (MNoReset i)]))]
235
    let _, _, inst = control_on_clock env ctx_dummy c True
236
        (mk_conditional
237
           (translate_guard env r)
238
           [mkinstr True (MReset i)]
239
           [mkinstr True (MNoReset i)]) in
240
    [ inst ]
234 241
  | None -> []
235 242

  
236 243

  
237
let translate_eq env ctx eq =
244
let translate_eq env ctx i eq =
238 245
  let translate_expr = translate_expr env in
239 246
  let translate_act = translate_act env in
240
  let control_on_clock ck inst =
241
    let ctx, ins = control_on_clock env ctx ck inst in
242
    { ctx with s = ins :: ctx.s }
247
  let control_on_clock ck spec inst =
248
    let ctx, _spec, inst = control_on_clock env ctx ck spec inst in
249
    { ctx with
250
      s = { inst with
251
            instr_spec = mk_transition ~i ctx.id [] } :: ctx.s }
243 252
  in
244 253
  let reset_instance = reset_instance env in
245 254
  let mkinstr' = mkinstr ~lustre_eq:eq True in
246
  let ctl ?(ck=eq.eq_rhs.expr_clock) instr =
247
    control_on_clock ck (mkinstr' instr) in
255
  let ctl ?(ck=eq.eq_rhs.expr_clock) spec instr =
256
    control_on_clock ck spec (mkinstr' instr) in
248 257

  
249 258
  (* Format.eprintf "translate_eq %a with clock %a@." 
250 259
     Printers.pp_node_eq eq Clocks.print_ck eq.eq_rhs.expr_clock;  *)
251 260
  match eq.eq_lhs, eq.eq_rhs.expr_desc with
252 261
  | [x], Expr_arrow (e1, e2)                     ->
253 262
    let var_x = env.get_var x in
254
    let o = new_instance (Arrow.arrow_top_decl ()) eq.eq_rhs.expr_tag in
263
    let td = Arrow.arrow_top_decl () in
264
    let o = new_instance td eq.eq_rhs.expr_tag in
255 265
    let c1 = translate_expr e1 in
256 266
    let c2 = translate_expr e2 in
257
    let ctx = ctl (MStep ([var_x], o, [c1;c2])) in
267
    let ctx = ctl
268
        (mk_transition (node_name td) [])
269
        (MStep ([var_x], o, [c1;c2])) in
258 270
    { ctx with
259 271
      si = mkinstr True (MReset o) :: ctx.si;
260
      j = IMap.add o (Arrow.arrow_top_decl (), []) ctx.j;
272
      j = IMap.add o (td, []) ctx.j;
261 273
    }
274

  
262 275
  | [x], Expr_pre e1 when env.is_local x    ->
263 276
    let var_x = env.get_var x in
264
    let ctx = ctl (MStateAssign (var_x, translate_expr e1)) in
277
    let ctx = ctl
278
        True
279
        (MStateAssign (var_x, translate_expr e1)) in
265 280
    { ctx with
266 281
      m = VSet.add var_x ctx.m;
267 282
    }
283

  
268 284
  | [x], Expr_fby (e1, e2) when env.is_local x ->
269 285
    let var_x = env.get_var x in
270
    let ctx = ctl (MStateAssign (var_x, translate_expr e2)) in
286
    let ctx = ctl
287
        True
288
        (MStateAssign (var_x, translate_expr e2)) in
271 289
    { ctx with
272 290
      m = VSet.add var_x ctx.m;
273 291
      si = mkinstr' (MStateAssign (var_x, translate_expr e1)) :: ctx.si;
274 292
    }
293

  
275 294
  | p, Expr_appl (f, arg, r)
276 295
    when not (Basic_library.is_expr_internal_fun eq.eq_rhs) ->
277 296
    let var_p = List.map (fun v -> env.get_var v) p in
......
284 303
        el [eq.eq_rhs.expr_clock] in
285 304
    let call_ck = Clock_calculus.compute_root_clock
286 305
        (Clock_predef.ck_tuple env_cks) in
287
    let ctx = ctl ~ck:call_ck (MStep (var_p, o, vl)) in
306
    let ctx = ctl
307
        ~ck:call_ck
308
        True
309
        (MStep (var_p, o, vl)) in
288 310
    (*Clocks.new_var true in
289 311
      Clock_calculus.unify_imported_clock (Some call_ck) eq.eq_rhs.expr_clock eq.eq_rhs.expr_loc;
290 312
      Format.eprintf "call %a: %a: %a@," Printers.pp_expr eq.eq_rhs Clocks.print_ck (Clock_predef.ck_tuple env_cks) Clocks.print_ck call_ck;*)
......
297 319
           else reset_instance o r call_ck)
298 320
          @ ctx.s
299 321
    }
322

  
300 323
  | [x], _ ->
301 324
    let var_x = env.get_var x in
302
    control_on_clock eq.eq_rhs.expr_clock (translate_act (var_x, eq.eq_rhs))
325
    control_on_clock eq.eq_rhs.expr_clock True (translate_act (var_x, eq.eq_rhs))
326

  
303 327
  | _ ->
304 328
    Format.eprintf "internal error: Machine_code.translate_eq %a@?"
305 329
      Printers.pp_node_eq eq;
......
317 341
    locals []
318 342

  
319 343
let translate_eqs env ctx eqs =
320
  List.fold_right (fun eq ctx -> translate_eq env ctx eq) eqs ctx
344
  List.fold_right (fun eq (ctx, i) ->
345
      let ctx = translate_eq env ctx i eq in
346
      ctx, i - 1)
347
    eqs (ctx, List.length eqs)
348
  |> fst
321 349

  
322 350

  
323 351
(****************************************************************)
......
357 385
    in
358 386
    vars, eql, assertl
359 387

  
360
let translate_core sorted_eqs locals other_vars =
388
let translate_core nid sorted_eqs locals other_vars =
361 389
  let constant_eqs = constant_equations locals in
362 390

  
363 391
  let env = build_env locals other_vars  in
364 392

  
365 393
  (* Compute constants' instructions  *)
366
  let ctx0 = translate_eqs env ctx_init constant_eqs in
394
  let ctx0 = translate_eqs env (ctx_init nid) constant_eqs in
367 395
  assert (VSet.is_empty ctx0.m);
368 396
  assert (ctx0.si = []);
369 397
  assert (IMap.is_empty ctx0.j);
370 398

  
371 399
  (* Compute ctx for all eqs *)
372
  let ctx = translate_eqs env ctx_init sorted_eqs in
400
  let ctx = translate_eqs env (ctx_init nid) sorted_eqs in
373 401

  
374 402
  ctx, ctx0.s
375 403

  
......
402 430
   *   VSet.pp inout_vars
403 431
   * ; *)
404 432

  
405
  let ctx, ctx0_s = translate_core (assert_instrs@sorted_eqs) locals inout_vars in
433
  let ctx, ctx0_s = translate_core
434
      nd.node_id (assert_instrs@sorted_eqs) locals inout_vars in
406 435

  
407 436
  (* Format.eprintf "ok4@.@?"; *)
408 437

  
src/machine_code_common.ml
3 3
open Spec_types
4 4
open Spec_common
5 5
open Corelang
6
  
6
open Utils.Format
7

  
7 8
let print_statelocaltag = true
8 9

  
9 10
let is_memory m id =
......
16 17
  | Var v    ->
17 18
     if is_memory m v then
18 19
       if print_statelocaltag then
19
	 Format.fprintf fmt "%s(S)" v.var_id
20
	 fprintf fmt "{%s}" v.var_id
20 21
       else
21
	 Format.pp_print_string fmt v.var_id 
22
	 pp_print_string fmt v.var_id
22 23
     else     
23 24
       if print_statelocaltag then
24
	 Format.fprintf fmt "%s(L)" v.var_id
25
	 fprintf fmt "%s" v.var_id
25 26
       else
26
	 Format.pp_print_string fmt v.var_id
27
  | Array vl      -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val)  vl
28
  | Access (t, i) -> Format.fprintf fmt "%a[%a]" pp_val t pp_val i
29
  | Power (v, n)  -> Format.fprintf fmt "(%a^%a)" pp_val v pp_val n
30
  | Fun (n, vl)   -> Format.fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
27
	 pp_print_string fmt v.var_id
28
  | Array vl      -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:", " pp_val)  vl
29
  | Access (t, i) -> fprintf fmt "%a[%a]" pp_val t pp_val i
30
  | Power (v, n)  -> fprintf fmt "(%a^%a)" pp_val v pp_val n
31
  | Fun (n, vl)   -> fprintf fmt "%s (%a)" n (Utils.fprintf_list ~sep:", " pp_val)  vl
32

  
33
module PrintSpec = PrintSpec(struct
34
    type t = value_t
35
    type ctx = machine_t
36
    let pp_val = pp_val
37
  end)
31 38

  
32 39
let rec  pp_instr m fmt i =
33 40
 let     pp_val = pp_val m and
34 41
      pp_branch = pp_branch m in
35 42
  let _ =
36 43
    match i.instr_desc with
37
    | MLocalAssign (i,v) -> Format.fprintf fmt "%s<-l- %a" i.var_id pp_val v
38
    | MStateAssign (i,v) -> Format.fprintf fmt "%s<-s- %a" i.var_id pp_val v
39
    | MReset i           -> Format.fprintf fmt "reset %s" i
40
    | MNoReset i         -> Format.fprintf fmt "noreset %s" i
44
    | MLocalAssign (i,v) -> fprintf fmt "%s := %a" i.var_id pp_val v
45
    | MStateAssign (i,v) -> fprintf fmt "{%s} := %a" i.var_id pp_val v
46
    | MReset i           -> fprintf fmt "reset %s" i
47
    | MNoReset i         -> fprintf fmt "noreset %s" i
41 48
    | MStep (il, i, vl)  ->
42
       Format.fprintf fmt "%a = %s (%a)"
43
	 (Utils.fprintf_list ~sep:", " (fun fmt v -> Format.pp_print_string fmt v.var_id)) il
49
       fprintf fmt "%a = %s (%a)"
50
	 (Utils.fprintf_list ~sep:", " (fun fmt v -> pp_print_string fmt v.var_id)) il
44 51
	 i
45 52
	 (Utils.fprintf_list ~sep:", " pp_val) vl
46 53
    | MBranch (g,hl)     ->
47
       Format.fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
54
       fprintf fmt "@[<v 2>case(%a) {@,%a@,}@]"
48 55
	 pp_val g
49 56
	 (Utils.fprintf_list ~sep:"@," pp_branch) hl
50
    | MComment s -> Format.pp_print_string fmt s
51
    | MSpec s -> Format.pp_print_string fmt ("@" ^ s)
57
    | MComment s -> pp_print_string fmt s
58
    | MSpec s -> pp_print_string fmt ("@" ^ s)
52 59
       
53 60
  in
54 61
  (* Annotation *)
55 62
  (* let _ = *)
56
  (*   match i.lustre_expr with None -> () | Some e -> Format.fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
63
  (*   match i.lustre_expr with None -> () | Some e -> fprintf fmt " -- original expr: %a" Printers.pp_expr e *)
57 64
  (* in *)
58
  let _ = 
59
    match i.lustre_eq with None -> () | Some eq -> Format.fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
60
  in
61
  ()
62
    
65
  begin match i.lustre_eq with
66
  | None -> ()
67
  | Some eq -> fprintf fmt " -- original eq: %a" Printers.pp_node_eq eq
68
  end;
69
  fprintf fmt "@ --%@ %a" (PrintSpec.pp_spec m) i.instr_spec
70

  
71

  
63 72
and pp_branch m fmt (t, h) =
64
  Format.fprintf fmt "@[<v 2>%s:@,%a@]" t (Utils.fprintf_list ~sep:"@," (pp_instr m)) h
73
  fprintf fmt "@[<v 2>%s:@,%a@]" t
74
    (pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)) h
65 75

  
66
and pp_instrs m fmt il =
67
  Format.fprintf fmt "@[<v 2>%a@]" (Utils.fprintf_list ~sep:"@," (pp_instr m)) il
76
let pp_instrs m =
77
  pp_print_list ~pp_open_box:pp_open_vbox0 (pp_instr m)
68 78

  
69 79

  
70 80
(* merge log: get_node_def was in c0f8 *)
......
74 84
    let (decl, _) = List.assoc id m.mcalls in
75 85
    Corelang.node_of_top decl
76 86
  with Not_found -> ( 
77
    (* Format.eprintf "Unable to find node %s in list [%a]@.@?" *)
87
    (* eprintf "Unable to find node %s in list [%a]@.@?" *)
78 88
    (*   id *)
79
    (*   (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> Format.fprintf fmt "%s" n)) m.mcalls *)
89
    (*   (Utils.fprintf_list ~sep:", " (fun fmt (n,_) -> fprintf fmt "%s" n)) m.mcalls *)
80 90
    (* ; *)
81 91
    raise Not_found
82 92
  )
......
85 95
let machine_vars m = m.mstep.step_inputs @ m.mstep.step_locals @ m.mstep.step_outputs @ m.mmemory
86 96

  
87 97
let pp_step m fmt s =
88
  Format.fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
89
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_inputs
90
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_outputs
91
    (Utils.fprintf_list ~sep:", " Printers.pp_var) s.step_locals
92
    (Utils.fprintf_list ~sep:", " (fun fmt (_, c) -> pp_val m fmt c)) s.step_checks
93
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) s.step_instrs
94
    (Utils.fprintf_list ~sep:", " (pp_val m)) s.step_asserts
98
  let pp_list = pp_print_list ~pp_sep:pp_print_comma in
99
  fprintf fmt "@[<v>inputs : %a@ outputs: %a@ locals : %a@ checks : %a@ instrs : @[%a@]@ asserts : @[%a@]@]@ "
100
    (pp_list Printers.pp_var) s.step_inputs
101
    (pp_list Printers.pp_var) s.step_outputs
102
    (pp_list Printers.pp_var) s.step_locals
103
    (pp_list (fun fmt (_, c) -> pp_val m fmt c))
104
    s.step_checks
105
    (pp_instrs m) s.step_instrs
106
    (pp_list (pp_val m)) s.step_asserts
95 107

  
96 108

  
97 109
let pp_static_call fmt (node, args) =
98
 Format.fprintf fmt "%s<%a>"
110
 fprintf fmt "%s<%a>"
99 111
   (node_name node)
100 112
   (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) args
101 113

  
102 114
let pp_machine fmt m =
103
  Format.fprintf fmt
115
  fprintf fmt
104 116
    "@[<v 2>machine %s@ \
105 117
     mem      : %a@ \
106 118
     instances: %a@ \
......
112 124
     annot    : @[%a@]@]@ "
113 125
    m.mname.node_id
114 126
    (Utils.fprintf_list ~sep:", " Printers.pp_var) m.mmemory
115
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> Format.fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
127
    (Utils.fprintf_list ~sep:", " (fun fmt (o1, o2) -> fprintf fmt "(%s, %a)" o1 pp_static_call o2)) m.minstances
116 128
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.minit
117 129
    (Utils.fprintf_list ~sep:"@ " (pp_instr m)) m.mconst
118 130
    (pp_step m) m.mstep
119 131
    (fun fmt -> match m.mspec.mnode_spec with
120 132
       | None -> ()
121
       | Some (NodeSpec id) -> Format.fprintf fmt "cocospec: %s" id
133
       | Some (NodeSpec id) -> fprintf fmt "cocospec: %s" id
122 134
       | Some (Contract spec) -> Printers.pp_spec fmt spec)
123 135
    (Utils.fprintf_list ~sep:"@ " Printers.pp_expr_annot) m.mannot
124 136

  
125 137
let pp_machines fmt ml =
126
  Format.fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
138
  fprintf fmt "@[<v 0>%a@]" (Utils.fprintf_list ~sep:"@," pp_machine) ml
127 139

  
128 140
  
129 141
let rec is_const_value v =
......
159 171

  
160 172
let mk_conditional ?lustre_eq c t e =
161 173
  mkinstr ?lustre_eq
162
    (Ternary (Val c,
163
              And (List.map get_instr_spec t),
164
              And (List.map get_instr_spec e)))
174
    (* (Ternary (Val c,
175
     *           And (List.map get_instr_spec t),
176
     *           And (List.map get_instr_spec e))) *)
177
    True
165 178
    (MBranch(c, [
166 179
         (tag_true, t);
167 180
         (tag_false, e) ]))
168 181

  
169 182
let mk_branch ?lustre_eq c br =
170 183
  mkinstr ?lustre_eq
171
    (And (List.map (fun (l, instrs) ->
172
         Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
173
         br))
184
    (* (And (List.map (fun (l, instrs) ->
185
     *      Imply (Equal (Val c, Tag l), And (List.map get_instr_spec instrs)))
186
     *      br)) *)
187
    True
174 188
    (MBranch (c, br))
175 189

  
176 190
let mk_assign ?lustre_eq x v =
177 191
  mkinstr ?lustre_eq
178
    (Equal (Var x, Val v))
192
    (* (Equal (Var x, Val v)) *)
193
    True
179 194
    (MLocalAssign (x, v))
180 195

  
181 196
let mk_val v t =
......
290 305
 try
291 306
    Utils.desome (get_machine_opt machines node_name) 
292 307
 with Utils.DeSome ->
293
   Format.eprintf "Unable to find machine %s in machines %a@.@?"
308
   eprintf "Unable to find machine %s in machines %a@.@?"
294 309
     node_name
295
     (Utils.fprintf_list ~sep:", " (fun fmt m -> Format.pp_print_string fmt m.mname.node_id)) machines
310
     (Utils.fprintf_list ~sep:", " (fun fmt m -> pp_print_string fmt m.mname.node_id)) machines
296 311
      ; assert false
297 312
     
298 313
let get_const_assign m id =
src/machine_code_types.ml
46 46

  
47 47
type static_call = top_decl * (Dimension.dim_expr list)
48 48

  
49
type mc_transition_t = value_t transition_t
50

  
49 51
type machine_spec = {
50 52
  mnode_spec: node_spec_t option;
51
  mtransitions: value_t transition_t list
53
  mtransitions: mc_transition_t list
52 54
}
53 55
  
54 56
type machine_t = {
src/spec_types.ml
14 14
type predicate_t =
15 15
  (* | Memory_pack *)
16 16
  | Clocked_on of ident
17
  | Transition
17
  | Transition of ident * int option
18 18
  | Initialization
19 19

  
20 20
type 'a formula_t =
src/types.ml
187 187
  | Tarray (e, ty) ->
188 188
    fprintf fmt "%a^%a" print_ty ty Dimension.pp_dimension e
189 189
  | Tlink ty ->
190
      print_ty fmt ty
190
    print_ty fmt ty
191 191
  | Tunivar ->
192 192
    fprintf fmt "'%s" (name_of_type ty.tid)
193 193

  
src/typing.ml
208 208
      let rec unif t1 t2 =
209 209
        let t1 = repr t1 in
210 210
        let t2 = repr t2 in
211
        if t1==t2 then
211
        if t1 == t2 then
212 212
          ()
213 213
        else
214 214
          match t1.tdesc,t2.tdesc with
215 215
          (* strictly subtyping cases first *)
216 216
          | _ , Tclock t2 when sub && (get_clock_base_type t1 = None) ->
217
	     unif t1 t2
217
            unif t1 t2
218 218
          | _ , Tstatic (_, t2) when sub && (get_static_value t1 = None) ->
219
	     unif t1 t2
219
            unif t1 t2
220 220
          (* This case is not mandatory but will keep "older" types *)
221 221
          | Tvar, Tvar ->
222
             if t1.tid < t2.tid then
223
               t2.tdesc <- Tlink t1
224
             else
225
               t1.tdesc <- Tlink t2
222
            if t1.tid < t2.tid then
223
              t2.tdesc <- Tlink t1
224
            else
225
              t1.tdesc <- Tlink t2
226 226
          | Tvar, _ when (not semi) && (not (occurs t1 t2)) ->
227
             t1.tdesc <- Tlink t2
227
            t1.tdesc <- Tlink t2
228 228
          | _, Tvar when (not (occurs t2 t1)) ->
229
             t2.tdesc <- Tlink t1
229
            t2.tdesc <- Tlink t1
230 230
          | Tarrow (t1,t2), Tarrow (t1',t2') ->
231
	     begin
232
               unif t2 t2';
233
	       unif t1' t1
234
	     end
231
            begin
232
              unif t2 t2';
233
              unif t1' t1
234
            end
235 235
          | Ttuple tl, Ttuple tl' when List.length tl = List.length tl' ->
236
	     List.iter2 unif tl tl'
236
            List.iter2 unif tl tl'
237 237
          | Ttuple [t1]        , _                  -> unif t1 t2
238 238
          | _                  , Ttuple [t2]        -> unif t1 t2
239 239
          | Tstruct fl, Tstruct fl' when List.map fst fl = List.map fst fl' ->
240
	     List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
240
            List.iter2 (fun (_, t) (_, t') -> unif t t') fl fl'
241 241
          | Tclock _, Tstatic _
242
            | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
242
          | Tstatic _, Tclock _ -> raise (Unify (t1, t2))
243 243
          | Tclock t1', Tclock t2' -> unif t1' t2'
244
          | Tbasic t1, Tbasic t2 when t1 == t2 -> ()
244
          (* | Tbasic t1, Tbasic t2 when t1 == t2 -> () *)
245 245
          | Tunivar, _ | _, Tunivar -> ()
246 246
          | (Tconst t, _) ->
247
	     let def_t = get_type_definition t in
248
	     unif def_t t2
247
            let def_t = get_type_definition t in
248
            unif def_t t2
249 249
          | (_, Tconst t)  ->
250
	     let def_t = get_type_definition t in
251
	     unif t1 def_t
250
            let def_t = get_type_definition t in
251
            unif t1 def_t
252 252
          | Tenum tl, Tenum tl' when tl == tl' -> ()
253 253
          | Tstatic (e1, t1'), Tstatic (e2, t2')
254
            | Tarray (e1, t1'), Tarray (e2, t2') ->
255
	     let eval_const =
256
	       if semi
257
	       then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
258
	       else (fun _ -> None) in
259
	     begin
260
	       unif t1' t2';
261
	       Dimension.eval Basic_library.eval_dim_env eval_const e1;
262
	       Dimension.eval Basic_library.eval_dim_env eval_const e2;
263
	       Dimension.unify ~semi:semi e1 e2;
264
	     end
254
          | Tarray (e1, t1'), Tarray (e2, t2') ->
255
            let eval_const =
256
              if semi
257
              then (fun c -> Some (Dimension.mkdim_ident Location.dummy_loc c))
258
              else (fun _ -> None) in
259
            begin
260
              unif t1' t2';
261
              Dimension.eval Basic_library.eval_dim_env eval_const e1;
262
              Dimension.eval Basic_library.eval_dim_env eval_const e2;
263
              Dimension.unify ~semi:semi e1 e2;
264
            end
265 265
          (* Special cases for machine_types. Rules to unify static types infered
266
      	 for numerical constants with non static ones for variables with
267
      	 possible machine types *)
266
             for numerical constants with non static ones for variables with
267
             possible machine types *)
268 268
          | Tbasic bt1, Tbasic bt2 when BasicT.is_unifiable bt1 bt2 -> BasicT.unify bt1 bt2
269 269
          | _,_ -> raise (Unify (t1, t2))
270 270
      in unif t1 t2
......
274 274
      try
275 275
        unify ~sub:sub ~semi:semi ty1 ty2
276 276
      with
277
      | Unify _ ->
277
      | Unify (t1', t2') ->
278 278
         raise (Error (loc, Type_clash (ty1,ty2)))
279 279
      | Dimension.Unify _ ->
280 280
         raise (Error (loc, Type_clash (ty1,ty2)))

Also available in: Unified diff