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)).
20module_wants_mavis(Module) :-
21 Module \= mavis,
22 predicate_property(Module:the(_,_), imported_from(mavis)).
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" 39usergoal_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 271userterm_expansion((Head:-Body), (Head:-TypeGoal,Body)) :- 272 Slash = '/', 273 build_type_assertions(Slash, Head, TypeGoal). 274 275userterm_expansion(Head,(Head:-TypeGoal)) :- 276 bodyless_predicate(Head), 277 Slash = '/', 278 build_type_assertions(Slash, Head, TypeGoal). 279 280userterm_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). 294usergoal_expansion(Goal,Wrapped) :- 295 build_determinism_assertions(Goal,Wrapped), 296 debug(mavis,'~q => ~q~n', [Goal,Wrapped]). 297 298:- multifile prolog:message//1. 299prologmessage(determinism_error(Goal, Det)) --> 300 [ 'The Goal ~q is not of determinism ~q'-[Goal,Det]]. 301prologmessage(domain_error(Domain, Term)) --> 302 [ 'The term ~q is not in the domain ~q'-[Term,Domain]]. 303prologmessage(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
317:- dynamic type_subtype/2. 318:- multifile type_subtype/2.
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 !.
358:- dynamic type_intersection/2. 359:- multifile type_intersection/2.
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 Type, Subtype, Value) (:- 381 between(1,100,_), 382 quickcheck:arbitrary(Subtype, Value), 383 error:is_of_type(Type, Value), 384 !.
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. 401errorhas_type(type, T) :- 402 known_type(T)
Optional type declarations
Declare optional types which are checked during development time. See pack documentation for more information. */