builtin.elpi

% File generated by elpi -document-builtins, do not edit

%  == Core builtins =====================================

%  -- Logic --

pred true.

true.

pred fail.

pred false.

external pred (=) o:A, o:A. % unification

typeabbrev int (ctype "int").


typeabbrev string (ctype "string").


typeabbrev float (ctype "float").


pred (;) o:prop, o:prop.

(A ; _) :- A.

(_ ; B) :- B.

type (:-) prop -> prop -> prop.

type (:-) prop -> list prop -> prop.

type (,) variadic prop prop.

type uvar A.

type (as) A -> A -> A.

type (=>) prop -> prop -> prop.

type (=>) list prop -> prop -> prop.

%  -- Control --

external pred !. % The cut operator

pred not i:prop.

not X :- X, !, fail.

not _.

% [declare_constraint C Key1 Key2...] declares C blocked
% on Key1 Key2 ... (variables, or lists thereof).
external type declare_constraint any -> any -> variadic any prop.

external pred print_constraints. % prints all constraints

% [halt ...] halts the program and print the terms
external type halt variadic any prop.

pred stop.

stop :- halt.

%  -- Evaluation --

% [calc Expr Out] unifies Out with the value of Expr. It can be used in
% tandem with spilling, eg [f {calc (N + 1)}]
external pred calc i:A, o:A.

pred (is) o:A, i:A.

X is Y :- calc Y X.

type (-) A -> A -> A.

type (i-) int -> int -> int.

type (r-) float -> float -> float.

type (+) int -> int -> int.

type (+) float -> float -> float.

type (i+) int -> int -> int.

type (r+) float -> float -> float.

type (*) int -> int -> int.

type (*) float -> float -> float.

type (/) float -> float -> float.

type (mod) int -> int -> int.

type (div) int -> int -> int.

type (^) string -> string -> string.

type (~) int -> int.

type (~) float -> float.

type (i~) int -> int.

type (r~) float -> float.

type abs int -> int.

type abs float -> float.

type iabs int -> int.

type rabs float -> float.

type max int -> int -> int.

type max float -> float -> float.

type min int -> int -> int.

type min float -> float -> float.

type sqrt float -> float.

type sin float -> float.

type cos float -> float.

type arctan float -> float.

type ln float -> float.

type int_to_real int -> float.

type floor float -> int.

type ceil float -> int.

type truncate float -> int.

type size string -> int.

type chr int -> string.

type rhc string -> int.

type string_to_int string -> int.

type int_to_string int -> string.

type substring string -> int -> int -> string.

type real_to_string float -> string.

%  -- Arithmetic tests --

% [lt_ X Y] checks if X < Y. Works for string, int and float
external pred lt_ i:A, i:A.

% [gt_ X Y] checks if X > Y. Works for string, int and float
external pred gt_ i:A, i:A.

% [le_ X Y] checks if X =< Y. Works for string, int and float
external pred le_ i:A, i:A.

% [ge_ X Y] checks if X >= Y. Works for string, int and float
external pred ge_ i:A, i:A.

type (<), (>), (=<), (>=) A -> A -> prop.

X  > Y  :- gt_ X Y.

X  < Y  :- lt_ X Y.

X  =< Y :- le_ X Y.

X  >= Y :- ge_ X Y.

type (i<), (i>), (i=<), (i>=) int -> int -> prop.

X i< Y  :- lt_ X Y.

X i> Y  :- gt_ X Y.

X i=< Y :- le_ X Y.

X i>= Y :- ge_ X Y.

type (r<), (r>), (r=<), (r>=) float -> float -> prop.

X r< Y  :- lt_ X Y.

X r> Y  :- gt_ X Y.

X r=< Y :- le_ X Y.

X r>= Y :- ge_ X Y.

type (s<), (s>), (s=<), (s>=) string -> string -> prop.

X s< Y  :- lt_ X Y.

X s> Y  :- gt_ X Y.

X s=< Y :- le_ X Y.

X s>= Y :- ge_ X Y.

%  -- Standard data types (supported in the FFI) --

kind list type -> type.

type (::) X -> list X -> list X.

type ([]) list X.

