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