module type EqualityIndex =
sig
- module PosEqSet : Set.S with type elt = Utils.pos * Inference.equality
+ module PosEqSet : Set.S with type elt = Utils.pos * Equality.equality
val arities : (Cic.term, int) Hashtbl.t
type key = Cic.term
type t = Discrimination_tree.DiscriminationTreeIndexing(PosEqSet).t
val retrieve_generalizations : t -> key -> PosEqSet.t
val retrieve_unifiables : t -> key -> PosEqSet.t
val init_index : unit -> unit
- val remove_index : t -> Inference.equality -> t
- val index : t -> Inference.equality -> t
- val in_index : t -> Inference.equality -> bool
+ val remove_index : t -> Equality.equality -> t
+ val index : t -> Equality.equality -> t
+ val in_index : t -> Equality.equality -> bool
end
module DT =
struct
module OrderedPosEquality = struct
- type t = Utils.pos * Inference.equality
- let compare = Pervasives.compare
+ type t = Utils.pos * Equality.equality
+ let compare (p1,e1) (p2,e2) =
+ let rc = Pervasives.compare p1 p2 in
+ if rc = 0 then Equality.compare e1 e2 else rc
end
module PosEqSet = Set.Make(OrderedPosEquality);;
;;
let remove_index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
match ordering with
| Utils.Gt -> remove_index tree l (Utils.Left, equality)
| Utils.Lt -> remove_index tree r (Utils.Right, equality)
remove_index tree l (Utils.Left, equality)
let index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
match ordering with
| Utils.Gt -> index tree l (Utils.Left, equality)
| Utils.Lt -> index tree r (Utils.Right, equality)
let in_index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
let meta_convertibility (pos,equality') =
- Inference.meta_convertibility_eq equality equality'
+ Equality.meta_convertibility_eq equality equality'
in
in_index tree l meta_convertibility || in_index tree r meta_convertibility
module PT =
struct
module OrderedPosEquality = struct
- type t = Utils.pos * Inference.equality
- let compare = Pervasives.compare
+ type t = Utils.pos * Equality.equality
+ let compare (p1,e1) (p2,e2) =
+ let rc = Pervasives.compare p1 p2 in
+ if rc = 0 then Equality.compare e1 e2 else rc
end
module PosEqSet = Set.Make(OrderedPosEquality);;
;;
let remove_index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
match ordering with
| Utils.Gt -> remove_index tree l (Utils.Left, equality)
| Utils.Lt -> remove_index tree r (Utils.Right, equality)
remove_index tree l (Utils.Left, equality)
let index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
match ordering with
| Utils.Gt -> index tree l (Utils.Left, equality)
| Utils.Lt -> index tree r (Utils.Right, equality)
let in_index tree equality =
- let _, _, (_, l, r, ordering), _ = equality in
+ let _, _, (_, l, r, ordering), _,_ = Equality.open_equality equality in
let meta_convertibility (pos,equality') =
- Inference.meta_convertibility_eq equality equality'
+ Equality.meta_convertibility_eq equality equality'
in
in_index tree l meta_convertibility || in_index tree r meta_convertibility
end