Merge branch 'elpi-1.8'

coq-builtin.elpi

@@ -640,6 +640,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)
@@ -692,6 +698,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.
@@ -711,6 +720,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.
@@ -1176,6 +1188,226 @@ external pred std.loc.set.elements i:std.loc.set, o:list @loc.
 % [std.loc.set.cardinal M N] N is the number of elements of M
 external pred std.loc.set.cardinal i:std.loc.set, o:int.
 
+#line 0 "builtin_map.elpi"
+kind std.map type -> type -> type.
+type std.map std.map.private.map K V -> (K -> K -> cmp -> prop) -> std.map K V.
+
+namespace std.map {
+
+% [make Eq Ltn M] builds an empty map M where keys are compared using Eq and Ltn
+pred make i:(K -> K -> cmp -> prop), o:std.map K V.
+make Cmp (std.map private.empty Cmp).
+
+% [find K M V] looks in M for the value V associated to K
+pred find i:K, i:std.map K V, o:V.
+find K (std.map M Cmp) V :- private.find M Cmp K V.
+
+% [add K V M M1] M1 is M where K is bound to V
+pred add i:K, i:V, i:std.map K V, o:std.map K V.
+add K V (std.map M Cmp) (std.map M1 Cmp) :- private.add M Cmp K V M1.
+
+% [remove K M M1] M1 is M where K is unbound
+pred remove i:K, i:std.map K V, o:std.map K V.
+remove K (std.map M Cmp) (std.map M1 Cmp) :- private.remove M Cmp K M1.
+
+% [bindings M L] L is the key-value pairs in increasing order
+pred bindings i:std.map K V, o:list (pair K V).
+bindings (std.map M _) L :- private.bindings M [] L.
+
+namespace private {
+
+% Taken from OCaml's map.ml
+kind map type -> type -> type.
+type empty map K V.
+type node map K V -> K -> V -> map K V -> int -> map K V.
+
+pred height i:map K V, o:int.
+height empty 0.
+height (node _ _ _ _ H) H.
+
+pred create i:map K V, i:K, i:V, i:map K V, o:map K V.
+create L K V R (node L K V R H) :- H is {std.max {height L} {height R}} + 1.
+
+pred bal i:map K V, i:K, i:V, i:map K V, o:map K V.
+bal L K V R T :-
+  height L HL,
+  height R HR,
+  HL2 is HL + 2,
+  HR2 is HR + 2,
+  bal.aux HL HR HL2 HR2 L K V R T.
+
+bal.aux HL _ _ HR2 (node LL LV LD LR _) X D R T :-
+  HL > HR2, {height LL} >= {height LR}, !,
+  create LL LV LD {create LR X D R} T.
+bal.aux HL _ _ HR2 (node LL LV LD (node LRL LRV LRD LRR _) _) X D R T :-
+  HL > HR2, !,
+  create {create LL LV LD LRL} LRV LRD {create LRR X D R} T.
+bal.aux _ HR HL2 _ L X D (node RL RV RD RR _) T :-
+  HR > HL2, {height RR} >= {height RL}, !,
+  create {create L X D RL} RV RD RR T.
+bal.aux _ HR HL2 _ L X D (node (node RLL RLV RLD RLR _) RV RD RR _) T :-
+  HR > HL2, !,
+  create {create L X D RLL} RLV RLD {create RLR RV RD RR} T.
+bal.aux _ _ _ _ L K V R T :- create L K V R T.
+
+pred add i:map K V, i:(K -> K -> cmp -> prop), i:K, i:V, o:map K V.
+add empty _ K V T :- create empty K V empty T.
+add (node _ X _ _ _ as M) Cmp X1 XD M1 :- Cmp X1 X E, add.aux E M Cmp X1 XD M1.
+add.aux eq (node L _ _ R H) _   X XD T :- T = node L X XD R H. 
+add.aux lt (node L V D R _) Cmp X XD T :- bal {add L Cmp X XD} V D R T.
+add.aux gt (node L V D R _) Cmp X XD T :- bal L V D {add R Cmp X XD} T.
+
+pred find i:map K V, i:(K -> K -> cmp -> prop), i:K, o:V.
+find (node L K1 V1 R _) Cmp K V :- Cmp K K1 E, find.aux E Cmp L R V1 K V.
+find.aux eq _   _ _ V _ V.
+find.aux lt Cmp L _ _ K V :- find L Cmp K V.
+find.aux gt Cmp _ R _ K V :- find R Cmp K V.
+
+pred remove-min-binding i:map K V, o:map K V.
+remove-min-binding (node empty _ _ R _) R :- !.
+remove-min-binding (node L V D R _) X :- bal {remove-min-binding L} V D R X.
+
+pred min-binding i:map K V, o:K, o:V.
+min-binding (node empty V D _ _) V D :- !.
+min-binding (node L _ _ _ _) V D :- min-binding L V D.
+
+pred merge i:map K V, i:map K V, o:map K V.
+merge empty X X :- !.
+merge X empty X :- !.
+merge M1 M2 R :-
+  min-binding M2 X D,
+  bal M1 X D {remove-min-binding M2} R.
+
+pred remove i:map K V, i:(K -> K -> cmp -> prop), i:K, o:map K V.
+remove empty _ _ empty :- !.
+remove (node L V D R _) Cmp X M :- Cmp X V E, remove.aux E Cmp L R V D X M.
+remove.aux eq _   L R _ _ _ M :- merge L R M.
+remove.aux lt Cmp L R V D X M :- bal {remove L Cmp X} V D R M.
+remove.aux gt Cmp L R V D X M :- bal L V D {remove R Cmp X} M.
+
+pred bindings i:map K V, i:list (pair K V), o:list (pair K V).
+bindings empty X X.
+bindings (node L V D R _) X X1 :-
+  bindings L [pr V D|{bindings R X}] X1.
+
+
+} % std.map.private
+} % std.map
+
+
+#line 0 "builtin_set.elpi"
+kind std.set type -> type.
+type std.set std.set.private.set E -> (E -> E -> cmp -> prop) -> std.set E.
+
+namespace std.set {
+
+% [make Eq Ltn M] builds an empty set M where keys are compared using Eq and Ltn
+pred make i:(E -> E -> cmp -> prop), o:std.set E.
+make Cmp (std.set private.empty Cmp).
+
+% [mem E M] looks if E is in M
+pred mem i:E, i:std.set E.
+mem E (std.set M Cmp):- private.mem M Cmp E.
+
+% [add E M M1] M1 is M + {E}
+pred add i:E, i:std.set E, o:std.set E.
+add E (std.set M Cmp) (std.set M1 Cmp) :- private.add M Cmp E M1.
+
+% [remove E M M1] M1 is M - {E}
+pred remove i:E, i:std.set E, o:std.set E.
+remove E (std.set M Cmp) (std.set M1 Cmp) :- private.remove M Cmp E M1.
+
+% [cardinal S N] N is the number of elements of S
+pred cardinal i:std.set E, o:int.
+cardinal (std.set M _) N :- private.cardinal M N.
+
+pred elements i:std.set E, o:list E.
+elements (std.set M _) L :- private.elements M [] L.
+
+namespace private {
+
+% Taken from OCaml's set.ml
+kind set type -> type.
+type empty set E.
+type node set E -> E -> set E -> int -> set E.
+
+pred height i:set E, o:int.
+height empty 0.
+height (node _ _ _ H) H.
+
+pred create i:set E, i:E, i:set E, o:set E.
+create L E R (node L E R H) :- H is {std.max {height L} {height R}} + 1.
+
+pred bal i:set E, i:E, i:set E, o:set E.
+bal L E R T :-
+  height L HL,
+  height R HR,
+  HL2 is HL + 2,
+  HR2 is HR + 2,
+  bal.aux HL HR HL2 HR2 L E R T.
+
+bal.aux HL _ _ HR2 (node LL LV LR _) X R T :-
+  HL > HR2, {height LL} >= {height LR}, !,
+  create LL LV {create LR X R} T.
+bal.aux HL _ _ HR2 (node LL LV (node LRL LRV LRR _) _) X R T :-
+  HL > HR2, !,
+  create {create LL LV LRL} LRV {create LRR X R} T.
+bal.aux _ HR HL2 _ L X (node RL RV RR _) T :-
+  HR > HL2, {height RR} >= {height RL}, !,
+  create {create L X RL} RV RR T.
+bal.aux _ HR HL2 _ L X (node (node RLL RLV RLR _) RV RR _) T :-
+  HR > HL2, !,
+  create {create L X RLL} RLV {create RLR RV RR} T.
+bal.aux _ _ _ _ L E R T :- create L E R T.
+
+pred add i:set E, i:(E -> E -> cmp -> prop), i:E, o:set E.
+add empty _ E T :- create empty E empty T.
+add (node L X R H) Cmp X1 S :- Cmp X1 X E, add.aux E Cmp L R X X1 H S.
+add.aux eq _ L R X _ H (node L X R H).
+add.aux lt Cmp L R E X _ T :- bal {add L Cmp X} E R T.
+add.aux gt Cmp L R E X _ T :- bal L E {add R Cmp X} T.
+
+pred mem i:set E, i:(E -> E -> cmp -> prop), i:E.
+mem (node L K R _) Cmp E :- Cmp E K O, mem.aux O Cmp L R E.
+mem.aux eq _ _ _ _.
+mem.aux lt Cmp L _ E :- mem L Cmp E.
+mem.aux gt Cmp _ R E :- mem R Cmp E.
+
+pred remove-min-binding i:set E, o:set E.
+remove-min-binding (node empty _ R _) R :- !.
+remove-min-binding (node L E R _) X :- bal {remove-min-binding L} E R X.
+
+pred min-binding i:set E, o:E.
+min-binding (node empty E _ _) E :- !.
+min-binding (node L _ _ _) E :- min-binding L E.
+
+pred merge i:set E, i:set E, o:set E.
+merge empty X X :- !.
+merge X empty X :- !.
+merge M1 M2 R :-
+  min-binding M2 X,
+  bal M1 X {remove-min-binding M2} R.
+
+pred remove i:set E, i:(E -> E -> cmp -> prop), i:E, o:set E.
+remove empty _ _ empty.
+remove (node L E R _) Cmp X M :- Cmp X E O, remove.aux O Cmp L R E X M.
+remove.aux eq _   L R _ _ M :- merge L R M.
+remove.aux lt Cmp L R E X M :- bal {remove L Cmp X} E R M.
+remove.aux gt Cmp L R E X M :- bal L E {remove R Cmp X} M.
+
+pred cardinal i:set E, o:int.
+cardinal empty 0.
+cardinal (node L _ R _) N :- N is {cardinal L} + 1 + {cardinal R}.
+
+pred elements i:set E, i:list E, o:list E.
+elements empty X X.
+elements (node L E R _) Acc X :-
+  elements L [E|{elements R Acc}] X.
+
+} % std.set.private
+} % std.set
+
+
 %
 % #############################################################################
 

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 =[];

src/coq_elpi_vernacular.ml

@@ -176,7 +176,7 @@ let builtin_declarations =
    LPDoc "#############################################################################"; ] @
   core_builtins @
   elpi_builtins @ elpi_nonlogical_builtins @
-  elpi_stdlib @
+  elpi_stdlib @ elpi_map @ elpi_set @
   [LPDoc "#############################################################################";
    LPDoc "Internal use only (Elpi Print/Typecheck). Please don't use.";
    LPDoc "#############################################################################"; ] @

theories/examples/example_reflexive_tactic.v

@@ -221,7 +221,7 @@ solve [trm Zero, trm Op] [G] _ :-
           = (interp lp:T lp:Zero lp:Op lp:L lp:AstB) }},
   % This implements "change": there is no "cast"
   % term constructor in Coq-Elpi since a degenerate let-in can do it as well
-  refine {{ let x : lp:Ty := _ in x }} G GL.
+  P = {{ let x : lp:Ty := _ in x }}.
 
 :name "error"
 solve _ _ _ :- coq.error "Not an equality / no signature provided".