%--------------------------------------------------%
% vim: ft=mercury ts=4 sw=4 et
%--------------------------------------------------%
% Copyright (C) 2002-2007, 2009-2012 The University of Melbourne.
% Copyright (C) 2013-2018 The Mercury team.
% This file is distributed under the terms specified in COPYING.LIB.
%--------------------------------------------------%
%
% File: type_desc.m.
% Main author: fjh, zs.
% Stability: low.
%
%--------------------------------------------------%
%--------------------------------------------------%

:- module type_desc.
:- interface.

:- import_module list.

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

    % The `type_desc', `pseudo_type_desc' and `type_ctor_desc' types
    % provide access to type information.
    % A type_desc represents a type, e.g. `list(int)'.
    % A pseudo_type_desc represents a type that possibly contains type
    % variables, e.g. `list(T)'.
    % A type_ctor_desc represents a type constructor, e.g. `list/1'.
    %
:- type type_desc.
:- type pseudo_type_desc.
:- type type_ctor_desc.

    % The possibly nonground type represented by a pseudo_type_desc
    % is either a type constructor applied to zero or more
    % pseudo_type_descs, or a type variable. If the latter, the
    % type variable may be either universally or existentially quantified.
    % In either case, the type is identified by an integer, which has no
    % meaning beyond the fact that two type variables will be represented
    % by identical integers if and only if they are the same type variable.
    % Existentially quantified type variables may have type class
    % constraints placed on them, but for now we can't return these.
    %
:- type pseudo_type_rep
    --->    bound(type_ctor_desc, list(pseudo_type_desc))
    ;       univ_tvar(int)
    ;       exist_tvar(int).

:- pred pseudo_type_desc_is_ground(pseudo_type_desc::in) is semidet.

    % This function allows the caller to look into the structure
    % of the given pseudo_type_desc.
    %
:- func pseudo_type_desc_to_rep(pseudo_type_desc) = pseudo_type_rep.

    % Convert a type_desc, which by definition describes a ground type,
    % to a pseudo_type_desc.
    %
:- func type_desc_to_pseudo_type_desc(type_desc) = pseudo_type_desc.

    % Convert a pseudo_type_desc describing a ground type to a type_desc.
    % If the pseudo_type_desc describes a non-ground type, fail.
    %
:- func ground_pseudo_type_desc_to_type_desc(pseudo_type_desc) = type_desc
    is semidet.
:- pred ground_pseudo_type_desc_to_type_desc(pseudo_type_desc::in,
    type_desc::out) is semidet.

    % Convert a pseudo_type_desc describing a ground type to a type_desc.
    % Throw an exception if the pseudo_type_desc describes a non-ground type.
    %
:- func det_ground_pseudo_type_desc_to_type_desc(pseudo_type_desc) = type_desc.

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

    % The function type_of/1 returns a representation of the type
    % of its argument.
    %
    % (Note: it is not possible for the type of a variable to be an unbound
    % type variable; if there are no constraints on a type variable, then the
    % typechecker will use the type `void'. `void' is a special (builtin) type
    % that has no constructors. There is no way of creating an object of
    % type `void'. `void' is not considered to be a discriminated union, so
    % get_functor/5 and construct/3 will fail if used upon a value of
    % this type.)
    %
:- func type_of(T::unused) = (type_desc::out) is det.

    % The predicate has_type/2 is basically an existentially typed inverse
    % to the function type_of/1. It constrains the type of the first argument
    % to be the type represented by the second argument.
    %
:- some [T] pred has_type(T::unused, type_desc::in) is det.

    % The predicate same_type/2 ensures type identity of the two arguments.
    %
:- pred same_type(T::unused, T::unused) is det.

    % type_name(Type) returns the name of the specified type
    % (e.g. type_name(type_of([2,3])) = "list.list(int)").
    % Any equivalence types will be fully expanded.
    % Builtin types (those defined in builtin.m) will not have
    % a module qualifier.
    %
