1:- module(mavis, [ the/2
    2                 , has_intersection/2
    3                 , has_subtype/2
    4                 , known_type/1
    5                 , build_type_assertions/3
    6                 , build_determinism_assertions/2
    7                 , run_goal_at_mode/4
    8                 ]).    9
   10
   11:- use_module(library(quickcheck)).   12:- use_module(library(error)).

Optional type declarations

Declare optional types which are checked during development time. See pack documentation for more information. */

   20module_wants_mavis(Module) :-
   21    Module \= mavis,
   22    predicate_property(Module:the(_,_), imported_from(mavis)).
 the(+Type:type, ?Value) is det
Declare that Value has the given Type. Succeeds if Value is bound to a value that's compatible with Type. Throws an informative exception if Value is bound to a value that's not compatible with Type. If Value is not bound, the type check is delayed until Value becomes ground.

When optimizations are enabled (current_prolog_flag(optimise, true)) a macro removes the entirely so that it always succeeds.

   36:- if(current_prolog_flag(optimise,true)).   37
   38the(_,_).  % avoid "Exported procedure mavis:the/2 is not defined"
   39user:goal_expansion(the(_,_), true).
   40
   41build_determinism_assertions(_,_) :- fail.  
   42build_type_assertions(_,_,_) :- fail.  
   43run_goal_at_mode(_,_,_,_) :- fail.
   44
   45:- else.   46
   47:- use_module(library(apply), [exclude/3]).   48:- use_module(library(charsio), [read_term_from_chars/3]).   49:- use_module(library(list_util), [xfy_list/3,split_at/4]).   50:- use_module(library(pldoc)).   51:- use_module(library(pldoc/doc_wiki), [indented_lines/3]).   52:- use_module(library(when), [when/2]).   53:- doc_collect(true).   54
   55% extract mode declaration from a structured comment
   56mode_declaration(Comment, ModeCodes) :-
   57    string_to_list(Comment, Codes),
   58    phrase(pldoc_process:structured_comment(Prefixes,_), Codes, _),
   59    indented_lines(Codes, Prefixes, Lines),
   60    pldoc_modes:mode_lines(Lines, ModeCodes, [], _).
   61
   62% There may be more varieties of this that we have to handle
   63% see read_term/2
   64end_pos(Pos,End) :- 
   65    (   Pos=term_position(_, End, _, _, _)
   66    ->  true
   67    ;   Pos=_-End).
   68
   69exhaustive_read_term(Codes,[Term|Terms]) :-
   70    Options = [module(pldoc_modes),
   71               variable_names(Vars),
   72               subterm_positions(Pos)],
   73    read_term_from_chars(Codes,Term,Options),
   74    end_pos(Pos,End),
   75    Term \= end_of_file,
   76    !,
   77    maplist(call,Vars),
   78    Next is End + 2, % one for 0 offset, one for '.'
   79    split_at(Next,Codes,_,NewCodes),
   80    exhaustive_read_term(NewCodes,Terms).
   81exhaustive_read_term(_Codes,[]).
   82
   83% read all mode declarations from character codes
   84read_mode_declarations(ModeCodes, Modes) :-
   85    exhaustive_read_term(ModeCodes, Modes).
   86
   87% convert mode declarations to a standard form
   88normalize_mode(Mode0, Args, Det) :-
   89    (Mode0 = is(Mode1, Det) -> true; Mode1=Mode0, Det=nondet),
   90    (Mode1 = //(Mode2) -> Slash='//'; Mode2=Mode1, Slash='/' ),
   91    _ = Slash, % avoid singleton warnings (until Slash is needed)
   92    Mode2 =.. [_|RawArgs],
   93    maplist(normalize_args, RawArgs, Args).
   94
   95normalize_args(X0, arg(Mode,Name,Type)) :-
   96    ( var(X0) -> X1 = ?(X0:any) ; X1=X0 ),
   97    ( X1 =.. [Mode0,Arg] -> true; Mode0='?', Arg=X1 ),
   98    ( member(Mode0, [++,+,-,--,?,:,@,!]) -> Mode=Mode0; Mode='?' ),
   99    ( nonvar(Arg), Arg=Name:Type -> true; Name=Arg, Type=any).
  100
  101the(Type, Value) :-
  102    when(ground(Value), error:must_be(Type, Value)).
  103
  104% create a the/2 type assertion based on a variable and
  105% the declared mode information for that variable.
  106type_declaration(Var, arg(_,_,Type), the(Type, Var)).
  107
  108% convert a clause head into a goal which asserts all types
  109% associated with that head.  Slash is '/' for a normal
  110% predicate and '//' for a DCG.  Pneumonic: foo/1 vs foo//1
  111build_type_assertions(Slash, Head, TypeGoal) :-
  112    % does this module want mavis type assertions?
  113    prolog_load_context(module, Module),
  114    mavis:module_wants_mavis(Module),
  115
  116    % fetch this predicate's structured comment
  117    functor(Head, Name, Arity),
  118    Indicator =.. [Slash, Name, Arity],
  119    pldoc_process:doc_comment(Module:Indicator,_,_,Comment),
  120
  121    % parse and normalize mode description
  122    mode_declaration(Comment, ModeText),
  123    %debug(mavis, "~q has modeline `~s`~n", [Module:Indicator, ModeText]),
  124    % Warning: Potential bug!!!
  125    % We assume type consistency between modes...
  126    %debug(mavis, "~q has modeline `~s`~n", [Module:Indicator, ModeText]),
  127    read_mode_declarations(ModeText, [RawMode|_]),
  128    debug(mavis, "~q has types from `~q`~n", [Module:Indicator, RawMode]),
  129    normalize_mode(RawMode, ModeArgs, _Determinism),
  130
  131    Head =.. [Name|HeadArgs],
  132    maplist(type_declaration, HeadArgs, ModeArgs, AllTypes),
  133    exclude(=@=(the(any, _)), AllTypes, Types),
  134    xfy_list(',', TypeGoal, Types).
  135
  136build_determinism_assertions(Goal,Wrapped) :-
  137    % does this module want mavis type assertions?
  138    prolog_load_context(module, Module),
  139    mavis:module_wants_mavis(Module),
  140    
  141    % fetch this predicate's structured comment
  142    functor(Goal, Name, Arity),
  143    Indicator =.. ['/', Name, Arity],
  144
  145    pldoc_process:doc_comment(Module:Indicator,_,_,Comment),
  146    
  147    % parse and normalize mode description
  148    mode_declaration(Comment, ModeText),
  149    read_mode_declarations(ModeText, RawModes),
  150    % fail if there are no mode declarations (to leave the goal unchanged)
  151    \+ RawModes = [],
  152    maplist([RawMode,mode(ModeArgs,Determinism)]>>normalize_mode(RawMode, ModeArgs, Determinism),
  153            RawModes,Modes),
  154    %%debug(mavis, "~q has modeline `~s`~n", [Module:Indicator, Modes]),        
  155    % We should really check for mode consistency here.
  156    
  157    Goal =.. [Name|Args],
  158    Wrapped = mavis:run_goal_at_mode(Module,Name,Modes,Args).
  159
  160% pre_check_groundedness(arg(Groundedness,_,Type),Arg,Demote) is det.
  161% Promote holds a 0 or 1 depending on whether we should demote
  162% in the event of increased nondeterminism.
  163pre_check_groundedness(arg('++',_,Type),Arg,0) :-
  164    ground(Arg),
  165    (   \+ error:has_type(Type,Arg)
  166    ->  throw(domain_error(Type,Arg))
  167    ;   true).
  168pre_check_groundedness(arg('+',_,Type),Arg,0) :-
  169    % This will be type checked too late due to suspension
  170    % unless we do it now.
  171    % (negation avoids bindings)
  172    \+ var(Arg),
  173    (   \+ error:has_type(Type,Arg)
  174    ->  throw(domain_error(Type,Arg))
  175    ;   true).
  176pre_check_groundedness(arg('-',_,_),Arg,Demote) :-
  177    (   var(Arg)
  178    ->  Demote = 0
  179    ;   Demote = 1).
  180pre_check_groundedness(arg('--',_,_),Arg,0) :-
  181    var(Arg).
  182pre_check_groundedness(arg('?',_,_),Arg,Demote) :-
  183    (   var(Arg)
  184    ->  Demote = 0
  185    ;   Demote = 1).
  186pre_check_groundedness(arg(':',_,_),_Arg,0).
  187pre_check_groundedness(arg('!',_,_),_Arg,0).
  188pre_check_groundedness(arg('@',_,_),_Arg,0).
  189
  190post_check_groundedness(arg('-',_,Type),Arg) :-
  191    !,
  192    (   \+ error:has_type(Type,Arg)
  193    ->  throw(domain_error(Type,Arg))
  194    ;   true).
  195post_check_groundedness(arg('--',_,Type),Arg) :-
  196    !,
  197    (   \+ error:has_type(Type,Arg)
  198    ->  throw(domain_error(Type,Arg))
  199    ;   true).
  200post_check_groundedness(arg(_,_,_),_Arg).
  201
  202demote(det,1,semidet).
  203demote(multi,1,nondet).
  204demote(fail,1,fail).
  205demote(semidet,1,semidet).
  206demote(nondet,1,nondet).
  207demote(erroneous,1,erroneous).
  208demote(X,0,X).
  209
  210choose_mode([mode(Mode,Determinism)|_Modes],Args,_Module,_Name,
  211            mode(Mode,DeterminismPrime)) :-
  212    maplist(pre_check_groundedness,Mode,Args,DemotionVotes),
  213    foldl([X,Y,R]>>(R is X \/ Y),DemotionVotes,0,Demote),
  214    demote(Determinism,Demote,DeterminismPrime),
  215    !.
  216choose_mode([_|Modes],Args,Module,Name,Mode) :-
  217    choose_mode(Modes,Args,Module,Name,Mode).
  218        
  219run_goal_at_mode(Module,Name,Modes,Args) :-
  220    Goal =.. [Name|Args],
  221    (   choose_mode(Modes,Args,Module,Name,mode(Mode,Determinism))
  222    ->  true
  223    ;   throw(mode_error(Modes,apply(Module:Name,Args)))),
  224    run_goal_with_determinism(Determinism,Module,Goal),
  225    (   maplist(post_check_groundedness,Mode,Args)
  226    ->  true
  227    ;   throw(mode_error(Modes,apply(Module:Name,Args)))).
  228
  229run_goal_with_determinism(erroneous,Module,Goal) :-
  230    !,
  231    throw(determinism_error(Module:Goal,erroneous)).
  232run_goal_with_determinism(failure,Module,Goal) :-
  233    !,
  234    call(Module:Goal),
  235    throw(determinism_error(Module:Goal,failure)).
  236run_goal_with_determinism(det,Module,Goal) :-
  237    !,
  238    (   call_cleanup(Module:Goal, Det=true),
  239        (   Det == true
  240        ->  true
  241        ;   throw(determinism_error(Module:Goal, det))
  242        )
  243    ->  true
  244    ;   throw(determinism_error(Module:Goal, det))
  245    ).
  246run_goal_with_determinism(semidet,Module,Goal) :-
  247    !,
  248    (   call_cleanup(Module:Goal, Det=true),
  249        (   Det == true
  250        ->  true
  251        ;   throw(determinism_error(Module:Goal, semidet))
  252        )
  253    ->  true
  254    ;   fail
  255    ).
  256run_goal_with_determinism(multi,Module,Goal) :-
  257    !,
  258    (   call(Module:Goal)
  259    *-> true
  260    ;   throw(determinism_error(Module:Goal,multi))
  261    ).
  262run_goal_with_determinism(_,Module,Goal) :-
  263    call(Module:Goal).
  264
  265bodyless_predicate(Term) :-
  266    \+ Term = (:-_),
  267    \+ Term = (_:-_),
  268    \+ Term = (_-->_),
  269    \+ Term = end_of_file.
  270
  271user:term_expansion((Head:-Body), (Head:-TypeGoal,Body)) :-
  272    Slash = '/',
  273    build_type_assertions(Slash, Head, TypeGoal).
  274
  275user:term_expansion(Head,(Head:-TypeGoal)) :-
  276    bodyless_predicate(Head),
  277    Slash = '/', 
  278    build_type_assertions(Slash, Head, TypeGoal).
  279
  280user:term_expansion((Head-->Body), (Head-->{TypeGoal},Body)) :-
  281    Slash = '//',
  282    build_type_assertions(Slash, Head, TypeGoal).
  283
  284% TODO:
  285% We need to check mode assignments and discover if they are
  286% A) disjoint
  287%    a) if they are disjoint we need to check groundedness
  288%       1) Add dynamic check groudedness.
  289%       2) Do a separate determinism check per groudedness.
  290%    b) Throw runtime error if not disjoint.
  291%
  292% TODO:
  293% Later it would be nice if we had skeletons (ala mercury).
  294user:goal_expansion(Goal,Wrapped) :-
  295    build_determinism_assertions(Goal,Wrapped),
  296    debug(mavis,'~q => ~q~n', [Goal,Wrapped]).
  297
  298:- multifile prolog:message//1.  299prolog:message(determinism_error(Goal, Det)) -->
  300    [ 'The Goal ~q is not of determinism ~q'-[Goal,Det]].
  301prolog:message(domain_error(Domain, Term)) -->
  302    [ 'The term ~q is not in the domain ~q'-[Term,Domain]].
  303prolog:message(mode_error(Mode, Term)) -->
  304    [ 'The term ~q does not have a valid mode in ~q'-[Term,Mode]].
  305
  306:- endif.  307
  308
  309% below here, code that loads all the time
 type_subtype(?Type, ?Subtype)
