ALE/TRALE -- Attribute Logic Engine

% [Documentation] %%%%%%%%%%%%%%%%%%%%% % TRALE 1.0 % Gerald Penn % University of Toronto % % Developed with SICStus Prolog 3.10.1, December, 2003 % % set environment variable TRALE_HOME to the directory that contains this % file % Added 'signature' default signature file specification. % 6/24/99 - G. Penn % Added logical variable macros and *> constraints % 7/10/99 - G. Penn % Bug corrected: parentheses missing on ale_macro and := calls. % 7/13/99 - G. Penn % Bug corrected: trale_abolish_preds had to be renamed to abolish_preds to % work with the debugger. % 7/14/99 - G. Penn % Bug corrected: retrieve_user_cons/3 expected only one complex_cons/5 clause % for any given type. % 8/27/99 - G. Penn % Now loads call for CHR library, since new ale.new.pl does not. % 9/15/99 - G. Penn % Adapted to reference-based FS data structure. No longer uses CHR. % 4/28/02 - G. Penn % Bug corrected: compile_sig_act/0 was calling link_cons/0 instead of link_cons_act/0 - % left choice-point in compilation chain. % 4/29/02 - G. Penn % Cleaned up and rewrote on-line FV map code to write dif/2 statements into compiled % trale_maps_init/2 to keep compiled logic code streams smaller. % 6/9/02 - G. Penn % Rewrote compute_maxcount/2 to compute and tabulate the actual maximal covers - cheaper % than decomposing joins. % 6/11/02 - G. Penn % Bug corrected: trale_maps_init/2 should not be inherited like other constraints - now % attach at ucons/7, add_to_typecons/6, and mgsat_cons/6. % 6/14/02 - G. Penn % Added ord_add_element/3 to the abolish list. % 6/18/02 - G. Penn % Bug corrected: resuspension on full-deref was not guarded by nonvar(FSVs) delay in trale_maps/4. % 8/14/02 - G. Penn % Bug corrected: recursive call in fully_deref_map/4 was guarded by nonvar(V) delay. % 8/14/02 - G. Penn % Bug corrected: logical macro argument mode declarations weren't optional. % 8/31/02 - G. Penn % Reorganised compilation chain slightly to do constraint linking entirely in constraint phase. % 9/5/02 - G. Penn % Bug corrected: new compilation chain was not integrated correctly with compile_gram/0,1 from ale.pl % 9/12/02 - G. Penn % Bug corrected: macro/2 was not instantiating LVLHS before looking up :=/2. % 9/16/02 - G. Penn % Bug corrected: add_lv_macro_descs/4 was binding variable LVArgs to Var-Desc pairs. % 9/19/02 - G. Penn % Bug corrected: missing macro/2 in abolish_preds/0. % 9/29/02 - G. Penn % Now trap shared or bound variables in logical variable macro heads. % 11/22/02 - G. Penn % Added fun/1 to abolish_preds/0. % 11/22/02 - G. Penn % Changed trale_signature hook to accommodate multiple signature files and new pth.pl. % 11/27/02 - G. Penn % Updated to SP 3.10.1. % 7/14/03 - G. Penn % Updated to matrix-based signature compiler. % 7/16/03 - G. Penn % Updated to new definition of imm_sub_type/2. % 8/11/03 - G. Penn % RCS banners % $Id: trale.pl,v 1.5 2003/12/19 00:12:19 mhaji Exp $ % $Log: trale.pl,v $ % Revision 1.5 2003/12/19 00:12:19 mhaji % added links % % Revision 1.4 2003/12/09 19:14:41 mhaji % added link for logical variable macros % % Revision 1.3 2003/12/01 00:24:05 gpenn % Corrected typos in header % % Revision 1.2 2003/11/30 20:02:28 mhaji % added chapter on compiling complex-antecedent constraints % % Revision 1.1 2003/11/24 21:32:41 mhaji % added trale.pl % % Revision 1.2 1999/02/06 17:01:07 gpenn % Version 0.2 - bug corrections and support for a_/1 atoms. % % Revision 1.1 1998/10/24 17:20:15 gpenn % Initial revision % :- ensure_loaded(ale). :- abolish([memberchk/2,member/2,reverse/2,append/3,ord_union/3,get_assoc/3, put_assoc/4,ord_intersect/2,ord_intersection/3,ord_add_element/3, is_list/1,ord_subtract/3]). :- compile(sics). :- multifile file_search_path/2. :- dynamic file_search_path/2. trale_search_path_add(Name,Path) :- (clause(file_search_path(Name,Path),true) -> true ; assertz(file_search_path(Name,Path))). :- environ('TRALE_HOME',Path), trale_search_path_add(trale_home,Path), trale_search_path_add(common,Path). :- compile(utilities). :- compile(pth). :- use_module(library(ugraphs),[vertices_edges_to_ugraph/3,neighbours/3, top_sort/2]). :- use_module(library(lists),[remove_duplicates/2]). :- use_module(library(terms),[variant/2,term_subsumer/3]). :- use_module(library(ordsets),[ord_union/2]). :- multifile if_b/2. :- multifile term_expansion/2. :- discontiguous term_expansion/2. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Compiler patches %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- abolish([abolish_preds/0]). abolish_preds :- % this is ALE's abolish_preds/0 with trale_cons/2 and ':=' abolish((empty)/1), abolish((rule)/2), abolish((lex_rule)/2), abolish(('--->')/2), abolish((sub)/2), abolish((if)/2), abolish((':=')/2), abolish((macro)/2), abolish((ext)/1), abolish((cons)/2), abolish(('*>')/2), abolish((intro)/2), % 5/1/96 - Octav -- added abolish/2 calls for generation predicates abolish((semantics)/1), abolish(('+++>')/2), abolish((fun)/1), abolish((trale_cons)/2), abolish((signature)/1). % % Signature patches % % no incremental signature compilation because of TRALE signature file :- abolish([compile_sub_type/1,compile_sub_type/0, compile_approp/1,compile_approp/0]). :- abolish(compile_sig_act/0). compile_sig_act :- alec_announce('Reading signature file...'), assert(alec(trale_signature)), compile('.alec_throw'), compile_sub_type_act(_,_,_,_), % compile_unify_type_act, % statistics(walltime,B), compile_approp_act, % statistics(walltime,E), % write(user_error,'begin: '),write(user_error,B), % nl(user_error), % write(user_error,'end: '),write(user_error,E), % nl(user_error), % DEBUG compile_extensional_act, compile_deranged_act. % compile_deranged/0 % Add constraints to enforce exhaustive subtyping covering, e.g.: % % bot % a f:bool g:bool % b f:plus g:minus % c f:minus g:plus % bool % plus % minus % % In TRALE, there are no objects of type a with f:minus g:minus or % f:plus g:plus, because all a-objects are of either type b or c. % Types, such as a, whose feature values are not exhaustively covered by % by their subtypes' feature values, are called *deranged* types. compile_deranged :- touch('.alec_throw'), absolute_file_name('.alec_throw',AbsFileName), retractall(ale_compiling(_)), assert(ale_compiling(AbsFileName)), compile_deranged_act, retract(ale_compiling(_)). compile_deranged_act :- alec_announce('Compiling subtype covering constraints...'), retractall(deranged(_,_)), retractall(deranged_maps(_,_)), retractall(maxcount(_,_,_)), compile_deranged_assert, assert(alec(trale_deranged)), compile('.alec_throw'). % % Constraint compiler patches % :- abolish([compile_cons/1,compile_cons_act/0]). % cons/2 capture - must map to trale_cons/2 so that compile_deranged can add % constraints for exhaustive subtype covering :- op(900,xfx,trale_cons). term_expansion((Type cons Cons),(Type trale_cons Cons)). % probably don't need to transform cons/2 layout compile_cons(File) :- abolish((trale_cons)/2),abolish((cons)/2),abolish(('*>')/2), reconsult(File), compile_cons. compile_cons_act :- alec_announce('Compiling type constraints...'), abolish((ct)/4), retractall(constrained(_)), % retract_fs_palettes(ct), retractall(complex_cons(_,_,_,_,_)), compile_complex_assert, link_cons_act, (current_predicate(cons,(_ cons _)) -> [bot,has,constraints] if_error ( bot cons _ ), [multiple,constraint,declarations,for,CType] if_error (bagof(CT,Cons^(CT cons Cons),CTypes), duplicated(CType,CTypes)), [constraint,declaration,given,for,atom] if_error ( (a_ _) cons _ ), assert(alec(ct)), \+ \+ compile('.alec_throw') ; ([no,constraints,found] if_warning true) ). link_cons :- touch('.alec_throw'), absolute_file_name('.alec_throw',AbsFileName), retractall(ale_compiling(_)), assert(ale_compiling(AbsFileName)), link_cons_act, retract(ale_compiling(_)). link_cons_act :- assert(alec(trale_link)), compile('.alec_throw'). :- op(900,xfx,'*>'). :- dynamic complex_cons/5. % Complex Antecedent Constraints % [User's Manual] [Reference Manual] compile_complex_assert :- current_predicate('*>',(_ *> _)) -> \+ (Antecedent *> Consequent goal Goal, find_narrow_vars(Antecedent,AntecNoQs,NarrowVars), find_trigger_type(AntecNoQs,bot,Trigger), assert(complex_cons(Trigger,AntecNoQs,Consequent,Goal,NarrowVars)), fail), \+ (Antecedent *> Consequent, \+ (Consequent = (_ goal _)), find_narrow_vars(Antecedent,AntecNoQs,NarrowVars), find_trigger_type(AntecNoQs,bot,Trigger), assert(complex_cons(Trigger,AntecNoQs,Consequent,true,NarrowVars)), fail) ; true. find_narrow_vars(Antecedent,AntecNoQs,NarrowVars) :- find_nv_act(Antecedent,AntecNoQs,[],NarrowVars). find_nv_act(X^(Antecedent),AntecNoQs,NVsIn,NVsOut) :- !,find_nv_act(Antecedent,AntecNoQs,[X|NVsIn],NVsOut). find_nv_act(AntecNoQs,AntecNoQs,NVs,NVs). find_trigger_type(Var,Trigger,Trigger) :- var(Var), !. find_trigger_type(Feat:_,TrigIn,TrigOut) :- !,introduce(Feat,Intro), unify_type(Intro,TrigIn,TrigOut). find_trigger_type((D1,D2),TrigIn,TrigOut) :- !,find_trigger_type(D1,TrigIn,TrigMid), find_trigger_type(D2,TrigMid,TrigOut). find_trigger_type((D1;D2),TrigIn,TrigOut) :- !,find_trigger_type(D1,TrigIn,TrigOut1), find_trigger_type(D2,TrigIn,TrigOut2), generalise(TrigOut1,TrigOut2,TrigOut). find_trigger_type(Type,TrigIn,TrigOut) :- type(Type), !,unify_type(Type,TrigIn,TrigOut). find_trigger_type(Ant,_,_) :- error_msg((nl,write('compile_cons: illegal description, '),write(Ant), write(', used in complex antecedent constraint'),nl)). % add deranged type map-checks to code stream after cons/2 constraints - shouldn't use % cons/2 itself because only resulting type's maps need to be checked, i.e. no inheritance :- abolish(ucons/5). ucons(Type,ET1,ET2,FS,SubGoals) :- findall(T,(clause(constrained(T),true), sub_type(T,Type), % find set of types whose constraints must be \+sub_type(T,ET1), % satisfied \+sub_type(T,ET2)),ConsTypes), map_cons(ConsTypes,FS,SubGoals,SubGoalsRest), ( clause(deranged_maps(Type,_),true) -> SubGoalsRest = [trale_maps_init(Type,FS)] ; SubGoalsRest = [] ). :- abolish(add_to_typecons/4). add_to_typecons(Type,ET,FS,SubGoals) :- findall(T,(clause(constrained(T),true), sub_type(T,Type), % find set of types whose constraints \+sub_type(T,ET)),ConsTypes), % must be satisfied map_cons(ConsTypes,FS,SubGoals,SubGoalsRest), ( clause(deranged_maps(Type,_),true) -> SubGoalsRest = [trale_maps_init(Type,FS)] ; SubGoalsRest = [] ). :- abolish(mgsat_cons/4). mgsat_cons(Type,FS,ConsGoals,ConsGoalsRest) :- findall(T,(clause(constrained(T),true), sub_type(T,Type)),ConsTypes), map_cons(ConsTypes,FS,ConsGoals,ConsGoalsMid), ( clause(deranged_maps(Type,_),true) -> ConsGoalsMid = [trale_maps_init(Type,FS)|ConsGoalsRest] ; ConsGoalsMid = ConsGoalsRest ). % compute_cons: collect complex antecedent constraints into cons/2 clauses compute_cons([],[end_of_file]). compute_cons([Type|Types],Code) :- (retrieve_user_cons(Type,Cons,Goal) % user has cons, either directly or through '*>'/2 -> Code = [(Type cons Cons goal Goal)|CodeRest] ; Code = CodeRest % nothing to add ), compute_cons(Types,CodeRest). retrieve_user_cons(Type,Cons,Goal) :- current_predicate(trale_cons,(_ trale_cons _)), (Type trale_cons TCons goal TGoal), !,findall(cc(CondVar,Cond,Conseq,CGoal), (clause(complex_cons(Type,Antec,Conseq,CGoal,NarrowVars),true), apply_narrow_vars(NarrowVars,(CondVar=Antec),Cond)), ComplexConss), ( ComplexConss == [] -> Cons = TCons, Goal = TGoal ; Cons = (FS,TCons), apply_ccs(ComplexConss,FS,TGoal,Goal) ). retrieve_user_cons(Type,Cons,Goal) :- current_predicate(trale_cons,(_ trale_cons _)), (Type trale_cons TCons), !,findall(cc(CondVar,Cond,Conseq,CGoal), (clause(complex_cons(Type,Antec,Conseq,CGoal,NarrowVars),true), apply_narrow_vars(NarrowVars,(CondVar=Antec),Cond)), ComplexConss), ( ComplexConss == [] -> Cons = TCons, Goal = true ; Cons = (FS,TCons), apply_ccs(ComplexConss,FS,true,Goal) ). retrieve_user_cons(Type,Cons,Goal) :- findall(cc(CondVar,Cond,Conseq,CGoal), (clause(complex_cons(Type,Antec,Conseq,CGoal,NarrowVars),true), apply_narrow_vars(NarrowVars,(CondVar=Antec),Cond)), ComplexConss), ComplexConss \== [], % otherwise fail to add no code Cons = FS, apply_ccs(ComplexConss,FS,true,Goal). apply_narrow_vars([],Cond,Cond). apply_narrow_vars([NV|NVs],CondIn,CondOut) :- apply_narrow_vars(NVs,NV^(CondIn),CondOut). apply_ccs([],_,TGoal,TGoal). apply_ccs([cc(FS,Cond,Conseq,CGoal)|CCs],FS,TGoal,Goal) :- apply_ccs(CCs,FS,(TGoal,when(Cond,(FS=Conseq,CGoal))),Goal). tag_maps([],[],Code,Code). tag_maps([Map|Maps],[TaggedMap|TaggedMaps],Code,CodeRest) :- tag_map(Map,TaggedMap,Code,CodeMid), tag_maps(Maps,TaggedMaps,CodeMid,CodeRest). tag_map(Map,TaggedMap,Code,CodeRest) :- add_tags(Map,TaggedMap), inequate_tags(TaggedMap,[],Code,CodeRest). add_tags([],[]). add_tags([T|TRest],[T-_Tag|TaggedTRest]) :- add_tags(TRest,TaggedTRest). inequate_tags([],_,Code,Code). inequate_tags([T-Tag|ToTagRest],TMapAccum,Code,CodeRest) :- inequate_tags_act(TMapAccum,T,Tag,ToTagRest,TMapAccum,Code,CodeRest). inequate_tags_act([],T,Tag,ToTagRest,TMapAccum,Code,CodeRest) :- inequate_tags(ToTagRest,[T-Tag|TMapAccum],Code,CodeRest). inequate_tags_act([T2-Tag2|TMapRest],T1,Tag1,ToTagRest,TMapAccum,Code, CodeRest) :- (\+ \+ unify_type(T1,T2,_)) -> inequate_tags_act(TMapRest,T1,Tag1,ToTagRest,TMapAccum,Code,CodeRest) ; Code = [dif(Tag1,Tag2)|CodeMid], inequate_tags_act(TMapRest,T1,Tag1,ToTagRest,TMapAccum, CodeMid,CodeRest). % could be more selective here - if appropriateness conditions at the current % type exclude equality, then no dif's are necessary. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Exhaustive subtype covering constraint compilation %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Subtype Covering % [User's Manual] [Reference Manual] % % Could optimise compiler by: % - using clause/2 or module-level variables for access to dynamic predicates % - precompiling code for attested branching factors that would eliminate % recursion through maps (represented as lists) % - tabulating minimal disjoint maps of deranged types for reuse while % checking supertypes % Could optimise run-time constraint-checking by: % - using generalise_maps/2 (see below) % - using a better data structure for FS's :- multifile alec_catch_hook/2. :- discontiguous alec_catch_hook/2. alec_catch_hook(trale_deranged,Code) :- multi_hash(0,(trale_maps_init/2),Code,[end_of_file]). trale_maps_init(Type,FS) if_b SubGoals :- clause(deranged_maps(Type,Maps),true), tag_maps(Maps,TaggedMaps,SubGoals,[trale_maps_init_act(Type,FS,TaggedMaps)]). compile_deranged_assert :- !,findall(Super-Sub,(non_a_type(Super), imm_sub_type(Super,Sub)),SubGEdges), vertices_edges_to_ugraph([],SubGEdges,SubG), % base_graph(SubG,BaseSubG), top_sort(SubG,RevSortedTypes), reverse(RevSortedTypes,SortedTypes), compute_maxcount(SortedTypes,SubG), compute_deranged(SortedTypes,SubG). % compute_cons(SortedTypes,Code). alec_catch_hook(trale_link,Code) :- findall(Type,type(Type),Types), % maxcount/3 and deranged/2 are already compute_cons(Types,Code). % there - just re-attach to user constraints % computeMaxCount % [User's Manual] [Reference Manual] % maxcount/2 counts the number of maximal types subsumed % by every type. maxcount/2 of every maximal type is 1. maxcount/2 of % a non-maximal type is the sum of the maxcounts of the types in its % immediate subtype cover, as given by the base subsumption graph. :- dynamic maxcount/3. compute_maxcount([],_). compute_maxcount([Type|Types],SubG) :- (Type = (a_ _) -> assert(maxcount(Type,1,[(a_ [])])) % treat a_/1 atoms specially ; neighbours(Type,SubG,ImmedSubCover), ( ImmedSubCover == [] -> assert(maxcount(Type,1,[Type])) ; maxcount_cover(ImmedSubCover,[],MaxCover), length(MaxCover,MaxCount), assert(maxcount(Type,MaxCount,MaxCover)) ) ), compute_maxcount(Types,SubG). % maxcount_map/2 % [User's Manual] [Reference Manual] % A map is a product of types, such as that found in a set of % appropriate features. maxcount_map/2 counts the number of maximal maps % subsumed by every map. A maximal map is one that has a maximal type in % every dimension (feature). maxcount_map/2 of a map is the product of the % maxcount/2 of every dimension. maxcount_map([],Count,Count). maxcount_map([T|MapRest],Accum,Count) :- clause(maxcount(T,TCount,_),true), NewAccum is Accum * TCount, maxcount_map(MapRest,NewAccum,Count). maxcount_map_list([],Total,Total). maxcount_map_list([Map|Maps],Accum,Total) :- maxcount_map(Map,1,Count), NewAccum is Accum + Count, maxcount_map_list(Maps,NewAccum,Total). maxcount_cover([],Accum,Cover) :- ord_union(Accum,Cover). % ord_union/2 uses divide-and-conquer maxcount_cover([Type|Types],Accum,Cover) :- clause(maxcount(Type,_,TCover),true), maxcount_cover(Types,[TCover|Accum],Cover). % compute_deranged: deranged/2 indicates the status of every type for the % purpose of classifying deranged types. A deranged type is one whose % map of appropriate value restrictions is not exhaustively covered by the % maps of appropriate value restrictions of its maximally specific subtypes. % The status is one of: % % normal: non-deranged types - these can be treated as maximal when % checking a potentially deranged supertype, even if they aren't. % deranged(NormalCover,NCRest): deranged - when checking potentially deranged % supertypes, these types must be replaced by a minimal covering % of non-deranged subtypes given by NormalCover-NCRest. % % Since atoms are downward-closed, we don't need to add an entry for them. % All maximal types are normal. :- dynamic deranged/2. :- dynamic deranged_maps/2. compute_deranged([],_). compute_deranged([Type|Types],SubG) :- approps(Type,FRs,_), ( FRs == [] -> compute_deranged(Types,SubG) % Type has no approp % features so dont add deranged/2 entry - includes a_ atoms ; maximal(Type) -> assert(deranged(Type,normal)), compute_deranged(Types,SubG) ; build_root_map(FRs,Root,MapFeats), neighbours(Type,SubG,Cover), normalise_cover(Cover,NormalCover), build_cover_maps(NormalCover,MapFeats,NMaps), minimise_disjoin_maps(NMaps,[],SubG,MDNMaps), atomic_equal(MDNMaps,Root,AEMaps), ( AEMaps == [] -> % no cover maps cover a_ atomic values - deranged append(NormalCover,NCRest,NCAssert), assert(deranged(Type,deranged(NCAssert,NCRest))), generalise_maps(MDNMaps,GenMaps), assert(deranged_maps(Type,GenMaps)) ; atomic_prune(Root,AEMaps,APRoot,APMaps), ( APRoot == [] -> % no other values to cover - normal assert(deranged(Type,normal)) ; maxcount_map(APRoot,1,RootCount), % use counts instead of types - this maxcount_map_list(APMaps,0,APCount), % is what makes this algorithm % polynomial in number of types (APCount < RootCount % Cover maps dont cover root map -> append(NormalCover,NCRest,NCAssert), % so root type is deranged assert(deranged(Type,deranged(NCAssert,NCRest))), generalise_maps(MDNMaps,GenMaps), assert(deranged_maps(Type,GenMaps)) ; % APCount = RootCount assert(deranged(Type,normal)) ) ) ), compute_deranged(Types,SubG) ). % atomic_prune/4 % [User's Manual] [Reference Manual] % having identified maps that cover the a_/1 atoms of the root % map (AMaps), prune off the dimensions that have a_/1 atoms from both the % AMaps and the root. The standard counting algorithm applies to what % remains (APMaps and APRoot). atomic_prune([],_,[],APMaps) :- atomic_prune_close(APMaps). atomic_prune([RType|RTypes],AMaps,RPTypes,APMaps) :- ( RType = (a_ _) -> atomic_prune_delete(AMaps,AMapsRest), atomic_prune(RTypes,AMapsRest,RPTypes,APMaps) ; RPTypes = [RType|RPTypesRest], atomic_prune_copy(AMaps,APMaps,AMapsRest,APMapsRest), atomic_prune(RTypes,AMapsRest,RPTypesRest,APMapsRest)). atomic_prune_delete([],[]). atomic_prune_delete([[_Type|Types]|MapsRest],[Types|NewMapsRest]) :- atomic_prune_delete(MapsRest,NewMapsRest). atomic_prune_close([]). atomic_prune_close([[]|PMapsRest]) :- atomic_prune_close(PMapsRest). atomic_prune_copy([],[],[],[]). atomic_prune_copy([[Type|Types]|MapsRest],[[Type|PTypes]|PMapsRest], [Types|NewMapsRest],[PTypes|NewPMapsRest]) :- atomic_prune_copy(MapsRest,PMapsRest,NewMapsRest,NewPMapsRest). % atomic_equal/3: find those maps which, in every dimension for which the root % map has bot or an a_/1 atom, have types that exhaustively cover the root % map's restrictions. a_/1 atoms must be treated specially because their % arguments are Prolog terms, and in the lattice of generalised atomic % formulae, every non-ground term has an infinite number of maximal subtypes % in its cover. AEMaps are those maps that manage to encompass these % infinite covers (with infinite covers of their own). In contrast to the % rest of the type hierarchy, no collection of finite covers will suffice. % % If the root map does not subsume a_/1 atoms in any dimension, then all % Maps are trivially included in AEMaps. atomic_equal([],_,[]). atomic_equal([Map|Maps],Root,AEMaps) :- atomic_equal_map(Root,Map,Map,Maps,Root,AEMaps). atomic_equal_map([],[],Map,Maps,Root,[Map|AEMapsRest]) :- atomic_equal(Maps,Root,AEMapsRest). atomic_equal_map([RType|RTypes],[MType|MTypes],Map,Maps,Root,AEMaps) :- ( RType = (a_ RX) -> MType = (a_ MX), variant(MX,RX) ; RType = bot -> ( MType = (a_ MX) -> var(MX) ; true) % other types are allowed - it could be that % a_/1 atoms do not occur in any maximal extension % and therefore should never occur. ; true) -> atomic_equal_map(RTypes,MTypes,Map,Maps,Root,AEMaps) ; atomic_equal(Maps,Root,AEMaps). % normalise_cover: replace all deranged types in Cover with their non-deranged % subtype covers normalise_cover([],[]). normalise_cover([Type|Types],NormalCover) :- clause(deranged(Type,Status),true), (Status == normal -> NormalCover = [Type|NCRest], normalise_cover(Types,NCRest) ; % Status = deranged(NormalCover,NCRest), arg(1,Status,NormalCover), arg(2,Status,NCRest), normalise_cover(Types,NCRest)). % minimise_disjoin_cover/4: for each type in cover, first eliminate all types % that it subsumes (or eliminate it if it is subsumed), then ensure that it % is disjoint with every other type (doesn't unify). If it is not, create % a new minimal cover of it that isolates the intersection type, eliminates % it, and proceed with the remaining cover types instead. minimise_disjoin_cover([],MDCover,_,MDCover). minimise_disjoin_cover([C|Covers],Accum,SubG,MDCover) :- minimise_disjoin_cover_act(Accum,C,NewAccum,NewAccum,Covers,SubG,MDCover). minimise_disjoin_cover_act([],C,NewAccum,NewAccumRest,Covers,SubG,MDCover) :- ( C = (a_ _) -> NewAccumRest = [C], % cant dissolve this minimise_disjoin_cover(Covers,NewAccum,SubG,MDCover) ; NewAccumRest = [], disjoin_cover_act(NewAccum,C,NewerAccum,NewerAccum,Covers,SubG,MDCover) ). minimise_disjoin_cover_act([AccC|AccumRest],C,NewAccum,NewAccumRest,Covers, SubG,MDCover) :- (sub_type(AccC,C) -> NewAccumRest = [AccC|AccumRest], minimise_disjoin_cover(Covers,NewAccum,SubG,MDCover) % throw out C ; (sub_type(C,AccC) -> minimise_disjoin_cover_act(AccumRest,C,NewAccum,NewAccumRest,Covers, SubG,MDCover) % throw out AccC ; NewAccumRest = [AccC|NewAccumRest2], minimise_disjoin_cover_act(AccumRest,C,NewAccum,NewAccumRest2,Covers, SubG,MDCover))). disjoin_cover_act([],C,NewAccum,[C],Covers,SubG,MDCover) :- minimise_disjoin_cover(Covers,NewAccum,SubG,MDCover). disjoin_cover_act([AccC|AccumRest],C,NewAccum,NewAccumRest,Covers,SubG, MDCover) :- unify_type(AccC,C,UnifC) -> dissolve_map_dim(C,UnifC,SubG,NewCovers,Covers), NewAccumRest = [AccC|AccumRest], minimise_disjoin_cover(NewCovers,NewAccum,SubG,MDCover) ; NewAccumRest = [AccC|NewAccumRest2], disjoin_cover_act(AccumRest,C,NewAccum,NewAccumRest2,Covers,SubG, MDCover). % minimise_disjoin_maps: for each map, first eliminate all maps that it % subsumes (or eliminate it if it is subsumed), then ensure that it is % disjoint with every other map (doesn't unify coordinate-wise). If it % is not, create a new minimal cover of it that isolates the intersection, % eliminate the intersection, and proceed with the remaining maps instead. % This is a generalisation of minimise_disjoin_cover/4 to products of types. minimise_disjoin_maps([],MDMaps,_,MDMaps). minimise_disjoin_maps([Map|Maps],Accum,SubG,MDMaps) :- minimise_disjoin_maps_act(Accum,Map,NewAccum,NewAccum,Maps,SubG,MDMaps). minimise_disjoin_maps_act([],Map,NewAccum,NewAccumRest,Maps,SubG,MDMaps) :- ( a_atoms(Map) -> NewAccumRest = [Map], % cant dissolve these minimise_disjoin_maps(Maps,NewAccum,SubG,MDMaps) ; NewAccumRest = [], disjoin_maps_act(NewAccum,Map,NewerAccum,NewerAccum,Maps,SubG,MDMaps) ). minimise_disjoin_maps_act([AccMap|AccumRest],Map,NewAccum,NewAccumRest,Maps, SubG,MDMaps) :- (subsume_map(AccMap,Map) -> NewAccumRest = [AccMap|AccumRest], minimise_disjoin_maps(Maps,NewAccum,SubG,MDMaps) % throw out Map ; (subsume_map(Map,AccMap) -> minimise_disjoin_maps_act(AccumRest,Map,NewAccum,NewAccumRest,Maps, SubG,MDMaps) % throw out AccMap ; NewAccumRest = [AccMap|NewAccumRest2], minimise_disjoin_maps_act(AccumRest,Map,NewAccum,NewAccumRest2,Maps, SubG,MDMaps))). disjoin_maps_act([],Map,NewAccum,[Map],Maps,SubG,MDMaps) :- minimise_disjoin_maps(Maps,NewAccum,SubG,MDMaps). disjoin_maps_act([AccMap|AccumRest],Map,NewAccum,NewAccumRest,Maps,SubG, MDMaps) :- unify_map(AccMap,Map,UnifMap) -> dissolve_map(Map,UnifMap,SubG,NewMaps,Maps), NewAccumRest = [AccMap|AccumRest], minimise_disjoin_maps(NewMaps,NewAccum,SubG,MDMaps) ; NewAccumRest = [AccMap|NewAccumRest2], disjoin_maps_act(AccumRest,Map,NewAccum,NewAccumRest2,Maps,SubG, MDMaps). dissolve_map(Ts,Ss,SubG,NewMaps,NewMapsRest) :- dissolve_map_act(Ts,Ss,SubG,NewMapsbyDim), permute_dimensions(NewMapsbyDim,NewMapsbyType,NewMapsRest), select(Ss,NewMapsbyType,NewMaps). % a_ atoms will unify their args here dissolve_map_act([],[],_,[]). dissolve_map_act([T|Ts],[S|Ss],SubG,[OtherSs|OtherDims]) :- dissolve_map_dim(T,S,SubG,OtherSsBag,[]), remove_duplicates(OtherSsBag,OtherSs), dissolve_map_act(Ts,Ss,SubG,OtherDims). dissolve_map_dim(T,S,SubG,OtherSs,OtherSsRest) :- (variant(T,S) % variant/2 for equality check with a_ atoms -> OtherSs = [T|OtherSsRest] ; (sub_type(T,S) -> ( T = (a_ _) -> OtherSs = [T|OtherSsRest] ; neighbours(T,SubG,Neibs), dissolve_map_neibs(Neibs,S,SubG,OtherSs,OtherSsRest) ) ; OtherSs = [T|OtherSsRest])). dissolve_map_neibs([],_,_,OtherSs,OtherSs). dissolve_map_neibs([N|Neibs],S,SubG,OtherSs,OtherSsRest) :- dissolve_map_dim(N,S,SubG,OtherSs,OtherSsMid), dissolve_map_neibs(Neibs,S,SubG,OtherSsMid,OtherSsRest). % permute_dimensions/3: Convert [[a1,a2,...,a_n1],[b1,b2,...,b_n2],...] to % [[a1,b1,...],[a1,b2,...],[a2,b1,...],[a2,b2,...],...[a_n1,b_n2,...]]. % This is exponential in the number of features per type, i.e., max(i)(ni). permute_dimensions(NewMapsbyDim,NewMapsbyType,NewMapsRest) :- findall(Map,permute_dimensions_act(NewMapsbyDim,Map), NewMapsbyType,NewMapsRest). permute_dimensions_act([],[]). permute_dimensions_act([Dim|DimsRest],[T|MapRest]) :- member(T,Dim), % this leaves a choice-point that findall/4 backtracks to permute_dimensions_act(DimsRest,MapRest). % generalise_maps/2: Given a list of mutually disjoint maps, add all of the % dimension-relative generalisations of any sublist, then remove all maps % subsumed by another map (in all dimensions) on the list. A dimension- % relative (or k-relative) generalisation of a set of maps, A, is a map in % which, for one dimension, k, it has a type that is exhaustively covered by % the k-dimensions of A and, for all other dimensions, i, has a type that is % the intersection (unification) of the i-dimensions of A. % It can be shown that if a map is exhaustively covered by a finite set of % maps A, then it can be derived from A by a finite sequence of dimension- % relative generalisations. Because these derivation sequences satisfy the % Church-Rosser property, each dimension in turn can be closed under its % relative generalisations once. % Closing under exhaustive generalisation can allow us to kill coroutined % constraints on feature structures earlier by identifying more general maps % that satisfy deranged type constraints. generalise_maps(Maps,Maps). % skip for now %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Run-time exhaustive type constraint enforcement %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% trale_maps_init_act(CType,AleFS,TMaps) :- deref(AleFS,Tag,SVs), (SVs =.. [CType|Vs] -> % can't be a_/1 atom - no features project_map(Vs,VsMap,Condition,nonvar(Tag)), trale_check_maps(TMaps,VsMap,[],Condition,CType,AleFS) ; true % if the new type is deranged, then its own exhaustive % type constraints will take care of it. If it is % normal, then its appropriate value restrictions will % take care of it. ). trale_maps(CType,AleFS,TMaps,VsMap) :- trale_deref(AleFS,Tag,SVs), ( var(Tag) -> ( functor(SVs,CType,_) % can't be a_/1 atom - no features -> update_map(VsMap,NewVsMap,Condition,nonvar(Tag),Condition,CType,AleFS, TMaps,NewVsMap,check) ; true) % if the new type is deranged, then its own exhaustive % type constraints will take care of it. If it is % normal, then its appropriate value restrictions will % take care of it. ; Tag=fully(FTag,FSVs) -> when(nonvar(FSVs),(FSVs =.. [_|Vs], % can't be a_/1 atom - no features fully_deref_map(Vs,NewVsMap,Condition,nonvar(FTag)), when(Condition,trale_maps(CType,FTag-FSVs,TMaps,NewVsMap)))) ; % number(Tag), % used by pp_fs to mark coindexing true). % simply succeed - constraint will be revived when stack unwinds % at the end of the pp_fs call trale_check_maps([],VsMap,TMaps,Condition,CType,AleFS) :- TMaps \== [], % more to try or else VsMap cannot have a maximal extension when(Condition,trale_maps(CType,AleFS,TMaps,VsMap)). trale_check_maps([TMap|TMapsRest],VsMap,TMapAccum,Condition,CType,AleFS) :- (subsume_tmap(TMap,VsMap) % VsMap is guaranteed to have a maximal extension -> true ; \+ \+ unify_tmap_check(TMap,VsMap) % VsMap has one now, but might lose it % later -> trale_check_maps(TMapsRest,VsMap,[TMap|TMapAccum],Condition,CType, AleFS) ; trale_check_maps(TMapsRest,VsMap,TMapAccum,Condition,CType,AleFS)). % throw this Map out and try the others % project_map/4: create a feature value map from Vs, along with a conditional for % delaying until a change is observed. project_map([],[],CondRest,CondRest). project_map([V|Vs],[VType-VTag|VsMapRest],(nonvar(VTag);CondMid),CondRest) :- deref(V,VTag,VSVs), ( functor(VSVs,'a_',1) -> VType = VSVs ; functor(VSVs,VType,_) ), project_map(Vs,VsMapRest,CondMid,CondRest). % update_map/9: update the feature value map VsMap after one or more referencing and % full dereferencing events. Also create a new conditional. If there were only % referencing events, check the maps. update_map([],[],CondRest,CondRest,Condition,CType,AleFS,TMaps,NewVsMap,Action) :- ( Action == resuspend -> when(Condition,trale_maps(CType,AleFS,TMaps,NewVsMap)) ; % Action == check, trale_check_maps(TMaps,NewVsMap,[],Condition,CType,AleFS) ). update_map([VType-VTag|VsMap],[VType-NewVTag|NewVsMapRest],(nonvar(NewVTag);CondMid), CondRest,Condition,CType,AleFS,TMaps,NewVsMap,Action0) :- ( var(VTag) -> NewVTag = VTag, Action = Action0 ; VTag = NewVTag-_ -> Action = Action0 ; VTag = fully(NewVTag,_) -> Action = resuspend ), update_map(VsMap,NewVsMapRest,CondMid,CondRest,Condition,CType,AleFS,TMaps,NewVsMap,Action). % fully_deref_map/4: update a feature value map for a FS that has just undergone full % dereferencing, create a new conditional, and resuspend. This is identical to % project_map/4 except that it delays rather than dereferences. fully_deref_map([],[],CondRest,CondRest). fully_deref_map([V|Vs],[VType-VTag|VsMap],(nonvar(VTag);CondMid),CondRest) :- when(nonvar(V),(arg(1,V,VTag), arg(2,V,VSVs), when(nonvar(VSVs),(( functor(VSVs,'a_',1) -> VType = VSVs ; functor(VSVs,VType,_) ))))), fully_deref_map(Vs,VsMap,CondMid,CondRest). % trale_deref/4: dereference a feature structure, but stop at tags % instantiated to fully/2 (used by fully_deref) or numbers (used by pp_fs). trale_deref(Tag-SVs,TagOut,SVsOut) :- var(Tag) -> TagOut = Tag, SVsOut = SVs ; functor(Tag,-,2) -> trale_deref(Tag,TagOut,SVsOut) ; TagOut = Tag, % stop at number or fully/2. SVsOut = SVs. %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Signature file input - calls read_ths/4 from pth.pl and converts to ALE % sub/intro representation in O(n log n) time %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% alec_catch_hook(trale_signature,Code) :- !,(current_predicate(signature,signature(_)) -> findall(File,signature(File),[SigFile|Rest]), [multiple,signature,specifications,found,'-',using,'first:',SigFile] if_warning (Rest \== []) ; SigFile = 'signature' ), read_ths(SigFile,SubL,AppL,_), sort(SubL,SortedSubL), trale_sub(SortedSubL,Code,CodeMid), sort(AppL,SortedAppL), trale_intro(SortedAppL,CodeMid,[end_of_file]). trale_sub([X-Y|SubLMid],[(X sub [Y|Ys])|CodeMid],CodeRest) :- trale_sub_act(SubLMid,X,Ys,CodeMid,CodeRest). trale_sub_act([],_,[],Code,Code). trale_sub_act([X-Y|SubLMid],Last,Ys,Code,CodeRest) :- (X = Last -> Ys = [Y|YsRest], trale_sub_act(SubLMid,Last,YsRest,Code,CodeRest) ; Ys = [], Code = [(X sub [Y|YsRest])|CodeMid], trale_sub_act(SubLMid,X,YsRest,CodeMid,CodeRest)). trale_intro([],CodeRest,CodeRest). trale_intro([app(T,F,R,_)|AppLMid],[(T intro [F:R|FRs])|CodeMid],CodeRest) :- trale_intro_act(AppLMid,T,FRs,CodeMid,CodeRest). trale_intro_act([],_,[],Code,Code). trale_intro_act([app(T,F,R,_)|AppLMid],Last,FRs,Code,CodeRest) :- (T = Last -> FRs = [F:R|FRsRest], trale_intro_act(AppLMid,Last,FRsRest,Code,CodeRest) ; FRs = [], Code = [(T intro [F:R|FRsRest])|CodeMid], trale_intro_act(AppLMid,T,FRsRest,CodeMid,CodeRest)). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Utilities %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% a_atoms([]). a_atoms([(a_ _)|AsRest]) :- a_atoms(AsRest). subsume_map([],[]). subsume_map([T|Ts],[S|Ss]) :- sub_type(T,S), subsume_map(Ts,Ss). unify_map([],[],[]). unify_map([T1|T1s],[T2|T2s],[T3|T3s]) :- unify_type(T1,T2,T3), unify_map(T1s,T2s,T3s). subsume_tmap([],[]). subsume_tmap([T-_|Ts],[S-_|Ss]) :- % dont need to check tags - if Ss is sub_type(T,S), % subsumed, then structure-sharing must subsume_map(Ts,Ss). % be allowed % must call this predicate inside \+ \+ in order not to bind a_ atoms or % tags permanently unify_tmap_check([],[]). unify_tmap_check([T1-Tag|T1s],[T2-Tag|T2s]) :- unify_type(T1,T2,_), unify_tmap_check(T1s,T2s). build_root_map([],[],[]). build_root_map([F:R|FRs],[R|Root],[F|MapFeats]) :- build_root_map(FRs,Root,MapFeats). build_cover_maps([],_,[]). build_cover_maps([Type|Types],MapFeats,[Map|Maps]) :- build_cover_map(MapFeats,Type,Map), build_cover_maps(Types,MapFeats,Maps). build_cover_map([],_,[]). build_cover_map([F|Feats],Type,[R|Map]) :- approp(F,Type,R), build_cover_map(Feats,Type,Map). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Logical-Variable Macros with Modes % [User's Manual] [Reference Manual] %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % notation: % someMacro(X-a,Y-b) := t, abc:X, def:Y. % OR % someMacro(X,Y) := t, abc:X, def:Y. :- op(1150,xfx,':='). :- abolish([compile_fun/1,compile_fun/0,compile_fun_act/0]). compile_fun(File):- abolish(('+++>')/2), abolish((fun)/1), retractall(fun_exp(_,_,_)), abolish((macro)/2), abolish(':='/2), reconsult(File), compile_fun. compile_fun :- touch('.alec_throw'), absolute_file_name('.alec_throw',AbsFileName), retractall(ale_compiling(_)), assert(ale_compiling(AbsFileName)), compile_fun_act, retract(ale_compiling(_)). compile_fun_act :- alec_announce('Compiling functional and macro descriptions...'), retractall(fun_spec(_,_,_)), compile_fun_assert, compile_macro_act. compile_macro_act :- current_predicate(':=',(_ := _)) -> assert(alec(macro)), compile('.alec_throw') ; true. alec_catch_hook(macro,[(:- multifile macro/2)|Code]) :- % this is going to create warnings whenever user defines macro/2 without % multifile - KNOWN BUG findall(logmacro(LVLHS,RHS),(LVLHS := RHS),LogMacros), compute_macros(LogMacros,Code). compute_macros([],[end_of_file]). compute_macros([logmacro(LVLHS,RHS)|LogMacros],[(LHS macro RHS)|Code]) :- functor(LVLHS,MacroName,Arity), % match the macro by name and arity functor(LHS,MacroName,Arity), ( add_lv_macro_descs(0,Arity,LVLHS,LHS) -> compute_macros(LogMacros,Code) ; error_msg((nl,write('error: logical macro arguments must be unshared variables in '), write(LVLHS),nl)) ). add_lv_macro_descs(A,A,_,_) :- !. add_lv_macro_descs(OldP,A,LVLHS,LHS) :- P is OldP + 1, arg(P,LVLHS,LVArg), % LVArg is either macro-var. or macrovar-Desc pair arg(P,LHS,TArg), ( var(LVArg) -> LVArg = (TArg,_) % if Desc is missing, interpret as bot ; LVArg = Var-Desc -> var(Var), % check before instantiating to catch shared vars Var = (TArg,Desc,_) % adding anonymous variable pushes structure % sharing on Prolog level in RHS into % structure sharing on (ALE) logical level. ), add_lv_macro_descs(P,A,LVLHS,LHS). % ------------------------------------------------------------------------------ % generalise(Type1:type,Type2:type,TypeGen:type) % ------------------------------------------------------------------------------ % The meet of Type1 and Type2 % ------------------------------------------------------------------------------ generalise(bot,a_ _,bot) :- !. generalise(a_ _,bot,bot) :- !. generalise(a_ X,a_ Y,a_ Z) :- !,term_subsumer(X,Y,Z). generalise(Type1,Type2,TypeGLB) :- findall(TypeLB,(sub_type(TypeLB,Type1), sub_type(TypeLB,Type2)),TypeLBs), map_max(TypeLBs,[],TypeGLBs), TypeGLBs = [TypeGLB]. map_max([],SsMax,SsMax). map_max([S|Ss],SsTemp,SsMax) :- insert_if_maximal(SsTemp,S,SsTempNew), map_max(Ss,SsTempNew,SsMax). insert_if_maximal([],S,[S]). insert_if_maximal([S2|Ss2],S,[S2|Ss2]):- sub_type(S,S2), !. insert_if_maximal([S2|Ss2],S,Ss3):- sub_type(S2,S), !, insert_if_maximal(Ss2,S,Ss3). insert_if_maximal([S2|Ss2],S,[S2|Ss3]):- insert_if_maximal(Ss2,S,Ss3). %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Banner %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% :- nl,write(' TRALE Version 1.0; April, 2002 Copyright (C) 2002, Gerald Penn All rights reserved'),nl.