Project

General

Profile

« Previous | Next » 

Revision ca7ff3f7

Added by LĂ©lio Brun 8 months ago

reformatting

View differences:

src/printers.ml
13 13
open Utils
14 14
open Format
15 15

  
16
let kind2_language_cst =
17
  [ "initial" ]
18
  
16
let kind2_language_cst = [ "initial" ]
17

  
19 18
let kind2_protect id =
20
  if List.mem id kind2_language_cst then
21
    "_KIND2_PROTECT_" ^ id
22
  else
23
    id
24
  
25
   
19
  if List.mem id kind2_language_cst then "_KIND2_PROTECT_" ^ id else id
20

  
26 21
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
27 22
   following the C convention for multiple lines macro *)
28 23
let pp_as_c_macro pp_fun fmt v =
29 24
  let formatter_out_funs = pp_get_formatter_out_functions fmt () in
30 25
  let macro_newline () =
31
    begin
32
      formatter_out_funs.out_string "\\" 0 1;
33
      formatter_out_funs.out_newline ()
34
    end in
35
  begin
36
    pp_set_formatter_out_functions fmt { formatter_out_funs with out_newline = macro_newline };
37
    pp_fun fmt v;
38
    pp_set_formatter_out_functions fmt formatter_out_funs;
39
  end
26
    formatter_out_funs.out_string "\\" 0 1;
27
    formatter_out_funs.out_newline ()
28
  in
29
  pp_set_formatter_out_functions fmt
30
    { formatter_out_funs with out_newline = macro_newline };
31
  pp_fun fmt v;
32
  pp_set_formatter_out_functions fmt formatter_out_funs
40 33

  
41 34
let rec pp_var_struct_type_field fmt (label, tdesc) =
42 35
  fprintf fmt "%a : %a;" pp_print_string label pp_var_type_dec_desc tdesc
36

  
43 37
and pp_var_type_dec_desc fmt tdesc =
44
  match tdesc with 
45
  | Tydec_any -> fprintf fmt "<any>"
46
  | Tydec_int -> fprintf fmt "int"
47
  | Tydec_real -> fprintf fmt "real"
38
  match tdesc with
39
  | Tydec_any ->
40
    fprintf fmt "<any>"
41
  | Tydec_int ->
42
    fprintf fmt "int"
43
  | Tydec_real ->
44
    fprintf fmt "real"
48 45
  (* | Tydec_float -> fprintf fmt "float" *)
49
  | Tydec_bool -> fprintf fmt "bool"
50
  | 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
46
  | Tydec_bool ->
47
    fprintf fmt "bool"
48
  | Tydec_clock t ->
49
    fprintf fmt "%a clock" pp_var_type_dec_desc t
50
  | Tydec_const t ->
51
    fprintf fmt "%s" t
52
  | Tydec_enum id_list ->
53
    fprintf fmt "enum {%a }" (fprintf_list ~sep:", " pp_print_string) id_list
54
  | Tydec_struct f_list ->
55
    fprintf fmt "struct {%a }"
56
      (fprintf_list ~sep:" " pp_var_struct_type_field)
57
      f_list
58
  | Tydec_array (s, t) ->
59
    fprintf fmt "%a^%a" pp_var_type_dec_desc t Dimension.pp_dimension s
60

  
61
let pp_var_type_dec fmt ty = pp_var_type_dec_desc fmt ty.ty_dec_desc
58 62

  
59 63
let pp_var_name fmt id =
60
  fprintf fmt "%s" (if !Options.kind2_print then kind2_protect id.var_id else id.var_id) 
64
  fprintf fmt "%s"
65
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
61 66

  
62 67
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
68
  if !Options.print_dec_types then pp_var_type_dec fmt id.var_dec_type
69
  else Types.print_node_ty fmt id.var_type
70

  
67 71
let pp_var_clock fmt id = Clocks.print_ck_suffix fmt id.var_clock
68
  
72

  
69 73
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
70 74

  
71 75
let pp_var fmt id =
......
74 78
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
75 79
    pp_var_type id
76 80

  
77
let pp_vars fmt vars =
78
  fprintf_list ~sep:"; " pp_var fmt vars
79
  
81
let pp_vars fmt vars = fprintf_list ~sep:"; " pp_var fmt vars
82

  
80 83
let pp_quantifiers fmt (q, vars) =
81 84
  match q with
82
    | Forall -> fprintf fmt "forall %a" pp_vars vars 
83
    | Exists -> fprintf fmt "exists %a" pp_vars vars 
85
  | Forall ->
86
    fprintf fmt "forall %a" pp_vars vars
87
  | Exists ->
88
    fprintf fmt "exists %a" pp_vars vars
84 89

  
85 90
let rec pp_struct_const_field fmt (label, c) =
86 91
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
87
and pp_const fmt c = 
88
  match c with
89
    | Const_int i -> pp_print_int fmt i
90
    | Const_real r -> Real.pp fmt r
