Project

General

Profile

Revision 01d48bb0

View differences:

src/automata.ml
24 24
      actual_s : var_decl
25 25
    }
26 26

  
27
let cpvar_decl var_decl =
28
 mkvar_decl var_decl.var_loc ~orig:var_decl.var_orig (var_decl.var_id, var_decl.var_dec_type, var_decl.var_dec_clock, var_decl.var_dec_const, var_decl.var_dec_value)
29

  
27 30
let as_clock var_decl =
28 31
  let tydec = var_decl.var_dec_type in
29 32
  { var_decl with var_dec_type = { ty_dec_desc = Tydec_clock tydec.ty_dec_desc; ty_dec_loc = tydec.ty_dec_loc } }
......
99 102
  let actual_r = mk_new_name used (id ^ "__restart_act") in
100 103
  let actual_s = mk_new_name used (id ^ "__state_act") in
101 104
  {
102
    incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false);
103
    incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false);
104
    incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false);
105
    incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false);
106
    actual_r = mkvar_decl loc (actual_r  , tydec_bool, ckdec_any, false);
107
    actual_s = mkvar_decl loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false)
105
    incoming_r' = mkvar_decl loc (incoming_r', tydec_bool, ckdec_any, false, None);
106
    incoming_s' = mkvar_decl loc (incoming_s', tydec_state typedef.tydef_id, ckdec_any, false, None);
107
    incoming_r = mkvar_decl loc (incoming_r, tydec_bool, ckdec_any, false, None);
108
    incoming_s = mkvar_decl loc (incoming_s, tydec_state typedef.tydef_id, ckdec_any, false, None);
109
    actual_r = mkvar_decl loc (actual_r  , tydec_bool, ckdec_any, false, None);
110
    actual_s = mkvar_decl loc (actual_s  , tydec_state typedef.tydef_id, ckdec_any, false, None)
108 111
  }
109 112

  
110 113
let vars_of_aut_state aut_state =
......
123 126
    node_id = node_id;
124 127
    node_type = Types.new_var ();
125 128
    node_clock = Clocks.new_var true;
126
    node_inputs = var_inputs;
127
    node_outputs = var_outputs;
129
    node_inputs = List.map cpvar_decl var_inputs;
130
    node_outputs = List.map cpvar_decl var_outputs;
128 131
    node_locals = [];
129 132
    node_gencalls = [];
130 133
    node_checks = [];
......
173 176
    node_id = node_id;
174 177
    node_type = Types.new_var ();
175 178
    node_clock = Clocks.new_var true;
176
    node_inputs = var_inputs;
177
    node_outputs = aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs;
178
    node_locals = new_var_locals @ handler.hand_locals;
179
    node_inputs = List.map cpvar_decl var_inputs;
180
    node_outputs = List.map cpvar_decl (aut_state.incoming_r :: aut_state.incoming_s :: new_var_outputs);
181
    node_locals = List.map cpvar_decl (new_var_locals @ handler.hand_locals);
179 182
    node_gencalls = [];
180 183
    node_checks = [];
181 184
    node_asserts = handler.hand_asserts; 
src/backends/C/c_backend.ml
26 26
*)
27 27

  
28 28
let gen_files funs basename prog machines dependencies header_file source_lib_file source_main_file makefile_file machines =
29

  
29 30
  let header_out = open_out header_file in
30 31
  let header_fmt = formatter_of_out_channel header_out in
31 32
  let source_lib_out = open_out source_lib_file in
32 33
  let source_lib_fmt = formatter_of_out_channel source_lib_out in
33
  
34

  
34 35
  let print_header, print_lib_c, print_main_c, print_makefile = funs in
35 36
  (* Generating H file *)
36 37
  print_header header_fmt basename prog machines dependencies;
37
  
38
 
38 39
  (* Generating Lib C file *)
39 40
  print_lib_c source_lib_fmt basename prog machines dependencies;
40

  
41
 
41 42
  close_out header_out;
42 43
  close_out source_lib_out;
43 44

  
......
64 65
    end
65 66
  )
66 67

  
67
let translate_to_c header source_lib source_main makefile basename prog machines dependencies  =
68

  
68
let translate_to_c header source_lib source_main makefile basename prog machines dependencies =
69 69
  match !Options.spec with
70 70
  | "no" -> begin
71 71
    let module HeaderMod = C_backend_header.EmptyMod in
......
77 77
    let module Source = C_backend_src.Main (SourceMod) in
78 78
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
79 79
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
80
        
80

  
81 81
    let funs = 
82 82
      Header.print_alloc_header, 
83 83
      Source.print_lib_c, 
......
100 100
    let module Source = C_backend_src.Main (SourceMod) in
101 101
    let module SourceMain = C_backend_main.Main (SourceMainMod) in
102 102
    let module Makefile = C_backend_makefile.Main (MakefileMod) in
103
        
103

  
104 104
    let funs = 
105 105
      Header.print_alloc_header, 
106 106
      Source.print_lib_c,
src/backends/C/c_backend_common.ml
51 51
    var_dec_type = mktyp Location.dummy_loc Tydec_any;
52 52
    var_dec_clock = mkclock Location.dummy_loc Ckdec_any;
53 53
    var_dec_const = false;
54
    var_dec_value = None;
54 55
    var_type = Type_predef.type_arrow (Types.new_var ()) (Types.new_var ());
55 56
    var_clock = Clocks.new_var true;
56 57
    var_loc = loc }
......
133 134
      (Utils.duplicate 0 (Dimension.size_const_dimension d))
134 135
  | _ -> assert false
135 136

  
137

  
138
let pp_c_tag fmt t =
139
 pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
140

  
141
(* Prints a constant value *)
142
let rec pp_c_const fmt c =
143
  match c with
144
    | Const_int i     -> pp_print_int fmt i
145
    | Const_real r    -> pp_print_string fmt r
146
    | Const_float r   -> pp_print_float fmt r
147
    | Const_tag t     -> pp_c_tag fmt t
148
    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
149
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
150
    | Const_string _ -> assert false (* string occurs in annotations not in C *)
151

  
152
(* Prints a value expression [v], with internal function calls only.
153
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
154
   but an offset suffix may be added for array variables
155
*)
156
let rec pp_c_val self pp_var fmt v =
157
  match v with
158
  | Cst c         -> pp_c_const fmt c
159
  | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
160
  | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
161
  | Power (v, n)  -> assert false
162
  | LocalVar v    -> pp_var fmt v
163
  | StateVar v    ->
164
    (* array memory vars are represented by an indirection to a local var with the right type,
165
       in order to avoid casting everywhere. *)
166
    if Types.is_array_type v.var_type
167
    then fprintf fmt "%a" pp_var v
168
    else fprintf fmt "%s->_reg.%a" self pp_var v
169
  | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
170

  
171
(* Access to the value of a variable:
172
   - if it's not a scalar output, then its name is enough
173
   - otherwise, dereference it (it has been declared as a pointer,
174
     despite its scalar Lustre type)
175
   - moreover, dereference memory array variables.
176
*)
177
let pp_c_var_read m fmt id =
178
  if Types.is_address_type id.var_type
179
  then
180
    if is_memory m id
181
    then fprintf fmt "(*%s)" id.var_id
182
    else fprintf fmt "%s" id.var_id
183
  else
184
    if is_output m id
185
    then fprintf fmt "*%s" id.var_id
186
    else fprintf fmt "%s" id.var_id
187

  
188
(* Addressable value of a variable, the one that is passed around in calls:
189
   - if it's not a scalar non-output, then its name is enough
190
   - otherwise, reference it (it must be passed as a pointer,
191
     despite its scalar Lustre type)
192
*)
193
let pp_c_var_write m fmt id =
194
  if Types.is_address_type id.var_type
195
  then
196
    fprintf fmt "%s" id.var_id
197
  else
198
    if is_output m id
199
    then
200
      fprintf fmt "%s" id.var_id
201
    else
202
      fprintf fmt "&%s" id.var_id
203

  
136 204
(* Declaration of an input variable:
137 205
   - if its type is array/matrix/etc, then declare it as a mere pointer,
138 206
     in order to cope with unknown/parametric array dimensions, 
......
159 227
     known in order to statically allocate memory, 
160 228
     so we print the full type
161 229
*)
162
let pp_c_decl_local_var fmt id =
163
  pp_c_type id.var_id fmt id.var_type
230
let pp_c_decl_local_var m fmt id =
231
  if id.var_dec_const
232
  then
233
    Format.fprintf fmt "%a = %a"
