Project

General

Profile

Download (22.8 KB) Statistics
| Branch: | Tag: | Revision:
1 a2d97a3e ploc
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
12 8446bf03 ploc
open Lustre_types
13 22fe1c93 ploc
open Format
14
open Utils
15
16 7075d9fc ploc
let kind2_language_cst =
17
  [ "initial" ]
18
  
19
let kind2_protect id =
20
  if List.mem id kind2_language_cst then
21
    "_KIND2_PROTECT_" ^ id
22
  else
23
    id
24
  
25
   
26 22fe1c93 ploc
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
27
   following the C convention for multiple lines macro *)
28
let pp_as_c_macro pp_fun fmt v =
29 04a63d25 xthirioux
  let formatter_out_funs = pp_get_formatter_out_functions fmt () in
30
  let macro_newline () =
31
    begin
32
      formatter_out_funs.out_string "\\" 0 1;
33
      formatter_out_funs.out_newline ()
34
    end in
35 22fe1c93 ploc
  begin
36 04a63d25 xthirioux
    pp_set_formatter_out_functions fmt { formatter_out_funs with out_newline = macro_newline };
37 22fe1c93 ploc
    pp_fun fmt v;
38 04a63d25 xthirioux
    pp_set_formatter_out_functions fmt formatter_out_funs;
39 22fe1c93 ploc
  end
40
41 74ca6b61 ploc
let rec pp_var_struct_type_field fmt (label, tdesc) =
42
  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
43
and pp_var_type_dec_desc fmt tdesc =
44
  match tdesc with 
45
  | Tydec_any -> fprintf fmt "<any>"
46 ec433d69 xthirioux
  | Tydec_int -> fprintf fmt "int"
47 04a63d25 xthirioux
  | Tydec_real -> fprintf fmt "real"
48 74ca6b61 ploc
  (* | Tydec_float -> fprintf fmt "float" *)
49 ec433d69 xthirioux
  | Tydec_bool -> fprintf fmt "bool"
50 74ca6b61 ploc
  | Tydec_clock t -> fprintf fmt "%a clock" pp_var_type_dec_desc t
51
  | Tydec_const t -> fprintf fmt "%s" t
52
  | Tydec_enum id_list -> fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
53
  | Tydec_struct f_list -> fprintf fmt "struct {%a }" (fprintf_list ~sep:" " pp_var_struct_type_field) f_list
54
  | Tydec_array (s, t) -> fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
55
56
let pp_var_type_dec fmt ty =
57
  pp_var_type_dec_desc fmt ty.ty_dec_desc
58 22fe1c93 ploc
59 7075d9fc ploc
let pp_var_name fmt id =
60
  fprintf fmt "%s" (if !Options.kind2_print then kind2_protect id.var_id else id.var_id) 
61
62 74ca6b61 ploc
let pp_var_type fmt id =
63
  if !Options.print_dec_types then
64
    pp_var_type_dec fmt id.var_dec_type
65
  else
66
    Types.print_node_ty fmt id.var_type
67
let pp_var_clock fmt id = Clocks.print_ck_suffix fmt id.var_clock
68 9f0f88dd ploc
  
69 22fe1c93 ploc
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
70
71 74ca6b61 ploc
let pp_var fmt id =
72
  fprintf fmt "%s%s: %a"
73
    (if id.var_dec_const then "const " else "")
74 7075d9fc ploc
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
75 74ca6b61 ploc
    pp_var_type id
76 af5af1e8 ploc
77 1fd3d002 ploc
let pp_vars fmt vars =
78
  fprintf_list ~sep:"; " pp_var fmt vars
79
  
80 af5af1e8 ploc
let pp_quantifiers fmt (q, vars) =
81
  match q with
82 1fd3d002 ploc
    | Forall -> fprintf fmt "forall %a" pp_vars vars 
83
    | Exists -> fprintf fmt "exists %a" pp_vars vars 
84 af5af1e8 ploc
85 12af4908 xthirioux
let rec pp_struct_const_field fmt (label, c) =
86
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
87
and pp_const fmt c = 
88 22fe1c93 ploc
  match c with
89
    | Const_int i -> pp_print_int fmt i
