Project

General

Profile

Revision e057dd08 src/backends/Horn/horn_backend_printers.ml

View differences:

src/backends/Horn/horn_backend_printers.ml
49 49
let rec get_type_cst c =
50 50
  match c with
51 51
  | Const_int(n) -> new_ty Tint
52
  | Const_real(x) -> new_ty Treal
53
  | Const_float(f) -> new_ty Treal
52
  | Const_real _ -> new_ty Treal
53
  (* | Const_float _ -> new_ty Treal *)
54 54
  | Const_array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type_cst (List.hd l)))
55 55
  | Const_tag(tag) -> new_ty Tbool
56 56
  | Const_string(str) ->  assert false(* used only for annotations *)
57 57
  | Const_struct(l) -> new_ty (Tstruct(List.map (fun (label, t) -> (label, get_type_cst t)) l))
58 58

  
59
let rec get_type v = 
59
let rec get_type v =
60 60
  match v with
61
  | Cst c -> get_type_cst c             
61
  | Cst c -> get_type_cst c
62 62
  | Access(tab, index) -> begin
63
                           let rec remove_link ltype = match (dynamic_type ltype).tdesc with 
64
                             | Tlink t -> t
65
                             | _ -> ltype
66
                           in
67
                            match (dynamic_type (remove_link (get_type tab))).tdesc with
68
                            | Tarray(size, t) -> remove_link t
69
                            | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
70
                            | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
71
                            | _ -> Format.eprintf "Type of access is not an array "; assert false
63
      let rec remove_link ltype =
64
        match (dynamic_type ltype).tdesc with
65
        | Tlink t -> t
66
        | _ -> ltype
67
      in
68
      match (dynamic_type (remove_link (get_type tab))).tdesc with
69
      | Tarray(size, t) -> remove_link t
70
      | Tvar -> Format.eprintf "Type of access is a variable... "; assert false
71
      | Tunivar -> Format.eprintf "Type of access is a variable... "; assert false
72
      | _ -> Format.eprintf "Type of access is not an array "; assert false
72 73
                          end
73 74
  | Power(v, n) -> assert false
74 75
  | LocalVar v -> v.var_type
75 76
  | StateVar v -> v.var_type
76 77
  | Fun(n, vl) -> begin match n with
77
                  | "+" 
78
                  | "-" 
78
                  | "+"
79
                  | "-"
79 80
                  | "*" -> get_type (List.hd vl)
80 81
                  | _ -> Format.eprintf "Function undealt with : %s" n ;assert false
81 82
                  end
82
  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int (Location.dummy_loc) (List.length l), get_type (List.hd l)))
83
  | Array(l) -> new_ty (Tarray(Dimension.mkdim_int
84
                                 (Location.dummy_loc)
85
                                 (List.length l),
86
                               get_type (List.hd l)))
83 87
  | _ -> assert false
84 88

  
85 89

  
......
116 120
                              let rec print tab x =
117 121
                                match tab with
118 122
                                | [] -> default_val fmt (get_type v)(*fprintf fmt "YAY"*)
119
                                | h::t -> fprintf fmt "(store "; print t (x+1); fprintf fmt " %i " x; pp_horn_val ~is_lhs:is_lhs self pp_var fmt h; fprintf fmt ")" 
123
                                | h::t -> fprintf fmt "(store "; print t (x+1); fprintf fmt " %i " x; pp_horn_val ~is_lhs:is_lhs self pp_var fmt h; fprintf fmt ")"
120 124
                              in
121 125
                              print initlist 0
122 126
    | Access(tab,index)      -> fprintf fmt "(select "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt tab; fprintf fmt " "; pp_horn_val ~is_lhs:is_lhs self pp_var fmt index; fprintf fmt ")"
......
458 462

  
459 463

  
460 464
let mk_flags arity =
461
 let b_range =
465
  let b_range =
462 466
   let rec range i j =
463 467
     if i > arity then [] else i :: (range (i+1) j) in
464 468
   range 2 arity;

Also available in: Unified diff