Project

General

Profile

Revision c1adf235 src/basic_library.ml

View differences:

src/basic_library.ml
48 48
      "&&", (static_op type_bin_bool_op);
49 49
      "||", (static_op type_bin_bool_op);
50 50
      "xor", (static_op type_bin_bool_op);
51
      "equi", (static_op type_bin_bool_op);
51 52
      "impl", (static_op type_bin_bool_op);
52 53
      "<", (static_op type_bin_comp_op);
53 54
      "<=", (static_op type_bin_comp_op);
......
67 68
      ["uminus"; "not"] init_env in
68 69
  let env' = 
69 70
    List.fold_right (fun op env -> CE.add_value env op ck_bin_univ)
70
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
71
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
71 72
  env'
72 73

  
73 74
module DE = Env
......
79 80
      ["uminus"; "not"] init_env in
80 81
  let env' = 
81 82
    List.fold_right (fun op env -> DE.add_value env op delay_binary_poly_op)
82
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
83
      ["+"; "-"; "*"; "/"; "mod"; "&&"; "||"; "xor"; "equi"; "impl"; "<"; "<="; ">"; ">="; "!="; "="] env' in
83 84
  let env' = 
84 85
    List.fold_right (fun op env -> DE.add_value env op delay_ternary_poly_op)
85 86
      [] env' in
......
99 100
    "&&", (function [Dbool a; Dbool b] -> Dbool (a&&b)  | _ -> assert false);
100 101
    "||", (function [Dbool a; Dbool b] -> Dbool (a||b)  | _ -> assert false);
101 102
    "xor", (function [Dbool a; Dbool b] -> Dbool (a<>b) | _ -> assert false);
103
    "equi", (function [Dbool a; Dbool b] -> Dbool (a=b) | _ -> assert false);
102 104
    "impl", (function [Dbool a; Dbool b] -> Dbool (a<=b)| _ -> assert false);
103 105
    "<", (function [Dint a; Dint b] -> Dbool (a<b)      | _ -> assert false);
104 106
    ">", (function [Dint a; Dint b] -> Dbool (a>b)      | _ -> assert false);
......
113 115
    VE.initial
114 116
    defs
115 117

  
116
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"]
117

  
118
let homomorphic_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"impl";"uminus";"not"]
118
let internal_funs = ["+";"-";"*";"/";"mod";"&&";"||";"xor";"equi";"impl";"<";">";"<=";">=";"!=";"=";"uminus";"not"]
119 119

  
120 120
let is_internal_fun x =
121 121
  List.mem x internal_funs
122 122

  
123

  
124 123
let pp_c i pp_val fmt vl =
125 124
  match i, vl with
126 125
  (*  | "ite", [v1; v2; v3] -> Format.fprintf fmt "(%a?(%a):(%a))" pp_val v1 pp_val v2 pp_val v3 *)
......
128 127
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
129 128
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
130 129
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
131
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2 
132
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a ^ %a)" pp_val v1 pp_val v2
130
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
131
    | "equi", [v1; v2] -> Format.fprintf fmt "(!%a == !%a)" pp_val v1 pp_val v2
132
    | "xor", [v1; v2] -> Format.fprintf fmt "(!%a != !%a)" pp_val v1 pp_val v2
133 133
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
134 134
    | _ -> failwith i
135 135

  
......
140 140
    | "not", [v] -> Format.fprintf fmt "(!%a)" pp_val v 
141 141
    | "impl", [v1; v2] -> Format.fprintf fmt "(!%a || %a)" pp_val v1 pp_val v2 
142 142
    | "=", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2 
143
    | "mod", [v1; v2] -> Format.fprintf fmt "(%a %% %a)" pp_val v1 pp_val v2
144
    | "equi", [v1; v2] -> Format.fprintf fmt "(%a == %a)" pp_val v1 pp_val v2
145
    | "xor", [v1; v2] -> Format.fprintf fmt "(%a != %a)" pp_val v1 pp_val v2
143 146
    | _, [v1; v2] -> Format.fprintf fmt "(%a %s %a)" pp_val v1 i pp_val v2 
144 147
    | _ -> assert false
145 148

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

Also available in: Unified diff