Project

General

Profile

« Previous | Next » 

Revision 36454535

Added by Pierre-Loïc Garoche over 10 years ago

Merged horn_traces branch

View differences:

src/printers.ml
40 40

  
41 41
let pp_eq_lhs = fprintf_list ~sep:", " pp_print_string
42 42

  
43
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
44

  
45
let pp_node_var fmt id = 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
46

  
47
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
48

  
49
let pp_quantifiers fmt (q, vars) =
50
  match q with
51
    | Forall -> fprintf fmt "forall %a" (fprintf_list ~sep:"; " pp_var) vars 
52
    | Exists -> fprintf fmt "exists %a" (fprintf_list ~sep:"; " pp_var) vars 
53

  
54
(*
55
let pp_econst fmt c = 
56
  match c with
57
    | EConst_int i -> pp_print_int fmt i
58
    | EConst_real r -> pp_print_string fmt r
59
    | EConst_float r -> pp_print_float fmt r
60
    | EConst_tag  t -> pp_print_string fmt t
61
    | EConst_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
62

  
63

  
64
let rec pp_eexpr fmt eexpr = 
65
  match eexpr.eexpr_desc with
66
    | EExpr_const c -> pp_econst fmt c
67
    | EExpr_ident id -> pp_print_string fmt id
68
    | EExpr_tuple el -> fprintf_list ~sep:"," pp_eexpr fmt el
69
    | EExpr_arrow (e1, e2) -> fprintf fmt "%a -> %a" pp_eexpr e1 pp_eexpr e2
70
    | EExpr_fby (e1, e2) -> fprintf fmt "%a fby %a" pp_eexpr e1 pp_eexpr e2
71
    (* | EExpr_concat (e1, e2) -> fprintf fmt "%a::%a" pp_eexpr e1 pp_eexpr e2 *)
72
    (* | EExpr_tail e -> fprintf fmt "tail %a" pp_eexpr e *)
73
    | EExpr_pre e -> fprintf fmt "pre %a" pp_eexpr e
74
    | EExpr_when (e, id) -> fprintf fmt "%a when %s" pp_eexpr e id
75
    | EExpr_merge (id, e1, e2) -> 
76
      fprintf fmt "merge (%s, %a, %a)" id pp_eexpr e1 pp_eexpr e2
77
    | EExpr_appl (id, e, r) -> pp_eapp fmt id e r
78
    | EExpr_forall (vars, e) -> fprintf fmt "forall %a; %a" pp_node_args vars pp_eexpr e 
79
    | EExpr_exists (vars, e) -> fprintf fmt "exists %a; %a" pp_node_args vars pp_eexpr e 
80

  
81

  
82
    (* | EExpr_whennot _ *)
83
    (* | EExpr_uclock _ *)
84
    (* | EExpr_dclock _ *)
85
    (* | EExpr_phclock _ -> assert false *)
86
and pp_eapp fmt id e r =
87
  match r with
88
  | None ->
89
    (match id, e.eexpr_desc with
90
    | "+", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a + %a)" pp_eexpr e1 pp_eexpr e2
91
    | "uminus", _ -> fprintf fmt "(- %a)" pp_eexpr e
92
    | "-", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a - %a)" pp_eexpr e1 pp_eexpr e2
93
    | "*", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a * %a)" pp_eexpr e1 pp_eexpr e2
94
    | "/", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a / %a)" pp_eexpr e1 pp_eexpr e2
95
    | "mod", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a mod %a)" pp_eexpr e1 pp_eexpr e2
96
    | "&&", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a && %a)" pp_eexpr e1 pp_eexpr e2
97
    | "||", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a || %a)" pp_eexpr e1 pp_eexpr e2
98
    | "xor", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ^^ %a)" pp_eexpr e1 pp_eexpr e2
99
    | "impl", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a ==> %a)" pp_eexpr e1 pp_eexpr e2
100
    | "<", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a < %a)" pp_eexpr e1 pp_eexpr e2
101
    | "<=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a <= %a)" pp_eexpr e1 pp_eexpr e2
102
    | ">", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a > %a)" pp_eexpr e1 pp_eexpr e2
103
    | ">=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a >= %a)" pp_eexpr e1 pp_eexpr e2
104
    | "!=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a != %a)" pp_eexpr e1 pp_eexpr e2
105
    | "=", EExpr_tuple([e1;e2]) -> fprintf fmt "(%a == %a)" pp_eexpr e1 pp_eexpr e2
106
    | "not", _ -> fprintf fmt "(! %a)" pp_eexpr e
107
    | "ite", EExpr_tuple([e1;e2;e3]) -> fprintf fmt "(if %a then %a else %a)" pp_eexpr e1 pp_eexpr e2 pp_eexpr e3
108
    | _ -> fprintf fmt "%s (%a)" id pp_eexpr e)
109
  | Some x -> fprintf fmt "%s (%a) every %s" id pp_eexpr e x 