:- func type_name(type_desc) = string.

    % type_ctor_and_args(Type, TypeCtor, TypeArgs):
    %
    % True iff `TypeCtor' is a representation of the top-level type constructor
    % for `Type', and `TypeArgs' is a list of the corresponding type arguments
    % to `TypeCtor', and `TypeCtor' is not an equivalence type.
    %
    % For example, type_ctor_and_args(type_of([2,3]), TypeCtor, TypeArgs)
    % will bind `TypeCtor' to a representation of the type constructor list/1,
    % and will bind `TypeArgs' to the list `[Int]', where `Int' is a
    % representation of the type `int'.
    %
    % Note that the requirement that `TypeCtor' not be an equivalence type
    % is fulfilled by fully expanding any equivalence types. For example,
    % if you have a declaration `:- type foo == bar.', then
    % type_ctor_and_args/3 will always return a representation of type
    % constructor `bar/0', not `foo/0'. (If you don't want them expanded,
    % you can use the reverse mode of make_type/2 instead.)
    %
:- pred type_ctor_and_args(type_desc::in,
    type_ctor_desc::out, list(type_desc)::out) is det.

    % pseudo_type_ctor_and_args(Type, TypeCtor, TypeArgs):
    %
    % True iff `TypeCtor' is a representation of the top-level type constructor
    % for `Type', and `TypeArgs' is a list of the corresponding type arguments
    % to `TypeCtor', and `TypeCtor' is not an equivalence type.
    %
    % Similar to type_ctor_and_args, but works on pseudo_type_infos.
    % Fails if the input pseudo_type_info is a variable.
    %
:- pred pseudo_type_ctor_and_args(pseudo_type_desc::in,
    type_ctor_desc::out, list(pseudo_type_desc)::out) is semidet.

    % type_ctor(Type) = TypeCtor :-
    %   type_ctor_and_args(Type, TypeCtor, _).
    %
:- func type_ctor(type_desc) = type_ctor_desc.

    % pseudo_type_ctor(Type) = TypeCtor :-
    %   pseudo_type_ctor_and_args(Type, TypeCtor, _).
    %
:- func pseudo_type_ctor(pseudo_type_desc) = type_ctor_desc is semidet.

    % type_args(Type) = TypeArgs :-
    %   type_ctor_and_args(Type, _, TypeArgs).
    %
:- func type_args(type_desc) = list(type_desc).

    % pseudo_type_args(Type) = TypeArgs :-
    %   pseudo_type_ctor_and_args(Type, _, TypeArgs).
    %
:- func pseudo_type_args(pseudo_type_desc) = list(pseudo_type_desc) is semidet.

    % type_ctor_name(TypeCtor) returns the name of specified type constructor.
    % (e.g. type_ctor_name(type_ctor(type_of([2,3]))) = "list").
    %
:- func type_ctor_name(type_ctor_desc) = string.

    % type_ctor_module_name(TypeCtor) returns the module name of specified
    % type constructor.
    % (e.g. type_ctor_module_name(type_ctor(type_of(2))) = "builtin").
    %
:- func type_ctor_module_name(type_ctor_desc) = string.

    % type_ctor_arity(TypeCtor) returns the arity of specified
    % type constructor.
    % (e.g. type_ctor_arity(type_ctor(type_of([2,3]))) = 1).
    %
:- func type_ctor_arity(type_ctor_desc) = int.

    % type_ctor_name_and_arity(TypeCtor, ModuleName, TypeName, Arity) :-
    %   Name = type_ctor_name(TypeCtor),
    %   ModuleName = type_ctor_module_name(TypeCtor),
    %   Arity = type_ctor_arity(TypeCtor).
    %
:- pred type_ctor_name_and_arity(type_ctor_desc::in,
    string::out, string::out, int::out) is det.

    % make_type(TypeCtor, TypeArgs) = Type:
    %
    % True iff `Type' is a type constructed by applying the type constructor
    % `TypeCtor' to the type arguments `TypeArgs'.
    %
    % Operationally, the forwards mode returns the type formed by applying
    % the specified type constructor to the specified argument types, or fails
    % if the length of TypeArgs is not the same as the arity of TypeCtor.
    % The reverse mode returns a type constructor and its argument types,
    % given a type_desc; the type constructor returned may be an equivalence
    % type (and hence this reverse mode of make_type/2 may be more useful
    % for some purposes than the type_ctor/1 function).
    %
:- func make_type(type_ctor_desc, list(type_desc)) = type_desc.
:- mode make_type(in, in) = out is semidet.
:- mode make_type(out, out) = in is cc_multi.

    % det_make_type(TypeCtor, TypeArgs):
    %
    % Returns the type formed by applying the specified type constructor
    % to the specified argument types. Throws an exception if the length of
    % `TypeArgs' is not the same as the arity of `TypeCtor'.
    %
:- func det_make_type(type_ctor_desc, list(type_desc)) = type_desc.

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