Move the dubious compare and hash functions from Constr to a Termops submodule

dev/ci/user-overlays/21863-ppedrot-constr-type-as-first-order-data.sh

@@ -0,0 +1,11 @@
+overlay aac_tactics https://github.com/ppedrot/aac-tactics constr-type-as-first-order-data 21863
+
+overlay equations https://github.com/ppedrot/Coq-Equations constr-type-as-first-order-data 21863
+
+overlay mtac2 https://github.com/ppedrot/Mtac2 constr-type-as-first-order-data 21863
+
+overlay smtcoq https://github.com/ppedrot/smtcoq constr-type-as-first-order-data 21863
+
+overlay stalmarck https://github.com/ppedrot/stalmarck constr-type-as-first-order-data 21863
+
+overlay itauto https://gitlab.inria.fr/pedrot/itauto constr-type-as-first-order-data 21863

engine/termops.ml

@@ -1282,3 +1282,153 @@ let env_rel_context_chop k env =
   let ctx1,ctx2 = List.chop k rels in
   push_rel_context ctx2 (reset_with_named_context (named_context_val env) env),
   ctx1
+
+(** Terms as a datatype *)
+
+module ConstrData =
+struct
+
+open Constr
+
+type t = Constr.t
+
+let compare_invert f iv1 iv2 =
+  match iv1, iv2 with
+  | NoInvert, NoInvert -> 0
+  | NoInvert, CaseInvert _ -> -1
+  | CaseInvert _, NoInvert -> 1
+  | CaseInvert iv1, CaseInvert iv2 ->
+    Array.compare f iv1.indices iv2.indices
+
+let constr_ord_int f t1 t2 =
+  let open! Compare in
+  let fix_cmp (a1, i1) (a2, i2) =
+    compare [(Array.compare Int.compare,a1,a2); (Int.compare,i1,i2)]
+  in
+  let ctx_cmp f (_n1, p1) (_n2, p2) = f p1 p2 in
+  match kind t1, kind t2 with
+    | Cast (c1,_,_), _ -> f c1 t2
+    | _, Cast (c2,_,_) -> f t1 c2
+    (* Why this special case? *)
+    | App (c1,l1), _ when isCast c1 -> let c1 = pi1 (destCast c1) in f (mkApp (c1,l1)) t2
+    | _, App (c2,l2) when isCast c2 -> let c2 = pi1 (destCast c2) in f t1 (mkApp (c2,l2))
+    | Rel n1, Rel n2 -> Int.compare n1 n2
+    | Rel _, _ -> -1 | _, Rel _ -> 1
+    | Var id1, Var id2 -> Id.compare id1 id2
+    | Var _, _ -> -1 | _, Var _ -> 1
+    | Meta m1, Meta m2 -> Int.compare m1 m2
+    | Meta _, _ -> -1 | _, Meta _ -> 1
+    | Evar (e1,l1), Evar (e2,l2) ->
+      compare [(Evar.compare, e1, e2); (SList.compare f, l1, l2)]
+    | Evar _, _ -> -1 | _, Evar _ -> 1
+    | Sort s1, Sort s2 -> Sorts.compare s1 s2
+    | Sort _, _ -> -1 | _, Sort _ -> 1
+    | Prod (_,t1,c1), Prod (_,t2,c2)
+    | Lambda (_,t1,c1), Lambda (_,t2,c2) -> compare [(f,t1,t2); (f,c1,c2)]
+    | Prod _, _ -> -1 | _, Prod _ -> 1
+    | Lambda _, _ -> -1 | _, Lambda _ -> 1
+    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> compare [(f,b1,b2); (f,t1,t2); (f,c1,c2)]
+    | LetIn _, _ -> -1 | _, LetIn _ -> 1
+    | App (c1,l1), App (c2,l2) -> compare [(f,c1,c2); (Array.compare f, l1, l2)]
+    | App _, _ -> -1 | _, App _ -> 1
+    | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2
+    | Const _, _ -> -1 | _, Const _ -> 1
+    | Ind (ind1, _u1), Ind (ind2, _u2) -> Ind.CanOrd.compare ind1 ind2
+    | Ind _, _ -> -1 | _, Ind _ -> 1
+    | Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2
+    | Construct _, _ -> -1 | _, Construct _ -> 1
+    | Case (_,_u1,pms1,(p1,_r1),iv1,c1,bl1), Case (_,_u2,pms2,(p2,_r2),iv2,c2,bl2) ->
+      compare [
+        (Array.compare f, pms1, pms2);
+        (ctx_cmp f, p1, p2);
+        (compare_invert f, iv1, iv2);
+        (f, c1, c2);
+        (Array.compare (ctx_cmp f), bl1, bl2);
+      ]
+    | Case _, _ -> -1 | _, Case _ -> 1
+    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
+      compare [(fix_cmp, ln1, ln2); (Array.compare f, tl1, tl2); (Array.compare f, bl1, bl2)]
+    | Fix _, _ -> -1 | _, Fix _ -> 1
+    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
+      compare [(Int.compare, ln1, ln2); (Array.compare f, tl1, tl2); (Array.compare f, bl1, bl2)]
+    | CoFix _, _ -> -1 | _, CoFix _ -> 1
+    | Proj (p1,_r1,c1), Proj (p2,_r2,c2) -> compare [(Projection.CanOrd.compare, p1, p2); (f, c1, c2)]
+    | Proj _, _ -> -1 | _, Proj _ -> 1
+    | Int i1, Int i2 -> Uint63.compare i1 i2
+    | Int _, _ -> -1 | _, Int _ -> 1
+    | Float f1, Float f2 -> Float64.total_compare f1 f2
+    | Float _, _ -> -1 | _, Float _ -> 1
+    | String s1, String s2 -> Pstring.compare s1 s2
+    | String _, _ -> -1 | _, String _ -> 1
+    | Array(_u1,t1,def1,ty1), Array(_u2,t2,def2,ty2) ->
+      compare [(Array.compare f, t1, t2); (f, def1, def2); (f, ty1, ty2)]
+    (*| Array _, _ -> -1 | _, Array _ -> 1*)
+
+let rec compare m n =
+  constr_ord_int compare m n
+
+let equal m n = Int.equal (compare m n) 0
+
+(* Exported hashing fonction on constr, used mainly in plugins. *)
+
+open UVars
+open Hashset.Combine
+
+let rec hash t =
+  match kind t with
+    | Var i -> combinesmall 1 (Id.hash i)
+    | Sort s -> combinesmall 2 (Sorts.hash s)
+    | Cast (c, k, t) ->
+      let hc = hash c in
+      let ht = hash t in
+      combinesmall 3 (combine3 hc (hash_cast_kind k) ht)
+    | Prod (_, t, c) -> combinesmall 4 (combine (hash t) (hash c))
+    | Lambda (_, t, c) -> combinesmall 5 (combine (hash t) (hash c))
+    | LetIn (_, b, t, c) ->
+      combinesmall 6 (combine3 (hash b) (hash t) (hash c))
+    | App (c,l) -> begin match kind c with
+        | Cast (c, _, _) -> hash (mkApp (c,l)) (* WTF *)
+        | _ -> combinesmall 7 (combine (hash_term_array l) (hash c))
+      end
+    | Evar (e,l) ->
+      combinesmall 8 (combine (Evar.hash e) (hash_term_list l))
+    | Const (c,u) ->
+      combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u))
+    | Ind (ind,u) ->
+      combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u))
+    | Construct (c,u) ->
+      combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u))
+    | Case (_ , u, pms, (p,r), iv, c, bl) ->
+      combinesmall 12 (combine5 (hash c) (hash_invert iv) (hash_term_array pms) (Instance.hash u)
+                         (combine3 (hash_under_context p) (Sorts.relevance_hash r) (hash_branches bl)))
+    | Fix (_ln ,(_, tl, bl)) ->
+      combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
+    | CoFix(_ln, (_, tl, bl)) ->
+       combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl))
+    | Meta n -> combinesmall 15 n
+    | Rel n -> combinesmall 16 n
+    | Proj (p,r, c) ->
+      combinesmall 17 (combine3 (Projection.CanOrd.hash p) (Sorts.relevance_hash r) (hash c))
+    | Int i -> combinesmall 18 (Uint63.hash i)
+    | Float f -> combinesmall 19 (Float64.hash f)
+    | String s -> combinesmall 20 (Pstring.hash s)
+    | Array(u,t,def,ty) ->
+      combinesmall 21 (combine4 (Instance.hash u) (hash_term_array t) (hash def) (hash ty))
+
+and hash_invert = function
+  | NoInvert -> 0
+  | CaseInvert {indices;} ->
+    combinesmall 1 (hash_term_array indices)
+
+and hash_term_array t =
+  Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
+
+and hash_term_list t =
+  SList.Skip.fold (fun acc t -> combine (hash t) acc) 0 t
+
+and hash_under_context (_, t) = hash t
+
+and hash_branches bl =
+  Array.fold_left (fun acc t -> combine acc (hash_under_context t)) 0 bl
+
+end