110
*)
111

  
112

  
43 113
let rec pp_struct_const_field fmt (label, c) =
44 114
  fprintf fmt "%a = %a;" pp_print_string label pp_const c
45 115
and pp_const fmt c = 
......
52 122
    | Const_struct fl -> Format.fprintf fmt "{%a }" (Utils.fprintf_list ~sep:" " pp_struct_const_field) fl
53 123
    | Const_string s -> pp_print_string fmt ("\"" ^ s ^ "\"")
54 124

  
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
56

  
57
and pp_node_var fmt id = 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
58 125

  
59
and pp_expr fmt expr =
60
  match expr.expr_desc with
126
let rec pp_expr fmt expr =
127
  (match expr.expr_annot with 
128
  | None -> fprintf fmt "%t" 
129
  | Some ann -> fprintf fmt "(%a %t)" pp_expr_annot ann)
130
    (fun fmt -> 
131
      match expr.expr_desc with
61 132
    | Expr_const c -> pp_const fmt c
62 133
    | Expr_ident id -> Format.fprintf fmt "%s" id
63 134
    | Expr_array a -> fprintf fmt "[%a]" pp_tuple a
......
72 143
    | Expr_merge (id, hl) -> 
73 144
      fprintf fmt "merge %s %a" id pp_handlers hl
74 145
    | Expr_appl (id, e, r) -> pp_app fmt id e r
75

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

  
......
107 178
    | _ -> fprintf fmt "%s (%a)" id pp_expr e
108 179
)
109 180
  | Some (x, l) -> fprintf fmt "%s (%a) every %s(%s)" id pp_expr e l x 
181

  
182

  
183

  
184
and pp_eexpr fmt e =
185
  fprintf fmt "%a%t %a"
186
    (Utils.fprintf_list ~sep:"; " pp_quantifiers) e.eexpr_quantifiers
187
    (fun fmt -> match e.eexpr_quantifiers with [] -> () | _ -> fprintf fmt ";")
188
    pp_expr e.eexpr_qfexpr
189

  
190

  
191
and pp_expr_annot fmt expr_ann =
192
  let pp_annot fmt (kwds, ee) =
193
    Format.fprintf fmt "(*! %t: %a *)"
194
      (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)
195
      pp_eexpr ee
196
  in
197
  fprintf_list ~sep:"@ " pp_annot fmt expr_ann.annots
198
    
110 199
	
111 200
let pp_node_eq fmt eq = 
112 201
  fprintf fmt "%a = %a;" 
......
115 204

  
116 205
let pp_node_eqs = fprintf_list ~sep:"@ " pp_node_eq 
117 206

  
118
let pp_node_args = fprintf_list ~sep:"; " pp_node_var 
119 207

  
120 208
let pp_var_type_dec fmt ty =
121 209
  let rec pp_var_struct_type_field fmt (label, tdesc) =
......
146 234
(*   ) *)
147 235

  
148 236

  
149

  
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

  
161 237
let pp_spec fmt spec =
162 238
  fprintf fmt "@[<hov 2>(*@@ ";
163 239
  fprintf_list ~sep:"@;@@ " (fun fmt r -> fprintf fmt "requires %a;" pp_eexpr r) fmt spec.requires;
......
171 247
  fprintf fmt "@]*)";
172 248
  ()
173 249

  
250

  
251
let pp_asserts fmt asserts =
252
  match asserts with 
253
  | _::_ -> (
254
  fprintf fmt "(* Asserts definitions *)@ ";
255
  fprintf_list ~sep:"@ " (fun fmt assert_ -> 
256
    let expr = assert_.assert_expr in
257
    fprintf fmt "assert %a;" pp_expr expr 
258
  ) fmt asserts 
259
  )
260
  | _ -> ()
261
    
174 262
let pp_node fmt nd = 
175
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@]@ @]@.tel@]@."
263
fprintf fmt "@[<v 0>%a%t%s %s (%a) returns (%a)@.%a%alet@.@[<h 2>   @ @[<v>%a@ %a@ %a@]@ @]@.tel@]@."
176 264
  (fun fmt s -> match s with Some s -> pp_spec fmt s | _ -> ()) nd.node_spec
177 265
  (fun fmt -> match nd.node_spec with None -> () | Some _ -> Format.fprintf fmt "@.")
178 266
  (if nd.node_dec_stateless then "function" else "node")
......
193 281
	 (fun fmt d -> fprintf fmt "%a" Dimension.pp_dimension d))
194 282
      checks
195 283
  ) nd.node_checks
284
  (fprintf_list ~sep:"@ " pp_expr_annot) nd.node_annot
196 285
  pp_node_eqs nd.node_eqs
286
  pp_asserts nd.node_asserts
197 287
(*fprintf fmt "@ /* Scheduling: %a */ @ " (fprintf_list ~sep:", " pp_print_string) (Scheduling.schedule_node nd)*)
198 288

  
199 289
let pp_imported_node fmt ind = 

Also available in: Unified diff