234
      (pp_c_type id.var_id) id.var_type
235
      (pp_c_val "" (pp_c_var_read m)) (get_const_assign m id)
236
  else
237
    Format.fprintf fmt "%a"
238
      (pp_c_type id.var_id) id.var_type
164 239

  
165 240
let pp_c_decl_array_mem self fmt id =
166 241
  fprintf fmt "%a = (%a) (%s->_reg.%s)"
......
177 252
  then pp_c_type (sprintf "(*%s)" id.var_id) fmt (Types.array_base_type id.var_type)
178 253
  else pp_c_type                  id.var_id  fmt id.var_type
179 254

  
180
(* Access to the value of a variable:
181
   - if it's not a scalar output, then its name is enough
182
   - otherwise, dereference it (it has been declared as a pointer,
183
     despite its scalar Lustre type)
184
   - moreover, dereference memory array variables.
185
*)
186
let pp_c_var_read m fmt id =
187
  if Types.is_address_type id.var_type
188
  then
189
    if is_memory m id
190
    then fprintf fmt "(*%s)" id.var_id
191
    else fprintf fmt "%s" id.var_id
192
  else
193
    if is_output m id
194
    then fprintf fmt "*%s" id.var_id
195
    else fprintf fmt "%s" id.var_id
196

  
197
(* Addressable value of a variable, the one that is passed around in calls:
198
   - if it's not a scalar non-output, then its name is enough
199
   - otherwise, reference it (it must be passed as a pointer,
200
     despite its scalar Lustre type)
201
*)
202
let pp_c_var_write m fmt id =
203
  if Types.is_address_type id.var_type
204
  then
205
    fprintf fmt "%s" id.var_id
206
  else
207
    if is_output m id
208
    then
209
      fprintf fmt "%s" id.var_id
210
    else
211
      fprintf fmt "&%s" id.var_id
212

  
213 255
let pp_c_decl_instance_var fmt (name, (node, static)) = 
214 256
  fprintf fmt "%a *%s" pp_machine_memtype_name (node_name node) name
215 257

  
216
let pp_c_tag fmt t =
217
 pp_print_string fmt (if t = tag_true then "1" else if t = tag_false then "0" else t)
218

  
219
(* Prints a constant value *)
220
let rec pp_c_const fmt c =
221
  match c with
222
    | Const_int i     -> pp_print_int fmt i
223
    | Const_real r    -> pp_print_string fmt r
224
    | Const_float r   -> pp_print_float fmt r
225
    | Const_tag t     -> pp_c_tag fmt t
226
    | Const_array ca  -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " pp_c_const) ca
227
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
228
    | Const_string _ -> assert false (* string occurs in annotations not in C *)
229

  
230
(* Prints a value expression [v], with internal function calls only.
231
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
232
   but an offset suffix may be added for array variables
233
*)
234
let rec pp_c_val self pp_var fmt v =
235
  match v with
236
  | Cst c         -> pp_c_const fmt c
237
  | Array vl      -> fprintf fmt "{%a}" (Utils.fprintf_list ~sep:", " (pp_c_val self pp_var)) vl
238
  | Access (t, i) -> fprintf fmt "%a[%a]" (pp_c_val self pp_var) t (pp_c_val self pp_var) i
239
  | Power (v, n)  -> assert false
240
  | LocalVar v    -> pp_var fmt v
241
  | StateVar v    ->
242
    (* array memory vars are represented by an indirection to a local var with the right type,
243
       in order to avoid casting everywhere. *)
244
    if Types.is_array_type v.var_type
245
    then fprintf fmt "%a" pp_var v
246
    else fprintf fmt "%s->_reg.%a" self pp_var v
247
  | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
248

  
249 258
let pp_c_checks self fmt m =
250 259
  Utils.fprintf_list ~sep:"" 
251 260
    (fun fmt (loc, check) -> 
src/backends/C/c_backend_header.ml
36 36
let print_import_standard fmt =
37 37
  fprintf fmt "#include \"%s/arrow.h\"@.@." Version.include_path
38 38

  
39
let print_static_declare_instance attr fmt (i, (m, static)) =
39
let rec print_static_val pp_var fmt v =
40
  match v with
41
  | Cst c         -> pp_c_const fmt c
42
  | LocalVar v    -> pp_var fmt v
43
  | Fun (n, vl)   -> Basic_library.pp_c n (print_static_val pp_var) fmt vl
44
  | _             -> (Format.eprintf "Internal error: C_backend_header.print_static_val"; assert false)
45

  
46
let print_constant m pp_var fmt v =
47
  Format.fprintf fmt "inst ## %s = %a"
48
    v.var_id
49
    (print_static_val pp_var) (Machine_code.get_const_assign m v)
50

  
51
let print_static_constant (m, attr, inst) fmt const_locals =
52
  let pp_var fmt v =
53
    if List.mem v const_locals
54
    then
55
      Format.fprintf fmt "%s ## %s" inst v.var_id
56
    else 
57
      Format.fprintf fmt "%s" v.var_id in
58
  Format.fprintf fmt "%a%t"
59
    (Utils.fprintf_list ~sep:";\\@," (print_constant m pp_var)) const_locals
60
    (Utils.pp_final_char_if_non_empty ";\\@," const_locals)
61

  
62
let print_static_declare_instance (m, attr, inst) const_locals fmt (i, (n, static)) =
63
  let pp_var fmt v =
64
    if List.mem v const_locals
65
    then
66
      Format.fprintf fmt "%s ## %s" inst v.var_id
67
    else 
68
      Format.fprintf fmt "%s" v.var_id in
69
  let values = List.map (Machine_code.value_of_dimension m) static in
40 70
  fprintf fmt "%a(%s, %a%t%s)"
41
    pp_machine_static_declare_name (node_name m)
71
    pp_machine_static_declare_name (node_name n)
42 72
    attr
43
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
73
    (Utils.fprintf_list ~sep:", " (print_static_val pp_var)) values
44 74
    (Utils.pp_final_char_if_non_empty ", " static)
45 75
    i
46 76

  
47
let print_static_declare_macro fmt m =
77
let print_static_declare_macro fmt (m, attr, inst) =
78
  let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
48 79
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
49
  let inst = mk_instance m in
50
  let attr = mk_attribute m in
51
  fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%s %a %s;\\@,%a%t%a;@,@]"
80
  fprintf fmt "@[<v 2>#define %a(%s, %a%t%s)\\@,%a%s %a %s;\\@,%a%t%a;@,@]"
52 81
    pp_machine_static_declare_name m.mname.node_id
53 82
    attr
54 83
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
55 84
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
56 85
    inst
86
    (* constants *)
87
    (print_static_constant (m, attr, inst)) const_locals
57 88
    attr
58 89
    pp_machine_memtype_name m.mname.node_id
59 90
    inst
60
    (Utils.fprintf_list ~sep:";\\@," pp_c_decl_local_var) array_mem
91
    (Utils.fprintf_list ~sep:";\\@," (pp_c_decl_local_var m)) array_mem
61 92
    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)
