Skip to content

Test for fix type name collision #908

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 3 commits into
base: master
Choose a base branch
from
+82 −64
Draft

Test for fix type name collision #908

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
4bdad2c
update builtins
gares Oct 17, 2025
210f857
test
gares Oct 17, 2025
2eac94f
test
gares Oct 17, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
128 changes: 64 additions & 64 deletions builtin-doc/elpi-builtin.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -31,29 +31,29 @@ kind string type.
kind float type.


external symbol (;) prop -> prop -> prop.
external symbol (;) (pred) -> (pred) -> (pred).

(A ; _) :- A.

(_ ; B) :- B.

external symbol (:-) : (func) -> (func) -> (func) = "core".

external symbol (:-) : (func) -> list prop -> (func) = "core".
external symbol (:-) : (func) -> list (pred) -> (func) = "core".

external symbol (,) : variadic (func) (func).

external symbol uvar : A = "core".

external symbol (as) : A -> A -> A = "core".

external symbol (=>) : prop -> (func) -> (func) = "core".
external symbol (=>) : (pred) -> (func) -> (func) = "core".

external symbol (=>) : list prop -> (func) -> (func) = "core".
external symbol (=>) : list (pred) -> (func) -> (func) = "core".

external symbol (==>) : prop -> (func) -> (func).
external symbol (==>) : (pred) -> (func) -> (func).

external symbol (==>) : list prop -> (func) -> (func).
external symbol (==>) : list (pred) -> (func) -> (func).

% -- Control --

Expand Down Expand Up @@ -428,12 +428,12 @@ external func open_safe safe -> list A.

% [if C T E] picks the first success of C then runs T (never E).
% if C has no success it runs E.
func if prop, (func), (func).
func if (pred), (func), (func).
if B T _ :- B, !, T.
if _ _ E :- E.

% [if2 C1 B1 C2 B2 E] like if but with 2 then branches (and one else branch).
func if2 prop, (func), prop, (func), (func).
func if2 (pred), (func), (pred), (func), (func).
if2 G1 P1 _ _ _ :- G1, !, P1.
if2 _ _ G2 P2 _ :- G2, !, P2.
if2 _ _ _ _ E :- !, E.
Expand Down Expand Up @@ -496,7 +496,7 @@ assert-ok! Cond Msg :- Cond Diagnostic, !, (Diagnostic = ok ; Diagnostic = error
assert-ok! _ Msg :- fatal-error-w-data Msg "no diagnostic returned".

% [spy P] traces the call to P, printing all success and the final failure
pred spy i:prop.
pred spy (pred).
spy P :- trace.counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
debug-print "----<<---- enter: " P,
P,
Expand Down Expand Up @@ -537,7 +537,7 @@ func append list A, list A -> list A.
append [X|XS] L [X|L1] :- append XS L L1 .
append [] L L .

pred appendR o:list A, o:list A, o:list A.
pred appendR -> list A, list A, list A.
appendR [] L L.
appendR [X|XS] L [X|L1] :- appendR XS L L1.

Expand Down Expand Up @@ -631,34 +631,34 @@ nth N _ _ :- N < 0, !, fatal-error "nth got a negative index".
nth _ _ _ :- fatal-error "nth run out of list items".

% [lookup L K V] sees L as a map from K to V
pred lookup i:list (pair A B), i:A, o:B.
pred lookup list (pair A B), A -> B.
lookup [pr X Y|_] X Y.
lookup [_|LS] X Y :- lookup LS X Y.
lookup [_|LS] X Y :- lookup LS X Y.

% [lookup! L K V] sees L as a map from K to V, stops at the first binding
func lookup! list (pair A B), A -> B.
lookup! [pr X Y|_] X Y :- !.
lookup! [_|LS] X Y :- lookup! LS X Y.
lookup! [_|LS] X Y :- lookup! LS X Y.

% [mem! L X] succeeds once if X occurs inside L
func mem! list A, A ->.
mem! [X|_] X :- !.
mem! [_|L] X :- mem! L X.

% [mem L X] succeeds every time if X occurs inside L
pred mem i:list A, o:A.
pred mem list A -> A.
mem [X|_] X.
mem [_|L] X :- mem L X.

func exists! list A, (pred i:A) ->.
func exists! list A, (pred A).
exists! [X| _] P :- P X, !.
exists! [_|XS] P :- exists! XS P.

pred exists i:list A, i:(pred i:A).
pred exists list A, (pred A).
exists [X|_] P :- P X.
exists [_|L] P :- exists L P.

pred exists2 i:list A, i:list B, i:(pred i:A, i:B).
pred exists2 list A, list B, (pred A, B).
exists2 [] [_|_] _ :- fatal-error "exists2 on lists of different length".
exists2 [_|_] [] _ :- fatal-error "exists2 on lists of different length".
exists2 [X|_] [Y|_] P :- P X Y.
Expand All @@ -683,7 +683,7 @@ filter [] _ [].
filter [X|L] P R :- if (P X) (R = X :: L1) (R = L1), filter L P L1.

:index (1)
func partition list A, (pred i:A) -> list A, list A.
func partition list A, (pred A) -> list A, list A.
partition [] _ [] [].
partition [X|XS] P [X|R] L :- P X, !, partition XS P R L.
partition [X|XS] P R [X|L] :- partition XS P R L.
Expand Down Expand Up @@ -747,13 +747,13 @@ pred do-ok! o:diagnostic, i:list (pred o:diagnostic).
do-ok! ok [].
do-ok! S [P|PS] :- P S0, !, if (S0 = ok) (do-ok! S PS) (S = S0).

pred lift-ok i:prop, i:string, o:diagnostic.
pred lift-ok (pred), string -> diagnostic.
lift-ok P Msg R :- (P, R = ok; R = error Msg).

func spy-do! list prop.
spy-do! L :- map L (x\y\y = spy x) L1, do! L1.

func while-ok-do! diagnostic, list (pred o:diagnostic) -> diagnostic.
func while-ok-do! diagnostic, list (pred -> diagnostic) -> diagnostic.
while-ok-do! (error _ as E) _ E.
while-ok-do! ok [] ok.
while-ok-do! ok [P|PS] R :- P C, !, while-ok-do! C PS R.
Expand Down Expand Up @@ -1071,28 +1071,28 @@ external func std.loc.set.partition std.loc.set,

#line 1 "builtin_map.elpi"
kind std.map type -> type -> type.
type std.map std.map.private.map K V -> (pred i:K, i:K, o:cmp) -> std.map K V.
type std.map std.map.private.map K V -> (func K, K -> cmp) -> 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:(pred i:K, i:K, o:cmp), o:std.map K V.
func make (func K, K -> cmp) -> 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.
func find K, std.map K V -> 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.
func add K, V, std.map K V -> 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.
func remove K, std.map K V -> 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).
func bindings std.map K V -> list (pair K V).
bindings (std.map M _) L :- private.bindings M [] L.

