1
|
(********************************************************************)
|
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
|
open LustreSpec
|
13
|
open Format
|
14
|
open Utils
|
15
|
|
16
|
(* Prints [v] as [pp_fun] would do, but adds a backslash at each end of line,
|
17
|
following the C convention for multiple lines macro *)
|
18
|
let pp_as_c_macro pp_fun fmt v =
|
19
|
let formatter_out_funs = pp_get_formatter_out_functions fmt () in
|
20
|
let macro_newline () =
|
21
|
begin
|
22
|
formatter_out_funs.out_string "\\" 0 1;
|
23
|
formatter_out_funs.out_newline ()
|
24
|
end in
|
25
|
begin
|
26
|
pp_set_formatter_out_functions fmt { formatter_out_funs with out_newline = macro_newline };
|
27
|
pp_fun fmt v;
|
28
|
pp_set_formatter_out_functions fmt formatter_out_funs;
|
29
|
end
|
30
|
|
31
|
let rec print_dec_struct_ty_field fmt (label, cty) =
|
32
|
fprintf fmt "%a : %a" pp_print_string label print_dec_ty cty
|
33
|
and print_dec_ty fmt cty =
|
34
|
match (*get_repr_type*) cty with
|
35
|
| Tydec_any -> fprintf fmt "Any"
|
36
|
| Tydec_int -> fprintf fmt "int"
|
37
|
| Tydec_real -> fprintf fmt "real"
|
38
|
| Tydec_bool -> fprintf fmt "bool"
|
39
|
| Tydec_clock cty' -> fprintf fmt "%a clock" print_dec_ty cty'
|
40
|
| Tydec_const c -> fprintf fmt "%s" c
|
41
|
| Tydec_enum taglist -> fprintf fmt "enum {%a }"
|
42
|
(Utils.fprintf_list ~sep:", " pp_print_string) taglist
|
43
|
| Tydec_struct fieldlist -> fprintf fmt "struct {%a }"
|
44
|
(Utils.fprintf_list ~sep:"; " print_dec_struct_ty_field) fieldlist
|
45
|
| Tydec_array (d, cty') -> fprintf fmt "%a^%a" print_dec_ty cty' Dimension.pp_dimension d
|
46
|
|
47
|
let pp_var_name fmt id = fprintf fmt "%s" id.var_id
|
48
|
|
49
|
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
|
50
|
|
51
|
let pp_var fmt id = fprintf fmt "%s%s: %a" (if id.var_dec_const then "const " else "") id.var_id Types.print_ty id.var_type
|
52
|
|
53
|
let pp_quantifiers fmt (q, vars) =
|
54
|
match q with
|
55
|
| Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars
|
56
|
| Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars
|
57
|
|
58
|
let rec pp_struct_const_field fmt (label, c) =
|
59
|
fprintf fmt "%a = %a;" pp_print_string label pp_const c
|
60
|
and pp_const fmt c =
|
61
|
match c with
|
62
|
| Const_int i -> pp_print_int fmt i
|
63
|
| Const_real (c, e, s) -> pp_print_string fmt s (*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 *)
|
64
|
(* | Const_float r -> pp_print_float fmt r *)
|
65
|
| Const_tag t -> pp_print_string fmt t
|
66
|
| Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
|
67
|
| Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
|
68
|
| Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
|
69
|
|
70
|
|
71
|
let rec pp_expr fmt expr =
|
72
|
(match expr.expr_annot with
|
73
|
| None -> fprintf fmt "%t"
|
74
|
| Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann)
|
75
|
(fun fmt ->
|
76
|
match expr.expr_desc with
|
77
|
| Expr_const c -> pp_const fmt c
|
78
|
| Expr_ident id -> Format.fprintf fmt "%s" id
|
79
|
| Expr_array a -> fprintf fmt "[%a]" pp_tuple a
|
80
|
| Expr_access (a, d) -> fprintf fmt "%a[%a]" pp_expr a Dimension.pp_dimension d
|
81
|
| Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d
|
82
|
| Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el
|
83
|
| Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e
|
84
|
| Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
|
85
|
| Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2
|
86
|
| Expr_pre e -> fprintf fmt "pre %a" pp_expr e
|
87
|
| Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id
|
88
|
| Expr_merge (id, hl) ->
|
89
|
fprintf fmt "merge %s %a" id pp_handlers hl
|
90
|
| Expr_appl (id, e, r) -> pp_app fmt id e r
|
91
|
)
|
92
|
and pp_tuple fmt el =
|
93
|
fprintf_list ~sep:"," pp_expr fmt el
|
94
|
|
95
|
and pp_handler fmt (t, h) =
|
96
|
fprintf fmt "(%s -> %a)" t pp_expr h
|
97
|
|
98
|
and pp_handlers fmt hl =
|
99
|
fprintf_list ~sep:" " pp_handler fmt hl
|
100
|
|
101
|
and pp_app fmt id e r =
|
102
|
match r with
|
103
|
| None -> pp_call fmt id e
|
104
|
| Some c -> fprintf fmt "%t every (%a)" (fun fmt -> pp_call fmt id e) pp_expr c
|
105
|
|
106
|
and pp_call fmt id e =
|
107
|
match id, e.expr_desc with
|
108
|
| "+", Expr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_expr e1 pp_expr e2
|
109
|
| "uminus", _ -> fprintf fmt "(- %a)" pp_expr e
|
110
|
| "-", Expr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_expr e1 pp_expr e2
|
111
|
| "*", Expr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_expr e1 pp_expr e2
|
112
|
| "/", Expr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_expr e1 pp_expr e2
|
113
|
| "mod", Expr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_expr e1 pp_expr e2
|
114
|
| "&&", Expr_tuple([e1;e2]) -> fprintf fmt "(%a and %a)" pp_expr e1 pp_expr e2
|
115
|
| "||", Expr_tuple([e1;e2]) -> fprintf fmt "(%a or %a)" pp_expr e1 pp_expr e2
|
116
|
| "xor", Expr_tuple([e1;e2]) -> fprintf fmt "(%a xor %a)" pp_expr e1 pp_expr e2
|
117
|
| "impl", Expr_tuple([e1;e2]) -> fprintf fmt "(%a => %a)" pp_expr e1 pp_expr e2
|
118
|
| "<", Expr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_expr e1 pp_expr e2
|
119
|
| "<=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_expr e1 pp_expr e2
|
120
|
| ">", Expr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_expr e1 pp_expr e2
|
121
|
| ">=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_expr e1 pp_expr e2
|
122
|
| "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2
|
123
|
| "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2
|
124
|
| "not", _ -> fprintf fmt "(not %a)" pp_expr e
|
125
|
| _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e
|
126
|
| _ -> fprintf fmt "%s (%a)" id pp_expr e
|
127
|
|
128
|
and pp_eexpr fmt e =
|
129
|
fprintf fmt "%a%t %a"
|
130
|
(Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
|
131
|
(fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
|
132
|
pp_expr e.eexpr_qfexpr
|
133
|
|
134
|
|
135
|
and pp_expr_annot fmt expr_ann =
|
136
|
let pp_annot fmt (kwds, ee) =
|
137
|
Format.fprintf fmt "(*! %t: %a; *)"
|
138
|
(fun fmt -> match kwds with | [] -> assert false | [x] -> Format.pp_print_string fmt x | _ -> Format.fprintf fmt "/%a/" (fprintf_list ~sep:"/" Format.pp_print_string) kwds)
|
139
|
pp_eexpr ee
|
140
|
in
|
141
|
fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
|
142
|
|
143
|
(*
|
144
|
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
|
145
|
*)
|
146
|
let pp_node_var fmt id =
|
147
|
begin
|
148
|
fprintf fmt "%s%s: %a%a" (if id.var_dec_const then "const " else "") id.var_id Types.print_node_ty id.var_type Clocks.print_ck_suffix id.var_clock;
|
149
|
match id.var_dec_value with
|
150
|
| None -> ()
|
151
|
| Some v -> fprintf fmt " = %a" pp_expr v
|
152
|
end
|
153
|
|
154
|
let pp_node_args = fprintf_list ~sep:"; " pp_node_var
|
155
|
|
156
|
let pp_node_eq fmt eq =
|
157
|
fprintf fmt "%a = %a;"
|
158
|
pp_eq_lhs eq.eq_lhs
|
159
|
pp_expr eq.eq_rhs
|
160
|
|
161
|
let pp_restart fmt restart =
|
162
|
Format.fprintf fmt "%s" (if restart then "restart" else "resume")
|
163
|
|
164
|
let pp_unless fmt (_, expr, restart, st) =
|
165
|
Format.fprintf fmt "unless %a %a %s@ "
|
166
|
pp_expr expr
|
167
|
pp_restart restart
|
168
|
st
|
169
|
|
170
|
let pp_until fmt (_, expr, restart, st) =
|
171
|
Format.fprintf fmt "until %a %a %s@ "
|
172
|
pp_expr expr
|
173
|
pp_restart restart
|
174
|
st
|
175
|
|
176
|
let rec pp_handler fmt handler =
|
177
|
Format.fprintf fmt "state %s ->@ @[<v 2> %a%alet@,@[<v 2> %a@]@,tel%a@]"
|
178
|
handler.hand_state
|
179
|
(Utils.fprintf_list ~sep:"@," pp_unless) handler.hand_unless
|
180
|
(fun fmt locals ->
|
181
|
match locals with [] -> () | _ ->
|
182
|
Format.fprintf fmt "@[<v 4>var %a@]@ "
|
183
|
(Utils.fprintf_list ~sep:"@ "
|
184
|
(fun fmt v -> Format.fprintf fmt "%a;" pp_node_var v))
|
185
|
locals |