%--------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%--------------------------------------------------%
% Copyright (C) 1994-2007, 2010-2012 The University of Melbourne.
% Copyright (C) 2014-2018 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%--------------------------------------------------%
%
% File: builtin.m.
% Main author: fjh.
% Stability: low.
%
% This file is automatically imported into every module.
% It is intended for things that are part of the language,
% but which are implemented just as normal user-level code
% rather than with special coding in the compiler.
%
%--------------------------------------------------%
%--------------------------------------------------%
:- module builtin.
:- interface.
%--------------------------------------------------%
%
% Types.
%
% The types `character', `int', `int8', `int16', `int32', `int64',
% `uint', `uint8', `uint16', `uint32', `uint64', `float', and `string',
% and tuple types `{}', `{T}', `{T1, T2}', ...
% and the types `pred', `pred(T)', `pred(T1, T2)', `pred(T1, T2, T3)', ...
% and `func(T1) = T2', `func(T1, T2) = T3', `func(T1, T2, T3) = T4', ...
% are builtin and are implemented using special code in the type-checker.
% The type c_pointer can be used by predicates that use the C interface.
%
% NOTE: We *strongly* recommend using a `foreign_type' pragma instead
% of using this type.
%
:- type c_pointer.
%--------------------------------------------------%
%
% Insts.
%
% The standard insts `free', `ground', and `bound(...)' are builtin and are
% implemented using special code in the parser and mode-checker.
%
% So are the standard unique insts `unique', `unique(...)', `mostly_unique',
% `mostly_unique(...)', and `clobbered'.
%
% Higher-order predicate insts `pred(<modes>) is <detism>'
% and higher-order function insts `func(<modes>) = <mode> is <detism>'
% are also builtin.
%
% The `any' inst used for constraint solver interfaces is builtin and so are
% its higher-order variants: `any_pred(<modes>) is <detism>' and
% `any_func(<modes>) = <mode> is <detism>'.
% The name `dead' is allowed as a synonym for `clobbered'.
% Similarly, `mostly_dead' is a synonym for `mostly_clobbered'.
%
:- inst dead == clobbered.
:- inst mostly_dead == mostly_clobbered.
%--------------------------------------------------%
%
% Standard modes.
%
:- mode unused == free >> free.
% This mode is deprecated, use `out' instead.
%
:- mode output == free >> ground.
% This mode is deprecated, use `in' instead.
%
:- mode input == ground >> ground.
:- mode in == ground >> ground.
:- mode out == free >> ground.
:- mode in(Inst) == Inst >> Inst.
:- mode out(Inst) == free >> Inst.
:- mode di(Inst) == Inst >> clobbered.
:- mode mdi(Inst) == Inst >> mostly_clobbered.
%--------------------------------------------------%
%
% Unique modes.
%
% XXX These are still not fully implemented.
% unique output
%
:- mode uo == free >> unique.
% unique input
%
:- mode ui == unique >> unique.
% destructive input
%
:- mode di == unique >> clobbered.
%--------------------------------------------------%
%
% "Mostly" unique modes.
%
% Unique except that they may be referenced again on backtracking.
% mostly unique output
%
:- mode muo == free >> mostly_unique.
% mostly unique input
%
:- mode mui == mostly_unique >> mostly_unique.
% mostly destructive input
%
:- mode mdi == mostly_unique >> mostly_clobbered.
%--------------------------------------------------%
%
% Dynamic modes.
%
% Solver type modes.
%
:- mode ia == any >> any.
:- mode oa == free >> any.
%--------------------------------------------------%
%
% Predicates.
%
% copy/2 makes a deep copy of a data structure.
% The resulting copy is a `unique' value, so you can use
% destructive update on it.
%
:- pred copy(T, T).
:- mode copy(ui, uo) is det.
:- mode copy(in, uo) is det.
% unsafe_promise_unique/2 is used to promise the compiler that you
% have a `unique' copy of a data structure, so that you can use
% destructive update. It is used to work around limitations in
% the current support for unique modes.
% `unsafe_promise_unique(X, Y)' is the same as `Y = X' except that
% the compiler will assume that `Y' is unique.
%
% Note that misuse of this predicate may lead to unsound results:
% if there is more than one reference to the data in question,
% i.e. it is not `unique', then the behaviour is undefined.
% (If you lie to the compiler, the compiler will get its revenge!)
%
:- func unsafe_promise_unique(T::in) = (T::uo) is det.
:- pred unsafe_promise_unique(T::in, T::uo) is det.
% A synonym for fail/0; this name is more in keeping with Mercury's
% declarative style rather than its Prolog heritage.
%
:- pred false is failure.
%--------------------------------------------------%
% This function is useful for converting polymorphic non-solver type
% values with inst any to inst ground (the compiler recognises that
% inst any is equivalent to ground for non-polymorphic non-solver
% type values.)
%
% Do not call this on solver type values unless you are *absolutely sure*
% that they are semantically ground.
%
:- func unsafe_cast_any_to_ground(T::ia) = (T::out) is det.
%--------------------------------------------------%
% A call to the function `promise_only_solution(Pred)' constitutes a
% promise on the part of the caller that `Pred' has at most one
% solution, i.e. that `not some [X1, X2] (Pred(X1), Pred(X2), X1 \=
% X2)'. `promise_only_solution(Pred)' presumes that this assumption is
% satisfied, and returns the X for which Pred(X) is true, if there is
% one.
%
% You can use `promise_only_solution' as a way of introducing
% `cc_multi' or `cc_nondet' code inside a `det' or `semidet' procedure.
%
% Note that misuse of this function may lead to unsound results: if the
% assumption is not satisfied, the behaviour is undefined. (If you lie
% to the compiler, the compiler will get its revenge!)
%
% NOTE: This function is deprecated and will be removed in a future
% release. Use a `promise_equivalent_solutions' goal instead.
%
:- pragma obsolete(func(promise_only_solution/1)).
:- func promise_only_solution(pred(T)) = T.
:- mode promise_only_solution(pred(out) is cc_multi) = out is det.
:- mode promise_only_solution(pred(uo) is cc_multi) = uo is det.
:- mode promise_only_solution(pred(out) is cc_nondet) = out is semidet.
:- mode promise_only_solution(pred(uo) is cc_nondet) = uo is semidet.
% `promise_only_solution_io' is like `promise_only_solution', but for
% procedures with unique modes (e.g. those that do IO).
%
% A call to `promise_only_solution_io(P, X, IO0, IO)' constitutes a
% promise on the part of the caller that for the given IO0, there is
% only one value of `X' and `IO' for which `P(X, IO0, IO)' is true.
% `promise_only_solution_io(P, X, IO0, IO)' presumes that this
% assumption is satisfied, and returns the X and IO for which `P(X,
% IO0, IO)' is true.
%
% Note that misuse of this predicate may lead to unsound results: if
% the assumption is not satisfied, the behaviour is undefined. (If you
% lie to the compiler, the compiler will get its revenge!)
%
% NOTE: This predicate is deprecated and will be removed in a future
% release. Use a `promise_equivalent_solutions' goal instead.
%
:- pragma obsolete(pred(promise_only_solution_io/4)).
:- pred promise_only_solution_io(
pred(T, IO, IO)::in(pred(out, di, uo) is cc_multi), T::out,
IO::di, IO::uo) is det.
%--------------------------------------------------%
% unify(X, Y) is true iff X = Y.
%
:- pred unify(T::in, T::in) is semidet.
% For use in defining user-defined unification predicates.
% The relation defined by a value of type `unify', must be an
% equivalence relation; that is, it must be symmetric, reflexive,
% and transitive.
%
:- type unify(T) == pred(T, T).
:- inst unify == (pred(in, in) is semidet).
:- type comparison_result
---> (=)
; (<)
; (>).
% compare(Res, X, Y) binds Res to =, <, or > depending on whether
% X is =, <, or > Y in the standard ordering.
%
:- pred compare(comparison_result, T, T).
:- mode compare(uo, in, in) is det.
:- mode compare(uo, ui, ui) is det.
:- mode compare(uo, ui, in) is det.
:- mode compare(uo, in, ui) is det.
% For use in defining user-defined comparison predicates.
% For a value `ComparePred' of type `compare', the following
% conditions must hold:
%
% - the relation
% compare_eq(X, Y) :- ComparePred((=), X, Y).
% must be an equivalence relation; that is, it must be symmetric,
% reflexive, and transitive.
%
% - the relations
% compare_leq(X, Y) :-
% ComparePred(R, X, Y), (R = (=) ; R = (<)).
% compare_geq(X, Y) :-
% ComparePred(R, X, Y), (R = (=) ; R = (>)).
% must be total order relations: that is they must be antisymmetric,
% reflexive and transitive.
%
:- type compare(T) == pred(comparison_result, T, T).
:- inst compare == (pred(uo, in, in) is det).
% ordering(X, Y) = R <=> compare(R, X, Y)
%
:- func ordering(T, T) = comparison_result.
% The standard inequalities defined in terms of compare/3.
% XXX The ui modes are commented out because they don't yet work properly.
%
:- pred T @< T.
:- mode in @< in is semidet.
% :- mode ui @< in is semidet.
% :- mode in @< ui is semidet.
% :- mode ui @< ui is semidet.
:- pred T @=< T.
:- mode in @=< in is semidet.
% :- mode ui @=< in is semidet.
% :- mode in @=< ui is semidet.
% :- mode ui @=< ui is semidet.
:- pred T @> T.
:- mode in @> in is semidet.
% :- mode ui @> in is semidet.
% :- mode in @> ui is semidet.
% :- mode ui @> ui is semidet.
:- pred T @>= T.
:- mode in @>= in is semidet.
% :- mode ui @>= in is semidet.
% :- mode in @>= ui is semidet.
% :- mode ui @>= ui is semidet.
% Values of types comparison_pred/1 and comparison_func/1 are used
% by predicates and functions which depend on an ordering on a given
% type, where this ordering is not necessarily the standard ordering.
% In addition to the type, mode and determinism constraints, a
% comparison predicate C is expected to obey two other laws.
% For all X, Y and Z of the appropriate type, and for all
% comparison_results R:
% 1) C(X, Y, (>)) if and only if C(Y, X, (<))
% 2) C(X, Y, R) and C(Y, Z, R) implies C(X, Z, R).
% Comparison functions are expected to obey analogous laws.
%
% Note that binary relations <, > and = can be defined from a
% comparison predicate or function in an obvious way. The following
% facts about these relations are entailed by the above constraints:
% = is an equivalence relation (not necessarily the usual equality),
% and the equivalence classes of this relation are totally ordered
% with respect to < and >.
%
:- type comparison_pred(T) == pred(T, T, comparison_result).
:- inst comparison_pred(I) == (pred(in(I), in(I), out) is det).
:- inst comparison_pred == comparison_pred(ground).
:- type comparison_func(T) == (func(T, T) = comparison_result).
:- inst comparison_func(I) == (func(in(I), in(I)) = out is det).
:- inst comparison_func == comparison_func(ground).
% In addition, the following predicate-like constructs are builtin:
%
% :- pred (T = T).
% :- pred (T \= T).
% :- pred (pred , pred).
% :- pred (pred ; pred).
% :- pred (\+ pred).
% :- pred (not pred).
% :- pred (pred -> pred).
% :- pred (if pred then pred).
% :- pred (if pred then pred else pred).
% :- pred (pred => pred).
% :- pred (pred <= pred).
% :- pred (pred <=> pred).
%
% (pred -> pred ; pred).
% some Vars pred
% all Vars pred
% call/N
%--------------------------------------------------%
% `semidet_succeed' is exactly the same as `true', except that
% the compiler thinks that it is semi-deterministic. You can use
% calls to `semidet_succeed' to suppress warnings about determinism
% declarations that could be stricter.
%
:- pred semidet_succeed is semidet.
% `semidet_fail' is like `fail' except that its determinism is semidet
% rather than failure.
%
:- pred semidet_fail is semidet.
% A synonym for semidet_succeed/0.
%
:- pred semidet_true is semidet.
% A synonym for semidet_fail/0.
%
:- pred semidet_false is semidet.
% `cc_multi_equal(X, Y)' is the same as `X = Y' except that it
% is cc_multi rather than det.
%
:- pred cc_multi_equal(T, T).
:- mode cc_multi_equal(di, uo) is cc_multi.
:- mode cc_multi_equal(in, out) is cc_multi.
% `impure_true' is like `true' except that it is impure.
%
:- impure pred impure_true is det.
% `semipure_true' is like `true' except that it is semipure.
%
:- semipure pred semipure_true is det.
%--------------------------------------------------%
% dynamic_cast(X, Y) succeeds with Y = X iff X has the same ground type
% as Y (so this may succeed if Y is of type list(int), say, but not if
% Y is of type list(T)).
%
:- pred dynamic_cast(T1::in, T2::out) is semidet.
%--------------------------------------------------%
%--------------------------------------------------%