% Boolean values: tt and ff since true and false are predicates
kind bool type.
type tt bool.
type ff bool.

% Pair: the constructor is pr, since ',' is for conjunction
kind pair type -> type -> type.
type pr A -> B -> pair A B.

pred fst  i:pair A B, o:A.

fst (pr A _) A.

pred snd  i:pair A B, o:B.

snd (pr _ B) B.

% The option type (aka Maybe)
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.

% Used in builtin variants that return Coq's error rather than failing
kind diagnostic type.
type ok diagnostic. % Success
type error string -> diagnostic. % Failure

%  == I/O builtins =====================================

%  -- I/O --

typeabbrev in_stream (ctype "in_stream").

type std_in in_stream.

typeabbrev out_stream (ctype "out_stream").

type std_out out_stream.
type std_err out_stream.

% [open_in FileName InStream] opens FileName for input
external pred open_in i:string, o:in_stream.

% [open_out FileName OutStream] opens FileName for output
external pred open_out i:string, o:out_stream.

% [open_append FileName OutStream] opens FileName for output in append mode
external pred open_append i:string, o:out_stream.

% [close_in InStream] closes input stream InStream
external pred close_in i:in_stream.

% [close_out OutStream] closes output stream OutStream
external pred close_out i:out_stream.

% [output OutStream Data] writes Data to OutStream
external pred output i:out_stream, i:string.

% [flush OutStream] flush all output not yet finalized to OutStream
external pred flush i:out_stream.

% [input InStream Bytes Data] reads Bytes from InStream
external pred input i:in_stream, i:int, o:string.

% [input_line InStream Line] reads a full line from InStream
external pred input_line i:in_stream, o:string.

% [eof InStream] checks if no more data can be read from InStream
external pred eof i:in_stream.

%  -- System --

% [gettimeofday T] sets T to the number of seconds elapsed since 1/1/1970
external pred gettimeofday o:float.

% [getenv VarName Value] Like Sys.getenv
external pred getenv i:string, o:option string.

% [system Command RetVal] executes Command and sets RetVal to the exit code
external pred system i:string, o:int.

%  -- Unix --

% [unix.open-process Executable Arguments Environment StdIn StdOut StdErr
% Diagnostic] OCaml's Unix.open_process_args_full.
% Note that the first argument is the executable name (as in
% argv[0]).
% Environment can be left unspecified, defaults to the current process
% environment.
% This API only works reliably since OCaml 4.12.
external pred unix.open-process i:string, i:list string, i:list string, 
                                o:out_stream, o:in_stream, o:in_stream, 
                                o:diagnostic.

% [unix.close-process StdIn StdOut StdErr Diagnostic] OCaml's
% Unix.close_process_full
external pred unix.close-process i:out_stream, i:in_stream, i:in_stream, 
                                 o:diagnostic.


kind process type.
type process out_stream -> in_stream -> in_stream -> process.

pred open-process i:list string, i:list string, o:process, o:diagnostic.
open-process Args Env (process In Out Err) Diag :-
  Args = [Cmd | _],
  unix.open-process Cmd Args Env In Out Err Diag.

pred close-process i:process, o:diagnostic.
close-process (process In Out Err) Diag :-
  unix.close-process In Out Err Diag.


%  -- Debugging --

% [term_to_string T S] prints T to S
external pred term_to_string i:any, o:string.

% == Lambda Prolog builtins =====================================

%  -- Extra I/O --

% [open_string DataIn InStream] opens DataIn as an input stream
external pred open_string i:string, o:in_stream.

% [lookahead InStream NextChar] peeks one byte from InStream
external pred lookahead i:in_stream, o:string.

%  -- Hacks --

% [string_to_term S T] parses a term T from S
external pred string_to_term i:string, o:any.

% [readterm InStream T] reads T from InStream, ends with \n
external pred readterm i:in_stream, o:any.

pred printterm i:out_stream, i:A.

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

pred read o:A.

read S :- flush std_out, input_line std_in X, string_to_term X S.

% == Elpi builtins =====================================

% [dprint ...] prints raw terms (debugging)
external type dprint variadic any prop.

% [print ...] prints terms
external type print variadic any prop.