91
    (*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
    (* | Const_float r -> pp_print_float fmt r *)
93
    | Const_tag  t -> pp_print_string fmt t
94
    | 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
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
99
    | Const_modeid s -> pp_print_string fmt ("\"" ^ s ^ "\"")
100 92

  
93
and pp_const fmt c =
94
  match c with
95
  | Const_int i ->
96
    pp_print_int fmt i
97
  | Const_real r ->
98
    Real.pp fmt r
99
  (*if e = 0 then pp_print_int fmt c else if e < 0 then Format.fprintf fmt
100
    "%ie%i" c (-e) else Format.fprintf fmt "%ie-%i" c e *)
101
  (* | Const_float r -> pp_print_float fmt r *)
102
  | Const_tag t ->
103
    pp_print_string fmt t
104
  | Const_array ca ->
105
    fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
106
  | Const_struct fl ->
107
    fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
108
  (* used only for annotations *)
109
  | Const_string s ->
110
    pp_print_string fmt ("\"" ^ s ^ "\"")
111
  | Const_modeid s ->
112
    pp_print_string fmt ("\"" ^ s ^ "\"")
101 113

  
102 114
let pp_annot_key fmt kwds =
103 115
  match kwds with
104
  | [] -> assert false
105
  | [x] -> pp_print_string fmt x
106
  | _ -> fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds
116
  | [] ->
117
    assert false
118
  | [ x ] ->
119
    pp_print_string fmt x
120
  | _ ->
121
    fprintf fmt "/%a/" (fprintf_list ~sep:"/" pp_print_string) kwds
107 122

  
108 123
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
  
124
  if l = "true" then fprintf fmt "%s" id
125
  else if l = "false" then fprintf fmt "not(%s)" id
126
  else fprintf fmt "(%s=%s)" l id
127

  
117 128
let rec pp_expr fmt expr =
118
  (match expr.expr_annot with 
119
   | None -> fprintf fmt "%t" 
120
   | Some ann -> fprintf fmt "@[(%a %t)@]" pp_expr_annot ann)
121
    (fun fmt ->
122
      let pp fmt = 
123
      match expr.expr_desc with
124
      | Expr_const c -> pp_const fmt c
125
      | Expr_ident id ->
126
         fprintf fmt "%s"
127
           (if !Options.kind2_print then kind2_protect id else id)
128

  
129
      | 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
         else
141
           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
129
  (match expr.expr_annot with
130
  | None ->
131
    fprintf fmt "%t"
132
  | Some ann ->
133
    fprintf fmt "@[(%a %t)@]" pp_expr_annot ann) (fun fmt ->
134
      let pp fmt =
135
        match expr.expr_desc with
136
        | Expr_const c ->
137
          pp_const fmt c
138
        | Expr_ident id ->
139
          fprintf fmt "%s"
140
            (if !Options.kind2_print then kind2_protect id else id)
141
        | Expr_array a ->
142
          fprintf fmt "[%a]" pp_tuple a
143
        | Expr_access (a, d) ->
144
          fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
145
        | Expr_power (a, d) ->
146
          fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
147
        | Expr_tuple el ->
148
          fprintf fmt "(%a)" pp_tuple el
149
        | Expr_ite (c, t, e) ->
150
          fprintf fmt
151
            "@[<hov 1>(if %a then@ @[<hov 2>%a@]@ else@ @[<hov 2>%a@]@])"
152
            pp_expr c pp_expr t pp_expr e
153
        | Expr_arrow (e1, e2) ->
154
          fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
155
        | Expr_fby (e1, e2) ->
156
          fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
157
        | Expr_pre e ->
158
          fprintf fmt "pre %a" pp_expr e
159
        | Expr_when (e, id, l) ->
160
          if !Options.kind2_print then
161
            fprintf fmt "%a when %a" pp_expr e pp_kind2_when (l, id)
162
          else fprintf fmt "%a when %s(%s)" pp_expr e l id
163
        | Expr_merge (id, hl) ->
164
          fprintf fmt "merge %s %a" id pp_handlers hl
165
        | Expr_appl (id, e, r) ->
166
          pp_app fmt id e r
145 167
      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
    )
152
and pp_tuple fmt el =
153
  fprintf_list ~sep:"," pp_expr fmt el
168
      if false (* extra debug *) then
169
        Format.fprintf fmt "%t: %a" pp Types.print_ty expr.expr_type
170
      else pp fmt)
154 171

  
155
and pp_handler fmt (t, h) =
156
  fprintf fmt "(%s -> %a)" t pp_expr h
172
and pp_tuple fmt el = fprintf_list ~sep:"," pp_expr fmt el
157 173

  
158
and pp_handlers fmt hl =
159
  fprintf_list ~sep:" " pp_handler fmt hl
174
and pp_handler fmt (t, h) = fprintf fmt "(%s -> %a)" t pp_expr h
175

  
176
and pp_handlers fmt hl = fprintf_list ~sep:" " pp_handler fmt hl
160 177

  
161 178
and pp_app fmt id e r =
162
  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
          rejected by Kind2 *)