62 93
    (Utils.fprintf_list ~sep:";\\@,"
63 94
       (fun fmt (i',m') ->
64
	 let path = sprintf "inst ## _%s" i' in
95
	 let path = sprintf "%s ## _%s" inst i' in
65 96
	 fprintf fmt "%a"
66
	   (print_static_declare_instance attr) (path,m')
97
	   (print_static_declare_instance (m, attr, inst) const_locals) (path, m')
67 98
       )) m.minstances
68 99

  
69 100
      
......
73 104
(* Allocation of a node struct:
74 105
   - if node memory is an array/matrix/etc, we cast it to a pointer (see pp_registers_struct)
75 106
*)
76
let print_static_link_macro fmt m =
107
let print_static_link_macro fmt (m, attr, inst) =
77 108
  let array_mem = List.filter (fun v -> Types.is_array_type v.var_type) m.mmemory in
78
  fprintf fmt "@[<v>@[<v 2>#define %a(inst) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
109
  fprintf fmt "@[<v>@[<v 2>#define %a(%s) do {\\@,%a%t%a;\\@]@,} while (0)@.@]"
79 110
    pp_machine_static_link_name m.mname.node_id
111
    inst
80 112
    (Utils.fprintf_list ~sep:";\\@,"
81 113
       (fun fmt v ->
82
	 fprintf fmt "inst._reg.%s = (%a*) &%s"
114
	 fprintf fmt "%s._reg.%s = (%a*) &%s"
115
	   inst
83 116
	   v.var_id
84 117
           (fun fmt v -> pp_c_type "" fmt (Types.array_base_type v.var_type)) v
85 118
	   v.var_id
......
87 120
    (Utils.pp_final_char_if_non_empty ";\\@," array_mem)
88 121
    (Utils.fprintf_list ~sep:";\\@,"
89 122
       (fun fmt (i',m') ->
90
	 let path = sprintf "inst ## _%s" i' in
91
	 fprintf fmt "%a;\\@,inst.%s = &%s"
123
	 let path = sprintf "%s ## _%s" inst i' in
124
	 fprintf fmt "%a;\\@,%s.%s = &%s"
92 125
	   print_static_link_instance (path,m')
126
	   inst
93 127
	   i'
94 128
	   path
95 129
       )) m.minstances
96
      
97
let print_static_alloc_macro fmt m =
98
  fprintf fmt "@[<v>@[<v 2>#define %a(attr,%a%tinst)\\@,%a(attr,%a%tinst);\\@,%a(inst);@]@,@]@."
130

  
131
let print_static_alloc_macro fmt (m, attr, inst) =
132
  fprintf fmt "@[<v>@[<v 2>#define %a(%s, %a%t%s)\\@,%a(%s, %a%t%s);\\@,%a(%s);@]@,@]@."
99 133
    pp_machine_static_alloc_name m.mname.node_id
134
    attr
100 135
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
101 136
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
137
    inst
102 138
    pp_machine_static_declare_name m.mname.node_id
139
    attr
103 140
    (Utils.fprintf_list ~sep:", " (pp_c_var_read m)) m.mstatic
104 141
    (Utils.pp_final_char_if_non_empty ", " m.mstatic)
142
    inst
105 143
    pp_machine_static_link_name m.mname.node_id
144
    inst
106 145

  
107
 
108 146
let print_machine_decl fmt m =
109 147
  Mod.print_machine_decl_prefix fmt m;
110 148
  if fst (get_stateless_status m) then
......
117 155
    begin
118 156
      (* Static allocation *)
119 157
      if !Options.static_mem
120
      then (
121
	fprintf fmt "%a@.%a@.%a@."
122
	  print_static_declare_macro m
123
	  print_static_link_macro m
124
	  print_static_alloc_macro m
125
      )
126
      else ( 
158
      then
159
	begin
160
	  let inst = mk_instance m in
161
	  let attr = mk_attribute m in
162
	  fprintf fmt "%a@.%a@.%a@."
163
	    print_static_declare_macro (m, attr, inst)
164
	    print_static_link_macro (m, attr, inst)
165
	    print_static_alloc_macro (m, attr, inst)
166
	end
167
      else
168
	begin 
127 169
        (* Dynamic allocation *)
128
	fprintf fmt "extern %a;@.@."
129
	  print_alloc_prototype (m.mname.node_id, m.mstatic)
130
      );
170
	  fprintf fmt "extern %a;@.@."
171
	    print_alloc_prototype (m.mname.node_id, m.mstatic)
172
	end;
131 173
      let self = mk_self m in
132 174
      fprintf fmt "extern %a;@.@."
133 175
	(print_reset_prototype self) (m.mname.node_id, m.mstatic);
......
148 190
      then
149 191
	begin
150 192
	  (* Static allocation *)
193
	  let inst = mk_instance m in
194
	  let attr = mk_attribute m in
151 195
	  fprintf fmt "%a@.%a@.%a@."
152
		  print_static_declare_macro m
153
		  print_static_link_macro m
154
		  print_static_alloc_macro m
196
		  print_static_declare_macro (m, attr, inst)
197
		  print_static_link_macro (m, attr, inst)
198
		  print_static_alloc_macro (m, attr, inst)
155 199
	end
156 200
      else
157 201
	begin 
src/backends/C/c_backend_main.ml
31 31
(********************************************************************************************)
32 32

  
33 33
let print_get_input fmt v =
34
  match v.var_type.Types.tdesc with
34
  match (Types.repr v.var_type).Types.tdesc with
35 35
    | Types.Tint -> fprintf fmt "_get_int(\"%s\")" v.var_id
36 36
    | Types.Tbool -> fprintf fmt "_get_bool(\"%s\")" v.var_id
37 37
    | Types.Treal -> fprintf fmt "_get_double(\"%s\")" v.var_id
......
39 39

  
40 40
let print_put_outputs fmt ol = 
41 41
  let po fmt o =
42
    match o.var_type.Types.tdesc with
42
    match (Types.repr o.var_type).Types.tdesc with
43 43
    | Types.Tint -> fprintf fmt "_put_int(\"%s\", %s)" o.var_id o.var_id
44 44
    | Types.Tbool -> fprintf fmt "_put_bool(\"%s\", %s)" o.var_id o.var_id
45 45
    | Types.Treal -> fprintf fmt "_put_double(\"%s\", %s)" o.var_id o.var_id
src/backends/C/c_backend_src.ml
293 293
    pp_machine_alloc_name (node_name m)
294 294
    (Utils.fprintf_list ~sep:", " Dimension.pp_dimension) static
295 295

  
296
let print_alloc_const fmt m =
297
  let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
298
  fprintf fmt "%a%t"
299
    (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals
300
    (Utils.pp_final_char_if_non_empty ";@," const_locals)
301

  
296 302
let print_alloc_array fmt vdecl =
297 303
  let base_type = Types.array_base_type vdecl.var_type in
298 304
  let size_types = Types.array_type_multi_dimension vdecl.var_type in
......
321 327
    fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
322 328
      print_stateless_prototype (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
323 329
      (* locals *)
324
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
330
      (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
325 331
      (Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
326 332
      (* check assertions *)
327 333
      (pp_c_checks self) m
......
336 342
    fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
337 343
      print_stateless_prototype (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
338 344
      (* locals *)
339
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
345
      (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
340 346
      (Utils.pp_final_char_if_non_empty ";" base_locals)
341 347
      (* check assertions *)
342 348
      (pp_c_checks self) m
......
346 352
      (fun fmt -> fprintf fmt "return;")
347 353

  
348 354
let print_reset_code dependencies fmt m self =
349
  fprintf fmt "@[<v 2>%a {@,%a%treturn;@]@,}@.@."
355
  let const_locals = List.filter (fun vdecl -> vdecl.var_dec_const) m.mstep.step_locals in
356
  fprintf fmt "@[<v 2>%a {@,%a%t@,%a%treturn;@]@,}@.@."
350 357
    (print_reset_prototype self) (m.mname.node_id, m.mstatic)
358
    (* constant locals decl *)
359
    (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) const_locals
360
    (Utils.pp_final_char_if_non_empty ";" const_locals)
361
    (* instrs *)
351 362
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr dependencies m self)) m.minit
352 363
    (Utils.pp_newline_if_non_empty m.minit)
353 364

  
......
359 370
    fprintf fmt "@[<v 2>%a {@,%a%t%a%t@,%a%a%t%t@]@,}@.@."
360 371
      (print_step_prototype self) (m.mname.node_id, m.mstep.step_inputs, m.mstep.step_outputs)
361 372
      (* locals *)
362
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) m.mstep.step_locals
373
      (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) m.mstep.step_locals
363 374
      (Utils.pp_final_char_if_non_empty ";@," m.mstep.step_locals)
364 375
      (* array mems *)
365 376
      (Utils.fprintf_list ~sep:";@," (pp_c_decl_array_mem self)) array_mems
......
377 388
    fprintf fmt "@[<v 2>%a {@,%a%t@,%a%a%t%t@]@,}@.@."
378 389
      (print_step_prototype self) (m.mname.node_id, (m.mstep.step_inputs@gen_locals@gen_calls), m.mstep.step_outputs)
379 390
      (* locals *)
380
      (Utils.fprintf_list ~sep:";@," pp_c_decl_local_var) base_locals
391
      (Utils.fprintf_list ~sep:";@," (pp_c_decl_local_var m)) base_locals
381 392
      (Utils.pp_final_char_if_non_empty ";" base_locals)
382 393
      (* check assertions *)
383 394
      (pp_c_checks self) m
......
402 413
      (* Alloc function, only if non static mode *)
403 414
      if (not !Options.static_mem) then  
404 415
	begin
405
	  fprintf fmt "@[<v 2>%a {@,%a@]@,}@.@."
416
	  fprintf fmt "@[<v 2>%a {@,%a%a@]@,}@.@."
406 417
	    print_alloc_prototype (m.mname.node_id, m.mstatic)
418
	    print_alloc_const m
407 419
	    print_alloc_code m;
408 420
	end;
409 421
      let self = mk_self m in
......
435 447
  fprintf source_fmt "@[<v>";
436 448
  List.iter (fun c -> print_const_def source_fmt (const_of_top c)) (get_consts prog);
437 449
  fprintf source_fmt "@]@.";
450

  
438 451
  if not !Options.static_mem then
439 452
    begin
440 453
      fprintf source_fmt "/* External allocation function prototypes */@.";
......
446 459
      List.iter (fun m -> fprintf source_fmt "%a;@." print_alloc_prototype (m.mname.node_id, m.mstatic)) machines;
447 460
      fprintf source_fmt "@]@.";
448 461
    end;
462

  
449 463
  (* Print the struct definitions of all machines. *)
450 464
  fprintf source_fmt "/* Struct definitions */@.";
451 465
  fprintf source_fmt "@[<v>";
src/causality.ml
28 28
   by duplication of some mem vars into local node vars.
29 29
   Thus, cylic dependency errors may only arise between no-mem vars.
30 30
   non-mem variables are:
31
   - inputs: not needed for causality/scheduling, needed only for detecting useless vars
31
   - constants/inputs: not needed for causality/scheduling, needed only for detecting useless vars
32 32
   - read mems (fake vars): same remark as above.
33 33
   - outputs: decoupled from mems, if necessary
34 34
   - locals
......
133 133
let node_local_variables nd =
134 134
 List.fold_left (fun locals v -> ISet.add v.var_id locals) ISet.empty nd.node_locals
135 135

  
136
let node_constant_variables nd =
137
  List.fold_left (fun locals v -> if v.var_dec_const then ISet.add v.var_id locals else locals) ISet.empty nd.node_locals
138

  
136 139
let node_output_variables nd =
137 140
 List.fold_left (fun outputs v -> ISet.add v.var_id outputs) ISet.empty nd.node_outputs
138 141

  
......
533 536

  
534 537
let global_dependency node =
535 538
  let mems = ExprDep.node_memory_variables node in
536
  let inputs = ExprDep.node_input_variables node in
539
  let inputs =
540
    ISet.union
541
      (ExprDep.node_input_variables node)
542
      (ExprDep.node_constant_variables node) in
537 543
  let outputs = ExprDep.node_output_variables node in
538 544
  let node_vars = ExprDep.node_variables node in
539 545
  let (g_non_mems, g_mems) = ExprDep.dependence_graph mems inputs node_vars node in
src/clock_calculus.ml
779 779
      if Types.get_clock_base_type vdecl.var_type <> None
780 780
      then new_ck (Ccarrying ((new_carrier Carry_name scoped),ck)) scoped
781 781
      else ck in
782
  vdecl.var_clock <- ck;
782
  (if vdecl.var_dec_const
783
   then match vdecl.var_dec_value with
784
   | None   -> ()
785
   | Some v ->
786
     begin
787
       let ck_static = clock_expr env v in
788
       try_unify ck ck_static v.expr_loc
789
     end);
790
  try_unify ck vdecl.var_clock vdecl.var_loc;
783 791
  Env.add_value env vdecl.var_id ck
784 792

  
785 793
(* Clocks a variable declaration list *)
src/clock_predef.ml
42 42
  let cuniv = new_carrier Carry_var false in
43 43
  new_ck (Carrow (new_ck (Ccarrying (cuniv, univ)) false, univ))
44 44

  
45
let ck_carrier id ck =
46
 new_ck (Ccarrying (new_carrier (Carry_const id) true, ck)) true
45 47
(* Local Variables: *)
46 48
(* compile-command:"make -C .." *)
47 49
(* End: *)
src/compiler_common.ml
73 73
    Parse.report_error err;
74 74
    raise exc
75 75
  | Corelang.Error (loc, err) as exc ->
76
    eprintf "Parsing error %a%a@."
76
    eprintf "Parsing error: %a%a@."
77 77
      Corelang.pp_error err
78 78
      Location.pp_loc loc;
79 79
    raise exc
......
83 83
  try
84 84
    Stateless.check_prog decls
85 85
  with (Stateless.Error (loc, err)) as exc ->
86
    eprintf "Stateless status error %a%a@."
86
    eprintf "Stateless status error: %a%a@."
87 87
      Stateless.pp_error err
88 88
      Location.pp_loc loc;
89 89
    raise exc
......
95 95
      try
96 96
	Typing.type_prog env decls
97 97
      with (Types.Error (loc,err)) as exc ->
98
	eprintf "Typing error %a%a@."
98
	eprintf "Typing error: %a%a@."
99 99
	  Types.pp_error err
100 100
	  Location.pp_loc loc;
101 101
	raise exc
......
112 112
      try
113 113
	Clock_calculus.clock_prog env decls
114 114
      with (Clocks.Error (loc,err)) as exc ->
115
	eprintf "Clock calculus error %a%a@." Clocks.pp_error err Location.pp_loc loc;
115
	eprintf "Clock calculus error: %a%a@." Clocks.pp_error err Location.pp_loc loc;
116 116
	raise exc
117 117
    end
118 118
  in
src/corelang.ml
41 41
let mkclock loc d =
42 42
  { ck_dec_desc = d; ck_dec_loc = loc }
43 43

  
44
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const) =
44
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
45
  assert (value = None || is_const);
45 46
  { var_id = id;
46 47
    var_orig = orig;
47 48
    var_dec_type = ty_dec;
48 49
    var_dec_clock = ck_dec;
49 50
    var_dec_const = is_const;
51
    var_dec_value = value;
50 52
    var_type = Types.new_var ();
51 53
    var_clock = Clocks.new_var true;
52 54
    var_loc = loc }
......
66 68
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
67 69
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
68 70
    var_dec_const = true;
71
    var_dec_value = None;
69 72
    var_type = c.const_type;
70 73
    var_clock = Clocks.new_var false;
71 74
    var_loc = c.const_loc }
......
93 96
let mkpredef_call loc funname args =
94 97
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
95 98

  
99
let is_clock_dec_type cty =
100
  match cty with
101
  | Tydec_clock _ -> true
102
  | _             -> false
96 103

  
97 104
let const_of_top top_decl =
98 105
  match top_decl.top_decl_desc with
......
578 585
(************************************************************************)
579 586
(*        Renaming                                                      *)
580 587

  
588
let rec rename_static rename cty =
589
 match cty with
590
 | Tydec_array (d, cty') -> Tydec_array (Dimension.expr_replace_expr rename d, rename_static rename cty')
591
 | Tydec_clock cty       -> Tydec_clock (rename_static rename cty)
592
 | Tydec_struct fl       -> Tydec_struct (List.map (fun (f, cty) -> f, rename_static rename cty) fl)
593
 | _                      -> cty
594

  
595
let rec rename_carrier rename cck =
596
 match cck with
597
 | Ckdec_bool cl -> Ckdec_bool (List.map (fun (c, l) -> rename c, l) cl)
598
 | _             -> cck
599

  
600
(*Format.eprintf "Types.rename_static %a = %a@." print_ty ty print_ty res; res*)
601

  
602
(* applies the renaming function [fvar] to all variables of expression [expr] *)
603
 let rec expr_replace_var fvar expr =
604
  { expr with expr_desc = expr_desc_replace_var fvar expr.expr_desc }
605

  
606
 and expr_desc_replace_var fvar expr_desc =
607
   match expr_desc with
608
   | Expr_const _ -> expr_desc
609
   | Expr_ident i -> Expr_ident (fvar i)
610
   | Expr_array el -> Expr_array (List.map (expr_replace_var fvar) el)
611
   | Expr_access (e1, d) -> Expr_access (expr_replace_var fvar e1, d)
612
   | Expr_power (e1, d) -> Expr_power (expr_replace_var fvar e1, d)
613
   | Expr_tuple el -> Expr_tuple (List.map (expr_replace_var fvar) el)
614
   | Expr_ite (c, t, e) -> Expr_ite (expr_replace_var fvar c, expr_replace_var fvar t, expr_replace_var fvar e)
615
   | Expr_arrow (e1, e2)-> Expr_arrow (expr_replace_var fvar e1, expr_replace_var fvar e2) 
616
   | Expr_fby (e1, e2) -> Expr_fby (expr_replace_var fvar e1, expr_replace_var fvar e2)
617
   | Expr_pre e' -> Expr_pre (expr_replace_var fvar e')
618
   | Expr_when (e', i, l)-> Expr_when (expr_replace_var fvar e', fvar i, l)
619
   | Expr_merge (i, hl) -> Expr_merge (fvar i, List.map (fun (t, h) -> (t, expr_replace_var fvar h)) hl)
620
   | Expr_appl (i, e', i') -> Expr_appl (i, expr_replace_var fvar e', Utils.option_map (expr_replace_var fvar) i')
621

  
622
(* Applies the renaming function [fvar] to every rhs
623
   only when the corresponding lhs satisfies predicate [pvar] *)
624
 let eq_replace_rhs_var pvar fvar eq =
625
   let pvar l = List.exists pvar l in
626
   let rec replace lhs rhs =
627
     { rhs with expr_desc = replace_desc lhs rhs.expr_desc }
628
   and replace_desc lhs rhs_desc =
629
     match lhs with
630
     | []  -> assert false
631
     | [_] -> if pvar lhs then expr_desc_replace_var fvar rhs_desc else rhs_desc
632
     | _   ->
633
       (match rhs_desc with
634
       | Expr_tuple tl ->
635
	 Expr_tuple (List.map2 (fun v e -> replace [v] e) lhs tl)
636
       | Expr_appl (f, arg, None) when Basic_library.is_internal_fun f ->
637
	 let args = expr_list_of_expr arg in
638
	 Expr_appl (f, expr_of_expr_list arg.expr_loc (List.map (replace lhs) args), None)
639
       | Expr_array _
640
       | Expr_access _
641
       | Expr_power _
642
       | Expr_const _
643
       | Expr_ident _
644
       | Expr_appl _   ->
645
	 if pvar lhs
646
	 then expr_desc_replace_var fvar rhs_desc
647
	 else rhs_desc
648
       | Expr_ite (c, t, e)   -> Expr_ite (replace lhs c, replace lhs t, replace lhs e)
649
       | Expr_arrow (e1, e2)  -> Expr_arrow (replace lhs e1, replace lhs e2) 
650
       | Expr_fby (e1, e2)    -> Expr_fby (replace lhs e1, replace lhs e2)
651
       | Expr_pre e'          -> Expr_pre (replace lhs e')
652
       | Expr_when (e', i, l) -> let i' = if pvar lhs then fvar i else i
653
				 in Expr_when (replace lhs e', i', l)
654
       | Expr_merge (i, hl)   -> let i' = if pvar lhs then fvar i else i
655
				 in Expr_merge (i', List.map (fun (t, h) -> (t, replace lhs h)) hl)
656
       )
657
   in { eq with eq_rhs = replace eq.eq_lhs eq.eq_rhs }
658

  
659

  
660
 let rec rename_expr  f_node f_var f_const expr =
661
   { expr with expr_desc = rename_expr_desc f_node f_var f_const expr.expr_desc }
662
 and rename_expr_desc f_node f_var f_const expr_desc =
663
   let re = rename_expr  f_node f_var f_const in
664
   match expr_desc with
665
   | Expr_const _ -> expr_desc
666
   | Expr_ident i -> Expr_ident (f_var i)
667
   | Expr_array el -> Expr_array (List.map re el)
668
   | Expr_access (e1, d) -> Expr_access (re e1, d)
669
   | Expr_power (e1, d) -> Expr_power (re e1, d)
670
   | Expr_tuple el -> Expr_tuple (List.map re el)
671
   | Expr_ite (c, t, e) -> Expr_ite (re c, re t, re e)
672
   | Expr_arrow (e1, e2)-> Expr_arrow (re e1, re e2) 
673
   | Expr_fby (e1, e2) -> Expr_fby (re e1, re e2)
674
   | Expr_pre e' -> Expr_pre (re e')
675
   | Expr_when (e', i, l)-> Expr_when (re e', f_var i, l)
676
   | Expr_merge (i, hl) -> 
677
     Expr_merge (f_var i, List.map (fun (t, h) -> (t, re h)) hl)
678
   | Expr_appl (i, e', i') -> 
679
     Expr_appl (f_node i, re e', Utils.option_map re i')
680
  
681
 let rename_node_annot f_node f_var f_const expr  =
682
   expr
683
 (* TODO assert false *)
684

  
685
 let rename_expr_annot f_node f_var f_const annot =
686
   annot
687
 (* TODO assert false *)
688

  
689
let rename_node f_node f_var f_const nd =
690
  let rename_var v = { v with var_id = f_var v.var_id } in
691
  let rename_eq eq = { eq with
692
      eq_lhs = List.map f_var eq.eq_lhs; 
693
      eq_rhs = rename_expr f_node f_var f_const eq.eq_rhs
694
    } 
695
  in
696
  let inputs = List.map rename_var nd.node_inputs in
697
  let outputs = List.map rename_var nd.node_outputs in
698
  let locals = List.map rename_var nd.node_locals in
699
  let gen_calls = List.map (rename_expr f_node f_var f_const) nd.node_gencalls in
700
  let node_checks = List.map (Dimension.expr_replace_var f_var)  nd.node_checks in
701
  let node_asserts = List.map 
702
    (fun a -> 
703
      {a with assert_expr = 
704
	  let expr = a.assert_expr in
705
	  rename_expr f_node f_var f_const expr})
706
    nd.node_asserts
707
  in
708
  let node_stmts = List.map (fun eq -> Eq (rename_eq eq)) (get_node_eqs nd) in
709
  let spec = 
710
    Utils.option_map 
711
      (fun s -> rename_node_annot f_node f_var f_const s) 
712
      nd.node_spec 
713
  in
714
  let annot =
715
    List.map 
716
      (fun s -> rename_expr_annot f_node f_var f_const s) 
717
      nd.node_annot
718
  in
719
  {
720
    node_id = f_node nd.node_id;
721
    node_type = nd.node_type;
722
    node_clock = nd.node_clock;
723
    node_inputs = inputs;
724
    node_outputs = outputs;
725
    node_locals = locals;
726
    node_gencalls = gen_calls;
727
    node_checks = node_checks;
728
    node_asserts = node_asserts;
729
    node_stmts = node_stmts;
730
    node_dec_stateless = nd.node_dec_stateless;
731
    node_stateless = nd.node_stateless;
732
    node_spec = spec;
733
    node_annot = annot;
734
  }
735

  
736

  
737
let rename_const f_const c =
738
  { c with const_id = f_const c.const_id }
739

  
740
let rename_typedef f_var t =
741
  match t.tydef_desc with
742
  | Tydec_enum tags -> { t with tydef_desc = Tydec_enum (List.map f_var tags) }
743
  | _               -> t
744

  
745
let rename_prog f_node f_var f_const prog =
746
  List.rev (
747
    List.fold_left (fun accu top ->
748
      (match top.top_decl_desc with
749
      | Node nd -> 
750
	 { top with top_decl_desc = Node (rename_node f_node f_var f_const nd) }
751
      | Const c -> 
752
	 { top with top_decl_desc = Const (rename_const f_const c) }
753
      | TypeDef tdef ->
754
	 { top with top_decl_desc = TypeDef (rename_typedef f_var tdef) }
755
      | ImportedNode _
756
      | Open _       -> top)
757
      ::accu
758
) [] prog
759
		   )
760

  
761
(**********************************************************************)
762
(* Pretty printers *)
763

  
764
let pp_decl_type fmt tdecl =
765
  match tdecl.top_decl_desc with
766
  | Node nd ->
767
    fprintf fmt "%s: " nd.node_id;
768
    Utils.reset_names ();
769
    fprintf fmt "%a@ " Types.print_ty nd.node_type
770
  | ImportedNode ind ->
771
    fprintf fmt "%s: " ind.nodei_id;
772
    Utils.reset_names ();
773
    fprintf fmt "%a@ " Types.print_ty ind.nodei_type
774
  | Const _ | Open _ | TypeDef _ -> ()
775

  
776
let pp_prog_type fmt tdecl_list =
777
  Utils.fprintf_list ~sep:"" pp_decl_type fmt tdecl_list
778

  
779
let pp_decl_clock fmt cdecl =
780
  match cdecl.top_decl_desc with
781
  | Node nd ->
782
    fprintf fmt "%s: " nd.node_id;
783
    Utils.reset_names ();
784
    fprintf fmt "%a@ " Clocks.print_ck nd.node_clock
785
  | ImportedNode ind ->
786
    fprintf fmt "%s: " ind.nodei_id;
787
    Utils.reset_names ();
788
    fprintf fmt "%a@ " Clocks.print_ck ind.nodei_clock
789
  | Const _ | Open _ | TypeDef _ -> ()
790

  
791
let pp_prog_clock fmt prog =
792
  Utils.fprintf_list ~sep:"" pp_decl_clock fmt prog
793

  
794
let pp_error fmt = function
795
    Main_not_found ->
796
      fprintf fmt "Cannot compile node %s: could not find the node definition.@."
797
	!Options.main_node
798
  | Main_wrong_kind ->
799
    fprintf fmt
800
      "Name %s does not correspond to a (non-imported) node definition.@." 
801
      !Options.main_node
802
  | No_main_specified ->
803
    fprintf fmt "No main node specified@."
804
  | Unbound_symbol sym ->
805
    fprintf fmt
806
      "%s is undefined.@."
807
      sym
808
  | Already_bound_symbol sym -> 
809
    fprintf fmt
810
      "%s is already defined.@."
811
      sym
812
  | Unknown_library sym ->
813
    fprintf fmt
814
      "impossible to load library %s.lusic@.Please compile the corresponding interface or source file.@."
815
      sym
816
  | Wrong_number sym ->
817
    fprintf fmt
818
      "library %s.lusic has a different version number and may crash compiler@.Please recompile the corresponding interface or source file.@."
819
      sym
820

  
821
(* filling node table with internal functions *)
822
let vdecls_of_typ_ck cpt ty =
823
  let loc = Location.dummy_loc in
824
  List.map
825
    (fun _ -> incr cpt;
826
              let name = sprintf "_var_%d" !cpt in
827
              mkvar_decl loc (name, mktyp loc Tydec_any, mkclock loc Ckdec_any, false, None))
828
    (Types.type_list_of_type ty)
829

  
830
let mk_internal_node id =
831
  let spec = None in
832
  let ty = Env.lookup_value Basic_library.type_env id in
833
  let ck = Env.lookup_value Basic_library.clock_env id in
834
  let (tin, tout) = Types.split_arrow ty in
835
  (*eprintf "internal fun %s: %d -> %d@." id (List.length (Types.type_list_of_type tin)) (List.length (Types.type_list_of_type tout));*)
836
  let cpt = ref (-1) in
837
  mktop
838
    (ImportedNode
839
       {nodei_id = id;
840
	nodei_type = ty;
841
	nodei_clock = ck;
842
	nodei_inputs = vdecls_of_typ_ck cpt tin;
843
	nodei_outputs = vdecls_of_typ_ck cpt tout;
844
	nodei_stateless = Types.get_static_value ty <> None;
845
	nodei_spec = spec;
846
	nodei_prototype = None;
847
       	nodei_in_lib = None;
848
       })
849

  
850
let add_internal_funs () =
851
  List.iter
852
    (fun id -> let nd = mk_internal_node id in Hashtbl.add node_table id nd)
853
    Basic_library.internal_funs
854

  
855

  
856

  
857
(* Replace any occurence of a var in vars_to_replace by its associated
858
   expression in defs until e does not contain any such variables *)
859
let rec substitute_expr vars_to_replace defs e =
860
  let se = substitute_expr vars_to_replace defs in
861
  { e with expr_desc = 
862
      let ed = e.expr_desc in
863
      match ed with
864
      | Expr_const _ -> ed
865
      | Expr_array el -> Expr_array (List.map se el)
866
      | Expr_access (e1, d) -> Expr_access (se e1, d)
867
      | Expr_power (e1, d) -> Expr_power (se e1, d)
868
      | Expr_tuple el -> Expr_tuple (List.map se el)
869
      | Expr_ite (c, t, e) -> Expr_ite (se c, se t, se e)
870
      | Expr_arrow (e1, e2)-> Expr_arrow (se e1, se e2) 
871
      | Expr_fby (e1, e2) -> Expr_fby (se e1, se e2)
872
      | Expr_pre e' -> Expr_pre (se e')
873
      | Expr_when (e', i, l)-> Expr_when (se e', i, l)
874
      | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, se h)) hl)
875
      | Expr_appl (i, e', i') -> Expr_appl (i, se e', i')
876
      | Expr_ident i -> 
877
	if List.exists (fun v -> v.var_id = i) vars_to_replace then (
878
	  let eq_i eq = eq.eq_lhs = [i] in
879
	  if List.exists eq_i defs then
880
	    let sub = List.find eq_i defs in
881
	    let sub' = se sub.eq_rhs in
882
	    sub'.expr_desc
883
	  else 
884
	    assert false
885
	)
886
	else
887
	  ed
888

  
889
  }
890
(* FAUT IL RETIRER ?
891
  
892
 let rec expr_to_eexpr  expr =
893
   { eexpr_tag = expr.expr_tag;
894
     eexpr_desc = expr_desc_to_eexpr_desc expr.expr_desc;
895
     eexpr_type = expr.expr_type;
896
     eexpr_clock = expr.expr_clock;
897
     eexpr_loc = expr.expr_loc
898
   }
899
 and expr_desc_to_eexpr_desc expr_desc =
900
   let conv = expr_to_eexpr in
901
   match expr_desc with
902
   | Expr_const c -> EExpr_const (match c with
903
     | Const_int x -> EConst_int x 
904
     | Const_real x -> EConst_real x 
905
     | Const_float x -> EConst_float x 
906
     | Const_tag x -> EConst_tag x 
907
     | _ -> assert false
908

  
909
   )
910
   | Expr_ident i -> EExpr_ident i
911
   | Expr_tuple el -> EExpr_tuple (List.map conv el)
912

  
913
   | Expr_arrow (e1, e2)-> EExpr_arrow (conv e1, conv e2) 
914
   | Expr_fby (e1, e2) -> EExpr_fby (conv e1, conv e2)
915
   | Expr_pre e' -> EExpr_pre (conv e')
916
   | Expr_appl (i, e', i') -> 
917
     EExpr_appl 
918
       (i, conv e', match i' with None -> None | Some(id, _) -> Some id)
919

  
920
   | Expr_when _
921
   | Expr_merge _ -> assert false
922
   | Expr_array _ 
923
   | Expr_access _ 
924
   | Expr_power _  -> assert false
925
   | Expr_ite (c, t, e) -> assert false 
926
   | _ -> assert false
927

  
928
     *)