% Deprecated, use trace.counter
pred counter i:string, o:int.
counter C N :- trace.counter C N.

% [quote_syntax FileName QueryText QuotedProgram QuotedQuery] quotes the
% program from FileName and the QueryText. See elpi-quoted_syntax.elpi for
% the syntax tree
external pred quote_syntax i:string, i:string, o:list A, o:A.

typeabbrev loc (ctype "Loc.t").


% [loc.fields Loc File StartChar StopChar Line LineStartsAtChar] Decomposes
% a loc into its fields
external pred loc.fields i:loc, o:string, o:int, o:int, o:int, o:int.

% == Regular Expressions =====================================

% [rex.match Rex Subject] checks if Subject matches Rex. Matching is based
% on OCaml's Str library
external pred rex.match i:string, i:string.

% [rex.replace Rex Replacement Subject Out] Out is obtained by replacing all
% occurrences of Rex with Replacement in Subject. See also OCaml's
% Str.global_replace
external pred rex.replace i:string, i:string, i:string, o:string.

% [rex.split Rex Subject Out] Out is obtained by splitting Subject at all
% occurrences of Rex. See also OCaml's Str.split
external pred rex.split i:string, i:string, o:list string.

% Deprecated, use rex.match
pred rex_match i:string, i:string.
rex_match Rx S :- rex.match Rx S.

% Deprecated, use rex.replace
pred rex_replace i:string, i:string, i:string, o:string.
rex_replace Rx R S O :- rex.replace Rx R S O.

% Deprecated, use rex.split
pred rex_split i:string, i:string, o:list string.
rex_split Rx S L :- rex.split Rx S L.

% == Elpi nonlogical builtins =====================================

% Opaque ML data types
kind ctyp type.
type ctype string -> ctyp.

% [var V ...] checks if the term V is a variable. When used with tree
% arguments it relates an applied variable with its head and argument list.
external type var any -> variadic any prop.

% [prune V L] V is pruned to L (V is unified with a variable that only sees
% the list of names L)
external pred prune o:any, i:list any.

% [distinct_names L] checks if L is a list of distinct names. If L is the
% scope of a unification variable (its arguments, as per var predicate) then
% distinct_names L checks that such variable is in the Miller pattern
% fragment (L_\lambda)
external pred distinct_names i:list any.

% [same_var V1 V2] checks if the two terms V1 and V2 are the same variable,
% ignoring the arguments of the variables
external pred same_var i:A, i:A.

% [same_term T1 T2] checks if the two terms T1 and T2 are syntactically
% equal (no unification). It behaves differently than same_var since it
% recursively compares the arguments of the variables
external pred same_term i:A, i:A.


% Infix notation for same_term
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.

% [constant T ...] checks if T is a (global) constant.  When used with tree
% arguments it relates an applied constant with its head and argument list.
external type constant any -> variadic any prop.

external pred names % generates the list of eigenvariable
  o:list any. % list of eigenvariables in order of age (young first)
  
external pred occurs % checks if the atom occurs in the term
  i:any, % an atom, that is a global constant or a bound name (aka eigenvariable)
  i:any. % a term
  
% [closed_term T] unify T with a variable that has no eigenvariables in
% 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.

pred primitive? i:A, i:string.

primitive? X S :- is_cdata X (ctype S).

% [new_int N] unifies N with a different int every time it is called. Values
% of N are guaranteed to be incresing.
external pred new_int o:int.

% [findall_solution P L] finds all the solved instances of P and puts them
% in L
% in the order in which they are found. Instances can contain
% eigenvariables
% and unification variables.

external pred findall_solutions i:prop, o:list prop.

% Holds data across bracktracking; can only contain closed terms
typeabbrev safe (ctype "safe").


% [new_safe Safe] creates a safe: a store that persists across backtracking
external pred new_safe o:safe.

% [stash_in_safe Safe Data] stores Data in the Safe
external pred stash_in_safe i:safe, i:A.