90 7075d9fc ploc
    | Const_real r -> Real.pp fmt r
91 096f48d5 ploc
    (*if e = 0 then pp_print_int fmt c else if e < 0 then Format.fprintf fmt "%ie%i" c (-e) else Format.fprintf fmt "%ie-%i" c e *)
92 04a63d25 xthirioux
    (* | Const_float r -> pp_print_float fmt r *)
93 22fe1c93 ploc
    | Const_tag  t -> pp_print_string fmt t
94 34d3f022 ploc
    | Const_array ca -> fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
95
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
96
97
    (* used only for annotations *)
98 01c7d5e1 ploc
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
99 34d3f022 ploc
    | Const_modeid s -> pp_print_string fmt ("\"" ^ s ^ "\"")
100 22fe1c93 ploc
101
102 66359a5e ploc
let pp_annot_key fmt kwds =
103
  match kwds with
104
  | [] -> assert false
105 34d3f022 ploc
  | [x] -> pp_print_string fmt x
106
  | _ -> fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds
107 66359a5e ploc
108 0323b9e6 ploc
let pp_kind2_when fmt (id, l) =
109
  if l = "true" then 
110
    fprintf fmt "%s" id
111
  else if l = "false" then
112
    fprintf fmt "not(%s)" id
113
  else
114
    fprintf fmt "(%s=%s)" l id
115
       
116
  