929
let rec get_expr_calls nodes e =
930
  get_calls_expr_desc nodes e.expr_desc
931
and get_calls_expr_desc nodes expr_desc =
932
  let get_calls = get_expr_calls nodes in
933
  match expr_desc with
934
  | Expr_const _ 
935
   | Expr_ident _ -> Utils.ISet.empty
936
   | Expr_tuple el
937
   | Expr_array el -> List.fold_left (fun accu e -> Utils.ISet.union accu (get_calls e)) Utils.ISet.empty el
938
   | Expr_pre e1 
939
   | Expr_when (e1, _, _) 
940
   | Expr_access (e1, _) 
941
   | Expr_power (e1, _) -> get_calls e1
942
   | Expr_ite (c, t, e) -> Utils.ISet.union (Utils.ISet.union (get_calls c) (get_calls t)) (get_calls e) 
943
   | Expr_arrow (e1, e2) 
944
   | Expr_fby (e1, e2) -> Utils.ISet.union (get_calls e1) (get_calls e2)
945
   | Expr_merge (_, hl) -> List.fold_left (fun accu (_, h) -> Utils.ISet.union accu (get_calls h)) Utils.ISet.empty  hl
946
   | Expr_appl (i, e', i') -> 
947
     if Basic_library.is_internal_fun i then 