166
    ( (* 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, _ = 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

  
218
  else (
179
  if !Options.kind2_print && not (List.mem id Basic_library.internal_funs) then
180
    (* We only translate calls to nodes in kind2. The other may be rejected by
181
       Kind2 *)
182
    (* Small local function to extract the first layer of when constructs *)
183
    let rec un_when_ed_expr e =
184
      match e.expr_desc with
185
      | Expr_when (e, i, l) ->
186
        Some (i, l), e
187
      | Expr_tuple el -> (
188
        let un_when_ed_el = List.map un_when_ed_expr el in
189
        if List.length un_when_ed_el < 1 then assert false;
190
        (* tuple should have at least one element*)
191
        let init_when = fst (List.hd un_when_ed_el) in
192
        let common_when =
193
          List.fold_left
194
            (fun accu (new_opt, _) ->
195
              match accu, new_opt with
196
              | Some c1, Some c2 ->
197
                if c1 = c2 then Some c1
198
                else assert false (* should not be clocked *)
199
              | None, None ->
200
                None
201
              | _ ->
202
                assert false
203
              (* If this is not even, there should be a clocking problem*))
204
            init_when (List.tl un_when_ed_el)
205
        in
206
        match common_when with
207
        | None ->
208
          None, e
209
        | Some _ ->
210
          ( common_when,
211
            { e with expr_desc = Expr_tuple (List.map snd un_when_ed_el) } ))
212
      | _ ->
213
        None, e
214
    in
215
    let when_expr, _ = un_when_ed_expr e in
216
    match r, when_expr with
217
    | None, None ->
218
      pp_call fmt id e
219
    | None, Some w ->
220
      fprintf fmt "(activate %s every (%a)) (%a)" id pp_kind2_when w pp_expr e
221
    | Some r, None ->
222
      fprintf fmt "(restart %s every (%a)) (%a)" id pp_expr r pp_expr e
223
    | Some r, Some w ->
224
      fprintf fmt "(activate %s every (%a) restart every (%a)) (%a)" id
225
        pp_kind2_when w pp_expr r pp_expr e
226
  else
219 227
    match r with
220
    | None -> pp_call fmt id e
228
    | None ->
229
      pp_call fmt id e
221 230
    | Some c ->
222
       fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c 
223
  )
224
  
231
      fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
232

  
225 233
and pp_call fmt id e =
226 234
  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
  | "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
242
  | "=", 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
235
  | "+", Expr_tuple [ e1; e2 ] ->
236
    fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
237
  | "uminus", _ ->
238
    fprintf fmt "(- %a)" pp_expr e
239
  | "-", Expr_tuple [ e1; e2 ] ->
240
    fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
241
  | "*", Expr_tuple [ e1; e2 ] ->
242
    fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
243
  | "/", Expr_tuple [ e1; e2 ] ->
244
    fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
245
  | "mod", Expr_tuple [ e1; e2 ] ->
246
    fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
247
  | "&&", Expr_tuple [ e1; e2 ] ->
248
    fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
249
  | "||", Expr_tuple [ e1; e2 ] ->
250
    fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
251
  | "xor", Expr_tuple [ e1; e2 ] ->
252
    fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
253
  | "impl", Expr_tuple [ e1; e2 ] ->
254
    fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
255
  | "<", Expr_tuple [ e1; e2 ] ->
256
    fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
257
  | "<=", Expr_tuple [ e1; e2 ] ->
258
    fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
259
  | ">", Expr_tuple [ e1; e2 ] ->
260
    fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
261
  | ">=", Expr_tuple [ e1; e2 ] ->
262
    fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
263
  | "!=", Expr_tuple [ e1; e2 ] ->
264
    fprintf fmt "(%a <> %a)" pp_expr e1 pp_expr e2
265
  | "=", Expr_tuple [ e1; e2 ] ->
266
    fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
267
  | "not", _ ->
268
    fprintf fmt "(not %a)" pp_expr e
269
  | _, Expr_tuple _ ->
270
    fprintf fmt "%s %a" id pp_expr e
271
  | _ ->
272
    fprintf fmt "%s (%a)" id pp_expr e
246 273

  
247 274
and pp_eexpr fmt e =
248 275
  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 ";")
276
    (Utils.fprintf_list ~sep:"; " pp_quantifiers)
277
    e.eexpr_quantifiers
278
    (fun fmt ->
279
      match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
251 280
    pp_expr e.eexpr_qfexpr
252 281

  
253
and  pp_sf_value fmt e =
282
and pp_sf_value fmt e =
254 283
  fprintf fmt "%a"
255 284
    (* (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers *)
256 285
    (* (fun fmt -> match e.eexpr_quantifiers *)
......
261 290
and pp_s_function fmt expr_ann =
262 291
  let pp_annot fmt (kwds, ee) =
263 292
    fprintf fmt " %t : %a"
264
      (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)
293
      (fun fmt ->
294
        match kwds with
295
        | [] ->
296
          assert false
297
        | [ x ] ->
298
          pp_print_string fmt x
299
        | _ ->
300
          fprintf fmt "%a" (fprintf_list ~sep:"/" pp_print_string) kwds)
268 301
      pp_sf_value ee
269 302
  in
270 303
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
271 304

  
272 305
and pp_expr_annot fmt expr_ann =
273 306
  let pp_annot fmt (kwds, ee) =
274
    fprintf fmt "(*!%a: %a; *)"
275
      pp_annot_key kwds
276
      pp_eexpr ee
307
    fprintf fmt "(*!%a: %a; *)" pp_annot_key kwds pp_eexpr ee
277 308
  in
278 309
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
279
 
280 310

  
281 311
let pp_asserts fmt asserts =
282
  match asserts with 
283
  | _::_ -> (
312
  match asserts with
313
  | _ :: _ ->
284 314
    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
(*
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
*)
315
    fprintf_list ~sep:"@ "
316
      (fun fmt assert_ ->
317
        let expr = assert_.assert_expr in
318
        fprintf fmt "assert %a;" pp_expr expr)
319
      fmt asserts
320
  | _ ->
321
    ()
322

  
323
(* let pp_node_var fmt id = fprintf fmt "%s%s: %a(%a)%a" (if id.var_dec_const
324
   then "const " else "") id.var_id print_dec_ty id.var_dec_type.ty_dec_desc
325
   Types.print_ty id.var_type Clocks.print_ck_suffix id.var_clock *)
295 326
let pp_node_var fmt id =
296
  begin
297
    fprintf fmt "%s%s: %a%a"
298
      (if id.var_dec_const then "const " else "")
299
      (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
300
      pp_var_type id
301
      pp_var_clock id;
302
    match id.var_dec_value with
303
    | None -> () 
304
    | Some v -> fprintf fmt " = %a" pp_expr v
305
  end 
306

  
307
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var 
308

  
309
let pp_node_eq fmt eq = 
310
  fprintf fmt "%a = %a;" 
311
    pp_eq_lhs eq.eq_lhs
312
    pp_expr eq.eq_rhs
327
  fprintf fmt "%s%s: %a%a"
328
    (if id.var_dec_const then "const " else "")
329
    (if !Options.kind2_print then kind2_protect id.var_id else id.var_id)
330
    pp_var_type id pp_var_clock id;
331
  match id.var_dec_value with
332
  | None ->
333
    ()
334
  | Some v ->
335
    fprintf fmt " = %a" pp_expr v
336

  
337
let pp_node_args = fprintf_list ~sep:";@ " pp_node_var
338

  
339
let pp_node_eq fmt eq =
340
  fprintf fmt "%a = %a;" pp_eq_lhs eq.eq_lhs pp_expr eq.eq_rhs
313 341

  
314 342
let pp_restart fmt restart =
315 343
  fprintf fmt "%s" (if restart then "restart" else "resume")
316 344

  
317 345
let pp_unless fmt (_, expr, restart, st) =
318
  fprintf fmt "unless %a %a %s"
319
    pp_expr expr
320
    pp_restart restart
321
    st
346
  fprintf fmt "unless %a %a %s" pp_expr expr pp_restart restart st
322 347

  
323 348
let pp_until fmt (_, expr, restart, st) =
324
  fprintf fmt "until %a %a %s"
325
    pp_expr expr
326
    pp_restart restart
327
    st
349
  fprintf fmt "until %a %a %s" pp_expr expr pp_restart restart st
328 350

  
329 351
let rec pp_handler fmt handler =
330 352
  fprintf fmt "state %s:@ @[<v 2>  %a%t%alet@,@[<v 2>  %a@ %a@ %a@]@,tel@ %a@]"
331 353
    handler.hand_state
332
    (Utils.fprintf_list ~sep:"@ " pp_unless) handler.hand_unless
354
    (Utils.fprintf_list ~sep:"@ " pp_unless)
355
    handler.hand_unless
333 356
    (fun fmt -> if not ([] = handler.hand_unless) then fprintf fmt "@ ")
334 357
    (fun fmt locals ->
335
      match locals with [] -> () | _ ->
336
	fprintf fmt "@[<v 4>var %a@]@ " 
337
	  (Utils.fprintf_list ~sep:"@ " 
338
	     (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
339
	  locals)
358
      match locals with
359
      | [] ->
360
        ()
361
      | _ ->
362
        fprintf fmt "@[<v 4>var %a@]@ "
363
          (Utils.fprintf_list ~sep:"@ " (fun fmt v ->
364
               fprintf fmt "%a;" pp_node_var v))
365
          locals)
340 366
    handler.hand_locals
341
    (fprintf_list ~sep:"@ " pp_expr_annot) handler.hand_annots
342
    pp_node_stmts handler.hand_stmts
343
    pp_asserts handler.hand_asserts
344
    (Utils.fprintf_list ~sep:"@," pp_until) handler.hand_until
367
    (fprintf_list ~sep:"@ " pp_expr_annot)
368
    handler.hand_annots pp_node_stmts handler.hand_stmts pp_asserts
369
    handler.hand_asserts
370
    (Utils.fprintf_list ~sep:"@," pp_until)
371
    handler.hand_until
345 372

  
346 373
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
374
  match stmt with Eq eq -> pp_node_eq fmt eq | Aut aut -> pp_node_aut fmt aut
350 375

  
351 376
and pp_node_stmts fmt stmts =
352
  pp_print_list
353
    ~pp_open_box:pp_open_vbox0
354
    ~pp_sep:pp_print_cut
355
    pp_node_stmt fmt stmts
377
  pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cut pp_node_stmt fmt
378
    stmts
356 379

  
357 380
and pp_node_aut fmt aut =
358
  fprintf fmt "@[<v 0>automaton %s@,%a@]"
359
    aut.aut_id
360
    (Utils.fprintf_list ~sep:"@ " pp_handler) aut.aut_handlers
381
  fprintf fmt "@[<v 0>automaton %s@,%a@]" aut.aut_id
382
    (Utils.fprintf_list ~sep:"@ " pp_handler)
383
    aut.aut_handlers
361 384

  
362 385
and pp_node_eqs fmt eqs = fprintf_list ~sep:"@ " pp_node_eq fmt eqs
363 386

  
364 387
let pp_typedef fmt ty =
365 388
  fprintf fmt "type %s = %a;" ty.tydef_id pp_var_type_dec_desc ty.tydef_desc
366 389

  
367
let pp_typedec fmt ty =
368
  fprintf fmt "type %s;" ty.tydec_id
390
let pp_typedec fmt ty = fprintf fmt "type %s;" ty.tydec_id
369 391

  
370 392
(* let rec pp_var_type fmt ty =  *)
371 393
(*   fprintf fmt "%a" (match ty.tdesc with  *)
......
378 400
(*     | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *)
379 401
(*   ) *)
380 402

  
381

  
382

  
383 403
(* let pp_quantifiers fmt (q, vars) =
384 404
 *   match q with
385 405
 *     | Forall -> fprintf fmt "forall %a" pp_vars vars 
386
 *     | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars  *)
406
 *     | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars *)
407

  
408
(*let pp_eexpr fmt e = fprintf fmt "%a%t %a" (Utils.fprintf_list ~sep:"; "
409
  pp_quantifiers) e.eexpr_quantifiers (fun fmt -> match e.eexpr_quantifiers with
410
  [] -> () | _ -> fprintf fmt ";") pp_expr e.eexpr_qfexpr *)
411

  
412
let pp_spec_eq fmt eq =
413
  fprintf fmt "var %a : %a = %a;" pp_eq_lhs eq.eq_lhs Types.print_node_ty
414
    eq.eq_rhs.expr_type pp_expr eq.eq_rhs
387 415

  
388
(*let pp_eexpr fmt e =
389
  fprintf fmt "%a%t %a"
390
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
391
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
392
    pp_expr e.eexpr_qfexpr
393
 *)
394
    
395
let pp_spec_eq fmt eq = 
396
  fprintf fmt "var %a : %a = %a;" 
397
    pp_eq_lhs eq.eq_lhs
398
    Types.print_node_ty eq.eq_rhs.expr_type
399
    pp_expr eq.eq_rhs
400
  
401 416
let pp_spec_stmt fmt stmt =
402
  match stmt with
403
  | Eq eq -> pp_spec_eq fmt eq
404
  | Aut _ -> assert false (* Not supported yet *)
405
             
406
  
417
  match stmt with Eq eq -> pp_spec_eq fmt eq | Aut _ -> assert false
418
(* Not supported yet *)
419

  
407 420
let pp_spec fmt spec =
408 421
  (* const are prefixed with const in pp_var and with nothing for regular
409 422
     variables. We adapt the call to produce the appropriate output. *)
410
    fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt v ->
411
    fprintf fmt "%a = %t;"
412
      pp_var v
413
      (fun fmt -> match v.var_dec_value with None -> assert false | Some e -> pp_expr fmt e)
414
    ) fmt spec.consts;
415
  
416
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt s -> pp_spec_stmt fmt s) fmt spec.stmts;
417
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r) fmt spec.assume;
418
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r) fmt spec.guarantees;
419
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt mode ->
420
    fprintf fmt "mode %s (@[<v 0>%a@ %a@]);" 
421
      mode.mode_id
422
      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "require %a;" pp_eexpr r)) mode.require