% [open_safe Safe Data] retrieves the Data stored in Safe
external pred open_safe i:safe, o: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.
pred if i:prop, i:prop, i:prop.
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).
pred if2 i:prop, i:prop, i:prop, i:prop, i:prop.
if2 G1 P1 _  _  _ :- G1, !, P1.
if2 _  _  G2 P2 _ :- G2, !, P2.
if2 _  _  _  _  E :- !, E. 

% [random.init Seed] Initialize OCaml's PRNG with the given Seed
external pred random.init i:int.

% [random.self_init] Initialize OCaml's PRNG with some seed
external pred random.self_init .

% [random.int Bound N] unifies N with a random int between 0 and Bound
% (excluded)
external pred random.int i:int, o:int.

#line 0 "builtin_stdlib.elpi"
% == stdlib =======================================================

% Conventions:
% - all predicates declare a mode with some input arguments, unless...
% - predicates whose name ends with R are relations (work in any direction,
%   that is all arguments are in output mode)
% - predicates whose name ends with ! do contain a cut and generate only the
%   first result
% - all errors given by this library end up calling fatal-error[-w-data],
%   override it in order to handle them differently
% - all debug prints by this library end up calling debug-print, override it
%   in order to handle them differently

namespace std {

pred fatal-error i:string.
:name "default-fatal-error"
fatal-error Msg :- halt Msg.

pred fatal-error-w-data i:string, i:A.
:name "default-fatal-error-w-data"
fatal-error-w-data Msg Data :- halt Msg ":" Data.

pred debug-print i:string, i:A.
:name "default-debug-print"
debug-print Msg Data :- print Msg Data.

%  -- Errors, Debugging, Hacks --

pred ignore-failure! i:prop.
ignore-failure! P :- P, !.
ignore-failure! _.

% [assert! C M] takes the first success of C or fails with message M 
pred assert! i:prop, i:string.
assert! Cond Msg :- (Cond ; fatal-error-w-data Msg Cond), !.

% [assert-ok! C M] like assert! but the last argument of the predicate must
% be a diagnostic that is printed after M in case it is not ok
pred assert-ok! i:(diagnostic -> prop), i:string.
assert-ok! Cond Msg :- Cond Diagnostic, !, (Diagnostic = ok ; Diagnostic = error S, fatal-error-w-data Msg S), !.
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.
spy P :- trace.counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
         debug-print "----<<---- enter: " P,
         P,
         debug-print "---->>---- exit: " P.
spy P :- debug-print "---->>---- fail: " P, fail.

% [spy! P] traces the first call to P without leaving a choice point
pred spy! i:prop.
spy! P :- trace.counter "run" NR, if (not(NR = 0)) (debug-print "run=" NR) true,
         debug-print "----<<---- enter: " P,
         P,
         debug-print "---->>---- exit: " P, !.
spy! P :- debug-print "---->>---- fail: " P, fail.

% to silence the type checker
pred unsafe-cast o:A, o:B.
unsafe-cast X X.

% -- List processing --

pred length i:list A, o:int.
length [_|L] N :- length L N1, N is N1 + 1.
length []    0.

pred rev i:list A, o:list A.
rev L RL  :- rev.aux L []  RL.
rev.aux [X|XS] ACC R :- rev.aux XS [X|ACC] R.
rev.aux [] L L.

pred last i:list A, o:A.
last [] _ :- fatal-error "last on empty list".
last [X] X :- !.
last [_|XS] R :- last XS R.

pred append i:list A, i:list A, o: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.
appendR [X|XS] L [X|L1] :- appendR XS L L1 .
appendR [] L L .

pred take i:int, i:list A, o:list A.
take 0 _ [] :- !.
take N [X|XS] [X|L] :- !, N1 is N - 1, take N1 XS L.
take _ _ _ :- fatal-error "take run out of list items".

pred take-last i:int, i:list A, o:list A.
take-last N L R :-
  length L M,
  D is M - N,
  drop D L R.

pred drop i:int, i:list A, o:list A.
drop 0 L L :- !.
drop N [_|XS] L :- !, N1 is N - 1, drop N1 XS L.
drop _ _ _ :- fatal-error "drop run out of list items".

pred drop-last i:int, i:list A, o:list A.
drop-last N L R :-
  length L M, I is M - N, take I L R.

pred split-at i:int, i:list A, o:list A, o:list A.
split-at 0 L [] L :- !.
split-at N [X|XS] [X|LN] LM :- !, N1 is N - 1, split-at N1 XS LN LM.
split-at _ _ _ _ :- fatal-error "split-at run out of list items".

pred fold i:list B, i:A, i:(B -> A -> A -> prop), o:A.
fold [] A _ A.
fold [X|XS] A F R :- F X A A1, fold XS A1 F R.

pred fold2 i:list C, i:list B, i:A, i:(C -> B -> A -> A -> prop), o:A.
fold2 [] [_|_] _ _ _ :- fatal-error "fold2 on lists of different length".
fold2 [_|_] [] _ _ _ :- fatal-error "fold2 on lists of different length".
fold2 [] [] A _ A.
fold2 [X|XS] [Y|YS] A F R :- F X Y A A1, fold2 XS YS A1 F R.

pred map i:list A, i:(A -> B -> prop), o:list B.
map [] _ [].
map [X|XS] F [Y|YS] :- F X Y, map XS F YS.

pred map-i i:list A, i:(int -> A -> B -> prop), o:list B.
map-i L F R :- map-i.aux L 0 F R.
map-i.aux [] _ _ [].
map-i.aux [X|XS] N F [Y|YS] :- F N X Y, M is N + 1, map-i.aux XS M F YS.

pred map-filter i:list A, i:(A -> B -> prop), o:list B.
map-filter [] _ [].
map-filter [X|XS] F [Y|YS] :- F X Y, !, map-filter XS F YS.
map-filter [_|XS] F YS :- map-filter XS F YS.

:index(1 1)
pred map2 i:list A, i:list B, i:(A -> B -> C -> prop), o:list C.
map2 [] [_|_] _ _ :- fatal-error "map2 on lists of different length".
map2 [_|_] [] _ _ :- fatal-error "map2 on lists of different length".
map2 [] [] _ [].
map2 [X|XS] [Y|YS] F [Z|ZS] :- F X Y Z, map2 XS YS F ZS.

pred map2-filter i:list A, i:list B, i:(A -> B -> C -> prop), o:list C.
map2-filter [] [_|_] _ _ :- fatal-error "map2-filter on lists of different length".
map2-filter [_|_] [] _ _ :- fatal-error "map2-filter on lists of different length".
map2-filter [] [] _ [].
map2-filter [X|XS] [Y|YS] F [Z|ZS] :- F X Y Z, !, map2-filter XS YS F ZS.
map2-filter [_|XS] [_|YS] F ZS :- map2-filter XS YS F ZS.

pred map-ok i:list A, i:(A -> B -> diagnostic -> prop), o:list A, o:diagnostic.
map-ok [X|L] P [Y|YS] S :- P X Y S0, if (S0 = ok) (map-ok L P YS S) (S = S0).
map-ok [] _ [] ok.

pred fold-map i:list A, i:B, i:(A -> B -> C -> B -> prop), o:list C, o:B.
fold-map [] A _ [] A.
fold-map [X|XS] A F [Y|YS] A2 :- F X A Y A1, fold-map XS A1 F YS A2.

pred omap i:option A, i:(A -> B -> prop), o:option B.
omap none _ none.
omap (some X) F (some Y) :- F X Y.

% [nth N L X] picks in X the N-th element of L (L must be of length > N)
pred nth i:int, i:list A, o:A.
nth 0 [X|_ ] R :- !, X = R.
nth N [_|XS] R :- N > 0, !, N1 is N - 1, nth N1 XS R.
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.
lookup [pr X Y|_] 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
pred lookup! i:list (pair A B), i:A, o:B.
lookup! [pr X Y|_] X Y :- !.
lookup! [_|LS]       X Y :- lookup! LS X Y.

% [mem! L X] succeeds once if X occurs inside L 
pred mem! i:list A, o: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.
mem [X|_] X.
mem [_|L] X :- mem L X.

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

pred exists2 i:list A, i:list B, i:(A -> B -> prop).
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.
exists2 [_|L] [_|M] P :- exists2 L M P.

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

pred forall-ok i:list A, i:(A -> diagnostic -> prop), o:diagnostic.
forall-ok [X|L] P S :- P X S0, if (S0 = ok) (forall-ok L P S) (S = S0).
forall-ok [] _ ok.

pred forall2 i:list A, i:list B, i:(A -> B -> prop).
forall2 [] [_|_] _ :- fatal-error "forall2 on lists of different length".
forall2 [_|_] [] _ :- fatal-error "forall2 on lists of different length".
forall2 [X|XS] [Y|YS] P :- P X Y, forall2 XS YS P.
forall2 [] [] _.

pred filter i:list A, i:(A -> prop), o:list A.
filter []    _ [].
filter [X|L] P R :- if (P X) (R = X :: L1) (R = L1), filter L P L1.

pred zip i:list A, i:list B, o:list (pair A B).
zip [_|_] [] _ :- fatal-error "zip on lists of different length".
zip [] [_|_] _ :- fatal-error "zip on lists of different length".
zip [X|LX] [Y|LY] [pr X Y|LR] :- zip LX LY LR.
zip [] [] [].

pred unzip i:list (pair A B), o:list A, o:list B.
unzip [] [] [].
unzip [pr X Y|L] [X|LX] [Y|LY] :- unzip L LX LY.

pred flatten i:list (list A), o:list A.
flatten [X|LS] R :- flatten LS LS', append X LS' R.
flatten []     [].

pred null i:list A.
null [].

pred iota i:int, o:list int.
iota N L :- iota.aux 0 N L.
iota.aux X X [] :- !.
iota.aux N X [N|R] :- M is N + 1, iota.aux M X R.

% [intersperse X L R] R is [L0, X, ..., X, LN]
:index(_ 1)
pred intersperse i:A, i:list A, o:list A.
intersperse _ [] [].
intersperse _ [X] [X] :- !.
intersperse Sep [X|XS] [X,Sep|YS] :- intersperse Sep XS YS.

%  -- Misc --

pred flip i:(A -> B -> prop), i:B, i:A.
flip P X Y :- P Y X.

pred time i:prop, o:float.
time P T :- gettimeofday Before, P, gettimeofday After, T is After - Before.

pred do! i:list prop.
do! [].
do! [P|PS] :- P, !, do! PS.

:index(_ 1)
pred do-ok! o:diagnostic, i:list (diagnostic -> prop).
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.
lift-ok P Msg R :- (P, R = ok; R = error Msg).

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

pred while-ok-do! i:diagnostic, i:list (diagnostic -> prop), o: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.

pred any->string i:A, o:string.
any->string X Y :- term_to_string X Y.

pred max i:A, i:A, o:A.
max N M N :- N >= M, !.
max _ M M.

% [findall P L] L is the list [P1,P2,P3..] where each Pi is a solution to P.
pred findall i:prop, o:list prop.
findall P L :- findall_solutions P L.

}

