Commit f495d946 authored by Andrei Paskevich's avatar Andrei Paskevich

ban the physical equality from everywhere

parent 8b97535c
......@@ -93,7 +93,7 @@ let rec unify t1 t2 = match t1, t2 with
not (occurs v t) && (v.type_val <- Some t; true)
(* recursive types *)
| Tyapp (s1, l1), Tyapp (s2, l2) ->
s1 == s2 && List.length l1 = List.length l2 &&
ts_equal s1 s2 && List.length l1 = List.length l2 &&
List.for_all2 unify l1 l2
| Tyapp _, _ | _, Tyapp _ ->
false
......
......@@ -88,7 +88,7 @@ let rec print_ty drv fmt ty = match ty.ty_node with
(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
let rec lookup v ty = match ty.ty_node with
| Tyvar u when u == v -> true
| Tyvar u when tv_equal u v -> true
| _ -> ty_any (lookup v) ty
in
let lookup v = List.exists (lookup v) fs.ls_args in
......
......@@ -99,7 +99,7 @@ and print_tyapp drv fmt = function
(* can the type of a value be derived from the type of the arguments? *)
let unambig_fs fs =
let rec lookup v ty = match ty.ty_node with
| Tyvar u when u == v -> true
| Tyvar u when tv_equal u v -> true
| _ -> ty_any (lookup v) ty
in
let lookup v = List.exists (lookup v) fs.ls_args in
......
......@@ -114,7 +114,7 @@ and expr_desc env loc = function
let e1 = dexpr env e1 in
let e2 = dexpr env e2 in
begin match e1.dexpr_type with
| Tyapp (ts, [ty2; ty]) when ts == env.ts_arrow ->
| Tyapp (ts, [ty2; ty]) when Ty.ts_equal ts env.ts_arrow ->
expected_type e2 ty2;
DEapply (e1, e2), ty
| _ ->
......
......@@ -144,7 +144,7 @@ and rewriteF kn state av sign f = match f.f_node with
(rewriteF kn state Svs.empty sign) tr in
let av = List.fold_left (fun s v -> Svs.add v s) av vl in
let f1' = rewriteF kn state av sign f1 in
if f1' == f1 && trl_equal tr' tr then f else f_quant q vl tr' f1'
if f_equal f1' f1 && trl_equal tr' tr then f else f_quant q vl tr' f1'
| Fbinop (o, _, _) when (o = Fand && sign) || (o = For && not sign) ->
f_map_sign (rewriteT kn state) (rewriteF kn state av) sign f
| Flet (t1, _) ->
......
......@@ -28,7 +28,7 @@ let rec elim_t letl contT t = match t.t_node with
| Tlet (t1,tb) ->
let u,t2 = t_open_bound tb in
let t_let e1 e2 =
if e1 == t1 && e2 == t2 then t else t_let u e1 e2
if t_equal e1 t1 && t_equal e2 t2 then t else t_let u e1 e2
in
let cont_in t1 t2 = contT (t_let t1 t2) in
let cont_let t1 = elim_t ((u,t1)::letl) (cont_in t1) t2 in
......
......@@ -89,7 +89,7 @@ let load_prelude query env =
let th_uc = create_theory (id_fresh ("encoding_decorate_for_"^name)) in
let th_uc = Theory.use_export th_uc prelude in
let th_uc =
if ts == ts_int || ts = ts_real then th_uc
if ts_equal ts ts_int || ts_equal ts ts_real then th_uc
else Theory.add_ty_decl th_uc [ts,Tabstract] in
let ty = ty_app ts [] in
let add_fsymbol fs th_uc =
......@@ -123,7 +123,7 @@ let load_prelude query env =
let is_kept tenv ts =
ts.ts_args = [] &&
begin
ts == ts_int || ts == ts_real (* for the constant *)
ts_equal ts ts_int || ts_equal ts ts_real (* for the constant *)
|| match tenv.query with
| None -> true (* every_simple *)
| Some query ->
......@@ -165,13 +165,13 @@ let conv_ty_pos tenv ty =
(* Convert a logic symbols to the encoded one *)
let conv_ls tenv ls =
if ls == ps_equ
if ls_equal ls ps_equ
then ls
else
let tyl = List.map (conv_ty_neg tenv) ls.ls_args in
let ty_res = Util.option_map (conv_ty_pos tenv) ls.ls_value in
if Util.option_eq (==) ty_res ls.ls_value
&& List.for_all2 (==) tyl ls.ls_args
if Util.option_eq ty_equal ty_res ls.ls_value
&& List.for_all2 ty_equal tyl ls.ls_args
then ls
else
let preid = id_clone ls.ls_name in
......@@ -187,14 +187,14 @@ let conv_ts tenv ts =
specials if needed*)
let conv_arg tenv tvar t ty =
let tty = t.t_ty in
if tty == ty then t else
if ty == tenv.deco then
if ty_equal tty ty then t else
if ty_equal ty tenv.deco then
let tylconv = Hty.find tenv.specials tty in
let t = (t_app tylconv.t2u [t] tenv.undeco) in
sort_app tenv tvar t tty
else (* tty is tenv.deco *)
begin
assert (tty == tenv.deco);
assert (ty_equal tty tenv.deco);
let tylconv = Hty.find tenv.specials ty in
t_app tylconv.d2t [t] ty
end
......@@ -202,9 +202,9 @@ let conv_arg tenv tvar t ty =
(* Convert to undeco or to a specials an application *)
let conv_res_app tenv tvar p tl ty =
let tty = Util.of_option p.ls_value in
if tty == ty then t_app p tl tty else
if ty_equal tty ty then t_app p tl tty else
begin
assert (tty == tenv.undeco);
assert (ty_equal tty tenv.undeco);
let t = t_app p tl tenv.undeco in
sort_app tenv tvar t ty
end
......@@ -212,7 +212,7 @@ let conv_res_app tenv tvar p tl ty =
let conv_vs tenv tvar (vsvar,acc) vs =
let tres,vsres =
let ty_res = conv_ty_pos tenv vs.vs_ty in
if ty_res == vs.vs_ty then
if ty_equal ty_res vs.vs_ty then
t_var vs,vs
else
let tty = term_of_ty tenv tvar vs.vs_ty in
......@@ -239,7 +239,7 @@ let rec rewrite_term tenv tvar vsvar t =
let (vsvar,u) = conv_vs tenv tvar (vsvar,[]) u in
let u = List.hd u in
let t1' = fnT vsvar t1 in let t2' = fnT vsvar t2 in
if t1' == t1 && t2' == t2 then t else t_let u t1' t2'
if t_equal t1' t1 && t_equal t2' t2 then t else t_let u t1' t2'
| Tcase _ | Teps _ | Tbvar _ ->
Register.unsupportedTerm t
"Encoding decorate : I can't encode this term"
......@@ -248,7 +248,7 @@ and rewrite_fmla tenv tvar vsvar f =
let fnT = rewrite_term tenv tvar vsvar in
let fnF = rewrite_fmla tenv tvar in
match f.f_node with
| Fapp(p, tl) when p == ps_equ ->
| Fapp(p, tl) when ls_equal p ps_equ ->
let tl = List.map fnT tl in
begin
match tl with
......@@ -270,7 +270,7 @@ and rewrite_fmla tenv tvar vsvar f =
let (vsvar,vl) = List.fold_left (conv_vs tenv tvar) (vsvar,[]) vl in
let f1' = fnF vsvar f1 in
let tl' = [] (* TODO *) in
if f1' == f1 (*&& tr_equal tl' tl*) then f
if f_equal f1' f1 (*&& tr_equal tl' tl*) then f
else
let vl = List.rev vl in
f_quant q vl tl' f1'
......@@ -278,7 +278,7 @@ and rewrite_fmla tenv tvar vsvar f =
let (vsvar,u) = conv_vs tenv tvar (vsvar,[]) u in
let u = List.hd u in
let t1' = fnT t1 in let f2' = fnF vsvar f2 in
if t1' == t1 && f2' == f2 then f else f_let u t1' f2'
if t_equal t1' t1 && f_equal f2' f2 then f else f_let u t1' f2'
| _ -> f_map fnT (fnF vsvar) f
let decl (tenv:tenv) d =
......
......@@ -75,13 +75,13 @@ let fold isnotinlinedt isnotinlinedf d (env, task) =
match e with
| Term t ->
let t = replacet env t in
if isnotinlinedt t || t_s_any ffalse ((==) ls) t
if isnotinlinedt t || t_s_any ffalse (ls_equal ls) t
then env, add_decl task
(create_logic_decl [make_fs_defn ls vs t])
else {env with fs = Mls.add ls (vs,t) env.fs},task
| Fmla f ->
let f = replacep env f in
if isnotinlinedf f || f_s_any ffalse ((==) ls) f
if isnotinlinedf f || f_s_any ffalse (ls_equal ls) f
then env, add_decl task
(create_logic_decl [make_ps_defn ls vs f])
else {env with ps = Mls.add ls (vs,f) env.ps},task
......
......@@ -58,11 +58,11 @@ let list_apply f = List.fold_left (fun acc x -> List.rev_append (f x) acc) []
let list_fold_product f acc l1 l2 =
List.fold_left
List.fold_left
(fun acc e1 ->
List.fold_left
(fun acc e2 -> f acc e1 e2)
acc l2)
List.fold_left
(fun acc e2 -> f acc e1 e2)
acc l2)
acc l1
let list_fold_product_l f acc ll =
......@@ -88,13 +88,13 @@ let ffalse _ = false
module Sstr = Set.Make(String)
module Mstr = Map.Make(String)
(* Set, Map, Hashtbl on structures with a unique tag and physical equality *)
(* Set, Map, Hashtbl on structures with a unique tag *)
module OrderedHash (X : Hashweak.Tagged) =
struct
type t = X.t
let equal = (==)
let hash = X.tag
let equal ts1 ts2 = X.tag ts1 == X.tag ts2
let compare ts1 ts2 = Pervasives.compare (X.tag ts1) (X.tag ts2)
end
......
......@@ -17,7 +17,7 @@
(* *)
(**************************************************************************)
(** Useful functions *)
(** Useful functions *)
(* useful option combinators *)
......@@ -45,19 +45,19 @@ val map_join_left : ('a -> 'b) -> ('b -> 'b -> 'b) -> 'a list -> 'b
val list_apply : ('a -> 'b list) -> 'a list -> 'b list
val list_fold_product :
val list_fold_product :
('a -> 'b -> 'c -> 'a) -> 'a -> 'b list -> 'c list -> 'a
(** [list_fold_product f acc l1 l2] apply the function [f] with the
accumulator [acc] on all the pair of elements of [l1] and [l2]
tail-reccursive
*)
val list_fold_product_l :
val list_fold_product_l :
('a -> 'b list -> 'a) -> 'a -> 'b list list -> 'a
(** generalisation of {! list_fold_product}
(** generalisation of {! list_fold_product}
not tail-reccursive
*)
(* boolean fold accumulators *)
exception FoldSkip
......@@ -75,14 +75,14 @@ val ttrue : 'a -> bool
module Sstr : Set.S with type elt = string
module Mstr : Map.S with type key = string
(* Set, Map, Hashtbl on structures with a unique tag and physical equality *)
(* Set, Map, Hashtbl on structures with a unique tag *)
open Hashweak
module OrderedHash (X : Tagged) :
sig
type t = X.t
val equal : t -> t -> bool
val hash : t -> int
val equal : t -> t -> bool
val compare : t -> t -> int
end
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment