Project

General

Profile

« Previous | Next » 

Revision ea8f51ae

Added by Pierre-Loïc Garoche about 6 years ago

Basic library printers moved into backend specific printer files

View differences:

src/backends/C/c_backend_common.ml
108 108
let pp_machine_clear_name fmt id = fprintf fmt "%s_clear" id
109 109
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
110 110

  
111
let pp_basic_lib_fun i pp_val fmt vl =
112
  match i, vl with
113
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
114
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
115
  | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
116
  | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
117
  | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
118
  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
119
  | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
120
  | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
121
  | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
122
  | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
123

  
124

  
111 125
let rec pp_c_dimension fmt dim =
112 126
  match dim.Dimension.dim_desc with
113 127
  | Dimension.Dident id       ->
114
    fprintf fmt "%s" id
128
     fprintf fmt "%s" id
115 129
  | Dimension.Dint i          ->
116
    fprintf fmt "%d" i
130
     fprintf fmt "%d" i
117 131
  | Dimension.Dbool b         ->
118
    fprintf fmt "%B" b
132
     fprintf fmt "%B" b
119 133
  | Dimension.Dite (i, t, e)  ->
120
    fprintf fmt "((%a)?%a:%a)"
134
     fprintf fmt "((%a)?%a:%a)"
121 135
       pp_c_dimension i pp_c_dimension t pp_c_dimension e
122
 | Dimension.Dappl (f, args) ->
123
     fprintf fmt "%a" (Basic_library.pp_c f pp_c_dimension) args
124
 | Dimension.Dlink dim' -> fprintf fmt "%a" pp_c_dimension dim'
125
 | Dimension.Dvar       -> fprintf fmt "_%s" (Utils.name_of_dimension dim.Dimension.dim_id)
126
 | Dimension.Dunivar    -> fprintf fmt "'%s" (Utils.name_of_dimension dim.Dimension.dim_id)
136
  | Dimension.Dappl (f, args) ->
137
     fprintf fmt "%a" (pp_basic_lib_fun f pp_c_dimension) args
138
  | Dimension.Dlink dim' -> fprintf fmt "%a" pp_c_dimension dim'
139
  | Dimension.Dvar       -> fprintf fmt "_%s" (Utils.name_of_dimension dim.Dimension.dim_id)
140
  | Dimension.Dunivar    -> fprintf fmt "'%s" (Utils.name_of_dimension dim.Dimension.dim_id)
127 141

  
128 142
let is_basic_c_type t =
129 143
  Types.is_int_type t || Types.is_real_type t || Types.is_bool_type t
......
190 204
    | Const_struct fl -> fprintf fmt "{%a }" (Utils.fprintf_list ~sep:", " (fun fmt (f, c) -> pp_c_const fmt c)) fl
191 205
    | Const_string _ -> assert false (* string occurs in annotations not in C *)
192 206

  
207
       