namespace private {
Expand All @@ -1102,22 +1102,22 @@ 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.
func height map K V -> 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.
func create map K V, K, V, map K V -> 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.
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.

pred bal.aux i:int, i:int, i:int, i:int, i:map K V, i:K, i:V, i:map K V, o:map K V.
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.
Expand All @@ -1132,48 +1132,48 @@ bal.aux _ HR HL2 _ L X D (node (node RLL RLV RLD RLR _) RV RD RR _) T :-
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:(pred i:K, i:K, o:cmp), i:K, i:V, o:map K V.
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.

pred add.aux i:cmp, i:map K V, i:(pred i:K, i:K, o:cmp), i:K, i:V, o:map K V.
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 :- 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:(pred i:K, i:K, o:cmp), i:K, o:V.
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.

pred find.aux i:cmp, i:(pred i:K, i:K, o:cmp), i:map K V, i:map K V, i:V, i:K, o: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.

pred remove-min-binding i:map K V, o:map 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.

pred min-binding i:map K V, o:K, o:V.
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.

pred merge i:map K V, i:map K V, o:map K V.
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.

pred remove i:map K V, i:(pred i:K, i:K, o:cmp), i:K, o:map K V.
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.

pred remove.aux i:cmp, i:(pred i:K, i:K, o:cmp), i:map K V, i:map K V, i:K, i:V, i:K, o:map K V.
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.

pred bindings i:map K V, i:list (pair K V), o:list (pair K V).
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.
Expand All @@ -1185,31 +1185,31 @@ bindings (node L V D R _) X X1 :-

#line 1 "builtin_set.elpi"
kind std.set type -> type.
type std.set std.set.private.set E -> (pred i:E, i:E, o:cmp) -> std.set E.
type std.set std.set.private.set E -> (func E, E -> cmp) -> 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:(pred i:E, i:E, o:cmp), o:std.set E.
func make (func E, E -> cmp) -> 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.
func mem E, 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.
func add E, std.set E -> 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.
func remove E, std.set E -> 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.
func cardinal std.set E -> int.
cardinal (std.set M _) N :- private.cardinal M N.

pred elements i:std.set E, o:list E.
func elements std.set E -> list E.
elements (std.set M _) L :- private.elements M [] L.

namespace private {
Expand All @@ -1219,22 +1219,22 @@ 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.
func height set E -> int.
height empty 0.
height (node _ _ _ H) H.

pred create i:set E, i:E, i:set E, o:set E.
func create set E, E, set E -> 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.
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.

pred bal.aux i:int, i:int, i:int, i:int, i:set E, i:E, i:set E, o:set E.
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.
Expand All @@ -1249,52 +1249,52 @@ bal.aux _ HR HL2 _ L X (node (node RLL RLV RLR _) RV RR _) T :-
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:(pred i:E, i:E, o:cmp), i:E, o:set E.
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.

pred add.aux i:cmp, i:(pred i:E, i:E, o:cmp), i:set E, i:set E, i:E, i:E, i:int, o:set E.
func add.aux cmp, (func E, E -> cmp), set E, set E, E, E, int -> set E.
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:(pred i:E, i:E, o:cmp), i:E.
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.
mem.aux eq _ _ _ _.

pred mem.aux i:cmp, i:(pred i:E, i:E, o:cmp), i:set E, i:set E, i: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.

pred remove-min-binding i:set E, o:set 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.

pred min-binding i:set E, o:E.
func min-binding set E -> 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.
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.

pred remove i:set E, i:(pred i:E, i:E, o:cmp), i:E, o:set E.
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.

pred remove.aux i:cmp, i:(pred i:E, i:E, o:cmp), i:set E, i:set E, i:E, i:E, o:set E.
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.

pred cardinal i:set E, o:int.
func cardinal set E -> 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.
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.
Expand Down Expand Up @@ -1439,7 +1439,7 @@ external func open_string string -> in_stream.
% [lookahead InStream NextChar] peeks one byte from InStream
external func lookahead in_stream -> string.

pred printterm i:out_stream, i:A.
pred printterm out_stream, A.

printterm S T :- term_to_string T T1, output S T1.

Expand Down
Loading
Loading