Merge pull request #356 from LPCIC/oc-opt-out

attribute to disable occur check

Author: gares

.github/workflows/users.yml

@@ -33,7 +33,7 @@ jobs:
         - run: opam pin --ignore-constraints-on elpi add rocq-elpi https://github.com/LPCIC/coq-elpi.git#master
         - run: opam pin --ignore-constraints-on elpi add coq-elpi  https://github.com/LPCIC/coq-elpi.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-stdlib https://github.com/rocq-prover/stdlib.git#master
-        - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#rename-class
+        - run: opam pin --ignore-constraints-on elpi add rocq-hierarchy-builder https://github.com/math-comp/hierarchy-builder.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-boot https://github.com/math-comp/math-comp.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-order https://github.com/math-comp/math-comp.git#master
         - run: opam pin --ignore-constraints-on elpi add rocq-mathcomp-fingroup https://github.com/math-comp/math-comp.git#master

CHANGES.md

@@ -1,5 +1,11 @@
 # UNRELEASED
 
+- Language:
+  - New attribute `:nooc` to disable occur check
+- Stdlib:
+  - New `unsound_unif` performing unification without occur check
+  - New `std.fset` and `std.fmap` that work on ground terms and
+    disable occur check
 - Compiler:
   - Change raise an error in case of type/typeabbrev collision
 

src/API.ml

@@ -237,7 +237,7 @@ module Execute = struct
         relocate_assignment_to_runtime = (fun ~target ~depth s ->
           Compiler.relocate_closed_term ~from
             (Util.StrMap.find s assignments |> full_deref ~depth:idepth |> uvar2discard ~depth:idepth) ~to_:target
-          |> Stdlib.Result.map (hmove ?avoid:None ~from:depth ~to_:depth)
+          |> Stdlib.Result.map (hmove ?oc:None ~from:depth ~to_:depth)
         );
         }
 
@@ -479,7 +479,7 @@ module BuiltInData = struct
     let ty = Conversion.(TyName ty) in
     let embed ~depth state (x,from) =
       let module R = (val !r) in let open R in