117 af5af1e8 ploc
let rec pp_expr fmt expr =
118
  (match expr.expr_annot with 
119 0323b9e6 ploc
   | None -> fprintf fmt "%t" 
120
   | Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
121 4e9ba094 ploc
    (fun fmt ->
122
      let pp fmt = 
123 af5af1e8 ploc
      match expr.expr_desc with
124 0323b9e6 ploc
      | Expr_const c -> pp_const fmt c
125 7075d9fc ploc
      | Expr_ident id ->
126
         fprintf fmt "%s"
127
           (if !Options.kind2_print then kind2_protect id else id)
128
129 0323b9e6 ploc
      | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
130
      | Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
131
      | Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
132
      | Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
133
      | Expr_ite (c, t, e) -> fprintf fmt "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])" pp_expr c pp_expr t pp_expr e
134
      | Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
135
      | Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
136
      | Expr_pre e -> fprintf fmt "pre %a" pp_expr e
137
      | Expr_when (e, id, l) ->
138
         if !Options.kind2_print then
139
           fprintf fmt "%a when %a" pp_expr e pp_kind2_when (l, id)
140 ff61a638 ploc
         else
141 0323b9e6 ploc
           fprintf fmt "%a when %s(%s)" pp_expr e l id
142
      | Expr_merge (id, hl) -> 
143
         fprintf fmt "merge %s %a" id pp_handlers hl
144
      | Expr_appl (id, e, r) -> pp_app fmt id e r
145 4e9ba094 ploc
      in
146
      if false (* extra debug *)
147
      then
148
        Format.fprintf fmt "%t: %a" pp Types.print_ty expr.expr_type 
149
      else
150
        pp fmt
151 af5af1e8 ploc
    )
152 22fe1c93 ploc
and pp_tuple fmt el =
153 0323b9e6 ploc
  fprintf_list ~sep:"," pp_expr fmt el
154 22fe1c93 ploc
155
and pp_handler fmt (t, h) =
156 0323b9e6 ploc
  fprintf fmt "(%s -> %a)" t pp_expr h
157 22fe1c93 ploc
158
and pp_handlers fmt hl =
159 0323b9e6 ploc
  fprintf_list ~sep:" " pp_handler fmt hl
160 22fe1c93 ploc
161
and pp_app fmt id e r =
162 0323b9e6 ploc
  if !Options.kind2_print &&
163
       not (List.mem id Basic_library.internal_funs) then
164
    (* We only translate calls to nodes in kind2. The other may be
165 1d3f2f66 ploc
          rejected by Kind2 *)
166 0323b9e6 ploc
    ( (* Small local function to extract the first layer of when constructs *)
167
      let rec un_when_ed_expr e =
168
        match e.expr_desc with
169
          Expr_when (e,i,l) -> (Some (i,l)), e
170
        | Expr_tuple el -> (
171
          let un_when_ed_el = List.map un_when_ed_expr el in
172
          if List.length un_when_ed_el < 1 then
173
            assert false; (* tuple should have at least one element*)
174
          let init_when =
175
            fst (List.hd un_when_ed_el)
176
          in
177
          let common_when =
178
            List.fold_left (fun accu (new_opt,_) ->
179
                match accu, new_opt with
180
                | Some c1, Some c2 ->
181
                   if c1 = c2 then
182
                     Some c1
183
                   else
184
                     assert false  (* should not be clocked *)
185
                | None, None -> None
186
                | _ -> assert false (* If this is not even, there
187
                                       should be a clocking problem*)
188
              ) init_when (List.tl un_when_ed_el)
189
          in
190
          match common_when with
191
          | None -> None, e
192
          | Some _ -> common_when, { e with expr_desc =
193
                                              Expr_tuple (List.map snd un_when_ed_el) } 
194
        )
195
        | _ -> None, e
196
      in
197
      let when_expr, unwhen_ed_e = un_when_ed_expr e in
198
      match r, when_expr with
199
      | None, None -> pp_call fmt id e
200
      | None, Some w ->
201
         fprintf fmt "(activate %s every (%a)) (%a)"
202
           id
203
           pp_kind2_when w
204
           pp_expr e
205
      | Some r, None ->
206
         fprintf fmt "(restart %s every (%a)) (%a)"
207
           id
208
           pp_expr r
209
           pp_expr e
210
      | Some r, Some w ->
211
         fprintf fmt "(activate %s every (%a) restart every (%a)) (%a)"
212
           id
213
           pp_kind2_when w
214
           pp_expr r
215
           pp_expr e
216
    )
217 70df2f87 xthirioux
218 0323b9e6 ploc
  else (
219
    match r with
220
    | None -> pp_call fmt id e
221
    | Some c ->
222
       fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 
223
  )
224
  
225 70df2f87 xthirioux
and pp_call fmt id e =
226
  match id, e.expr_desc with
227
  | "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
228
  | "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
229
  | "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
230
  | "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
231
  | "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
232
  | "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
233
  | "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
234
  | "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
235
  | "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
236
  | "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
237
  | "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
238
  | "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
239
  | ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
240
  | ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
241 2ae3ef3f ploc
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
242 70df2f87 xthirioux
  | "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
243
  | "not", _ -> fprintf fmt "(not %a)" pp_expr e
244
  | _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
245
  | _ -> fprintf fmt "%s (%a)" id pp_expr e
246 af5af1e8 ploc
247
and pp_eexpr fmt e =
248
  fprintf fmt "%a%t %a"
249
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
250
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
251
    pp_expr e.eexpr_qfexpr
252
253 1b57e111 Teme
and  pp_sf_value fmt e =
254 0323b9e6 ploc
  fprintf fmt "%a"
255
    (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
256
    (* (fun fmt -> match e.eexpr_quantifiers *)
257
    (*             with [] -> () *)
258
    (*                | _ -> fprintf fmt ";") *)
259
    pp_expr e.eexpr_qfexpr
260 1b57e111 Teme
261
and pp_s_function fmt expr_ann =
262
  let pp_annot fmt (kwds, ee) =
263 34d3f022 ploc
    fprintf fmt " %t : %a"
264 0323b9e6 ploc
      (fun fmt -> match kwds with
265
                  | [] -> assert false
266
                  | [x] -> pp_print_string fmt x
267
                  | _ -> fprintf fmt "%a" (fprintf_list ~sep:"/" pp_print_string) kwds)
268
      pp_sf_value ee
269 1b57e111 Teme
  in
270
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
271 af5af1e8 ploc
272
and pp_expr_annot fmt expr_ann =
273
  let pp_annot fmt (kwds, ee) =
274 fbcd3ad1 ploc
    fprintf fmt "(*!%a: %a; *)"
275 66359a5e ploc
      pp_annot_key kwds
276 af5af1e8 ploc
      pp_eexpr ee
277
  in
278
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
279 4e9ba094 ploc
 
280 27e5a70d ploc
281
let pp_asserts fmt asserts =
282
  match asserts with 
283
  | _::_ -> (
284
    fprintf fmt "(* Asserts definitions *)@ ";
285
    fprintf_list ~sep:"@ " (fun fmt assert_ -> 
286
      let expr = assert_.assert_expr in
287
      fprintf fmt "assert %a;" pp_expr expr 
288
    ) fmt asserts 
289
  )
290
  | _ -> ()
291
292 ec433d69 xthirioux
(*
293
let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock
294
*)
295
let pp_node_var fmt id =
296
  begin
297 74ca6b61 ploc
    fprintf fmt "%s%s: %a%a"
298
      (if id.var_dec_const then "const " else "")
299 7075d9fc ploc
      (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
300 74ca6b61 ploc
      pp_var_type id
301
      pp_var_clock id;
302 ec433d69 xthirioux
    match id.var_dec_value with
303
    | None -> () 
304
    | Some v -> fprintf fmt " = %a" pp_expr v
305
  end 
306
307 27e5a70d ploc
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var 
308 ec433d69 xthirioux
309 22fe1c93 ploc
let pp_node_eq fmt eq = 
310
  fprintf fmt "%a = %a;" 
311
    pp_eq_lhs eq.eq_lhs
312
    pp_expr eq.eq_rhs
313
314 b08ffca7 xthirioux
let pp_restart fmt restart =
315 34d3f022 ploc
  fprintf fmt "%s" (if restart then "restart" else "resume")
316 b08ffca7 xthirioux
317
let pp_unless fmt (_, expr, restart, st) =
318 34d3f022 ploc
  fprintf fmt "unless %a %a %s"
319 b08ffca7 xthirioux
    pp_expr expr
320
    pp_restart restart
321
    st
322
323
let pp_until fmt (_, expr, restart, st) =
324 34d3f022 ploc
  fprintf fmt "until %a %a %s"
325 b08ffca7 xthirioux
    pp_expr expr
326
    pp_restart restart
327
    st
328
329
let rec pp_handler fmt handler =
330 34d3f022 ploc
  fprintf fmt "state %s:@ @[<v 2>  %a%t%alet@,@[<v 2>  %a@ %a@ %a@]@,tel@ %a@]"
331 b08ffca7 xthirioux
    handler.hand_state
332 27e5a70d ploc
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
333
    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
334 b08ffca7 xthirioux
    (fun fmt locals ->
335
      match locals with [] -> () | _ ->
336 34d3f022 ploc
	fprintf fmt "@[<v 4>var %a@]@ " 
337 b08ffca7 xthirioux
	  (Utils.fprintf_list ~sep:"@ " 
338 34d3f022 ploc
	     (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
339 b08ffca7 xthirioux
	  locals)
340
    handler.hand_locals
341 27e5a70d ploc
    (fprintf_list ~sep:"@ " pp_expr_annot) handler.hand_annots
342 b08ffca7 xthirioux
    pp_node_stmts handler.hand_stmts
343 27e5a70d ploc
    pp_asserts handler.hand_asserts
344 54d032f5 xthirioux
    (Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
345 b08ffca7 xthirioux
346
and pp_node_stmt fmt stmt =
347
  match stmt with
348
  | Eq eq -> pp_node_eq fmt eq
349
  | Aut aut -> pp_node_aut fmt aut
350
351
and pp_node_stmts fmt stmts = fprintf_list ~sep:"@ " pp_node_stmt fmt stmts
352
353
and pp_node_aut fmt aut =
354 34d3f022 ploc
  fprintf fmt "@[<v 0>automaton %s@,%a@]"
355 b08ffca7 xthirioux
    aut.aut_id
356
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
357
358
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
359 22fe1c93 ploc
360 ef34b4ae xthirioux
let pp_typedef fmt ty =
361 94cf0fc5 ploc
  fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
362 ef34b4ae xthirioux
363
let pp_typedec fmt ty =
364 94cf0fc5 ploc
  fprintf fmt "type %s;" ty.tydec_id
365 22fe1c93 ploc
366
(* let rec pp_var_type fmt ty =  *)
367
(*   fprintf fmt "%a" (match ty.tdesc with  *)
368
(*     | Tvar | Tarrow | Tlink | Tunivar -> assert false *)
369
(*     | Tint -> pp_print_string fmt "int" *)
370
(*     | Treal -> pp_print_string fmt "real" *)
371
(*     | Tbool -> pp_print_string fmt "bool" *)
372
(*     | Trat -> pp_print_string fmt "rat" *)
373
(*     | Tclock -> pp_print_string fmt "clock"  *)
374
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
375
(*   ) *)
376
377 e2380d4d ploc
378 949b2e1e ploc
379 1fd3d002 ploc
(* let pp_quantifiers fmt (q, vars) =
380
 *   match q with
381
 *     | Forall -> fprintf fmt "forall %a" pp_vars vars 
382
 *     | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars  *)
383 949b2e1e ploc
384 1fd3d002 ploc
(*let pp_eexpr fmt e =
385 949b2e1e ploc
  fprintf fmt "%a%t %a"
386
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
387
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
388
    pp_expr e.eexpr_qfexpr
389 1fd3d002 ploc
 *)
390 217837e2 ploc
    
391
let pp_spec_eq fmt eq = 
392
  fprintf fmt "var %a : %a = %a;" 
393
    pp_eq_lhs eq.eq_lhs
394
    Types.print_node_ty eq.eq_rhs.expr_type
395
    pp_expr eq.eq_rhs
396
  
397
let pp_spec_stmt fmt stmt =
398
  match stmt with
399
  | Eq eq -> pp_spec_eq fmt eq
400
  | Aut aut -> assert false (* Not supported yet *)
401
             
402
  
403 e2380d4d ploc
let pp_spec fmt spec =
404 778c80fd ploc
  (* const are prefixed with const in pp_var and with nothing for regular
405
     variables. We adapt the call to produce the appropriate output. *)
406 217837e2 ploc
    fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->
407 1fd3d002 ploc
    fprintf fmt "%a = %t;"
408 778c80fd ploc
      pp_var v
409 217837e2 ploc
      (fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)
410
    ) fmt spec.consts;
411
  
412
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
413
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
414 67ef9395 ploc
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r) fmt spec.guarantees;
415 217837e2 ploc
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
416 1fd3d002 ploc
    fprintf fmt "mode %s (@[<v 0>%a@ %a@]);" 
417 778c80fd ploc
      mode.mode_id
418 1fd3d002 ploc
      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
419
      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
420 778c80fd ploc
  ) fmt spec.modes;
421 217837e2 ploc
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
422 778c80fd ploc
    fprintf fmt "import %s (%a) returns (%a);" 
423
      import.import_nodeid
424 f4cba4b8 ploc
      pp_expr import.inputs
425
      pp_expr import.outputs
426 217837e2 ploc
  ) fmt spec.imports
427 e2380d4d ploc
428 1fd3d002 ploc
(* Project the contract node as a pure contract: local memories are pushed back in the contract definition. Should mainly be used to print it *) 
429
let node_as_contract nd =
430 f4cba4b8 ploc
  match nd.node_spec with
431
  | None | Some (NodeSpec _) -> raise (Invalid_argument "Not a contract")
432
  | Some (Contract c) -> (
433 1fd3d002 ploc
    (* While a processed contract shall have no locals, sttms nor
434
       consts, an unprocessed one could. So we conservatively merge
435
       elements, to enable printing unprocessed contracts *)
436
    let consts, locals = List.partition(fun v -> v.var_dec_const) nd.node_locals in
437 f4cba4b8 ploc
    { c with
438 1fd3d002 ploc
      consts = consts @ c.consts;
439
      locals = locals @ c.locals;
440
      stmts = nd.node_stmts @ c.stmts;
441 f4cba4b8 ploc
    }
442
  )
443 c6c8786b ploc
444
(* Printing top contract as comments in regular output and as contract
445
   in kind2 *)
446 f4cba4b8 ploc
let pp_contract fmt nd =    
447 c6c8786b ploc
   let c = node_as_contract nd in
448
  fprintf fmt "@[<v 2>%scontract %s(%a) returns (%a);@ "
449
    (if !Options.kind2_print then "" else "(*@")
450 f4cba4b8 ploc
    nd.node_id
451 1fd3d002 ploc
    pp_node_args nd.node_inputs
452
    pp_node_args nd.node_outputs;
453
  fprintf fmt "@[<v 2>let@ ";
454 f4cba4b8 ploc
  pp_spec fmt c;
455 c6c8786b ploc
  fprintf fmt "@]@ tel@ @]%s@ "
456
  (if !Options.kind2_print then "" else "*)")
457 af5af1e8 ploc
    
458 f4cba4b8 ploc
let pp_spec_as_comment fmt (inl, outl, spec) =
459
  match spec with
460
  | Contract c -> (* should have been processed by now *)
461 5b4c0069 ploc
     fprintf fmt "@[<hov 2>(*@contract@ ";
462 f4cba4b8 ploc
     pp_spec fmt c;
463
     fprintf fmt "@]*)@ "
464
     
465
  | NodeSpec name -> (* Pushing stmts in contract. We update the
466
                      original information with the computed one in
467
                      nd. *)
468
     let pp_l = fprintf_list ~sep:"," pp_var_name in
469 5b4c0069 ploc
     fprintf fmt "@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ "
470 f4cba4b8 ploc
       name
471
       pp_l inl
472
       pp_l outl
473
     
474 2120af73 ploc
let pp_node_vs_function fmt nd =
475
  fprintf fmt "%s" (if nd.node_dec_stateless then "function" else "node")
476
  
477 bc3139b0 ploc
let pp_node fmt nd =
478
  fprintf fmt "@[<v 0>";
479
  (* Prototype *)
480 2120af73 ploc
  fprintf fmt  "%a @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
481
    pp_node_vs_function nd
482 bc3139b0 ploc
    nd.node_id
483
    pp_node_args nd.node_inputs
484
    pp_node_args nd.node_outputs;
485
  (* Contracts *)
486 1fd3d002 ploc
  fprintf fmt "%a"
487 f4cba4b8 ploc
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s) | _ -> ()) nd.node_spec
488 1fd3d002 ploc
    (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ") *);
489 bc3139b0 ploc
  (* Locals *)
490
  fprintf fmt "%a" (fun fmt locals ->
491
      match locals with [] -> () | _ ->
492
                                    fprintf fmt "@[<v 4>var %a@]@ " 
493
                                      (fprintf_list ~sep:"@ " 
494
	                                 (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
495
                                      locals
496
    ) nd.node_locals;
497
  (* Checks *)
498
  fprintf fmt "%a"
499
    (fun fmt checks ->
500
      match checks with [] -> () | _ ->
501
                                    fprintf fmt "@[<v 4>check@ %a@]@ " 
502
                                      (fprintf_list ~sep:"@ " 
503
	                                 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
504
                                      checks
505
    ) nd.node_checks;
506
  (* Body *)
507
  fprintf fmt "let@[<h 2>   @ @[<v>";
508
  (* Annotations *)
509
  fprintf fmt "%a@ " (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
510
  (* Statements *)
511
  fprintf fmt "%a@ " pp_node_stmts nd.node_stmts;
512
  (* Asserts *)    
513
  fprintf fmt "%a" pp_asserts nd.node_asserts;
514
  (* closing boxes body (2)  and node (1) *) 
515
  fprintf fmt "@]@]@ tel@]@ "
516
517
518 22fe1c93 ploc
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
519
520 f4cba4b8 ploc
let pp_node fmt nd =
521
  match nd.node_spec, nd.node_iscontract with
522
  | None, false
523
    | Some (NodeSpec _), false 
524
    -> pp_node fmt nd
525
  | Some (Contract _), false -> pp_node fmt nd (* may happen early in the compil process *)
526
  | Some (Contract _), true -> pp_contract fmt nd 
527
  | _ -> assert false
528
     
529 22fe1c93 ploc
let pp_imported_node fmt ind = 
530 217837e2 ploc
  fprintf fmt "@[<v 0>";
531
  (* Prototype *)
532
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
533 52cfee34 xthirioux
    (if ind.nodei_stateless then "function" else "node")
534 22fe1c93 ploc
    ind.nodei_id
535
    pp_node_args ind.nodei_inputs
536 217837e2 ploc
    pp_node_args ind.nodei_outputs;
537
  (* Contracts *)
538
  fprintf fmt "%a%t"
539 f4cba4b8 ploc
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s) | _ -> ()) ind.nodei_spec
540 217837e2 ploc
    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
541
  fprintf fmt "@]@ "
542
  
543 22fe1c93 ploc
544 ef34b4ae xthirioux
let pp_const_decl fmt cdecl =
545
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
546
547
let pp_const_decl_list fmt clist = 
548
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
549 54ae8ac7 ploc
550 34d3f022 ploc
551
  
552 22fe1c93 ploc
let pp_decl fmt decl =
553
  match decl.top_decl_desc with
554 94cf0fc5 ploc
  | Node nd -> fprintf fmt "%a" pp_node nd
555 67ef9395 ploc
  | ImportedNode ind -> (* We do not print imported nodes *)
556
     fprintf fmt "(* imported %a; *)" pp_imported_node ind
557 94cf0fc5 ploc
  | Const c -> fprintf fmt "const %a" pp_const_decl c
558
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"" s else fprintf fmt "#open <%s>" s
559 19a1e66b ploc
  | Include s -> fprintf fmt "include \"%s\"" s
560 94cf0fc5 ploc
  | TypeDef tdef -> fprintf fmt "%a" pp_typedef tdef
561 34d3f022 ploc
  
562 2120af73 ploc
let pp_prog pp_decl fmt prog =
563 333e3a25 ploc
  (* we first print types: the function SortProg.sort could do the job but ut
564
     introduces a cyclic dependance *)
565 a879351b ploc
566
  let open_decl, prog =
567
    List.partition (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false) prog
568
  in
569
  let type_decl, prog =
570 753d4562 ploc
    List.partition (fun decl -> match decl.top_decl_desc with TypeDef _ -> true | _ -> false) prog
571
  in
572 a879351b ploc
  fprintf fmt "@[<v 0>%a@]" (fprintf_list ~sep:"@ " pp_decl) (open_decl@type_decl@prog)
573 22fe1c93 ploc
574 34d3f022 ploc
(* Gives a short overview of model content. Do not print all node content *)
575 22fe1c93 ploc
let pp_short_decl fmt decl =
576
  match decl.top_decl_desc with
577 2120af73 ploc
  | Node nd -> fprintf fmt "%a %s@ "
578
                 pp_node_vs_function nd
579
                 nd.node_id
580 22fe1c93 ploc
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
581 ef34b4ae xthirioux
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
582 19a1e66b ploc
  | Include s -> fprintf fmt "include \"%s\"" s
583 ef34b4ae xthirioux
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
584
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
585 2120af73 ploc
586
let pp_prog_short = pp_prog pp_short_decl
587
let pp_prog = pp_prog pp_decl
588
            
589 5c1184ad ploc
let pp_lusi fmt decl = 
590
  match decl.top_decl_desc with
591 ef34b4ae xthirioux
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
592
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
593 19a1e66b ploc
  | Include s -> fprintf fmt "include \"%s\"" s
594 ef34b4ae xthirioux
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
595
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
596
  | Node _ -> assert false
597 34d3f022 ploc
                
598 ef34b4ae xthirioux
let pp_lusi_header fmt basename prog =
599 521e2a6b ploc
  fprintf fmt "@[<v 0>";
600
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
601
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));
602
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";
603
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
604 c4fb63af ploc
  fprintf fmt "@]@."
605 d7b73fed xthirioux
606
let pp_offset fmt offset =
607
  match offset with
608
  | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
609
  | Field f -> fprintf fmt ".%s" f
610
611 a0c92fa8 ploc
let pp_node_list fmt prog =
612
  Format.fprintf fmt "@[<h 2>%a@]"
613
    (fprintf_list
614
       ~sep:"@ "
615
       (fun fmt decl ->
616
         match decl.top_decl_desc with
617
         | Node nd -> Format.fprintf fmt "%s" nd.node_id
618
         | _ -> ()
619
    ))
620
    prog
621
    
622 22fe1c93 ploc
(* Local Variables: *)
623
(* compile-command:"make -C .." *)
624
(* End: *)