Multifile predicate for declaring that a Type has a Subtype. It should only be necessary to add clauses to this predicate if has_subtype/2 has trouble deriving this information based on your definition of arbitrary/2.
  317:- dynamic type_subtype/2.  318:- multifile type_subtype/2.
 has_subtype(+Type, +Subtype) is semidet
True if all values of Subtype are also values of Type. This can be used to determine whether arguments of one type can be passed to a predicate which demands arguments of another type.

This predicate performs probabilistic subtype detection by leveraging your definitions for error:has_type/2 and arbitrary/2. If this predicate is not detecting your types correctly, either improve your arbitrary/2 definition or add clauses to the multifile predicate type_subtype/2.

  331has_subtype(Type, Subtype) :-
  332    ( var(Type); var(Subtype) ),
  333    !,
  334    fail.
  335has_subtype(Type, Subtype) :-
  336    type_subtype(Type, Subtype),
  337    !.
  338has_subtype(Type, Subtype) :-
  339    error:must_be(nonvar, Type),
  340    error:must_be(arbitrary_type, Subtype),
  341    \+ counter_example(Type, Subtype, _),
  342    assert(type_subtype(Type, Subtype)).
  343
  344% find a value (Example) which belongs to Subtype but not
  345% to Type.  This demonstrates that Subtype is not a strict
  346% subset of Type.
  347counter_example(Type, Subtype, Example) :-
  348    between(1,100,_),
  349    quickcheck:arbitrary(Subtype, Example),
  350    \+ error:is_of_type(Type, Example),
  351    !.
 type_intersection(?Type, ?IntersectionType)
