Project

General

Profile

Revision 7c95dcab src/backends/Horn/horn_backend.ml

View differences:

src/backends/Horn/horn_backend.ml
22 22
let pp_machine_step_name fmt id = fprintf fmt "%s_step" id
23 23
let pp_machine_stateless_name fmt id = fprintf fmt "%s" id
24 24

  
25
let pp_type fmt t =
25
let rec pp_type fmt t =
26 26
  match (Types.repr t).Types.tdesc with
27
  | Types.Tbool           -> Format.fprintf fmt "Bool"
28
  | Types.Tint            -> Format.fprintf fmt "Int"
29
  | Types.Treal           -> Format.fprintf fmt "Real"
30
  | Types.Tclock _
27
  | Types.Tbool           -> fprintf fmt "Bool"
28
  | Types.Tint            -> fprintf fmt "Int"
29
  | Types.Treal           -> fprintf fmt "Real"
30
  | Types.Tconst ty       -> pp_print_string fmt ty
31
  | Types.Tclock t        -> pp_type fmt t
31 32
  | Types.Tarray _
32 33
  | Types.Tstatic _
33
  | Types.Tconst _
34 34
  | Types.Tarrow _
35 35
  | _                     -> Format.eprintf "internal error: pp_type %a@."
36 36
    Types.print_ty t; assert false
......
231 231
    (Utils.pp_final_char_if_non_empty " " static)
232 232
    self inst
233 233

  
234
(* TODO *)
235
let rec pp_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
234

  
235
let rec pp_bool_conditional machines ?(init=false)  (m: machine_t) self fmt c tl el =
236 236
  fprintf fmt "@[<v 2>if (%a) {%t%a@]@,@[<v 2>} else {%t%a@]@,}"
237 237
    (pp_horn_val self (pp_horn_var m)) c
238 238
    (Utils.pp_newline_if_non_empty tl)
239 239
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) tl
240 240
    (Utils.pp_newline_if_non_empty el)
241 241
    (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) el
242

  
242
(* and pp_enum_conditional machines ?(init=false)  (m: machine_t) self fmt g hl = *)
243
(* (\* TODO: check that the enum has all its constructor defined: Xavier how have you handled that, could we have partial definition? *\) *)
244
(*   match hl with *)
245
(*   | [] -> assert false *)
246
(*   | [el] -> Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self) fmt el *)
247
(*   | hd::tl -> *)
248
(*   fprintf fmt "@[<v 2>if (= %a %a) {%t%a@]@,@[<v 2>} else {@.(%a)xxxx@]@,}" *)
249
(*     (pp_horn_val self (pp_horn_var m)) c *)
250
(*     TODOg *)
251
(*     (Utils.pp_newline_if_non_empty tl) *)
252
(*     (Utils.fprintf_list ~sep:"@," (pp_machine_instr machines ~init:init  m self)) hd *)
253
(*     pp_print_newline fmt; *)
254
    
255
    
256
(* fprintf fmt  *)
243 257
and pp_machine_instr machines ?(init=false) (m: machine_t) self fmt instr =
244 258
  match instr with
245 259
  | MReset i ->
......
256 270
    assert false (* This should not happen anymore *)
257 271
  | MStep (il, i, vl) ->
258 272
    pp_instance_call machines ~init:init m self fmt i vl il
259
  | MBranch (g,hl) ->
260
    if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false
261
    then (* boolean case, needs special treatment in C because truth value is not unique *)
262
      (* may disappear if we optimize code by replacing last branch test with default *)
263
      let tl = try List.assoc tag_true  hl with Not_found -> [] in
264
      let el = try List.assoc tag_false hl with Not_found -> [] in
265
      pp_conditional machines ~init:init m self fmt g tl el
266
    else assert false (* enum type case *)
273
  | MBranch (g,hl) -> (* should not be produced *)
274
    assert false
275

  
276
    (* if hl <> [] && let t = fst (List.hd hl) in t = tag_true || t = tag_false *)
277
    (* then (\* boolean case, needs special treatment in C because truth value is not unique *\) *)
278
    (*   (\* may disappear if we optimize code by replacing last branch test with default *\) *)
279
    (*   let tl = try List.assoc tag_true  hl with Not_found -> [] in *)
280
    (*   let el = try List.assoc tag_false hl with Not_found -> [] in *)
281
    (*   pp_bool_conditional machines ~init:init m self fmt g tl el *)
282
    (* else (\* enum type case *\) *)
283

  
284
    (*   pp_enum_conditional machines ~init:init m self fmt g hl  *)
267 285

  
268 286

  
269 287
(**************************************************************)
......
520 538
      get_cex machines fmt node machine)
521 539
end
522 540

  
541
let print_type_definitions fmt =
542
  let cpt_type = ref 0 in
543
  Hashtbl.iter (fun typ decl ->
544
		match typ with
545
		| Tydec_const var ->
546
		   (match decl.top_decl_desc with
547
		    | TypeDef tdef -> (
548
		      match tdef.tydef_desc with
549
		      | Tydec_enum tl ->
550
			incr cpt_type;
551
			fprintf fmt "(declare-datatypes () ((%s %a));@.@."
552
			  var
553
			  (Utils.fprintf_list ~sep:" " pp_print_string) tl
554
		      | _ -> assert false
555
		    )
556
		    | _ -> assert false
557
		   )
558
		| _        -> ()) type_table
559

  
523 560

  
524 561
let translate fmt basename prog machines =
562
  (* We print typedef *)
563
  print_type_definitions fmt;
564

  
525 565
  List.iter (print_machine machines fmt) (List.rev machines);
526 566
  main_print machines fmt
527 567

  

Also available in: Unified diff