% [std.string.concat Separator Items Result] concatenates Items
% interspersing Separator
external pred std.string.concat i:string, i:list string, o:string.

% CAVEAT: the type parameter of std.string.map must be a closed term

kind std.string.map type -> type.

% [std.string.map.empty M] The empty map
external pred std.string.map.empty o:std.string.map A.

% [std.string.map.mem S M] Checks if S is bound in M
external pred std.string.map.mem i:string, i:std.string.map A.

% [std.string.map.add S V M M1] M1 is M where V is bound to S
external pred std.string.map.add i:string, i:A, i:std.string.map A, 
                                 o:std.string.map A.

% [std.string.map.remove S M M1] M1 is M where S is unbound
external pred std.string.map.remove i:string, i:std.string.map A, 
                                    o:std.string.map A.

% [std.string.map.find S M V] V is the binding of S in M
external pred std.string.map.find i:string, i:std.string.map A, o:A.

% [std.string.map.bindings M L] L is M transformed into an associative list
external pred std.string.map.bindings i:std.string.map A, 
                                      o:list (pair string A).

% CAVEAT: the type parameter of std.int.map must be a closed term

kind std.int.map type -> type.

% [std.int.map.empty M] The empty map
external pred std.int.map.empty o:std.int.map A.

% [std.int.map.mem S M] Checks if S is bound in M
external pred std.int.map.mem i:int, i:std.int.map A.

% [std.int.map.add S V M M1] M1 is M where V is bound to S
external pred std.int.map.add i:int, i:A, i:std.int.map A, 
                              o:std.int.map A.

% [std.int.map.remove S M M1] M1 is M where S is unbound
external pred std.int.map.remove i:int, i:std.int.map A, o:std.int.map A.

% [std.int.map.find S M V] V is the binding of S in M
external pred std.int.map.find i:int, i:std.int.map A, o:A.

% [std.int.map.bindings M L] L is M transformed into an associative list
external pred std.int.map.bindings i:std.int.map A, o:list (pair int A).

% CAVEAT: the type parameter of std.loc.map must be a closed term

kind std.loc.map type -> type.

% [std.loc.map.empty M] The empty map
external pred std.loc.map.empty o:std.loc.map A.

% [std.loc.map.mem S M] Checks if S is bound in M
external pred std.loc.map.mem i:loc, i:std.loc.map A.

% [std.loc.map.add S V M M1] M1 is M where V is bound to S
external pred std.loc.map.add i:loc, i:A, i:std.loc.map A, 
                              o:std.loc.map A.

% [std.loc.map.remove S M M1] M1 is M where S is unbound
external pred std.loc.map.remove i:loc, i:std.loc.map A, o:std.loc.map A.

% [std.loc.map.find S M V] V is the binding of S in M
external pred std.loc.map.find i:loc, i:std.loc.map A, o:A.

% [std.loc.map.bindings M L] L is M transformed into an associative list
external pred std.loc.map.bindings i:std.loc.map A, o:list (pair loc A).

kind std.string.set type.

% [std.string.set.empty A] The empty set
external pred std.string.set.empty o:std.string.set.

% [std.string.set.mem Elem A] Checks if Elem is in a
external pred std.string.set.mem i:string, i:std.string.set.

% [std.string.set.add Elem A B] B is A union {Elem}
external pred std.string.set.add i:string, i:std.string.set, 
                                 o:std.string.set.

% [std.string.set.remove Elem A B] B is A \ {Elem}
external pred std.string.set.remove i:string, i:std.string.set, 
                                    o:std.string.set.

% [std.string.set.union A B X] X is A union B
external pred std.string.set.union i:std.string.set, i:std.string.set, 
                                   o:std.string.set.

% [std.string.set.inter A B X] X is A intersection B
external pred std.string.set.inter i:std.string.set, i:std.string.set, 
                                   o:std.string.set.

% [std.string.set.diff A B X] X is A \ B
external pred std.string.set.diff i:std.string.set, i:std.string.set, 
                                  o:std.string.set.

% [std.string.set.equal A B] tests A and B for equality
external pred std.string.set.equal i:std.string.set, i:std.string.set.

% [std.string.set.subset A B] tests if A is a subset of B
external pred std.string.set.subset i:std.string.set, i:std.string.set.

% [std.string.set.elements M L] L is M transformed into list
external pred std.string.set.elements i:std.string.set, o:list string.

% [std.string.set.cardinal M N] N is the number of elements of M
external pred std.string.set.cardinal i:std.string.set, o:int.

kind std.int.set type.

% [std.int.set.empty A] The empty set
external pred std.int.set.empty o:std.int.set.

% [std.int.set.mem Elem A] Checks if Elem is in a
external pred std.int.set.mem i:int, i:std.int.set.

% [std.int.set.add Elem A B] B is A union {Elem}
external pred std.int.set.add i:int, i:std.int.set, o:std.int.set.

% [std.int.set.remove Elem A B] B is A \ {Elem}
external pred std.int.set.remove i:int, i:std.int.set, o:std.int.set.

% [std.int.set.union A B X] X is A union B
external pred std.int.set.union i:std.int.set, i:std.int.set, 
                                o:std.int.set.

% [std.int.set.inter A B X] X is A intersection B
external pred std.int.set.inter i:std.int.set, i:std.int.set, 
                                o:std.int.set.

% [std.int.set.diff A B X] X is A \ B
external pred std.int.set.diff i:std.int.set, i:std.int.set, 
                               o:std.int.set.

% [std.int.set.equal A B] tests A and B for equality
external pred std.int.set.equal i:std.int.set, i:std.int.set.

% [std.int.set.subset A B] tests if A is a subset of B
external pred std.int.set.subset i:std.int.set, i:std.int.set.

% [std.int.set.elements M L] L is M transformed into list
external pred std.int.set.elements i:std.int.set, o:list int.

% [std.int.set.cardinal M N] N is the number of elements of M
external pred std.int.set.cardinal i:std.int.set, o:int.

kind std.loc.set type.

% [std.loc.set.empty A] The empty set
external pred std.loc.set.empty o:std.loc.set.

% [std.loc.set.mem Elem A] Checks if Elem is in a
external pred std.loc.set.mem i:loc, i:std.loc.set.

% [std.loc.set.add Elem A B] B is A union {Elem}
external pred std.loc.set.add i:loc, i:std.loc.set, o:std.loc.set.

% [std.loc.set.remove Elem A B] B is A \ {Elem}
external pred std.loc.set.remove i:loc, i:std.loc.set, o:std.loc.set.

% [std.loc.set.union A B X] X is A union B
external pred std.loc.set.union i:std.loc.set, i:std.loc.set, 
                                o:std.loc.set.

% [std.loc.set.inter A B X] X is A intersection B
external pred std.loc.set.inter i:std.loc.set, i:std.loc.set, 
                                o:std.loc.set.

% [std.loc.set.diff A B X] X is A \ B
external pred std.loc.set.diff i:std.loc.set, i:std.loc.set, 
                               o:std.loc.set.

% [std.loc.set.equal A B] tests A and B for equality
external pred std.loc.set.equal i:std.loc.set, i:std.loc.set.

% [std.loc.set.subset A B] tests if A is a subset of B
external pred std.loc.set.subset i:std.loc.set, i:std.loc.set.

% [std.loc.set.elements M L] L is M transformed into list
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


% == Elpi runtime builtins =====================================

% [trace.counter Name Value] reads the Value of a trace point Name
external pred trace.counter i:string, o:int.

% [gc.get MinorHeapSize MajorHeapIncrement SpaceOverhead Verbose MaxOverhead
% StackLimit AllocationPolicy WindowSize] Reads the current settings of the
% garbage collector. See also OCaml's Gc.control type documentation.
external pred gc.get o:int, o:int, o:int, o:int, o:int, o:int, o:int, 
                     o:int.

% [gc.set MinorHeapSize MajorHeapIncrement SpaceOverhead Verbose MaxOverhead
% StackLimit AllocationPolicy WindowSize] Writes the current settings of the
% garbage collector. Any parameter left unspecificed (eg _) is not changed.
% See also OCaml's Gc.control type documentation.
external pred gc.set i:int, i:int, i:int, i:int, i:int, i:int, i:int, 
                     i:int.

% [gc.minor] See OCaml's Gc.minor documentation.
external pred gc.minor .

% [gc.major] See OCaml's Gc.major documentation.
external pred gc.major .

% [gc.full] See OCaml's Gc.full_major documentation.
external pred gc.full .

% [gc.compact] See OCaml's Gc.compact documentation.
external pred gc.compact .

% [gc.stat MinorWords PromotedWords MajorWords MinorCollections
% MajorCollections HeapWords HeapChunks LiveWords LiveBlocks FreeWords
% FreeBlocks LargestFree Fragments Compactions TopHeapWords StackSize] See
% OCaml's Gc.stat documentation.
external pred gc.stat o:float, o:float, o:float, o:int, o:int, o:int, 
                      o:int, o:int, o:int, o:int, o:int, o:int, o:int, 
                      o:int, o:int, o:int.

% [gc.quick-stat MinorWords PromotedWords MajorWords MinorCollections
% MajorCollections HeapWords HeapChunks Compactions TopHeapWords StackSize]
% See OCaml's Gc.quick_stat documentation.
external pred gc.quick-stat o:float, o:float, o:float, o:int, o:int, 
                            o:int, o:int, o:int, o:int, o:int.