From c7362fe3582e25ddd76c25e7c1315546538db6c2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@Inria.fr>
Date: Fri, 4 Oct 2019 17:57:16 +0200
Subject: [PATCH] elpi 1.8

---
 coq-builtin.elpi     | 12 ++++++++++++
 src/coq_elpi_HOAS.ml | 23 ++++++++++++-----------
 2 files changed, 24 insertions(+), 11 deletions(-)

diff --git a/coq-builtin.elpi b/coq-builtin.elpi
index b3624bb93..3ba6d0f08 100644
--- a/coq-builtin.elpi
+++ b/coq-builtin.elpi
@@ -638,6 +638,12 @@ kind option type -> type.
 type none option A.
 type some A -> option A.
 
+% Result of a comparison
+kind cmp type.
+type eq cmp.
+type lt cmp.
+type gt cmp.
+
 % == Elpi builtins =====================================
 
 % [dprint ...] prints raw terms (debugging)
@@ -690,6 +696,9 @@ pred (==) i:A, i:A.
 X == Y :- same_term X Y.
 
 
+% [cmp_term A B Cmp] Compares A and B. Only works if A and B are ground.
+external pred cmp_term i:any, i:any, o:cmp.
+
 % [name T ...] checks if T is a eigenvariable. When used with tree arguments
 % it relates an applied name with its head and argument list.
 external type name any -> variadic any prop.
@@ -709,6 +718,9 @@ external pred occurs % checks if the constant occurs in the term
 % scope
 external pred closed_term o:any.
 
+% [ground_term T] Checks if T contains unification variables
+external pred ground_term i:any.
+
 % [is_cdata T Ctype] checks if T is primitive of type Ctype, eg (ctype
 % "int")
 external pred is_cdata i:any, o:ctyp.
diff --git a/src/coq_elpi_HOAS.ml b/src/coq_elpi_HOAS.ml
index 212601fa7..22025d62a 100644
--- a/src/coq_elpi_HOAS.ml
+++ b/src/coq_elpi_HOAS.ml
@@ -32,7 +32,7 @@ let namein, isname, nameout, name =
     doc = "Name.Name.t: Name hints (in binders), can be input writing a name between backticks, e.g. `x` or `_` for anonymous. Important: these are just printing hints with no meaning, hence in elpi two @name are always related: `x` = `y`";
     pp = (fun fmt x ->
       Format.fprintf fmt "`%s`" (Pp.string_of_ppcmds (Name.print x)));
-    eq = (fun _ _ -> true);
+    compare = (fun _ _ -> 0);
     hash = (fun _ -> 0);
     hconsed = false;
     constants = [];
@@ -120,7 +120,7 @@ let univin, isuniv, univout, univ_to_be_patched =
         | x :: y :: _ -> y ^ "." ^ x
         | _ -> s in
       Format.fprintf fmt "«%s»" s);
-    eq = Univ.Universe.equal;
+    compare = Univ.Universe.compare;
     hash = Univ.Universe.hash;
     hconsed = false;
     constants = [];
@@ -134,10 +134,11 @@ type global_constant = Variable of Names.Id.t  | Constant of Names.Constant.t
 let hash_global_constant = function
   | Variable id -> Names.Id.hash id
   | Constant c -> Names.Constant.hash c
-let equal_global_constat x y = match x,y with
-  | Variable v1, Variable v2 -> Names.Id.equal v1 v2
-  | Constant c1, Constant c2 -> Names.Constant.equal c1 c2
-  | _ -> false
+let compare_global_constant x y = match x,y with
+  | Variable v1, Variable v2 -> Names.Id.compare v1 v2
+  | Constant c1, Constant c2 -> Names.Constant.CanOrd.compare c1 c2
+  | Variable _, _ -> -1
+  | _ -> 1
 
 let global_constant_of_globref = function
   | Globnames.VarRef x -> Variable x
@@ -154,7 +155,7 @@ let constant, inductive, constructor =
         | Variable x -> Globnames.VarRef x
         | Constant c -> Globnames.ConstRef c in
       Format.fprintf fmt "«%s»" (Pp.string_of_ppcmds (Printer.pr_global x)));
-    eq = equal_global_constat;
+    compare = compare_global_constant;
     hash = hash_global_constant;
     hconsed = false;
     constants = [];
@@ -163,7 +164,7 @@ let constant, inductive, constructor =
     name = "inductive";
     doc = "Inductive type name";
     pp = (fun fmt x -> Format.fprintf fmt "«%s»" (Pp.string_of_ppcmds (Printer.pr_global (Globnames.IndRef x))));
-    eq = Names.eq_ind;
+    compare = Names.ind_ord;
     hash = Names.ind_hash;
     hconsed = false;
     constants = [];
@@ -172,7 +173,7 @@ let constant, inductive, constructor =
     name = "constructor";
     doc = "Inductive constructor name";
     pp = (fun fmt x -> Format.fprintf fmt "«%s»" (Pp.string_of_ppcmds (Printer.pr_global (Globnames.ConstructRef x))));
-    eq = Names.eq_constructor;
+    compare = Names.constructor_ord;
     hash = Names.constructor_hash;
     hconsed = false;
     constants = [];
@@ -228,7 +229,7 @@ let mpin, ismp, mpout, modpath =
     doc = "Name of a module /*E*/";
     pp = (fun fmt x ->
             Format.fprintf fmt "«%s»" (Names.ModPath.to_string x));
-    eq = Names.ModPath.equal;
+    compare = Names.ModPath.compare;
     hash = Names.ModPath.hash;
     hconsed = false;
     constants = [];
@@ -241,7 +242,7 @@ let mptyin, istymp, mptyout, modtypath =
     doc = "Name of a module type /*E*/";
     pp = (fun fmt x ->
             Format.fprintf fmt "«%s»" (Names.ModPath.to_string x));
-    eq = Names.ModPath.equal;
+    compare = Names.ModPath.compare;
     hash = Names.ModPath.hash;
     hconsed = false;
     constants =[];