Revision ca7ff3f7
Added by Lélio Brun over 1 year ago
| 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
reformatting