423
      (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r -> fprintf fmt "ensure %a;" pp_eexpr r)) mode.ensure
424
  ) fmt spec.modes;
425
  fprintf_list ~eol:"@, " ~sep:"@, " (fun fmt import ->
426
    fprintf fmt "import %s (%a) returns (%a);" 
427
      import.import_nodeid
428
      pp_expr import.inputs
429
      pp_expr import.outputs
430
  ) fmt spec.imports
431

  
432
(* Project the contract node as a pure contract: local memories are pushed back in the contract definition. Should mainly be used to print it *) 
423
  fprintf_list ~eol:"@, " ~sep:"@, "
424
    (fun fmt v ->
425
      fprintf fmt "%a = %t;" pp_var v (fun fmt ->
426
          match v.var_dec_value with
427
          | None ->
428
            assert false
429
          | Some e ->
430
            pp_expr fmt e))
431
    fmt spec.consts;
432

  
433
  fprintf_list ~eol:"@, " ~sep:"@, "
434
    (fun fmt s -> pp_spec_stmt fmt s)
435
    fmt spec.stmts;
436
  fprintf_list ~eol:"@, " ~sep:"@, "
437
    (fun fmt r -> fprintf fmt "assume %a;" pp_eexpr r)
438
    fmt spec.assume;