engine/termops.mli

@@ -239,6 +239,16 @@ val pr_evd_qglobal : evar_map -> Sorts.QGlobal.t -> Pp.t
 val pr_evd_qvar : evar_map -> Sorts.QVar.t -> Pp.t
 val pr_evd_quality : evar_map -> Sorts.Quality.t -> Pp.t
 
+(* Treat terms as a concrete data type with an otherwise unspecified
+   representation. You should be wary about the lack of invariants of this API. *)
+module ConstrData :
+sig
+type t = Constr.t
+val compare : t -> t -> int
+val equal : t -> t -> bool
+val hash : t -> int
+end
+
 module Internal : sig
 
 (** NOTE: to print terms you always want to use functions in

kernel/constr.ml

@@ -1012,81 +1012,6 @@ let leq_constr_univs univs m n =
 let rec eq_constr_nounivs m n =
   (m == n) || compare_head_gen (fun _ _ _ -> true) (fun _ _ -> true) (eq_existential eq_constr_nounivs) (fun _ -> eq_constr_nounivs) 0 m n
 
-let compare_invert f iv1 iv2 =
-  match iv1, iv2 with
-  | NoInvert, NoInvert -> 0
-  | NoInvert, CaseInvert _ -> -1
-  | CaseInvert _, NoInvert -> 1
-  | CaseInvert iv1, CaseInvert iv2 ->
-    Array.compare f iv1.indices iv2.indices
-
-let constr_ord_int f t1 t2 =
-  let open! Compare in
-  let fix_cmp (a1, i1) (a2, i2) =
-    compare [(Array.compare Int.compare,a1,a2); (Int.compare,i1,i2)]
-  in
-  let ctx_cmp f (_n1, p1) (_n2, p2) = f p1 p2 in
-  match kind t1, kind t2 with
-    | Cast (c1,_,_), _ -> f c1 t2
-    | _, Cast (c2,_,_) -> f t1 c2
-    (* Why this special case? *)
-    | App (c1,l1), _ when isCast c1 -> let c1 = pi1 (destCast c1) in f (mkApp (c1,l1)) t2
-    | _, App (c2,l2) when isCast c2 -> let c2 = pi1 (destCast c2) in f t1 (mkApp (c2,l2))
-    | Rel n1, Rel n2 -> Int.compare n1 n2
-    | Rel _, _ -> -1 | _, Rel _ -> 1
-    | Var id1, Var id2 -> Id.compare id1 id2
-    | Var _, _ -> -1 | _, Var _ -> 1
-    | Meta m1, Meta m2 -> Int.compare m1 m2
-    | Meta _, _ -> -1 | _, Meta _ -> 1
-    | Evar (e1,l1), Evar (e2,l2) ->
-      compare [(Evar.compare, e1, e2); (SList.compare f, l1, l2)]
-    | Evar _, _ -> -1 | _, Evar _ -> 1
-    | Sort s1, Sort s2 -> Sorts.compare s1 s2
-    | Sort _, _ -> -1 | _, Sort _ -> 1
-    | Prod (_,t1,c1), Prod (_,t2,c2)
-    | Lambda (_,t1,c1), Lambda (_,t2,c2) -> compare [(f,t1,t2); (f,c1,c2)]
-    | Prod _, _ -> -1 | _, Prod _ -> 1
-    | Lambda _, _ -> -1 | _, Lambda _ -> 1
-    | LetIn (_,b1,t1,c1), LetIn (_,b2,t2,c2) -> compare [(f,b1,b2); (f,t1,t2); (f,c1,c2)]
-    | LetIn _, _ -> -1 | _, LetIn _ -> 1
-    | App (c1,l1), App (c2,l2) -> compare [(f,c1,c2); (Array.compare f, l1, l2)]
-    | App _, _ -> -1 | _, App _ -> 1
-    | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2
-    | Const _, _ -> -1 | _, Const _ -> 1
-    | Ind (ind1, _u1), Ind (ind2, _u2) -> Ind.CanOrd.compare ind1 ind2
-    | Ind _, _ -> -1 | _, Ind _ -> 1
-    | Construct (ct1,_u1), Construct (ct2,_u2) -> Construct.CanOrd.compare ct1 ct2
-    | Construct _, _ -> -1 | _, Construct _ -> 1
-    | Case (_,_u1,pms1,(p1,_r1),iv1,c1,bl1), Case (_,_u2,pms2,(p2,_r2),iv2,c2,bl2) ->
-      compare [
-        (Array.compare f, pms1, pms2);
-        (ctx_cmp f, p1, p2);
-        (compare_invert f, iv1, iv2);
-        (f, c1, c2);
-        (Array.compare (ctx_cmp f), bl1, bl2);
-      ]
-    | Case _, _ -> -1 | _, Case _ -> 1
-    | Fix (ln1,(_,tl1,bl1)), Fix (ln2,(_,tl2,bl2)) ->
-      compare [(fix_cmp, ln1, ln2); (Array.compare f, tl1, tl2); (Array.compare f, bl1, bl2)]
-    | Fix _, _ -> -1 | _, Fix _ -> 1
-    | CoFix(ln1,(_,tl1,bl1)), CoFix(ln2,(_,tl2,bl2)) ->
-      compare [(Int.compare, ln1, ln2); (Array.compare f, tl1, tl2); (Array.compare f, bl1, bl2)]
-    | CoFix _, _ -> -1 | _, CoFix _ -> 1
-    | Proj (p1,_r1,c1), Proj (p2,_r2,c2) -> compare [(Projection.CanOrd.compare, p1, p2); (f, c1, c2)]
-    | Proj _, _ -> -1 | _, Proj _ -> 1
-    | Int i1, Int i2 -> Uint63.compare i1 i2
-    | Int _, _ -> -1 | _, Int _ -> 1
-    | Float f1, Float f2 -> Float64.total_compare f1 f2
-    | Float _, _ -> -1 | _, Float _ -> 1
-    | String s1, String s2 -> Pstring.compare s1 s2
-    | String _, _ -> -1 | _, String _ -> 1
-    | Array(_u1,t1,def1,ty1), Array(_u2,t2,def2,ty2) ->
-      compare [(Array.compare f, t1, t2); (f, def1, def2); (f, ty1, ty2)]
-    (*| Array _, _ -> -1 | _, Array _ -> 1*)
-
-let rec compare m n=
-  constr_ord_int compare m n
-
 (*******************)
 (*  hash-consing   *)
 (*******************)
@@ -1212,66 +1137,6 @@ let hash_cast_kind = function
 | NATIVEcast -> 1
 | DEFAULTcast -> 2
 
-(* Exported hashing fonction on constr, used mainly in plugins.
-   Slight differences from [snd (hash_term t)] above: it ignores binders. *)
-
-let rec hash t =
-  match kind t with
-    | Var i -> combinesmall 1 (Id.hash i)
-    | Sort s -> combinesmall 2 (Sorts.hash s)
-    | Cast (c, k, t) ->
-      let hc = hash c in
-      let ht = hash t in
-      combinesmall 3 (combine3 hc (hash_cast_kind k) ht)
-    | Prod (_, t, c) -> combinesmall 4 (combine (hash t) (hash c))
-    | Lambda (_, t, c) -> combinesmall 5 (combine (hash t) (hash c))
-    | LetIn (_, b, t, c) ->
-      combinesmall 6 (combine3 (hash b) (hash t) (hash c))
-    | App (c,l) -> begin match kind c with
-        | Cast (c, _, _) -> hash (mkApp (c,l)) (* WTF *)
-        | _ -> combinesmall 7 (combine (hash_term_array l) (hash c))
-      end
-    | Evar (e,l) ->
-      combinesmall 8 (combine (Evar.hash e) (hash_term_list l))
-    | Const (c,u) ->
-      combinesmall 9 (combine (Constant.CanOrd.hash c) (Instance.hash u))
-    | Ind (ind,u) ->
-      combinesmall 10 (combine (Ind.CanOrd.hash ind) (Instance.hash u))
-    | Construct (c,u) ->
-      combinesmall 11 (combine (Construct.CanOrd.hash c) (Instance.hash u))
-    | Case (_ , u, pms, (p,r), iv, c, bl) ->
-      combinesmall 12 (combine5 (hash c) (hash_invert iv) (hash_term_array pms) (Instance.hash u)
-                         (combine3 (hash_under_context p) (Sorts.relevance_hash r) (hash_branches bl)))
-    | Fix (_ln ,(_, tl, bl)) ->
-      combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl))
-    | CoFix(_ln, (_, tl, bl)) ->
-       combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl))
-    | Meta n -> combinesmall 15 n
-    | Rel n -> combinesmall 16 n
-    | Proj (p,r, c) ->
-      combinesmall 17 (combine3 (Projection.CanOrd.hash p) (Sorts.relevance_hash r) (hash c))
-    | Int i -> combinesmall 18 (Uint63.hash i)
-    | Float f -> combinesmall 19 (Float64.hash f)
-    | String s -> combinesmall 20 (Pstring.hash s)
-    | Array(u,t,def,ty) ->
-      combinesmall 21 (combine4 (Instance.hash u) (hash_term_array t) (hash def) (hash ty))
-
-and hash_invert = function
-  | NoInvert -> 0
-  | CaseInvert {indices;} ->
-    combinesmall 1 (hash_term_array indices)
-
-and hash_term_array t =
-  Array.fold_left (fun acc t -> combine acc (hash t)) 0 t
-
-and hash_term_list t =
-  SList.Skip.fold (fun acc t -> combine (hash t) acc) 0 t
-
-and hash_under_context (_, t) = hash t
-
-and hash_branches bl =
-  Array.fold_left (fun acc t -> combine acc (hash_under_context t)) 0 bl
-
 module CaseinfoHash =
 struct
   type t = case_info

