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


13 builtin

%--------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et wm=0 tw=0
%--------------------------------------------------%
% Copyright (C) 1994-2007, 2010-2012 The University of Melbourne.
% This file may only be copied under the terms of the GNU Library General
% Public License - see the file COPYING.LIB in the Mercury distribution.
%--------------------------------------------------%
% 
% 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', `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.  (XXX TODO: report an error for attempts to redefine
% these types.)

    % 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 functions insts `func(<modes>) = <mode> is det'
% are also builtin.

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

    % The `any' inst used for the constraint solver interface is also
    % builtin.  The insts `new' and `old' are allowed as synonyms for
    % `free' and `any', respectively, since some of the literature uses
    % this terminology.
    %
:- inst old == any.
:- inst new == free.

%--------------------------------------------------%
%
% Standard modes
%

:- mode unused == free >> free.
:- mode output == free >> ground.
:- 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.

    % The modes `no' and `oo' are allowed as synonyms, since some of the
    % literature uses this terminology.
    %
:- mode no == new >> old.
:- mode oo == old >> old.

%--------------------------------------------------%
%
% 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: we recommend using the a `promise_equivalent_solutions' goal
    %       instead of this function.
    %
:- 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: we recommend using a `promise_equivalent_solutions' goal
    %       instead of this predicate.
    %
:- 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).
    % Note to implementors: the modes must appear in this order:
    % compiler/higher_order.m depends on it, as does
    % compiler/simplify.m (for the inequality simplification.)
:- 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: , Up: Top   [Contents]