Project

General

Profile

« Previous | Next » 

Revision 58272238

Added by Teme Kahsai almost 10 years ago

modifed / to div in horn backend

View differences:

src/basic_library.ml
23 23
  type_static (mkdim_var ()) ty
24 24

  
25 25
let type_env =
26
  List.fold_left 
26
  List.fold_left
27 27
    (fun env (op, op_type) -> TE.add_value env op op_type)
28 28
    TE.initial
29 29
    [
30 30
      "true", (static_op type_bool);
31 31
      "false", (static_op type_bool);
32 32
      "+", (static_op type_bin_poly_op);
33
      "uminus", (static_op type_unary_poly_op); 
34
      "-", (static_op type_bin_poly_op); 
33
      "uminus", (static_op type_unary_poly_op);
34
      "-", (static_op type_bin_poly_op);
35 35
      "*", (static_op type_bin_poly_op);
36 36
      "/", (static_op type_bin_poly_op);
37 37
      "mod", (static_op type_bin_int_op);
......
48 48
      "=", (static_op type_bin_comp_op);
49 49
      "not", (static_op type_unary_bool_op)
50 50
]
51
 
51

  
52 52
module CE = Env
53 53

  
54 54
let clock_env =
......
56 56
  let env' =
57 57
    List.fold_right (fun op env -> CE.add_value env op ck_nullary_univ)
58 58
      ["true"; "false"] init_env in
59
  let env' = 
59
  let env' =
60 60
    List.fold_right (fun op env -> CE.add_value env op ck_unary_univ)
61 61
      ["uminus"; "not"] env' in
62
  let env' = 
62
  let env' =
63 63
    List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
64 64
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
65 65
  env'
......
74 74
  let env' =
75 75
    List.fold_right (fun op env -> DE.add_value env op delay_unary_poly_op)
76 76
      ["uminus"; "not"] env' in
77
  let env' = 
77
  let env' =
78 78
    List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
79 79
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
80
  let env' = 
80
  let env' =
81 81
    List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op)
82 82
      [] env' in
83 83
  env'
......
85 85
module VE = Env
86 86

  
87 87
let eval_env =
88
  let defs = [ 
88
  let defs = [
89 89
    "uminus", (function [Dint a] -> Dint (-a)           | _ -> assert false);
90 90
    "not", (function [Dbool b] -> Dbool (not b)         | _ -> assert false);
91 91
    "+", (function [Dint a; Dint b] -> Dint (a+b)       | _ -> assert false);
......
106 106
    "=", (function [a; b] -> Dbool (a=b)                | _ -> assert false);
107 107
  ]
108 108
  in
109
  List.fold_left 
109
  List.fold_left
110 110
    (fun env (op, op_eval) -> VE.add_value env op op_eval)
111 111
    VE.initial
112 112
    defs
......
120 120
  match i, vl with
121 121
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
122 122
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
123
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
124
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
125
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
123
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
124
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
125
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
126 126
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
127 127
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
128 128
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
129
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
129
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
130 130
    | _ -> failwith i
131 131

  
132 132
let pp_java i pp_val fmt vl =
133 133
  match i, vl with
134 134
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
135 135
    | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
136
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
137
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
138
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
136
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v
137
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2
138
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
139 139
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
140 140
    | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
141 141
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
142
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
142
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2
143 143
    | _ -> assert false
144 144

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

  
148 149
  | "uminus", [v] -> Format.fprintf fmt "(- %a)" pp_val v
149
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v 
150
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2 
151
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2 
152
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2 
153
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2 
150
  | "not", [v] -> Format.fprintf fmt "(not %a)" pp_val v
151
  | "=", [v1; v2] -> Format.fprintf fmt "(= %a %a)" pp_val v1 pp_val v2
152
  | "&&", [v1; v2] -> Format.fprintf fmt "(and %a %a)" pp_val v1 pp_val v2
153
  | "||", [v1; v2] -> Format.fprintf fmt "(or %a %a)" pp_val v1 pp_val v2
154
  | "impl", [v1; v2] -> Format.fprintf fmt "(=> %a %a)" pp_val v1 pp_val v2
154 155
  | "mod", [v1; v2] -> Format.fprintf fmt "(mod %a %a)" pp_val v1 pp_val v2
155 156
  | "equi", [v1; v2] -> Format.fprintf fmt "(%a = %a)" pp_val v1 pp_val v2
156 157
  | "xor", [v1; v2] -> Format.fprintf fmt "(%a xor %a)" pp_val v1 pp_val v2
157
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2 
158
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2 
158
  | "!=", [v1; v2] -> Format.fprintf fmt "(not (= %a %a))" pp_val v1 pp_val v2
159
  | "/", [v1; v2] -> Format.fprintf fmt "(div %a %a)" pp_val v1 pp_val v2
160
  | _, [v1; v2] -> Format.fprintf fmt "(%s %a %a)" i pp_val v1 pp_val v2
159 161
  | _ -> assert false
160
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
161
  
162
(*  | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
163

  
162 164
*)
163 165

  
164 166
(* Local Variables: *)

Also available in: Unified diff