439
  fprintf_list ~eol:"@, " ~sep:"@, "
440
    (fun fmt r -> fprintf fmt "guarantee %a;" pp_eexpr r)
441
    fmt spec.guarantees;
442
  fprintf_list ~eol:"@, " ~sep:"@, "
443
    (fun fmt mode ->
444
      fprintf fmt "mode %s (@[<v 0>%a@ %a@]);" mode.mode_id
445
        (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r ->
446
             fprintf fmt "require %a;" pp_eexpr r))
447
        mode.require
448
        (fprintf_list ~eol:"" ~sep:"@ " (fun fmt r ->
449
             fprintf fmt "ensure %a;" pp_eexpr r))
450
        mode.ensure)
451
    fmt spec.modes;
452
  fprintf_list ~eol:"@, " ~sep:"@, "
453
    (fun fmt import ->
454
      fprintf fmt "import %s (%a) returns (%a);" import.import_nodeid pp_expr
455
        import.inputs pp_expr import.outputs)
456
    fmt spec.imports
457

  
458
(* Project the contract node as a pure contract: local memories are pushed back
459
   in the contract definition. Should mainly be used to print it *)
433 460
let node_as_contract nd =
434 461
  match nd.node_spec with
435
  | None | Some (NodeSpec _) -> raise (Invalid_argument "Not a contract")
