% ==============================================================================
% ALE -- Attribute Logic Engine
% ==============================================================================
% Version 3.0  ---  May, 1998
% Developed under: SICStus Prolog, Version 3.0 #6

% Authors:

% Bob Carpenter                     
% ---------------------------
% Bell Laboratories
% Lucent Technologies              
% 600 Mountain Ave., 2D-329        
% Murray Hill, NJ 07974            
% USA                              
% carp@research.bell-labs.com       
%
% Gerald Penn
% --------------------------------
% Sonderforschungsbereich 340
% Universitaet Tuebingen
% Kl. Wilhelmstr. 113
% 72074 Tuebingen
% Germany
% gpenn@sfs.nphil.uni-tuebingen.de
%

% Quintus patch code

:- no_style_check(discontiguous).

findall(Temp,Goal,NewBag,Remainder) :-
  findall(Temp,Goal,Bag),
  append(Bag,Remainder,NewBag).

% :- multifile portray_message/2.
% portray_message(warning,no_match(abolish(_))). % suppress abolish/1 warnings

% end Quintus patch code

:- prolog_flag(character_escapes,_,off).
:- use_module(library(terms),[subsumes_chk/2]).

:- dynamic verbose_interpreter/0.
:- dynamic quiet_interpreter/0.
:- dynamic no_interpreter/0.
:- dynamic no_subsumption/0.
:- dynamic go/1.
:- dynamic suppress_adderrs/0.
:- dynamic parsing/0, generating/0.

parse :-
  retractall(generating),
  asserta(parsing),
  nl,write('compiler will produce code for parsing only'),
  nl.

generate :-
  retractall(parsing),
  asserta(generating),
  nl,write('compiler will produce code for generation only'),
  nl.

parse_and_gen :-
  asserta(parsing),
  asserta(generating),
  nl,write('compiler will produce code for parsing and generation'),
  nl.

interp :-
  retractall(quiet_interpreter),
  retractall(no_interpreter),
  asserta(verbose_interpreter),
  nl, write('interpreter is active'),
  nl.

nointerp :-
  retractall(verbose_interpreter),
  retractall(quiet_interpreter),
  asserta(no_interpreter),
  nl, write('interpreter is inactive'),
  nl.

subtest :-
  retractall(no_subsumption),
  nl, write('edge subsumption checking active'),
  nl.
nosubtest :-
  asserta(no_subsumption),
  nl, write('edge subsumption checking inactive'),
  nl.

secret_quiet :-
  retractall(verbose_interpreter),
  retractall(no_interpreter),
  asserta(quiet_interpreter).
secret_verbose :-
  quiet_interpreter,
  !,retractall(quiet_interpreter),
  retractall(no_interpreter),
  asserta(verbose_interpreter).
secret_verbose.

clear :-
  retractall(edge(_,_,_,_,_,_,_,_)),
  retractall(parsing(_)),
  retractall(num(_)), % edge index
  retractall(go(_)),  % interpreter go flag
  secret_verbose.

noadderrs :-
  asserta(suppress_adderrs),
  nl, write('Errors from adding descriptions will be suppressed.'),
  nl.
adderrs :-
  retractall(suppress_adderrs),
  nl, write('Errors from adding descriptions will be displayed.'),
  nl.

secret_noadderrs :-
  asserta(suppress_adderrs).
secret_adderrs :-
  retractall(suppress_adderrs).

% ==============================================================================
% Operators
% ==============================================================================

% ------------------------------------------------------------------------------
% SRK Descriptions
% ------------------------------------------------------------------------------
:-op(375,fx,a_).
:-op(375,fx,@).
:-op(700,xfx,=@).
%:-op(700,xfx,==).
:-op(775,fx,=\=).
:-op(800,xfy,:).
%:-op(1000,xfy,',').
%:-op(1100,xfy,';').

% ------------------------------------------------------------------------------
% Signatures
% ------------------------------------------------------------------------------
:- dynamic sub_def/2.

:-op(800,xfx,goal).
:-op(900,xfx,cons).
:-op(800,xfx,intro).
:-op(900,xfx,sub).
:-op(900,xfx,sub_def).
:-op(900,xfx,subs).

% ------------------------------------------------------------------------------
% Grammars
% ------------------------------------------------------------------------------
:-op(1125,xfy,then).
:-op(1150,xfx,===>).
:-op(1150,xfx,--->).
:-op(1150,xfx,macro).
:-op(1150,xfx,+++>).
:-op(1150,fx,empty).
:-op(1175,xfx,rule).
:-op(1175,xfx,lex_rule).
:-op(1160,xfx,morphs).
:-op(1125,xfx,'**>').
:-op(950,xfx,when).
:-op(900,xfx,becomes).
:-op(1175,fx,semantics).

% ------------------------------------------------------------------------------
% Definite Clauses
% ------------------------------------------------------------------------------
:-op(1150,xfx,if).

% ------------------------------------------------------------------------------
% Compiler
% ------------------------------------------------------------------------------
:-op(800,xfx,if_h).
:-op(800,xf,if_h).
:-op(800,xfx,if_b).
:-op(800,xf,if_b).
:-op(800,xfx,if_error).   
:-op(800,xfx,if_warning_else_fail).   
:-op(800,xfx,if_warning).

% ------------------------------------------------------------------------------
% I/O
% ------------------------------------------------------------------------------
:-op(1125,fx,mgsat).
:-op(1100,fx,macro).
:-op(1100,fx,query).
:-op(1100,fx,rule).
:-op(1100,fx,lex_rule).
:-op(1100,fx,show_clause).
:-op(1100,fx,rec).
:-op(800,fx,show_type).
:-op(500,fx,no_write_type).
:-op(500,fx,no_write_feat).  


% ==============================================================================
% Type Inheritance and Unification
% ==============================================================================

% Type:<type> sub Types:<type>s intro FRs:<fv>s                             user
% ------------------------------------------------------------------------------
% Types is set of immediate subtypes of Types and FRs is list
% of appropriate features paired with restrictions on values.
% When FRs is not specified, it is equivalent to '[]'.
% ------------------------------------------------------------------------------

% Type:<type> sub_def Types:<type>s intro FRs:<fv>s
% ------------------------------------------------------------------------------
%  Same as sub except these are asserted by the default type preprocessors
% ------------------------------------------------------------------------------

% Type:<type> subs Types:<types>s intro FRs:<fv>s
% ------------------------------------------------------------------------------
% Subsumption predicate for use in ALE.  If there is a sub_def clause with
%  left-hand argument Type, then subs uses that; otherwise, it uses sub
% ------------------------------------------------------------------------------
T subs Ts :-
  T sub_def Ts.
T subs Ts :-
  T sub Ts,
  \+ T sub_def _.


% ------------------------------------------------------------------------------
% Type:<type> cons Cons:<desc> goal Goal:<goal>                             user
% ------------------------------------------------------------------------------
% Cons is the general description which must be satisfied by all structures of
%  type Type, and Goal is an optional procedural attachment which also must
%  be satisfied when present.  An absent constraint is equivalent to 'bot', 
%  and an absent goal is equivalent to 'true'.
% ------------------------------------------------------------------------------

% ------------------------------------------------------------------------------
% type(Type:<type>)                                                         eval
% ------------------------------------------------------------------------------
% Type is a type
% ------------------------------------------------------------------------------
type(Type):- 
    Type subs _.
type(a_ _).

% ------------------------------------------------------------------------------
% immed_subtypes(Type:<type>, SubTypes:<type>s)                             eval
% ------------------------------------------------------------------------------
% SubTypes is set of immediate subtypes of Type (SubTypes cover Type)
% ------------------------------------------------------------------------------
immed_subtypes(Type,SubTypes):-
    Type subs SubTypes, 
    \+ (SubTypes = (_ intro _))
  ; Type subs SubTypes intro _.

% ------------------------------------------------------------------------------
% imm_sub_type(Type:<type>, TypeSub:<type>)                                 eval
% ------------------------------------------------------------------------------
% TypeSub is immediate subtype of Type 
% ------------------------------------------------------------------------------
imm_sub_type(Type,TypeSub):-
  immed_subtypes(Type,TypeSubs),
  member(TypeSub,TypeSubs).

% ------------------------------------------------------------------------------
% immed_cons(Type:<type>,Cons:<desc>)
% ------------------------------------------------------------------------------
immed_cons(Type,Cons) :-
  type(Type),               % ALE WON'T CATCH A CONSTRAINT DEFINED FOR AN ATOM
  (\+current_predicate(cons,(_ cons _)),  %  UNTIL THE COMPILER IS RUN
   !,Cons = none
  ;Type cons Cons goal _,!  
  ;Type cons Cons).
  
% ------------------------------------------------------------------------------
% sub_type(Type:<type>, TypeSub:<type>)                                    mh(1)
% ------------------------------------------------------------------------------
% TypeSub is subtype of Type
% ------------------------------------------------------------------------------
(sub_type(Type,Type) if_h) :-
  type(Type).
(sub_type(Type,TypeSub) if_h) :-
  setof(Type-TypeSubs, immed_subtypes(Type,TypeSubs), Graph),
  transitive_closure(Graph,NewGraph),
  member(Type-TypeSubs,NewGraph),
  member(TypeSub,TypeSubs),
            [subtyping,cycle,at,Type] if_error
                 TypeSub = Type.
(sub_type(bot,a_ _) if_h).
(sub_type(a_ X,a_ Y) if_h [subsumes_chk(X,Y)]).

% ------------------------------------------------------------------------------
% unify_type(Type1:<type>, Type2:<type>, TypeLUB:<type>)                   mh(1)
% ------------------------------------------------------------------------------
% Type1 unified with Type2 is TypeLUB
% ------------------------------------------------------------------------------
(unify_type(Type1,Type2,TypeLUB) if_h) :-
  setof(TypeUB, ( sub_type(Type1,TypeUB), \+(Type1 = a_ _),
                  sub_type(Type2,TypeUB), \+(Type2 = a_ _)), TypeUBs),
  map_minimal(TypeUBs,[],TypeLUBs),
            [consistent,Type1,and,Type2,have,multiple,mgus,TypeLUBs] if_error
                 ( TypeLUBs = [_,_|_],
                   Type1 @< Type2 ),
  TypeLUBs = [TypeLUB].
(unify_type(bot,a_ X,a_ X) if_h).
(unify_type(a_ X,bot,a_ X) if_h).
(unify_type(a_ X,a_ X,a_ X) if_h).  % subsumes_chk/2 unhooks the vars - need
                                    % to do it ourselves

% ------------------------------------------------------------------------------
% map_minimal(Ss:<types>, SsTemp:<types>, SsMin:<types>)
% ------------------------------------------------------------------------------
% holds if SsMin is the list of minimal types of Ss unioned with SsTemp;
% elements of SsTemp are always incomparable
% ------------------------------------------------------------------------------
map_minimal([],SsMin,SsMin).
map_minimal([S|Ss],SsTemp,SsMin):-
  insert_if_minimal(SsTemp,S,SsTempNew),
  map_minimal(Ss,SsTempNew,SsMin).

% ------------------------------------------------------------------------------
% insert_if_minimal(Ss:<type>s, S:<type>, Ss2:<type>s)
% ------------------------------------------------------------------------------
% Ss2 is minimal elts of (Ss U {S}) where we know Ss are incomparable
% ------------------------------------------------------------------------------
insert_if_minimal([],S,[S]).
insert_if_minimal([S2|Ss2],S,[S2|Ss2]):-
  sub_type(S2,S), !.
insert_if_minimal([S2|Ss2],S,Ss3):-
  sub_type(S,S2), !,
  insert_if_minimal(Ss2,S,Ss3).
insert_if_minimal([S2|Ss2],S,[S2|Ss3]):-
  insert_if_minimal(Ss2,S,Ss3).

% ------------------------------------------------------------------------------
% unify_types(Types:<type>s, Type:<type>)                                
% ------------------------------------------------------------------------------
% Type is unification of Types
% ------------------------------------------------------------------------------
unify_types([],bot).
unify_types([Type|Types],TypeUnif):-
  unify_types(Types,Type,TypeUnif).

% ------------------------------------------------------------------------------
% unify_types(Types:<type>s, Type:<type>, TypeUnif:<type>)                
% ------------------------------------------------------------------------------
% TypeUnif is unification of set consisting of Types and Type
% ------------------------------------------------------------------------------
unify_types([],Type,Type).
unify_types([Type|Types],TypeIn,TypeOut):-
  unify_type(Type,TypeIn,TypeMid),
  unify_types(Types,TypeMid,TypeOut).

% ------------------------------------------------------------------------------
% extensional(Sort:<sort)
% ------------------------------------------------------------------------------
% Sort is an extensional sort.  Extensional sorts are assumed to be maximal.
% ------------------------------------------------------------------------------


% ==============================================================================
% Appropriateness
% ==============================================================================

% ------------------------------------------------------------------------------
% feature(F:<feat>)
% ------------------------------------------------------------------------------
% holds if $F$ is a feature mentioned somewhere in the code
% ------------------------------------------------------------------------------
feature(Feat):-
  setof(F,Type^Subs^R^FRs^((Type subs Subs intro FRs),
                           member(F:R,FRs)), 
        Feats),
  member(Feat,Feats)
 ;setof(F,Type^R^FRs^((Type intro FRs),
                      member(F:R,FRs)),
        Feats),
  member(Feat,Feats).

% ------------------------------------------------------------------------------
% restricts(Type:<type>, Feat:<feat>, TypeRestr:<type>)                     eval
% ------------------------------------------------------------------------------
% Type introduces the feature Feat imposing value restriction TypeRestr 
% ------------------------------------------------------------------------------
restricts(Type,Feat,TypeRestr):-
  Type subs _ intro FRs,
  member(Feat:TypeRestr,FRs)
 ;Type intro FRs,
  member(Feat:TypeRestr,FRs).

% ------------------------------------------------------------------------------
% introduce(Feat:<feat>, Type:<type>, TypeVal:<type>)                       eval
% ------------------------------------------------------------------------------
% Type is the most general type appropriate for Feat
% ------------------------------------------------------------------------------
introduce(Feat,Type):-
  setof(Type,TypeRestr^restricts(Type,Feat,TypeRestr),Types),
  map_minimal(Types,[],TypesMin),
            [feature,Feat,multiply,introduced,at,TypesMin] if_error
                 (\+ TypesMin = [Type]),
  TypesMin = [Type].

% ------------------------------------------------------------------------------
% approp(Feat:<feat>, Type:<type>, TypeRestr:<type>)                       mh(1)
% ------------------------------------------------------------------------------
% approp(Feat,Type) = TypeRestr
% ------------------------------------------------------------------------------
(approp(Feat,Type,ValRestr) if_h) :-
  setof(TypeRestr,TypeSubs^(sub_type(TypeSubs,Type),
                            restricts(TypeSubs,Feat,TypeRestr)),
        TypeRestrs),
               [incompatible,restrictions,on,feature,Feat,at,type,Type,
                are,TypeRestrs] if_error
                    (\+ unify_types(TypeRestrs,ValRestr)),    
  unify_types(TypeRestrs,ValRestr).
approp(_,_,_) if_h [fail] :-
  \+(_ subs _ intro _),
  \+(_ intro _).

% ------------------------------------------------------------------------------
% approps(Type:<type>, FRs:<feat_val>s)                                     eval
% ------------------------------------------------------------------------------
% FRs is list of appropriateness declarations for Type
% ------------------------------------------------------------------------------
approps(Type,FRs):-
  type(Type),  % ALE WON'T CATCH FEATURES DEFINED FOR ATOMS UNTIL COMPILER RUNS
  esetof(Feat:TypeRestr, approp(Feat,Type,TypeRestr), FRs).

% ------------------------------------------------------------------------------
% approp_feats(Type:<type>,Fs:<feat>s)
% ------------------------------------------------------------------------------
% Fs is list of appropriate features for Type
% ------------------------------------------------------------------------------
approp_feats(Type,Fs) :-
  type(Type), % ALE WON'T CATCH FEATURES DEFINED FOR ATOMS UNTIL COMPILER RUNS 
  esetof(Feat,TypeRestr^approp(Feat,Type,TypeRestr),Fs).


% ==============================================================================
% Feature Structure Unification
% ==============================================================================

% ------------------------------------------------------------------------------
% ud(FS1:<fs>, FS2:<fs>, IqsIn:<ineq>s, IqsOut:<ineq>s)                     eval
% ------------------------------------------------------------------------------
% unifies FS1 and FS2 (after dereferencing); 
% ------------------------------------------------------------------------------
ud(FS1,FS2,IqsIn,IqsOut):-
  deref(FS1,Ref1,SVs1), deref(FS2,Ref2,SVs2),
  ( Ref1 == Ref2, IqsOut = IqsIn,
    !
  ; u(SVs1,SVs2,Ref1,Ref2,IqsIn,IqsOut)
  ).

% ------------------------------------------------------------------------------
% deref(FSIn:<fs>, RefOut:<ref>, SVsOut:<svs>)
% ------------------------------------------------------------------------------
% RefOut-SVsOut is result of dereferencing FSIn at top level
% ------------------------------------------------------------------------------
deref(Ref-Vs,RefOut,VsOut):-
  ( var(Ref),
    !, RefOut = Ref, VsOut = Vs
  ; deref(Ref,RefOut,VsOut)
  ).

% ------------------------------------------------------------------------------
% deref_list(RefsIn:<ref>s, RefsOut:<ref>s)
% ------------------------------------------------------------------------------
% applies deref/4 on all elements of RefsIn to get RefsOut
% ------------------------------------------------------------------------------
deref_list([],[]).
deref_list([Ref-Vs|Rest],[RefOut-VsOut|RestOut]) :-
  deref(Ref,Vs,RefOut,VsOut),
  deref_list(Rest,RestOut).

% ------------------------------------------------------------------------------
% deref(RefIn:<ref>,SVsIn:<svs>, RefOut:<ref>, SVsOut:<svs>)
% ------------------------------------------------------------------------------
% RefOut-SVsOut is result of dereferencing FSIn at top level
% ------------------------------------------------------------------------------
deref(Ref,Vs,RefOut,VsOut):-
    var(Ref),
    !, RefOut = Ref, VsOut = Vs
  ; deref(Ref,RefOut,VsOut).

