Revision c02d255e
Added by Pierre-Loïc Garoche almost 9 years ago
| src/printers.ml | ||
|---|---|---|
| 60 | 60 |
| Expr_power (a, d) -> fprintf fmt "(%a^%a)" pp_expr a Dimension.pp_dimension d |
| 61 | 61 |
| Expr_tuple el -> fprintf fmt "(%a)" pp_tuple el |
| 62 | 62 |
| Expr_ite (c, t, e) -> fprintf fmt "(if %a then %a else %a)" pp_expr c pp_expr t pp_expr e |
| 63 |
| Expr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_expr e1 pp_expr e2
|
|
| 63 |
| Expr_arrow (e1, e2) -> fprintf fmt "(%a -> %a)" pp_expr e1 pp_expr e2
|
|
| 64 | 64 |
| Expr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_expr e1 pp_expr e2 |
| 65 | 65 |
| Expr_pre e -> fprintf fmt "pre %a" pp_expr e |
| 66 | 66 |
| Expr_when (e, id, l) -> fprintf fmt "%a when %s(%s)" pp_expr e l id |
| ... | ... | |
| 101 | 101 |
| "!=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_expr e1 pp_expr e2 |
| 102 | 102 |
| "=", Expr_tuple([e1;e2]) -> fprintf fmt "(%a = %a)" pp_expr e1 pp_expr e2 |
| 103 | 103 |
| "not", _ -> fprintf fmt "(not %a)" pp_expr e |
| 104 |
| _ -> fprintf fmt "%s (%a)" id pp_expr e) |
|
| 104 |
| _, Expr_tuple _ -> fprintf fmt "%s %a" id pp_expr e |
|
| 105 |
| _ -> fprintf fmt "%s (%a)" id pp_expr e |
|
| 106 |
) |
|
| 105 | 107 |
| Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x |
| 106 | 108 |
|
| 107 | 109 |
let pp_node_eq fmt eq = |
| ... | ... | |
| 138 | 140 |
(* | Ttuple tel -> fprintf_list ~sep:" * " pp_var_type fmt tel *) |
| 139 | 141 |
(* ) *) |
| 140 | 142 |
|
| 143 |
|
|
| 144 |
let pp_econst fmt c = |
|
| 145 |
match c with |
|
| 146 |
| EConst_int i -> pp_print_int fmt i |
|
| 147 |
| EConst_real r -> pp_print_string fmt r |
|
| 148 |
| EConst_float r -> pp_print_float fmt r |
|
| 149 |
| EConst_bool b -> pp_print_bool fmt b |
|
| 150 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
|
|
| 151 |
|
|
| 152 |
let rec pp_eexpr fmt eexpr = |
|
| 153 |
match eexpr.eexpr_desc with |
|
| 154 |
| EExpr_const c -> pp_econst fmt c |
|
| 155 |
| EExpr_ident id -> pp_print_string fmt id |
|
| 156 |
| EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el |
|
| 157 |
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2 |
|
| 158 |
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2 |
|
| 159 |
(* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *) |
|
| 160 |
(* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *) |
|
| 161 |
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e |
|
| 162 |
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id |
|
| 163 |
| EExpr_merge (id, e1, e2) -> |
|
| 164 |
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2 |
|
| 165 |
| EExpr_appl (id, e, r) -> pp_eapp fmt id e r |
|
| 166 |
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e |
|
| 167 |
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e |
|
| 168 |
|
|
| 169 |
|
|
| 170 |
(* | EExpr_whennot _ *) |
|
| 171 |
(* | EExpr_uclock _ *) |
|
| 172 |
(* | EExpr_dclock _ *) |
|
| 173 |
(* | EExpr_phclock _ -> assert false *) |
|
| 174 |
and pp_eapp fmt id e r = |
|
| 175 |
match r with |
|
| 176 |
| None -> |
|
| 177 |
(match id, e.eexpr_desc with |
|
| 178 |
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 179 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e |
|
| 180 |
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 181 |
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 182 |
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 183 |
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 184 |
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 185 |
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 186 |
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 187 |
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 188 |
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 189 |
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 190 |
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 191 |
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 192 |
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 193 |
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 194 |
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e |
|
| 195 |
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3 |
|
| 196 |
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e) |
|
| 197 |
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x |
|
| 198 |
|
|
| 199 |
|
|
| 200 |
let pp_ensures fmt e = |
|
| 201 |
match e with |
|
| 202 |
| EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e |
|
| 203 |
| SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args |
|
| 204 |
|
|
| 205 |
let pp_spec fmt spec = |
|
| 206 |
fprintf fmt "@[<hov 2>(*@@ "; |
|
| 207 |
fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires; |
|
| 208 |
fprintf_list ~sep:"" pp_ensures fmt spec.ensures; |
|
| 209 |
fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> |
|
| 210 |
fprintf fmt "behavior %s:@[@ %a@ %a@]" |
|
| 211 |
name |
|
| 212 |
(fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes |
|
| 213 |
(fprintf_list ~sep:"@ " pp_ensures) requires |
|
| 214 |
) fmt spec.behaviors; |
|
| 215 |
fprintf fmt "@]*)"; |
|
| 216 |
() |
|
| 217 |
|
|
| 141 | 218 |
let pp_node fmt nd = |
| 142 |
fprintf fmt "@[<v>node %s (%a) returns (%a)@ %a%alet@ @[<h 2> @ @[%a@]@ @]@ tel@]@ " |
|
| 219 |
fprintf fmt "@[<v 0>%a%tnode %s (%a) returns (%a)@.%a%alet@.@[<h 2> @ @[%a@]@ @]@.tel@]@." |
|
| 220 |
(fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec |
|
| 221 |
(fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.") |
|
| 143 | 222 |
nd.node_id |
| 144 | 223 |
pp_node_args nd.node_inputs |
| 145 | 224 |
pp_node_args nd.node_outputs |
| ... | ... | |
| 212 | 291 |
pp_node_args nd.node_outputs |
| 213 | 292 |
| ImportedNode _ | ImportedFun _ | Consts _ | Open _ -> () |
| 214 | 293 |
|
| 215 |
let pp_econst fmt c = |
|
| 216 |
match c with |
|
| 217 |
| EConst_int i -> pp_print_int fmt i |
|
| 218 |
| EConst_real r -> pp_print_string fmt r |
|
| 219 |
| EConst_float r -> pp_print_float fmt r |
|
| 220 |
| EConst_bool b -> pp_print_bool fmt b |
|
| 221 |
| EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
|
|
| 222 | 294 |
|
| 223 |
let rec pp_eexpr is_output fmt eexpr = |
|
| 224 |
let pp_eexpr = pp_eexpr is_output in |
|
| 225 |
match eexpr.eexpr_desc with |
|
| 226 |
| EExpr_const c -> pp_econst fmt c |
|
| 227 |
| EExpr_ident id -> |
|
| 228 |
if is_output id then pp_print_string fmt ("*" ^ id) else pp_print_string fmt id
|
|
| 229 |
| EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el |
|
| 230 |
| EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2 |
|
| 231 |
| EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2 |
|
| 232 |
| EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 |
|
| 233 |
| EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e |
|
| 234 |
| EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e |
|
| 235 |
| EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id |
|
| 236 |
| EExpr_merge (id, e1, e2) -> |
|
| 237 |
fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2 |
|
| 238 |
| EExpr_appl (id, e, r) -> pp_eapp is_output fmt id e r |
|
| 239 |
| EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e |
|
| 240 |
| EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e |
|
| 241 |
|
|
| 242 |
|
|
| 243 |
| EExpr_whennot _ |
|
| 244 |
| EExpr_uclock _ |
|
| 245 |
| EExpr_dclock _ |
|
| 246 |
| EExpr_phclock _ -> assert false |
|
| 247 |
and pp_eapp is_output fmt id e r = |
|
| 248 |
let pp_eexpr = pp_eexpr is_output in |
|
| 249 |
match r with |
|
| 250 |
| None -> |
|
| 251 |
(match id, e.eexpr_desc with |
|
| 252 |
| "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 253 |
| "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e |
|
| 254 |
| "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 255 |
| "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 256 |
| "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 257 |
| "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 258 |
| "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 259 |
| "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 260 |
| "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 261 |
| "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 262 |
| "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 263 |
| "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 264 |
| ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 265 |
| ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 266 |
| "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 267 |
| "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2 |
|
| 268 |
| "not", _ -> fprintf fmt "(! %a)" pp_eexpr e |
|
| 269 |
| "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3 |
|
| 270 |
| _ -> fprintf fmt "%s (%a)" id pp_eexpr e) |
|
| 271 |
| Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x |
|
| 272 |
|
|
| 273 |
|
|
| 274 |
let pp_ensures is_output fmt e = |
|
| 275 |
let pp_eexpr = pp_eexpr is_output in |
|
| 276 |
match e with |
|
| 277 |
| EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e |
|
| 278 |
| SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args |
|
| 279 |
|
|
| 280 |
let pp_acsl_spec outputs fmt spec = |
|
| 281 |
let is_output = fun oid -> List.exists (fun v -> v.var_id = oid) outputs in |
|
| 282 |
let pp_eexpr = pp_eexpr is_output in |
|
| 283 |
fprintf fmt "@[<v 2>/*@@ "; |
|
| 284 |
fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires; |
|
| 285 |
fprintf_list ~sep:"" (pp_ensures is_output) fmt spec.ensures; |
|
| 286 |
fprintf fmt "@ "; |
|
| 287 |
(* fprintf fmt "assigns *self%t%a;@ " *) |
|
| 288 |
(* (fun fmt -> if List.length outputs > 0 then fprintf fmt ", ") *) |
|
| 289 |
(* (fprintf_list ~sep:"," (fun fmt v -> fprintf fmt "*%s" v.var_id)) outputs; *) |
|
| 290 |
fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> |
|
| 291 |
fprintf fmt "behavior %s:@[@ %a@ %a@]" |
|
| 292 |
name |
|
| 293 |
(fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes |
|
| 294 |
(fprintf_list ~sep:"@ " (pp_ensures is_output)) requires |
|
| 295 |
) fmt spec.behaviors; |
|
| 296 |
fprintf fmt "@]@ */@."; |
|
| 297 |
() |
|
| 298 | 295 |
|
| 299 | 296 |
|
| 300 | 297 |
let pp_lusi_header fmt filename prog = |
Also available in: Unified diff
Solved some bugs in the lustre printer
Generation of a witness with both the main node and hte inlined main node
Test script modified to check consistency of the inlining process