Next: , Previous: bt_array, Up: Top   [Contents]


13 builtin

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

%--------------------------------------------------%
%--------------------------------------------------%


Next: , Previous: bt_array, Up: Top   [Contents]