% ------------------------------------------------------------------------------
% fully_deref_prune(RefIn:<ref>,SVsIn:<svs>, RefOut:<ref>, SVsOut:<svs>, 
%                   IqsIn:<ineq>s, IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% In addition to fully dereferencing the given feature structure, this
%  predicate checks the associated inequations both for their satisfaction,
%  and for their relevance, and rebuilds them in terms of the new feature
%  structure.  An inequation is deemed relevant if both of its terms are 
%  substructures of the given feature structure, or if one of its terms is, 
%  and the other one is fully extensional (which means that it and each of its 
%  substructures is of an extensional sort).  Currently, full extensionality is
%  not actually enforced, but rather only a check that the term itself is of an
%  extensional sort is made.
% ------------------------------------------------------------------------------
fully_deref_prune(Tag,SVs,TagOut,SVsOut,IqsIn,IqsOut) :-
  fully_deref(Tag,SVs,TagOut,SVsOut),
  prune(IqsIn,IqsOut). 

%prune(Var,Var) :- var(Var), !.			% !!! CHECK IF NECESSARY
prune([],[]).
prune([ineq(Tag1,SVs1,Tag2,SVs2,Ineqs)|IqsIn],IqsOut) :-
  prune_deref(Tag1,SVs1,Tag1Out,SVs1Out,InFlag1),
  prune_deref(Tag2,SVs2,Tag2Out,SVs2Out,InFlag2),
  (InFlag1 = out,InFlag2 = out,  % both are out
   !, prune(IqsIn,IqsOut)
  ;InFlag1 = out,                % one is out, and it's intensional
   \+(SVs1 = a_ _),         % structure-sharing inside atoms could cause 
   functor(SVs1,Sort1,_),   %  trouble later - so keep them around
   \+extensional(Sort1),
   !,prune(IqsIn,IqsOut)
  ;InFlag2 = out,
   \+(SVs2 = a_ _),
   functor(SVs2,Sort2,_),
   \+extensional(Sort2),
   !,prune(IqsIn,IqsOut)
  ;check_inequal_conjunct(ineq(Tag1Out,SVs1Out,Tag2Out,SVs2Out,Ineqs),
                          IqOut,Result),
   prune_act(Result,IqOut,IqsIn,IqsOut)).

prune_act(done,done,_,_) :-   % conjunct failed
  !,fail.
prune_act(succeed,_,IqsIn,IqsOut) :-  % conjunct succeeded
  !,prune(IqsIn,IqsOut).
prune_act(_,IqOut,IqsIn,[IqOut|IqsOut]) :-  % conjunct temporarily succeeded
  prune(IqsIn,IqsOut).

prune_deref(Tag,SVs,Tag,SVsOut,out) :-
  var(Tag),
  !,
  (SVs = a_ _,
   !,SVsOut = SVs
  ;SVs =.. [Sort|Vs],  % some substructures may still be shared
   prune_deref_feats(Vs,VsOut),
   SVsOut =.. [Sort|VsOut]
  ).
prune_deref(fully(TagOut,SVsOut),_,TagOut,SVsOut,in).
prune_deref(Tag-SVs,_,TagOut,SVsOut,InFlag) :-
  prune_deref(Tag,SVs,TagOut,SVsOut,InFlag).

prune_deref_feats([],[]).
prune_deref_feats([Ref-SVs|Vs],[RefOut-SVsOut|VsOut]) :-
  prune_deref(Ref,SVs,RefOut,SVsOut,_),
  prune_deref_feats(Vs,VsOut).

% ------------------------------------------------------------------------------
% fully_deref(RefIn:<ref>,SVsIn:<svs>, RefOut:<ref>, SVsOut:<svs>)
% ------------------------------------------------------------------------------
% RefOut-SVsOut is result of recursively dereferencing FSIn;
% destroys RefIn-SVsIn by overwriting Tags
% ------------------------------------------------------------------------------
fully_deref(Tag,SVs,TagOut,SVsOut):-
  ( nonvar(Tag),
    !, fully_deref_act(Tag,SVs,TagOut,SVsOut)
  ; Tag = (fully(TagOut,SVsOut)-SVsOut),
    (SVs = a_ X,
     !,SVsOut = a_ X
    ;functor(SVs,Rel,Arity),
     functor(SVsOut,Rel,Arity),
     fully_deref_args(Arity,SVs,SVsOut)
    )
  ).

fully_deref_act(fully(TagOut,_),SVs,TagOut,SVs).
fully_deref_act(TagMid-SVsMid,_,TagOut,SVsOut):-
  fully_deref(TagMid,SVsMid,TagOut,SVsOut).

fully_deref_args(0,_,_):-!.
fully_deref_args(N,SVs,SVsOut):-
  arg(N,SVs,TagN-SVsN),
  fully_deref(TagN,SVsN,TagOutN,SVsOutN),
  arg(N,SVsOut,TagOutN-SVsOutN),
  M is N-1,
  fully_deref_args(M,SVs,SVsOut).

% ------------------------------------------------------------------------------
% u(SVs1:<svs>,SVs2:<svs>,Ref1:<ref>,Ref2:<ref>,IqsIn:<ineq>s,
%   IqsOut:<ineqs>)                                                        mh(2)
% ------------------------------------------------------------------------------
% compiles typed version of the Martelli and Montanari unification
% algorithm for dereferenced feature structures Ref1-SVs1 and Ref2-SVs2 
% ------------------------------------------------------------------------------
u(SVs1,SVs2,Ref1,Ref2,IqsIn,IqsOut) if_h SubGoals:-
  unify_type(Type1,Type2,Type3),
  uact(Type3,SVs1,SVs2,Ref1,Ref2,Type1,Type2,IqsIn,IqsOut,SubGoals).

% ------------------------------------------------------------------------------
% uact(Type3,SVs1,SVs2,Ref1,Ref2,Type1,Type2,IqsIn,IqsOut,SubGoals)
% ------------------------------------------------------------------------------
% SubGoals is list of goals required to unify Ref1-SVs1 and Ref2-SVs2,
% where Ref1-SVs1 is of type Type1, Ref2-SVs2 is of type Type2 and
% Type1 unify Type2 = Type3
% ------------------------------------------------------------------------------
uact(a_ X,a_ X,a_ X,Ref,Ref,a_ X,a_ X,Iqs,Iqs,[]) :- !.
uact(a_ X,bot,a_ X,Ref-(a_ X),Ref,bot,a_ X,Iqs,Iqs,[]) :- !.
uact(a_ X,a_ X,bot,Ref,Ref-(a_ X),a_ X,bot,Iqs,Iqs,[]) :- !.
uact(Type3,SVs1,SVs2,Ref1,Ref2,Type1,Type2,IqsIn,IqsOut,SubGoals):-
  approps(Type1,FRs1),    % we know Type1, Type2, and Type3 aren't a_ atoms
  ( Type1 = Type2, 
    !, Ref1 = Ref2,
    map_feats_eq(FRs1,Vs1,Vs2,IqsIn,IqsOut,SubGoals)
  ; approps(Type2,FRs2),                % Type1 \== Type2,
    ( Type2 = Type3,
      !, Ref1 = Ref2-SVs2,
      map_feats_subs(FRs1,FRs2,Vs1,Vs2,IqsIn,IqsOut,SubGoals)
    ; Type1 = Type3,
      !, Ref2 = Ref1-SVs1,
      map_feats_subs(FRs2,FRs1,Vs2,Vs1,IqsIn,IqsOut,SubGoals)
    ; Ref1 = Tag3-SVs3, Ref2 = Ref1,       % Type1 \== Type3, Type2 \== Type3
      approps(Type3,FRs3),
      map_feats_unif(FRs1,FRs2,FRs3,Vs1,Vs2,Vs3,IqsIn,IqsMid,SubGoals,
                     [ucons(Type3,Type2,Type1,Tag3,SVs3,IqsMid,IqsOut)]),
      SVs3 =.. [Type3|Vs3]
    )
  ),
  SVs1 =.. [Type1|Vs1],
  SVs2 =.. [Type2|Vs2].

% ------------------------------------------------------------------------------
% ucons(Type:<type>,ExclType1:<type>,ExclType2:<type>,Tag:<ref>,SVs:<sv>s,
%       IqsIn:<ineq>s,IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% Enforce the constraint for Type, and for all supersorts of Type, excluding
%  ExclType1 and ExclType2, on Tag-SVs
% ------------------------------------------------------------------------------
ucons(Type,ET1,ET2,Tag,SVs,IqsIn,IqsOut) if_h SubGoals :-
  compile_cons(Tag,SVs,TypeConsPs),

%  asserta(typeconsps(Tag,SVs,TypeConsPs)),  % save it for add_to_typecons
% too big for prolog - so we must recompute it

  !,unify_type(ET1,ET2,Type),
  esetof(T,(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,TypeConsPs,IqsIn,IqsOut,SubGoals).

% ------------------------------------------------------------------------------
% compile_cons(Tag:<ref>,SVs:<sv>s,TypeConsPs:<tcp>s)
% ------------------------------------------------------------------------------
% Compiles the constraints associated with each type (including procedural
%  attachments)
% ------------------------------------------------------------------------------
compile_cons(Tag,SVs,TypeConsPs) :-
  esetof(Type,type(Type),Types),
  compile_cons_types(Types,Tag,SVs,TypeConsPs).

compile_cons_types([],_,_,[]).
compile_cons_types([Type|Types],Tag,SVs,
                   [tcp(Type,Rest,Rest,Iqs,Iqs)|TypeConsPs]) :-
  (\+current_predicate(cons,(_ cons _))  % check if there are any cons's
  ; \+(Type cons _)),                    % check if Type has a cons specified
  !,compile_cons_types(Types,Tag,SVs,TypeConsPs).
compile_cons_types([Type|Types],Tag,SVs,
                   [tcp(Type,NewGoals,Rest,IqsIn,IqsOut)|TypeConsPs]) :-
  Type cons Cons goal Goal,
  !,compile_desc(Cons,Tag-SVs,IqsIn,IqsMid,NewGoals,GoalsRest),
  compile_body(Goal,[],[],IqsMid,IqsOut,GoalsRest,Rest),
  compile_cons_types(Types,Tag,SVs,TypeConsPs).
compile_cons_types([Type|Types],Tag,SVs,
                   [tcp(Type,Goals,Rest,IqsIn,IqsOut)|TypeConsPs]) :-
  Type cons Cons,
  compile_desc(Cons,Tag-SVs,IqsIn,IqsOut,Goals,Rest),
  compile_cons_types(Types,Tag,SVs,TypeConsPs).

% ------------------------------------------------------------------------------
% map_cons(Types:<type>s,TypeConsPs:<tcp>s,IqsIn:<ineq>s,IqsOut:<ineq>s,
%          SubGoals:<goal>s)
% ------------------------------------------------------------------------------
% Given a set of types, strings together the goals and inequations for them.
% ------------------------------------------------------------------------------
map_cons([],_,Iqs,Iqs,[]).
map_cons([Type|Types],TypeConsPs,IqsIn,IqsOut,SubGoals) :-
  select(tcp(Type,SubGoals,GoalsRest,IqsIn,IqsMid),TypeConsPs,TypeConsRest),
  map_cons(Types,TypeConsRest,IqsMid,IqsOut,GoalsRest).

%ucons(Type,ET1,ET2,Tag,SVs,IqsIn,IqsOut) :-
%  make_topology(Top),

%make_topology(Top) :-
%  top_sort(bot,[],_,TopTypes,[]),
%  make_sets(TopTypes,TopSets),

% ------------------------------------------------------------------------------
% top_sort(Type:<type>,VisIn:<type>s,VisOut:<type>s,TopIn:<type>s,
%          TopOut:<type>s)
% ------------------------------------------------------------------------------
%  Topologically sorts the types in the principal filter rooted at
%   Type.  The order used is such that Type will be the first element on the
%   list TopOut.
% ------------------------------------------------------------------------------
top_sort(Type,VisIn,VisOut,TopIn,[Type|TopMid]) :-
  \+member(Type,VisIn),
  !,Type sub SubTypes,
  top_sort_list(SubTypes,[Type|VisIn],VisOut,TopIn,TopMid).
top_sort(_,Vis,Vis,Top,Top).

top_sort_list([],Vis,Vis,Top,Top).
top_sort_list([Type|Types],VisIn,VisOut,TopIn,TopOut) :-
  top_sort(Type,VisIn,VisMid,TopIn,TopMid),
  top_sort_list(Types,VisMid,VisOut,TopMid,TopOut).

% ------------------------------------------------------------------------------
% make_sets(TopTypes:<type>s,TopSets:<top>s)
% ------------------------------------------------------------------------------
%  TopTypes is in topological order.  TopSets is a list of top(Type,Set)'s for
%   each type in TopTypes, where Set is the set of types which subsume Type, 
%   each only occuring once.

% ------------------------------------------------------------------------------
% map_feats_eq(FRs:<feat>s,Vs1:<fs>s,Vs2:<fs>s,IqsIn:<ineq>s,IqsOut:<ineq>s,
%              Goals:<goal>s)
% ------------------------------------------------------------------------------
% Vs1 and Vs2 set to same length as FRs and a subgoal added to Goals
% to unify value of each feature;
% ------------------------------------------------------------------------------
map_feats_eq([],[],[],Iqs,Iqs,[]).
map_feats_eq([_|FRs],[V1|Vs1],[V2|Vs2],IqsIn,IqsOut,
             [ud(V1,V2,IqsIn,IqsMid)|SubGoals]):-
  map_feats_eq(FRs,Vs1,Vs2,IqsMid,IqsOut,SubGoals).
  
% ------------------------------------------------------------------------------
% map_feats_subs(FRs1:<feat>s, FRs2:<feat>s, Vs1:<fs>s, Vs2:<fs>s, 
%                IqsIn:<ineq>s, IqsOut:<ineq>s, Goals:<goal>s) 
% ------------------------------------------------------------------------------
% Vs1 and Vs2 set to same length as FRs1 and FRs2 and a subgoal 
% added to Goals for each shared feature;  
% ------------------------------------------------------------------------------
map_feats_subs([],FRs,[],Vs,Iqs,Iqs,[]):-
  same_length(FRs,Vs).
map_feats_subs([F:_|FRs1],FRs2,[V1|Vs1],Vs2,IqsIn,IqsOut,
                [ud(V1,V2,IqsIn,IqsMid)|SubGoals]):-
  map_feats_find(F,FRs2,V2,Vs2,FRs2Out,Vs2Out),
  map_feats_subs(FRs1,FRs2Out,Vs1,Vs2Out,IqsMid,IqsOut,SubGoals).

% ------------------------------------------------------------------------------
% map_feats_find(F:<feat>, FRs:<feat>s, V:<fs>, Vs:<fs>s, 
%                FRsOut:<feat>s, VsOut:<fs>s)
% ------------------------------------------------------------------------------
% if F is the Nth element of FRs then V is the Nth element of Vs;
% FRsOut and VsOut are the rest (after the Nth) of FRs and Vs
% ------------------------------------------------------------------------------
map_feats_find(F,[F:_|FRs],V,[V|Vs],FRs,Vs):-!.
map_feats_find(F,[_|FRs],V,[_|Vs],FRsOut,VsOut):-
  map_feats_find(F,FRs,V,Vs,FRsOut,VsOut).

% ------------------------------------------------------------------------------
% map_feats_unif(FRs1:<feat>s,FRs2:<feat>s,FRs3:<feat>s,Vs1:<fs>s,Vs2:<fs>s,
%                 Vs3:<fs>s,IqsIn:<ineq>s,IqsOut:<ineq>s,Goals:<goal>s,
%                 GoalsRest:<goal>s)
% ------------------------------------------------------------------------------
% Vs1, Vs2 and Vs3 set to same length as Feats1, FRs2 and FRs3;
% a subgoal's added to Goals for each feature shared in FRs1 and FRs2;  
% feats shared in Vs1,Vs2 and Vs3 passed; new Vs3 entries are created
% ------------------------------------------------------------------------------
map_feats_unif([],FRs2,FRs3,[],Vs2,Vs3,IqsIn,IqsOut,Goals,GoalsRest):-
  map_new_feats(FRs2,FRs3,Vs2,Vs3,IqsIn,IqsOut,Goals,GoalsRest).
map_feats_unif([F1:R1|FRs1],FRs2,FRs3,Vs1,Vs2,Vs3,IqsIn,IqsOut,Goals,
               GoalsRest):-
  map_feats_unif_ne(FRs2,F1,R1,FRs1,FRs3,Vs1,Vs2,Vs3,IqsIn,IqsOut,Goals,
                    GoalsRest).

map_feats_unif_ne([],F1,R1,FRs1,FRs3,Vs1,[],Vs3,IqsIn,IqsOut,Goals,GoalsRest):-
  map_new_feats([F1:R1|FRs1],FRs3,Vs1,Vs3,IqsIn,IqsOut,Goals,GoalsRest).
map_feats_unif_ne([F2:R2|FRs2],F1,R1,FRs1,FRs3,Vs1,Vs2,Vs3,
                  IqsIn,IqsOut,Goals,GoalsRest):-
  compare(Comp,F1,F2),
  map_feats_unif_act(Comp,F1,F2,R1,R2,FRs1,FRs2,FRs3,Vs1,Vs2,Vs3,
                     IqsIn,IqsOut,Goals,GoalsRest).

map_feats_unif_act(=,F1,_F2,R1,R2,FRs1,FRs2,FRs3,[V1|Vs1],[V2|Vs2],Vs3,
                   IqsIn,IqsOut,[ud(V1,V2,IqsIn,IqsMid)|Goals1],GoalsRest):-
  unify_type(R1,R2,R1UnifyR2),
  map_new_feats_find(F1,R1UnifyR2,FRs3,V1,Vs3,FRs3Out,Vs3Out,IqsMid,IqsMid2,
                     Goals1,Goals2),
  map_feats_unif(FRs1,FRs2,FRs3Out,Vs1,Vs2,Vs3Out,IqsMid2,IqsOut,Goals2,
                 GoalsRest).
map_feats_unif_act(<,F1,F2,R1,R2,FRs1,FRs2,FRs3,[V1|Vs1],Vs2,Vs3,
                   IqsIn,IqsOut,Goals,GoalsRest2):-
  map_new_feats_find(F1,R1,FRs3,V1,Vs3,FRs3Out,Vs3Out,IqsIn,IqsMid,
                     Goals,GoalsRest1),
  map_feats_unif_ne(FRs1,F2,R2,FRs2,FRs3Out,Vs2,Vs1,Vs3Out,
                    IqsMid,IqsOut,GoalsRest1,GoalsRest2).
map_feats_unif_act(>,F1,F2,R1,R2,FRs1,FRs2,FRs3,Vs1,[V2|Vs2],Vs3,
                   IqsIn,IqsOut,Goals,GoalsRest2):-
  map_new_feats_find(F2,R2,FRs3,V2,Vs3,FRs3Out,Vs3Out,IqsIn,IqsMid,
                     Goals,GoalsRest1),
  map_feats_unif_ne(FRs2,F1,R1,FRs1,FRs3Out,Vs1,Vs2,Vs3Out,
                    IqsMid,IqsOut,GoalsRest1,GoalsRest2).

% ------------------------------------------------------------------------------
% map_new_feats(FRs:<feat>s, FRsNew:<feat>s, Vs:<fs>s, VsNew:<fs>s, 
%               IqsIn:<ineq>s,IqsOut:<ineq>s,Gs:<goal>s,GsRest:<goal>s)
% ------------------------------------------------------------------------------
% FRs and FRsNew must be instantiated in alpha order where
% FRs is a sublist of NewFs;
% create Vs and VsNew where Vs and VsNew share a value if the
% feature in Fs and NewFs matches up, otherwise VsNew gets a fresh
% minimum feature structure (_-bot) for a value;
% all necessary value coercion is also performed
% ------------------------------------------------------------------------------
map_new_feats([],FRsNew,[],VsNew,IqsIn,IqsOut,SubGoals,SubGoalsRest):-
  map_new_feats_introduced(FRsNew,VsNew,IqsIn,IqsOut,SubGoals,SubGoalsRest).
map_new_feats([Feat:TypeRestr|FRs],FRsNew,[V|Vs],VsNew,IqsIn,IqsOut,SubGoals,
              SubGoalsRest2):-
  map_new_feats_find(Feat,TypeRestr,FRsNew,V,VsNew,
                     FRsNewLeft,VsNewLeft,IqsIn,IqsMid,SubGoals,SubGoalsRest1),
 map_new_feats(FRs,FRsNewLeft,Vs,VsNewLeft,IqsMid,IqsOut,SubGoalsRest1,
               SubGoalsRest2).

% ------------------------------------------------------------------------------
% map_new_feats_find(Feat,TypeRestr,FRs,V,Vs,FRs2,Vs2,IqsIn,IqsOut,
%                    SubGoals,SubGoalsRest)
% ------------------------------------------------------------------------------
% finds Feat value V in Vs, parallel to FRs, with restriction TypeRestr on V, 
% with FRs2 being left over;  carries out coercion on new feature values
% with SubGoals-SubGoalsRest being the code to do this
% ------------------------------------------------------------------------------
map_new_feats_find(Feat,TypeRestr,[Feat:TypeRestrNew|FRs],
                    V,[V|Vs],FRs,Vs,IqsIn,IqsOut,SubGoals,SubGoalsRest):-
  !,
  ( sub_type(TypeRestrNew,TypeRestr),
    !, SubGoals = SubGoalsRest,
    IqsOut = IqsIn
  ; TypeRestrNew = a_ X,
    !,Goal =.. ['add_to_type_a_',V,IqsIn,IqsOut,X],
    SubGoals = [Goal|SubGoalsRest]
  ; cat_atoms(add_to_type_,TypeRestrNew,Rel),
    Goal =.. [Rel,V,IqsIn,IqsOut],
    SubGoals = [Goal|SubGoalsRest]
  ).
map_new_feats_find(Feat,TypeRestr,[_:TypeRestrNew|FRs],
                   V,[(Tag-bot)|Vs],FRsNew,VsNew,IqsIn,IqsOut,
                   [Goal|SubGoalsMid],
                   SubGoalsRest):-
 (TypeRestrNew = a_ X,
  !,Goal =.. ['add_to_type_a_',bot,Tag,IqsIn,IqsMid,X]
 ;
  cat_atoms(add_to_type_,TypeRestrNew,Rel),
  Goal =.. [Rel,bot,Tag,IqsIn,IqsMid]),
  map_new_feats_find(Feat,TypeRestr,FRs,V,Vs,FRsNew,
                     VsNew,IqsMid,IqsOut,SubGoalsMid,SubGoalsRest).

% ------------------------------------------------------------------------------
% map_new_feats_introduced(FRs,Vs,IqsIn,IqsOut,SubGoals,SubGoalsRest)
% ------------------------------------------------------------------------------
% instantiates Vs to act as values of features in FRs;  SubGoals contains
% type coercions necessary so that Vs satisfy constraints in FRs
% ------------------------------------------------------------------------------
map_new_feats_introduced([],[],Iqs,Iqs,Rest,Rest).
map_new_feats_introduced([_:TypeRestr|FRs],[(Ref-bot)|Vs],IqsIn,IqsOut,
                         SubGoals,SubGoalsRest2):-
  SubGoals = [Goal|SubGoalsRest1],
 (TypeRestr = a_ X,
  !,Goal =.. ['add_to_type_a_',bot,Ref,IqsIn,IqsMid,X]
 ;cat_atoms(add_to_type_,TypeRestr,Rel),
  Goal =.. [Rel,bot,Ref,IqsIn,IqsMid]),
  map_new_feats_introduced(FRs,Vs,IqsMid,IqsOut,SubGoalsRest1,SubGoalsRest2).


% ==============================================================================
% Lexical Rules
% ==============================================================================

% ------------------------------------------------------------------------------
% lex_rule(WordIn,TagIn,SVsIn,WordOut,TagOut,SVsOut,IqsIn,IqsOut)          mh(0)
% ------------------------------------------------------------------------------
% WordOut with category TagOut-SVsOut can be produced from
% WordIn with category TagIn-SVsIn by the application of a single
% lexical rule;  TagOut-SVsOut is fully dereferenced on output;
% Words are converted to character lists and back again
% ------------------------------------------------------------------------------
lex_rule(WordIn,TagIn,SVsIn,WordOut,TagOut,SVsOut,IqsIn,IqsOut) 
                                                   if_h SubGoalsFinal:-
  ( (_LexRuleName lex_rule DescIn **> DescOut morphs Morphs),
    Cond = true
  ; (_LexRuleName lex_rule DescIn **> DescOut if Cond morphs Morphs)
  ),
  compile_desc(DescIn,TagIn-SVsIn,IqsIn,IqsMid,SubGoalsFinal,SubGoalsRest1),
  compile_body(Cond,[],[],IqsMid,IqsMid2,SubGoalsRest1,SubGoalsMid),
  compile_desc(DescOut,TagMid-bot,IqsMid2,IqsMid3,SubGoalsMid,
               [morph(Morphs,WordIn,WordOut),
                fully_deref_prune(TagMid,bot,TagOut,SVsOut,IqsMid3,IqsOut)]).

% ------------------------------------------------------------------------------
% morph(Morphs,WordIn,WordOut)
% ------------------------------------------------------------------------------
% converst WordIn to list of chars, performs morph_chars using Morphs
% and then converts resulting characters to WordOut
% ------------------------------------------------------------------------------
morph(Morphs,WordIn,WordOut):-
  name(WordIn,CodesIn),
  make_char_list(CodesIn,CharsIn), 
  morph_chars(Morphs,CharsIn,CharsOut),
  make_char_list(CodesOut,CharsOut),
  name(WordOut,CodesOut).

% ------------------------------------------------------------------------------
% morph_chars(Morphs:<seq(<morph>)>, 
%             CharsIn:<list(<char>)>, CharsOut:<list(<char>)>)
% ------------------------------------------------------------------------------
% applies first pattern rewriting in Morphs that matches input CharsIn
% to produce output CharsOut;  CharsIn should be instantiated and
% CharsOut should be uninstantiated for sound result
% ------------------------------------------------------------------------------
morph_chars((Morph,Morphs),CharsIn,CharsOut):-
    morph_template(Morph,CharsIn,CharsOut), 
    !
  ; morph_chars(Morphs,CharsIn,CharsOut).
morph_chars(Morph,CharsIn,CharsOut):-
  morph_template(Morph,CharsIn,CharsOut).

% ------------------------------------------------------------------------------
% morph_template(Morph:<morph>, CharsIn:<chars>, CharsOut:<chars>)
% ------------------------------------------------------------------------------
% applies tempalte Morph to CharsIn to produce Chars Out;  first
% breaks Morph into an input and output pattern and optional condition
% ------------------------------------------------------------------------------
morph_template((PattIn becomes PattOut),CharsIn,CharsOut):-
  morph_pattern(PattIn,CharsIn),
  morph_pattern(PattOut,CharsOut).
morph_template((PattIn becomes PattOut when Cond),CharsIn,CharsOut):-
  morph_pattern(PattIn,CharsIn),
  call(Cond),
  morph_pattern(PattOut,CharsOut).

% ------------------------------------------------------------------------------
% morph_pattern(Patt:<pattern>,Chars:<list(<char>)>)
% ------------------------------------------------------------------------------
% apply pattern Patt, which is sequence of atomic patterns,
% to list of characters Chars, using conc/3 to deconstruct Chars
% ------------------------------------------------------------------------------
morph_pattern(Var,CharsIn):-
  var(Var),  
  !, Var = CharsIn.
morph_pattern((AtPatt,Patt),CharsIn):-
  !, make_patt_list(AtPatt,List),
  conc(List,CharsMid,CharsIn),
  morph_pattern(Patt,CharsMid).
morph_pattern(AtPatt,CharsIn):-
  make_patt_list(AtPatt,CharsIn).

% ------------------------------------------------------------------------------
% make_patt_list(AtPatt:<atomic_pattern>,List:<list(<char>)>)
% ------------------------------------------------------------------------------
% turns an atomic pattern AtPatt, either a variable, list of characters
% or atom into a list of characters (or possibly a variable);  List
% should not be instantiated
% ------------------------------------------------------------------------------
make_patt_list(Var,Var):-
  var(Var),
  !.
make_patt_list([H|T],[H|TOut]):-
  !, make_patt_list(T,TOut).
make_patt_list([],[]):-
  !.
make_patt_list(Atom,CharList):-
  atom(Atom),
  name(Atom,Name),
  make_char_list(Name,CharList).

% ------------------------------------------------------------------------------
% make_char_list(CharNames:<list(<ascii>)>, CharList:<list(<char>)>)
% ------------------------------------------------------------------------------
% turns list of character ASCII codes and returns list of corresponding
% characters
% ------------------------------------------------------------------------------
make_char_list([],[]).
make_char_list([CharName|Name],[Char|CharList]):-
  name(Char,[CharName]),
  make_char_list(Name,CharList).


% ==============================================================================
% Rounds-Kasper Logic
% ==============================================================================

% ------------------------------------------------------------------------------
% add_to(Phi:<desc>, Tag:<tag>, SVs:<svs>, IqsIn:<ineq>s, IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% Info in Phi is added to FSIn (FSIn already derefenced);
% ------------------------------------------------------------------------------
add_to(Ref1-bot,Ref2,SVs2,IqsIn,IqsOut):-
  !,    % also instantiates variable first arguments
  ( deref(Ref1,bot,Ref3,SVs3),
    u(SVs2,SVs3,Ref2,Ref3,IqsIn,IqsOut)
  ; suppress_adderrs,!,fail
  ; \+   ( deref(Ref1,bot,Ref3,SVs3),
           u(SVs2,SVs3,Ref2,Ref3,IqsIn,IqsOut) ),
    error_msg((nl, write('add_to could not unify '),
             \+ \+ (duplicates_list([Ref1-bot,Ref2-SVs2],IqsIn,[],_,[],_,0,_),
                    nl,tab(5),pp_fs(Ref1-bot,[],VisMid,5), nl, 
                    write('and '), pp_fs(Ref2-SVs2,VisMid,VisOut,5),
                    pp_iqs(IqsIn,VisOut,_,5)),
             ttynl))
  ).
add_to([],Ref,SVs,IqsIn,IqsOut):-
  !, add_to(e_list,Ref,SVs,IqsIn,IqsOut).
add_to([H|T],Ref,SVs,IqsIn,IqsOut):-
  !, add_to((hd:H,tl:T),Ref,SVs,IqsIn,IqsOut).
add_to(Path1 == Path2,Tag,SVs,IqsIn,IqsOut):-
  !, pathval(Path1,Tag,SVs,TagAtPath1,SVsAtPath1,IqsIn,IqsMid),
  deref(Tag,SVs,TagMid,SVsMid),
  pathval(Path2,TagMid,SVsMid,TagAtPath2,SVsAtPath2,IqsMid,IqsMid2),
  ( u(SVsAtPath1,SVsAtPath2,TagAtPath1,TagAtPath2,IqsMid2,IqsOut)
  ; suppress_adderrs,!,fail
  ; \+ u(SVsAtPath1,SVsAtPath2,TagAtPath1,TagAtPath2,IqsMid2,IqsOut),
    error_msg((nl, write('add_to could not unify paths '), 
              write(Path1), write(' and '), 
              write(Path2), write(' in '),
              nl, pp_fs(Tag-SVs,IqsIn,5),
              ttynl))
  ).
add_to(=\= Desc,Tag,SVs,IqsIn,IqsOut):-
  !, add_to(Desc,Tag2,bot,IqsIn,IqsMid),
  ( check_inequal_conjunct(
          ineq(Tag,SVs,Tag2,bot,done),IqOut,Result),
    ( (Result = succeed) ->
      IqsOut = IqsMid
    ; IqOut \== done,
      IqsOut = [IqOut|IqsMid]),
  !
  ; suppress_adderrs,!,fail
  ; error_msg((nl, write('add_to could not inequate '),
              nl, pp_fs(Tag2-bot,[],5),
              nl, write('and '),
              nl, pp_fs(Tag-SVs,IqsIn,5),
              ttynl))
  ).
add_to(Feat:Desc,Ref,SVs,IqsIn,IqsOut):-
  !, 
  ( featval(Feat,SVs,Ref,FSatFeat,IqsIn,IqsMid), 
    deref(FSatFeat,RefatFeat,SVsatFeat),
    add_to(Desc,RefatFeat,SVsatFeat,IqsMid,IqsOut)
  ; suppress_adderrs,!,fail
  ; \+ featval(Feat,SVs,Ref,FSatFeat,IqsIn,IqsMid), 
    error_msg((nl, write('add_to could not add feature '), write(Feat), 
              write(' to '), pp_fs(Ref-SVs,IqsIn,5),
              ttynl))
  ).
add_to((Desc1,Desc2),Ref,SVs,IqsIn,IqsOut):-
  !, add_to(Desc1,Ref,SVs,IqsIn,IqsMid),
  deref(Ref,SVs,Ref2,SVs2), 
  add_to(Desc2,Ref2,SVs2,IqsMid,IqsOut).
add_to((Desc1;Desc2),Ref,SVs,IqsIn,IqsOut):-
  !, 
  ( add_to(Desc1,Ref,SVs,IqsIn,IqsOut)
  ; add_to(Desc2,Ref,SVs,IqsIn,IqsOut)
  ).
add_to(@ MacroName,Ref,SVs,IqsIn,IqsOut):-
  !, 
  ( (MacroName macro Desc),
    !, add_to(Desc,Ref,SVs,IqsIn,IqsOut)
  ; error_msg((nl, write('add_to could not add undefined macro '),
              write(MacroName),
              write(' to '), pp_fs(Ref-SVs,IqsIn,5),
              ttynl))
  ).
add_to(Type,Ref,SVs,IqsIn,IqsOut):-
  type(Type),
  !,
  (\+add_to_type(Type,SVs,Ref,IqsIn,_),
   (suppress_adderrs,!,fail
   ; error_msg((nl, write('add_to could not add incompatible type '), 
               write(Type),
               nl, write('to '), pp_fs(Ref-SVs,IqsIn,5),
               ttynl)))
  ; add_to_type(Type,SVs,Ref,IqsIn,IqsOut)
  ).
add_to(FunDesc,Ref,SVs,IqsIn,IqsOut) :-   % complex function constraints
  fun(FunDesc),
  mg_sat_goal(FunDesc,Fun,IqsIn,IqsMid), % can use for fun. desc.'s too
  !,fsolve(Fun,Ref-SVs,IqsMid,IqsOut).
add_to(Atom,Ref,SVs,Iqs,Iqs) :-
  atomic(Atom),
  !, 
  error_msg((nl, write('add_to could not add undefined type '), write(Atom),
             nl, write('to '), pp_fs(Ref-SVs,Iqs,5),
             ttynl)).
add_to(Desc,Ref,SVs,Iqs,Iqs):-
  error_msg((nl,write('add_to could not add ill formed complex description '), 
            nl, tab(5), write(Desc),
            nl, write('to '),
            pp_fs(Ref-SVs,Iqs,5),
            ttynl)).

% add_to_list(Descs:<desc>s,FSs:<fs>s,IqsIn:<ineq>s,IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
%  add each description in Descs to the respective FS in FSs
% ------------------------------------------------------------------------------
add_to_list([],[],Iqs,Iqs).
add_to_list([Desc|Descs],[FS|FSs],IqsIn,IqsOut) :-
  deref(FS,Tag,SVs),
  add_to(Desc,Tag,SVs,IqsIn,IqsMid),
  add_to_list(Descs,FSs,IqsMid,IqsOut).

% add_to_fresh(Descs:<desc>s,FSs:<fs>s,IqsIn:<ineq>s,IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
%  same as add_to_list, but instantiates the FS's first to bottom
% ------------------------------------------------------------------------------
add_to_fresh([],[],Iqs,Iqs).
add_to_fresh([Desc|Descs],[Ref-bot|FSs],IqsIn,IqsOut) :-
  add_to(Desc,Ref,bot,IqsIn,IqsMid),
  add_to_fresh(Descs,FSs,IqsMid,IqsOut).

% ------------------------------------------------------------------------------
% pathval(P:<path>,TagIn:<tag>,SVsIn:<svs>,TagOut:<tag:,SVsOut:<svs>,
%         IqsIn:<ineq>s,IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% TagOut-SVsOut is the undereferenced value of dereferenced TagIn-SVsIn
% at path P
% ------------------------------------------------------------------------------
pathval([],Tag,SVs,Tag,SVs,Iqs,Iqs).
pathval([Feat|Path],Tag,SVs,TagOut,SVsOut,IqsIn,IqsOut):-
  ( featval(Feat,SVs,Tag,FSMid,IqsIn,IqsMid),
    deref(FSMid,TagMid,SVsMid),
    pathval(Path,TagMid,SVsMid,TagOut,SVsOut,IqsMid,IqsOut)
  ; suppress_adderrs,!,fail
  ; \+ featval(Feat,SVs,Tag,FSMid,IqsIn,IqsMid),
    write('feature '), write(Feat), write(' in path '), write([Feat|Path]),
    write('could not be added to '), pp_fs(Tag-SVs,[],5),
    fail
  ).

% ------------------------------------------------------------------------------
% add_to_type(Type:<type>,SVs:<svs>,Ref:<ref>,IqsIn:<ineq>s,
%             IqsOut:<ineq>s)                                              mh(2)
% ------------------------------------------------------------------------------
% adds Type to Ref-SVs -- arranged so that it can be compiled
% ------------------------------------------------------------------------------
add_to_type(Type1,SVs2,Ref,IqsIn,IqsOut) if_h SubGoals :-
  unify_type(Type1,Type2,Type3),
  add_to_typeact(Type3,Type1,Type2,SVs2,Ref,IqsIn,IqsOut,SubGoals).

% ------------------------------------------------------------------------------
% add_to_typeact(Type3,Type1,Type2,SVs,Ref,IqsIn,IqsOut,SubGoals)
% ------------------------------------------------------------------------------
% SubGoals is code to add type Type1 to Ref-SVs of type Type2, with
% result being of Type3
% ------------------------------------------------------------------------------
add_to_typeact(a_ X,a_ X,a_ X,a_ X,_,Iqs,Iqs,[]) :- !.
add_to_typeact(a_ X,bot,a_ X,a_ X,_,Iqs,Iqs,[]) :- !.
add_to_typeact(a_ X,a_ X,bot,bot,_-(a_ X),Iqs,Iqs,[]) :- !.
add_to_typeact(Type3,Type1,Type2,SVs2,Ref,IqsIn,IqsOut,SubGoals):-
  approps(Type2,FRs2),
  ( sub_type(Type1,Type2),
    !, same_length(FRs2,Vs2),
    SubGoals = [],
    IqsOut = IqsIn
  ; % \+ sub_type(Type1,Type2),
    approps(Type3,FRs3), 
    map_new_feats(FRs2,FRs3,Vs2,Vs3,IqsIn,IqsMid,SubGoals,
                  [add_to_typecons(Type3,Type2,Tag3,SVs3,IqsMid,IqsOut)]),
    ( Vs3 = [],
      !, 
      SVs3 = Type3
    ; % Vs3 \== [],
      SVs4 =.. [Type3|Vs3],
      SVs3 = SVs4
    ),
    Ref = (Tag3-SVs3)
  ),
  SVs2 =.. [Type2|Vs2].

% ------------------------------------------------------------------------------
% add_to_typecons(Type:<type>,ExclType:<type>,Tag:<ref>,SVs:<sv>s,
%                 IqsIn:<ineq>s,IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% Enforce the constraint for Type, and for all supersorts of Type, excluding
%  ExclType, on Tag-SVs
% ------------------------------------------------------------------------------

add_to_typecons(Type,ET,Tag,SVs,IqsIn,IqsOut) if_h SubGoals :-
%  retract(typeconsps(Tag,SVs,TypeConsPs)),  % recall from ucons
% too big for prolog - so recompute instead:
  compile_cons(Tag,SVs,TypeConsPs),
  esetof(at(T2,T3),T1^unify_type(T1,T2,T3),AddTypes),
  !,member(at(ET,Type),AddTypes),
  esetof(T,(sub_type(T,Type),             % find set of types whose constraints
            \+sub_type(T,ET)),ConsTypes), %  must be satisfied
  map_cons(ConsTypes,TypeConsPs,IqsIn,IqsOut,SubGoals).
% this map_cons is the same as the one for ucons

% ------------------------------------------------------------------------------
% featval(F:<feat>,SVs:<SVs>,Ref:<ref>,V:<fs>,
%         IqsIn:<ineq>s,IqsOut:<ineq>s)                                    mh(1)
% ------------------------------------------------------------------------------
% Ref-SVs value for feature F is V -- may involve coercion; 
% Ref-SVs is fully dereferenced;  V may not be
% ------------------------------------------------------------------------------
featval(F,SVs,Tag,V,IqsIn,IqsOut) if_h SubGoals:-
  introduce(F,TypeIntro),
  add_to_type(TypeIntro,SVs,Tag,IqsIn,IqsOut) if_h SubGoals,
  deref(Tag,SVs,_NewTag,NewSVs),
  NewSVs =.. [Sort|Vs],   % don't have to worry about atoms as long as
  approps(Sort,FRs),      %  TypeIntro can't be bot (i.e. bot has no features)
  find_featval(F,FRs,Vs,V).

% ------------------------------------------------------------------------------
% find_featval(Feat,FRs,Vs,V)
% ------------------------------------------------------------------------------
% V is element of Vs same distance from front as F:_ is from front of FRs
% ------------------------------------------------------------------------------
find_featval(F,[F:_TypeRestr|_],[V|_Vs],V):-!.
find_featval(F,[_|FRs],[_|Vs],V):-
  find_featval(F,FRs,Vs,V).

% ------------------------------------------------------------------------------
% iso(FS1:<fs>, FS2:<fs>)
% ------------------------------------------------------------------------------
% determines whether structures FS1 and FS2 are isomorphic;
% not currently used, but perhaps necessary for inequations
% ------------------------------------------------------------------------------
iso(FS1,FS2):-
  iso_seq(iso(FS1,FS2,done)).

% ------------------------------------------------------------------------------
% iso_seq(FSSeq:<fs_seq>)
% ------------------------------------------------------------------------------
% takes structure <fs_seq> consisting of done/0 or iso(FS1,FS2,Isos)
% representing list of isomorphisms.  makes sure that all are isomorphic
% ------------------------------------------------------------------------------
iso_seq(done).
iso_seq(iso(FS1,FS2,Isos)):-
  deref(FS1,Tag1,SVs1),
  deref(FS2,Tag2,SVs2),
  ( Tag1 == Tag2,
    !, iso_seq(Isos)
  ; Tag1 = Tag2,
    iso_sub_seq(SVs1,SVs2,Isos)
  ).

iso_sub_seq(a_ X,a_ Y,Isos) if_h [X==Y,iso_seq(Isos)].  % ext. like Prolog
iso_sub_seq(SVs1,SVs2,Isos) if_h SubGoal :-
  extensional(Sort),
  \+ (Sort = a_ _),
  approps(Sort,FRs),
  length(FRs,N),
  functor(SVs1,Sort,N),
  functor(SVs2,Sort,N),
  new_isos(N,SVs1,SVs2,Isos,SubGoal).

new_isos(0,_,_,SubGoal,[iso_seq(SubGoal)]) :-
  !.
new_isos(N,SVs1,SVs2,Isos,SubGoal) :-
  arg(N,SVs1,V1),
  arg(N,SVs2,V2),
  M is N-1,
  new_isos(M,SVs1,SVs2,iso(V1,V2,Isos),SubGoal).

% ------------------------------------------------------------------------------
% extensionalise(Ref:<ref>, SVs:<svs>, Iqs:<iqs>)
%-------------------------------------------------------------------------------
% search for extensional types which should be unified in Tag-SVs, and its
%  inequations, and do it.  Extensional types are assumed to be maximal.
%-------------------------------------------------------------------------------
extensionalise(Ref,SVs,Iqs) :-
  ext_act([Ref-SVs],_,done,Iqs).

extensionalise(FS,Iqs) :-
  ext_act([FS],_,done,Iqs).

ext_act([Ref-SVs|FSs],ExtQ,Ineqs,Iqs) :-
  traverseQ(ExtQ,ExtQ,Ref,SVs,FSs,Ineqs,Iqs).
ext_act([],ExtQ,Ineqs,Iqs) :-
  ext_ineq(Ineqs,ExtQ,Iqs).

ext_ineq(ineq(Ref1,SVs1,Ref2,SVs2,Ineqs),ExtQ,Iqs) :-
  ext_act([Ref1-SVs1,Ref2-SVs2],ExtQ,Ineqs,Iqs).
ext_ineq(done,ExtQ,Iqs) :-
  ext_iqs(Iqs,ExtQ).

ext_iqs([Iq|Iqs],ExtQ) :-
  ext_ineq(Iq,ExtQ,Iqs).
ext_iqs([],_).

extensionalise_list(FSs,Iqs) :-
  ext_act(FSs,_,done,Iqs).

% ------------------------------------------------------------------------------
% traverseQ(ExtQRest:<ext>s,ExtQ:<ext>s,Ref:<ref>,SVs:<svs>,FSs:<fs>s,
%           Ineqs:<ineq>s,Iqs:<iq>s)
% ------------------------------------------------------------------------------
% Add Ref-SVs to the extensionality queue, ExtQ.  Only ExtQRest remains to
% traverse (ExtQ is the head).  If the difference is unbound, then add Ref-SVs
% to the end.  If the first element on the difference is the same FS as
% Ref-SVs, then no need to add.  If the first element can be extensionally
% identified with Ref-SVs, then stop looking, since now Ref-SVs is the same as
% that FS.  If none of these, then go on to the next element.
% ------------------------------------------------------------------------------
traverseQ(Rest,ExtQ,Ref,SVs,FSs,Ineqs,Iqs) :-
  var(Rest),
  !,Rest = ext(Ref,SVs,_),
 (SVs = a_ _,
  !,ext_act(FSs,ExtQ,Ineqs,Iqs)
 ;SVs =.. [_|Vs],
  conc(Vs,FSs,NewFSs),
  ext_act(NewFSs,ExtQ,Ineqs,Iqs)
 ).
traverseQ(ext(ERef,_,_),ExtQ,Ref,_,FSs,Ineqs,Iqs) :-
  ERef == Ref,
  !,ext_act(FSs,ExtQ,Ineqs,Iqs).
traverseQ(ext(ERef,ESVs,_),ExtQ,Ref,SVs,FSs,Ineqs,Iqs) :-
  iso(Ref-SVs,ERef-ESVs),
  !,ext_act(FSs,ExtQ,Ineqs,Iqs).
traverseQ(ext(_,_,ERest),ExtQ,Ref,SVs,FSs,Ineqs,Iqs) :-
  traverseQ(ERest,ExtQ,Ref,SVs,FSs,Ineqs,Iqs).

% ------------------------------------------------------------------------------
% check_inequal(IqsIn:<ineq>s,IqsOut:<ineq>s)
%-------------------------------------------------------------------------------
% Checks the inequations in IqsIn.  Inequations are given in CNF, hence
% IqsIn = [Iq_1,...,Iq_n] holds if Iq_1 holds and ... and Iq_n holds
% Iq_i = ineq(Tag1,SVs1,Tag2,SVs2,ineq(...,done)...) holds if FS1 is not 
% structure-shared with FS2 or ... ("done" marks end of list)
%-------------------------------------------------------------------------------
%check_inequal(Var,Var) :- var(Var), !.
check_inequal([],[]).
check_inequal([IqIn|IqsIn],IqsOut) :-
  check_inequal_conjunct(IqIn,IqOut,Result),
  check_inequal_act(Result,IqOut,IqsIn,IqsOut).

check_inequal_act(done,done,_,_) :-  % conjunct not satisfied
  !,fail.
check_inequal_act(succeed,_,IqsIn,IqsOut) :-  % conjunct satisfied
  !,check_inequal(IqsIn,IqsOut).
check_inequal_act(_,IqOut,IqsIn,[IqOut|IqsOut]) :-  % conjunct temporarily
  check_inequal(IqsIn,IqsOut).                      %  satisfied

check_inequal_conjunct(done,done,done).
check_inequal_conjunct(ineq(ITag1,ISVs1,ITag2,ISVs2,IqInRest),IqOut,Result) :-
  deref(ITag1,ISVs1,Tag1,SVs1),
  deref(ITag2,ISVs2,Tag2,SVs2),
  ( Tag1 == Tag2,
    !, check_inequal_conjunct(IqInRest,IqOut,Result)
  ; SVs1 = a_ X,      % fold in results of unify_type/3 and atom extensionality
    ( SVs2 = a_ Y,    
      (X==Y,          
       !,check_inequal_conjunct(IqInRest,IqOut,Result) 
      ;\+ \+(X=Y),
       !,IqOut = ineq(Tag1,SVs1,Tag2,SVs2,IqOutRest),
       check_inequal_conjunct(IqInRest,IqOutRest,Result)
      ;!,Result = succeed)
    ; functor(SVs2,Sort2,_),
      Sort2 \== bot,
      !, Result = succeed
    ; !, IqOut = ineq(Tag1,SVs1,Tag2,SVs2,IqOutRest),
      check_inequal_conjunct(IqInRest,IqOutRest,Result))
  ; SVs2 = a_ _,
    ( functor(SVs1,Sort1,_),
      Sort1 \== bot,
      !, Result = succeed
    ; !, IqOut = ineq(Tag1,SVs1,Tag2,SVs2,IqOutRest),
      check_inequal_conjunct(IqInRest,IqOutRest,Result))
  ; functor(SVs1,Sort1,_),
    functor(SVs2,Sort2,_),
    \+unify_type(Sort1,Sort2,_),
    !, Result = succeed
  ; check_sub_seq(SVs1,SVs2,IqInRest,IqOut,Result),
    !
  ; IqOut = ineq(Tag1,SVs1,Tag2,SVs2,IqOutRest),
    check_inequal_conjunct(IqInRest,IqOutRest,Result)
  ).

check_sub_seq(_,_,_,_,_) if_h [fail] :-  % atoms never make it to check_sub_seq
  \+ (extensional(S),(\+ (S = a_ _))).
                                        
check_sub_seq(SVs1,SVs2,IqInRest,IqOut,Result) if_h SubGoal :-
  extensional(Sort),
  \+ (Sort = a_ _),
  approps(Sort,FRs),
  length(FRs,N),
  functor(SVs1,Sort,N),
  functor(SVs2,Sort,N),
  new_checks(N,SVs1,SVs2,IqInRest,IqOut,Result,SubGoal).

new_checks(0,_,_,SubGoal,IqOut,Result,
           [check_inequal_conjunct(SubGoal,IqOut,Result)]) :-
  !.
new_checks(N,SVs1,SVs2,IqInRest,IqOut,Result,SubGoal) :-
  arg(N,SVs1,VTag1-VSVs1),
  arg(N,SVs2,VTag2-VSVs2),
  M is N-1,
  new_checks(M,SVs1,SVs2,ineq(VTag1,VSVs1,VTag2,VSVs2,IqInRest),
             IqOut,Result,SubGoal).

% ------------------------------------------------------------------------------
% match_list(Sort:<type>,Vs:<vs>,Tag:<var>,SVs:<svs>,Right:<int>,N:<int>,
%            Dtrs:<ints>,DtrsRest:<var>,NextRight:<int>,
%            IqsIn:<iqs>,IqsOut:<iqs>)
% ------------------------------------------------------------------------------
% Run-time predicate compiled into rules.  Matches a list of cats specified by 
%  Sort(Vs), to span an edge to OldRight, the first of which is Tag-SVs, which 
%  spans to Right.  Also matches an edge for the next category of the current 
%  rule to use (necessary because an initial empty-list cats matches nothing).
% ------------------------------------------------------------------------------
match_list(Sort,[HdFS,TlFS],Tag,SVs,Right,N,[N|DtrsMid],DtrsRest,NextRight,
           IqsIn,IqsOut) :-
  sub_type(ne_list,Sort),
  !,ud(HdFS,Tag-SVs,IqsIn,IqsMid),
  check_inequal(IqsMid,IqsMid2),
  deref(TlFS,_,TlSVs),
  TlSVs =.. [TlSort|TlVs],  % a_ correctly causes error in recursive call
  match_list_rest(TlSort,TlVs,Right,NextRight,DtrsMid,DtrsRest,IqsMid2,IqsOut).

match_list(Sort,_,_,_,_,_,_,_,_,_,_) :-
  error_msg((nl,write('error: cats> value with sort, '),write(Sort),
            write(' is not a valid list argument'))).

% ------------------------------------------------------------------------------
% match_list_rest(Sort<type>,Vs:<vs>,Right:<int>,NewRight:<int>,
%                 DtrsRest:<ints>,DtrsRest2:<var>,IqsIn:<iqs>,IqsOut:<iqs>)
% ------------------------------------------------------------------------------
% same as match_list, except edge spans from Right to NewRight, and no
%  matches for the next category are necessary
% ------------------------------------------------------------------------------
match_list_rest(e_list,_,Right,Right,DtrsRest,DtrsRest,Iqs,Iqs) :- 
  !.
match_list_rest(Sort,[HdFS,TlFS],Right,NewRight,[N|DtrsRest],DtrsRest2,IqsIn,
                IqsOut) :-
  sub_type(ne_list,Sort),
  !,edge(N,Right,MidRight,Tag,SVs,EdgeIqs,_,_),
  ud(HdFS,Tag-SVs,IqsIn,IqsMid),
  conc(IqsMid,EdgeIqs,IqsMid2),
  check_inequal(IqsMid2,IqsMid3),
  deref(TlFS,_,TlSVs),
  TlSVs =.. [TlSort|TlVs],  % a_ correctly causes error in recursive call
  match_list_rest(TlSort,TlVs,MidRight,NewRight,DtrsRest,DtrsRest2,IqsMid3,
                  IqsOut).
match_list_rest(Sort,_,_,_,_,_,_,_) :-
  error_msg((nl,write('error: cats> value with sort, '),write(Sort),
            write(' is not a valid list argument'))).


% ==============================================================================
% Chart Parser
% ==============================================================================

% ------------------------------------------------------------------------------
% rec(+Ws:<word>s, Tag:<var_tag>, SVs:<svs>, Iqs:<ineq>s)
% ------------------------------------------------------------------------------
% Ws can be parsed as category Tag-SVs with inequations Iqs;  Tag-SVs 
%  uninstantiated to start
% ------------------------------------------------------------------------------
:- dynamic num/1.

rec(Ws,Tag,SVs,IqsOut):-
  clear,
  assert(parsing(Ws)),
  asserta(num(0)),
  reverse_count(Ws,[],WsRev,0,Length),
  build(WsRev,Length),
  edge(_,0,Length,Tag,SVs,IqsIn,_,_),
  extensionalise(Tag,SVs,IqsIn),
  check_inequal(IqsIn,IqsOut).

% ------------------------------------------------------------------------------
% build(Ws:<word>s, Right:<int>)
% ------------------------------------------------------------------------------
% fills in charts inactive edges from beginning to Right using 
% Ws, representing words in chart in reverse order
% ------------------------------------------------------------------------------
build([W|Ws],Right):-
  RightMinus1 is Right - 1,
  ( empty_cat(Tag,SVs,Iqs),
    add_edge(Right,Right,Tag,SVs,Iqs,[],empty)
  ;       [no,lexical,entry,for,W] if_error
              (\+ lex(W,_,_,_) ), 
    lex(W,Tag,SVs,Iqs),
    add_edge(RightMinus1,Right,Tag,SVs,Iqs,[],lexicon)
  ; build(Ws,RightMinus1)
  ).
build([],_):-
  empty_cat(Tag,SVs,Iqs),
  add_edge(0,0,Tag,SVs,Iqs,[],empty).
build([],_) :-
  quiet_interpreter,  % if quiet mode was on, turn it off.
  !,secret_verbose.
build([],_).

% ------------------------------------------------------------------------------
% add_edge_deref(Left:<int>, Right:<int>, Tag:<var_tag>, SVs:<svs>, 
%                Iqs:<ineq>s,Dtrs:<fs>s,RuleName)                           eval
% ------------------------------------------------------------------------------
% adds dereferenced category Tag-SVs,Iqs as inactive edge from Left to Right;
% check for any rules it might start, then look for categories in chart
% to complete those rules
% ------------------------------------------------------------------------------
add_edge_deref(Left,Right,Tag,SVs,IqsIn,Dtrs,RuleName):-
  fully_deref_prune(Tag,SVs,TagOut,SVsOut,IqsIn,IqsOut),
  (subsumed(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName),
   !,fail
  ;edge_assert(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,N),
   apply_rule(TagOut,SVsOut,IqsOut,Left,Right,N)).

add_edge(Left,Right,TagOut,SVsOut,IqsIn,Dtrs,RuleName):-
  check_inequal(IqsIn,IqsOut),    % CAN PROBABLY REMOVE THIS
  (subsumed(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName),
   !,fail
  ;edge_assert(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,N),
   apply_rule(TagOut,SVsOut,IqsOut,Left,Right,N)).

apply_rule(TagOut,SVsOut,IqsOut,Left,Right,N) :-
  N >= 0,   % make sure the proposed edge was asserted
  rule(TagOut,SVsOut,IqsOut,Left,Right,N).

gennum(N) :-
  retract(num(N)),
  NewN is N+1,
  asserta(num(NewN)).

count_edges(N):-
  setof(edge(M,X,Y,Z,W,I,D,R),edge(M,X,Y,Z,W,I,D,R),Es),
  length(Es,N).

% subsumed(Left:<int>,Right:<int>,Tag:<var_tag>,SVs:<svs>,Iqs:<ineq>s,
%          Dtrs:<int>s,RuleName)
% ------------------------------------------------------------------------------
% Check if any edge spanning Left to Right subsumes Tag-SVs, the feature
%  structure of the candidate edge, or vice versa.  Succeeds based on whether
%  or not Tag-SVs is subsumed - but all edges subsumed by Tag-SVs are also
%  retracted.
% ------------------------------------------------------------------------------
subsumed(_,_,_,_,_,_,_) :-
  no_subsumption,
  !,fail.

subsumed(Left,Right,Tag,SVs,Iqs,Dtrs,RuleName) :-
  edge(EI,Left,Right,ETag,ESVs,EIqs,_,_),  % this may have more than 1 soln!
  subsume([s(Tag,SVs,ETag,ESVs)],Iqs,EIqs,<,>,LReln,RReln,[],[]),
  subsumed_act(RReln,LReln,EI,Tag,SVs,Iqs,Dtrs,RuleName,Left,Right).

subsumed_act(>,LReln,EI,Tag,SVs,Iqs,Dtrs,RuleName,Left,Right) :- % edge subsumes
  !,edge_discard(LReln,EI,Tag,SVs,Iqs,Dtrs,RuleName,Left,Right). %  candidate 
subsumed_act(#,<,EI,Tag,SVs,Iqs,Dtrs,RuleName,_,_) :-
  edge_retract(EI,Tag,SVs,Iqs,Dtrs,RuleName).         % candidate subsumes edge
% subsumed_act(#,#,_,_,_,_,_,_,_,_) fails

% subsume(Ss,Iqs1,Iqs2,LeftRelnIn,RightRelnIn,LeftRelnOut,RightRelnOut,H,K)
% ------------------------------------------------------------------------------
% LeftRelnOut is bound to < if there exists a subsumption morphism, H (see
%  Carpenter, 1992, p. 41) from Tag1-SVs1 to Tag2-SVs2, for every 
%  s(Tag1,SVs1,Tag2,SVs2) in Ss, and from the inequations in Iqs1 to those in
%  Iqs2.  Otherwise, LeftReln is bound to #.  RightRelnOut is bound to > if
%  a subsumption morphism, K, exists in the reverse direction, and is bound
%  otherwise to #.  The FS's in the s-structures are expected to be fully
%  dereferenced, with irrelevant inequations pruned off (which can be
%  achieved by using fully_deref_prune).
% ------------------------------------------------------------------------------
subsume([],Iqs,EIqs,LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K) :-
  subsume_iqs(Iqs,EIqs,LRelnIn,LRelnOut,H),
  subsume_iqs(EIqs,Iqs,RRelnIn,RRelnOut,K).
subsume([s(Tag,SVs,ETag,ESVs)|Ss],Iqs,EIqs,
         LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K) :-
  map_h_eq(H,Tag,HTag,_,HRes),
  map_h_eq(K,ETag,KTag,_,KRes),
  subsume_act(HRes,KRes,HTag,KTag,Tag,SVs,ETag,ESVs,Ss,Iqs,EIqs,
              LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K).

subsume_act(?,?,_,_,Tag,SVs,ETag,ESVs,Ss,Iqs,EIqs,
            LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K) :-
  !,subsume_type(<,Tag,SVs,ETag,ESVs,Ss,Iqs,EIqs,  % not # in 1st arg 
                 LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K).
subsume_act(?,!,_,_,Tag,SVs,ETag,ESVs,Ss,Iqs,EIqs,
            LRelnIn,_,LRelnOut,#,H,K) :-
  !,subsume_type(LRelnIn,Tag,SVs,ETag,ESVs,Ss,Iqs,EIqs,
                 LRelnIn,#,LRelnOut,#,H,K).
subsume_act(!,?,_,_,Tag,SVs,ETag,ESVs,Ss,Iqs,EIqs,
            _,RRelnIn,#,RRelnOut,H,K) :-
  !,subsume_type(RRelnIn,Tag,SVs,ETag,ESVs,Ss,Iqs,EIqs,
                 #,RRelnIn,#,RRelnOut,H,K).

subsume_act(!,!,HTag,KTag,Tag,_,ETag,_,Ss,Iqs,EIqs,
            LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K) :-        % already visited,
  KTag == Tag,              % so go on to the rest unless already incomparable
  !,subsume_act2(HTag,ETag,Ss,Iqs,EIqs,LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K).
subsume_act(!,!,HTag,_,_,_,ETag,_,Ss,Iqs,EIqs,
            LRelnIn,_,LRelnOut,#,H,K) :-
  subsume_act2(HTag,ETag,Ss,Iqs,EIqs,LRelnIn,#,LRelnOut,#,H,K).
subsume_act2(HTag,ETag,Ss,Iqs,EIqs,LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K) :-
  HTag == ETag,
  !,subsume_act3(LRelnIn,RRelnIn,Ss,Iqs,EIqs,LRelnOut,RRelnOut,H,K).
subsume_act2(_,_,Ss,Iqs,EIqs,_,RRelnIn,#,RRelnOut,H,K) :-
  subsume_act3(#,RRelnIn,Ss,Iqs,EIqs,#,RRelnOut,H,K).

subsume_act3(#,#,_,_,_,#,#,_,_) :- !. % incomparable 
subsume_act3(LRelnIn,RRelnIn,Ss,Iqs,EIqs,LRelnOut,RRelnOut,H,K) :-
  subsume(Ss,Iqs,EIqs,LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K).

% compare types if Reln isn't # yet
subsume_type(#,_,_,_,_,_,_,_,_,_,#,#,_,_) :- !.
subsume_type(_,Tag,SVs,ETag,ESVs,Ss,Iqs,EIqs,
             LRelnIn,RRelnIn,LRelnOut,RRelnOut,H,K) :-
  ((SVs = (a_ X)) ->
   (Sort = (a_ X),Vs=[])
   ;SVs =.. [Sort|Vs]),
  ((ESVs = (a_ X)) ->
   (ESort = (a_ X),EVs=[])
   ;ESVs =.. [ESort|EVs]),
  sub_type_reln(Sort,ESort,TReln),
  subsume_type_act(TReln,LRelnIn,RRelnIn,LRelnOut,RRelnOut,Tag,ETag,Sort,ESort,
                   Vs,EVs,SVs,ESVs,Ss,Iqs,EIqs,H,K).

% add common values to S-list
subsume_type_act(=,#,RRelnIn,#,RRelnOut,Tag,ETag,_,_,
                 Vs,EVs,SVs,_,Ss,Iqs,EIqs,H,K) :-
  !,subsume_type_act2(RRelnIn,RRelnOut,#,#,H,
                      Tag,ETag,Vs,EVs,SVs,Ss,Iqs,EIqs,K).
subsume_type_act(=,LRelnIn,RRelnIn,LRelnOut,RRelnOut,Tag,ETag,_,_,
                 Vs,EVs,SVs,ESVs,Ss,Iqs,EIqs,H,K) :-
  !,subsume_type_act2(RRelnIn,RRelnOut,LRelnIn,LRelnOut,[h(Tag,ETag,ESVs)|H],
                      Tag,ETag,Vs,EVs,SVs,Ss,Iqs,EIqs,K).
subsume_type_act2(#,#,LRelnIn,LRelnOut,NewH,_,_,Vs,EVs,_,Ss,Iqs,EIqs,K) :-
  !,append_s(Vs,EVs,Ss,NewSs),
  subsume(NewSs,Iqs,EIqs,LRelnIn,#,LRelnOut,#,NewH,K).
subsume_type_act2(RRelnIn,RRelnOut,LRelnIn,LRelnOut,NewH,
                  Tag,ETag,Vs,EVs,SVs,Ss,Iqs,EIqs,K) :-
  append_s(Vs,EVs,Ss,NewSs),
  subsume(NewSs,Iqs,EIqs,LRelnIn,RRelnIn,LRelnOut,RRelnOut,
          NewH,[h(ETag,Tag,SVs)|K]).

subsume_type_act(<,#,_,#,#,_,_,_,_,_,_,_,_,_,_,_,_,_) :- !.
subsume_type_act(<,LRelnIn,_,LRelnOut,#,Tag,ETag,Sort,ESort,Vs,EVs,_,ESVs,
                 Ss,Iqs,EIqs,H,K) :-
  approps(Sort,FRs),
  approps(ESort,EFRs),
  sub_feats(FRs,EFRs,EVs,SubEVs),
  append_s(Vs,SubEVs,Ss,NewSs),
  subsume(NewSs,Iqs,EIqs,LRelnIn,#,LRelnOut,#,[h(Tag,ETag,ESVs)|H],K).
subsume_type_act(>,_,#,#,#,_,_,_,_,_,_,_,_,_,_,_,_,_) :- !.
subsume_type_act(>,_,RRelnIn,#,RRelnOut,Tag,ETag,Sort,ESort,Vs,EVs,SVs,_,
                 Ss,Iqs,EIqs,H,K) :-
  approps(Sort,FRs),
  approps(ESort,EFRs),
  sub_feats(EFRs,FRs,Vs,SubVs),
  append_s(SubVs,EVs,Ss,NewSs),
  subsume(NewSs,Iqs,EIqs,#,RRelnIn,#,RRelnOut,H,[h(ETag,Tag,SVs)|K]).
subsume_type_act(#,_,_,#,#,_,_,_,_,_,_,_,_,_,_,_,_,_).

subsume_iqs([],_,Reln,Reln,_).
subsume_iqs([_|_],_,#,#,_) :- !.
subsume_iqs([Iq|Iqs1],Iqs2,RelnIn,RelnOut,H) :-
  subsume_iq(Iq,Iqs2,RelnIn,RelnMid,H),% make sure image of each conjunct holds
  subsume_iqs(Iqs1,Iqs2,RelnMid,RelnOut,H). % in image FS

subsume_iq(done,Iqs2Out,_,#,_) :- % negated image of conjunct is satisfied
  check_inequal(Iqs2Out,_),     % by image FS, so no subsumption morphism 
  !.                            % exists.
subsume_iq(ineq(Tag1,SVs1,Tag2,SVs2,IqRest),Iqs2Mid,RelnIn,RelnOut,H) :-
  map_h_eq(H,Tag1,HTag1,HSVs1,HRes),   % test which inequated FS has an image
  map_h_eq(H,Tag2,HTag2,HSVs2,KRes),
  subsume_iq_act(HRes,KRes,HTag1,HSVs1,HTag2,HSVs2,Tag1,SVs1,Tag2,SVs2,
                 IqRest,Iqs2Mid,RelnIn,RelnOut,H),
  !.   % need this cut since the call to subsume_iq in unify_disjunct_image
       % may succeed with the next clause, and we don't want it twice.

subsume_iq(_,_,Reln,Reln,_). % image of conjunct is either satisfied by an 
                             %  inequation conjunct of the image FS (which 
                             %  failed in the 1st clause above), or is 
                             %  implicitly encoded in the image FS (since 
                             %  unifying the images of the inequated FS's of
                             %  every disjunct failed in the 2nd clause above).

subsume_iq_act(?,_,_,_,HTag2,HSVs2,Tag1,SVs1,_,_,IqRest,Iqs2Mid,
               RelnIn,RelnOut,H) :-  % Inequation is relevant so KRes is !
  !,unify_disjunct_image(Tag1,SVs1,HTag2,HSVs2,IqRest,Iqs2Mid,
                         RelnIn,RelnOut,H).
  % use an inequated FS with no image itself for matching conjuncts
subsume_iq_act(!,KRes,HTag1,HSVs1,HTag2,HSVs2,_,_,Tag2,SVs2,IqRest,Iqs2Mid,
               RelnIn,RelnOut,H) :-
  subsume_iq_act2(KRes,HTag2,HSVs2,HTag1,HSVs1,Tag2,SVs2,IqRest,Iqs2Mid,
                  RelnIn,RelnOut,H).

subsume_iq_act2(?,_,_,HTag1,HSVs1,Tag2,SVs2,IqRest,Iqs2Mid,RelnIn,RelnOut,H) :-
  !,unify_disjunct_image(HTag1,HSVs1,Tag2,SVs2,IqRest,Iqs2Mid,
                         RelnIn,RelnOut,H).
subsume_iq_act2(!,HTag2,HSVs2,HTag1,HSVs1,_,_,
                IqRest,Iqs2Mid,RelnIn,RelnOut,H) :-
  unify_disjunct_image(HTag1,HSVs1,HTag2,HSVs2,IqRest,Iqs2Mid,
                       RelnIn,RelnOut,H).

unify_disjunct_image(Tag1,SVs1,Tag2,SVs2,IqRest,Iqs2Mid,RelnIn,RelnOut,H) :-
  u(SVs1,SVs2,Tag1,Tag2,Iqs2Mid,Iqs2Out),
  subsume_iq(IqRest,Iqs2Out,RelnIn,RelnOut,H).


% sub_feats(SubFRs,FRs,Vs,SubVs)
% ------------------------------------------------------------------------------
% SubFRs is a sorted sublist of sorted feature:restriction list, FRs.  Vs is
%  a list of values of features of FRs in order.  SubVs is the sublist of Vs 
%  consisting of values of features of SubFRs in order.
% ------------------------------------------------------------------------------
sub_feats([],_,_,[]) :- 
  !.
sub_feats([Feat:_|SubFRs],[Feat:_|FRs],[V|Vs],[V|SubVs]) :-
  !,sub_feats(SubFRs,FRs,Vs,SubVs).
sub_feats(SubFRs,[_|FRs],[_|Vs],SubVs) :-
  sub_feats(SubFRs,FRs,Vs,SubVs).

% append_s(Vs,EVs,Ss,NewSs)
% ------------------------------------------------------------------------------
% NewSs is Ss plus in-order pairs of FS's from Vs and EVs (which are the same
%  length), in s-structures.
% ------------------------------------------------------------------------------
append_s([],[],Ss,Ss).
append_s([Tag-SVs|Vs],[ETag-ESVs|EVs],Ss,[s(Tag,SVs,ETag,ESVs)|NewSs]) :-
  append_s(Vs,EVs,Ss,NewSs).

% map_h_eq(H,Tag,ImageTag,ImageSV,Result)
% ------------------------------------------------------------------------------
%  Find the image of Tag under subsumption morphism, H.  If the image is 
%   known, return Result !; if not, return ?.
% ------------------------------------------------------------------------------
map_h_eq([],_,_,_,?).
map_h_eq([h(Tag1,Tag2,SVs2)|_],Tag,Tag2,SVs2,!) :-
  Tag1 == Tag,!.
map_h_eq([_|H],Tag1,Tag2,SVs2,Result) :-
  map_h_eq(H,Tag1,Tag2,SVs2,Result).

% sub_type_reln(Sort1,Sort2,Reln)
% ------------------------------------------------------------------------------
%  Reln is =,<,>, or # based on subsumption comparison of Sort1 and Sort2
% ------------------------------------------------------------------------------
sub_type_reln(Sort,ESort,Reln) :-
  sub_type(Sort,ESort),
  !,(sub_type(ESort,Sort) -> (Reln = '=')   % can't use unification for =
                           ; (Reln = '<')). % because of poss. atom subsumption
sub_type_reln(Sort,ESort,>) :-
  sub_type(ESort,Sort),
  !.
sub_type_reln(_,_,#).


% edge_discard(LReln:<var>/#,I:<int>,Tag:<var_tag>,SVs:<sv>s,Iqs:<ineq>s,
%             Dtrs:<int>s,RuleName,Left:<int>,Right:<int>)
% ------------------------------------------------------------------------------
% Discard edge Tag-SVs, with inequations Iqs, daughters Dtrs, created by rule
%  RuleName, because it is subsumed by the edge with index I.  If LReln is a
%  variable, then the two are equal - otherwise, LReln is #, which indicates
%  strict subsumption.
% ------------------------------------------------------------------------------
edge_discard(_,_,_,_,_,_,_,_,_) :-
  no_interpreter,
  !.
edge_discard(_,_,_,_,_,_,_,_,_) :-
  quiet_interpreter,
  !.
edge_discard(LReln,I,Tag,SVs,Iqs,Dtrs,RuleName,Left,Right) :-
  verbose_interpreter,
  length(Dtrs,ND),
  !,print_edge_discard(LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).

print_edge_discard(LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nl,pp_fs(Tag-SVs,Iqs),
  nl,write('Edge created for category above:'),
%  nl,write('     index: '),write(I),
  nl,write('      from: '),write(Left),write(' to: '),write(Right),
  nl,write('    string: '),write_out(Left,Right),
  nl,write('      rule: '),write(RuleName),
  nl,write(' # of dtrs: '),write(ND),nl,
  print_edge_discard_act(LReln,I),
  nl,query_discard(LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).

print_edge_discard_act(<,I) :-
  !,nl,write('is equal to an existing edge, index:'),write(I),write('.').
print_edge_discard_act(#,I) :-
  nl,write('is subsumed by an existing edge, index:'),write(I),write('.').

query_discard(_,_,_,_,_,_,_,_,_,_) :-
  go(_),
  !.
query_discard(LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nl,write('Action(noadd,continue,break,dtr-#,existing,abort)? '),
  nl,read(Response),
  query_discard_act(Response,LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).

query_discard_act(noadd,_,_,_,_,_,_,_,_,_,_) :- !.
query_discard_act(continue,_,_,_,_,_,_,_,_,_,_) :- 
  !,fail.
query_discard_act(break,LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  !,break,
  print_edge_discard(LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).
query_discard_act(dtr-D,LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nth_index(Dtrs,D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule),
  !,length(DDtrs,DND),
  print_dtr_edge(D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND),
  print_edge_discard(LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).
query_discard_act(existing,LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  edge(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName),
  !,edge_act(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName),  
  print_edge_discard(LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).
query_discard_act(abort,_,_,_,_,_,_,_,_,_,_) :-
  !,abort.
query_discard_act(_,LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  query_discard(LReln,I,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).

% edge_retract(I:<int>,Tag:<var_tag>,SVs:<svs>,Iqs:<ineq>s,Dtrs:<int>s,
%              RuleName)
% ------------------------------------------------------------------------------
% Retract edge with index I because it is subsumed by Tag-SVs, with inequations
%  Iqs, daughters Dtrs, created by rule RuleName
% ------------------------------------------------------------------------------
edge_retract(I,_,_,_,_,_) :-
  no_interpreter,
  retract(edge(I,_,_,_,_,_,_,_)),
  !,fail.     % failure-drive through all subsumed edges

edge_retract(I,_,_,_,_,_) :-
  quiet_interpreter,
  retract(edge(I,_,_,_,_,_,_,_)),
  !,fail.

edge_retract(I,Tag,SVs,Iqs,Dtrs,RuleName) :-
  verbose_interpreter,
  !,edge(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName),
  length(EDtrs,NED),
  print_edge_retract(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                     Tag,SVs,Iqs,Dtrs,RuleName).

print_edge_retract(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                   Tag,SVs,Iqs,Dtrs,RuleName) :-
  nl,pp_fs(ETag-ESVs,EIqs),
  nl,write('Edge created for category above:'),
  nl,write('     index: '),write(I),
  nl,write('      from: '),write(Left),write(' to: '),write(Right),
  nl,write('    string: '),write_out(Left,Right),
  nl,write('      rule: '),write(ERuleName),
  nl,write(' # of dtrs: '),write(NED),nl,
  nl,write('is subsumed by an incoming edge.'),
  nl,query_retract(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                   Tag,SVs,Iqs,Dtrs,RuleName).

query_retract(I,_,_,_,_,_,_,_,_,_,_,_,_,_) :-
  go(_),
  retract(edge(I,_,_,_,_,_,_,_)),
  !,fail.
query_retract(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
              Tag,SVs,Iqs,Dtrs,RuleName) :-
  nl,write('Action(retract,continue,break,dtr-#,incoming,abort)? '),
  nl,read(Response),
  query_retract_act(Response,I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                    Tag,SVs,Iqs,Dtrs,RuleName).
query_retract_act(retract,I,_,_,_,_,_,_,_,_,_,_,_,_,_) :-
  retract(edge(I,_,_,_,_,_,_,_)),
  !,fail.
query_retract_act(remain,_,_,_,_,_,_,_,_,_,_,_,_,_,_) :-
  !,fail.
query_retract_act(continue,_,_,_,_,_,_,_,_,_,_,_,_,_,_) :-
  !.
query_retract_act(break,I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                  Tag,SVs,Iqs,Dtrs,RuleName) :-
  !,break,
  print_edge_retract(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                     Tag,SVs,Iqs,Dtrs,RuleName).
query_retract_act(dtr-D,I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                  Tag,SVs,Iqs,Dtrs,RuleName) :-
  nth_index(EDtrs,D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule),
  !,length(DDtrs,DND),
  print_dtr_edge(D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND),
  print_edge_retract(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                     Tag,SVs,Iqs,Dtrs,RuleName).
query_retract_act(incoming,I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                  Tag,SVs,Iqs,Dtrs,RuleName) :-
  !,length(Dtrs,ND),
  print_incoming_edge(Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND),
  !
  ;print_edge_retract(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                     Tag,SVs,Iqs,Dtrs,RuleName).
query_retract_act(abort,_,_,_,_,_,_,_,_,_,_,_,_,_,_) :-
  !,abort.
query_retract_act(_,I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                  Tag,SVs,Iqs,Dtrs,RuleName) :-
  query_retract(I,Left,Right,ETag,ESVs,EIqs,EDtrs,ERuleName,NED,
                Tag,SVs,Iqs,Dtrs,RuleName).

print_incoming_edge(Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nl,pp_fs(Tag-SVs,Iqs),
  nl,write('Incoming Edge: '),
  nl,write('      from: '),write(Left),write(' to: '),write(Right),
  nl,write('    string: '),write_out(Left,Right),
  nl,write('      rule:  '),write(RuleName),
  nl,write(' # of dtrs: '),write(ND),
  query_incoming_edge(Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).

query_incoming_edge(Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nl,write('Action(noadd,dtr-#,existing,abort)?' ),
  nl,read(Response),
  query_incoming_act(Response,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).
query_incoming_act(noadd,_,_,_,_,_,_,_,_) :-
  !.
query_incoming_act(existing,_,_,_,_,_,_,_,_) :-
  !,fail.
query_incoming_act(abort,_,_,_,_,_,_,_,_) :-
  !,abort.
query_incoming_act(dtr-D,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nth_index(Dtrs,D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule),
  !,length(DDtrs,DND),
  print_dtr_edge(D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND),
  print_incoming_edge(Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).
query_incoming_act(_,Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  query_incoming_edge(Left,Right,Tag,SVs,Iqs,Dtrs,RuleName,ND).

% ==============================================================================
% Interpreter
% ==============================================================================

edge_assert(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,N) :- 
  no_interpreter,                                      
  !,gennum(N),
  asserta(edge(N,Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName)). 

edge_assert(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,N) :-
  quiet_interpreter,
  !,gennum(N),
  asserta(edge(N,Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName)).

edge_assert(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,N) :-
  verbose_interpreter,
  !,nl,
  length(Dtrs,ND),
  print_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND),
  edge_assert_act(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,N).

% REWRITE THIS
edge_assert_act(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,N) :-
  retract(assert_edge),
  !,gennum(N),
  asserta(edge(N,Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName)).
edge_assert_act(_,_,_,_,_,_,_,-1).  % apply_rule will check N >= 0.

print_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND) :-
  nl,pp_fs(TagOut-SVsOut,IqsOut),
  nl,write('Edge created for category above: '),
  nl,write('      from: '),write(Left),write(' to: '),write(Right),
  nl,write('    string: '),write_out(Left,Right),
  nl,write('      rule:  '),write(RuleName),
  nl,write(' # of dtrs: '),write(ND),
  nl,query_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND).

query_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND) :-
  go(Left),               % right-to-left parser triggers on left
  !,retractall(go(_)),
  query_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND).
query_edge(_,_,_,_,_,_,_,_) :-
  go(_),
  !,asserta(assert_edge).
query_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND) :-
  nl,write('Action(add,noadd,go(-#),quiet,break,dtr-#,abort)? '),
  nl,read(Response),
  query_edge_act(Response,Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND).

query_edge_act(add,_,_,_,_,_,_,_,_) :-
  !,asserta(assert_edge).
query_edge_act(noadd,_,_,_,_,_,_,_,_) :- !.
query_edge_act(go,_,_,_,_,_,_,_,_) :-
  !,asserta(assert_edge),
  asserta(go(go)).
query_edge_act(go-G,_,_,_,_,_,_,_,_) :-
  !,asserta(assert_edge),
  asserta(go(G)).
query_edge_act(quiet,_,_,_,_,_,_,_,_) :-
  !,asserta(assert_edge),
  secret_quiet.
query_edge_act(break,Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND) :-
  !,break,
  print_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND).
query_edge_act(dtr-D,Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND):-
  nth_index(Dtrs,D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule),
  !,length(DDtrs,DND),
  print_dtr_edge(D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND),
  print_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND).
query_edge_act(abort,_,_,_,_,_,_,_,_) :-
  !,abort.
query_edge_act(_,Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND) :-
  query_edge(Left,Right,TagOut,SVsOut,IqsOut,Dtrs,RuleName,ND).

print_dtr_edge(D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND) :-
  nl,pp_fs(DTag-DSVs,DIqs),
  nl,write('Daughter number '), write(D),
  nl,write('      from: '),write(DLeft),write(' to: '),write(DRight),
  nl,write('    string: '),write_out(DLeft,DRight),
  nl,write('      rule:  '),write(DRule),
  nl,write(' # of dtrs: '),write(DND),
  query_dtr_edge(D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND).

query_dtr_edge(D,I,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND) :-
  nl,write('Action(retract,dtr-#,parent,abort)?' ),
  nl,read(Response),
  query_dtr_act(Response,D,I,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND).
query_dtr_act(parent,_,_,_,_,_,_,_,_,_,_) :-
  !.
query_dtr_act(retract,_,I,_,_,_,_,_,_,_,_) :-
  retract(edge(I,_,_,_,_,_,_,_)),
  !.
query_dtr_act(abort,_,_,_,_,_,_,_,_,_,_) :-
  !,abort.
query_dtr_act(dtr-DD,D,I,Left,Right,Tag,SVs,Iqs,Dtrs,Rule,ND) :-
  nth_index(Dtrs,DD,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule),
  !,length(DDtrs,DND),
  print_dtr_edge(DD,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND),
  print_dtr_edge(D,I,Left,Right,Tag,SVs,Iqs,Dtrs,Rule,ND).
query_dtr_act(_,D,I,Left,Right,Tag,SVs,Iqs,Dtrs,Rule,ND) :-
  query_dtr_edge(D,I,Left,Right,Tag,SVs,Iqs,Dtrs,Rule,ND).

% REWRITE THIS
nth_index([I|_],1,I,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule) :- 
  !,edge(I,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule).
nth_index([_|Is],N,I,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule) :-
  N > 1,
  NMinus1 is N-1,
  nth_index(Is,NMinus1,I,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule).

edge_dtrs([],[],Iqs,Iqs).
edge_dtrs([I|Is],[Tag-SVs|FSs],DtrIqs,MotherIqs) :-
  edge(I,_,_,Tag,SVs,Iqs,_,_),
  conc(Iqs,Rest,DtrIqs),
  edge_dtrs(Is,FSs,Rest,MotherIqs).

% ==============================================================================
% Functional Description Resolution/Compilation
% ==============================================================================

% fsolve(Fun:<fun>,FS:<fs>,IqsIn:<ineq>s,IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
%  Solve function constraint, Fun, along with its argument descriptions.
% ------------------------------------------------------------------------------
fsolve(_,_,_,_) if_b [fail] :-
  \+ current_predicate(+++>,+++>(_,_)).
fsolve(Fun,FS,IqsIn,IqsOut) if_b Goals :-
  current_predicate(+++>,+++>(_,_)),
  (FHead +++> FResult),
  FHead =.. [Rel|ArgDescs],
  compile_descs(ArgDescs,Args,IqsIn,IqsMid,Goals,
                [check_inequal(IqsMid,IqsMid2)|GoalsMid]),
  Fun =.. [Rel|Args],
  compile_desc(FResult,FS,IqsMid2,IqsOut,GoalsMid,[]).


% ==============================================================================
% Definite Clause Resolution/Compilation
% ==============================================================================

% ------------------------------------------------------------------------------
% solve(Goals:<goal>s,IqsIn:<ineq>s,IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% Gs is list of goals to be called
% ------------------------------------------------------------------------------
solve([],Iqs,Iqs).
solve([Goal|TailGoals],IqsIn,IqsOut):-
  solve(Goal,TailGoals,IqsIn,IqsOut).

% ------------------------------------------------------------------------------
% solve(Goal:<goal>, TailGoals:<goal>s, IqsIn:<ineq>s, IqsOut:<ineq>s)     mh(0)
% ------------------------------------------------------------------------------
% solves Goal and then tail recursively solves TailGoals
% ------------------------------------------------------------------------------
solve(_,_,_,_) if_b [fail] :-
  \+ current_predicate(if,if(_,_)).
solve(Goal,TailGoals,IqsIn,IqsOut) if_b PGoals:-
  current_predicate(if,if(_,_)),
  (Head if Body),
  Head =.. [Rel|ArgDescs],
  compile_descs(ArgDescs,Args,IqsIn,IqsMid,PGoals,
                [check_inequal(IqsMid,IqsMid2)|PGoalsRest]),
  Goal =.. [Rel|Args],
  compile_body(Body,[],TailGoals,IqsMid2,IqsOut,PGoalsRest,[]).
solve(true,TailGoals,IqsIn,IqsOut) if_b 
      [solve(TailGoals,IqsIn,IqsOut)]. 
      % needed for trivial input case
% to add more Prolog power to solve/2, could use the following:
%solve((G1;G2),TailGoals) if_b [( solve(G1,TailGoals) 
%                               ; solve(G2,TailGoals) 
%                               )].
%solve((G1,G2),TailGoals) if_b [solve(G1,[]), solve(G2,TailGoals)].

% ------------------------------------------------------------------------------
% compile_body(GoalDesc,ContGoals,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest)
% ------------------------------------------------------------------------------
% compiles arbitrary Goal, assuming ContGoals is a list of goals to solve
% first and TailGoals is list of goals to solve last;  TailGoals 
% is uninstantiated at compile time;  
% PGoals is instantiated to list of Prolog goals required to add
% arguments relations in Goal and then call the procedure to solve them
% IqsIn and IqsOut are uninstantiated at compile time.
% ------------------------------------------------------------------------------
compile_body(((GD1,GD2),GD3),ContGoals,TailGoals,IqsIn,IqsOut,
             PGoals,PGoalsRest):-
  !, compile_body((GD1,(GD2,GD3)),ContGoals,TailGoals,IqsIn,IqsOut,
                  PGoals,PGoalsRest).
compile_body(((GD1;GD2),GD3),ContGoals,TailGoals,IqsIn,IqsOut,
             PGoals,PGoalsRest):-
  !, compile_body(((GD1,GD3);(GD2,GD3)),ContGoals,TailGoals,IqsIn,IqsOut,
                  PGoals,PGoalsRest).
compile_body((\+ GD1, GD2),ContGoals,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  !, compile_cont(ContGoals,IqsIn,IqsMid,PGoals,[\+ PGoal|PGoalsMid]),
  compile_body(GD1,[],[],IqsMid,_,PGoalsList,[]),
  goal_list_to_seq(PGoalsList,PGoal),
  compile_body(GD2,[],TailGoals,IqsMid,IqsOut,PGoalsMid,PGoalsRest).
compile_body((Desc1 =@ Desc2,GD),ContGoals,TailGoals,IqsIn,IqsOut,
             PGoals,PGoalsRest):-
  !,compile_cont(ContGoals,IqsIn,IqsMid,PGoals,PGoalsMid),
  compile_desc(Desc1,Tag1-bot,IqsMid,IqsMid2,PGoalsMid,PGoalsMid2),
  compile_desc(Desc2,Tag2-bot,IqsMid2,IqsMid3,PGoalsMid2,
               [deref(Tag1,bot,DTag1,DSVs1),
                deref(Tag2,bot,DTag2,DSVs2),
                extensionalise_list([DTag1-DSVs1,DTag2-DSVs2],IqsMid3),
                check_inequal(IqsMid3,IqsMid4),
                deref(DTag1,DSVs1,Tag1Out,_),
                deref(DTag2,DSVs2,Tag2Out,_),
                (Tag1Out == Tag2Out)|PGoalsMid3]),
  compile_body(GD,[],TailGoals,IqsMid4,IqsOut,PGoalsMid3,PGoalsRest).
compile_body((true,GD),Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  !, compile_body(GD,Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest).
compile_body((!,PGD),Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  !, compile_cont(Cont,IqsIn,IqsMid,PGoals,[!|PGoalsMid]),
  compile_body(PGD,[],TailGoals,IqsMid,IqsOut,PGoalsMid,PGoalsRest).
compile_body((prolog(Goal),GD),ContGoals,TailGoals,IqsIn,IqsOut,
             PGoals,PGoalsRest) :-
  !,compile_cont(ContGoals,IqsIn,IqsMid,PGoals,[Goal|PGoalsMid]),
  compile_body(GD,[],TailGoals,IqsMid,IqsOut,PGoalsMid,PGoalsRest).
compile_body((AGD,GD2),Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  !, AGD =.. [Rel|ArgDescs],
  compile_descs_fresh(ArgDescs,Args,IqsIn,IqsMid,PGoals,PGoalsMid),
  Goal =.. [Rel|Args],
  conc(Cont,[Goal],NewCont),
  compile_body(GD2,NewCont,TailGoals,IqsMid,IqsOut,PGoalsMid,PGoalsRest).
compile_body((GD1;GD2),Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  !, compile_cont(Cont,IqsIn,IqsMid,PGoals,[(PGoal1;PGoal2)|PGoalsRest]),
  compile_body(GD1,[],TailGoals,IqsMid,IqsOut,PGoals1,[]),
  compile_body(GD2,[],TailGoals,IqsMid,IqsOut,PGoals2,[]),
  goal_list_to_seq(PGoals1,PGoal1),
  goal_list_to_seq(PGoals2,PGoal2).
compile_body((\+ GD),Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  !, compile_cont(Cont,IqsIn,IqsMid,PGoals,
                  [\+ PGoal,solve(TailGoals,IqsMid,IqsOut)|PGoalsRest]),
  compile_body(GD,[],[],IqsMid,_,PGoalsList,[]),
  goal_list_to_seq(PGoalsList,PGoal).
compile_body((Desc1 =@ Desc2),ContGoals,TailGoals,IqsIn,IqsOut,
             PGoals,PGoalsRest):-
  !,compile_cont(ContGoals,IqsIn,IqsMid,PGoals,PGoalsMid),
  compile_desc(Desc1,Tag1-bot,IqsMid,IqsMid2,PGoalsMid,PGoalsMid2),
  compile_desc(Desc2,Tag2-bot,IqsMid2,IqsMid3,PGoalsMid2,
               [deref(Tag1,bot,DTag1,DSVs1),
                deref(Tag2,bot,DTag2,DSVs2),
                extensionalise_list([DTag1-DSVs1,DTag2-DSVs2],IqsMid3),
                check_inequal(IqsMid3,IqsMid4),
                deref(DTag1,DSVs1,Tag1Out,_),
                deref(DTag2,DSVs2,Tag2Out,_),
                (Tag1Out == Tag2Out),
                solve(TailGoals,IqsMid4,IqsOut)|PGoalsRest]).
compile_body(!,Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  !, compile_cont(Cont,IqsIn,IqsMid,PGoals,
                  [!,solve(TailGoals,IqsMid,IqsOut)|PGoalsRest]).
compile_body(true,Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  !, conc(Cont,TailGoals,NewGoals),
  compile_cont(NewGoals,IqsIn,IqsOut,PGoals,PGoalsRest).
compile_body(prolog(Goal),ContGoals,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest) :-
  !,compile_cont(ContGoals,IqsIn,IqsMid,PGoals,
               [Goal,solve(TailGoals,IqsMid,IqsOut)|PGoalsRest]).
compile_body(AtGD,Cont,TailGoals,IqsIn,IqsOut,PGoals,PGoalsRest):-
  conc(Cont,[AtGoal|TailGoals],[FirstGoal|RestGoals]),
  AtGD =.. [Rel|ArgDescs],
  compile_descs_fresh(ArgDescs,Args,IqsIn,IqsMid,PGoals,
                      [solve(FirstGoal,RestGoals,IqsMid,IqsOut)|PGoalsRest]),
  AtGoal =.. [Rel|Args].

% ------------------------------------------------------------------------------
% compile_cont(Gs:<goals>,IqsIn:<ineq>s,IqsOut:<ineq>s,PGoals:<prolog_goals>,
%              PGoalsRest:<prolog_goals>)
% ------------------------------------------------------------------------------
% instantiates diff list PGoals-PGoalsRest of Prolog goals to appropriate
% solve/1, solve/2 or nothing condition for solving Gs; calls solve/1 on vars
% ------------------------------------------------------------------------------
compile_cont(VarGs,IqsIn,IqsOut,[solve(VarGs,IqsIn,IqsOut)|PGoals],PGoals):-
  var(VarGs), !.
compile_cont([],Iqs,Iqs,PGoals,PGoals).
compile_cont([G|Gs],IqsIn,IqsOut,[solve(G,Gs,IqsIn,IqsOut)|PGoals],PGoals).

% ------------------------------------------------------------------------------
% goal_list_to_seq(Goals:<goal>s, GoalsSeq:<goal_seq>)
% ------------------------------------------------------------------------------
%
% ------------------------------------------------------------------------------
goal_list_to_seq([],true).
goal_list_to_seq([true|Gs],GsSeq):-
  !, goal_list_to_seq(Gs,GsSeq).
goal_list_to_seq([G],G):-!.
goal_list_to_seq([G|Gs],(G,GsSeq)):-
  goal_list_to_seq(Gs,GsSeq).
  
% ------------------------------------------------------------------------------
% compile_descs(Descs,Vs,IqsIn,IqsOut,Goals,GoalsRest)
% ------------------------------------------------------------------------------
% compiles descriptions Descs to constraint Vs into diff list Goals-GoalsRest
% ------------------------------------------------------------------------------
compile_descs([],[],Iqs,Iqs,Goals,Goals).
compile_descs([ArgDesc|ArgDescs],[Arg|Args],IqsIn,IqsOut,
              SubGoals,SubGoalsRest):-
  compile_desc(ArgDesc,Arg,IqsIn,IqsMid,SubGoals,SubGoalsMid),
  compile_descs(ArgDescs,Args,IqsMid,IqsOut,SubGoalsMid,SubGoalsRest).

% ------------------------------------------------------------------------------
% compile_descs_fresh(Descs,Vs,IqsIn,IqsOut,Goals,GoalsRest)
% ------------------------------------------------------------------------------
% similar to compile_descs, except that Vs are instantiated to Ref-bot
% before compiling Descs
% ------------------------------------------------------------------------------
compile_descs_fresh([],[],Iqs,Iqs,Goals,Goals).
compile_descs_fresh([ArgDesc|ArgDescs],[Ref-bot|Args],IqsIn,IqsOut,
                    SubGoals,SubGoalsRest):-
  compile_desc(ArgDesc,Ref-bot,IqsIn,IqsMid,SubGoals,SubGoalsMid),
  compile_descs_fresh(ArgDescs,Args,IqsMid,IqsOut,SubGoalsMid,SubGoalsRest).


% ==============================================================================
% Phrase Structure Rule Compiler
% ==============================================================================

:-dynamic curr_lex_rule_depth/1.
curr_lex_rule_depth(2).

% ------------------------------------------------------------------------------
% lex_rule_depth(N:<int>)
% ------------------------------------------------------------------------------
% asserts curr_lex_rule_depth/1 to N -- controls lexical rule depth
% ------------------------------------------------------------------------------
lex_rule_depth(N):-
  retractall(curr_lex_rule_depth(_)),
  assert(curr_lex_rule_depth(N)).

% ------------------------------------------------------------------------------
% lex(Word:<word>, Tag:<var_tag>, SVs:<svs>, IqsOut:<ineq>s)               mh(0)
% ------------------------------------------------------------------------------
% Word has category Tag-SVs
% ------------------------------------------------------------------------------
(lex(Word,Tag,SVs,IqsOut) if_h) :-
  (WordStart ---> Desc),
       [unsatisfiable,lexical,entry,for,WordStart] if_error
            (\+ add_to(Desc,_,bot,[],_)),
  add_to(Desc,TagStart,bot,[],IqsMid),
  curr_lex_rule_depth(Max),
  lex_close(0,Max,WordStart,TagStart,bot,Word,TagMid,SVsMid,IqsMid,IqsMid2),  
  fully_deref_prune(TagMid,SVsMid,Tag,SVs,IqsMid2,IqsOut).

% ------------------------------------------------------------------------------
% lex_close(WordIn:<word>,TagIn:<var_tag>, SVsIn:<svs>,
%           WordOut:<word>,TagOut:<var_tag>, SVsOut:<svs>, IqsIn:<ineq>s,
%           IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% If WordIn has category TagIn-SVsIn, then WordOut has category
% TagOut-SVsOut;  computed by closing under lexical rules
% ------------------------------------------------------------------------------
lex_close(_,_,Word,Tag,SVs,Word,Tag,SVs,Iqs,Iqs).
lex_close(N,Max,WordIn,TagIn,SVsIn,WordOut,TagOut,SVsOut,IqsIn,IqsOut):-
  current_predicate(lex_rule,lex_rule(_,_,_,_,_,_,_,_)),
  N < Max,
  lex_rule(WordIn,TagIn,SVsIn,WordMid,TagMid,SVsMid,IqsIn,IqsMid),
  NPlus1 is N + 1,
  lex_close(NPlus1,Max,WordMid,TagMid,SVsMid,WordOut,TagOut,SVsOut,IqsMid,
            IqsOut).

% ------------------------------------------------------------------------------
% empty_cat(Tag:<var_tag>, SVs:<svs>, Iqs:<ineq>s)                         mh(0)
% ------------------------------------------------------------------------------
empty_cat(_,_,_) if_h [fail] :-
  \+ current_predicate(empty,empty(_)),
  !.
empty_cat(TagOut,SVsOut,IqsOut) if_h []:-
  empty(Desc),
  add_to(Desc,Tag,bot,[],IqsIn),
%  curr_lex_rule_depth(Max),             % should we be closing empty cat's
%  lex_close(0,Max,e,Tag,bot,_,TagMid,SVsMid,IqsIn,IqsMid), % under lex. rules?
  fully_deref_prune(Tag,bot,TagOut,SVsOut,IqsIn,IqsOut).

% ------------------------------------------------------------------------------
% rule(<Tag:<var_tag>, SVs:<svs>, Iqs:<ineq>s, Left:<int>, Right:<int>,
%           N:<int>)                                                       mh(0)
% ------------------------------------------------------------------------------
% adds the result of any rule of which Tag-SVs from Left to Right
% might be the first element and the rest of the categories are in the chart
% ------------------------------------------------------------------------------
rule(Tag,SVs,Iqs,Left,Right,N) if_h SubGoals :-
  (RuleName rule Mother ===> Daughters),
  compile_dtrs(Daughters,Tag,SVs,Iqs,Left,Right,N,SubGoals,[],Mother,RuleName).

% ------------------------------------------------------------------------------
% compile_dtrs(Dtrs,Tag,SVs,Iqs,Left,Right,N,PGoals,PGoalsRest,Mother,RuleName)
% ------------------------------------------------------------------------------
% compiles description Dtrs to apply rule to first category Tag-SVs,
% at position Left-Right in chart, producing a list of Prolog goals
% diff list PGoals-PGoalsRest;  Mother is result produced
% ------------------------------------------------------------------------------
compile_dtrs((cat> Dtr,Rest),Tag,SVs,IqsIn,Left,Right,N,PGoals,PGoalsRest,
             Mother,RuleName):-
  !, compile_desc(Dtr,Tag-SVs,IqsIn,IqsMid,PGoals,
                  [check_inequal(IqsMid,IqsOut)|PGoalsMid]),
  compile_dtrs_rest(Rest,Left,Right,IqsOut,PGoalsMid,PGoalsRest,Mother,
                    [N|DtrsRest],DtrsRest,RuleName).
compile_dtrs((sem_head> Dtr,Rest),Tag,SVs,IqsIn,Left,Right,N,PGoals,PGoalsRest,
             Mother,RuleName):-
  !, compile_desc(Dtr,Tag-SVs,IqsIn,IqsMid,PGoals,
                  [check_inequal(IqsMid,IqsOut)|PGoalsMid]),
  compile_dtrs_rest(Rest,Left,Right,IqsOut,PGoalsMid,PGoalsRest,Mother,
                    [N|DtrsRest],DtrsRest,RuleName).
compile_dtrs((cats> Dtrs,Rest),Tag,SVs,IqsIn,Left,Right,N,PGoals,PGoalsRest,
             Mother,RuleName) :-
  !,compile_desc(Dtrs,Tag2-bot,IqsIn,IqsMid,PGoals,
       [check_inequal(IqsMid,IqsMid2),
        deref(Tag2,bot,_,DescSVs),
        DescSVs =.. [Sort|Vs], 
        ((Sort == e_list) ->
          PGoal_elist
        ; (match_list(Sort,Vs,Tag,SVs,Right,N,RuleDtrs,DtrsRest,NextRight,
                     IqsMid2,IqsOut),  % a_ correctly causes error
           PGoal_nelist))|PGoalsRest]), 
  compile_dtrs_rest(Rest,Left,NextRight,IqsOut,PGoalsMid_nelist,[],
               Mother,RuleDtrs,DtrsRest,RuleName),
  compile_dtrs(Rest,Tag,SVs,IqsMid2,Left,Right,N,PGoalsMid_elist,[],
               Mother,RuleName),
  goal_list_to_seq(PGoalsMid_nelist,PGoal_nelist),
  goal_list_to_seq(PGoalsMid_elist,PGoal_elist).
compile_dtrs((goal> Goal,Rest),Tag,SVs,IqsIn,Left,Right,N,PGoals,PGoalsRest,
             Mother,RuleName):-
  !, compile_body(Goal,[],[],IqsIn,IqsMid,PGoals,PGoalsMid),
  compile_dtrs(Rest,Tag,SVs,IqsMid,Left,Right,N,PGoalsMid,PGoalsRest,
               Mother,RuleName).
compile_dtrs((sem_goal> Goal,Rest),Tag,SVs,IqsIn,Left,Right,N,PGoals,PGoalsRest,
             Mother,RuleName):-
  !, compile_body(Goal,[],[],IqsIn,IqsMid,PGoals,PGoalsMid),
  compile_dtrs(Rest,Tag,SVs,IqsMid,Left,Right,N,PGoalsMid,PGoalsRest,
               Mother,RuleName).
compile_dtrs((cat> Dtr),Tag,SVs,IqsIn,Left,Right,N,PGoals,PGoalsRest,Mother,
             RuleName):-
  !, compile_desc(Dtr,Tag-SVs,IqsIn,IqsMid,PGoals,
                  [check_inequal(IqsMid,IqsMid2)|PGoalsMid]),
  compile_desc(Mother,Tag2-bot,IqsMid2,IqsOut,PGoalsMid,
               [add_edge_deref(Left,Right,Tag2,bot,IqsOut,[N],RuleName)|
                PGoalsRest]).
compile_dtrs((sem_head> Dtr),Tag,SVs,IqsIn,Left,Right,N,PGoals,PGoalsRest,
	     Mother,RuleName):-
  !, compile_desc(Dtr,Tag-SVs,IqsIn,IqsMid,PGoals,
                  [check_inequal(IqsMid,IqsMid2)|PGoalsMid]),
  compile_desc(Mother,Tag2-bot,IqsMid2,IqsOut,PGoalsMid,
               [add_edge_deref(Left,Right,Tag2,bot,IqsOut,[N],RuleName)|
                PGoalsRest]).
% don't check inequations after mother since add_edge_deref does that
compile_dtrs((cats> Dtrs),Tag,SVs,IqsIn,Left,Right,N,PGoals,PGoalsRest,
             Mother,RuleName) :-
  !,compile_desc(Dtrs,Tag3-bot,IqsIn,IqsMid,PGoals,
      [check_inequal(IqsMid,IqsMid2),
       deref(Tag3,bot,_,DescSVs),
       DescSVs =.. [Sort|Vs], 
       ((Sort == e_list) ->
         fail
       ; (match_list(Sort,Vs,Tag,SVs,Right,N,RuleDtrs,[],NextRight,
                     IqsMid2,IqsMid3),
          PGoal))|PGoalsRest]),                            % a_ correctly
  compile_desc(Mother,Tag2-bot,IqsMid3,IqsOut,PGoalsMid,   %  causes error
          [add_edge_deref(Left,NextRight,Tag2,bot,IqsOut,RuleDtrs,RuleName)]),
  goal_list_to_seq(PGoalsMid,PGoal).
compile_dtrs(Foo,_,_,_,_,_,_,_,_,_,_):-
  !,       [invalid,line,Foo,in,rule] if_error
              true,
  fail.

% ------------------------------------------------------------------------------
% compile_dtrs_rest(Dtrs,Left,Right,IqsMid,PGoals,PGoalsRest,Mother,
%                   PrevDtrs,DtrsRest,RuleName)
% ------------------------------------------------------------------------------
% same as compile_dtrs, only after first category on RHS of rule is
% found;  thus looks for an edge/4 if a cat> or cats> spec is found
% ------------------------------------------------------------------------------
compile_dtrs_rest((cat> Dtr,Rest),Left,Right,IqsMid,
                  [edge(N,Right,NewRight,Tag,SVs,EdgeIqs,_,_)|PGoals],
                  PGoalsRest,Mother,PrevDtrs,[N|DtrsRest],RuleName):-
  !,compile_desc(Dtr,Tag-SVs,IqsMid,IqsMid2,PGoals,
                 [conc(IqsMid2,EdgeIqs,IqsMid3),
                  check_inequal(IqsMid3,IqsOut)|PGoalsMid]),
  compile_dtrs_rest(Rest,Left,NewRight,IqsOut,PGoalsMid,PGoalsRest,Mother,
                    PrevDtrs,DtrsRest,RuleName).
compile_dtrs_rest((sem_head> Dtr,Rest),Left,Right,IqsMid,
                  [edge(N,Right,NewRight,Tag,SVs,EdgeIqs,_,_)|PGoals],
                  PGoalsRest,Mother,PrevDtrs,[N|DtrsRest],RuleName):-
  !,compile_desc(Dtr,Tag-SVs,IqsMid,IqsMid2,PGoals,
                 [conc(IqsMid2,EdgeIqs,IqsMid3),
                  check_inequal(IqsMid3,IqsOut)|PGoalsMid]),
  compile_dtrs_rest(Rest,Left,NewRight,IqsOut,PGoalsMid,PGoalsRest,Mother,
                    PrevDtrs,DtrsRest,RuleName).
compile_dtrs_rest((cats> Dtrs,Rest),Left,Right,IqsMid,PGoals,PGoalsRest,
                  Mother,PrevDtrs,DtrsRest,RuleName) :-
  !,compile_desc(Dtrs,Tag-bot,IqsMid,IqsMid2,PGoals,
                               [check_inequal(IqsMid2,IqsMid3),
                                                deref(Tag,bot,_,SVs),
                                                SVs =.. [Sort|Vs],
     match_list_rest(Sort,Vs,Right,NewRight,DtrsRest,DtrsRest2,IqsMid3,IqsOut)|
                                                PGoalsMid]),% a_ causes error
  compile_dtrs_rest(Rest,Left,NewRight,IqsOut,PGoalsMid,PGoalsRest,Mother,
                    PrevDtrs,DtrsRest2,RuleName).
compile_dtrs_rest((goal> Goal,Rest),Left,Right,IqsMid,PGoals,PGoalsRest,
                  Mother,PrevDtrs,DtrsRest,RuleName):-
  !, compile_body(Goal,[],[],IqsMid,IqsMid2,PGoals,PGoalsMid),
  compile_dtrs_rest(Rest,Left,Right,IqsMid2,PGoalsMid,PGoalsRest,Mother,
                    PrevDtrs,DtrsRest,RuleName).
compile_dtrs_rest((sem_goal> Goal,Rest),Left,Right,IqsMid,PGoals,PGoalsRest,
                  Mother,PrevDtrs,DtrsRest,RuleName):-
  !, compile_body(Goal,[],[],IqsMid,IqsMid2,PGoals,PGoalsMid),
  compile_dtrs_rest(Rest,Left,Right,IqsMid2,PGoalsMid,PGoalsRest,Mother,
                    PrevDtrs,DtrsRest,RuleName).
compile_dtrs_rest((cat> Dtr),Left,Right,IqsMid,
                  [edge(N,Right,NewRight,Tag,SVs,EdgeIqs,_,_)|PGoals],
                  PGoalsRest,Mother,PrevDtrs,[N],RuleName):-
  !,compile_desc(Dtr,Tag-SVs,IqsMid,IqsMid2,PGoals,
                 [conc(IqsMid2,EdgeIqs,IqsMid3),
                  check_inequal(IqsMid3,IqsMid4)|PGoalsMid]),
  compile_desc(Mother,Tag2-bot,IqsMid4,IqsOut,PGoalsMid,
               [add_edge_deref(Left,NewRight,Tag2,bot,IqsOut,
                               PrevDtrs,RuleName)|PGoalsRest]).
compile_dtrs_rest((sem_head> Dtr),Left,Right,IqsMid,
                  [edge(N,Right,NewRight,Tag,SVs,EdgeIqs,_,_)|PGoals],
                  PGoalsRest,Mother,PrevDtrs,[N],RuleName):-
  !,compile_desc(Dtr,Tag-SVs,IqsMid,IqsMid2,PGoals,
                 [conc(IqsMid2,EdgeIqs,IqsMid3),
                  check_inequal(IqsMid3,IqsMid4)|PGoalsMid]),
  compile_desc(Mother,Tag2-bot,IqsMid4,IqsOut,PGoalsMid,
               [add_edge_deref(Left,NewRight,Tag2,bot,IqsOut,
                               PrevDtrs,RuleName)|PGoalsRest]).
% don't check inequations after mother since add_edge_deref does that
compile_dtrs_rest((cats> Dtrs),Left,Right,IqsMid,PGoals,PGoalsRest,
                  Mother,PrevDtrs,DtrsRest,RuleName) :-
  !,compile_desc(Dtrs,Tag-bot,IqsMid,IqsMid2,PGoals,
                              [check_inequal(IqsMid2,IqsMid3),
                                              deref(Tag,bot,_,SVs),
                                              SVs =.. [Sort|Vs],
    match_list_rest(Sort,Vs,Right,NewRight,DtrsRest,[],IqsMid3,IqsMid4)|
                                              PGoalsMid]),% a_ causes error
  compile_desc(Mother,Tag2-bot,IqsMid4,IqsOut,PGoalsMid,
               [add_edge_deref(Left,NewRight,Tag2,bot,IqsOut,
                               PrevDtrs,RuleName)|PGoalsRest]).
% don't check inequations after mother since add_edge_deref does that
compile_dtrs_rest((goal> Goal),Left,Right,IqsMid,PGoals,PGoalsRest,Mother,
                  PrevDtrs,[],RuleName):-
  !, compile_body(Goal,[],[],IqsMid,IqsMid2,PGoals,PGoalsMid),
  compile_desc(Mother,Tag2-bot,IqsMid2,IqsOut,PGoalsMid,
               [add_edge_deref(Left,Right,Tag2,bot,IqsOut,
                               PrevDtrs,RuleName)|PGoalsRest]).
% don't check inequations after mother since add_edge_deref does that
compile_dtrs_rest((sem_goal> Goal),Left,Right,IqsMid,PGoals,PGoalsRest,Mother,
                  PrevDtrs,[],RuleName):-
  !, compile_body(Goal,[],[],IqsMid,IqsMid2,PGoals,PGoalsMid),
  compile_desc(Mother,Tag2-bot,IqsMid2,IqsOut,PGoalsMid,
               [add_edge_deref(Left,Right,Tag2,bot,IqsOut,
                               PrevDtrs,RuleName)|PGoalsRest]).
% don't check inequations after mother since add_edge_deref does that
compile_dtrs_rest(Foo,_,_,_,_,_,_,_,_,_):-
       [invalid,line,Foo,in,rule] if_error
            true,
  !, fail.

% ------------------------------------------------------------------------------
% compile_desc(Desc:<desc>, FS:<fs>, IqsIn:<ineq>s, IqsOut:<ineq>s, 
%              Goals:<goal>s, GoalsRest:<goal>s)
% ------------------------------------------------------------------------------
% Goals are the Prolog goals required to add the description Desc
% to the feature structure FS.  IqsIn and IqsOut are uninstantiated at
% compile time.
% ------------------------------------------------------------------------------
compile_desc(Tag1-bot,Tag2-SVs2,IqsIn,IqsOut,
             [ud(Tag1-bot,Tag2-SVs2,IqsIn,IqsOut)|GoalsRest],GoalsRest):-
  !.  % this instantiates variable first arguments
compile_desc([],FS,IqsIn,IqsOut,Goals,GoalsRest):-
  !, compile_desc(e_list,FS,IqsIn,IqsOut,Goals,GoalsRest).
compile_desc([H|T],FS,IqsIn,IqsOut,Goals,GoalsRest):-
  !, compile_desc((hd:H,tl:T),FS,IqsIn,IqsOut,Goals,GoalsRest).
compile_desc(Path1 == Path2,FS,IqsIn,IqsOut,Goals,GoalsRest):-
  !, compile_pathval(Path1,FS,FSatPath1,IqsIn,IqsMid,Goals,GoalsMid),
  compile_pathval(Path2,FS,FSatPath2,IqsMid,IqsMid2,
                  GoalsMid,[ud(FSatPath1,FSatPath2,IqsMid2,IqsOut)|GoalsRest]).
compile_desc(=\= Desc,Tag-SVs,IqsIn,IqsOut,Goals,GoalsRest) :-
  !,compile_desc(Desc,Tag2-bot,IqsIn,IqsMid,Goals,
      [check_inequal_conjunct(ineq(Tag,SVs,Tag2,bot,done),IqOut,Result),
       ((Result = succeed) -> IqsOut = IqsMid
       ;IqOut \== done, IqsOut = [IqOut|IqsMid])
      |GoalsRest]).
compile_desc(Feat:Desc,FS,IqsIn,IqsOut,[Goal|GoalsMid],GoalsRest):-
  !,     [description,uses,unintroduced,feature,Feat] if_error
              (\+ approp(Feat,_,_)),
  cat_atoms('featval_',Feat,Rel),
  Goal =.. [Rel,FS,FSatFeat,IqsIn,IqsMid],
  compile_desc(Desc,FSatFeat,IqsMid,IqsOut,GoalsMid,GoalsRest).
compile_desc((Desc1,Desc2),FS,IqsIn,IqsOut,Goals,GoalsRest):-
  !, compile_desc(Desc1,FS,IqsIn,IqsMid,Goals,GoalsMid),
  compile_desc(Desc2,FS,IqsMid,IqsOut,GoalsMid,GoalsRest).
compile_desc((Desc1;Desc2),FS,IqsIn,IqsOut,
             [(Goals1Seq;Goals2Seq)|GoalsRest],GoalsRest):-
  !, compile_desc(Desc1,FS,IqsIn,IqsOut,Goals1,[]),
  compile_desc(Desc2,FS,IqsIn,IqsOut,Goals2,[]),
  make_seq(Goals1,Goals1Seq), 
  make_seq(Goals2,Goals2Seq).
compile_desc(@ MacroName,FS,IqsIn,IqsOut,Goals,GoalsRest):-
  !,      [undefined,macro,MacroName,used,in,description] if_error
               (\+ (MacroName macro Desc)),
  (MacroName macro Desc),
  compile_desc(Desc,FS,IqsIn,IqsOut,Goals,GoalsRest).
compile_desc(a_ X,FS,IqsIn,IqsOut,[Goal|GoalsRest],GoalsRest) :-
  !, Goal =.. ['add_to_type_a_',FS,IqsIn,IqsOut,X].
compile_desc(Fun,FS,IqsIn,IqsOut,Goals,GoalsRest):-
  fun(Fun),
  !,compile_fun(Fun,FS,IqsIn,IqsOut,Goals,GoalsRest).
compile_desc(Type,FS,IqsIn,IqsOut,[Goal|GoalsRest],GoalsRest):-
       [undefined,type,Type,used,in,description] if_error
            (\+ type(Type)),
  type(Type),
  cat_atoms('add_to_type_',Type,AddtotypeType),
  Goal =.. [AddtotypeType,FS,IqsIn,IqsOut].

% ------------------------------------------------------------------------------
% compile_pathval(Path:<path>,FSIn:<fs>,FSOut:<fs>,
%                 IqsIn:<ineq>s,IqsOut:<ineq>s,
%                 Goals:<goal>s, GoalsRest:<goal>s)
% ------------------------------------------------------------------------------
% Goals-GoalsRest is difference list of goals needed to determine that
% FSOut is the (undereferenced) value of dereferenced FSIn at Path;
% might instantiate Tag or substructures in SVs in finding path value
% ------------------------------------------------------------------------------
compile_pathval([],FS,FS,Iqs,Iqs,Goals,Goals) :- !.
compile_pathval([Feat|Feats],FS,FSAtPath,IqsIn,IqsOut,
                [Goal|GoalsMid],GoalsRest):-
  !,   [undefined,feature,Feat,used,in,path,[Feat|Feats]] if_error
            (\+ approp(Feat,_,_)),
  cat_atoms('featval_',Feat,Rel),
  Goal =.. [Rel,FS,FSAtFeat,IqsIn,IqsMid],
  compile_pathval(Feats,FSAtFeat,FSAtPath,IqsMid,IqsOut,GoalsMid,GoalsRest).
compile_pathval(P,_,_,_,_,_,_) :-
  error_msg((nl,write('pathval: illegal path specified - '),
                write(P))).

% compile_fun(Fun:<fun>,FS:<fs>,IqsIn:<ineq>s,IqsOut:<ineq>s,
%             Goals:<goal>s,GoalsRest:<goal>s)
% ------------------------------------------------------------------------------
% Goals-RoalsRest is difference list of goals needed to determine that FS
%  satisfies functional constraint Fun
% ------------------------------------------------------------------------------
compile_fun(FunDesc,FS,IqsIn,IqsOut,Goals,GoalsRest) :-
  FunDesc =.. [Rel|ArgDescs],
  compile_descs_fresh(ArgDescs,Args,IqsIn,IqsMid,Goals,
                      [fsolve(Fun,FS,IqsMid,IqsOut)|GoalsRest]),
  Fun =.. [Rel|Args].


% ==============================================================================
% Compiler
% ==============================================================================

% ------------------------------------------------------------------------------
% reload
% ------------------------------------------------------------------------------
% reloads previously compiled files
% ------------------------------------------------------------------------------

reload(File) :-
  compile(File),
  reload.

reload:-
  compile(['.sub_type',
           '.unify_type',
           '.approp',
           '.extensional',
           '.iso_sub_seq',
           '.check_sub_seq',
           '.ucons',
           '.add_to_typecons',
           '.add_to_type',
           '.add_to_type3',
           '.featval',
           '.featval4',
           '.u',
           '.empty_cat',
           '.lex',
           '.rule',
           '.fun',
           '.fsolve',
           '.solve']).

% ------------------------------------------------------------------------------
% compile_gram(File:<file>)
% ------------------------------------------------------------------------------
% compiles grammar from File;  all commands set up same way, with optional
% argument for file, which is recompiled, if necessary
% ------------------------------------------------------------------------------
compile_gram(File):-
  abolish_preds,
  consult(File),
  compile_gram.

abolish_preds :-
  abolish((empty)/1), abolish((rule)/2), abolish((lex_rule)/2), 
  abolish((lex_rule)/8), abolish(('--->')/2), abolish((sub)/2), 
  abolish((if)/2), abolish((macro)/2), 
  abolish((ext)/1), abolish((cons)/2), abolish((approp)/3), 
  abolish((iso_sub_seq)/3), abolish((check_sub_seq)/5), 
  abolish((extensional)/1), abolish((unify_type)/3),
  abolish((sub_type)/2), abolish((ucons)/7), abolish((add_to_typecons)/6),
  abolish((add_to_type)/5), abolish((add_to_type3)/3), abolish((featval)/6),
  abolish((intro)/2),
  abolish((featval4)/4), abolish((u)/6), abolish((lex)/4), 
  abolish((lexicon)/1), abolish((node)/11), abolish((branch)/12), 
  abolish((empty_cat)/3), abolish((rule)/6),
  abolish((chain_rule)/10), abolish((non_chain_rule)/10), abolish((chained)/6),
  abolish((semantics)/1), abolish((generate)/6), abolish((solve)/4), 
  abolish((fsolve)/4), abolish((fun)/1), abolish(('+++>')/2).

compile_gram:-
  compile_sig,
  compile_fun,
  compile_cons,
  compile_logic,
  compile_dcs,
  compile_grammar.

compile_sig(File):-
  abolish((sub)/2),abolish((approp)/3),abolish((ext)/1),
  abolish((extensional)/1),
  abolish((iso_sub_seq)/3),abolish((check_sub_seq)/5),abolish((unify_type)/3),
  abolish((sub_type)/2),abolish((intro)/2),
  consult(File),
  compile_sig.

compile_sig:-
  compile_sub_type,
  compile_unify_type,
  compile_approp,
  compile_extensional. % now includes compile_iso and compile_check

compile_sub_type(File):-
  abolish((sub)/2),abolish((intro)/2),abolish((sub_type)/2),
  consult(File),
  compile_sub_type.

compile_sub_type:-
  retractall(_ sub_def _),
  ([no,types,defined] if_warning_else_fail
    (\+current_predicate(sub,_ sub _),
     \+current_predicate(intro,_ intro _))
  ; (current_predicate(sub,_ sub _) ->
           [S,subsumes,bot] if_error
             (S sub Ss, 
              (member(bot,Ss)   % fails if Ss = _ intro _
              ; Ss = (Ts intro _),
                member(bot,Ts))),
           [subtype/feature,specification,given,for,'a_/1',atom] if_error
                ( (a_ _) sub _ ),
           ['a_/1',atom,declared,subsumed,by,type,Type] if_error
                ( immed_subtypes(Type,SubTypes),
                  member(a_ _,SubTypes) ),
           [Type,multiply,defined] if_error
                ( bagof(S,Subs^(S sub Subs),Types),
                  duplicated(Type,Types) ),
           [illegal,variable,occurence,in,Type,sub,SubTypes,intro,FRs] if_error
              (Type sub SubTypes intro FRs,
               (var(Type)
               ;member(SubType,SubTypes),
                var(SubType)
               ;member(F:R,FRs),
                (var(F)
                ;var(R)))), % R can be a variable if parametric types are added
           [illegal,variable,occurence,in,Type,sub,SubTypes] if_error
              (Type sub SubTypes,
               \+(SubTypes = (_ intro _)),
               (var(Type)
               ;member(SubType,SubTypes),
                var(SubType)))
           ; true),
    (current_predicate(intro,_ intro _) ->
           [illegal,variable,occurence,in,Type,intro,FRs] if_error
              (Type intro FRs,
               (var(Type)
               ;member(F:R,FRs),
                (var(F)
                ;var(R))))  % R can be a variable if parametric types added
           ; true),
  ensure_sub_intro,
  maximal_defaults,
  bottom_defaults,
           [unary,branch,from,Type,to,SubType] if_warning
                immed_subtypes(Type,[SubType]),
  multi_hash(1,(sub_type)/2)).

maximal_defaults :-
  _ sub Xs,
  (Xs = (SubTypes intro _) ->
     member(SubType,SubTypes)
    ;member(SubType,Xs)),
 \+SubType subs _,
  ttynl,write_list([assuming,SubType,is,a,maximal,type]),
  assert(SubType sub_def []),
  fail.
maximal_defaults :-
  IType intro _,
  \+IType subs _,
  ttynl,write_list([assuming,IType,is,a,maximal,type]),
  assert(IType sub_def []),
  fail.
maximal_defaults.

bottom_defaults :-
  setof(Type,(type(Type),
              \+imm_sub_type(_,Type),
              Type \== bot,
              \+Type = (a_ _)),BDTypes),
  !,ttynl,
  write_list([assuming,the,'type(s):']),
  nl,write_list(BDTypes),
  nl,write_list([are,immediately,subsumed,by,bottom]),nl,
  (bot sub Xs ->
   (Xs = (BotTypes intro BotIntros) ->    % bottom declared with intro
     conc(BDTypes,BotTypes,NewBotTypes),
     assert(bot sub_def NewBotTypes intro BotIntros)
   ;conc(BDTypes,Xs,NewBotTypes),       % bottom declared w/o intro
    assert(bot sub_def NewBotTypes))
  ;assert(bot sub_def BDTypes)).        % bottom not declared
bottom_defaults :-    
   (bot subs _) -> true       % bot declared and no other types necessary
 ; assert(bot sub_def []).    % bot not declared and no other types necessary

ensure_sub_intro :-
 (\+current_predicate(sub,(_ sub _)) -> assertz((_ sub _ :- fail)) ; true),
 (\+current_predicate(intro,(_ intro _)) -> assertz((_ intro _ :- fail)) 
  ; true).

compile_unify_type:-
  multi_hash(1,(unify_type)/3).

compile_approp:-
  [bot,has,appropriate,features] if_error
        (bot sub _ intro [_:_|_]),
  [no,features,introduced] if_warning
        (\+ (_ sub _ intro [_:_|_]),
         \+ (_ intro [_:_|_])),
  [multiple,specification,for,F,in,declaration,of,S] if_error
            ( S sub _ intro FRs,
              duplicated(F:_,FRs)
            ; S intro FRs2,
              duplicated(F:_,FRs2)),
  [multiple,feature,specifications,for,type,S] if_error
       (S sub _ intro _,
        S intro _
       ;bagof(IType,FRs^(IType intro FRs),ITypes),
        duplicated(S,ITypes)),             % multiple sub/2 taken care of above
  [atom,'a_',X,is,ground,in,declaration,of,S] if_warning
            ( ( S sub _ intro FRs
              ; S intro FRs),
              member((_:(a_ X)),FRs),
              ground(X)),
  multi_hash(1,(approp)/3),
         [appropriateness,cycle,following,path,Fs,from,type,S] if_error
              ( type(S), feat_cycle(S,Fs) ),   
         [homomorphism,condition,fails,for,F,in,S1,and,S2] if_warning
              ( approp(F,S1,T1), approp(F,S2,T2),
                unify_type(S1,S2,S3),
                approp(F,S3,T3),
                unify_type(T1,T2,T1UnifyT2),
                \+sub_type(T3,T1UnifyT2)). % must check with sub_type because 
                                           %   of atoms
compile_extensional(File) :-
  abolish((ext)/1),abolish((extensional)/1),abolish((iso_sub_seq)/3),
  abolish((check_sub_seq)/5),
  consult(File),
  compile_extensional.

compile_extensional :-
 tell('.extensional.pl'),
 write('% COMPILED FILE: .extensional.pl '),nl,
 write('% ----------------------------------- '),nl,
 ((\+current_predicate(ext,ext(_))
    ; ext([])),
  !
 ;(ext(Exts),
   compile_ext_act(Exts))),
 write('extensional(a_ _).'),nl,
 nl,told,
 compile('.extensional.pl'),
 compile_iso,
 compile_check.

compile_ext_act([]).
compile_ext_act([a_ _|Exts]) :-
  !,compile_ext_act(Exts).
compile_ext_act([E|Exts]) :-
  [extensional,type,E,is,not,maximal] if_error
    (sub_type(E,S),
     S \== E),
  write('extensional('),write(E),write(').'),nl,
  compile_ext_act(Exts).

compile_iso :-
  multi_hash(0,(iso_sub_seq)/3).

compile_check :-
  multi_hash(0,(check_sub_seq)/5).

compile_cons :-
            [bot,has,constraints] if_error
                 (current_predicate(cons,(_ cons _)),( bot cons _ )),
            [constraint,declaration,given,for,atom] if_error
                 (current_predicate(cons,(_ cons _)),( (a_ _) cons _ )),
  ['=@',accessible,by,procedural,attachment,calls,from,constraint,for,Type]
            if_warning (current_predicate(cons,(_ cons _)),
                        current_predicate(if,(_ if _)),
                        find_xeqs([],EGs),
                        Type cons _ goal Gs,
                        find_xeq_act(Gs,EGs)),
  compile_ucons,
  compile_add_to_typecons.

compile_cons(File) :-
  abolish((cons)/2),abolish((ucons)/7),abolish((add_to_typecons)/6),
  consult(File),
  compile_cons.

find_xeqs(Accum,EGs) :-
  findall(EG,find_xeq(Accum,EG),NewAccum,Accum),
  find_xeqs_act(NewAccum,Accum,EGs).

find_xeqs_act(EGs,EGs,EGs) :- !.
find_xeqs_act(NewAccum,_,EGs) :-
  find_xeqs(NewAccum,EGs).

find_xeq(Accum,G/N) :-
  (Head if Body),
  functor(Head,G,N),
  \+member(G/N,Accum),
  find_xeq_act(Body,Accum).

find_xeq_act(=@(_,_),_) :- !.
find_xeq_act((G1,_),Accum) :-
  find_xeq_act(G1,Accum),
  !.
find_xeq_act((_,G2),Accum) :-
  find_xeq_act(G2,Accum),
  !.
find_xeq_act((G1;_),Accum) :-
  find_xeq_act(G1,Accum),
  !.
find_xeq_act((_;G2),Accum) :-
  find_xeq_act(G2,Accum),
  !.
find_xeq_act((\+ G),Accum) :-
  find_xeq_act(G,Accum),
  !.
find_xeq_act(At,Accum) :-
  functor(At,AG,AN),
  member(AG/AN,Accum).


compile_logic:-
  compile_add_to_type,
  compile_featval,
  compile_u.

compile_add_to_type:-
  multi_hash(1,(add_to_type)/5),
  compile_add_to_type3.
 
compile_add_to_type3:-
  tell('.add_to_type3.pl'),
  Type subs _,
  cat_atoms('add_to_type_',Type,Rel),
  Goal =.. [Rel,FS,IqsIn,IqsOut],
  Goal2 =.. [Rel,SVs,Tag,IqsIn,IqsOut],
  write_clause(Goal,[deref(FS,Tag,SVs),Goal2],0),
  fail.
compile_add_to_type3 :-
  Goal =.. ['add_to_type_a_',FS,IqsIn,IqsOut,X],      % multi_hash puts X there
  Goal2 =.. ['add_to_type_a_',SVs,Tag,IqsIn,IqsOut,X], 
  write_clause(Goal,[deref(FS,Tag,SVs),Goal2],0),
  fail.
compile_add_to_type3:-
  nl, told,
  compile('.add_to_type3.pl').

compile_featval:-
  ( \+ (_ sub _ intro _),
    \+ (_ intro _), !
  ; multi_hash(1,(featval)/6),
    compile_featval4
  ).

compile_featval4:-
  tell('.featval4.pl'),
  setof(F,Type^Subs^FRs^R^((Type subs Subs intro FRs),
                               member(F:R,FRs)),
        Feats),
  member(Feat,Feats),
  cat_atoms('featval_',Feat,Rel),
  Goal =.. [Rel,FS,FSOut,IqsIn,IqsOut],
  Goal2 =.. [Rel,SVs,Tag,FSOut,IqsIn,IqsOut],
  write_clause(Goal,[deref(FS,Tag,SVs),Goal2],0),
  fail.
compile_featval4:-
  setof(F,Type^FRs^R^((Type intro FRs),
                       member(F:R,FRs)),
        Feats),
  member(Feat,Feats),
  cat_atoms('featval_',Feat,Rel),
  Goal =.. [Rel,FS,FSOut,IqsIn,IqsOut],
  Goal2 =.. [Rel,SVs,Tag,FSOut,IqsIn,IqsOut],
  write_clause(Goal,[deref(FS,Tag,SVs),Goal2],0),
  fail.
compile_featval4:-
  nl, told,
  compile('.featval4.pl').

compile_ucons :-
  multi_hash(1,(ucons)/7).    % should this be a 2?

compile_add_to_typecons :-
  multi_hash(1,(add_to_typecons)/6).  % this should definitely be 1

compile_u:-
  multi_hash(1,(u)/6).

compile_grammar(File):-
  abolish((empty)/1), abolish((empty_cat)/3),abolish((rule)/2),
  abolish((lex_rule)/2),
  abolish((lex_rule)/8), abolish(('--->')/2), abolish((lex)/4),
  abolish((lexicon)/1),
  abolish((node)/11), abolish((branch)/12), abolish((rule)/6), 
  abolish((chain_rule)/10),abolish((non_chain_rule)/10), abolish((chained)/6),
  abolish((semantics)/1), abolish((generate)/6),
  consult(File),
  compile_grammar.

compile_grammar:-
  compile_lex_rules,
  compile_lex,
  compile_empty,
  compile_rules,
  compile_generate.

compile_lex_rules(File):-
  abolish((lex_rule)/2), abolish((lex_rule)/8),
  consult(File),
  compile_lex_rules.

compile_lex_rules:-
  parsing ->
  ( [no,lexical,rules,found] if_warning_else_fail
        (\+ current_predicate(lex_rule,lex_rule(_,_))),
    !
  ; [lexical,rule,RuleName,lacks,morphs,specification] if_error
      ((RuleName lex_rule _ **> _ if _)
      ;(RuleName lex_rule _ **> _)),
    multi_hash(0,(lex_rule)/8)
  ) ; true.  

compile_lex(File):-
  abolish(('--->')/2), abolish((lex)/4), abolish((lexicon)/1),
  abolish((node)/11), abolish((branch)/12),
  consult(File),
  compile_lex.

compile_lex:-
  secret_noadderrs,
  (parsing ->
  ( [no,lexicon,found] if_warning_else_fail
      (\+ current_predicate('--->',(_ ---> _))),
    !
  ; multi_hash(0,(lex)/4),
    [lexical,description,for,W,is,unsatisfiable]
       if_warning ((W ---> _), \+lex(W,_,_,_))) ; true),
  (generating ->
  ([no,semantics,specification,found] if_warning_else_fail
     (\+ current_predicate(semantics,semantics(_))), !
  ; semantics(Pred), Goal =.. [Pred,_,_],
    [no,Pred,definite,clause,found] if_warning_else_fail
      (\+ (current_predicate(if,(_ if _)), (Goal if _))), !
  ; build_tree(Tree),
    assert(lexicon(Tree)),
    multi_hash(1,(node)/11),
    multi_hash(1,(branch)/12)) ; true),
  secret_adderrs.

compile_empty(File):-
  abolish((empty_cat)/3),abolish((empty)/1),
  consult(File),
  compile_empty.

compile_empty:-
  secret_noadderrs,
  (parsing -> multi_hash(0,(empty_cat)/3) ; true),
  secret_adderrs.
 
compile_rules(File):-
  abolish((rule)/2), abolish((rule)/6),
  abolish((chain_rule)/10), abolish((non_chain_rule)/10),abolish((chained)/6), 
  consult(File),
  compile_rules.

compile_rules:-
  ( [no,phrase,structure,rules,found] if_warning_else_fail
         (\+ current_predicate(rule,rule(_,_))),
    !
 ; [rule,RuleName,has,no,'cat>','cats>',or,'sem_head>',specification]
      if_error ((RuleName rule _ ===> Body),
                \+ cat_member(Body),
                \+ cats_member(Body),
	        \+ sem_head_member(Body)),
    [rule,RuleName,has,multiple,'sem_head>',specifications]
      if_error ((RuleName rule _ ===> Body),
	        multiple_heads(Body)),
    [rule,RuleName,has,wrongly,placed,'sem_goal>',specifications]
      if_error ((RuleName rule _ ===> Body),
                bad_sem_goal(Body)),
    (parsing -> multi_hash(0,(rule)/6) ; true),
  (generating ->
  (secret_noadderrs,
    ( [no,chain,rules,found] if_warning_else_fail
         (\+ ((_ rule _ ===> Body), split_dtrs(Body,_,_,_,_,_))), !
    ; multi_hash(0,(chain_rule)/10),
      multi_hash(0,(chained)/6)),
    ( [no,non_chain,rules,found] if_warning_else_fail
         (\+ ((_ rule _ ===> Body), \+ split_dtrs(Body,_,_,_,_,_)),
          \+ current_predicate(empty,empty(_)),
          \+ current_predicate('--->',(_ ---> _))), !
    ; multi_hash(0,(non_chain_rule)/10)),
  secret_adderrs) ; true)).

compile_generate(File) :-
  abolish((semantics)/1), abolish((generate)/6),
  consult(File),
  compile_generate.

compile_generate :-
  generating ->
  (  [no,semantics,specification,found] if_warning_else_fail
      (\+ current_predicate(semantics,semantics(_))), !
  ; semantics(Pred), Goal =.. [Pred,_,_],
    [no,Pred,definite,clause,found] if_warning_else_fail
      (\+ (current_predicate(if,(_ if _)), (Goal if _))), !
  ; multi_hash(0,(generate)/6)) ; true.

compile_dcs(File):-
  abolish((if)/2), abolish((solve)/4),
  consult(File),
  compile_dcs.

compile_dcs:-
  [no,definite,clauses,found] if_warning
    (\+ current_predicate(if,if(_,_))),
  multi_hash(0,(solve)/4).

compile_fun(File):-
  abolish(('+++>')/2),abolish((fsolve)/4),abolish((fun)/1),
  consult(File),
  compile_fun.

compile_fun:-
       [no,functional,descriptions,found] if_warning
           (\+ current_predicate(+++>,+++>(_,_))),
  tell('.fun.pl'),
  write('% COMPILED FILE: .fun.pl '),nl,
  write('%---------------------------- '),nl,
  ( \+ current_predicate(+++>,+++>(_,_)),
    write('fun(_) :- !,fail.'),nl,
    nl,told,
    compile('.fun.pl')
  ; setof(Functor/Arity,((F +++> _),
                         functor(F,Functor,Arity)),Functions),
    compile_fun_act(Functions),
    nl,told,
    compile('.fun.pl')),
    multi_hash(0,fsolve/4).

compile_fun_act([]).
compile_fun_act([(Functor/Arity)|Functions]) :-
  length(ArgList,Arity),
  Template =.. [Functor|ArgList],
  write('fun('),write(Template),write(').'),nl,
  compile_fun_act(Functions).

% ------------------------------------------------------------------------------
% cat_member(Dtrs)
% ------------------------------------------------------------------------------
% true if Dtrs has at least one category member
% ------------------------------------------------------------------------------
cat_member((cat> _)).
cat_member((cat> _, _)):-!.
cat_member((_,Body)):-
  cat_member(Body).

% ------------------------------------------------------------------------------
% sem_head_member(+Dtrs:<desc>s)
% ------------------------------------------------------------------------------
% true if Dtrs has at least one sem_head> member
% ------------------------------------------------------------------------------
sem_head_member((sem_head> _)).
sem_head_member((sem_head> _,_)):-!.
sem_head_member((_,Body)):-
  sem_head_member(Body).

% ------------------------------------------------------------------------------
% sem_goal_member(+Dtrs:<desc>s)
% ------------------------------------------------------------------------------
% true if Dtrs has at least one sem_goal> member
% ------------------------------------------------------------------------------
sem_goal_member((sem_goal> _)).
sem_goal_member((sem_goal> _,_)):-!.
sem_goal_member((_,Body)):-
  sem_goal_member(Body).

% ------------------------------------------------------------------------------
% cats_member(Dtrs)
% ------------------------------------------------------------------------------
% true if Dtrs has at least one cats member
% ------------------------------------------------------------------------------
cats_member((cats> _)).
cats_member((cats> _, _)):- !.  % doesn't check for cats> [] or elist!
cats_member((_,Body)):-
  cats_member(Body).

% ------------------------------------------------------------------------------
% multiple_heads(+Dtrs:<desc>s)
% ------------------------------------------------------------------------------
% checks whether Dtrs has multiple sem_head> members
% ------------------------------------------------------------------------------
multiple_heads((sem_head> _,Dtrs)) :- !,
  sem_head_member(Dtrs).
multiple_heads((_,Dtrs)) :-
  multiple_heads(Dtrs).

% ------------------------------------------------------------------------------
% bad_sem_goal(+Dtrs:<desc>s)
% ------------------------------------------------------------------------------
% checks whether Dtrs has wrongly placed sem_goal> members
% ------------------------------------------------------------------------------
bad_sem_goal(Dtrs) :-      % there's a sem_head
  split_dtrs(Dtrs,_,_,_,DtrsBefore,DtrsAfter), !,
  (sem_goal_member(DtrsBefore), !
  ;sem_goal_member(DtrsAfter)).
bad_sem_goal(Dtrs) :-      % there's no sem_head
  sem_goal_member(Dtrs).

% ------------------------------------------------------------------------------
% if_h(Goal:<goal>, SubGoals:<goal>s)                                      +user
% ------------------------------------------------------------------------------
% accounts for multi-hash goals with no subgoals given
% ------------------------------------------------------------------------------
Goal if_h [] :-
  Goal if_h.

% ------------------------------------------------------------------------------
% multi_hash(N:<int>, Fun/Arity:<fun_sym>/<int>)
% ------------------------------------------------------------------------------
% for each solution T1,...,TK of ?- G(T1,...,TK) if_h SubGoals. 
%   G(f1(X11,...,X1J1),V2,...,VK):-
%       G_f1(V2,...,VK,X11,...,X1J1).
%   ...
%   G_f1_f2_..._fN(TN+1,...,TK,X11,...,X1J1,X21,..,X2J2,...,XN1,..,XNJN):-
%     SubGoals.
% prints into and compiles from a file named Fun.pl
% order matters for clauses listed with if_b, but not with if_h
% clauses with if_b must have subgoals listed, even if empty (for order)
% ------------------------------------------------------------------------------
multi_hash(N,(Fun)/Arity):-
  cat_atoms(Fun,'.pl',FileNameTail),
  cat_atoms('.',FileNameTail,FileName),
  tell(FileName),
  write('% '), write('COMPILED FILE: '), write(FileName),
  nl, write('% ----------------------------------------------------------------------'), nl,
  length(Args,Arity),
  Goal =.. [Fun|Args],
  ( setof(sol(Args,SubGoals), if_h(Goal,SubGoals), Sols), 
    !
  ; bagof(sol(Args,SubGoals), if_b(Goal,SubGoals), Sols)
  ),
  mh(N,Sols,Fun,0),
  nl, told,
  compile(FileName).  
       % cat_atoms('rm ',Filename,RemoveFile), unix(shell(RemoveFile)). 

mh(0,Sols,Fun,Col):-
  !, mh_zero(Sols,Fun,Col).
mh(N,Sols,Fun,Col):-
  mh_nonzero(Sols,Fun,N,Col).

mh_zero([],_,_).
mh_zero([sol(Args,SubGoals)|Sols],Fun,Col):-
  write_soln(Args,SubGoals,Fun,Col),
  mh_zero(Sols,Fun,Col).

write_soln(Args,SubGoals,Fun,Col):-                                   % eval
  Goal =.. [Fun|Args],
  write_clause(Goal,SubGoals,Col).

mh_nonzero([],_,_,_).
mh_nonzero([sol(Args,SubGoals)],Fun,_,Col):-
  !, write_soln(Args,SubGoals,Fun,Col).
mh_nonzero([sol([Arg|Args],SubGoals)|Sols],Fun,N,Col):-
  nonvar(Arg), 
  Arg =.. [FunArg|ArgsArg],
  length(ArgsArg,Arity),
  ( Sols = [sol([Arg2|_],_)|_],
    nonvar(Arg2), Arg2 =.. [FunArg|ArgsArg2],
    same_length(ArgsArg,ArgsArg2),
    !, cat_atoms('_',FunArg,FunTail),
    cat_atoms(Fun,FunTail,FunNew),
    same_length(Args,OtherArgs),
    Goal =.. [Fun,Arg|OtherArgs],
    conc(OtherArgs,ArgsArg,ArgsNew), 
    SubGoal =.. [FunNew|ArgsNew],
    conc(Args,ArgsArg,ArgsOld),
    write_clause(Goal,[SubGoal],Col),
    NewCol is Col, % + 2,
    mh_arg(FunArg,Arity,Sols,[sol(ArgsOld,SubGoals)],Fun,FunNew,N,NewCol)
  ; write_soln([Arg|Args],SubGoals,Fun,Col),
    mh_nonzero(Sols,Fun,N,Col)
  ).

mh_arg(FunMatch,Arity,[sol([Arg|Args],SubGoals)|Sols],SolsSub,Fun,FunNew,
       N,Col):-
  Arg =.. [FunMatch|ArgsSub],
  !, length(ArgsSub,Arity),
  conc(Args,ArgsSub,ArgsNew),
  mh_arg(FunMatch,Arity,Sols,[sol(ArgsNew,SubGoals)|SolsSub],Fun,FunNew,N,Col).
mh_arg(_,_,Sols,SolsSub,Fun,FunNew,N,Col):-
  NMinusOne is N-1,
  NewCol is Col + 2,
  mh(NMinusOne,SolsSub,FunNew,NewCol),
  mh_nonzero(Sols,Fun,N,Col).

% ------------------------------------------------------------------------------
% write_clause(Head:<single_goal>, Goals:<single_goal>s, Column:<int>)
% ------------------------------------------------------------------------------
% writes clause with head Head and sequence Goals of subgoals
% ------------------------------------------------------------------------------
write_clause(Head,Body,Col):-
  \+ \+ ( lettervars_track(Head+Body),
          nl, tab(Col), write(Head), 
          write_clause_act(Body,Col) ).

write_clause_act([],_):-
  write('.').
write_clause_act([G|Gs],Col):-
  write((:-)), 
  write_clause_goals(Gs,G,Col).
  
write_clause_goals([],Goal,Col):-
  nl, NewCol is Col+2, tab(NewCol), write_goal(Goal,NewCol), write('.').
write_clause_goals([Goal2|Goals],Goal1,Col):-
  nl, NewCol is Col+2, tab(NewCol), write_goal(Goal1,NewCol), write(','),
  write_clause_goals(Goals,Goal2,Col).

write_goal(\+ Goal,Col):-
  !, write('\+ '), write('( '), NewCol is Col+5, write_goal(Goal,NewCol),
  nl, tab(Col), tab(3), write(')').
write_goal((Goal1;Goal2),Col):-
  !, write('( '), NewCol is Col + 2,
  write_goal(Goal1,NewCol),
  nl, tab(Col), write('; '),
  write_goal(Goal2,NewCol),
  nl, tab(Col), write(')').
write_goal((Goal1,Goal2),Col):-
  !, write_goal(Goal1,Col), write(','),
  nl, tab(Col), write_goal(Goal2,Col).
write_goal(Goal,_):-
  write(Goal).

% lettervars_track(Term:<term>)
% ------------------------------------------------------------------------------
% instantiates shared variables in Term to constants V1,V2,...; 
% instantiates unshared variables to constant '_'
% ------------------------------------------------------------------------------
lettervars_track(Term):-
  vars_of(Term,[],Vars),
  eliminate_single_vars(Vars,0).

% ------------------------------------------------------------------------------
% vars_of(Term:<term>, VarsIn:<var>s, VarsOut:<var>s)
% ------------------------------------------------------------------------------
% VarsOut is VarsIn appended to variables in Term
% ------------------------------------------------------------------------------
vars_of(Var,VarsIn,[Var|VarsIn]):-
  var(Var), !.
vars_of(Term,VarsIn,VarsOut):-
  Term =.. [_|Args],
  vars_of_list(Args,VarsIn,VarsOut).

vars_of_list([],VarsIn,VarsIn).
vars_of_list([Arg|Args],VarsIn,VarsOut):-
  vars_of(Arg,VarsIn,VarsMid),
  vars_of_list(Args,VarsMid,VarsOut).

% ------------------------------------------------------------------------------
% eliminate_single_vars(Vars:<var>s, N:<int>)
% ------------------------------------------------------------------------------
% multiple occurences in Vars are set to numbers beginning with N, while
% single occurences are instantiated to constant '_'
% ------------------------------------------------------------------------------
eliminate_single_vars([],_).
eliminate_single_vars([Var|Vars],N):-
    var(Var), 
    !,
    ( select_eq(Var,Vars,VarsLeft),
      !, cat_atoms('V',N,Var),
      M is N+1, 
      eliminate_single_vars(VarsLeft,M)
    ; Var = '_',
      eliminate_single_vars(Vars,N) 
    )
  ; eliminate_single_vars(Vars,N). 


% ==============================================================================
% Debugger / Top Level I/O
% ==============================================================================

% ------------------------------------------------------------------------------
% show_type(Type:<type>)
% ------------------------------------------------------------------------------
% Displays information about Type, including appropriate features, immediate
% subtypes, supertypes, and constraints.  Continues by allowing to browse 
% super or subtypes
% ------------------------------------------------------------------------------
show_type(Type):-
  nl,  write('TYPE: '), write(Type),
  immed_subtypes(Type,SubTypes),
  nl, write('SUBTYPES: '), write(SubTypes),
  ( setof(T,T2^(sub_type(T,Type),
                T \== Type,
                \+ (sub_type(T2,Type),
                    T2 \== Type, T2 \== T,
                    sub_type(T,T2))),SuperTypes),
    !
  ; SuperTypes = []
  ),
  nl, write('SUPERTYPES: '), write(SuperTypes),
  (\+current_predicate(cons,(_ cons _)),
   !, Cons = none
  ; Type cons Cons goal _, !
  ; Type cons Cons),
  nl, write('IMMEDIATE CONSTRAINT: '), write(Cons),
  add_to(Type,Tag,bot,[],IqsIn),
  deref(Tag,bot,Ref,SVs),
  extensionalise(Ref,SVs,IqsIn),
  check_inequal(IqsIn,IqsOut),
  nl, write('MOST GENERAL SATISFIER: '), 
  pp_fs(Ref-SVs,IqsOut,5).

% ------------------------------------------------------------------------------
% show_cons(Type:<type>)
%-------------------------------------------------------------------------------
show_cons(Type):-
  immed_cons(Type,Cons),
  nl, write('Immediate Constraint for type: '),write(Type),
  nl, write(Cons).

% ------------------------------------------------------------------------------
% mgsat(Desc:<desc>)
% ------------------------------------------------------------------------------
% prints out most general satisfiers of Desc
% ------------------------------------------------------------------------------
mgsat(Desc):-
   nl, write('MOST GENERAL SATISFIER OF: '), write(Desc), nl,
  \+ \+
  (add_to(Desc,Tag,bot,[],Iqs),
   deref(Tag,bot,Ref,SVs),
   extensionalise(Ref,SVs,Iqs),
   check_inequal(Iqs,CheckedIqs),
   pp_fs(Ref-SVs,CheckedIqs),
   nl, query_proceed).

% ------------------------------------------------------------------------------
% iso_desc(Desc1:<desc>, Desc2:<desc>)
% ------------------------------------------------------------------------------
% checks if Desc1 and Desc2 create extensionally identical structures
% ------------------------------------------------------------------------------
iso_desc(D1,D2):-
  add_to(D1,Tag1,bot,[],IqsMid),
  add_to(D2,Tag2,bot,IqsMid,_),
  iso(Tag1-bot,Tag2-bot).

% ------------------------------------------------------------------------------
% rec(Words:<word>s)
% ------------------------------------------------------------------------------
% basic predicate to parse Words;  prints out recognized categories
% one at a time
% ------------------------------------------------------------------------------
rec(Words):-
  nl, write('STRING: '),
  nl, number_display(Words,0), 
  ttynl, rec(Words,Tag,SVs,Iqs),
  nl, write('CATEGORY: '),nl, ttyflush, 
  pp_fs(Tag-SVs,Iqs), 
  nl, query_proceed.

% ------------------------------------------------------------------------------
% lex(Word:<word>)
% ------------------------------------------------------------------------------
% prints out all categories for Word, querying user in between
% ------------------------------------------------------------------------------
lex(Word):-
  lex(Word,Tag,SVs,IqsIn),
  nl, write('WORD: '), write(Word),
  nl, write('ENTRY: '),
  extensionalise(Tag,SVs,IqsIn),
  check_inequal(IqsIn,IqsOut),
  pp_fs(Tag-SVs,IqsOut), 
  nl, query_proceed.

% ------------------------------------------------------------------------------
% query(GoalDesc:<goal_desc>)
% ------------------------------------------------------------------------------
% given a goal description GoalDesc, finds most general satisfier of it
% and then calls it as a goal
% ------------------------------------------------------------------------------
query(GoalDesc):-
  \+ \+
  (nl, mg_sat_goal(GoalDesc,Goal,[],IqsMid),
   solve(Goal,[],IqsMid,IqsMid2), 
   Goal =.. [_|Args],
   deref_list(Args,ArgsOut),
   extensionalise_list(ArgsOut,IqsMid2),
   check_inequal(IqsMid2,IqsOut),
   duplicates_list(ArgsOut,IqsOut,[],_,[],_,0,_),
   pp_goal(Goal,[],VisMid,0),
   nl, pp_iqs(IqsOut,VisMid,_,0),
   nl, query_proceed).

% ------------------------------------------------------------------------------
% mg_sat_goal(GoalDesc,Goal,IqsIn,IqsOut)                                   eval
% ------------------------------------------------------------------------------
% Goal is most general satisfier of GoalDesc
% (also used for functional descriptions)
% ------------------------------------------------------------------------------
mg_sat_goal((GDesc1;GDesc2),(G1;G2),IqsIn,IqsOut):-  
  !, mg_sat_goal(GDesc1,G1,IqsIn,IqsMid),   
  mg_sat_goal(GDesc2,G2,IqsMid,IqsOut).
mg_sat_goal(!,!,Iqs,Iqs):-!.
mg_sat_goal((GDesc1,GDesc2),(G1,G2),IqsIn,IqsOut):-
  !, mg_sat_goal(GDesc1,G1,IqsIn,IqsMid),
  mg_sat_goal(GDesc2,G2,IqsMid,IqsOut).
mg_sat_goal(GoalDesc,Goal,IqsIn,IqsOut):-
  GoalDesc =.. [Rel|ArgDescs],
  mg_sat_list(ArgDescs,Args,IqsIn,IqsOut),
  Goal =.. [Rel|Args].

% ------------------------------------------------------------------------------
% mg_sat_list(GoalDescs,Goals,IqsIn,IqsOut)
% ------------------------------------------------------------------------------
% maps mg_sat_goal on GoalDescs
% ------------------------------------------------------------------------------
mg_sat_list([],[],Iqs,Iqs).
mg_sat_list([ArgDesc|ArgDescs],[Ref-bot|Args],IqsIn,IqsOut):-
  add_to(ArgDesc,Ref,bot,IqsIn,IqsMid),
  mg_sat_list(ArgDescs,Args,IqsMid,IqsOut).

% ------------------------------------------------------------------------------
% macro(MacroName:<name>)
% ------------------------------------------------------------------------------
% prints out possible instantiations of macro named MacroName
% ------------------------------------------------------------------------------
macro(MacroName):-
  MacroName = VarName,
  \+ \+
  ((VarName macro Desc),
   add_to(Desc,Tag,bot,[],IqsMid),
   mg_sat_goal(VarName,MacroSat,IqsMid,IqsMid2),
   MacroSat =.. [_|MacroArgs],
   deref_list([Tag-bot|MacroArgs],ArgsOut),
   extensionalise_list(ArgsOut,IqsMid2),
   check_inequal(IqsMid2,IqsMid3),
   duplicates_list(ArgsOut,IqsMid3,[],_,[],_,0,_),
   nl, write('MACRO: '), nl, tab(4), pp_goal(MacroSat,[],VisMid,4),
   nl, write('ABBREVIATES:'), nl, tab(4), pp_fs(Tag-bot,VisMid,VisOut,4),
   nl, pp_iqs(IqsMid3,VisOut,_,4),
   nl, query_proceed).

insert_vars(MacroName,VarName):-
  MacroName =.. [Rel|Args],
  insert_vars_list(Args,ArgsVars),
  VarName =.. [Rel|ArgsVars].

insert_vars_list([],[]).
insert_vars_list([X|Xs],[(_,X)|XsVar]):-
  insert_vars_list(Xs,XsVar).

% ------------------------------------------------------------------------------
% empty
% ------------------------------------------------------------------------------
% displays empty categories
% ------------------------------------------------------------------------------
empty:-
  empty_cat(Tag,SVs,IqsIn),
  extensionalise(Tag,SVs,IqsIn),
  check_inequal(IqsIn,IqsOut),
  nl, write('EMPTY CATEGORY: '), 
  pp_fs(Tag-SVs,IqsOut,4),
  nl, query_proceed.

% ------------------------------------------------------------------------------
% edge(N:<int>, M:<int>)
% ------------------------------------------------------------------------------
% prints out edges from N to M, querying user in between
% ------------------------------------------------------------------------------
edge(I) :-
  edge(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName),
  nl, write('COMPLETED CATEGORY SPANNING: '),
  write_out(M,N),
  nl, edge_act(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName).

edge(M,N):-
  nl, write('COMPLETED CATEGORIES SPANNING: '),
  write_out(M,N),
  nl, edge(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName),
  nl, edge_act(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName),
  fail.

% used to assert variables for Dtrs and RuleName to keep edge-size small
%edge_act(_,_,_,Tag,SVs,Iqs,_,_) :-
%  no_interpreter,
%  !,pp_fs(Tag-SVs,Iqs).
%edge_act(_,_,_,Tag,SVs,Iqs,Dtrs,_) :-
%  var(Dtrs),
%  !,pp_fs(Tag-SVs,Iqs),
%  nl,write('(Edge created while interpreter was inactive)'),nl.
edge_act(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName) :-
  length(Dtrs,ND),
  print_edgeout(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND).

print_edgeout(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nl,pp_fs(Tag-SVs,Iqs),
  nl,write('Edge created for category above: '),
  nl,write('     index: '),write(I),
  nl,write('      from: '),write(M),write(' to: '),write(N),
  nl,write('    string: '),write_out(M,N),
  nl,write('      rule:  '),write(RuleName),
  nl,write(' # of dtrs: '),write(ND),
  query_edgeout(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND).

query_edgeout(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nl,write('Action(retract,dtr-#,continue,abort)? '),
  nl,read(Response),
  query_edgeout_act(Response,I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND).

query_edgeout_act(retract,I,_,_,_,_,_,_,_,_) :-
  retract(edge(I,_,_,_,_,_,_,_)),   % index is all which is needed to match
  !.
query_edgeout_act(dtr-D,I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  nth_index(Dtrs,D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule),
  !,length(DDtrs,DND),
  print_dtr_edge(D,DI,DLeft,DRight,DTag,DSVs,DIqs,DDtrs,DRule,DND),
  print_edgeout(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND).
query_edgeout_act(continue,_,_,_,_,_,_,_,_,_) :-
  !.
query_edgeout_act(abort,_,_,_,_,_,_,_,_,_) :-
  !,abort.
query_edgeout_act(_,I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND) :-
  query_edgeout(I,M,N,Tag,SVs,Iqs,Dtrs,RuleName,ND).

write_out(M,N):-
  parsing(Ws),
  all_but_first(M,Ws,WsRest),
  K is N-M,
  write_first(K,WsRest).

all_but_first(0,Ws,Ws):-!.
all_but_first(M,[_|Ws],WsOut):-
  K is M-1,
  all_but_first(K,Ws,WsOut).

write_first(0,_):-!.
write_first(N,[W|Ws]):-
  write(W), write(' '),
  K is N-1,
  write_first(K,Ws).

% ------------------------------------------------------------------------------
% lexrule(RuleName:<name>)
% ------------------------------------------------------------------------------
% Displays lexical rule with name RuleName
% ------------------------------------------------------------------------------
lex_rule(RuleName):-
  \+ \+
  lexrule2(RuleName).

lexrule2(RuleName):-
  (( (RuleName lex_rule Desc1 **> Desc2 if Cond morphs Morphs)
   ; (RuleName lex_rule Desc1 **> Desc2 morphs Morphs),
     Cond = none
   ),
   nl, write('LEX RULE: '), write(RuleName), 
   add_to(Desc1,Tag1,bot,[],IqsMid),
   add_to(Desc2,Tag2,bot,IqsMid,IqsMid2),
   mg_sat_goal(Cond,Goal,IqsMid2,IqsMid3),
   Goal =.. [_Rel|Args],
   deref_list([Tag1-bot,Tag2-bot|Args],ArgsOut),
   extensionalise_list(ArgsOut,IqsMid3),
   check_inequal(IqsMid3,IqsMid4),
   duplicates_list(ArgsOut,IqsMid4,[],_,[],_,0,_),
   nl, write('INPUT CATEGORY: '), 
   nl, tab(4), pp_fs(Tag1-bot,[],VisMid1,4),
   nl, write('OUTPUT CATEGORY: '),
   nl, tab(4), pp_fs(Tag2-bot,VisMid1,VisMid2,4),
   ( Cond = none,
     VisMid3 = VisMid2,
     !
   ; nl, write('CONDITION: '), 
     nl, tab(4), pp_goal(Goal,VisMid2,VisMid3,4)
   ),
   nl, write('MORPHS: '),
   numbervars(Morphs,0,_),
   pp_morphs(Morphs),
   nl, pp_iqs(IqsMid4,VisMid3,_,4),
   nl, query_proceed).

pp_morphs((Morph,Morphs)):-
  !, nl, tab(4), pp_morph(Morph),
  pp_morphs(Morphs).
pp_morphs(Morph):-
  nl, tab(4), pp_morph(Morph).

pp_morph((P1 becomes P2)):-
  pp_patt(P1), write(' becomes '), pp_patt(P2).
pp_morph((P1 becomes P2 when Cond)):-
  pp_patt(P1), write(' becomes '), pp_patt(P2),
  nl, tab(8), write('when '), write(Cond).
  
pp_patt((X,Xs)):-
  !, pp_at_patt(X), write(','),
  pp_patt(Xs).
pp_patt(X):-
  pp_at_patt(X).

pp_at_patt(Atom):-
  atom(Atom),
  !, name(Atom,Codes),
  make_char_list(Codes,Chars),
  write(Chars).
pp_at_patt(List):-
  write(List).

% ------------------------------------------------------------------------------
% show_clause(PredSpec:<predspec>)
% ------------------------------------------------------------------------------
% Displays definite clauses in feature structure format
% ------------------------------------------------------------------------------
show_clause(Spec):-
  \+ \+ show_clause2(Spec).

show_clause2(Spec):-
  (( Spec = Name/Arity,
     !
   ; Spec = Name
   ),
   (Head if Body),
   Head =.. [Name|Args],
   length(Args,Arity),
   satisfy_dtrs_goal(Head,Cats,CatsRest,HeadGoal,[],IqsMid),
   satisfy_dtrs_goal(Body,CatsRest,[],BodyGoal,IqsMid,IqsMid2),
   deref_list(Cats,CatsOut),
   extensionalise_list(CatsOut,IqsMid2),
   check_inequal(IqsMid2,IqsMid3),
   duplicates_list(CatsOut,IqsMid3,[],_,[],_,0,_),
   nl, write('HEAD: '), pp_goal(HeadGoal,[],Vis,6),
   nl, write('BODY: '), pp_goal(BodyGoal,Vis,Vis2,6),
   nl, pp_iqs(IqsMid3,Vis2,_,6),
   nl, query_proceed).

% ------------------------------------------------------------------------------
% rule(RuleName:<name>)
% ------------------------------------------------------------------------------
% Displays rule with name RuleName
% ------------------------------------------------------------------------------
rule(RuleName):-
  \+ \+
  ((RuleName rule Moth ===> DtrsDesc),
  nl, write('RULE: '), write(RuleName),
  add_to(Moth,TagMoth,bot,[],IqsMid),
  satisfy_dtrs(DtrsDesc,DtrCats,[],Dtrs,IqsMid,IqsMid2),
  deref_list([TagMoth-bot|DtrCats],CatsOut),
  extensionalise_list(CatsOut,IqsMid2),
  check_inequal(IqsMid2,IqsMid3),
  duplicates_list(CatsOut,IqsMid3,[],_,[],_,0,_),
  nl, nl, write('MOTHER: '), nl, nl, tab(2), pp_fs(TagMoth-bot,[],VisMid,2),
  nl, nl, write('DAUGHTERS/GOALS: '),   
  show_rule_dtrs(Dtrs,VisMid,VisMid2),
  nl, pp_iqs(IqsMid3,VisMid2,_,2),
  nl, query_proceed).

show_rule_dtrs([],Vis,Vis).
show_rule_dtrs([(cat> C)|Dtrs],VisIn,VisOut):-
  nl, nl, write('CAT  '), pp_fs(C,VisIn,VisMid,5),
  show_rule_dtrs(Dtrs,VisMid,VisOut).
show_rule_dtrs([(sem_head> C)|Dtrs],VisIn,VisOut):-
  nl, nl, write('SEM_HEAD  '), pp_fs(C,VisIn,VisMid,10),
  show_rule_dtrs(Dtrs,VisMid,VisOut).
show_rule_dtrs([(cats> Cs)|Dtrs],VisIn,VisOut):-
  nl, nl, write('CATs '), pp_fs(Cs,VisIn,VisMid,5),
  show_rule_dtrs(Dtrs,VisMid,VisOut).
show_rule_dtrs([(goal> G)|Dtrs],VisIn,VisOut):-
  nl, nl, write('GOAL  '), pp_goal(G,VisIn,VisMid,6),
  show_rule_dtrs(Dtrs,VisMid,VisOut).
show_rule_dtrs([(sem_goal> G)|Dtrs],VisIn,VisOut):-
  nl, nl, write('SEM_GOAL  '), pp_goal(G,VisIn,VisMid,10),
  show_rule_dtrs(Dtrs,VisMid,VisOut).

pp_goal(Goal):-
  Goal =.. [_|Args],
  duplicates_list(Args,[],[],_,[],_,0,_),
  pp_goal(Goal,[],_,0).

pp_goal(\+ Goal,VisIn,VisOut,Col):-
  !, write('\+ '), write('( '), 
  NewCol is Col+5, pp_goal(Goal,VisIn,VisOut,NewCol),
  nl, tab(Col), tab(3), write(')').
pp_goal((Goal1;Goal2),VisIn,VisOut,Col):-
  !, write('( '), NewCol is Col + 2,
  pp_goal(Goal1,VisIn,VisMid,NewCol),
  nl, tab(Col), write('; '),
  pp_goal(Goal2,VisMid,VisOut,NewCol),
  nl, tab(Col), write(')').
pp_goal((Goal1,Goal2),VisIn,VisOut,Col):-
  !, pp_goal(Goal1,VisIn,VisMid,Col), write(','),
  nl, tab(Col), pp_goal(Goal2,VisMid,VisOut,Col).
pp_goal(prolog(Hook),Vis,Vis,_) :-
  !, write(prolog(Hook)).
pp_goal(Goal,VisIn,VisOut,Col):-
  Goal =.. [Rel|Args],
  write(Rel),
  ( Args = [],
    !,
    VisOut = VisIn
  ; write('('),
    name(Rel,Name),
    length(Name,N),
    NewCol is Col+N+1,
    pp_goal_args(Args,VisIn,VisOut,NewCol)
  ).

pp_goal_args([],Vis,Vis,_):-
  write(')').
pp_goal_args([Arg],VisIn,VisOut,Col):-
  !, pp_fs(Arg,VisIn,VisOut,Col), write(')').
pp_goal_args([Arg|Args],VisIn,VisOut,Col):-
  pp_fs(Arg,VisIn,VisMid,Col), write(','), nl, tab(Col),
  pp_goal_args(Args,VisMid,VisOut,Col).

satisfy_dtrs((cat> Desc),[Tag-bot|DtrCatsRest],DtrCatsRest,
             [(cat> Tag-bot)],IqsIn,IqsOut):-
  !, add_to(Desc,Tag,bot,IqsIn,IqsOut).
satisfy_dtrs((sem_head> Desc),[Tag-bot|DtrCatsRest],DtrCatsRest,
             [(sem_head> Tag-bot)],IqsIn,IqsOut):-
  !, add_to(Desc,Tag,bot,IqsIn,IqsOut).
satisfy_dtrs((cats> Descs),[Tag-bot|DtrCatsRest],DtrCatsRest,
             [(cats> Tag-bot)],IqsIn,IqsOut) :-
  !, add_to(Descs,Tag,bot,IqsIn,IqsOut).
satisfy_dtrs((goal> GoalDesc),DtrCats,DtrCatsRest,
             [(goal> Goal)],IqsIn,IqsOut):-
  !, satisfy_dtrs_goal(GoalDesc,DtrCats,DtrCatsRest,Goal,IqsIn,IqsOut).
satisfy_dtrs((sem_goal> GoalDesc),DtrCats,DtrCatsRest,
             [(sem_goal> Goal)],IqsIn,IqsOut):-
  !, satisfy_dtrs_goal(GoalDesc,DtrCats,DtrCatsRest,Goal,IqsIn,IqsOut).
satisfy_dtrs(((cat> Desc),Dtrs),[Tag-bot|DtrCatsMid],DtrCatsRest,
             [(cat> Tag-bot)|DtrsSats],IqsIn,IqsOut):-
  !, add_to(Desc,Tag,bot,IqsIn,IqsMid),
  satisfy_dtrs(Dtrs,DtrCatsMid,DtrCatsRest,DtrsSats,IqsMid,IqsOut).
satisfy_dtrs(((sem_head> Desc),Dtrs),[Tag-bot|DtrCatsMid],DtrCatsRest,
             [(sem_head> Tag-bot)|DtrsSats],IqsIn,IqsOut):-
  !, add_to(Desc,Tag,bot,IqsIn,IqsMid),
  satisfy_dtrs(Dtrs,DtrCatsMid,DtrCatsRest,DtrsSats,IqsMid,IqsOut).
satisfy_dtrs(((cats> Descs),Dtrs),[Tag-bot|DtrCatsMid],DtrCatsRest,
             [(cats> Tag-bot)|DtrsSats],IqsIn,IqsOut):-
  !, add_to(Descs,Tag,bot,IqsIn,IqsMid),
  satisfy_dtrs(Dtrs,DtrCatsMid,DtrCatsRest,DtrsSats,IqsMid,IqsOut).
satisfy_dtrs(((goal> GoalDesc),Dtrs),DtrCats,DtrCatsRest,
              [goal> Goal|DtrsSats],IqsIn,IqsOut):-
  satisfy_dtrs_goal(GoalDesc,DtrCats,DtrCatsMid,Goal,IqsIn,IqsMid),
  satisfy_dtrs(Dtrs,DtrCatsMid,DtrCatsRest,DtrsSats,IqsMid,IqsOut).
satisfy_dtrs(((sem_goal> GoalDesc),Dtrs),DtrCats,DtrCatsRest,
              [sem_goal> Goal|DtrsSats],IqsIn,IqsOut):-
  satisfy_dtrs_goal(GoalDesc,DtrCats,DtrCatsMid,Goal,IqsIn,IqsMid),
  satisfy_dtrs(Dtrs,DtrCatsMid,DtrCatsRest,DtrsSats,IqsMid,IqsOut).

satisfy_dtrs_goal((GD1,GD2),DtrCats,DtrCatsRest,
                  (G1,G2),IqsIn,IqsOut):-
  !, satisfy_dtrs_goal(GD1,DtrCats,DtrCatsMid,G1,IqsIn,IqsMid),
  satisfy_dtrs_goal(GD2,DtrCatsMid,DtrCatsRest,G2,IqsMid,IqsOut).
satisfy_dtrs_goal((GD1;GD2),DtrCats,DtrCatsRest,
                  (G1;G2),IqsIn,IqsOut):-
  !, satisfy_dtrs_goal(GD1,DtrCats,DtrCatsMid,G1,IqsIn,IqsMid),
  satisfy_dtrs_goal(GD2,DtrCatsMid,DtrCatsRest,G2,IqsMid,IqsOut).
satisfy_dtrs_goal((\+ GD1),DtrCats,DtrCatsRest,
                  (\+ G1),IqsIn,IqsOut):-
  !, satisfy_dtrs_goal(GD1,DtrCats,DtrCatsRest,G1,IqsIn,IqsOut).
satisfy_dtrs_goal(prolog(Hook),DtrCats,DtrCats,prolog(Hook),Iqs,Iqs) :-
  !.
satisfy_dtrs_goal(AtGD,DtrCats,DtrCatsRest,AtG,IqsIn,IqsOut):-
  AtGD =.. [Rel|ArgDescs],
  same_length(ArgDescs,Args),
  AtG =.. [Rel|Args],
  satisfy_dtrs_goal_args(ArgDescs,DtrCats,DtrCatsRest,Args,IqsIn,IqsOut).

satisfy_dtrs_goal_args([],DtrCats,DtrCats,[],Iqs,Iqs).
satisfy_dtrs_goal_args([D|Ds],[Tag-bot|DtrCats],DtrCatsRest,[Tag-bot|Args],
                       IqsIn,IqsOut):-
  add_to(D,Tag,bot,IqsIn,IqsMid),
  satisfy_dtrs_goal_args(Ds,DtrCats,DtrCatsRest,Args,IqsMid,IqsOut).
  

% ==============================================================================
% Pretty Printing
% ==============================================================================

% ------------------------------------------------------------------------------
% pp_fs(FS:<fs>,Iqs:<ineq>s)
% ------------------------------------------------------------------------------
% pretty prints FS with inequations Iqs
% ------------------------------------------------------------------------------
pp_fs(FS,Iqs):-
  \+ \+ ( duplicates(FS,Iqs,[],_,[],_,0,_),
          nl, 
          pp_fs(FS,[],VisOut,0),
          nl,
          pp_iqs(Iqs,VisOut,_,0)).

pp_fs(FS,Iqs,N):-
  \+ \+ ( duplicates(FS,Iqs,[],_,[],_,0,_),
          nl, 
          tab(N), pp_fs(FS,[],VisOut,N),
          nl,
          pp_iqs(Iqs,VisOut,_,N)).

% ------------------------------------------------------------------------------
% duplicates(FS:<fs>, Iqs:<ineq>s, DupsIn:<ref>s, DupsOut:<ref>s, 
%            VisIn:<ref>s, VisOut:<ref>s, NumIn:<int>, NumOut:<int>)
% ------------------------------------------------------------------------------
% DupsOut is the result of adding the duplicate references
% in FS and Iqs to those in DupsIn.  VisIn are those nodes already
% visited and VisOut are those visited in FS.  NumIn is
% the current number for variables and NumOut is the
% next available after numbering only the shared refs in FS.
% ------------------------------------------------------------------------------
duplicates(FS,Iqs,DupsIn,DupsOut,VisIn,VisOut,NumIn,NumOut) :-
  duplicates_fs(FS,DupsIn,DupsMid,VisIn,VisMid,NumIn,NumMid),
  duplicates_iqs(Iqs,DupsMid,DupsOut,VisMid,VisOut,NumMid,NumOut).
duplicates_fs(FS,DupsIn,DupsOut,VisIn,VisOut,NumIn,NumOut):-
  deref_pp(FS,Ref,SVs),
  ( member_eq(Ref,DupsIn), 
    !, DupsOut = DupsIn, VisOut = VisIn, NumOut = NumIn
  ; member_eq(Ref,VisIn), 
    !, DupsOut = [Ref|DupsIn], VisIn = VisOut, 
    Ref = NumIn, NumOut is NumIn + 1 
  ; SVs = a_ _,
    !,DupsIn = DupsOut, VisOut = [Ref|VisIn], NumOut = NumIn
  ; SVs =.. [_|Vs],
    duplicates_list(Vs,[],DupsIn,DupsOut,[Ref|VisIn],VisOut,NumIn,NumOut)
  ).

duplicates_iqs([],Dups,Dups,Vis,Vis,Num,Num).
duplicates_iqs([Iq|Iqs],DupsIn,DupsOut,VisIn,VisOut,NumIn,NumOut) :-
  duplicates_ineq(Iq,DupsIn,DupsMid,VisIn,VisMid,NumIn,NumMid),
  duplicates_iqs(Iqs,DupsMid,DupsOut,VisMid,VisOut,NumMid,NumOut).

duplicates_ineq(done,Dups,Dups,Vis,Vis,Num,Num).
duplicates_ineq(ineq(Tag1,SVs1,Tag2,SVs2,Ineqs),DupsIn,DupsOut,VisIn,VisOut,
                NumIn,NumOut):-
  duplicates_fs(Tag1-SVs1,DupsIn,DupsMid1,VisIn,VisMid1,NumIn,NumMid1),
  duplicates_fs(Tag2-SVs2,DupsMid1,DupsMid2,VisMid1,VisMid2,NumMid1,NumMid2),
  duplicates_ineq(Ineqs,DupsMid2,DupsOut,VisMid2,VisOut,NumMid2,NumOut).

duplicates_list([],Iqs,DupsIn,DupsOut,VisIn,VisOut,NumIn,NumOut) :-
  duplicates_iqs(Iqs,DupsIn,DupsOut,VisIn,VisOut,NumIn,NumOut).
duplicates_list([V|Vs],Iqs,DupsIn,DupsOut,VisIn,VisOut,NumIn,NumOut):-
  duplicates_fs(V,DupsIn,DupsMid,VisIn,VisMid,NumIn,NumMid),
  duplicates_list(Vs,Iqs,DupsMid,DupsOut,VisMid,VisOut,NumMid,NumOut).

% ------------------------------------------------------------------------------
% pp_iqs(Iqs:<ineq>s, VisIn:<var>s, VisOut:<var>s,Col:<int>)
% ------------------------------------------------------------------------------
% pretty-prints a list of inequations, indented Col columns
%-------------------------------------------------------------------------------
pp_iqs([],Vis,Vis,_).
pp_iqs([ineq(Tag1,SVs1,Tag2,SVs2,Ineqs)|Iqs],VisIn,VisOut,Col) :-
  (Ineqs = done,!
   ;write('(')),
  pp_ineq(ineq(Tag1,SVs1,Tag2,SVs2,Ineqs),VisIn,VisMid,Col),
  (Ineqs = done,!
   ;write(')')),
  (Iqs = [],
   !,nl
   ;write(','),
    nl,
    pp_iqs(Iqs,VisMid,VisOut,Col)).

pp_ineq(done,Vis,Vis,_).
pp_ineq(ineq(Tag1,SVs1,Tag2,SVs2,Ineqs),VisIn,VisOut,Col) :-
  tab(Col),pp_fs(Tag1-SVs1,VisIn,VisMid1,Col),
  write('  =\=  '),
  NewCol is Col+7,
  pp_fs(Tag2-SVs2,VisMid1,VisMid2,NewCol),
  nl,
  (Ineqs = done
   ;write(';')),
  pp_ineq(Ineqs,VisMid2,VisOut,Col).

% ------------------------------------------------------------------------------
% pp_fs(FS:<fs>,VisIn:<var>s, VisOut:<var>s, Col:<int>)
% ------------------------------------------------------------------------------
% prints FS where VisOut is the result of adding all of the
% referents of substructures in FS to VisIn
% Col is where printing begins for FS
% ------------------------------------------------------------------------------
pp_fs(FS,VisIn,VisOut,Col):-
  deref_pp(FS,Ref,SVs),
  ( var(Ref)                            % print ref if shared (nonvar)
  ; nonvar(Ref), write('['), write(Ref), write(']'),
    ( member_eq(Ref,VisIn), !
    ; write(' ')
    )
  ),
  ( member_eq(Ref,VisIn), !, VisOut = VisIn
  ; SVs = a_ X,
    !,(no_write_type_flag(a_ X)
       ,!
      ;write(a_ X)
      ),
    VisOut = [Ref|VisIn]
  ; SVs =.. [Type|Vs],              % print FS if not already visited
    approps(Type,FRs),
    ( no_write_type_flag(Type),
      !, pp_vs_unwritten(FRs,Vs,[Ref|VisIn],VisOut,Col)
    ; write(Type),   
      pp_vs(FRs,Vs,[Ref|VisIn],VisOut,Col) 
    )
  ).

:- dynamic no_write_type_flag/1.
:- dynamic no_write_feat_flag/1.

write_types:-
  write_type(_).

write_feats:-
  write_feat(_).

write_type(Type):-
  retractall(no_write_type_flag(Type)).

write_feat(Feat):-
  retractall(no_write_feat_flag(Feat)).

no_write_type(Type):-
  retractall(no_write_type_flag(Type)),
  assert(no_write_type_flag(Type)).

no_write_feat(Feat):-
  retractall(no_write_feat_flag(Feat)),
  assert(no_write_feat_flag(Feat)).

% ------------------------------------------------------------------------------
% deref_pp(FS1:<fs>, FS2:<d_fs>)
% ------------------------------------------------------------------------------
% FS2 is the result of dereferencing FS1 where Ref might
% be constant due to printing refs
% ------------------------------------------------------------------------------
deref_pp(Ref-SVs,RefOut,SVsOut):-
   nonvar(Ref),  \+ atomic(Ref),
   !, deref_pp(Ref,RefOut,SVsOut)
 ; RefOut = Ref, SVsOut = SVs.

% ------------------------------------------------------------------------------
% pp_vs(FRs:<fs>, Vs:<vs>, Dups:<var>s, 
%        VisIn:<var>s, VisOut:<var>s, Col:<int>)
% ------------------------------------------------------------------------------
% prints Vs at Col 
% ------------------------------------------------------------------------------
pp_vs([],[],Vis,Vis,_).
pp_vs([F:_|FRs],[V|Vs],VisIn,VisOut,Col):-
  ( no_write_feat_flag(F),
    VisMid = VisIn, !
  ; nl, tab(Col),
    write_feature(F,LengthF), 
    NewCol is Col + LengthF +1,
    pp_fs(V,VisIn,VisMid,NewCol)
  ),
  pp_vs(FRs,Vs,VisMid,VisOut,Col).

pp_vs_unwritten([],[],Vis,Vis,_).
pp_vs_unwritten([F:_|FRs],[V|Vs],VisIn,VisOut,Col):-
  ( no_write_feat_flag(F),
    VisMid = VisIn, !
  ; write_feature(F,LengthF), 
    NewCol is Col + LengthF +1,
    pp_fs(V,VisIn,VisMid,NewCol)
  ),
  pp_vs(FRs,Vs,VisMid,VisOut,Col).

write_feature(F,LengthF):-
  name(F,NameF),
  count_and_capitalize(NameF,0,LengthF),
  write(' ').

count_and_capitalize([],Length,Length).
count_and_capitalize([L|Ls],LengthIn,Length):-
  capitalize(L,LCap),
  write(LCap),
  LengthInPlus1 is LengthIn + 1,
  count_and_capitalize(Ls,LengthInPlus1,Length).

capitalize(X,XCap):-
  ( name(a,[Name_a]), name(z,[Name_z]),
    Name_a =< X, X =< Name_z,
    !, name('A',[Name_A]),  
    Gap is Name_A - Name_a,
    NameXCap is X + Gap,
    name(XCap,[NameXCap])
  ; name(XCap,[X])
  ).


% ==============================================================================
% Utilities
% ==============================================================================

% ------------------------------------------------------------------------------
% conc/3
% ------------------------------------------------------------------------------
conc([],L,L).
conc([H1|T1],L2,[H1|T3]):-
  conc(T1,L2,T3).

% ------------------------------------------------------------------------------
% cat_atoms/3
% ------------------------------------------------------------------------------
cat_atoms(A1,A2,A3):-
  name(A1,L1),
  name(A2,L2),
  conc(L1,L2,L3),
  name(A3,L3).

% ------------------------------------------------------------------------------
% esetof(X:Alpha, Goal:<goal>, Xs:<list(Alpha)>)
% ------------------------------------------------------------------------------
% setof returning empty list if no solutions
% ------------------------------------------------------------------------------
esetof(_,Goal,[]):-
    \+ Goal, !.
esetof(X,Goal,Xs):- 
  setof(X,Goal,Xs).

% ------------------------------------------------------------------------------
% make_seq(List:<list(<goal>)>,Seq:<seq(<goal>)>)
% ------------------------------------------------------------------------------
% makes List into a sequence of goals
% ------------------------------------------------------------------------------
make_seq([],true).
make_seq([X],X):-
  !.
make_seq([X|Xs],(X,XsSeq)):-
  make_seq(Xs,XsSeq).

% ------------------------------------------------------------------------------
% make_list(Seq:<seq(<goal>)>, List:<list(<goal>)>)
% ------------------------------------------------------------------------------
% makes Seq into list of goals
% ------------------------------------------------------------------------------
make_list(true,[]):-
  !.
make_list((X,XsSeq),[X|Xs]):-
  !, make_list(XsSeq,Xs).
make_list(X,[X]).

% ------------------------------------------------------------------------------
% member(X:<term>, Xs:<term>s)
% ------------------------------------------------------------------------------
% X is member of list Xs; avoids choicepoint for last element
% ------------------------------------------------------------------------------
member(Element, [Head|Tail]) :-
	member_(Tail, Head, Element).

member_(_, Element, Element).
member_([Head|Tail], _, Element) :-
	member_(Tail, Head, Element).

% ------------------------------------------------------------------------------
% member_eq(X:<term>, Xs:<term>s)
% ------------------------------------------------------------------------------
% X is strictly == equal to a member of list Xs
% ------------------------------------------------------------------------------
member_eq(X,[Y|Ys]):-
    X==Y
  ; member_eq(X,Ys).

% ------------------------------------------------------------------------------
% member_ref_eq(X:<term>, Xs:<term>s)
%-------------------------------------------------------------------------------
% Ref-_ belongs to SortDom
%-------------------------------------------------------------------------------
member_ref_eq(Ref,SortDom) :-   %exactly this reference belongs
  member(SRef-_,SortDom),
  Ref == SRef.

% ------------------------------------------------------------------------------
% select(X:<term>, Ys:<term>s, XsLeft:<term>s)
%-------------------------------------------------------------------------------
% X is a member of Ys, with XsLeft left over.  Only the first of duplicates
%  is matched.
%-------------------------------------------------------------------------------
select(X,[X|Ys],Ys) :- !.
select(X,[Y|Ys],[Y|XsLeft]) :-
  select(X,Ys,XsLeft).

% ------------------------------------------------------------------------------
% select_eq(X:<term>, Xs:<term>s, XsLeft:<term>s)
% ------------------------------------------------------------------------------
% X is strictly == equal to a member of list Xs with XsLeft left over
% ------------------------------------------------------------------------------
select_eq(X,[Y|Ys],Zs):-
    X==Y,
    Zs = Ys
  ; Zs = [Y|Zs2],
    select_eq(X,Ys,Zs2).

% ------------------------------------------------------------------------------
% same_length(Xs:<list>, Ys:<list>)
% ------------------------------------------------------------------------------
% checks that Xs and Ys are same length; instantiating if necessary
% ------------------------------------------------------------------------------
same_length([],[]).
same_length([_|Xs],[_|Ys]):-
  same_length(Xs,Ys).

% ------------------------------------------------------------------------------
% transitive_closure(Graph:<graph>, Closure:<graph>)
% ------------------------------------------------------------------------------
% Warshall's Algorithm (O'Keefe, Craft of Prolog, p. 172)
% Input: Graph = [V1-Vs1,...,VN-VsN]
%   describes the graph G = <Vertices, Edges> where
%      * Vertices = {V1,..,VN} and
%      * VsI = {VJ | VI -> VJ in Edges}
% Output: Closure is transitive closure of Graph in same form
% ------------------------------------------------------------------------------
transitive_closure(Graph,Closure):-
  warshall(Graph,Graph,Closure).

warshall([],Closure,Closure).
warshall([V-_|G],E,Closure):-
  memberchk(V-Y,E),
  warshall(E,V,Y,NewE),
  warshall(G,NewE,Closure).

warshall([],_,_,[]).
warshall([X-Neibs|G],V,Y,[X-NewNeibs|NewG]):-
  memberchk(V,Neibs),
  !, ord_union(Neibs,Y,NewNeibs),
  warshall(G,V,Y,NewG).
warshall([X-Neibs|G],V,Y,[X-Neibs|NewG]):-
  warshall(G,V,Y,NewG).

% ------------------------------------------------------------------------------
% memberchk(X:<term>, Xs:<term>s)
% ------------------------------------------------------------------------------
% deterministic unification of X with first consistent term in Xs
% ------------------------------------------------------------------------------
memberchk(A,[A|_]):-!.
memberchk(A,[_|Bs]):-
  memberchk(A,Bs).

% ------------------------------------------------------------------------------
% ord_union(Xs:<term>s, Ys:<term>s, Zs:<term>s)
% ------------------------------------------------------------------------------
% Xs and Ys are list of ground terms in standard order and Zs is their
% union in standard order.  
% ------------------------------------------------------------------------------
ord_union([],Xs,Xs).
ord_union([X|Xs],Ys,Zs):-
  ord_union2(Ys,X,Xs,Zs).

ord_union2([],X,Xs,[X|Xs]).
ord_union2([Y|Ys],X,Xs,Zs):-
  compare(Comp,X,Y),
  ord_union_act(Comp,X,Xs,Y,Ys,Zs).   

ord_union_act(<,X,Xs,Y,Ys,[X|Zs]):-
  ord_union2(Xs,Y,Ys,Zs).
ord_union_act(>,X,Xs,Y,Ys,[Y|Zs]):-
  ord_union2(Ys,X,Xs,Zs).
ord_union_act(=,X,Xs,_,Ys,[X|Zs]):-
  ord_union(Xs,Ys,Zs).

% ------------------------------------------------------------------------------
% reverse_count(ListIn:<list>,Acc:<list>,ListOut:<list>,
%               CountIn:<int>,CountOut:<int>)
% ------------------------------------------------------------------------------
% using accumulators, reverses ListIn into ListOut, with initial segment
% Acc;  CountIn is current count (of Acc) and CountOut is result;  call
% by:  reverse_count(ListIn,[],ListOut,0,Count)
% ------------------------------------------------------------------------------
reverse_count([],Xs,Xs,Count,Count).
reverse_count([X|Xs],Ys,Zs,CountIn,Count):-
  CountInPlus1 is CountIn+1,
  reverse_count(Xs,[X|Ys],Zs,CountInPlus1,Count).

% ------------------------------------------------------------------------------
% query_proceed
% ------------------------------------------------------------------------------
% prompts user for n. response, otherwise proceeds
% ------------------------------------------------------------------------------
query_proceed:-
  ttynl, write('ANOTHER?  '), ttyflush, read(n).

% ------------------------------------------------------------------------------
% number_display/2
% ------------------------------------------------------------------------------
number_display([W|Ws],N):-
  write(N), write(' '), write(W), write(' '),
  SN is N + 1,
  number_display(Ws,SN).
number_display([],M):-
  write(M).

% ------------------------------------------------------------------------------
% error_msg(Goal:<goal>)
% ------------------------------------------------------------------------------
% tells user, solves Goal, then goes back to old file being told
% ------------------------------------------------------------------------------
error_msg(Goal):-
  telling(FileName),
  tell(user),
  Goal,
  told,
  tell(FileName),
  fail.  

% ------------------------------------------------------------------------------
% if_error(Msg,Cond)
% ------------------------------------------------------------------------------
% if condition Cond holds, provides Msg as error message;  always succeeds
% ------------------------------------------------------------------------------
if_error(Msg,Cond):-
  telling(FileName),
  tell(user),
  ( Cond, 
    ttynl, 
    write_list(['  **ERROR: '|Msg]),
    ttynl, ttynl,
    fail
  ; told,
    tell(FileName)
  ).

% ------------------------------------------------------------------------------
% if_warning_else_fail(Msg,Cond)
% ------------------------------------------------------------------------------
% if Cond holds, provides warning message Msg, otherwise fails
% ------------------------------------------------------------------------------
if_warning_else_fail(Msg,Cond):-
  if_warning(Msg,Cond),
  Cond.

% ------------------------------------------------------------------------------
% if_warning(Msg,Cond)
% ------------------------------------------------------------------------------
% if condition Cond holds, prints out Msg;  always succeeds
% ------------------------------------------------------------------------------
if_warning(Msg,Cond):-
  telling(FileName),
  tell(user),
  ( Cond, 
    ttynl,
    write_list(['  *Warning: '|Msg]),
    ttynl,
    fail
  ; told,
    tell(FileName)
  ).

% ------------------------------------------------------------------------------
% write_list(Xs)
% ------------------------------------------------------------------------------
% writes out elements of Xs with spaces between elements
% ------------------------------------------------------------------------------
write_list([]).
write_list([X|Xs]):-
  write(X), write(' '), write_list(Xs).

% ------------------------------------------------------------------------------
% query_user(Query)
% ------------------------------------------------------------------------------
% writes Query and then tries to read a y. from user
% ------------------------------------------------------------------------------
query_user(QueryList):-
  ttynl, ttynl, write_list(QueryList),
  read(y).

% ------------------------------------------------------------------------------
% duplicated(X,Xs)
% ------------------------------------------------------------------------------
% holds if X occurs more than once in Xsd
% ------------------------------------------------------------------------------
duplicated(X,[X|Xs]):-
  member(X,Xs).
duplicated(X,[_|Xs]):-
  duplicated(X,Xs).

% ------------------------------------------------------------------------------
% feat_cycle(S:<type>, Fs:<path>)
% ------------------------------------------------------------------------------
% holds if following the path Fs in the appropriateness definitions
% leads from S to S.  calls an auxiliary function which avoids infinite
% loops and tracks the features so far followed in reverse with an accumulator
% ------------------------------------------------------------------------------
feat_cycle(S,Fs):-
  feat_cycle2(S,S,[S],[],Fs).

% ------------------------------------------------------------------------------
% feat_cycle2(S1:<type), S2:<type), Ss:<list(<type>)>, 
%             FsIn:<path>, FsOut:<path>)
% ------------------------------------------------------------------------------
% assumes following reverse of FsIn led to S2 from S1, visiting
% Ss along the way.  FsOut is the result of appending a path that will
% get from S2 back to S1 to the reverse of FsIn
% ------------------------------------------------------------------------------
feat_cycle2(S1,S2,_Ss,FsIn,FsOut):-
  approp(F,S2,S1),
  reverse([F|FsIn],FsOut).
feat_cycle2(S1,S2,Ss,FsIn,FsOut):-
  approp(F,S2,S3),
  \+ member(S3,Ss),
  feat_cycle2(S1,S3,[S2|Ss],[F|FsIn],FsOut).

% ------------------------------------------------------------------------------
% reverse(Xs:<list>,Ys:<list>)
% ------------------------------------------------------------------------------
% Ys is result of reversing Xs
% ------------------------------------------------------------------------------
reverse(Xs,Ys):-
  reverse3(Xs,[],Ys).

reverse3([],Xs,Xs).
reverse3([X|Xs],Ys,Zs):-
  reverse3(Xs,[X|Ys],Zs).


% ==============================================================================
% Generator
% ==============================================================================

% ------------------------------------------------------------------------------
% Interpreter
% ------------------------------------------------------------------------------

% ------------------------------------------------------------------------------
% gen_int(+Cat:<desc>)
% gen_int(+Tag:<tag>, +SVs:<svs>, +Iqs:<ineq>)
% ------------------------------------------------------------------------------
% top-level user calls to generate a sentence from a descriptor Cat
% or a FS specified by Tag, SVs, Iqs
% ------------------------------------------------------------------------------
gen_int(Cat) :-
  add_to(Cat,Tag,bot,[],Iqs),
  gen_int(Tag,bot,Iqs).

gen_int(Tag,SVs,Iqs) :-
  secret_noadderrs,
  nl, write('CATEGORY: '), nl, ttyflush,
  pp_fs(Tag-SVs,Iqs), nl,
  gen_int(Tag,SVs,Iqs,Words),
  nl, write('STRING: '),
  nl, write_list(Words),
  nl, query_proceed,
  secret_adderrs.

% ------------------------------------------------------------------------------
% gen_int(+Tag:<tag>, +SVs:<svs>, +IqsIn:<ineq>s, -Words:<word>s)
% ------------------------------------------------------------------------------
% top-level functional interface for the generator
% generates the list of Words from the semantic specification of Tag-SVs,Iqs
% ------------------------------------------------------------------------------
gen_int(Tag,SVs,IqsIn,Words) :-
  ( [no,semantics,specification,found] if_warning_else_fail
      (\+ current_predicate(semantics,semantics(_))), !
  ; semantics(Pred), Goal =.. [Pred,_,_],
    [no,Pred,definite,clause,found] if_warning_else_fail
      (\+ current_predicate(if,if(Goal,_))), !
  ; 
%fully_deref_prune(Tag,SVs,NewTag,NewSVs,IqsIn,IqsPrunned),
    gen_int(Tag,SVs,IqsIn,IqsOut,Words,[])),
    extensionalise(Tag,SVs,IqsOut),
    check_inequal(IqsOut,_).   


% ------------------------------------------------------------------------------
% gen_int(+Tag:<tag>, +SVs:<svs>, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%         -Words:<word>s, -RestWords:<word>s)
% ------------------------------------------------------------------------------
% recursively generates the difference list Words-RestWords from the root
% Tag-SVs,IqsIn
% ------------------------------------------------------------------------------
gen_int(Tag,SVs,IqsIn,IqsOut,Words,RestWords) :-
  semantics(Pred), GoalIndex =.. [Pred,Tag-SVs,IndexTag-bot],
  GoalPivot =.. [Pred,PivotTag-bot,IndexTag-bot],
  solve(GoalIndex,[GoalPivot],IqsIn,IqsGoal),
  non_chain_rule(IndexTag,bot,IqsGoal,IqsRule,Mother,Dtrs),
  deref(PivotTag,bot,DPivotTag,DPivotSVs),
  add_to(Mother,DPivotTag,DPivotSVs,IqsRule,IqsMother),
  check_inequal(IqsMother,IqsMotherCkd),
  chained_nodes(DPivotTag,DPivotSVs,Tag,SVs,IqsMotherCkd,IqsChained),
  gen_dtrs(Dtrs,IqsChained,IqsDtrs,NewWords,RestNewWords),
%  fully_deref_prune(DPivotTag,DPivotSVs,PPivotTag,PPivotSVs,IqsDtrs,IqsPrunned),
  conn(DPivotTag,DPivotSVs,Tag,SVs,IqsDtrs,IqsOut,
       NewWords,RestNewWords,Words,RestWords).

% ------------------------------------------------------------------------------
% non_chain_rule(+IndexTag:<tag>, +IndexSVs:<svs>,
%                +IqsIn:<ineq>s, -IqsOut:<ineq>s, -Mother:<desc>, -Dtrs:<desc>s)
% ------------------------------------------------------------------------------
% looks for non-chain rules Mother ===> Dtrs among lexical entries,
% empty categories and proper non-chain grammar rules
% ------------------------------------------------------------------------------
non_chain_rule(IndexTag,IndexSVs,IqsIn,IqsOut,Mother,(word>Word)) :-
  lexicon(null:Branches),
  gen_lex_branch(Branches,IndexTag-IndexSVs,IndexTag,IndexSVs,IqsIn,IqsOut,
                 Mother,Word).
non_chain_rule(_,_,Iqs,Iqs,Mother,empty) :-
  current_predicate(empty,empty(_)),
  empty(Mother).
non_chain_rule(_,_,Iqs,Iqs,Mother,Dtrs) :-
  (_RuleName rule Mother ===> Dtrs),
  \+ split_dtrs(Dtrs,_,_,_,_,_).

% ------------------------------------------------------------------------------
% gen_lex_branch(+Branches:<branch>s, +Value:<type>, +IndexTag:<tag>,
%                +IndexSVs:<svs>, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%                -Mother:<desc>, -Word:<word>
% ------------------------------------------------------------------------------
% navigates through a list of branches in the indexing tree
% ------------------------------------------------------------------------------
gen_lex_branch([Type/Subtree|_],ValueTag-ValueSVs,IndexTag,IndexSVs,
               IqsIn,IqsOut,Mother,Word) :-
  deref(ValueTag,ValueSVs,DValueTag,DValueSVs),
  add_to(Type,DValueTag,DValueSVs,IqsIn,IqsValue),
  gen_lex(Subtree,IndexTag,IndexSVs,IqsValue,IqsOut,Mother,Word).
gen_lex_branch([_|Trees],Value,IndexTag,IndexSVs,IqsIn,IqsOut,Mother,Word) :-
  gen_lex_branch(Trees,Value,IndexTag,IndexSVs,IqsIn,IqsOut,Mother,Word).

% ------------------------------------------------------------------------------
% gen_lex(+Tree:<tree>, +IndexTag:<tag>, +IndexSVs:<svs>,
%         +IqsIn:<ineq>s, -IqsOut:<ineq>s, -Mother:<desc>, Word:<word>)
% ------------------------------------------------------------------------------
% navigates through the indexing Tree to retrive all Word ---> Mother entries
% matching the PivotTag-PivotSVs FS through the semantic goal
% ------------------------------------------------------------------------------
gen_lex([Entry|Entries],_,_,IqsIn,IqsOut,Mother,Word) :-
  member_(Entries,Entry,(Mother/IqsOut-IqsIn,Word)).
gen_lex(Path:Branches,IndexTag,IndexSVs,IqsIn,IqsOut,Mother,Word) :-
  connect_path(Path,Value,Feat),
  deref(IndexTag,IndexSVs,DIndexTag,DIndexSVs),
  add_to(Feat,DIndexTag,DIndexSVs,IqsIn,IqsValue),
  gen_lex_branch(Branches,Value,IndexTag,IndexSVs,IqsValue,IqsOut,Mother,Word).

% ------------------------------------------------------------------------------
% conn(+PivotTag:<tag>, +PivotSVs:<svs>, +Tag:<tag>, +SVs:<svs>,
%      +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%      +NewWords:<word>s, +RestNewWords:<word>s,
%      -Words:<word>s, -RestWords:<word>s)
% ------------------------------------------------------------------------------
% connects bottom-up the PivotTag-PivotSVs FS to the root Tag-SVS FS
% and at the same time generates the difference-list Words-RestWords by 
% threading the given HeadWords-RestHeadWords
% ------------------------------------------------------------------------------
conn(PivotTag,PivotSVs,Tag,SVs,IqsIn,IqsOut,Words,RestWords,Words,RestWords) :-
  ud(PivotTag-PivotSVs,Tag-SVs,IqsIn,IqsOut).
%  u(PivotSVs,SVs,PivotTag,Tag,IqsIn,IqsOut).
conn(PivotTag,PivotSVs,Tag,SVs,IqsIn,IqsOut,
     HeadWords,RestHeadWords,Words,RestWords) :-
  chain_rule(IqsIn,IqsRule,Mother,Head,SGBefore,SGAfter,DtrsBefore,DtrsAfter),
  gen_dtrs(SGBefore,IqsRule,IqsSGBefore,_,_),
  deref(PivotTag,PivotSVs,NewTag,NewSVs),
  add_to(Head,NewTag,NewSVs,IqsSGBefore,IqsHead),
  check_inequal(IqsHead,IqsHeadCkd),
  gen_dtrs(SGAfter,IqsHeadCkd,IqsSGAfter,_,_),
  add_to(Mother,MotherTag,bot,IqsSGAfter,IqsMother),
  check_inequal(IqsMother,IqsMotherCkd),
  chained_nodes(MotherTag,bot,Tag,SVs,IqsMotherCkd,IqsChained),
  gen_dtrs(DtrsBefore,IqsChained,IqsDtrsBefore,NewWords,HeadWords),
  gen_dtrs(DtrsAfter,IqsDtrsBefore,IqsDtrsAfter,RestHeadWords,RestNewWords),
%  fully_deref_prune(MotherTag,bot,PMotherTag,PMotherSVs,IqsMother,IqsPrunned),
  conn(MotherTag,bot,Tag,SVs,IqsDtrsAfter,IqsOut,
       NewWords,RestNewWords,Words,RestWords).

% ------------------------------------------------------------------------------
% chain_rule(+IqsIn:<ineq>s, -IqsOut:<ineq>s,
%            -Mother:<desc>, -Head:<desc>,
%            -SGBefore:<desc>, -SGAfter:<desc>,
%            -DtrsBefore:<desc>s, -DtrsAFter:<desc>s)
% ------------------------------------------------------------------------------
% looks for chain rules and at the same time splits their RHS into
% Head, DtrsBefore and DtrsAfter
% ------------------------------------------------------------------------------
chain_rule(Iqs,Iqs,Mother,Head,SGBefore,SGAfter,DtrsBefore,DtrsAfter) :-
  (_RuleName rule Mother ===> Dtrs),
  split_dtrs(Dtrs,Head,SGBefore,SGAfter,DtrsBefore,DtrsAfter).

% ------------------------------------------------------------------------------
% gen_dtrs(+Dtrs:<desc>s, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%          -Words:<word>s, -RestWords:<word>s)
% ------------------------------------------------------------------------------
% recursively generates the difference list Words-RestWords from the
% RHS of a rule
% ------------------------------------------------------------------------------
gen_dtrs(empty,Iqs,Iqs,Words,Words) :- !.
gen_dtrs((word> Word),Iqs,Iqs,[Word|RestWords],RestWords) :- !.
gen_dtrs((word> Word,RestDtrs),IqsIn,IqsOut,[Word|Words],RestWords) :- !,
  gen_dtrs(RestDtrs,IqsIn,IqsOut,Words,RestWords).
gen_dtrs((cat> Dtr),IqsIn,IqsOut,Words,RestWords) :- !,
  add_to(Dtr,DtrTag,bot,IqsIn,IqsDtr),
  deref(DtrTag,bot,NewTag,NewSVs),
  check_inequal(IqsDtr,IqsDtrCkd),
  gen_int(NewTag,NewSVs,IqsDtrCkd,IqsOut,Words,RestWords).
gen_dtrs((cat> Dtr,RestDtrs),IqsIn,IqsOut,Words,RestWords) :- !,
  add_to(Dtr,DtrTag,bot,IqsIn,IqsDtr),
  deref(DtrTag,bot,NewTag,NewSVs),
  check_inequal(IqsDtr,IqsDtrCkd),
  gen_int(NewTag,NewSVs,IqsDtrCkd,IqsGen,Words,MidWords),
  gen_dtrs(RestDtrs,IqsGen,IqsOut,MidWords,RestWords).
gen_dtrs((goal> Goal),IqsIn,IqsOut,Words,Words) :- !,
  compile_body(Goal,[],[],IqsIn,IqsOut,PGoals,[]),
  make_seq(PGoals,SeqPGoals),
  call(SeqPGoals).
gen_dtrs((sem_goal> Goal),IqsIn,IqsOut,Words,Words) :- !,
  compile_body(Goal,[],[],IqsIn,IqsOut,PGoals,[]),
  make_seq(PGoals,SeqPGoals),
  call(SeqPGoals).
gen_dtrs((goal> Goal,RestDtrs),IqsIn,IqsOut,Words,RestWords) :- !,
  compile_body(Goal,[],[],IqsIn,IqsBody,PGoals,[]),
  make_seq(PGoals,SeqPGoals),
  call(SeqPGoals),
  gen_dtrs(RestDtrs,IqsBody,IqsOut,Words,RestWords).
gen_dtrs((cats> DtrsList),IqsIn,IqsOut,Words,RestWords) :- !,
  add_to(DtrsList,Tag,bot,IqsIn,IqsList),
  check_inequal(IqsList,IqsListCkd),
  deref(Tag,bot,_,DSVs), DSVs =.. [Sort|Vs],
  gen_list_dtrs(Sort,Vs,IqsListCkd,IqsOut,Words,RestWords).
gen_dtrs((cats> DtrsList,RestDtrs),IqsIn,IqsOut,Words,RestWords) :- !,
  add_to(DtrsList,Tag,bot,IqsIn,IqsList),
  check_inequal(IqsList,IqsListCkd),
  deref(Tag,bot,_,DSVs), DSVs =.. [Sort|Vs],
  gen_list_dtrs(Sort,Vs,IqsListCkd,IqsGen,Words,MidWords),
  gen_dtrs(RestDtrs,IqsGen,IqsOut,MidWords,RestWords).

% ------------------------------------------------------------------------------
% gen_list_dtrs(+Sort:<sort>, +Vs:<vs>, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%               -Words:<word>s, +RestWords:<word>s)
% ------------------------------------------------------------------------------
% generates a list of words Words-RestWords from a variable list of descriptions
% Sort(Vs)
% ------------------------------------------------------------------------------
gen_list_dtrs(e_list,_,Iqs,Iqs,Words,Words) :- !.
gen_list_dtrs(Sort,[HdFS,TlFS],IqsIn,IqsOut,Words,RestWords) :-
  subtype(ne_list,Sort), !,
  deref(HdFS,DtrTag,DtrSVs),
  gen_int(DtrTag,DtrSVs,IqsIn,IqsDtr,Words,MidWords),
  deref(TlFS,_,TlSVs), TlSVs =.. [TlSort|TlVs],
  gen_list_dtrs(TlSort,TlVs,IqsDtr,IqsOut,MidWords,RestWords).

% ------------------------------------------------------------------------------
% chained_nodes(+PivotTag:<tag>, +PivotSVs:<svs>, +RootTag:<tag>,
%               +RootSVs:<svs>, +IqsIn:<ineq>s, -IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% checks whether PivotTag-PivotSVs and RootTag-RootSVs can be connected through
% a chain of 'chain' rules
% ------------------------------------------------------------------------------
chained_nodes(PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut) :-
  ud(PivotTag-PivotSVs,RootTag-RootSVs,IqsIn,IqsOut).
chained_nodes(PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut) :-
  (_Rule rule Mother ===> Body),
  split_dtrs(Body,HeadIn,_,_,_,_),
  add_to(Mother,RootTag,RootSVs,IqsIn,IqsMother),
  check_inequal(IqsMother,IqsMotherCkd),
  current_chain_length(Max),
  chained_nodes_close(0,Max,HeadIn,HeadOut,IqsMotherCkd,IqsChained),
  add_to(HeadOut,PivotTag,PivotSVs,IqsChained,IqsHead),
  check_inequal(IqsHead,IqsOut).

% ------------------------------------------------------------------------------
% chained_nodes_close(+N:<int>, +Max:<int>, +HeadIn:<desc>, -HeadOut:<desc>,
%                     +IqsIn:<ineq>s, -IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% computes the closure of the semantic head relation
% ------------------------------------------------------------------------------
chained_nodes_close(_,_,Head,Head,Iqs,Iqs).
chained_nodes_close(N,Max,HeadIn,HeadOut,IqsIn,IqsOut) :-
  N < Max,
  add_to(HeadIn,Tag,bot,IqsIn,IqsHead),
  check_inequal(IqsHead,IqsHeadCkd),
  (_Rule rule MotherIn ===> Body),
  split_dtrs(Body,HeadMid,_,_,_,_),
  add_to(MotherIn,Tag,bot,IqsHeadCkd,IqsMother),
  check_inequal(IqsMother,IqsMotherCkd),
  NPlus1 is N+1,
  chained_nodes_close(NPlus1,Max,HeadMid,HeadOut,IqsMotherCkd,IqsOut).

% ------------------------------------------------------------------------------
% split_dtrs(+Dtrs:<desc>s, -Head:<desc>,
%            -SemGoalBefore:<desc>, -SemGoalAfter:<desc>,
%            -DtrsBefore:<desc>, -DtrsAfter:<desc>s)
% ------------------------------------------------------------------------------
% splits the RHS of a chain rule into Head, SemGoalBefore the Head, SemGoalAfter
% the Head, DtrsBefore the Head, and DtrsAfter the Head
% ------------------------------------------------------------------------------
split_dtrs((sem_goal> SemGoalBefore,sem_head> Head,sem_goal> SemGoalAfter,
            DtrsAfter),
           Head,sem_goal> SemGoalBefore,sem_goal> SemGoalAfter,
           empty,DtrsAfter) :- !.
split_dtrs((sem_goal> SemGoalBefore,sem_head> Head,sem_goal> SemGoalAfter),
           Head,sem_goal> SemGoalBefore,sem_goal> SemGoalAfter,
           empty,empty) :- !.
split_dtrs((sem_goal> SemGoalBefore,sem_head> Head,DtrsAfter),
           Head,sem_goal> SemGoalBefore,empty,empty,DtrsAfter) :- !.
split_dtrs((sem_goal> SemGoalBefore,sem_head> Head),
           Head,sem_goal> SemGoalBefore,empty,empty,empty) :- !.
split_dtrs((sem_head> Head,sem_goal> SemGoalAfter,DtrsAfter),
           Head,empty,sem_goal> SemGoalAfter,empty,DtrsAfter) :- !.
split_dtrs((sem_head> Head,sem_goal> SemGoalAfter),
           Head,empty,sem_goal> SemGoalAfter,empty,empty) :- !.
split_dtrs((sem_head> Head,DtrsAfter),Head,empty,empty,empty,DtrsAfter) :- !.
split_dtrs((sem_head> Head),Head,empty,empty,empty,empty) :- !.
split_dtrs((Dtr,RestDtrs),Head,SemGoalBefore,SemGoalAfter,
           (Dtr,DtrsBefore),DtrsAfter) :- !,
  split_dtrs(RestDtrs,Head,SemGoalBefore,SemGoalAfter,DtrsBefore,DtrsAfter).

% ------------------------------------------------------------------------------
% Run-time generation support
% ------------------------------------------------------------------------------

% ------------------------------------------------------------------------------
% gen(+Cat:<desc>)
% gen(+Tag:<tag>, +SVs:<svs>, +Iqs:<ineq>)
% ------------------------------------------------------------------------------
% top-level user calls to generate a sentence from a descriptor Cat
% or a FS specified by Tag, SVs, Iqs
% ------------------------------------------------------------------------------
gen(Cat) :-
  add_to(Cat,Tag,bot,[],Iqs),
  gen(Tag,bot,Iqs).

gen(Tag,SVs,Iqs) :-
%  secret_noadderrs,
  nl, write('CATEGORY: '), nl, ttyflush,
  pp_fs(Tag-SVs,Iqs), nl,
  gen(Tag,SVs,Iqs,Words),
  nl, write('STRING: '),
  nl, write_list(Words),
  nl, query_proceed
%,
%  secret_adderrs
.

% ------------------------------------------------------------------------------
% gen(+Tag:<tag>, +SVs:<svs>, +IqsIn:<ineq>s, -Words:<word>s)
% ------------------------------------------------------------------------------
% top-level functional interface for the generator
% generates the list of Words from the semantic specification of Tag-SVs,Iqs
% ------------------------------------------------------------------------------
gen(Tag,SVs,IqsIn,Words) :-
%  fully_deref_prune(Tag,SVs,NewTag,NewSVs,IqsIn,IqsPrunned),
  generate(Tag,SVs,IqsIn,IqsOut,Words,[]),
  extensionalise(Tag,SVs,IqsOut),
  check_inequal(IqsOut,_).   

% ------------------------------------------------------------------------------
% connect(+PivotTag:<tag>, +PivotSVs:<svs>, +RootTag:<tag>, +RootSVs:<svs>,
%         +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%         +NewWords:<word>s, +RestNewWords:<word>s,
%         -Words:<word>s, -RestWords:<word>s)
% ------------------------------------------------------------------------------
% connects bottom-up the PivotTag-PivotSVs FS to the root Tag-SVS FS
% and at the same time generates the difference-list Words-RestWords by 
% threading the given HeadWords-RestHeadWords
% ------------------------------------------------------------------------------
connect(PivotTag,PivotSVs,Tag,SVs,IqsIn,IqsOut,
        Words,RestWords,Words,RestWords) :-
   ud(PivotTag-PivotSVs,Tag-SVs,IqsIn,IqsOut).
%  u(PivotSVs,SVs,PivotTag,Tag,IqsIn,IqsOut).
connect(PivotTag,PivotSVs,Tag,SVs,IqsIn,IqsOut,
        HeadWords,RestHeadWords,Words,RestWords) :-
  chain_rule(PivotTag,PivotSVs,Tag,SVs,IqsIn,IqsOut,
             HeadWords,RestHeadWords,Words,RestWords).
% generate_list(+Sort:<sort>, +Vs:<vs>, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%               -Words:<word>s, +RestWords:<word>s)
% ------------------------------------------------------------------------------
% generates a list of words Words-RestWords from a variable list of descriptions
% Sort(Vs)
% ------------------------------------------------------------------------------
generate_list(e_list,_,Iqs,Iqs,Words,Words) :- !.
generate_list(Sort,[HdFS,TlFS],IqsIn,IqsOut,Words,RestWords) :-
  subtype(ne_list,Sort), !,
  deref(HdFS,DtrTag,DtrSVs),
  generate(DtrTag,DtrSVs,IqsIn,IqsDtr,Words,MidWords),
  deref(TlFS,_,TlSVs), TlSVs =.. [TlSort|TlVs],
  generate_list(TlSort,TlVs,IqsDtr,IqsOut,MidWords,RestWords).


% ------------------------------------------------------------------------------
% Compiler
% ------------------------------------------------------------------------------

:- dynamic current_chain_length/1.
current_chain_length(4).

% ------------------------------------------------------------------------------
% chain_length(N:<int>)
% ------------------------------------------------------------------------------
% asserts chain_length/1 to N -- controls depth of chain rules application
% ------------------------------------------------------------------------------
chain_length(N):-
  retractall(current_chain_length(_)),
  assert(current_chain_length(N)).

% ------------------------------------------------------------------------------
% generate(+Tag:<tag>, +SVs:<svs>, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%          +Words:<word>s, +RestWords:<word>s)
% ------------------------------------------------------------------------------
% recursively generates the difference list Words-RestWords from the root
% Tag-SVs,IqsIn
% ------------------------------------------------------------------------------
generate(Tag,SVs,IqsIn,IqsOut,Words,RestWords) if_h
    [solve(GoalIndex,[GoalPivot],IqsIn,IqsMid),
     non_chain_rule(IndexTag,bot,PivotTag,bot,Tag,SVs,
                    IqsMid,IqsOut,Words,RestWords)] :-
  semantics(Pred),
  GoalIndex =.. [Pred,Tag-SVs,IndexTag-bot],
  GoalPivot =.. [Pred,PivotTag-bot,IndexTag-bot].

% ------------------------------------------------------------------------------
% non_chain_rule(+IndexTag:<tag>, +IndexSVs:<svs>, +PivotTag:<tag>,
%                +PivotSVs:<svs>, +RootTag:<tag>, +RootSVs:<svs>,
%                +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%                -Words:<word>s, -RestWords:<word>s)
% ------------------------------------------------------------------------------
% compiles nonheaded grammar rules, lexical entries and empty categories into
% non_chain_rule predicates which unifies the mother against the
% PivotTag-PivotSVs FS, generates top-down the RHS, and connects the mother FS
% to the next chain rule
% the result Words-RestWords is the final list of words which includes the list
% NewWords-RestNewWords corresponding to the expansion of the current rule
% ------------------------------------------------------------------------------
non_chain_rule(_,_,PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut,
               Words,RestWords) if_h PGoals :-
  (_RuleName rule Mother ===> Dtrs),
  \+ split_dtrs(Dtrs,_,_,_,_,_),
  compile_non_chain_rule(Mother,Dtrs,PivotTag,PivotSVs,RootTag,RootSVs,
                         IqsIn,IqsOut,Words,RestWords,PGoals).
non_chain_rule(_,_,PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut,
               Words,Words) if_h PGoals :-
  current_predicate(empty,empty(_)),
  empty(Mother),
  compile_non_chain_rule(Mother,empty,PivotTag,PivotSVs,RootTag,RootSVs,
                         IqsIn,IqsOut,Words,Words,PGoals).
non_chain_rule(IndexTag,IndexSVs,PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut,
               Words,RestWords) if_h
  [branch(0,IndexTag-IndexSVs,IndexTag,IndexSVs,PivotTag,PivotSVs,
          RootTag,RootSVs,IqsIn,IqsOut,Words,RestWords)].

% ------------------------------------------------------------------------------
% compile_non_chain_rule(+Mother:<desc>, +Dtrs:<desc>s,
%                        +PivotTag:<tag>, +PivotSVs:<svs>,
%                        +RootTag:<tag>, +RootSVs:<svs>,
%                        +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%                        -Words:<word>s, -RestWords:<word>s, -SubGoals:<goal>s)
% ------------------------------------------------------------------------------
% the common part of non_chain_rule compilation 
% ------------------------------------------------------------------------------
compile_non_chain_rule(Mother,Dtrs,PivotTag,PivotSVs,RootTag,RootSVs,
                       IqsIn,IqsOut,Words,RestWords,PGoalsMother) :-
  compile_desc(Mother,PivotTag-PivotSVs,IqsIn,IqsMother,
               PGoalsMother,PGoalsDesc),
  ( (Dtrs=(empty); Dtrs=(word>_)), !,
    IqsMotherCkd=IqsMother, PGoalsDesc=PGoalsChained
  ; PGoalsDesc=[check_inequal(IqsMother,IqsMotherCkd)|PGoalsChained]),
  PGoalsChained=[chained(PivotTag,PivotSVs,RootTag,RootSVs,
                         IqsMotherCkd,IqsChained)|PGoalsDtrs],
  compile_gen_dtrs(Dtrs,IqsChained,IqsDtrs,NewWords,RestNewWords,PGoalsDtrs,
                   [
%                   fully_deref_prune(PivotTag,PivotSVs,PPivotTag,PPivotSVs,
%                                     IqsDtrs,IqsPrunned),
                    connect(PivotTag,PivotSVs,RootTag,RootSVs,
                            IqsDtrs,IqsOut,NewWords,RestNewWords,
                            Words,RestWords)]).

% ------------------------------------------------------------------------------
% chain_rule(+PivotTag:<tag>, +PivotSVs:<svs>, +RootTag:<tag>, +RootSVs:<svs>,
%            +IqsIn:<ineq>s, -IqsOut:<ineq>s, +HeadWords:<word>s,
%            +RestHeadWords:<word>s, -Words:<word>s, RestWords:<word>s)
% ------------------------------------------------------------------------------
% compiles headed grammar rules into chain_rule predicates which unify the head
% agains the PivotTag-PivotSVS FS, generates top-down the rest of the RHS,
% and connects the mother FS to the next chain rule
% the result is the list Words-RestWords which includes the sublist
% HeadWords-RestHeadWords corresponding to the head
% ------------------------------------------------------------------------------
chain_rule(PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut,
           HeadWords,RestHeadWords,Words,RestWords) if_h PGoalsSGBefore :-
  (_RuleName rule Mother ===> Dtrs),
  split_dtrs(Dtrs,Head,SGBefore,SGAfter,DtrsBefore,DtrsAfter),
  compile_gen_dtrs(SGBefore,IqsIn,IqsSGBefore,_,_,
                   PGoalsSGBefore,PGoalsHead),
  compile_desc(Head,PivotTag-PivotSVs,IqsSGBefore,IqsHead,PGoalsHead,
               [check_inequal(IqsHead,IqsHeadCkd)|PGoalsMother]),
  compile_gen_dtrs(SGAfter,IqsHeadCkd,IqsSGAfter,_,_,
                   PGoalsMother,PGoalsSGAfter),
  compile_desc(Mother,MotherTag-bot,IqsSGAfter,IqsMother,PGoalsSGAfter,
               [check_inequal(IqsMother,IqsMotherCkd),
                chained(MotherTag,bot,RootTag,RootSVs,
                        IqsMotherCkd,IqsChained)|PGoalsLeft]),
  compile_gen_dtrs(DtrsBefore,IqsChained,IqsDtrsBefore,NewWords,HeadWords,
                   PGoalsLeft,PGoalsRight),
  compile_gen_dtrs(DtrsAfter,IqsDtrsBefore,IqsDtrsAfter,
                   RestHeadWords,RestNewWords,PGoalsRight,
                   [
%                   fully_deref_prune(MotherTag,bot,PMotherTag,PMotherSVs,
%                                     IqsDtrsAfter,IqsPrunned),
                    connect(MotherTag,bot,RootTag,RootSVs,IqsDtrsAfter,IqsOut,
                            NewWords,RestNewWords,Words,RestWords)]).

% ------------------------------------------------------------------------------
% compile_gen_dtrs(+Dtrs:<desc>, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%                  -Words:<word>s, -RestWords:<word>s,
%                  -Goals:<goal>s, -GoalsRest:<goal>s)
% ------------------------------------------------------------------------------
% compiles the top-down expansion of a sequence Dtrs of RHS items
% (daughters or goals)
% ------------------------------------------------------------------------------
compile_gen_dtrs(empty,IqsIn,IqsIn,Words,Words,PGoals,PGoals) :- !.
compile_gen_dtrs((word> Word),IqsIn,IqsIn,[Word|RestWords],RestWords,
                 PGoals,PGoals) :- !.
compile_gen_dtrs((word> Word,RestDtrs),IqsIn,IqsOut,[Word|Words],RestWords,
                 PGoalsDtrs,PGoalsRest) :- !,
  compile_gen_dtrs(RestDtrs,IqsIn,IqsOut,Words,RestWords,PGoalsDtrs,PGoalsRest).
compile_gen_dtrs((cat> Dtr),IqsIn,IqsOut,Words,RestWords,
                 PGoalsDtr,PGoalsRest) :- !,
  compile_desc(Dtr,Tag-bot,IqsIn,IqsDtr,PGoalsDtr,
               [check_inequal(IqsDtr,IqsDtrCkd),
                generate(Tag,bot,IqsDtrCkd,IqsOut,Words,RestWords)|
                PGoalsRest]).
compile_gen_dtrs((cat> Dtr,RestDtrs),IqsIn,IqsOut,Words,RestWords,
                 PGoalsDtr,PGoalsRest) :- !,
  compile_desc(Dtr,Tag-bot,IqsIn,IqsDtr,PGoalsDtr,
               [check_inequal(IqsDtr,IqsDtrCkd),
                generate(Tag,bot,IqsDtrCkd,IqsRest,Words,NewWords)|
                PGoalsDtrs]),
  compile_gen_dtrs(RestDtrs,IqsRest,IqsOut,NewWords,RestWords,
                   PGoalsDtrs,PGoalsRest).
compile_gen_dtrs((goal> Goal),IqsIn,IqsOut,Words,Words,
                 PGoalsBody,PGoalsRest) :- !,
  compile_body(Goal,[],[],IqsIn,IqsOut,PGoalsBody,PGoalsRest).
compile_gen_dtrs((sem_goal> Goal),IqsIn,IqsOut,Words,Words,
                 PGoalsBody,PGoalsRest) :- !,
  compile_body(Goal,[],[],IqsIn,IqsOut,PGoalsBody,PGoalsRest).
compile_gen_dtrs((goal> Goal,RestDtrs),IqsIn,IqsOut,Words,RestWords,
                 PGoalsBody,PGoalsRest) :- !,
  compile_body(Goal,[],[],IqsIn,IqsBody,PGoalsBody,PGoalsDtrs),
  compile_gen_dtrs(RestDtrs,IqsBody,IqsOut,Words,RestWords,
                   PGoalsDtrs,PGoalsRest).
compile_gen_dtrs((cats> Dtrs),IqsIn,IqsOut,Words,RestWords,
                 PGoalsDtrs,PGoalsRest) :- !,
  compile_desc(Dtrs,Tag-bot,IqsIn,IqsList,PGoalsDtrs,
               [check_inequal(IqsList,IqsListCkd),
                deref(Tag,bot,_,SVs),
                SVs =.. [Sort|Vs],
                generate_list(Sort,Vs,IqsListCkd,IqsOut,Words,RestWords)|
                PGoalsRest]).
compile_gen_dtrs((cats> Dtrs,RestDtrs),IqsIn,IqsOut,Words,RestWords,
                 PGoalsDtrs,PGoalsRest) :- !,
  compile_desc(Dtrs,Tag-bot,IqsIn,IqsList,PGoalsDtrs,
               [check_inequal(IqsList,IqsListCkd),
                deref(Tag,bot,_,SVs),
                SVs =.. [Sort|Vs],
                generate_list(Sort,Vs,IqsListCkd,IqsGen,Words,NewWords)|
                PGoalsRestDtrs]),
  compile_gen_dtrs(RestDtrs,IqsGen,IqsOut,NewWords,RestWords,
                   PGoalsRestDtrs,PGoalsRest).

% ------------------------------------------------------------------------------
% chained(+PivotTag:<tag>, +PivotSVs:<svs>, +RootTag:<tag>,
%         +RootSVs:<svs>, +IqsIn:<ineq>s, -IqsOut:<ineq>s)
% ------------------------------------------------------------------------------
% checks whether PivotTag-PivotSVs and RootTag-RootSVs can be connected through
% a chain of grammar rules
% ------------------------------------------------------------------------------
chained(PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut) if_h PGoals :-
  (_Rule rule Mother ===> Body),
  split_dtrs(Body,HeadIn,_,_,_,_),
  compile_desc(Mother,RootTag-RootSVs,IqsIn,IqsMother,PGoals,
               [check_inequal(IqsMother,IqsMotherCkd)|PGoalsHead]),
  current_chain_length(Max),
  chained_nodes_close(0,Max,HeadIn,HeadOut,[],IqsChain),
  conc(IqsChain,IqsMotherCkd,IqsBoth),
  compile_desc(HeadOut,PivotTag-PivotSVs,IqsBoth,IqsHead,PGoalsHead,
               [check_inequal(IqsHead,IqsOut)]).
chained(PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut) if_h 
  [ud(PivotTag-PivotSVs,RootTag-RootSVs,IqsIn,IqsOut)].

% ------------------------------------------------------------------------------
% Indexing the lexicon
% ------------------------------------------------------------------------------

:- dynamic lexicon/1.

% -----------------------------------------------------------------------------
% build_tree(-Tree:<node>)
% ------------------------------------------------------------------------------
% builds a decision tree which includes the whole lexicon
%   the tree is   Node=Path:Branches  with the root Path=null for interior nodes
%   and           Node=[(Mother/IqsOut-IqsIn,Word)|...]  for leaves
%   and           Branches=[Type/Node|...]
% ------------------------------------------------------------------------------
build_tree(Tree) :-
  collect_entries(Entries),
  index_list(Entries,Tree),
  close_tree(Tree).

% ------------------------------------------------------------------------------
% collect_entries(-Entries:<entry>s)
% ------------------------------------------------------------------------------
% collects all the lexical entries for indexing, both basic and generated by
% applying lexical rules
% ------------------------------------------------------------------------------
collect_entries(Entries) :-
  findall((IndexTag-bot,Mother/IqsOut-IqsIn,Word),
          (gen_lex_rule(IqsLex,Mother,(word>Word)),
           add_to(Mother,Tag,bot,IqsLex,IqsMother),
           semantics(Pred), GoalIndex =.. [Pred,Tag-bot,IndexTag-bot],
           solve(GoalIndex,[],IqsMother,IqsSolved),
% fully_deref_prune(IndexTag,bot,DIndexTag,DIndexSVs,IqsGoal,IqsOut),
	   conc(IqsSolved,IqsIn,IqsOut)),
          Entries).

% ------------------------------------------------------------------------------
% gen_lex_rule(+IqsIn:<ineq>s, -IqsOut:<ineq>s, -Mother:<desc>, -Dtrs:<desc>s)
% ------------------------------------------------------------------------------
% generates all lexical grammar rules Mother ===> Dtrs from lexical entries and
% recursive applications of proper lexical rules
% ------------------------------------------------------------------------------
gen_lex_rule(IqsLex,MotherOut,Dtrs) :-
  (Word ---> MotherIn),
  curr_lex_rule_depth(Max),
  gen_lex_close(0,Max,Word,MotherIn,(word> Word),[],IqsLex,MotherOut,Dtrs).

% ------------------------------------------------------------------------------
% gen_lex_close(+N:<int>, +Max:<int>, +WordIn:<word>, +MotherIn:<desc>,
%               +DtrsIn:<desc>s, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%               -MotherOut:<desc>, -DtrsOut:<desc>s)
% ------------------------------------------------------------------------------
% computes the closure of lexical entries under lexical rules to get additional
% lexical grammar rules MotherOut ===> DtrsOut
% ------------------------------------------------------------------------------
gen_lex_close(_,_,_,Mother,Dtrs,Iqs,Iqs,Mother,Dtrs).
gen_lex_close(N,Max,WordIn,MotherIn,_,IqsIn,IqsOut,MotherOut,DtrsOut) :-
  current_predicate(lex_rule,lex_rule(_,_)),
  N < Max, add_to(MotherIn,Tag,bot,IqsIn,IqsMother),
  check_inequal(IqsMother,IqsMotherCkd),
  deref(Tag,bot,InTag,InSVs),
  ( (_LexRuleName lex_rule DescIn **> DescOut morphs Morphs),
    add_to(DescIn,InTag,InSVs,IqsMotherCkd,IqsDesc),
    check_inequal(IqsDesc,IqsDescCkd)
  ; (_LexRuleName lex_rule DescIn **> DescOut if Cond morphs Morphs),
    add_to(DescIn,InTag,InSVs,IqsMotherCkd,IqsDesc),
    check_inequal(IqsDesc,IqsEntry),
    compile_body(Cond,[],[],IqsEntry,IqsDescCkd,PGoals,[]),
    make_seq(PGoals,SeqPGoals),
    call(SeqPGoals)),
  morph(Morphs,WordIn,WordOut),
  NPlus1 is N+1,
%  prune(IqsDescCkd,IqsPrunned),
  gen_lex_close(NPlus1,Max,WordOut,DescOut,(word> WordOut),IqsDescCkd,IqsOut,
                MotherOut,DtrsOut).

% ------------------------------------------------------------------------------
% index_list(+Entries:<entry>s, -Tree:<node>)
% ------------------------------------------------------------------------------
% builds an open tree by incrementally indexing each entry in Entries into an
% initially empty Tree
% ------------------------------------------------------------------------------
index_list([],_).
index_list([(IndexTag-IndexSVs,Entry)|Entries],Tree) :-
  deref(IndexTag,IndexSVs,DIndexTag,DIndexSVs),
  type_of(DIndexTag,DIndexSVs,Type),
  collect_paths(null-Type,DIndexTag,DIndexSVs,Paths,[]),
  index([null-Type|Paths],Entry,Tree),
  index_list(Entries,Tree).

% ------------------------------------------------------------------------------
% collect_paths(+Prefix-Type, +DIndexTag:<tag>, +DIndexSVs:<svs>,
%               -Paths:<path_type>s)
% ------------------------------------------------------------------------------
% collects all the paths appropriate for the dereferenced FS DIndexTag-DIndexSVs
% of type Type, and prefixed by Prefix
% ------------------------------------------------------------------------------
collect_paths(Prefix-Type,DIndexTag,DIndexSVs,Paths,RestPaths) :-
  approp_feats(Type,Feats),
  make_paths(Feats,Prefix,DIndexTag,DIndexSVs,Paths,PathsList),
  collect_paths_list(Feats,Paths,DIndexTag,DIndexSVs,
                     PathsList,RestPaths).

% ------------------------------------------------------------------------------
% collect_path_list(+Feats:<feat>s, PreFeats:+<path_type>s, +DIndexTag:<tag>,
%                   +DIndexSVs:<svs>, -Paths:<path_type>s,
%                   +RestPaths:<path_type>s)
% ------------------------------------------------------------------------------
% collects the paths in DIndexTag-DIndexSVs that follow from each feature in
% Feats 
% ------------------------------------------------------------------------------
collect_paths_list([],_,_,_,Paths,Paths).
collect_paths_list([Feat|Feats],[PreFeat|PreFeats],
                   DIndexTag,DIndexSVs,Paths,RestPaths) :-
  featval(Feat,DIndexSVs,DIndexTag,Tag-SVs,_,_),
  deref(Tag,SVs,DTag,DSVs),
  collect_paths(PreFeat,DTag,DSVs,Paths,PathsList),
  collect_paths_list(Feats,PreFeats,DIndexTag,DIndexSVs,
                     PathsList,RestPaths).

% ------------------------------------------------------------------------------
% make_paths(+Feats:<feat>s, +Prefix:<path>, +DIndexTag:<tag>, +DIndexSVs:<svs>,
%            -Paths:<path_type>s, +RestPaths:<path_type>s)
% ------------------------------------------------------------------------------
% creates all the possible paths by prefixing each feature in Feats with Prefix
% and adding the corresponding Type in DIndexTag-DIndexSVs
% ------------------------------------------------------------------------------
make_paths([],_,_,_,Paths,Paths).
make_paths([Feat|Feats],Prefix,DIndexTag,DIndexSVs,
           [PreFeat-Type|Paths],RestPaths) :-
  featval(Feat,DIndexSVs,DIndexTag,Tag-SVs,_,_),
  deref(Tag,SVs,DTag,DSVs),
  type_of(DTag,DSVs,Type),
  connect_path(Prefix,Feat,PreFeat),
  make_paths(Feats,Prefix,DIndexTag,DIndexSVs,Paths,RestPaths).

% ------------------------------------------------------------------------------
% type_of(+Tag:<tag>, +SVs:<svs>, -Type:<type>)
% ------------------------------------------------------------------------------
% returns the type of a dereferenced FS Tag-SVs
% ------------------------------------------------------------------------------
type_of(_,SVs,Type) :-
  SVs =.. [Type|_].

% ------------------------------------------------------------------------------
% index(+Paths:<path_type>s, +Entry:<entry>, -Tree:<node>)
% ------------------------------------------------------------------------------
% creates a new branch in the Tree with arcs labeled by paths in Paths, nodes
% labeled by type in Paths and leaf containing Entry
% ------------------------------------------------------------------------------
index([],Entry,Entries) :-
  memberchk(Entry,Entries).
index([Path-Type|Paths],Entry,Path:Branches) :-
  memberchk(Type/SubTree,Branches),
  index(Paths,Entry,SubTree).

% ------------------------------------------------------------------------------
% close_tree(-Tree:<node>)
% ------------------------------------------------------------------------------
% closes all the open lists in Tree
% ------------------------------------------------------------------------------
close_tree(_:Branches) :- !,
  close_tree_branches(Branches).
close_tree(Tree) :-
  close_tree_list(Tree).

% ------------------------------------------------------------------------------
% close_tree_branches(-Branches:<branch>s)
% ------------------------------------------------------------------------------
% closes all open Branches of a tree
% ------------------------------------------------------------------------------
close_tree_branches([]) :- !.
close_tree_branches([_/Tree|Branches]) :-
  close_tree(Tree),
  close_tree_branches(Branches).

% ------------------------------------------------------------------------------
% close_tree_list(-Tree:<node>)
% ------------------------------------------------------------------------------
% closes all open lists of entries in the tree
% ------------------------------------------------------------------------------
close_tree_list([]) :- !.
close_tree_list([_|List]) :-
  close_tree_list(List).

% ------------------------------------------------------------------------------
% node(+Label:<int>, +IndexTag:<tag>, +IndexSVs:<svs>, +PivotTag:<tag>,
%      +PivotSVs:<svs>, +RootTag:<tag>, +RootSVs:<svs>, +IqsIn:<ineq>s,
%      -IqsOut:<ineq>s, -Words:<word>s, +RestWords:<word>s)
% ------------------------------------------------------------------------------
% compiles all nodes in an indexing tree into Prolog clauses
% ------------------------------------------------------------------------------
node(Label,IndexTag,IndexSVs,PivotTag,PivotSVs,RootTag,RootSVs,IqsIn,IqsOut,
     Words,RestWords) if_h PGoals :-
  lexicon(_:Branches),
  retractall(label(_)), assert(label(0)),
  nodelist(Branches,Node,Label),
  compile_gen_lex(Node,Label,IndexTag,IndexSVs,PivotTag,PivotSVs,
                  RootTag,RootSVs,IqsIn,IqsOut,Words,RestWords,PGoals).

% ------------------------------------------------------------------------------
% nodelist(+Branches:<branch>s, -Node:<node>, -Label:<int>)
% ------------------------------------------------------------------------------
% returns all nodes in Branches with corresponding labels
% ------------------------------------------------------------------------------
nodelist([_/Tree|_],Node,Label) :-
  node(Tree,Node,Label).
nodelist([_|Branches],Node,Label) :-
  nodelist(Branches,Node,Label).

% ------------------------------------------------------------------------------
% node(+Tree:<node>, -Node:<node>, -Label:<int>)
% ------------------------------------------------------------------------------
% return all the nodes of Tree with corresponding labels
% ------------------------------------------------------------------------------
node(Tree,Tree,NewLabel) :-
  retract(label(Label)),
  NewLabel is Label + 1,
  assert(label(NewLabel)).
node(_:Branches,Node,Label) :-
  nodelist(Branches,Node,Label).

% ------------------------------------------------------------------------------
% compile_gen_lex(+Tree:<node>, +Label:<int>, +IndexTag:<tag>, +IndexSVs:<svs>,
%                 +PivotTag:<tag>, +PivotSVs:<svs>, +RootTag:<tag>,
%                 +RootSVs:<svs>, +IqsIn:<ineq>s, -IqsOut:<ineq>s,
%                 -Words:<word>s, +RestWords:<word>s, PGoals:<goal>s)
% ------------------------------------------------------------------------------
% compiles the body of a node in the indexing tree
% ------------------------------------------------------------------------------
compile_gen_lex([Entry|Entries],_,_,_,PivotTag,PivotSVs,
                RootTag,RootSVs,IqsIn,IqsOut,Words,RestWords,PGoals) :-
  member_(Entries,Entry,(Mother/IqsEntry-IqsIn,Word)),
  compile_non_chain_rule(Mother,(word>Word),PivotTag,PivotSVs,RootTag,RootSVs,
                         IqsEntry,IqsOut,Words,RestWords,PGoals).
compile_gen_lex(Path:_,Label,IndexTag,IndexSVs,PivotTag,PivotSVs,
                RootTag,RootSVs,IqsIn,IqsOut,Words,RestWords,PGoals) :-
%  cat_atoms('branch_',Label,BranchPred),
%  PGoalBranch =.. [BranchPred,Value,IndexTag,IndexSVs,PivotTag,PivotSVs,
%                   RootTag,RootSVs,IqsValue,IqsOut,Words,RestWords],
  PGoalBranch = branch(Label,Value,IndexTag,IndexSVs,PivotTag,PivotSVs,
                       RootTag,RootSVs,IqsValue,IqsOut,Words,RestWords),
  connect_path(Path,Value,Feat),
  compile_desc(Feat,IndexTag-IndexSVs,IqsIn,IqsValue,PGoals,
               [PGoalBranch]).

% ------------------------------------------------------------------------------
% connect_path(+Path:<path>, +Feat:<feat>, -NewPath:<path>)
% ------------------------------------------------------------------------------
% adds Feat to the end of Path to give NewPath
% ------------------------------------------------------------------------------
connect_path(null,Feat,Feat) :- !.
connect_path(Feat1:Path,Feat,Feat1:NewPath) :- !,
  connect_path(Path,Feat,NewPath).
connect_path(Feat1,Feat,Feat1:Feat).

% ------------------------------------------------------------------------------
% branch(+MotherLabel:<int>, +Value:<tag_svs>, +IndexTag:<tag>, +IndexSVs:<svs>,
%        +PivotTag:<tag>, +PivotSVs:<svs>, +RootTag:<tag>, +RootSVs:<svs>,
%        +IqsIn:<ineq>s, -IqsOut:<ineq>s, -Words:<word>s, +RestWords:<word>s,
%        -PGoals:<goal>s)
% ------------------------------------------------------------------------------
% compiles all branches of a tree, into Prolog clauses
% ------------------------------------------------------------------------------
branch(MotherLabel,Value,IndexTag,IndexSVs,PivotTag,PivotSVs,RootTag,RootSVs,
       IqsIn,IqsOut,Words,RestWords) if_h PGoals :-
  lexicon(Tree),
  retractall(label(_)), assert(label(0)),
  branch(Tree,Type,MotherLabel,DaughterLabel),
%  cat_atoms('node_',DaughterLabel,NodePred),
%  PGoalNode =.. [NodePred,IndexTag,IndexSVs,PivotTag,PivotSVs,
%                 RootTag,RootSVs,IqsValue,IqsOut,Words,RestWords],
  PGoalNode = node(DaughterLabel,IndexTag,IndexSVs,PivotTag,PivotSVs,
                   RootTag,RootSVs,IqsValue,IqsOut,Words,RestWords),
  compile_desc(Type,Value,IqsIn,IqsValue,PGoals,[PGoalNode]).

% ------------------------------------------------------------------------------
% branch(+Tree:<node>, -Type:<type>, -MotherLabel:<int>, -DaughterLabel:<int>)
% ------------------------------------------------------------------------------
% returns all branches in Tree with their Type and labels at the ends
% ------------------------------------------------------------------------------
branch(_:Branches,Type,MotherLabel,DaughterLabel) :-
  label(CurrentLabel),
  branchlist(Branches,Type,CurrentLabel,MotherLabel,DaughterLabel).

% ------------------------------------------------------------------------------
% branchlist(+Branches:<branch>s, -Type:<type>, +CurrentLabel:<int>,
%            -MotherLabel:<int>, -DaughterLabel:<int>)
% ------------------------------------------------------------------------------
% returns all branches in Branches with the appropriate Type, and end labels
% ------------------------------------------------------------------------------
branchlist([Type/_|_],Type,MotherLabel,MotherLabel,DaughterLabel) :-
  retract(label(Label)), DaughterLabel is Label+1,
  assert(label(DaughterLabel)).
branchlist([_/Tree|_],Type,_,MotherLabel,DaughterLabel) :-
  branch(Tree,Type,MotherLabel,DaughterLabel).
branchlist([_|Branches],Type,CurrentLabel,MotherLabel,DaughterLabel) :-
  branchlist(Branches,Type,CurrentLabel,MotherLabel,DaughterLabel).


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

:- nl,write('
ALE Version 3.0; May, 1998
Copyright (C) 1998, Bob Carpenter and Gerald Penn
All rights reserved'),nl,
   nointerp,
   nosubtest,
   parse.

subsume(Desc1,Desc2,LReln,RReln) :-
  add_to(Desc1,Tag1,bot,[],Iqs1),
  add_to(Desc2,Tag2,bot,[],Iqs2),
  fully_deref_prune(Tag1,bot,DTag1,DSVs1,Iqs1,DIqs1),
  fully_deref_prune(Tag2,bot,DTag2,DSVs2,Iqs2,DIqs2),
  subsume([s(DTag1,DSVs1,DTag2,DSVs2)],DIqs1,DIqs2,<,>,LReln,RReln,[],[]).