948
       (get_calls e') 
949
     else
950
       let calls =  Utils.ISet.add i (get_calls e') in
951
       let test = (fun n -> match n.top_decl_desc with Node nd -> nd.node_id = i | _ -> false) in
952
       if List.exists test nodes then
953
	 match (List.find test nodes).top_decl_desc with
954
	 | Node nd -> Utils.ISet.union (get_node_calls nodes nd) calls
955
	 | _ -> assert false
956
       else 
957
	 calls
958

  
959
and get_eq_calls nodes eq =
960
  get_expr_calls nodes eq.eq_rhs
961
and get_node_calls nodes node =
962
  List.fold_left (fun accu eq -> Utils.ISet.union (get_eq_calls nodes eq) accu) Utils.ISet.empty (get_node_eqs node)
963

  
964
let rec get_expr_vars vars e =
965
  get_expr_desc_vars vars e.expr_desc
966
and get_expr_desc_vars vars expr_desc =
967
  match expr_desc with
968
  | Expr_const _ -> vars
969
  | Expr_ident x -> Utils.ISet.add x vars
970
  | Expr_tuple el
971
  | Expr_array el -> List.fold_left get_expr_vars vars el
972
  | Expr_pre e1 -> get_expr_vars vars e1
973
  | Expr_when (e1, c, _) -> get_expr_vars (Utils.ISet.add c vars) e1 
974
  | Expr_access (e1, d) 
975
  | Expr_power (e1, d)   -> List.fold_left get_expr_vars vars [e1; expr_of_dimension d]
976
  | Expr_ite (c, t, e) -> List.fold_left get_expr_vars vars [c; t; e]
977
  | Expr_arrow (e1, e2) 
978
  | Expr_fby (e1, e2) -> List.fold_left get_expr_vars vars [e1; e2]
979
  | Expr_merge (c, hl) -> List.fold_left (fun vars (_, h) -> get_expr_vars vars h) (Utils.ISet.add c vars) hl
980
  | Expr_appl (_, arg, None)   -> get_expr_vars vars arg
981
  | Expr_appl (_, arg, Some r) -> List.fold_left get_expr_vars vars [arg; r]
982

  
983

  
984
let rec expr_has_arrows e =
985
  expr_desc_has_arrows e.expr_desc
986
and expr_desc_has_arrows expr_desc =
987
  match expr_desc with
988
  | Expr_const _ 
989
  | Expr_ident _ -> false
990
  | Expr_tuple el
991
  | Expr_array el -> List.exists expr_has_arrows el
992
  | Expr_pre e1 
993
  | Expr_when (e1, _, _) 
994
  | Expr_access (e1, _) 
995
  | Expr_power (e1, _) -> expr_has_arrows e1
996
  | Expr_ite (c, t, e) -> List.exists expr_has_arrows [c; t; e]
997
  | Expr_arrow (e1, e2) 
998
  | Expr_fby (e1, e2) -> true
999
  | Expr_merge (_, hl) -> List.exists (fun (_, h) -> expr_has_arrows h) hl
1000
  | Expr_appl (i, e', i') -> expr_has_arrows e'
1001

  
1002
and eq_has_arrows eq =
1003
  expr_has_arrows eq.eq_rhs
1004
and node_has_arrows node =
1005
  List.exists (fun eq -> eq_has_arrows eq) (get_node_eqs node)
1006

  
1007
let mkvar_decl loc ?(orig=false) (id, ty_dec, ck_dec, is_const, value) =
1008
  assert (value = None || is_const);
1009
  { var_id = id;
1010
    var_orig = orig;
1011
    var_dec_type = ty_dec;
1012
    var_dec_clock = ck_dec;
1013
    var_dec_const = is_const;
1014
    var_dec_value = value;
1015
    var_type = Types.new_var ();
1016
    var_clock = Clocks.new_var true;
1017
    var_loc = loc }
1018

  
1019
let mkexpr loc d =
1020
  { expr_tag = Utils.new_tag ();
1021
    expr_desc = d;
1022
    expr_type = Types.new_var ();
1023
    expr_clock = Clocks.new_var true;
1024
    expr_delay = Delay.new_var ();
1025
    expr_annot = None;
1026
    expr_loc = loc }
1027

  
1028
let var_decl_of_const c =
1029
  { var_id = c.const_id;
1030
    var_orig = true;
1031
    var_dec_type = { ty_dec_loc = c.const_loc; ty_dec_desc = Tydec_any };
1032
    var_dec_clock = { ck_dec_loc = c.const_loc; ck_dec_desc = Ckdec_any };
1033
    var_dec_const = true;
1034
    var_dec_value = None;
1035
    var_type = c.const_type;
1036
    var_clock = Clocks.new_var false;
1037
    var_loc = c.const_loc }
1038

  
1039
let mk_new_name used id =
1040
  let rec new_name name cpt =
1041
    if used name
1042
    then new_name (sprintf "_%s_%i" id cpt) (cpt+1)
1043
    else name
1044
  in new_name id 1
1045

  
1046
let mkeq loc (lhs, rhs) =
1047
  { eq_lhs = lhs;
1048
    eq_rhs = rhs;
1049
    eq_loc = loc }
1050

  
1051
let mkassert loc expr =
1052
  { assert_loc = loc;
1053
    assert_expr = expr
1054
  }
1055

  
1056
let mktop_decl loc own itf d =
1057
  { top_decl_desc = d; top_decl_loc = loc; top_decl_owner = own; top_decl_itf = itf }
1058

  
1059
let mkpredef_call loc funname args =
1060
  mkexpr loc (Expr_appl (funname, mkexpr loc (Expr_tuple args), None))
1061

  
1062
let is_clock_dec_type cty =
1063
  match cty with
1064
  | Tydec_clock _ -> true
1065
  | _             -> false
1066

  
1067
let const_of_top top_decl =
1068
  match top_decl.top_decl_desc with
1069
  | Const c -> c
1070
  | _ -> assert false
1071

  
1072
let node_of_top top_decl =
1073
  match top_decl.top_decl_desc with
1074
  | Node nd -> nd
1075
  | _ -> assert false
1076

  
1077
let imported_node_of_top top_decl =
1078
  match top_decl.top_decl_desc with
1079
  | ImportedNode ind -> ind
1080
  | _ -> assert false
1081

  
1082
let typedef_of_top top_decl =
1083
  match top_decl.top_decl_desc with
1084
  | TypeDef tdef -> tdef
1085
  | _ -> assert false
1086

  
1087
let dependency_of_top top_decl =
1088
  match top_decl.top_decl_desc with
1089
  | Open (local, dep) -> (local, dep)
1090
  | _ -> assert false
1091

  
1092
let consts_of_enum_type top_decl =
1093
  match top_decl.top_decl_desc with
1094
  | TypeDef tdef ->
1095
    (match tdef.tydef_desc with
1096
     | Tydec_enum tags -> List.map (fun tag -> let cdecl = { const_id = tag; const_loc = top_decl.top_decl_loc; const_value = Const_tag tag; const_type = Type_predef.type_const tdef.tydef_id } in { top_decl with top_decl_desc = Const cdecl }) tags
1097
     | _               -> [])
1098
  | _ -> assert false
1099

  
1100
(************************************************************)
1101
(*   Eexpr functions *)
1102
(************************************************************)
1103

  
1104
let merge_node_annot ann1 ann2 =
1105
  { requires = ann1.requires @ ann2.requires;
1106
    ensures = ann1.ensures @ ann2.ensures;
1107
    behaviors = ann1.behaviors @ ann2.behaviors;
1108
    spec_loc = ann1.spec_loc
1109
  }
1110

  
1111
let mkeexpr loc expr =
1112
  { eexpr_tag = Utils.new_tag ();
1113
    eexpr_qfexpr = expr;
1114
    eexpr_quantifiers = [];
1115
    eexpr_type = Types.new_var ();
1116
    eexpr_clock = Clocks.new_var true;
1117
    eexpr_normalized = None;
1118
    eexpr_loc = loc }
1119

  
1120
let extend_eexpr q e = { e with eexpr_quantifiers = q@e.eexpr_quantifiers }
1121

  
1122
(*
1123
let mkepredef_call loc funname args =
1124
  mkeexpr loc (EExpr_appl (funname, mkeexpr loc (EExpr_tuple args), None))
1125

  
1126
let mkepredef_unary_call loc funname arg =
1127
  mkeexpr loc (EExpr_appl (funname, arg, None))
1128
*)
1129

  
1130
let merge_expr_annot ann1 ann2 =
1131
  match ann1, ann2 with
1132
    | None, None -> assert false
1133
    | Some _, None -> ann1
1134
    | None, Some _ -> ann2
1135
    | Some ann1, Some ann2 -> Some {
1136
      annots = ann1.annots @ ann2.annots;
1137
      annot_loc = ann1.annot_loc
1138
    }
1139

  
1140
let update_expr_annot node_id e annot =
1141
  List.iter (fun (key, _) -> 
1142
    Annotations.add_expr_ann node_id e.expr_tag key
1143
  ) annot.annots;
1144
  { e with expr_annot = merge_expr_annot e.expr_annot (Some annot) }
1145

  
1146

  
1147
(***********************************************************)
1148
(* Fast access to nodes, by name *)
1149
let (node_table : (ident, top_decl) Hashtbl.t) = Hashtbl.create 30
1150
let consts_table = Hashtbl.create 30
1151

  
1152
let print_node_table fmt () =
1153
  begin
1154
    Format.fprintf fmt "{ /* node table */@.";
1155
    Hashtbl.iter (fun id nd ->
1156
      Format.fprintf fmt "%s |-> %a"
1157
	id
1158
	Printers.pp_short_decl nd
1159
    ) node_table;
1160
    Format.fprintf fmt "}@."
1161
  end
1162

  
1163
let print_consts_table fmt () =
1164
  begin
1165
    Format.fprintf fmt "{ /* consts table */@.";
1166
    Hashtbl.iter (fun id const ->
1167
      Format.fprintf fmt "%s |-> %a"
1168
	id
1169
	Printers.pp_const_decl (const_of_top const)
1170
    ) consts_table;
1171
    Format.fprintf fmt "}@."
1172
  end
1173

  
1174
let node_name td =
1175
    match td.top_decl_desc with 
1176
    | Node nd         -> nd.node_id
1177
    | ImportedNode nd -> nd.nodei_id
1178
    | _ -> assert false
1179

  
1180
let is_generic_node td =
1181
  match td.top_decl_desc with 
1182
  | Node nd         -> List.exists (fun v -> v.var_dec_const) nd.node_inputs
1183
  | ImportedNode nd -> List.exists (fun v -> v.var_dec_const) nd.nodei_inputs
1184
  | _ -> assert false
1185

  
1186
let node_inputs td =
1187
  match td.top_decl_desc with 
1188
  | Node nd         -> nd.node_inputs
1189
  | ImportedNode nd -> nd.nodei_inputs
1190
  | _ -> assert false
1191

  
1192
let node_from_name id =
1193
  try
1194
    Hashtbl.find node_table id
1195
  with Not_found -> (Format.eprintf "Unable to find any node named %s@ @?" id;
1196
		     assert false)
1197

  
1198
let is_imported_node td =
1199
  match td.top_decl_desc with 
1200
  | Node nd         -> false
1201
  | ImportedNode nd -> true
1202
  | _ -> assert false
1203

  
1204

  
1205
(* alias and type definition table *)
1206

  
1207
let mktop = mktop_decl Location.dummy_loc Version.include_path false 
1208

  
1209
let top_int_type = mktop (TypeDef {tydef_id = "int"; tydef_desc = Tydec_int})
1210
let top_bool_type = mktop (TypeDef {tydef_id = "bool"; tydef_desc = Tydec_bool})
1211
let top_float_type = mktop (TypeDef {tydef_id = "float"; tydef_desc = Tydec_float})
1212
let top_real_type = mktop (TypeDef {tydef_id = "real"; tydef_desc = Tydec_real})
1213

  
1214
let type_table =
1215
  Utils.create_hashtable 20 [
1216
    Tydec_int  , top_int_type;
1217
    Tydec_bool , top_bool_type;
1218
    Tydec_float, top_float_type;
1219
    Tydec_real , top_real_type
1220
  ]
1221

  
1222
let print_type_table fmt () =
1223
  begin
1224
    Format.fprintf fmt "{ /* type table */@.";
1225
    Hashtbl.iter (fun tydec tdef ->
1226
      Format.fprintf fmt "%a |-> %a"
1227
	Printers.pp_var_type_dec_desc tydec
1228
	Printers.pp_typedef (typedef_of_top tdef)
1229
    ) type_table;
1230
    Format.fprintf fmt "}@."
1231
  end
1232

  
1233
let rec is_user_type typ =
1234
  match typ with
1235
  | Tydec_int | Tydec_bool | Tydec_real 
1236
  | Tydec_float | Tydec_any | Tydec_const _ -> false
1237
  | Tydec_clock typ' -> is_user_type typ'
1238
  | _ -> true
1239

  
1240
let get_repr_type typ =
1241
  let typ_def = (typedef_of_top (Hashtbl.find type_table typ)).tydef_desc in
1242
  if is_user_type typ_def then typ else typ_def
1243

  
1244
let rec coretype_equal ty1 ty2 =
1245
  let res =
1246
  match ty1, ty2 with
1247
  | Tydec_any           , _
1248
  | _                   , Tydec_any             -> assert false
1249
  | Tydec_const _       , Tydec_const _         -> get_repr_type ty1 = get_repr_type ty2
1250
  | Tydec_const _       , _                     -> let ty1' = (typedef_of_top (Hashtbl.find type_table ty1)).tydef_desc
1251
	       					   in (not (is_user_type ty1')) && coretype_equal ty1' ty2
1252
  | _                   , Tydec_const _         -> coretype_equal ty2 ty1
1253
  | Tydec_int           , Tydec_int
1254
  | Tydec_real          , Tydec_real
1255
  | Tydec_float         , Tydec_float
1256
  | Tydec_bool          , Tydec_bool            -> true
1257
  | Tydec_clock ty1     , Tydec_clock ty2       -> coretype_equal ty1 ty2
1258
  | Tydec_array (d1,ty1), Tydec_array (d2, ty2) -> Dimension.is_eq_dimension d1 d2 && coretype_equal ty1 ty2
1259
  | Tydec_enum tl1      , Tydec_enum tl2        -> List.sort compare tl1 = List.sort compare tl2
1260
  | Tydec_struct fl1    , Tydec_struct fl2      ->
1261
       List.length fl1 = List.length fl2
1262
    && List.for_all2 (fun (f1, t1) (f2, t2) -> f1 = f2 && coretype_equal t1 t2)
1263
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl1)
1264
      (List.sort (fun (f1,_) (f2,_) -> compare f1 f2) fl2)
1265
  | _                                  -> false
1266
  in ((*Format.eprintf "coretype_equal %a %a = %B@." Printers.pp_var_type_dec_desc ty1 Printers.pp_var_type_dec_desc ty2 res;*) res)
1267

  
1268
let tag_true = "true"
1269
let tag_false = "false"
1270
let tag_default = "default"
1271

  
1272
let const_is_bool c =
1273
 match c with
1274
 | Const_tag t -> t = tag_true || t = tag_false
1275
 | _           -> false
1276

  
1277
(* Computes the negation of a boolean constant *)
1278
let const_negation c =
1279
  assert (const_is_bool c);
1280
  match c with
1281
  | Const_tag t when t = tag_true  -> Const_tag tag_false
1282
  | _                              -> Const_tag tag_true
1283

  
1284
let const_or c1 c2 =
1285
  assert (const_is_bool c1 && const_is_bool c2);
1286
  match c1, c2 with
1287
  | Const_tag t1, _            when t1 = tag_true -> c1
1288
  | _           , Const_tag t2 when t2 = tag_true -> c2
1289
  | _                                             -> Const_tag tag_false
1290

  
1291
let const_and c1 c2 =
1292
  assert (const_is_bool c1 && const_is_bool c2);
1293
  match c1, c2 with
1294
  | Const_tag t1, _            when t1 = tag_false -> c1
1295
  | _           , Const_tag t2 when t2 = tag_false -> c2
1296
  | _                                              -> Const_tag tag_true
1297

  
1298
let const_xor c1 c2 =
1299
  assert (const_is_bool c1 && const_is_bool c2);
1300
   match c1, c2 with
1301
  | Const_tag t1, Const_tag t2 when t1 <> t2  -> Const_tag tag_true
1302
  | _                                         -> Const_tag tag_false
1303

  
1304
let const_impl c1 c2 =
1305
  assert (const_is_bool c1 && const_is_bool c2);
1306
  match c1, c2 with
1307
  | Const_tag t1, _ when t1 = tag_false           -> Const_tag tag_true
1308
  | _           , Const_tag t2 when t2 = tag_true -> Const_tag tag_true
1309
  | _                                             -> Const_tag tag_false
1310

  
1311
(* To guarantee uniqueness of tags in enum types *)
1312
let tag_table =
1313
  Utils.create_hashtable 20 [
1314
   tag_true, top_bool_type;
1315
   tag_false, top_bool_type
1316
  ]
1317

  
1318
(* To guarantee uniqueness of fields in struct types *)
1319
let field_table =
1320
  Utils.create_hashtable 20 [
1321
  ]
1322

  
1323
let get_enum_type_tags cty =
1324
(*Format.eprintf "get_enum_type_tags %a@." Printers.pp_var_type_dec_desc cty;*)
1325
 match cty with
1326
 | Tydec_bool    -> [tag_true; tag_false]
1327
 | Tydec_const _ -> (match (typedef_of_top (Hashtbl.find type_table cty)).tydef_desc with
1328
                     | Tydec_enum tl -> tl
1329
                     | _             -> assert false)
1330
 | _            -> assert false
1331

  
1332
let get_struct_type_fields cty =
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff