builtin.elpi

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

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

%  -- Logic --

func true.

true.

func fail.

func false.


% [X = T] unifies X with Y, possibly assigning unification
% variables in X and Y.
external func (=) -> A, A.

% [pattern_matching T P] matches T against pattern P, only
% variables in P are assigned.
external func pattern_match A -> A.

external func (pi) (func A).

external func (sigma) (func A).

kind int type.


kind string type.


kind float type.


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

(A ; _) :- A.

(_ ; B) :- B.

external symbol (:-)  : (func) -> (func) -> (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 (=>)  : (pred) -> (func) -> (func) = "core".

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

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

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

%  -- Control --

external func !. % The cut operator

func not prop.

not X :- X, !, fail.

not _.

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

% [print_constraints] prints all constraints
external func print_constraints.

% [halt ...] halts the program and print the terms
external type halt variadic any (func).

func stop.

stop :- halt.

%  -- Evaluation --

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

X is Y :- calc Y X.

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

%  --- Operators ---

external symbol (-) : A -> A -> A = "1". 

external symbol (i-) : int -> int -> int = "1". 

external symbol (r-) : float -> float -> float = "1". 

external symbol (+) : float -> float -> float = "2". 

external symbol (+) : int -> int -> int = "1". 

external symbol (i+) : int -> int -> int = "1". 

external symbol (r+) : float -> float -> float = "1". 

external symbol (*) : float -> float -> float = "2". 

external symbol (*) : int -> int -> int = "1". 

external symbol (/) : float -> float -> float = "1". 

external symbol (mod) : int -> int -> int = "1". 

external symbol (div) : int -> int -> int = "1". 

external symbol (^) : string -> string -> string = "1". 

external symbol (~) : float -> float = "2". 

external symbol (~) : int -> int = "1". 

external symbol (i~) : int -> int = "1". 

external symbol (r~) : float -> float = "1". 

external symbol abs : float -> float = "2".

external symbol abs : int -> int = "1".

external symbol iabs : int -> int = "1".

external symbol rabs : float -> float = "1".

external symbol max : float -> float -> float = "2".

external symbol max : int -> int -> int = "1".

external symbol min : float -> float -> float = "2".

external symbol min : int -> int -> int = "1".

external symbol sqrt : float -> float = "1".

external symbol sin : float -> float = "1".

external symbol cos : float -> float = "1".

external symbol arctan : float -> float = "1".

external symbol ln : float -> float = "1".

external symbol int_to_real : int -> float = "1".

external symbol floor : float -> int = "1".

external symbol ceil : float -> int = "1".

external symbol truncate : float -> int = "1".

external symbol size : string -> int = "1".

external symbol chr : int -> string = "1".

external symbol rhc : string -> int = "1".

external symbol string_to_int : string -> int = "1".

external symbol int_to_string : int -> string = "1".

external symbol substring : string -> int -> int -> string = "1".

external symbol real_to_string : float -> string = "1".

%  -- Arithmetic tests --

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

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

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

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

func (>) A, A.
X > Y :- gt_ X Y.

func (<) A, A.
X < Y :- lt_ X Y.

func (=<) A, A.
X =< Y :- le_ X Y.

func (>=) A, A.
X >= Y :- ge_ X Y.

func (i>) int, int.
X i> Y :- gt_ X Y.

func (i<) int, int.
X i< Y :- lt_ X Y.

func (i=<) int, int.
X i=< Y :- le_ X Y.

func (i>=) int, int.
X i>= Y :- ge_ X Y.

func (r>) float, float.
X r> Y :- gt_ X Y.

func (r<) float, float.
X r< Y :- lt_ X Y.

func (r=<) float, float.
X r=< Y :- le_ X Y.

func (r>=) float, float.
X r>= Y :- ge_ X Y.

func (s>) string, string.
X s> Y :- gt_ X Y.

func (s<) string, string.
X s< Y :- lt_ X Y.

func (s=<) string, string.
X s=< Y :- le_ X Y.

func (s>=) string, string.
X s>= Y :- ge_ X Y.

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

kind list type -> type.

external symbol (::) : X -> list X -> list X = "core".

external symbol ([]) : list X = "core".

% Boolean values: tt and ff since true and false are predicates
kind bool type.
external symbol tt : bool = "1". 
external symbol ff : bool = "1". 

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

func fst  pair A B -> A.

fst (pr A _) A.

func snd  pair A B -> B.

snd (pr _ B) B.


kind triple type -> type -> type -> type.
type triple A -> B -> C -> triple A B C.

func triple_1 triple A B C -> A.
triple_1 (triple A _ _) A.

func triple_2 triple A B C -> B.
triple_2 (triple _ B _) B.

func triple_3 triple A B C -> C.
triple_3 (triple _ _ C) C.



% The option type (aka Maybe)
kind option type -> type.
external symbol none : option A = "1". 
external symbol some : A -> option A = "1". 

% Result of a comparison
kind cmp type.
external symbol eq : cmp = "1". 
external symbol lt : cmp = "1". 
external symbol gt : cmp = "1". 

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

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

%  -- I/O --

kind in_stream type.

external symbol std_in : in_stream = "1".

kind out_stream type.

external symbol std_err : out_stream = "1".
external symbol std_out : out_stream = "1".

% [open_in FileName InStream] opens FileName for input
external func open_in string -> in_stream.

% [open_out FileName OutStream] opens FileName for output
external func open_out string -> out_stream.

% [open_append FileName OutStream] opens FileName for output in append mode
external func open_append string -> out_stream.

% [close_in InStream] closes input stream InStream
external func close_in in_stream.

% [close_out OutStream] closes output stream OutStream
external func close_out out_stream.

% [output OutStream Data] writes Data to OutStream
external func output out_stream, string.

% [flush OutStream] flush all output not yet finalized to OutStream
external func flush out_stream.

% [input InStream Bytes Data] reads Bytes from InStream
external func input in_stream, int -> string.

% [input_line InStream Line] reads a full line from InStream
external func input_line in_stream -> string.

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

%  -- System --

% [gettimeofday T] sets T to the number of seconds elapsed since 1/1/1970
external func gettimeofday -> float.

% [sys.file_exists Path] is like [Sys.file_exists]. It succeeds if the file
% at [Path] exists
external func sys.file_exists string.

% [sys.is_directory Path Diagnostic] is like [Sys.is_directory]. It succeeds
% if [Diagnostic = ok] and [Path] is a directory or [Diagnostic = error Msg]
% and [Msg] describes an encountered system error.
external func sys.is_directory string -> diagnostic.

% [sys.remove Path Diagnostic] is like [Sys.remove]. It succeeds if
% [Diagnostic = ok] and the file at [Path] is removed or [Diagnostic = error
% Msg] and [Msg] describes an encountered system error.
external func sys.remove string -> diagnostic.

% [sys.rename OldPath NewPath Diagnostic] is like [Sys.rename]. It succeeds
% if [Diagnostic = ok] and the file at [OldPath] is renamed to [NewPath] or
% [Diagnostic = error Msg] and [Msg] describes an encountered system error.
external func sys.rename string, string -> diagnostic.

% [getenv VarName Value] Like Sys.getenv_opt
external func getenv string -> option string.

% [system Command RetVal] executes Command and sets RetVal to the exit code
external func system string -> int.

% [sys.chdir DirPath Diagnostic] is like [Sys.chdir]. It succeeds if
% [Diagnostic = ok] and the current working directory is updated to
% [DirPath] or [Diagnostic = error Msg] and [Msg] describes an encountered
% system error.
external func sys.chdir string -> diagnostic.

% [sys.mkdir DirPath Permissions Diagnostic] is like [Sys.mkdir]. It
% succeeds if [Diagnostic = ok] and the directory [DirPath] is created or
% [Diagnostic = error Msg] and [Msg] describes an encountered system error.
external func sys.mkdir string, int -> diagnostic.

% [sys.rmdir DirPath Diagnostic] is like [Sys.rmdir]. It succeeds if
% [Diagnostic = ok] and the directory [DirPath] is removed or [Diagnostic =
% error Msg] and [Msg] describes an encountered system error.
external func sys.rmdir string -> diagnostic.

% [sys.getcwd DirPath Diagnostic] is like [Sys.getcwd]. It succeeds if
% [Diagnostic = ok] and [DirPath] is the current working directory or
% [Diagnostic = error Msg] and [Msg] describes an encountered system error.
external func sys.getcwd -> string, diagnostic.

% [sys.readdir DirPath Contents Diagnostic] is like [Sys.readdir]. It
% succeeds if [Diagnostic = ok] and [Contents] is the list of files in
% [DirPath] or [Diagnostic = error Msg] and [Msg] describes an encountered
% system error.
external func sys.readdir string -> list string, diagnostic.

%  -- Unix --

% gathers the standard file descriptors or a process
kind unix.process type.
external symbol unix.process : out_stream -> in_stream -> in_stream ->
                               unix.process = "1". 

% [unix.process.open Executable Arguments Environment P Diagnostic] OCaml's
% Unix.open_process_args_full.
% Note that the first argument is the executable name (as in argv[0]).
% If Executable is omitted it defaults to the first element of
% Arguments.
% Environment can be left unspecified, defaults to the current process
% environment.
% This API only works reliably since OCaml 4.12.
external func unix.process.open string, list string, 
                               list string -> unix.process, diagnostic.

% [unix.process.close P Diagnostic] OCaml's Unix.close_process_full
external func unix.process.close unix.process -> diagnostic.

%  -- Debugging --

% [term_to_string T S] prints T to S
external func term_to_string -> any, string.

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

%  -- Extra I/O --

% [open_string DataIn InStream] opens DataIn as an input stream
external func open_string string -> in_stream.

% [lookahead InStream NextChar] peeks one byte from InStream
external func lookahead in_stream -> string.

pred printterm out_stream, A.

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

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

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

% [print ...] prints terms
external type print variadic any (func).

% Deprecated, use trace.counter
func counter string -> int.
counter C N :- trace.counter C N.

kind loc type.


% [loc.fields Loc File StartChar StopChar Line LineStartsAtChar] Decomposes
% a loc into its fields
external func loc.fields loc -> string, int, int, int, int.

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

% [rex.match Rex Subject] checks if Subject matches Rex. Matching is based
% on OCaml's Str library
external func rex.match string, 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 func rex.replace string, string, string -> string.

% [rex.split Rex Subject Out] Out is obtained by splitting Subject at all
% occurrences of Rex. See also OCaml's Str.split
external func rex.split string, string -> list string.

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

% Deprecated, use rex.replace
func rex_replace string, string, string -> string.
rex_replace Rx R S O :- rex.replace Rx R S O.

% Deprecated, use rex.split
func rex_split string, string -> list string.
rex_split Rx S L :- rex.split Rx S L.

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

% [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 func var -> any, any.. .


% [prune V L] V is pruned to L (V is unified with a variable that only sees
% the list of names L)
:functional :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 func distinct_names 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 func same_var A, 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 func same_term A, A.


% 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.


% [cmp_term A B Cmp] Compares A and B. Only works if A and B are ground.
external func cmp_term any, any -> 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 func name -> any, any.. .

% [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 func constant -> any, any.. .

external func names % generates the list of eigenvariable
  -> list any. % list of eigenvariables in order of age (young first)
  
external func occurs % checks if the atom occurs in the term
  any,  % an atom, that is a global constant or a bound name (aka eigenvariable)
  any.  % a term
  
% [closed_term T] unify T with a variable that has no eigenvariables in
% scope
external func closed_term -> any.

% [ground_term T] Checks if T contains unification variables
external func ground_term any.

% [is_cdata T Ctype] checks if T is primitive of type Ctype, eg "int"
external func is_cdata any -> string.

func primitive? any, string.

primitive? X S :- is_cdata X S.

% [new_int N] unifies N with a different int every time it is called. Values
% of N are guaranteed to be incresing.
external func new_int -> 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. P may or may not be
% instantiated. Instances should be found in L.

external func findall_solutions prop -> list prop.

% Holds data across bracktracking; can only contain closed terms
kind safe type.


% [new_safe Safe] creates a safe: a store that persists across backtracking
external func new_safe -> safe.

% [stash_in_safe Safe Data] stores Data in the Safe
external func stash_in_safe safe, A.

% [open_safe Safe Data] retrieves the Data stored in Safe
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 (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 (pred), (func), (pred), (func), (func).
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 func random.init int.

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

% [random.int Bound N] unifies N with a random int between 0 and Bound
% (excluded)
external func random.int int -> int.

#line 1 "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 {

func fatal-error string.
:name "default-fatal-error"
fatal-error Msg :- halt Msg.

func fatal-error-w-data string, any.
:name "default-fatal-error-w-data"
fatal-error-w-data Msg Data :- halt Msg ":" Data.

func debug-print string, any.
:name "default-debug-print"
debug-print Msg Data :- print Msg Data.

%  -- Errors, Debugging, Hacks --

func ignore-failure! prop ->.
ignore-failure! P :- P, !.
ignore-failure! _.

func once prop ->.
once P :- P, !.

% [assert! C M] takes the first success of C or fails with message M 
func assert! prop, 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
func assert-ok! (pred o:diagnostic), 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 (pred).
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
func spy! 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
func unsafe-cast A -> B.
:untyped unsafe-cast X X.

% -- List processing --

func length list A -> int.
length [_|L] N :- length L N1, N is N1 + 1.
length []    0.

func rev list A -> list A.
rev L RL  :- rev-append L []  RL.

func rev-append list A, list A -> list A.
rev-append [X|XS] ACC R :- rev-append XS [X|ACC] R.
rev-append [] L L.

func rev.aux list A, list A -> list A.
rev.aux L1 L2 L3 :- rev-append L1 L2 L3.

func last list A -> A.
last [] _ :- fatal-error "last on empty list".
last [X] X :- !.
last [_|XS] R :- last XS R.

func append list A, list A -> list A.
append [X|XS] L [X|L1] :- append XS L L1 .
append [] L L .

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

func take int, list A -> 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".

func take-last int, list A -> list A.
take-last N L R :-
  length L M,
  D is M - N,
  drop D L R.

func drop int, list A -> 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".

func drop-last int, list A -> list A.
drop-last N L R :-
  length L M, I is M - N, take I L R.

func split-at int, list A -> list A, 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".

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

func fold-right list B, A, (func B, A -> A) -> A.
fold-right [] A _ A.
fold-right [X|XS] A F R :- fold-right XS A F A', F X A' R.

:index (1 1)
func fold2 list C, list B, A, (func C, B, A -> A) -> 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.

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

func map-i list A, (func int, A -> B) -> list B.
map-i L F R :- map-i.aux L 0 F R.

func map-i.aux list A, int, (func int, A -> B) -> list B.
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.

func map-filter list A, (func A -> B) -> 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)
func map2 list A, list B, (func A, B -> C) -> 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.

func map2-filter list A, list B, (func A, B -> C) -> 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.

func map-ok list A, (func A -> B, diagnostic) -> list B, 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.

func fold-map list A, B, (func A, B -> C, B) -> list C, 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.

func omap option A, (func A -> B) -> 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)
func nth int, list A -> 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 list (pair A B), A -> 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
func lookup! list (pair A B), A -> 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 
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 list A -> A.
mem [X|_] X.
mem [_|L] X :- mem L X.

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

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

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.
exists2 [_|L] [_|M] P :- exists2 L M P.

func forall list A, (func A).
forall [] _.
forall [X|L] P :- P X, forall L P.

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

func forall2 list A, list B, (func A, B).
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 [] [] _.

func filter list A, (func A) -> list A.
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 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.


func zip list A, list B -> 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 [] [] [].

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

func flatten list (list A) -> list A.
flatten [X|LS] R :- flatten LS LS', append X LS' R.
flatten []     [].

func null list A.
null [].

% [make N E L] L is [E, ..., E] and L has length N
func list.make int, A -> list A.
list.make 0 _ [] :- !.
list.make N E [E|L] :- N' is N - 1, list.make N' E L.

% [init N F L] L is [F 0, ..., F (N-1)]
func list.init int, (func int -> A) -> list A.
list.init N F L :- assert! (N >= 0) ("list.init: negative length"), list.init.aux 0 N F L.

func list.init.aux int, int, (func int -> A) -> list A.
list.init.aux N N _ [] :- !.
list.init.aux N M F [E|L] :- F N E, N' is N + 1, list.init.aux N' M F L.

func iota int -> list int.
iota N L :- list.init N (x\y\ x = y) L.

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

%  -- Misc --

func flip (func A, B), B, A.
flip P X Y :- P Y X.

func time (func) -> float.
time P T :- gettimeofday Before, P, gettimeofday After, T is After - Before.

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

:index(_ 1)
:functional
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 (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 -> 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.

func any->string A -> string.
any->string X Y :- term_to_string X Y.

func max A, A -> 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.
func findall prop -> list prop.
findall P L :- findall_solutions P L.

}

% [std.string.concat Separator Items Result] concatenates Items
% interspersing Separator
external func std.string.concat string, list string -> 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 func std.string.map.empty -> std.string.map A.

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

% [std.string.map.add S V M M1] M1 is M where V is bound to S
external func std.string.map.add string, A, 
                                std.string.map A -> std.string.map A.

% [std.string.map.remove S M M1] M1 is M where S is unbound
external func std.string.map.remove string, 
                                   std.string.map A -> std.string.map A.

% [std.string.map.find S M V] V is the binding of S in M
external func std.string.map.find string, std.string.map A -> A.

% [std.string.map.bindings M L] L is M transformed into an associative list
external func std.string.map.bindings std.string.map A -> list (pair string A).

% [std.string.map.filter M F M1] Filter M w.r.t. the predicate F
external func std.string.map.filter std.string.map A, 
                                   (string -> A -> prop) -> std.string.map A.

% [std.string.map.map M F M1] Map M w.r.t. the predicate F
external func std.string.map.map std.string.map A, 
                                (string -> A -> B -> prop) -> std.string.map B.

% [std.string.map.fold M Acc F Acc1] fold M w.r.t. the predicate F
external func std.string.map.fold std.string.map A, C, 
                                 (string -> A -> C -> C -> prop) -> C.

% 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 func std.int.map.empty -> std.int.map A.

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

% [std.int.map.add S V M M1] M1 is M where V is bound to S
external func std.int.map.add int, A, std.int.map A -> std.int.map A.

% [std.int.map.remove S M M1] M1 is M where S is unbound
external func std.int.map.remove int, std.int.map A -> std.int.map A.

% [std.int.map.find S M V] V is the binding of S in M
external func std.int.map.find int, std.int.map A -> A.

% [std.int.map.bindings M L] L is M transformed into an associative list
external func std.int.map.bindings std.int.map A -> list (pair int A).

% [std.int.map.filter M F M1] Filter M w.r.t. the predicate F
external func std.int.map.filter std.int.map A, 
                                (int -> A -> prop) -> std.int.map A.

% [std.int.map.map M F M1] Map M w.r.t. the predicate F
external func std.int.map.map std.int.map A, 
                             (int -> A -> B -> prop) -> std.int.map B.

% [std.int.map.fold M Acc F Acc1] fold M w.r.t. the predicate F
external func std.int.map.fold std.int.map A, C, 
                              (int -> A -> C -> C -> prop) -> C.

% 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 func std.loc.map.empty -> std.loc.map A.

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

% [std.loc.map.add S V M M1] M1 is M where V is bound to S
external func std.loc.map.add loc, A, std.loc.map A -> std.loc.map A.

% [std.loc.map.remove S M M1] M1 is M where S is unbound
external func std.loc.map.remove loc, std.loc.map A -> std.loc.map A.

% [std.loc.map.find S M V] V is the binding of S in M
external func std.loc.map.find loc, std.loc.map A -> A.

% [std.loc.map.bindings M L] L is M transformed into an associative list
external func std.loc.map.bindings std.loc.map A -> list (pair loc A).

% [std.loc.map.filter M F M1] Filter M w.r.t. the predicate F
external func std.loc.map.filter std.loc.map A, 
                                (loc -> A -> prop) -> std.loc.map A.

% [std.loc.map.map M F M1] Map M w.r.t. the predicate F
external func std.loc.map.map std.loc.map A, 
                             (loc -> A -> B -> prop) -> std.loc.map B.

% [std.loc.map.fold M Acc F Acc1] fold M w.r.t. the predicate F
external func std.loc.map.fold std.loc.map A, C, 
                              (loc -> A -> C -> C -> prop) -> C.

kind std.string.set type.

% [std.string.set.empty A] The empty set
external func std.string.set.empty -> std.string.set.

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

% [std.string.set.add Elem A B] B is A union {Elem}
external func std.string.set.add string, std.string.set -> std.string.set.

% [std.string.set.remove Elem A B] B is A \ {Elem}
external func std.string.set.remove string, 
                                   std.string.set -> std.string.set.

% [std.string.set.union A B X] X is A union B
external func std.string.set.union std.string.set, 
                                  std.string.set -> std.string.set.

% [std.string.set.inter A B X] X is A intersection B
external func std.string.set.inter std.string.set, 
                                  std.string.set -> std.string.set.

% [std.string.set.diff A B X] X is A \ B
external func std.string.set.diff std.string.set, 
                                 std.string.set -> std.string.set.

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

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

% [std.string.set.elements M L] L is M transformed into list
external func std.string.set.elements std.string.set -> list string.

% [std.string.set.choose M X] X is an element of M
external func std.string.set.choose std.string.set -> string.

% [std.string.set.min M X] X is the smallest element of M
external func std.string.set.min std.string.set -> string.

% [std.string.set.max M X] X is the bigger of M
external func std.string.set.max std.string.set -> string.

% [std.string.set.cardinal M N] N is the number of elements of M
external func std.string.set.cardinal std.string.set -> int.

% [std.string.set.filter M F M1] Filter M w.r.t. the predicate F
external func std.string.set.filter std.string.set, 
                                   (string -> (func)) -> std.string.set.

% [std.string.set.map M F M1] Map M w.r.t. the predicate F
external func std.string.set.map std.string.set, 
                                (string -> string -> prop) -> std.string.set.

% [std.string.set.fold M Acc F Acc1] fold M w.r.t. the predicate F
external func std.string.set.fold std.string.set, A, 
                                 (string -> A -> A -> prop) -> A.

% [std.string.set.partition M F M1 M2] Partitions M w.r.t. the predicate F,
% M1 is where F holds
external func std.string.set.partition std.string.set, 
                                      (string -> (func)) -> std.string.set, 
                                      std.string.set.

kind std.int.set type.

% [std.int.set.empty A] The empty set
external func std.int.set.empty -> std.int.set.

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

% [std.int.set.add Elem A B] B is A union {Elem}
external func std.int.set.add int, std.int.set -> std.int.set.

% [std.int.set.remove Elem A B] B is A \ {Elem}
external func std.int.set.remove int, std.int.set -> std.int.set.

% [std.int.set.union A B X] X is A union B
external func std.int.set.union std.int.set, std.int.set -> std.int.set.

% [std.int.set.inter A B X] X is A intersection B
external func std.int.set.inter std.int.set, std.int.set -> std.int.set.

% [std.int.set.diff A B X] X is A \ B
external func std.int.set.diff std.int.set, std.int.set -> std.int.set.

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

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

% [std.int.set.elements M L] L is M transformed into list
external func std.int.set.elements std.int.set -> list int.

% [std.int.set.choose M X] X is an element of M
external func std.int.set.choose std.int.set -> int.

% [std.int.set.min M X] X is the smallest element of M
external func std.int.set.min std.int.set -> int.

% [std.int.set.max M X] X is the bigger of M
external func std.int.set.max std.int.set -> int.

% [std.int.set.cardinal M N] N is the number of elements of M
external func std.int.set.cardinal std.int.set -> int.

% [std.int.set.filter M F M1] Filter M w.r.t. the predicate F
external func std.int.set.filter std.int.set, 
                                (int -> (func)) -> std.int.set.

% [std.int.set.map M F M1] Map M w.r.t. the predicate F
external func std.int.set.map std.int.set, 
                             (int -> int -> prop) -> std.int.set.

% [std.int.set.fold M Acc F Acc1] fold M w.r.t. the predicate F
external func std.int.set.fold std.int.set, A, 
                              (int -> A -> A -> prop) -> A.

% [std.int.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
% is where F holds
external func std.int.set.partition std.int.set, 
                                   (int -> (func)) -> std.int.set, 
                                   std.int.set.

kind std.loc.set type.

% [std.loc.set.empty A] The empty set
external func std.loc.set.empty -> std.loc.set.

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

% [std.loc.set.add Elem A B] B is A union {Elem}
external func std.loc.set.add loc, std.loc.set -> std.loc.set.

% [std.loc.set.remove Elem A B] B is A \ {Elem}
external func std.loc.set.remove loc, std.loc.set -> std.loc.set.

% [std.loc.set.union A B X] X is A union B
external func std.loc.set.union std.loc.set, std.loc.set -> std.loc.set.

% [std.loc.set.inter A B X] X is A intersection B
external func std.loc.set.inter std.loc.set, std.loc.set -> std.loc.set.

% [std.loc.set.diff A B X] X is A \ B
external func std.loc.set.diff std.loc.set, std.loc.set -> std.loc.set.

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

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

% [std.loc.set.elements M L] L is M transformed into list
external func std.loc.set.elements std.loc.set -> list loc.

% [std.loc.set.choose M X] X is an element of M
external func std.loc.set.choose std.loc.set -> loc.

% [std.loc.set.min M X] X is the smallest element of M
external func std.loc.set.min std.loc.set -> loc.

% [std.loc.set.max M X] X is the bigger of M
external func std.loc.set.max std.loc.set -> loc.

% [std.loc.set.cardinal M N] N is the number of elements of M
external func std.loc.set.cardinal std.loc.set -> int.

% [std.loc.set.filter M F M1] Filter M w.r.t. the predicate F
external func std.loc.set.filter std.loc.set, 
                                (loc -> (func)) -> std.loc.set.

% [std.loc.set.map M F M1] Map M w.r.t. the predicate F
external func std.loc.set.map std.loc.set, 
                             (loc -> loc -> prop) -> std.loc.set.

% [std.loc.set.fold M Acc F Acc1] fold M w.r.t. the predicate F
external func std.loc.set.fold std.loc.set, A, 
                              (loc -> A -> A -> prop) -> A.

% [std.loc.set.partition M F M1 M2] Partitions M w.r.t. the predicate F, M1
% is where F holds
external func std.loc.set.partition std.loc.set, 
                                   (loc -> (func)) -> std.loc.set, 
                                   std.loc.set.

#line 1 "builtin_map.elpi"
kind std.map type -> type -> type.
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
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
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
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
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
func bindings std.map K V -> 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.

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 (node L K V R H) :- H is {std.max {height L} {height R}} + 1.

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 :- 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.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.
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
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
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}
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}
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
func cardinal std.set E -> int.
cardinal (std.set M _) N :- private.cardinal M N.

func elements std.set E -> 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.

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 (node L E R H) :- H is {std.max {height L} {height R}} + 1.

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 (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.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 =====================================

% [trace.counter Name Value] reads the Value of a trace point Name
external func trace.counter string -> int.

external func gc.get % Reads the current settings of the garbage collector. See also OCaml's Gc.control type documentation.
  -> int,  % MinorHeapSize
  int,     % MajorHeapIncrement
  int,     % SpaceOverhead
  int,     % Verbose
  int,     % MaxOverhead
  int,     % StackLimit
  int,     % AllocationPolicy
  int.     % WindowSize
  
% [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 func gc.set int, int, int, int, int, int, int, int.

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

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

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

% [gc.compact] See OCaml's Gc.compact documentation.
external func 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 func gc.stat -> float, float, float, int, int, int, int, int, 
                     int, int, int, int, int, int, int, int.

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