193 208
(* Prints a value expression [v], with internal function calls only.
194 209
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
195 210
   but an offset suffix may be added for array variables
......
207 222
    if Types.is_array_type v.var_type && not (Types.is_real_type v.var_type && !Options.mpfr)
208 223
    then fprintf fmt "%a" pp_var v
209 224
    else fprintf fmt "%s->_reg.%a" self pp_var v
210
  | Fun (n, vl)   -> Basic_library.pp_c n (pp_c_val self pp_var) fmt vl
225
  | Fun (n, vl)   -> pp_basic_lib_fun n (pp_c_val self pp_var) fmt vl
211 226

  
212 227
(* Access to the value of a variable:
213 228
   - if it's not a scalar output, then its name is enough
src/backends/C/c_backend_header.ml
55 55
  match v.value_desc with
56 56
  | Cst c         -> pp_c_const fmt c
57 57
  | LocalVar v    -> pp_var fmt v
58
  | Fun (n, vl)   -> Basic_library.pp_c n (print_static_val pp_var) fmt vl
58
  | Fun (n, vl)   -> pp_basic_lib_fun n (print_static_val pp_var) fmt vl
59 59
  | _             -> (Format.eprintf "Internal error: C_backend_header.print_static_val"; assert false)
60 60

  
61 61
let print_constant_decl (m, attr, inst) pp_var fmt v =
src/backends/C/c_backend_src.ml
163 163
    | _           :: q, Power (v, n)  ->
164 164
       pp_value_suffix self var_type q pp_value fmt v
165 165
    | _               , Fun (n, vl)   ->
166
       Basic_library.pp_c n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
166
       pp_basic_lib_fun n (pp_value_suffix self var_type loop_vars pp_value) fmt vl
167 167
    | _               , Access (v, i) ->
168 168
       let var_type = Type_predef.type_array (Dimension.mkdim_var ()) var_type in
169 169
       pp_value_suffix self var_type ((Dimension.mkdim_var (), LAcc i) :: loop_vars) pp_value fmt v
src/backends/Horn/horn_backend_printers.ml
112 112
  |_ -> assert false
113 113

  
114 114

  
115
let pp_basic_lib_fun i pp_val fmt vl =
116
  match i, vl with
117
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
118

  
119
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
120
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
121
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
122
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
123
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
124
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
125
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
126
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
127
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
128
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
129
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
130
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
131
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
132
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
133

  
134
*)
135

  
136

  
115 137
(* Prints a value expression [v], with internal function calls only.
116 138
   [pp_var] is a printer for variables (typically [pp_c_var_read]),
117 139
   but an offset suffix may be added for array variables
......
159 181
     if Types.is_array_type v.var_type
160 182
     then assert false
161 183
     else pp_var fmt (rename_machine self ((if is_lhs then rename_next else rename_current) (* self *) v))
162
  | Fun (n, vl)   -> fprintf fmt "%a" (Basic_library.pp_horn n (pp_horn_val self pp_var)) vl
184
  | Fun (n, vl)   -> fprintf fmt "%a" (pp_basic_lib_fun n (pp_horn_val self pp_var)) vl
163 185

  
164 186
(* Prints a [value] indexed by the suffix list [loop_vars] *)
165 187
let rec pp_value_suffix self pp_value fmt value =
166 188
 match value.value_desc with
167 189
 | Fun (n, vl)  ->
168
   Basic_library.pp_horn n (pp_value_suffix self pp_value) fmt vl
190
   pp_basic_lib_fun n (pp_value_suffix self pp_value) fmt vl
169 191
 |  _            ->
170 192
   pp_horn_val self pp_value fmt value
171 193

  
src/basic_library.ml
146 146
let is_stateless_fun x =
147 147
  List.mem x internal_funs
148 148

  
149
let pp_c i pp_val fmt vl =
150
  match i, vl with
151
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
152
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
153
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
154
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
155
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
156
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
157
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
158
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
159
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
160
    | _ -> (Format.eprintf "internal error: Basic_library.pp_c %s@." i; assert false)
161

  
162
let pp_java i pp_val fmt vl =
163
  match i, vl with
164
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
165
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
166
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
167
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
168
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
169
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
170
    | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
171
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
172
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
173
    | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false)
174

  
175
let pp_horn i pp_val fmt vl =
176
  match i, vl with
177
  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(@[<hov 2>ite %a@ %a@ %a@])" pp_val v1 pp_val v2 pp_val v3
178

  
179
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
180
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
181
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
182
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
183
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
184
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
185
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
186
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
187
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
188
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
189
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
190
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
191
  | _ -> (Format.eprintf "internal error: Basic_library.pp_horn %s@." i; assert false)
192
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
193

  
194
*)
149

  
150
(* let pp_java i pp_val fmt vl = *)
151
(*   match i, vl with *)
152
(*   (\*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *\) *)
153
(*     | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v *)
154
(*     | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v *)
155
(*     | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 *)
156
(*     | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *)
157
(*     | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 *)
158
(*     | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 *)
159
(*     | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2 *)
160
(*     | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 *)
161
(*     | _ -> (Format.eprintf "internal error: Basic_library.pp_java %s@." i; assert false) *)
162

  
195 163

  
196 164
(* Local Variables: *)
197 165
(* compile-command:"make -C .." *)

Also available in: Unified diff