% ==============================================================================
% 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),aboli