436
  | Some (Contract c) -> (
437
    (* While a processed contract shall have no locals, sttms nor
438
       consts, an unprocessed one could. So we conservatively merge
439
       elements, to enable printing unprocessed contracts *)
440
    let consts, locals = List.partition(fun v -> v.var_dec_const) nd.node_locals in
441
    { c with
462
  | None | Some (NodeSpec _) ->
463
    raise (Invalid_argument "Not a contract")
464
  | Some (Contract c) ->
465
    (* While a processed contract shall have no locals, sttms nor consts, an
466
       unprocessed one could. So we conservatively merge elements, to enable
467
       printing unprocessed contracts *)
468
    let consts, locals =
469
      List.partition (fun v -> v.var_dec_const) nd.node_locals
470
    in
471
    {
472
      c with
442 473
      consts = consts @ c.consts;
443 474
      locals = locals @ c.locals;
444 475
      stmts = nd.node_stmts @ c.stmts;
445 476
    }
446
  )
447 477

  
448
(* Printing top contract as comments in regular output and as contract
449
   in kind2 *)
450
let pp_contract fmt nd =    
451
   let c = node_as_contract nd in
478
(* Printing top contract as comments in regular output and as contract in kind2 *)
479
let pp_contract fmt nd =
480
  let c = node_as_contract nd in
452 481
  fprintf fmt "@[<v 2>%scontract %s(%a) returns (%a);@ "
453 482
    (if !Options.kind2_print then "" else "(*@")
454
    nd.node_id
455
    pp_node_args nd.node_inputs
456
    pp_node_args nd.node_outputs;
483
    nd.node_id pp_node_args nd.node_inputs pp_node_args nd.node_outputs;
457 484
  fprintf fmt "@[<v 2>let@ ";
458 485
  pp_spec fmt c;
459
  fprintf fmt "@]@ tel@ @]%s@ "
460
  (if !Options.kind2_print then "" else "*)")
461
    
486
  fprintf fmt "@]@ tel@ @]%s@ " (if !Options.kind2_print then "" else "*)")
487

  
462 488
let pp_spec_as_comment fmt (inl, outl, spec) =
463 489
  match spec with
464
  | Contract c -> (* should have been processed by now *)
465
     fprintf fmt "@[<hov 2>(*@contract@ ";
466
     pp_spec fmt c;
467
     fprintf fmt "@]*)@ "
468
     
469
  | NodeSpec name -> (* Pushing stmts in contract. We update the
470
                      original information with the computed one in
471
                      nd. *)
472
     let pp_l = fprintf_list ~sep:"," pp_var_name in
473
     fprintf fmt "@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ "
474
       name
475
       pp_l inl
476
       pp_l outl
477
     
490
  | Contract c ->
491
    (* should have been processed by now *)
492
    fprintf fmt "@[<hov 2>(*@contract@ ";
493
    pp_spec fmt c;
494
    fprintf fmt "@]*)@ "
495
  | NodeSpec name ->
496
    (* Pushing stmts in contract. We update the original information with the
497
       computed one in nd. *)
498
    let pp_l = fprintf_list ~sep:"," pp_var_name in
499
    fprintf fmt "@[<hov 2>(*@contract import %s(%a) returns (%a); @]*)@ " name
500
      pp_l inl pp_l outl
501

  
478 502
let pp_node_vs_function fmt nd =
479 503
  fprintf fmt "%s" (if nd.node_dec_stateless then "function" else "node")
480
  
504

  
481 505
let pp_node fmt nd =
482 506
  (* Prototype *)
483
  fprintf fmt  "%a @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
484
    pp_node_vs_function nd
485
    nd.node_id
486
    pp_node_args nd.node_inputs
487
    pp_node_args nd.node_outputs;
507
  fprintf fmt "%a @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
508
    pp_node_vs_function nd nd.node_id pp_node_args nd.node_inputs pp_node_args
509
    nd.node_outputs;
488 510
  (* Contracts *)
489 511
  fprintf fmt "%a"
490
    (fun fmt s -> match s with
491
       | Some s -> pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s)
492
       | _ -> ()) nd.node_spec