kernel/constr.mli

@@ -426,9 +426,6 @@ val leq_constr_univs : UGraph.t -> constr -> constr -> bool
    application grouping and ignoring universe instances. *)
 val eq_constr_nounivs : constr -> constr -> bool
 
-(** Total ordering compatible with [equal] *)
-val compare : constr -> constr -> int
-
 (** {6 Extension of Context with declarations on constr} *)
 
 type rel_declaration = (constr, types, Sorts.relevance) Context.Rel.Declaration.pt
@@ -621,8 +618,6 @@ val eq_invert : ('a -> 'a -> bool)
 
 (** {6 Hashconsing} *)
 
-val hash : constr -> int
-
 (*********************************************************************)
 
 module GenHCons(C:sig

plugins/btauto/refl_btauto.ml

@@ -49,7 +49,7 @@ end
 
 module Env = struct
 
-  module ConstrHashtbl = Hashtbl.Make (Constr)
+  module ConstrHashtbl = Hashtbl.Make (Termops.ConstrData)
 
   type t = (int ConstrHashtbl.t * int ref)
 

plugins/cc/ccalgo.ml

@@ -238,7 +238,7 @@ struct
     | Sort (Type _u) -> mkSort (type1)
     | _ -> Constr.map drop_univ c
 
-  let mkSymb s = make (Symb (s, Constr.hash (drop_univ s)))
+  let mkSymb s = make (Symb (s, Termops.ConstrData.hash (drop_univ s)))
 
   let mkProduct (s1, s2) = make (Product (s1, s2))
 
@@ -341,7 +341,7 @@ type node =
 module Constrhash = Hashtbl.Make
   (struct type t = constr
           let equal = eq_constr_nounivs
-          let hash = Constr.hash
+          let hash = Termops.ConstrData.hash (* XXX no guarantee that hash is compatible with equal *)
    end)
 module Typehash = Constrhash
 

plugins/firstorder/formula.ml

@@ -45,7 +45,7 @@ val repr : uid -> int
 end =
 struct
 
-module CM = Map.Make(Constr)
+module CM = Map.Make(Termops.ConstrData)
 
 type t = {
   max_uid : int;

plugins/firstorder/instances.ml

@@ -24,7 +24,7 @@ open Names
 open Context.Rel.Declaration
 
 let compare_instance inst1 inst2=
-        let cmp c1 c2 = Constr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
+        let cmp c1 c2 = Termops.ConstrData.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
         match inst1,inst2 with
             Phantom(d1),Phantom(d2)->
               (cmp d1 d2)