-      state, hmove ~from ~to_:depth ?avoid:None x, [] in
+      state, hmove ~from ~to_:depth ?oc:None x, [] in
     let readback ~depth state t =
       state, fresh_copy t depth, [] in
     { Conversion.embed; readback; ty;
@@ -906,7 +906,7 @@ module BuiltInPredicate = struct
 
   let beta ~depth t args =
     let module R = (val !r) in let open R in
-    deref_apparg ~from:depth ~to_:depth ?avoid:None t args
+    deref_apparg ~from:depth ~to_:depth ?oc:None t args
 
   module HOAdaptors = struct
 
@@ -1300,7 +1300,7 @@ module Utils = struct
 
   let move ~from ~to_ t =
     let module R = (val !r) in let open R in
-    hmove ~from ~to_ ?avoid:None t
+    hmove ~from ~to_ ?oc:None t
 
   let beta = BuiltInPredicate.beta
   let error = Util.error

src/builtin.elpi

@@ -462,6 +462,11 @@ external func same_term A, A.
 func (==) A, A.
 X == Y :- same_term X Y.
 
+% Unification without occur check. It can create infinite terms.
+:nooc
+func unsound_unif -> A, A.
+unsound_unif X X.
+
 
 % [cmp_term A B Cmp] Compares A and B. Only works if A and B are ground.
 external func cmp_term any, any -> cmp.
@@ -1276,6 +1281,136 @@ bindings (node L V D R _) X X1 :-
 } % std.map.private
 } % std.map
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Fast maps only work ground terms but do not perform occur check
+
+kind std.fmap type -> type -> type.
+type std.fmap std.fmap.private.map K V -> (func K, K -> cmp) -> std.fmap K V.
+
+namespace std.fmap {
+
+% [make Eq Ltn M] builds an empty map M where keys are compared using Eq and Ltn
+func make (func K, K -> cmp) -> std.fmap K V.
+make Cmp (std.fmap private.empty Cmp).
+
+% [find K M V] looks in M for the value V associated to K
+func find K, std.fmap K V -> V.
+find K (std.fmap M Cmp) V :-
+  private.assert-ground K,
+  private.find M Cmp K V.
+
+% [add K V M M1] M1 is M where K is bound to V
+func add K, V, std.fmap K V -> std.fmap K V.
+add K V (std.fmap M Cmp) R :-
+  private.assert-ground K,
+  private.assert-ground V,
+  private.add M Cmp K V M1,
+  unsound_unif R (std.fmap M1 Cmp).
+
+% [remove K M M1] M1 is M where K is unbound
+func remove K, std.fmap K V -> std.fmap K V.
+remove K (std.fmap M Cmp) R :-
+  private.assert-ground K,
+  private.remove M Cmp K M1,
+  unsound_unif R (std.fmap M1 Cmp).
+
+% [bindings M L] L is the key-value pairs in increasing order
+func bindings std.fmap K V -> list (pair K V).
+bindings (std.fmap M _) L :- private.bindings M [] L.
+
+namespace private {
+
+func assert-ground A.
+assert-ground A :- std.assert! (ground_term A) "std.fmap: not ground".
+
+% 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.
+
+func height map K V -> int.
+height empty 0.
+height (node _ _ _ _ H) H.
+
+func create map K V, K, V, map K V -> map K V.
+create L K V R X :-
+  H is {std.max {height L} {height R}} + 1,
+  unsound_unif X (node L K V R H).
+
+func bal map K V, K, V, map K V -> 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.
+
+func bal.aux int, int, int, int, map K V, K, V, map K V -> map K V.
+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.
+
+func add map K V, (func K, K -> cmp), K, V -> 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.
+
+func add.aux cmp, map K V, (func K, K -> cmp), K, V -> map K V.
+add.aux eq (node L _ _ R H) _   X XD T :- unsound_unif 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.
+
+func find map K V, (func K, K -> cmp), K -> V.
+find (node L K1 V1 R _) Cmp K V :- Cmp K K1 E, find.aux E Cmp L R V1 K V.
+
+func find.aux cmp, (func K, K -> cmp), map K V, map K V, V, 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.
+
+func remove-min-binding map K V -> 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.
+
+func min-binding map K V -> K, V.
+min-binding (node empty V D _ _) V D :- !.
+min-binding (node L _ _ _ _) V D :- min-binding L V D.
+
+func merge map K V, map K V -> 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.
+
+func remove map K V, (func K, K -> cmp), K -> 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.
+
+func remove.aux cmp, (func K, K -> cmp), map K V, map K V, K, V, K -> map K V.
+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.
+
+func bindings map K V, list (pair K V) -> 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.fmap.private
+} % std.fmap
+
 
 #line 1 "builtin_set.elpi"
 kind std.set type -> type.
@@ -1396,6 +1531,139 @@ elements (node L E R _) Acc X :-
 } % std.set.private
 } % std.set
 
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+% Fast sets only work ground terms but do not perform occur check
+
+kind std.fset type -> type.
+type std.fset std.fset.private.set E -> (func E, E -> cmp) -> std.fset E.
+
+namespace std.fset {
+
+% [make Eq Ltn M] builds an empty set M where keys are compared using Eq and Ltn
+func make (func E, E -> cmp) -> std.fset E.
+make Cmp (std.fset private.empty Cmp).
+
+% [mem E M] looks if E is in M
+func mem E, std.fset E.
+mem E (std.fset M Cmp):- private.mem M Cmp E.
+
+% [add E M M1] M1 is M + {E}
+func add E, std.fset E -> std.fset E.
+add E (std.fset M Cmp) R :-
+  private.assert-ground E,
+  private.add M Cmp E M1,
+  unsound_unif R (std.fset M1 Cmp).
+
+% [remove E M M1] M1 is M - {E}
+func remove E, std.fset E -> std.fset E.
+remove E (std.fset M Cmp) R :-
+  private.assert-ground E,
+  private.remove M Cmp E M1,
+  unsound_unif R (std.fset M1 Cmp).
+
+% [cardinal S N] N is the number of elements of S
+func cardinal std.fset E -> int.
+cardinal (std.fset M _) N :- private.cardinal M N.
+
+func elements std.fset E -> list E.
+elements (std.fset M _) L :- private.elements M [] L.
+
+namespace private {
+
+func assert-ground A.
+assert-ground A :- std.assert! (ground_term A) "std.fset: not ground".
+
+% Taken from OCaml's set.ml
+kind set type -> type.
+type empty set E.
+type node set E -> E -> set E -> int -> set E.
+
+func height set E -> int.
+height empty 0.
+height (node _ _ _ H) H.
+
+func create set E, E, set E -> set E.
+create L E R S :-
+  H is {std.max {height L} {height R}} + 1,
+  unsound_unif S (node L E R H).
+
+func bal set E, E, set E -> 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.
+
+func bal.aux int, int, int, int, set E, E, set E -> set E.
+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.
+
+func add set E, (func E, E -> cmp), E -> 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.
+
+func add.aux cmp, (func E, E -> cmp), set E, set E, E, E, int -> set E.
+add.aux eq _   L R X _ H S :- unsound_unif S (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.
+
+func mem set E, (func E, E -> cmp), E.
+mem (node L K R _) Cmp E :- Cmp E K O, mem.aux O Cmp L R E.
+
+func mem.aux cmp, (func E, E -> cmp), set E, set E, E.
+mem.aux eq _ _ _ _.
+mem.aux lt Cmp L _ E :- mem L Cmp E.
+mem.aux gt Cmp _ R E :- mem R Cmp E.
+
+func remove-min-binding set E -> 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.
+
+func min-binding set E -> E.
+min-binding (node empty E _ _) E :- !.
+min-binding (node L _ _ _) E :- min-binding L E.
+
+func merge set E, set E -> 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.
+
+func remove set E, (func E, E -> cmp), E -> 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.
+
+func remove.aux cmp, (func E, E -> cmp), set E, set E, E, E -> set E.
+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.
+
+func cardinal set E -> int.
+cardinal empty 0.
+cardinal (node L _ R _) N :- N is {cardinal L} + 1 + {cardinal R}.
+
+func elements set E, list E -> list E.
+elements empty X X.
+elements (node L E R _) Acc X :-
+  elements L [E|{elements R Acc}] X.
+
+} % std.fset.private
+} % std.fset
+
 
 % == Elpi runtime builtins =====================================
 

src/builtin.ml

@@ -851,6 +851,11 @@ let elpi_nonlogical_builtins = let open BuiltIn in let open BuiltInData in let o
 % Infix notation for same_term
 func (==) A, A.
 X == Y :- same_term X Y.
+
+% Unification without occur check. It can create infinite terms.
+:nooc
+func unsound_unif -> A, A.
+unsound_unif X X.
 |};
 
   MLCode(Pred("cmp_term",