493
    (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@ ") *);
512
    (fun fmt s ->
513
      match s with
514
      | Some s ->
515
        pp_spec_as_comment fmt (nd.node_inputs, nd.node_outputs, s)
516
      | _ ->
517
        ())
518
    nd.node_spec
519
  (* (fun fmt -> match nd.node_spec with None -> () | Some _ -> fprintf fmt "@
520
     ") *);
494 521
  (* Locals *)
495
  fprintf fmt "%a" (fun fmt locals ->
522
  fprintf fmt "%a"
523
    (fun fmt locals ->
496 524
      match locals with
497
      | [] -> ()
525
      | [] ->
526
        ()
498 527
      | _ ->
499 528
        fprintf fmt "@[<v 4>var %a@]@ "
500
          (fprintf_list ~sep:"@ "
501
	           (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
502
          locals
503
    ) nd.node_locals;
529
          (fprintf_list ~sep:"@ " (fun fmt v -> fprintf fmt "%a;" pp_node_var v))
530
          locals)
531
    nd.node_locals;
504 532
  (* Checks *)
505 533
  fprintf fmt "%a"
506 534
    (fun fmt checks ->
507
       match checks with
508
       | [] -> ()
509
       | _ ->
510
         fprintf fmt "@[<v 4>check@ %a@]@ "
511
           (fprintf_list ~sep:"@ "
512
	            (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
513
           checks
514
    ) nd.node_checks;
535
      match checks with
536
      | [] ->
537
        ()
538
      | _ ->
539
        fprintf fmt "@[<v 4>check@ %a@]@ "
540
          (fprintf_list ~sep:"@ " (fun fmt d ->
541
               fprintf fmt "%a" Dimension.pp_dimension d))
542
          checks)
543
    nd.node_checks;
515 544
  (* Body *)
516 545
  fprintf fmt "@[<v 2>let@ ";
517 546
  (* Annotations *)
518 547
  fprintf fmt "%a" (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot;
519 548
  (* Statements *)
520 549
  fprintf fmt "%a" pp_node_stmts nd.node_stmts;
521
  (* Asserts *)    
550
  (* Asserts *)
522 551
  fprintf fmt "%a" pp_asserts nd.node_asserts;
523
  (* closing boxes body (2)  and node (1) *) 
552
  (* closing boxes body (2) and node (1) *)
524 553
  fprintf fmt "@]@ tel"
525 554

  
526

  
527
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
555
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", "
556
  pp_print_string) (Scheduling.schedule_node nd)*)
528 557

  
529 558
let pp_node fmt nd =
530 559
  match nd.node_spec, nd.node_iscontract with
531
  | None, false
532
  | Some (NodeSpec _), false ->
560
  | None, false | Some (NodeSpec _), false ->
533 561
    pp_node fmt nd
534 562
  | Some (Contract _), false ->
535 563
    pp_node fmt nd (* may happen early in the compil process *)
536 564
  | Some (Contract _), true ->
537 565
    pp_contract fmt nd
538
  | _ -> assert false
539
     
540
let pp_imported_node fmt ind = 
566
  | _ ->
567
    assert false
568

  
569
let pp_imported_node fmt ind =
541 570
  fprintf fmt "@[<v 0>";
542 571
  (* Prototype *)
543
  fprintf fmt  "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
572
  fprintf fmt "%s @[<hov 0>%s (@[%a)@]@ returns (@[%a)@]@]@ "
544 573
    (if ind.nodei_stateless then "function" else "node")
545
    ind.nodei_id
546
    pp_node_args ind.nodei_inputs
547
    pp_node_args ind.nodei_outputs;
574
    ind.nodei_id pp_node_args ind.nodei_inputs pp_node_args ind.nodei_outputs;
548 575
  (* Contracts *)
549 576
  fprintf fmt "%a%t"
550
    (fun fmt s -> match s with Some s -> pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s) | _ -> ()) ind.nodei_spec
551
    (fun fmt -> match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
577
    (fun fmt s ->
578
      match s with
579
      | Some s ->
580
        pp_spec_as_comment fmt (ind.nodei_inputs, ind.nodei_outputs, s)
581
      | _ ->
582
        ())
583
    ind.nodei_spec
584
    (fun fmt ->
585
      match ind.nodei_spec with None -> () | Some _ -> fprintf fmt "@ ");
552 586
  fprintf fmt "@]@ "
553
  
554 587

  
555 588
let pp_const_decl fmt cdecl =
556 589
  fprintf fmt "%s = %a;" cdecl.const_id pp_const cdecl.const_value
557 590

  
558
let pp_const_decl_list fmt clist = 
591
let pp_const_decl_list fmt clist =
559 592
  fprintf_list ~sep:"@ " pp_const_decl fmt clist
560 593

  
561
  
562 594
let pp_decl fmt decl =
563 595
  match decl.top_decl_desc with
564 596
  | Node nd ->
565 597
    fprintf fmt "%a" pp_node nd
566
  | ImportedNode ind -> (* We do not print imported nodes *)
567
     fprintf fmt "(* imported %a; *)" pp_imported_node ind
598
  | ImportedNode ind ->
599
    (* We do not print imported nodes *)
600
    fprintf fmt "(* imported %a; *)" pp_imported_node ind
568 601
  | Const c ->
569 602
    fprintf fmt "const %a" pp_const_decl c
570 603
  | Open (local, s) ->
......
573 606
    fprintf fmt "include \"%s\"" s
574 607
  | TypeDef tdef ->
575 608
    fprintf fmt "%a" pp_typedef tdef
576
  
609

  
577 610
let pp_prog pp_decl fmt prog =
578 611
  (* we first print types: the function SortProg.sort could do the job but ut
579 612
     introduces a cyclic dependance *)
580

  
581 613
  let open_decl, prog =
582
    List.partition (fun decl -> match decl.top_decl_desc with
583
          Open _ -> true | _ -> false) prog
614
    List.partition
615
      (fun decl -> match decl.top_decl_desc with Open _ -> true | _ -> false)
616
      prog
584 617
  in
585 618
  let type_decl, prog =
586
    List.partition (fun decl -> match decl.top_decl_desc with
587
          TypeDef _ -> true | _ -> false) prog
619
    List.partition
620
      (fun decl ->
621
        match decl.top_decl_desc with TypeDef _ -> true | _ -> false)
622
      prog
588 623
  in
589
  pp_print_list
590
    ~pp_open_box:pp_open_vbox0
591
    ~pp_sep:pp_print_cutcut
592
    pp_decl
593
    fmt
624
  pp_print_list ~pp_open_box:pp_open_vbox0 ~pp_sep:pp_print_cutcut pp_decl fmt
594 625
    (open_decl @ type_decl @ prog)
595 626

  
596 627
(* Gives a short overview of model content. Do not print all node content *)
597 628
let pp_short_decl fmt decl =
598 629
  match decl.top_decl_desc with
599
  | Node nd -> fprintf fmt "%a %s@ "
600
                 pp_node_vs_function nd
601
                 nd.node_id
602
  | ImportedNode ind -> fprintf fmt "imported node %s" ind.nodei_id
603
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
604
  | Include s -> fprintf fmt "include \"%s\"" s
605
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
606
  | TypeDef tdef -> fprintf fmt "type %s;@ " tdef.tydef_id
630
  | Node nd ->
631
    fprintf fmt "%a %s@ " pp_node_vs_function nd nd.node_id
632
  | ImportedNode ind ->
633
    fprintf fmt "imported node %s" ind.nodei_id
634
  | Const c ->
635
    fprintf fmt "const %a@ " pp_const_decl c
636
  | Include s ->
637
    fprintf fmt "include \"%s\"" s
638
  | Open (local, s) ->
639
    if local then fprintf fmt "#open \"%s\"@ " s
640
    else fprintf fmt "#open <%s>@ " s
641
  | TypeDef tdef ->
642
    fprintf fmt "type %s;@ " tdef.tydef_id
607 643

  
608 644
let pp_prog_short = pp_prog pp_short_decl
645

  
609 646
let pp_prog = pp_prog pp_decl
610
            
611
let pp_lusi fmt decl = 
647

  
648
let pp_lusi fmt decl =
612 649
  match decl.top_decl_desc with
613
  | ImportedNode ind -> fprintf fmt "%a;@ " pp_imported_node ind
614
  | Const c -> fprintf fmt "const %a@ " pp_const_decl c
615
  | Include s -> fprintf fmt "include \"%s\"" s
616
  | Open (local, s) -> if local then fprintf fmt "#open \"%s\"@ " s else fprintf fmt "#open <%s>@ " s
617
  | TypeDef tdef -> fprintf fmt "%a@ " pp_typedef tdef
618
  | Node _ -> assert false
619
                
650
  | ImportedNode ind ->
651
    fprintf fmt "%a;@ " pp_imported_node ind
652
  | Const c ->
653
    fprintf fmt "const %a@ " pp_const_decl c
654
  | Include s ->
655
    fprintf fmt "include \"%s\"" s
656
  | Open (local, s) ->
657
    if local then fprintf fmt "#open \"%s\"@ " s
658
    else fprintf fmt "#open <%s>@ " s
659
  | TypeDef tdef ->
660
    fprintf fmt "%a@ " pp_typedef tdef
661
  | Node _ ->
662
    assert false
663

  
620 664
let pp_lusi_header fmt basename prog =
621 665
  fprintf fmt "@[<v 0>";
622 666
  fprintf fmt "(* Generated Lustre Interface file from %s.lus *)@ " basename;
623
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number pp_date (Unix.gmtime (Unix.time ()));
624
  fprintf fmt "(* Feel free to mask some of the definitions by removing them from this file. *)@ @ ";
667
  fprintf fmt "(* by Lustre-C compiler version %s, %a *)@ " Version.number
668
    pp_date
669
    (Unix.gmtime (Unix.time ()));
670
  fprintf fmt
671
    "(* Feel free to mask some of the definitions by removing them from this \
672
     file. *)@ @ ";
625 673
  List.iter (fprintf fmt "%a@ " pp_lusi) prog;
626 674
  fprintf fmt "@]@."
627 675

  
628 676
let pp_offset fmt offset =
629 677
  match offset with
630
  | Index i -> fprintf fmt "[%a]" Dimension.pp_dimension i
631
  | Field f -> fprintf fmt ".%s" f
678
  | Index i ->
679
    fprintf fmt "[%a]" Dimension.pp_dimension i
680
  | Field f ->
681
    fprintf fmt ".%s" f
632 682

  
633 683
let pp_node_list fmt prog =
634 684
  Format.fprintf fmt "@[<h 2>%a@]"
635
    (fprintf_list
636
       ~sep:"@ "
637
       (fun fmt decl ->
685
    (fprintf_list ~sep:"@ " (fun fmt decl ->
638 686
         match decl.top_decl_desc with
639
         | Node nd -> Format.fprintf fmt "%s" nd.node_id
640
         | _ -> ()
641
    ))
687
         | Node nd ->
688
           Format.fprintf fmt "%s" nd.node_id
689
         | _ ->
690
           ()))
642 691
    prog
643
    
692

  
644 693
(* Local Variables: *)
645 694
(* compile-command:"make -C .." *)
646 695
(* End: *)

Also available in: Unified diff