Multifile predicate for declaring that Type has an IntersectionType. See type_subtype/2 for further details.
  358:- dynamic type_intersection/2.  359:- multifile type_intersection/2.
 has_intersection(Type, IntersectionType) is semidet
True if some value of IntersectionType is also of Type. See has_subtype/2 for further details.
  366has_intersection(Type, Intersection) :-
  367    ( var(Type); var(Intersection) ),
  368    !,
  369    fail.
  370has_intersection(Type, Intersection) :-
  371    type_intersection(Type, Intersection),
  372    !.
  373has_intersection(Type, Subtype) :-
  374    error:must_be(nonvar, Type),
  375    error:must_be(arbitrary_type, Subtype),
  376    shared_value(Type, Subtype, _),
  377    assert(type_intersection(Type, Subtype)).
  378
  379% Find a value shared by both Type and Subtype
  380shared_value(Type, Subtype, Value) :-
  381    between(1,100,_),
  382    quickcheck:arbitrary(Subtype, Value),
  383    error:is_of_type(Type, Value),
  384    !.
 known_type(?Type:type) is semidet
True if Type is a type known to error:has_type/2. Iterates all known types on backtracking. Be aware that some types are polymorphic (like list(T)) so Type may be a non-ground term.

As a convenience, the type named type describes the set of all values for which known_type/1 is true.

  395known_type(Type) :-
  396    dif(Type, impossible),  % library(error) implementation detail
  397    clause(error:has_type(Type, _), _Body, _Ref).
  398
  399
  400:- multifile error:has_type/2.  401error:has_type(type, T) :-
  402    known_type(T)