Project

General

Profile

Revision 0038002e src/printers.ml

View differences:

src/printers.ml
50 50
    | Const_tag  t -> pp_print_string fmt t
51 51
    | Const_array ca -> Format.fprintf fmt "[%a]" (Utils.fprintf_list ~sep:"," pp_const) ca
52 52
    | Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
53
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
53 54

  
54 55
and 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
55 56

  
......
71 72
    | Expr_merge (id, hl) -> 
72 73
      fprintf fmt "merge %s %a" id pp_handlers hl
73 74
    | Expr_appl (id, e, r) -> pp_app fmt id e r
74
    | Expr_uclock _
75
    | Expr_dclock _
76
    | Expr_phclock _ -> assert false
77 75

  
78 76
and pp_tuple fmt el =
79 77
 fprintf_list ~sep:"," pp_expr fmt el
......
148 146
(*   ) *)
149 147

  
150 148

  
151
let pp_econst fmt c = 
152
  match c with
153
    | EConst_int i -> pp_print_int fmt i
154
    | EConst_real r -> pp_print_string fmt r
155
    | EConst_float r -> pp_print_float fmt r
156
    | EConst_bool b -> pp_print_bool fmt b
157
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
158

  
159
let rec pp_eexpr fmt eexpr = 
160
  match eexpr.eexpr_desc with
161
    | EExpr_const c -> pp_econst fmt c
162
    | EExpr_ident id -> pp_print_string fmt id
163
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
164
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
165
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
166
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
167
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
168
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
169
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
170
    | EExpr_merge (id, e1, e2) -> 
171
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
172
    | EExpr_appl (id, e, r) -> pp_eapp fmt id e r
173
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
174
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
175

  
176

  
177
    (* | EExpr_whennot _ *)
178
    (* | EExpr_uclock _ *)
179
    (* | EExpr_dclock _ *)
180
    (* | EExpr_phclock _ -> assert false *)
181
and pp_eapp fmt id e r =
182
  match r with
183
  | None ->
184
    (match id, e.eexpr_desc with
185
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
186
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
187
    | "-", 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
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %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
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
194
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
195
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
196
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
197
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
198
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
199
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
200
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
201
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
202
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
203
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
204
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
205 149

  
206
  
207
let pp_ensures fmt e =
208
  match e with
209
    | EnsuresExpr e -> fprintf fmt "ensures %a;@ " pp_eexpr e
210
    | SpecObserverNode (name, args) -> fprintf fmt "observer %s (%a);@ " name (fprintf_list ~sep:", " pp_eexpr) args
211
 
150
let pp_quantifiers fmt (q, vars) =
151
  match q with
152
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
153
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
154

  
155
let pp_eexpr fmt e =
156
  fprintf fmt "%a%t %a"
157
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
158
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
159
    pp_expr e.eexpr_qfexpr
160

  
212 161
let pp_spec fmt spec =
213 162
  fprintf fmt "@[<hov 2>(*@@ ";
214
  fprintf_list ~sep:"" (fun fmt r -> fprintf fmt "requires %a;@ " pp_eexpr r) fmt spec.requires;
215
  fprintf_list ~sep:"" pp_ensures fmt spec.ensures;
216
  fprintf_list ~sep:"@ " (fun fmt (name, assumes, requires) -> 
163
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
164
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "ensures %a; " pp_eexpr r) fmt spec.ensures;
165
  fprintf_list ~sep:"@;" (fun fmt (name, assumes, ensures, _) -> 
217 166
    fprintf fmt "behavior %s:@[@ %a@ %a@]" 
218 167
      name
219 168
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "assumes %a;" pp_eexpr r)) assumes
220
      (fprintf_list ~sep:"@ " pp_ensures) requires
169
      (fprintf_list ~sep:"@ " (fun fmt r -> fprintf fmt "ensures %a;" pp_eexpr r)) ensures
221 170
  ) fmt spec.behaviors;
222 171
  fprintf fmt "@]*)";
223 172
  ()

Also available in: Unified diff