%%%  -*- Mode: PROLOG; Package: PROLOG-USER -*-

%%%
%%% (c) 1991--1995  Sandiway Fong, NEC Research Institute, Inc.
%%%     with contributions from Martine Smets UIUC, Charles Yang MIT
%%%
%%%     2001 Revised by Sandiway Fong
%%%
%%%
%%% EXPORT
%%% (Recovery of Phrase Structure)
%%%	parsePF(I,ZLSS) 	parseSS(ZLSS,CF)
%%%
%%% (Theta Theory)
%%%	thRoleAsssign(CF)	thetaCriterion(CF)	dStructureCondition(CF)
%%%
%%% (Case Theory)
%%%	inCaseAssign(CF)	sCaseAssign(CF)		sBarDeletion(CF)
%%%	caseFilter(CF)		traceCaseCondition(CF)
%%%
%%% (Movement)
%%%	subjacency(CF)		resolveTraces(CF)	whInSyntax(CF)
%%%	lfMovement(SS,LF)
%%%
%%% (Binding Theory)
%%%	freeIndexing(CF)	expletiveLinking(CF)	coindexSubjAndINFL(CF)
%%%	functionalDet(CF)
%%%	conditionA(CF)		conditionB(CF)		conditionC(CF)
%%%	licenseClitics(CF)
%%%
%%% (Control Theory)
%%%	control(CF)
%%%
%%% (Empty Categories)
%%%	ecp(CF)			ecpLF(CF)
%%%	licenseObjectPro(CF)
%%%
%%% (Full Interpretation)
%%%	licenseOpVars(CF)	
%%%	licenseAdjuncts(CF)	licenseClausalArguments(CF) 
%%%	reanalyzeBoundProforms(CF)
%%%	quantifierScoping(CF)
%%%	whCompRequirement(CF)
%%%
%%% IMPORT
%%%	caseAdjacency				parametersL
%%%	boundingNode(C)	- subjacency
%%%	whInSyntax
%%%	proDrop
%%%	clitic(subject/object)
%%%     isomorphicPrinciple                     (subj/obj QP scoping)
%%%	(constructs and constituent processing)	progLang
%%%	(constituent processing)		utilities
%%%	(list processing)

%%% DISPLAY PREFERENCES

upper_panel_display_order( 
			 [thetaCriterion, dStructureCondition, 
			  subjacency, whInSyntax,  
			  agrCriterion,
			  sBarDeletion, caseFilter, traceCaseCondition,
			  coindexSubjAndINFL, 
			  conditionA, conditionB, conditionC, 
			  ecp, control,
			  licenseClitics, licenseObjectPro, 
			  ecpLF, 
			  licenseOpVars, quantifierScoping,
			  reanalyzeBoundProforms,
			  licenseClausalArguments, licenseAdjuncts, 
			  whCompRequirement]).

lower_panel_display_order( 
			 [parsePF, parseSS, 
			  thRoleAssign, inCaseAssign, sCaseAssign,
			  resolveTraces, functionalDet, freeIndexing, 
			  expletiveLinking, 
			  lfMovement]).

%%% RECOVERY OF PHRASE STRUCTURE

parsePF parser_operation 'Parse PF'
	with_components
		io	    	given_by [pf,ss],
		controlType 	given_by generator.

parseSS parser_operation 'Parse S-Structure'
	with_components
		io	    	given_by [ss,ss],
		dep		given_by parsePF,
		controlType 	given_by generator.

%%% THETA THEORY

%%% Declare thRoleAssign

thRoleAssign parser_operation 'Assign Theta-Roles'
	with_components
		io          given_by [ss],
		dep         given_by parseSS,
		controlType given_by filter,
		% optional ...
		abstract    given_by 1.
		
%%% THETA ROLE ASSIGNMENT

thRoleAssign in_all_configurations CF where
	thetaConfig(CF,Role,XP) then assignRole(Role,XP).

% thetaConfig(Config,Roles,L) holds when Config is identified as a
% O-role assignment configuration with components:
%	Els 	the elements to which O-roles are to be assigned
%	Roles	the O-roles that Els should receive
% NB. shared by O-role and inherent Case assignment 

thetaConfig(CF,Role,Complement) :-		% [Xi X Complement]
	Complement immediate complement_of CF,	% [Xj [Xi X ...] Complement]
	CF has_feature grid(_,Rs),
	(Complement has_feature indirectObject
    	-> secondRole(Rs,Role)
    	;  firstRole(Rs,Role)).

thetaConfig(NP,OptRole,Subject) :-	  	% [NP Subject [N1 N ..]]
	cat(NP,np),				% [Spec,NP] optionally
	cat(Subject,np),			% receives a O-role
	Subject immediate specifier_of NP,
	NP has_feature grid([Role],Int),
	(Int == []
        -> OptRole = Role
	;  optional(Role,OptRole)).

thetaConfig(VP,Role,Subject):-               %thetaConfig (VP... is new code
	( cat(VP,vp) ; cat(VP,ap)),                             
	\+ adjoined(VP),
	Subject specifier_of VP,
	externalRole(VP,Role).

thetaConfig(VP,Role,Adjunct) :-			% [VP [VP..] NP]
	cat(VP,vp),
	cat(Adjunct,np),
	adjoined(VP,Adjunct),
	\+ Adjunct has_feature apos,		  % distinguish scrambling
	VP has_feature allowExt(Role).

assignRole(CRole,Item) :-
	CRole has_role_name Role,
	roleAssignable(Role,Item),
	make Item have_feature theta(Role).

externalRole(XP,Role) :- 
	\+ XP has_feature blockTheta,
	XP has_feature grid([Role],_).

% externalRole(XP,Role) :-
%	\+ inheritsFeature(XP,blockTheta),
%	inheritsFeature(XP,grid(ExtR,_)),	  % external Role
%	ExtR = [Role].

unsaturatedExtRole(XP,Role) :- 
	inheritsFeature(XP,blockTheta),
	inheritsFeature(XP,grid(ExtR,_)),	  % external Role
	ExtR = [Role].

inheritsFeature(X,F) :-	
	X has_feature F
	-> true
%	;  (X subcategorizes_for Y
	;  (Y complement_of X
	   -> inheritsFeature(Y,F)
	   ;   adjoined(X,_,LowerX),
	       inheritsFeature(LowerX,F)).

%%% Declare ThetaCriterion

thetaCriterion parser_operation 'Theta Criterion'
	with_components
		io	     given_by [ss],
		multiple dep         given_by [thRoleAssign,resolveTraces],
		multiple controlType given_by [filter,generator],
		% optional...
		sCueFilter,
		abstract 	     given_by 1,
		pos.

%%% THETA CRITERION 
%%% checks at S-structure that for all chains:
%%%	1. All elements of a chain must not be assigned a theta-role, except
%%%	2. If chain is headed by an argument, 
%%%	   then the last element of the chain must be assigned a theta-role

thetaCriterion in_all_configurations CF where
	thetaRelevant(CF) then thetaMarked(CF) iff lastInAChain(CF).

thetaRelevant(X) :- cat(X,np), highestSegment(X).
thetaRelevant(X) :- cat(X,c2).
thetaRelevant(X) :- cat(X,i2), highestSegment(X).
thetaRelevant(X) :- cat(X,vp).               %new code
thetaMarked(X) :- X has_feature theta(Role), assigned(Role).

lastInAChain(X) :- \+ partOfChain(X), argument(X).
lastInAChain(X) :- baseTrace(X), recoverDsElement(Y,X),	argument(Y).

% definition of argument for S-structure has to be sensitive to:
% 1. (quasi) quantifiers in A- or A-bar-positions
% 2. variables
% Extra: assume empty NPs in adjunct A-positions are not arguments

argument(Arg) :- emptyArgument(Arg).
argument(Arg) :- overtArgument(Arg).

emptyArgument(NP)   :- 
	emptyNP(NP), 
	NP has_feature apos, 
	\+ NP has_feature adjunct,
	\+ NP has_feature nonarg(+).

emptyNP(NP) :- cat(NP,np), ec(NP).

overtArgument(NP) :- cat(NP,np), \+ ec(NP), overtNPArgument(NP).
overtArgument(S) :- clause(S), S has_feature apos.

overtNPArgument(NP) :- 
	(NP has_feature wh(+) ; NP has_feature op(+)) 
	-> NP has_feature apos
	;  \+ NP has_feature nonarg(+).

clause(IP) :- cat(IP,i2).
clause(CP) :- cat(CP,c2).

bPRO(X) :- emptyNP(X), X has_feature apos, X has_feature_set [a(+),p(+)].

pro(X) :- 
	proDrop, emptyNP(X), X has_feature apos, X has_feature_set [a(-),p(+)].

%%% Declare dStructureCondition

dStructureCondition parser_operation 'D-structure Theta Condition'
	with_components
		io           given_by [ss],
		multiple dep given_by [thRoleAssign,resolveTraces],
		controlType  given_by filter,
		% optional...
		sCueFilter,
		pos.

%%% D-STRUCTURE THETA-MARKING CONDITION
%%%	D-structures are uniform with respect to theta-marking.
%%%	Head A T-governs B if B is the complement or the subject of A.
%%%	D-structure uniformity condition is:
%%%		X T-governed by A => ( argument(X) iff A O-marks X )

dStructureCondition in_all_configurations CF where
	tGovConfig(CF,Item) then argIffThMarkedAtDS(Item).

tGovConfig(CF,Item) :- thetaConfig(CF,_Role,Item).

argIffThMarkedAtDS(SS) :-
	recoverDsElement(DS,SS),
	argument(DS) iff thetaMarked(SS).

%%% D-STRUCTURE ELEMENT RECOVERY
%%%	Given an S-structure element SS, recoverDsElement(DS,SS) returns 
%%%     the element that occupies the position of SS at D-structure
%%%	according to the following table:
%%%
%%% 	S-structure			D-structure
%%% 	1. base trace			head of chain
%%% 	2. intermediate trace		[NP e]
%%% 	3. head of nontrivial chain	[NP e]
%%% 	4. all others: S-structure element is also the D-structure element

recoverDsElement(DS,SS) :-
	baseTrace(SS)
	->  headOfChain(SSHead,SS),
	    copyItem1(SSHead,DS),		% elim chain/3 feature
	    inheritPositionFeatures(DS,SS)
	;(  partOfChain(SS)
	    ->  cat(SS,C), 
	        mkNull(C,DS),
		inheritPositionFeatures(DS,SS),
		addFeature(nonarg(+),DS)	  % bare NPs at D-s, nonarguments
	    ;   DS = SS).

%%% CASE THEORY

%%% Declare inCaseAssign

inCaseAssign parser_operation 'Inherent Case Assignment'
	with_components
		io           given_by [ss],
                multiple dep given_by [resolveTraces,thRoleAssign],
		controlType  given_by assigner,
		% optional ..
		abstract     given_by 2.
		
%%% INHERENT CASE ASSIGNMENT AT D-STRUCTURE
%%%
%%% 1.	N,A and P assign inherent Case 
%%%	(gen, gen, and obq (by default), respectively)
%%% 	in parallel with O-role assignment 
%%%	following the Uniformity Hypothesis
%%%
%%% 2.  V assigns inherent Case to indirect object NPs

inCaseAssign in_all_configurations CF where
	inCaseConfig(CF,Case,NP,SNP) 
		then assignICase(NP,Case,SNP).

inCaseConfig(CF,Case,DNP,NP) :-
	cat(NP,np),
	thetaConfig(CF,_,NP),		% potential
	Head head_of CF,
	inherentCaseAssigner(Head,NP,Case),
	recoverDsElement(DNP,NP).

inherentCaseAssigner(Head,NP,Case) :- 	% Case 1
	cat(Head,C),
	assignsInherentCase(C,NP,Case).
inherentCaseAssigner(Verb,NP,Case) :-   % Case 2a
	cat(Verb,C), 
	head(C,v),
	NP has_feature indirectObject,	
	\+ Verb has_feature noInherentCasemark,
	Verb has_feature idoCase(Case).
inherentCaseAssigner(Verb,NP,Case) :- % Case 2b
	Verb has_feature extCase(Case),
	NP has_feature adjunct.
inherentCaseAssigner(Head,_NP,Case) :-	% Case 3
	cat(Head,p),
	(Head has_feature doCase(Case)
	-> true
	;  Case = obq).

% defaults
assignsInherentCase(n1,_NP,gen).
assignsInherentCase(n,_NP,gen).

% wanna block NP in [AP NP [A1 A ..]] from getting inherent Case
assignsInherentCase(a,NP,gen) :- NP has_feature compl.

assignICase(NP,Case,SNP) :-
	NP has_feature case(Slot)
	-> (realizedAsMarker(Case)		  % language-particular
	   -> caseRealizationMode(NP,Mode),	  % language-specific
	      realizeICase(Mode,NP,Case,Slot,SNP)
	   ;  aBarCaseTransmit(_,SNP,Case))
%	   ;  checkMorphCase(NP,Case),
%	      Slot = Case)
	;  SNP has_feature theta(R),		% Theta/Case uniformity
	   notAssigned(R).

% if allowStranding, then permit Case to be realized 
% at the other end of the Chain.

realizeICase(Mode,NP,Case,Slot,SNP) :-
	realizeCase(Mode,NP,Case,Slot)
	-> true
	;  allowStranding,			  % language-particular
	   SNP has_feature case(Slot1),
	   realizeCase(Mode,SNP,Case,Slot1),
	   Case = Slot.

% Modes of Case realization: 
% (1) Morphological: as morphC(Case)
% (2) Case slot: as case(Case)
% (3) (2) + (1): with (2) taking priority

realizeCase(morphC,NP,Case,Case) :-
	ec(NP)
	-> nullCasemarkers			  % language-specific
	;  NP has_feature morphC(MCase),
	   compatibleCase(Case,MCase).
realizeCase(case,NP,Case,Slot) :-
	assigned(Slot)
	-> Case = Slot,
	   checkMorphCase(NP,Case)
	;  nullCasemarkers,
	   ec(NP).
realizeCase(caseMorphC,NP,Case,Slot) :-
	assigned(Slot)
	-> realizeCase(case,NP,Case,Slot)
	;  realizeCase(morphC,NP,Case,Slot).

% check that if NP has morphC, 
% then it is compatible with Case

checkMorphCase(NP,Case) :-
	    compatibleCase(Case,MCase)		  % language-particular
	      if NP has_feature morphC(MCase).

%%% Declare sCaseAssign

sCaseAssign parser_operation 'Assign Structural Case'
	with_components
		io          	given_by [ss],
		dep 		given_by parseSS,
		controlType 	given_by filter,
		% optional ...
		abstract    	given_by 3.

%%% STRUCTURAL CASE ASSIGNMENT AT S-STRUCTURE
%%%
%%%	structural Case is assigned under government (plus case adjacency)
%%%
%%% Assume Case transmission for A-to-A-bar movement only
%%%

sCaseAssign in_all_configurations CF where
	sCaseConfig(CF,Assigner,Case,NP) 
		then assignSCase(Assigner,Case,NP).

% sCaseConfig/4 holds when CF is identified as a structural
% Case assignment configuration with components:
%
%	Head		the structural Case assigner
%	Case		the Case to be assigned
%	NP		the Case receiver

sCaseConfig(CF,Head,Case,XP) :-
	\+ adjoined(CF),
	governs(Head,XP,CF),
	\+ ( cat(CF,vp), XP specifier_of CF),          % new code
	receivesCase(XP),
	\+ XP has_feature indirectObject,	 % inherent Case [Chomsky,KofL]
	caseAssigner(Head,Case),
	adjacent(Head,XP,CF) if caseAdjacency.

receivesCase(XP) :- cat(XP,C), memberchk(C,[np,c2,i2]).

caseAssigner(INFL,Case) :-			  % I(AGR) assigns 
	cat(INFL,i),				  % nominative Case
	\+ INFL has_feature noCasemark(+),
	(INFL has_feature subjCase(Case)
        -> true
        ;  Case = nom).
caseAssigner(Verb,Case) :-			  % Verbs assign Case
	cat(Verb,v),                              % to a direct object
	verbCase(Verb,Case1),
	ecmCase(Verb,Case1,Case).
caseAssigner(ECM,Case) :-			  % ECM complementizer 
	cat(ECM,c),				  % assigns oblique Case.
	ECM has_feature ecm,
	(ECM has_feature ecmCase(Case)
        -> true
    	;  Case = obq).

verbCase(Verb,Case) :-				  % V assigns non-acc Case
	Verb has_feature doCase(Case)		  % if marked o/w default is
	-> true					  % acc.
	;  Case = acc.
        
ecmCase(Verb,Case,Casep) :-
	Verb has_feature ecm(opt)
	-> optional(Case,Casep)
	;  Casep = Case.

% assignSCase: Assigner x Case x Receiver

% assignSCase(ECM,_,_) :-				  % optional Case assignment
%	ECM has_feature ecm(opt),
%	make ECM have_feature noGovernor.	  % for consistency with BT
assignSCase(X,Case,XP) :-
	clause(XP),
	XP has_feature case(Case) if \+ outOfRange(X).
assignSCase(Hd,Case,NP) :-
	cat(NP,np),
	(realizedAsMarker(Case)			  % language-particular
	-> realizeSCase(Hd,NP,Case)
	;  caseMark(Hd,NP,Case)).

outOfRange(X) :- cat(X,v), X has_feature dest(c).

% Case-marking at S-structure
% 	Do Case tranmission for A-to-A-bar movement
% 	For overt NPs, instantiate Case slot
% NB. 1st clause allows other modes of Case transmission

caseMark(Head,NP,Case) :-			
	caseTransmission(Head,NP,Case),		  % language-particular
	!.
caseMark(Head,NP,Case) :-	
	nonCasemarker(Head,NP)
	-> true
	;  plusCaseMark(Head,NP,Case).

% includes A-to-A-Bar Case Transmission

plusCaseMark(Head,NP,Case) :-
	ec(NP), 
	NP has_feature apos,
	antecedent(NP,A),
	\+ A has_feature apos
	-> \+ intermediateTrace(NP),		  % NEW
	   aBarCaseTransmit(Head,A,Case)
	;  checkMorphCase(NP,Case),
	   NP has_feature case(Case).

aBarCaseTransmit(Head,NP,Case) :-
	ec(NP), 
	antecedent(NP,A),
	\+ A has_feature apos
	-> NP has_feature case(Case),		  % touches intermediate trace
	   aBarCaseTransmit(Head,A,Case)
	;  checkMorphCase(NP,Case),
	   NP has_feature case(Case).

realizeSCase(Head,NP,Case) :-
	caseTransmission(Head,NP,Case),		  % language-particular
	!.
realizeSCase(Head,NP,Case) :-
	nonCasemarker(Head,NP)			  % anti-Case
	-> NP has_feature case(Slot),
	   unassigned(Slot)
	;  obligatoryCaseRealization(Head,NP,Case).

% Case-marking is suppressed for:
%
% (1) direct objects if noCasemark(+) is found on the assigner Head
%     NB. this is ignored if direct object takes non-objective Case
% (2) indirect objects if noInherentCasemark is found on the assigner Head

nonCasemarker(Head,NP) :-
	NP has_feature indirectObject
	-> Head has_feature noInherentCasemark
	;  Head has_feature noCasemark(+),
	   \+ Head has_feature doCase(_).	  % only specified for non-acc

obligatoryCaseRealization(Head,NP,Case) :-
	NP has_feature case(Slot),
	(ec(NP)
	-> (allowStranding			  % language-particular
	   ->  Case == Slot if assigned(Slot)
	   ;   (nullCasemarkers			  % language-particular
	       -> caseMark(Head,NP,Case)
	       ;  unassigned(Slot)))
	;  caseRealizationMode(NP,Mode),	  % language-specific
	   realizeCase(Mode,NP,Case,Slot)).

%%% GOVERNMENT

% X0 governs G in category C if
% 	1. X0 is the zero level head of C
% 	2. X0 in {N,V,A,P,I(AGR)}
% 	3. there are no intervening maximal projections between X0 and G
% Also, exceptional government:
%    	i.  comp `for' governs the specifier of IP
%    	ii. ECM head governs the specifier of its infinitival IP complement
%
%       iii. I into Spec-VP

governs(Comp,Spec,CP) :-			  % exceptional government (1)
	cat(CP,c2),
	CP has_feature ecm,
	Comp head_of CP,
	IP complement_of CP,
	Spec specifier_of IP.
governs(ECM,Spec,Proj) :-			  % exceptional government (2)
	\+ adjoined(Proj),
	Proj has_feature ecm(Type),
	ECM head_of Proj,			  % optional government
	XP complement_of Proj,
	nonfiniteClause(XP,Spec),
	checkCase(Spec) if Type == opt.
governs(ECM,Subj,Proj) :-			% governing 'small clause subj'
	\+ adjoined(Proj),
	ECM head_of Proj,
	ECM has_feature ecm,
	XP complement_of Proj,
	smallClause(XP,Subj).
governs(I,Subj,Proj) :-				  % governing into Spec-VP
	\+ adjoined(Proj),
	I head_of Proj,
	I has_feature agr(AGR),
	poorAGR(AGR),
	XP complement_of Proj,
	Subj specifier_of XP.
governs(Head,Gov,Proj) :-			  % regular government
	\+ adjunctionNonABar(Proj),		  % exclude A-bar adjuncts
	Head head_of Proj,
	governor(Head),
	governedIn(Proj,Gov).

smallClause(VP,Subj) :-				% [VPi Subj [VPi ... ]]
	VP has_feature sc(_),			% superfluous?
	adjoined(VP,Subj),
	Subj has_feature apos.

checkCase(X) :- X has_feature case(Case), \+ optionNotTaken(Case).

nonfiniteClause(CP,Spec) :-
	cat(CP,c2),
	IP complement_of CP,
	IP has_feature inf(_),			  % infinitival clause
	Spec specifier_of IP.
nonfiniteClause(IP,Spec) :-
	cat(IP,i2),
	IP has_feature inf(_),
	Spec specifier_of IP.

% Non A-bar adjunction structures are excluded from government
adjunctionNonABar(X) :- 
	adjoined(X,Adjunct),
	\+ Adjunct has_feature apos.

governedIn(Proj,Gov) :-
	X immediate nonprojection_of Proj,
	X ldominates Gov.
governedIn(Proj,Gov) :-
	Proj immediate projection_of X,
	cat(X,C),
	\+ head(C),				  % don't go inside head proj.
	governedIn(X,Gov).

%% lexical heads and I(AGR) are the possible governors

governor(Gov)  :- lexHead(Gov).
governor(INFL) :- cat(INFL,i), INFL has_feature agr(_).
governor(N1)   :- cat(N1,n1).			  % for [NP Spec [N1]]

%%% Declare sBarDeletion

sBarDeletion parser_operation 'S-bar Deletion'
	with_components
		io          given_by [ss],
		dep         given_by parseSS, 
		controlType given_by filter,
		% optional ...
		sCueFilter,
		skippable.

%%% S-BAR DELETION FILTER
%%%	ECM heads are S-bar deleters 

sBarDeletion in_all_configurations CF
	where sBarConfig(CF,Clause) then noSBar(CF,Clause).

sBarConfig(CF,Clause) :-
	\+ adjoined(CF),
	sBarDeleter(CF),
	Clause complement_of CF,
	nonfiniteClause(Clause).

sBarDeleter(X) :- X has_feature ecm(_).

nonfiniteClause(XP) :- nonfiniteClause(XP,_Subject).

noSBar(_,IP) :- cat(IP,i2).
noSBar(CF,CP) :-
	cat(CP,c2),
	nullSpecifier(CP),
	C head_of CP,
	ec(C),					  % empty Complementizer
	make CP have_feature noBarrier if obligSBarDeleter(CF).

nullSpecifier(X) :- Spec specifier_of X -> ec(Spec) ; true.

obligSBarDeleter(X) :- X has_feature ecm(oblig).  % for government

%%% Declare Case Filter

caseFilter parser_operation 'Case Filter'
	with_components
		io           given_by [ss],
		multiple dep given_by [inCaseAssign,sCaseAssign,
				       expletiveLinking],
		controlType  given_by filter,
		% optional ...
		sCueFilter,
		abstract     given_by 1.

%%% CASE FILTER 
%%%	lexical NPs must get Case

caseFilter in_all_configurations CF where
	lexicalNP(CF) then assignedCase(CF).

assignedCase(CF) :- CF has_feature case(Case), assigned(Case).

lexicalNP(NP) :- cat(NP,np), \+ ec(NP).

%%% Declare traceCaseCondition

traceCaseCondition parser_operation 'Case Condition on ECs'
	with_components
		io           given_by [ss],
		multiple dep given_by [inCaseAssign,sCaseAssign],
		controlType  given_by filter,
		% optional ...
		sCueFilter,
		abstract     given_by 1,
		pos.

%%% CASE CONDITION ON CHAINS
%%%
%%% 	[Spec,CP] NP-e in Chain requires Case, 
%%%	NP-traces cannot have Case

traceCaseCondition in_all_configurations CF
	where npTrace(CF) then noCase(CF)
	else specCPNPe(CF,NPe) then assignedCase(NPe).

% who[i] wh-t[i] was arrested np-t[i]

npTrace(T) :-					  % A-to-A movement 
	aposEmptyNP(T),				  % (non-adjunct antecedent)
	isTrace(T),
	antecedent(T,A),
	A has_feature apos,
	\+ A has_feature adjunct.

specCPNPe(CP,NPe) :-
	cat(CP,c2),
	NPe specifier_of CP,
	ec(NPe),
	cat(NPe,np),
	partOfChain(NPe).

noCase(XP) :- XP has_feature case(Case), notAssigned(Case).

%%% MOVEMENT IN SYNTAX

%%% Declare subjacency

subjacency parser_operation 'Subjacency'
	with_components
		io          given_by [ss],
		dep         given_by resolveTraces,
		controlType given_by filter,
		% optional...
		sCueFilter.
		
%%% SUBJACENCY
%%% 	A moved item and its trace are subjacent when they are dominated
%%%	by a common category such that the path between that common category
%%%	and its trace contains fewer than two bounding nodes
%%%
%%% NB. paths are produced by resolveTraces only

subjacency in_all_configurations CF where
	isTrace(CF), upPath(CF,Path) then lessThan2BoundingNodes(Path).

lessThan2BoundingNodes(Path) :-
	boundingNodes(Path,Nodes),
	lessThanTwo(Nodes).

boundingNodes(Path) those X in Path satisfying isBoundingNode(X).

isBoundingNode(X) :- cat(X,C), boundingNode(C), highestSegment(X).

lessThanTwo([]).				  % zero
lessThanTwo([_]).				  % one

%%% Declare resolveTraces

resolveTraces parser_operation 'Trace Theory'
	with_components
		io          	given_by [ss],
		dep		given_by parseSS,
		controlType 	given_by generator,
		constructor 	given_by chainFormation.

% NB. see French periphery for sCaseAssign dependency

%%% TRACE THEORY
%%%   Freely assign NPs to movement chains st.
%%%	1. Overt NPs can only appear as head of chains.
%%%	2. Impossible cases of movement are disallowed:
%%%	(a) In [Xi [Xi] Adjunct], lower Xi cannot appear in any chain.
%%%	(b) If X properly dominates Y, X and Y cannot be in the same chain.
%%%
%%%  Additional stipulation:
%%%     1. Prohibit vacuous empty NPs in A-bar positions.
%%%	(a)  All A-bar empty NPs must be part of a non-trivial chain.
%%%	(b)  No A-bar empty NP can start a non-trivial chain.

resolveTraces(SS) top resolveTraces(SS,[],L,_) st trivialChains(L).

trivialChains(List) each X in List satisfies trivialChain(X).

trivialChain(X) :-
	cat(X,C),
	(C == np
	-> (ec(X)
	   -> \+ isTrace(X), X has_feature apos
	   ;  instantiateChain([X]))
	;  (C == adv
	   -> \+ ec(X)				  % all ec advs must be used
	   ;  instantiateChain([X]))).

% compositional definition maintains two lists for each constituent:
% 1. partial chains
% 2. free NPs

resolveTraces produces [Chains,Free,Constraints]
	cases CF where
	  CF with_constituents X and Y st
   		X produces [ChsX,FrX,CX],
		Y produces [ChsY,FrY,CY],
		CF produces [Chs1,Fr1,C1]
	  then  append(CX,CY,C1),
		crossExtendChains(ChsX,FrX,ChsY,FrY,Chs1,Fr1,C1)
	  finally extendXPChain(CF,Chs1,Fr1,C1,Chains,Free,Constraints)
	else
	  moves(CF,C) then baseCase(C,CF,Chains,Free), Constraints=[].

baseCase(np,CF,Chs,Fr) :- npStart(CF,Chs,Fr).
baseCase(adv,CF,Chs,Fr) :- advStart(CF,Chs,Fr).
% baseCase(c2,CP,[[Item]],[]) :-  phraseToChainItem(CP,Item).

% For NPs: 
% (1) If overt, go on free list
% (2) If ec, either go on free or start a chain
%     ec NPs in A-bar or adjunct A-positions don't start chains

npStart(NP,Chains,Free) :-
	ec(NP)
	-> ecNPStart(NP,Chains,Free)
	;  onFreeList(NP,Chains,Free).

onFreeList(NP,[],[Item]) :- phraseToChainItem(NP,Item).

ecNPStart(NP,Chains,Free) :-
	(NP has_feature apos, \+ NP has_feature adjunct)
	-> phraseToChainItem(NP,Item),
	   optStart(Item,Chains,Free)
	;  onFreeList(NP,Chains,Free).

optStart(Item,[[Item]],[]).
optStart(Item,[],[Item]).

% Adv-traces optionally start a chain
% Overt Wh-Advs optionally start a chain
% Overt non-Wh-Advs don't participate

advStart(Adv,Chains,Free) :-
	ec(Adv)
	-> ecAdvStart(Adv,Chains,Free)
	;  ovAdvStart(Adv,Chains,Free).

ecAdvStart(Adv,Chains,Free) :-
	trace(Adv) 
	-> phraseToChainItem(Adv,Item), 
	   optStart(Item,Chains,Free)
	;  nonParticipant(Chains,Free).

nonParticipant([],[]).

ovAdvStart(Adv,Chains,Free) :-
	Adv has_feature wh(+)
	-> onFreeList(Adv,Chains,Free)
	;  nonParticipant(Chains,Free).

extendXPChain(CF,Chs,Fr,C,Chs,Fr2,C2) :-
	((moves(CF,X),max(X))
	-> adjunctionConstraint(CF,Fr,Fr1),
	   addXP(CF,Chs,Fr1,C,Fr2,C2)
	;  Fr2 = Fr, C2 = C),
	extendChainPaths(Chs,CF),
	extendPaths(Fr,CF).

%% In [Xi ..Xi..], the lower segment Xi must be in the free list.
%% Remove lower segment from free list since lower Xi can never 
%% appear in a non-trivial chain.
%
% Exception: [NP [A crazy] [N John]], N is not on the free list

adjunctionConstraint(X,Fr,Frp) :-
	( adjoined(X,Adjunct,LowerX),
	  cat(LowerX,C), cat(X,C),		% takes care of exception
	  \+ (cat(Adjunct,nq),ec(LowerX)))
	-> phraseToChainItem(LowerX,Item),
	   pick(Item,Fr,Frp)
	;  Frp = Fr.

addXP(XP,Chs,Fr,C,[Item|Fr],Cp) :- 
	chainIDs(Chs,IDs),
	(IDs == []
    	-> C1 = C
    	;  C1 = [not(Item,IDs)|C]),
	cat(XP,K),
	freeECs(Fr,K,ECs),
	(ECs == []
        -> Cp = C1
        ;  Cp = [dom(Item,ECs)|C1]),
	phraseToChainItem(XP,Item).

chainIDs(Chains,IDs) each Chain in Chains and ID in IDs
	satisfies Chain = [Head|_], chainID(Head,ID).

extendChainPaths(List,Node) each Chain in List 
	satisfies Chain = [Head|_], extendPath(Head,Node).

freeECs(List,K) those X in List satisfying ec(X), cat(X,K).

%% subtree chains     Free
%% 1       Cs1 ___.._ F1
%%               _\/
%% 2       Cs2 _/..\_ F2

crossExtendChains(Cs1,F1,Cs2,F2,Chains,Free,Deps) :-
	extendChains(Cs1,F2,F1,Cs1p,F2p,F1p,Deps),    	% leading diagonal
	extendChains(Cs2,F1p,F2p,Cs2p,F1pp,F2pp,Deps),	% trailing diagonal
	appChains(Cs1p,Cs2p,Chains),
	append(F1pp,F2pp,Free).

%% Cs _... OldF
%%      \__ F
%%
%% NB. 	marking is used to ensure that initial extensions can only come from 
%%	the new free list

extendChains(Cs,F,OldF,Cs,F,OldF,_).
extendChains(Cs,F,OldF,Cs2,F2,OldF2,Deps) :-
	Cs \== [],				% optimization
	pickFree(Ext,F,OldF,F1,OldF1),
	extendAChain(Ext,Cs,Cs1,Deps),
	extendChains(Cs1,F1,OldF1,Cs2,F2,OldF2,Deps).

% pick an item from either free list
pickFree(Item,F1,F2,F1p,F2) :- pick(Item,F1,F1p).
pickFree(Item,F1,F2,F1,F2p) :- pick(I,F2,F2p), marked(Item,I). % mark I => Item

% use NP Ext to extend one of the chain in the list (where compatible)
extendAChain(Ext,[Chain|Cs],List,Deps) :-
	extendChain(Ext,Chain,Chain1,Deps),
	addIfIncomplete(Chain1,Cs,List).
extendAChain(Ext,[Chain|Cs],[Chain|Cs1],Deps) :- extendAChain(Ext,Cs,Cs1,Deps).

%% Marking convention: only a new marked element can extend a marked chain

extendChain(New,Chain,Chainp,Deps) :-		
	(marked(New,New1)
	->  marked(Chain,Chain1),		  % only if both marked
	    addChain(New1,Chain1,Chainp1,Deps)
	;(  marked(Chain,Chain1)		 
	    -> addChain(New,Chain1,Chainp1,Deps)  % only chain marked
	    ;  addChain(New,Chain,Chainp1,Deps))),% nothing marked
	marked(Chainp,Chainp1).
	
% Add New to existing Chain
addChain(New,Chain,[New|Chain],Cs) :-
	Chain = [Head|L],
	coindex(New,Head),
	( agreeAGR(New,Head),
	  chainID(Head,ID),
	  constraintsSatisfied(Cs,New,ID,Chain) ) if cat(New,np),
	chainLink(New,Head,UpPath,DownPath),
	chainLinkConditions(New,Head,L,UpPath,DownPath). % periphery

constraintsSatisfied(Cs,New,ID,Chain) each C in Cs 
	satisfies constraint(C,New,ID,Chain).

constraint(not(Item,IDs),New,ID,_) :- \+ idIn(ID,IDs) if Item == New.
constraint(dom(Item,ECs),New,_,Chain) :- \+ common(Chain,ECs) if Item == New.
	
idIn(ID,[ID1|IDs]) :- idIn(ID,IDs) if ID \== ID1.

common(L1,L2) :- member(X,L1), member(Y,L2), sameCategory(X,Y).

appChains(L1,L2,L) :- unMark(L1,L3), unMark(L2,L4), append(L3,L4,L).

% add Chain to the list of incomplete chains only if it is non-maximal

addIfIncomplete(Chain,L,[Chain|L]) :-
	incompleteChain(Chain).
addIfIncomplete(Chain,L,L) :-
	removeMark(Chain,Chain1),
	maximalChain(Chain1),
	instantiateChain(Chain1).

incompleteChain(Chain) :-
	removeMark(Chain,[Head|_]),
	ec(Head),
	cat(Head,C),
	incompleteHead(C,Head).

incompleteHead(adv,_).
incompleteHead(np,Head) :- Head has_feature ec(Type), Type \== op.

% A chain is maximal if it is headed by:
% 1. an overt element, or
% 2. an empty operator
% (3. PRO/pro - don't use this just yet.)

maximalChain([Head,_Trace|_RestOfChain]) :- canHeadChain(Head).

canHeadChain(Item) :- \+ ec(Item).		  % overt items
canHeadChain(X) :- emptyNP(X), X has_feature apos. % was PRO
canHeadChain(Op) :-				  % empty operator
	emptyOperator(Op),			  % defined positionally
	\+ Op has_feature apos.

emptyOperator(Op) :-
	emptyNP(Op),
	Op has_feature_set [ec(op),a(A),p(P)],
	notAssigned(A),
	notAssigned(P).

%%% Declare whInSyntax

whInSyntax parser_operation 'Wh-movement in Syntax'
	with_components
		io          given_by [ss],
		dep         given_by parseSS,
		controlType given_by filter,
		% optional ...
		sCueFilter,
		skippable,
		abstract    given_by 1,
		pos.

%%% SYNTACTIC WH-MOVEMENT FILTER
%%% 	When whInSyntax parameter holds
%%%	
%%%	If Comp headed by a [+wh] element then [+wh] Comp 
%%%	Otherwise Q cannot be present

whInSyntax in_all_configurations CF 
	where cat(CF,c2) then whCompFilter(CF) if whInSyntax.

whCompFilter(CP) :- 
	Spec specifier_of CP
	-> (Spec has_feature wh(+) 
	   -> CP has_feature wh(+)
	   ;  whMinus(CP))
	;  nonQComp(CP).

nonQComp(CP) :- whMinus(C0) if (C0 head_of CP, ec(C0)).  % allow overt inv

% [-wh] or [+wh] if separately licensed
whMinus(X) :- X has_feature wh(-) -> true ; X has_feature licensed(wh).

%%% AGR CRITERION
%%%
%%% Rich AGR iff Spec-IP has a R-NP

agrCriterion parser_operation 'AGR Criterion'
	with_components
		io          given_by [ss],
		dep         given_by resolveTraces,
		controlType given_by filter,
		% optional...
		sCueFilter.

agrCriterion in_all_configurations CF where
	specIP(CF,Spec) then richAGRiffRNP(Spec,CF).

richAGRiffRNP(Spec,IP) :-
	IP has_feature agr(AGR),
	poorAGR(AGR) iff expletive(Spec).

expletive(X) :- X has_feature nonarg(+).

rNP(X) :- \+ ( X has_feature nonarg(+) ; possibleEmptyExpletive(X)).

richAGR(X) :- \+ unspecifiedForNumber(X).	  % also called by sCase
poorAGR(X) :- unspecifiedForNumber(X).

%%% BINDING THEORY


%%% Declare freeIndexing

freeIndexing parser_operation 'Free Indexation'
	with_components
		io          given_by [ss],
		dep         given_by resolveTraces,
		controlType given_by generator.
		
%%% FREE INDEXING
%%%	Assign indices freely to NPs in A-positions.

freeIndexing(CF) :-
	personalPronouns(CF,_),
	freeIndexing1(CF,_,_).

%%% Coindex 1st (and 2nd) person pronouns/anaphors
%%
%% possessive pronouns have 2 readings: anaphor and pronoun
%% 3rd person possessive pronouns are ambiguous wrt binding 
%% but 1st and 2nd person possessive pronouns are not..   
%%      
%% In the stmt, 'I gave MY books to Bill', MY is an anaphor only
%% whereas in 'he gave MY books to Bill', MY is a pronoun only
%%
%% If anaphor reading is possible for 1st and 2nd person poss pronouns,
%% pronoun reading is not possible..

personalPronouns on Is in_all_configurations CF 
	where cat(CF,np), \+ unspecifiedForAGR(CF), 
	      personalPronoun(CF,Is,J) 
		then index(CF,J).

% need to prevent (all) empty NPs from being assimilated into 
% personal pronouns
unspecifiedForAGR(X) :-	
	X has_feature agr(AGR),	
	(unassigned(AGR) 
	-> true
	;  unspecifiedForPerson(AGR)).

unspecifiedForAGR(X) :-	X has_feature agr(AGR),	unassigned(AGR).

personalPronoun(X,[I,_,_,_],I) :- intersectAGR(X,[1,sg,[m,f]]).
personalPronoun(X,[_,I,_,_],I) :- intersectAGR(X,[2,sg,[m,f]]).
personalPronoun(X,[_,_,I,_],I) :- intersectAGR(X,[1,pl,[m,f]]).
personalPronoun(X,[_,_,_,I],I) :- intersectAGR(X,[2,pl,[m,f]]).

freeIndexing1 produces [INPs,Cs]
	cases CF where
	CF with_constituents X and Y st
		X produces [XNPs,CXs],
		Y produces [YNPs,CYs],
		CF produces [CFNPs,CCFs]
	then crossIndex(XNPs,YNPs), 
	     constrainFI(CXs,CYs,CCFs),
	     unionWrtI(XNPs,YNPs,CFNPs)
	finally freelyIndexIfNP(CF,CFNPs,CCFs,INPs,Cs)
	else aposNP(CF) then generateIndex(CF,INPs,Cs).

aposNP(NP) :- cat(NP,np), NP has_feature apos, \+ NP has_feature adjunct.

generateIndex(NP,List,Cs) :-
	index(NP,_),
	(NP has_feature noCoindex		  % non-participant in indexing
	-> List = []
	;  List = [NP] ),
	(NP has_feature neq(I,J)
	-> Cs = [(I,J)]
	;  Cs = []).
		
% if constituent is an NP, then it participates in free-indexing
freelyIndexIfNP(NP,IndexedNPs1,Cs1,IndexedNPs,Cs) :-
	aposNP(NP)
	-> generateIndex(NP,List,Cs2),
	   crossIndex(List,IndexedNPs1),
	   constrainFI(Cs2,Cs1,Cs),
	   unionWrtI(List,IndexedNPs1,IndexedNPs)
	;  IndexedNPs = IndexedNPs1,
	   Cs = Cs1.

% cross-indexes two lists of NPs by freely coindexing those NPs in NPs1
% that are not in NPs2 with those NPs in NPs2 not in NPs

crossIndex(NPs1,NPs2) :-
	diffWrtI(NPs1,NPs2,NPs3),
	diffWrtI(NPs2,NPs1,NPs4),
	freelyCoindex(NPs3,NPs4).

% freelyCoindex(Items1,Item2) optionally coindexes pairs of items from
% Items1 and Items2

freelyCoindex([],_).
freelyCoindex([NP|L],NPs) :-
	optionallyCoindex(NP,NPs,NPsp),
	freelyCoindex(L,NPsp).

optionallyCoindex(NP1,NPs,NPs1) :-
	pick(NP2,NPs,NPs1),
	agreeAGR(NP1,NP2),
	coindex(NP1,NP2).
optionallyCoindex(_,NPs,NPs).

constrainFI([],Cs,Cs) :-
	constrainFI(Cs).
constrainFI([C|Cs],Cs1,[C|Cs2]) :-
	C = (I,J),
	I \== J,
	constrainFI(Cs,Cs1,Cs2).

constrainFI(List) each X in List satisfies X=(I,J), I \== J.

unionWrtI([],S,S).
unionWrtI([Item|Is],S,Sp) :-
	Item has_feature index(I),
	((indexOccursIn(S,I) ; indexOccursIn(Is,I))
	->  unionWrtI(Is,S,Sp)
	;   Sp=[Item|S1],
	    unionWrtI(Is,S,S1)).

diffWrtI([],_,[]).
diffWrtI([Item|Is],S,Sp) :-
	Item has_feature index(I),
	(indexOccursIn(S,I)
	->  diffWrtI(Is,S,Sp)
	;   Sp=[Item|S1],
	    diffWrtI(Is,S,S1)).

indexOccursIn(List,I) exists X in List 
	satisfying X has_feature index(J), sameIndex(I,J).

%%% Declare coindexSubjAndINFL

coindexSubjAndINFL parser_operation 'Coindex Subject'
	with_components
		io          given_by [ss],
		dep         given_by parseSS,
		controlType given_by filter.
		
%%% SUBJECT COINDEXATION
%%%	(1) Subject and Infl are always coindexed.

coindexSubjAndINFL in_all_configurations CF
	where specIP(CF,Subject) then coindexSubjAndINFL(Subject,CF).

specIP(IP,Subject) :- cat(IP,i2), Subject immediate specifier_of IP.

coindexSubjAndINFL(Subj,IP) :-
	coindex(Subj,IP),
	make IP have_feature indexed(agr).	  % signals for agreement

%%% Declare Expletive Linking

expletiveLinking parser_operation 'Expletive Linking'
	with_components
		io          given_by [ss],
		dep 	    given_by resolveTraces,
		controlType given_by filter. % assigner

%%% EXPLETIVE LINKING
%%%	Subject[nonarg(+),linkTo(XP)] 
%%%	Non-argument subject must be linked to a local complement/adjunct XP
%%%	VP-internal subject version
%%%
%%% Notes:
%%%	1. Case transfer between NPs
%%%	2. Coindexation between NP and clause for Binding theory
%%%	3. Linking done between last element of expletive Chain 
%%%	   (allows expletive raising)

expletiveLinking in_all_configurations CF
	where linkConfig(CF,Subject,XP) then expletiveLink(Subject,XP).

linkConfig(VP,Subj,XP) :-
	expletiveSubjChain(VP,Subj,C),
	linkPhrase(VP,C,XP).

linkConfig(CP,DummyWh,XP) :-
        cat(CP,c2),
	DummyWh specifier_of CP,
        DummyWh has_feature linkTo(wh),
	\+ DummyWh has_feature wh(+), % then it's already linked
	partialWhConfig(CP,DummyWh,XP).

partialWhConfig(CP,DummyWh,XP) :-
        cat(CP,c2),
	DummyWh specifier_of CP,
        DummyWh has_feature linkTo(wh),
	\+ DummyWh has_feature wh(+), % then it's already linked
        findThetaVP(CP,ThetaVP),
        !,
        has_constituent(ThetaVP,LowerCP),
        cat(LowerCP, c2),
        XP specifier_of LowerCP,
        true if partialWhConfig(LowerCP,XP,_YP). % side-effect: gets wh(+) for Dummy

expletiveSubjChain(XP,Subj,C) :-
	specMax(XP,X),
	(partOfChain(X)
	-> baseTrace(X),
	   headOfChain(Subj,X),
	   expletive(Subj,C)
        ;  expletive(X,C),
	   Subj = X).

% should work for VP, AP, ...
% need to eliminate the \+adjoined/1 restriction for 
% [AP [AP Spec [A1 tough] [C2..]]]
% consequence: we consider all segments now => possible multiple linking

specMax(XP,Spec) :-
%	\+ adjoined(XP),
	cat(XP,C),
	max(C),
	Spec specifier_of XP.

expletive(X,C) :-
	X has_feature nonarg(+),
	X has_feature linkTo(C).

findThetaVP(X,VP) :-
	Y complement_of X,
	cat(Y,C),
	(C == vp 
    	-> identifyThetaVP(X,VP)
        ;  memberchk(C,[i2,negp]),
	   findThetaVP(Y,VP)).
	    
% constituents of local clause only: see [Chomsky,KofL]
linkPhrase(XP,C,CP) :- CP complement_of XP, cat(CP,C).
% linkPhrase(XP,C,CP) :- XP subcategorizes_for YP, linkPhrase(YP,C,CP).
linkPhrase(XP,C,CP) :- YP complement_of XP, linkPhrase(YP,C,CP).
linkPhrase(XP,C,CP) :- adjoined(XP,CP), cat(CP,C).
	
expletiveLink(X,Y) :- 
	clause(Y) 
	-> coindex(X,Y)	
	; ( X has_feature linkTo(wh)         %%%%%%%%%%%%%%%%%%%%%%%
	    -> (addFeature(wh(+),X),         % This should all be
	       addFeature(wh(-),Y),          % replaced by a chain
               coindex(X,Y),                 % linking, but I wasn't
	       Y has_feature case(Case),     % able to do it.
	       Y has_feature theta(Theta),   %%%%%%%%%%%%%%%%%%%%%%%
	       X has_feature case(Case1)
	         -> Case1 = Case
	         ;  addFeature(case(Case),X),
	       X has_feature theta(Theta1)
	         -> Theta1 = Theta
	         ;  addFeature(theta(Theta),X),
	       addFeature(nonarg(+),X))
            ;  agreeAGR(X,Y),
	       X has_feature case(Case),
	       Y has_feature case(Case) ).



%%% Declare functionalDet

functionalDet parser_operation 'Functional Determination'
	with_components
		io          given_by [ss],
		dep         given_by freeIndexing,
		controlType given_by assigner.
			
%%% FUNCTIONAL DETERMINATION OF EMPTY CATEGORIES

% free empty NPs in A-positions must be [+P]
functionalDet(CF) top functionalDet(CF,IDoms) st pronouns(IDoms).

pronouns(Doms) each Dom in Doms 
	satisfies Dom has_components [P|_], pronoun(P).

% For proDrop, allow pro[nonarg(+)]
% Note: *PRO[nonarg(+)]

pronoun(P) :-
	P has_feature nonarg(+)
	-> proDrop, P has_feature_set [p(+),a(-)]
	;  P has_feature p(+), P has_feature a(+) if \+ proDrop.
	
functionalDet in_all_configurations CF 
	where aposEmptyNP(CF) 
		then localBinderDom(CF,Dom),
		     Dom has_components [_,Binder],
		     setBindingFs(Binder,CF,Dom).

aposEmptyNP(NP) :- 
	emptyNP(NP), NP has_feature apos, \+ NP has_feature nonarg(+).

localBinderDom(X) smallest_configuration CF
	with_components
		X,
		B given_by bindsFD(B,X,CF).

bindsFD(B,X,S) :- cat(B,np), binds(B,X,fD,S), \+ aBarImTrace(B).

%	(aBarImTrace(B) -> nl, write('ABITr: '), brprI(B), write(' binds '),
%	brprI(X), write(' in '), brprI(S),nl, fail
%        ; true).

aBarImTrace(X) :- intermediateTrace(X), \+ X has_feature apos.

% B is the local binder of A. Cases:
% 	1. B is in A-bar position and is an operator
%	   => -A -P (variable).
%	2. B is in A-bar position, but not an operator 
%	   => +A -P (anaphor) or -A -P
%	3. B is in A position, and has an independent O-role 
%	   => +A +P (PRO) or -A +P (pro)
%	4. B is in A position, shares O-role with A 
%	   => +A -P (anaphor) or -A -P

setBindingFs(Binder,Bindee,CF) :-
	Binder has_feature apos
	-> setABoundFs(Binder,Bindee)
	;  setABarBoundFs(Binder,Bindee,CF).

setABarBoundFs(Binder,Bindee,CF) :-		
	( operator(Binder)			  % A-bar bound by an operator
	; cat(CF,C),				% cheat: English topicalization
	  max(C))
	-> \+ Bindee has_feature nonarg(+),	  % constrained?
	   variable(Bindee),
	   make Bindee have_feature operator(Binder) % (see Condition C)
	;  Bindee has_feature p(-),		% A-bar bound, but not by an operator
	   Bindee has_feature a(+) if \+ proDrop.

setABoundFs(Binder,Bindee) :-			
	partOfSameChain(Binder,Bindee)		% binder and bindee share O-roles
	-> Bindee has_feature p(-),
	   Bindee has_feature a(+) if \+ proDrop
	;  mostlyPro(Bindee).

mostlyPro(Bindee) :-
	\+ Bindee has_feature nonarg(+),		% independent O-roles
	Bindee has_feature p(+),
	Bindee has_feature a(+)  if \+ proDrop.
mostlyPro(Bindee) :-
	anaphorDrop,
	\+ partOfChain(Bindee),			% pure anaphors only 
	Bindee has_feature p(-),
	Bindee has_feature a(+).

%% A c-commands B in S

c_commands(A,B,S) :-
	S has_constituents Cs,
	member(A,C,Cs),
	C dominates B.
c_commands(A,B,S) :-
	S has_constituent C,
	c_commands(A,B,C).

%%% EXTENDED BINDING
%%%	Allow binding to be extended for non-c-commanding binders, 
%%%	specifically to:
%%%	(1) adjuncts in the case of adjunction to the c-commanding element
%%%	    provided the c-commander is marked to be transparent.
%%%	    NB. Needed for ECP (heads) and for operator/variable licensing.
%%%
%%%     K is the transparency key.

binds(A,B,K,CF) :-
	c_commands(A1,B,CF),
	binder(A,K,A1),
	coindexed(A,B).

binder(X,_,X).
binder(X,bT,Y) :- 
	cat(Y,pp), cat(X,np),
	Y has_constituent X.
binder(X,K,Y)  :- 
	Y has_feature transparent(K),	
	adjoined(Y,Adjunct,Yp),
	(binder(X,K,Adjunct) ; binder(X,K,Yp)).
	
coindexed(A,B) :-
	A has_feature index(I), 
	B has_feature index(J), 
	sameIndex(I,J).

dominates(A,B) :-
	sameCategory(A,B).
dominates(A,B) :-
	A has_constituent C,
	dominates(C,B).

dominates(A,B,CF) :-
	dominates(CF,B),
	A = CF.
dominates(A,B,CF) :-
	CF has_constituents L,			% CF has_constituent CFp
	member(CFp,L),				% to fool compiler
	dominates(A,B,CFp).

%%% GOVERNING CATEGORY PREDICATES
%%% 	GC(A) is the minimal GC domain that contains:
%%% 		1. A, and
%%% 		2. a governor of A, and
%%% 		3. accessible SUBJECT
%%% 	where
%%%		GC domain is IP or NP
%%%		SUBJECT = subject + INFL(AGR)
%%%     and	B accessible to A if
%%%     		1. B c-commands A, and
%%%     		2. B is not coindexed with any category 
%%%			   properly containing A.
%%%
%%% NB. Require same government relations to be preserved for Binding Theory
%%%     and Case Theory when optionality arises.
%%% NB. Assume highest segment for GC domain.

%%% Governing category for pronominals, gcprime(X), is just the smallest
%%% NP or IP category surrounding them.                new code

% theory parameter
gcDomain(i2).
gcDomain(np).

gc(X) smallest_configuration CF st cat(CF,C), gcDomain(C), highestSegment(CF)
	with_components
		X,
		G given_by governs(G,X,CF),
		S given_by (accSubj(S,X,CF) ; auxiliaryHypothesis(S,G,CF)).


gcprime(X) smallest_configuration CF st cat(CF,C), gcDomain(C), 
         highestSegment(CF)
         with_components
         X, 
         G given_by governs(G,X,CF).        %new code


auxiliaryHypothesis(S,Gov,CF) :- (matrixIP(CF), assigned(Gov)) -> S = found.

matrixIP(X) :- cat(X,i2), X has_feature matrix.

accSubj(Subj,A,CF) :-				% Subj is accessible to A
	bigSubject(Subj,CF),
	c_commandsBT(Subj,A,CF),
	\+ coindexedIn(Subj,A,CF).
	
bigSubject(SUBJ,XP) :- subject(SUBJ,XP).	% ordinary subject
bigSubject(AGR,IP) :-				% I(AGR)
	cat(IP,i2),
	IP has_feature agr(_),
	AGR head_of IP.

subject(SUBJ,IP) :- cat(IP,i2),	SUBJ specifier_of IP. 		    % IP subj
subject(SUBJ,NP) :- cat(NP,np),	cat(SUBJ,np), SUBJ specifier_of NP. % NP subj

% normal c-command + I(AGR) c-commands [Spec,IP]

c_commandsBT(A,B,S) copy_of c_commands(A,B,S) with_clause (
c_commandsBT(AGR,NP,IP) :-
	cat(IP,i2),
	IP has_feature agr(_),
	NP specifier_of IP,
	AGR head_of IP
) prepended.

coindexedIn(X,A,YP) :-
	X has_feature index(I),
	downPath(YP,A,Path),
	member(Z,Path),
	accSubjRelevant(Z),
	Z has_feature index(J),
	sameIndex(I,J).
	
downPath(X,X,[]).
downPath(X,Y,[X|P]) :-
	X has_constituent Z,
	downPath(Z,Y,P).

accSubjRelevant(X) :- cat(X,C), accSubjIndexCategory(C).

accSubjIndexCategory(c2).
accSubjIndexCategory(np).


%%% Declare conditionA

conditionA parser_operation 'Condition A'
	with_components
		io           given_by [ss],
		multiple dep given_by [functionalDet,sCaseAssign,
				       expletiveLinking],
		controlType  given_by filter,
		% optional ...
		sCueFilter,
		skippable.

%%% BINDING THEORY CONDITION A: An anaphor must be A-bound in its GC
%%% (can be satisfied by PRO without a GC)

conditionA in_all_configurations CF
	where assuming anaphor(CF) then gc(CF,GC), aBound(CF,GC) holds.

within anaphor(NP) :- 
		subjToBT(NP), 
		NP has_feature a(A) assume A to_be '+' over '-'.

subjToBT(X) :- 
	cat(X,np), 
	(ec(X) 
	-> X has_feature apos
	;  highestSegment(X)).
	
aBound(B,S) :- aBinds(_A,B,S).
              
	
%%% Declare conditionB

conditionB parser_operation 'Condition B'
	with_components
		io           given_by [ss],
		multiple dep given_by [functionalDet,sCaseAssign,
				       expletiveLinking],
		controlType  given_by filter,
		% optional ...
		sCueFilter,
		skippable.

%%% BINDING THEORY CONDITION B: A pronominal must be A-free in its GC 
%%% (if GC doesn't exist, then it may be bound)

conditionB in_all_configurations CF            %new code
	where pronominal(CF) then gcprime(CF,GC), \+ aBound(CF,GC).

pronominal(NP) :- subjToBT(NP), NP has_feature p(+).
                 

%%% Declare conditionC

conditionC parser_operation 'Condition C'
	with_components
		io          given_by [ss],
		dep         given_by functionalDet,
		controlType given_by filter,
		% optional ...
		sCueFilter.

%%% BINDING THEORY CONDITION C: An R-expression must be A-free (in the
%%%				domain of the head of its nontrivial chain)

aBinds(A,B,S) :- binds(A,B,bT,S), A has_feature apos.

aBinderDom(X) smallest_configuration CF
	with_components
		X,
		A given_by aBinds(A,X,CF).
	
conditionC in_all_configurations CF
	where rExpr(CF) then aBinderDom(CF,Dom), aFreeCond(CF,Dom).

rExpr(NP) :- subjToBT(NP), NP has_feature_set [a(-),p(-)].

% only way that R-expr can be A-bound is if it's A-bound outside the domain 
aFreeCond(X,D) :-
	variable(X),
	X has_feature operator(Op),		% [D .. [D1 ..Op...] ..]
        emptyOperator(Op),
	D has_constituent D1,
	properlyDominates(D1,Op).

aFreeCond(X,D) :-
        antecedent(X,Op),
	reanalyzedAsOp(Op),			% reanalysis of trace
	D has_constituent D1,
	properlyDominatesA(D1,Op).

properlyDominates(X,Y) :- \+ sameCategory(X,Y), X dominates Y.

reanalyzedAsOp(Op) :-		
	emptyNP(Op),
	Op has_feature_set [op_ok,ec(trace),a(A),p(P)],
	notAssigned(A),
	notAssigned(P).

properlyDominatesA(X,Y) :- \+ unifiable(X,Y), dominatesA(X,Y).

dominatesA(X,Y) :- unifiable(X,Y).
dominatesA(X,Y) :- X has_constituent Z, dominatesA(Z,Y).

%%% Declare control

control parser_operation 'Control'
	with_components
		io          given_by [ss],
		dep 	    given_by functionalDet,
		controlType given_by filter.

%%% CONTROL THEORY
%%%   Basically:
%%%	PRO is controlled by the nearest appropriate binder (if one exists)
%%%   Modifications:
%%%   (1) Substitute appropriate "m-binder" for appropriate binder.
%%%   (2) Reconstruction required for clausal extraposition
%%%   (3) Intermediate traces can't be m-binders
%%%   Temporarily: do small pro checking here too.

control in_all_configurations CF where
	controlConfig(CF,_) then controlDom(CF,Dom), 
				 Dom has_components [_,PRO,NP],
				 controlledPRO(PRO,NP).
	
controlConfig(IP,PRO) :-
	cat(IP,i2),
	\+ partOfChain(IP),
	PRO specifier_of IP,
	bPRO(PRO).
controlConfig(IPt,PRO) :-
	cat(IPt,i2),
	isTrace(IPt),
	antecedent(IPt,IP),
	PRO specifier_of IP,
	bPRO(PRO).

controlDom(X) smallest_configuration CF
	with_components
		X,
		PRO given_by controlConfig(X,PRO),
		C given_by potentialController(C,PRO,X,CF).

potentialController(NP,PRO,X,S) :-
	m_commands(NP,PRO,X,S),
	\+ aBarImTrace(NP),
	\+ NP has_feature noControl.

m_commands(A,B,X,S) :-
	S has_constituents L,
	member(C,D,L),
	C ldominates A,
	cat(A,np),				% A unknown, must come here
	dominatesSub(D,B,X).
m_commands(A,B,X,S) :-
	S has_constituent T,
	m_commands(A,B,X,T).

% same as dominates/2 except blocked by an intervening maximal projection
X ldominates Y :- sameCategory(X,Y).
X ldominates Y :-
	cat(X,C), \+ max(C),
	X has_constituent Z,
	Z ldominates Y.

% Modified dominates for reconstruction
dominatesSub(D,A,Sub) :-
	isTrace(Sub)
	-> D dominates Sub
	;  D dominates A.

controlledPRO(PRO,NP) :-
	(partOfNonargumentChain(NP)
	-> \+ coindexed(PRO,NP)
	;  (\+ NP has_feature noControl
	   -> coindexed(PRO,NP) if \+ operator(NP))).

% Need to account for 
% [IP it[nonarg(+)] [VP t [V2 ..PRO..]]]
% where t m-commands PRO and t is part of a chain headed by 'it'.

partOfNonargumentChain(NP) :- 
	NP has_feature nonarg(+)
        -> true
        ;  partOfChain(NP),
	   headOfChain(Head,NP),
	   Head has_feature nonarg(+).

%%% Declare ecp

ecp parser_operation 'ECP'
	with_components
		io           given_by [ss],
		multiple dep given_by [freeIndexing,sBarDeletion],
		controlType  given_by filter,
		% optional ...
		sCueFilter.

%%% EMPTY CATEGORY PRINCIPLE (ECP)
%%%
%%%	An empty category must be properly governed
%%%	Proper government holds in two cases:
%%%	1. Lexical government: (government by a lexical head)
%%%	2. Antecedent government: an empty category may be bound by its 
%%%	   antecedent unless excluded by a barrier
%%%	Properly governed elements are marked with feature gamma(+).
%%%
%%%	Notes:
%%%	1. [C], PRO, and empty operators are not subject to the ECP
%%%	2. CP and NP are barriers
%%%	   However antecedent government into spec of CP is allowed
%%%	   Under S-bar deletion, CP is no longer a barrier
						
ecp in_all_configurations CF where
	subjectToECP(CF) 
		then must_satisfy lexGoverned(CF) ; aGovDom(CF,_).

subjectToECP(X) :- ec(X), X has_feature apos, \+ exceptionToECP(X,ss).

exceptionToECP(X,Level) :- X has_feature noECP(Level). 
exceptionToECP(X,_) 	:- cat(X,c).		  % null [C]
exceptionToECP(X,_) 	:- emptyOperator(X).	  % Op
exceptionToECP(X,_) 	:- bPRO(X).		  % PRO
exceptionToECP(X,_) 	:- emptyNP(X), X has_feature nonarg(+). % expletive

aGovDom(X) smallest_configuration CF under barrier(CF,X)
	with_components
		X,
		B given_by bindsECP(B,X,CF).
  
bindsECP(X,Y,CF) :- 
	binds(B,Y,ecp,CF), 
	segmentOf(X,B),
	antecedentOf(Y,X),
	\+ in_CED_config(Y,CF),            %new code   
	\+ X has_feature noECP(ss),
	gammaMark(Y).

in_CED_config(Y,CF):-                         
        dominates(Adjunct,Y,CF),
	\+ sameCategory(Adjunct,Y),
        \+ Adjunct projection_of Y,
%        \+ projStar(Y,Adjunct),   
        Adjunct has_feature adjunct.       %new code.  Need to add about
                                        %head adjunction and aux adj

gammaMark(X) :- make X have_feature gamma(+).

antecedentOf(X,A) :- antecedent(X,A).
antecedentOf(X,Y) :-				  % Head Movement fix
 	isTrace(X), 
 	coindexed(X,Y), 
 	cat(X,Ci), 
 	cat(Y,C),
	head(C),
 	projStar(C,Ci).

% things might have been adjoined to this element
heads(X,X).
heads(X,Y) :- adjoined(Y,_,LowerSeg), heads(X,LowerSeg).

barrier(B,X) :- potentialBarrier(B), \+ ( intoSpec(B,X) ; noBarrier(B) ).
%barrier(B,X) :- cat(B,np), \+ segmentOf(X,B).

potentialBarrier(B) :- (cat(B,np) ; cat(B,c2)), highestSegment(B).

intoSpec(B,X) :- X specifier_of B.

noBarrier(B) :- B has_feature noBarrier.

%% Warning: semantics of this is wrong, it just gets tested once, if it fails
%% that's it. Should be repeatedly tested until it succeeds

lexGoverned(X) exists_some_configuration CF where 
	governsECP(G,X,CF), 
	lexicalGovernor(G,X),
	gammaMark(X).         %  don't comment out--test   

governsECP(G,X,CF) :- governs(G,X,CF).

%% Warning: not right. Want to say X is LexG if CF if LexG. Fix above
%% semantics, will get automatic fix for this.

governsECP(_G,X,CF) :-  % to account for the case [NP NP-t]
	adjoined(CF,_,X).

lexicalGovernor(G,_) :- 
	lexHead(G).
lexicalGovernor(G,XP) :-			% for pro (subj pos) 
	proDrop,				% source: (?) [vanR&W]
	cat(G,i), 
	G has_feature agr(_),
	\+ isTrace(XP).				% subject can't be a trace

%%% LF

%%% Declare lfMovement

lfMovement parser_operation 'LF Movement'
	with_components
		io          given_by [ss,lf],
		dep         given_by resolveTraces,
		controlType given_by generator.

%%% LF MOVEMENT
%%%	Two types:
%%%	1. Quantifier Raising (QR): only Type II Qs (op(+)) are subject to this
%%%	2. Wh Raising: wh elements only

lfMovement(SS,LF) :-
	qr(SS,SS1),
	checkIsomorphic(SS1) if isomorphicPrinciple,  % (Huang 1982)
	moveWh(SS1,LF).

% QR is an (optional) local movement operation. type II Qs adjoin to
% the most proximate IP-node. No successive cyclic movement is possible
% (to maintain scope distinctions)

qr(X,Xp) :- raiseOneQ(X,Xp), Xp is_substituting_for X.
qr(X,X).

raiseOneQ(IP,IP3) :-
	highestIPsegment(IP),
	X opaque_when highestIPsegment(X) 
    	extract quantifier(_) from IP producing IP1 and [Q,Var],
	Var has_feature ec(qr),
	instantiateChain([Q,Var]),
	addFeature(moved(qr),Q),
	raiseOneQ(IP1,IP2),
	phraseToChainItem(Qp,Q),
	adjoinPhrase(Qp,IP2,IP3).

raiseOneQ(XP,XP) :- highestIPsegment(XP).
raiseOneQ(XP,XP1) :-
 	exists LeadsToQ in XP substitutes_for Raised in XP1 
        satisfying raiseOneQ(LeadsToQ,Raised), \+ LeadsToQ = Raised.

quantifier(X) :- cat(X,np), X has_feature op(+).

highestIPsegment(IP) :- cat(IP,i2), highestSegment(IP).

%% Isomorphic Principle (for Mandarin Chinese)
%% Huang 1982: 
%%
%%	if QP A c-commands B at SS, then it must do so at LF as well.
%%
%% Implementation: just check the trace list and the moved QR list
%% to see if they're compatible.

checkIsomorphic(SS1) :-
	qrT(SS1,TIs),
	qrQ(SS1,QIs),
	TIs == QIs.

qrT collect I in_all_configurations CF 
	where CF has_feature ec(qr), CF has_feature index(I).

qrQ collect I in_all_configurations CF 
	where CF has_feature moved(qr), CF has_feature index(I).

%% LF wh-movement (optionally) moves an element with feature [wh] into
%% [spec,COMP] (or adjoins to [Spec,COMP] if [Spec,COMP] is already occupied

moveWh(X,Y) :-
	moveWhs(X,Y,Chains),
	instantiateChains(Chains).		% put in chain features

moveWhs(X,X,[]).				% movement is optional
moveWhs(X,Y,Chains1) :-
	moveOneWh(X,Xp,Chain,noblock),
	Xp is_substituting_for X,
	moveWhs(Xp,Y,Chains),
	mergeChain(Chain,Chains,Chains1).

instantiateChains(List) each X in List satisfies instantiateChain(X).
	
moveOneWh(CP,CPp,Chain,noblock) :-		% raise one wh from within IP to this CP
	cat(CP,c2),
	IP complement_of CP,
	extract whLF(_) from IP producing IPp and Chain,
	Chain = [Wh,Trace],
	phraseToChainItem(Whp,Wh),
	Trace has_feature ec(wh),
	addToCP(Whp,IPp,CP,Chain,CPp),
	addFeature(blocked,CPp).
moveOneWh(XP,XPp,Chain,B) :-
	exists LeadsToWh in XP substitutes_for Raised in XPp 
        satisfying propagateBlocking(XP,B,Bp),
	           moveOneWh(LeadsToWh,Raised,Chain,Bp),
		   \+ LeadsToWh = Raised.

% nb. from moveWhs/3 - assume SCh (simple chain) built before Cs
mergeChain(Ch,[],[Ch]).				  % unmatched
mergeChain(SCh,[Ch|Cs],[Ch1|Cs1]) :-
	SCh = [Head,Tr],
	Ch = [Head1|_],
	(coindexed(Head,Head1)
	-> append(Ch,[Tr],Ch1),
	   Cs1 = Cs
	;  Ch1 = Ch,
	   mergeChain(SCh,Cs,Cs1)).

% strict cyclicity - put blocks on each CP from which a wh-element was raised
propagateBlocking(CP,Block,Block1) :-
	( cat(CP,c2),
	  Block = noblock,
	  CP has_feature blocked )
	-> Block1 = blocked
	;  Block1 = Block.

inComp(X,CP) :- Spec specifier_of CP, inComp1(X,Spec).
inComp(X,CP) :- C0 head_of CP,        inComp1(X,C0).

inComp1(X,X).
inComp1(X,CF) :- adjoined(CF,Adjunct),	inComp1(X,Adjunct).
inComp1(X,CF) :- adjoined(CF,_,CFp),	inComp1(X,CFp).

% adds a wh-NP to [Spec,CP] by substitution or adjunction
addToCP(Wh,IP,CP,Chain,CPp) :-			  
	addFeature(moved(lf),Wh),
	(Spec specifier_of CP
	-> adjoinSpecCP(Wh,IP,CP,Spec,Chain,CPp)
	;  substituteSpecCP(Wh,IP,CP,Chain,CPp)).

adjoinSpecCP(Wh,IP,CP,Spec,[Hd,Trace],CPp) :-	  % adjoin to wh [Spec,CP]
	Spec has_feature wh(+),		
	CP immed_projection_of C1,
	C1 immed_projection_of C0,
	projectPhrase(C0,[IP],C1p),
	copy_id(C1,C1p),
	copyItem(Spec,Spec1),
	adjoinPhrase(Wh,Spec1,Specp),
	addFeature(transparent(opVar),Specp),	  % allow Wh to op/var bind
	projectPhrase(C1p,[Specp],CPp),
	copy_id(CP,CPp),
	extendPath(Trace,C1),			  % C1 part of path for Trace
	extendPath(Hd,Specp).

substituteSpecCP(Wh,IP,CP,[_,Trace],CPp) :-	  % No [Spec,CP], substitute
	CP immed_projection_of C,
	projectPhrase(C,[IP],C1),
	projectPhrase(C1,[Wh],CPp),
	copy_id(CP,CPp),
	extendPath(Trace,C1).			  % C1 is on the path for Trace
	
whLF(X) :- cat(X,C), whCat(C), X has_feature wh(+).

whCat(np).	
whCat(adv).

%%% Declare ecpLF

ecpLF parser_operation 'ECP at LF'
	with_components
		io           given_by [lf],
		multiple dep given_by [lfMovement,freeIndexing],
		controlType  given_by filter.

%%% EMPTY CATEGORY PRINCIPLE (ECP) AT LF
%%%
%%% As for ECP at S-structure except:
%%%	(1) not restricted to A-positions
%%%	(2) only bothers with non-gamma-marked ECs
%%%	(3) deals with LF movement traces

ecpLF in_all_configurations CF where
	subjectToECPLF(CF) then must_satisfy 
		lexGoverned(CF) ; lfAGovDom(CF,_).

subjectToECPLF(X) :-
	ec(X),
	\+ exceptionToECP(X,lf),
	\+ X has_feature gamma(+).

lfAGovDom(X) smallest_configuration CF under barrier(CF,X)
	with_components
		X,
		B given_by bindsECPLF(B,X,CF).

bindsECPLF(X,Y,CF) :- 
	binds(B,Y,ecp,CF), 
	segmentOf(X,B),
	antecedentOf(Y,X),
	\+ X has_feature noECP(lf),
	\+ in_CED_config(Y,CF),          %new code   
	gammaMark(Y).

%%% Declare licenseOpVars

licenseOpVars parser_operation 'FI: License operator/variables'
	with_components
		io           given_by [lf],
		multiple dep given_by [lfMovement,freeIndexing],
		controlType  given_by filter,
		% optional ...
		sCueFilter.

%% OPERATOR-VARIABLE LICENSING
%% Operator-variable forms are licenced in LF as follows:
%% 1. An operator must bind a variable
%% 2. A variable must be strongly bound

licenseOpVars(LF) :-
	licenseOperators(LF), 
 	licenseVariables(LF,LF),
	cheatQR(LF),
	licenseOperatorPositions(LF).

licenseOperators in_all_configurations CF where
	opVarConfig(CF,Op,CCDomain) then opBindsVar(Op,CCDomain).

licenseVariables on SS in_all_configurations CF where
	unlicensedVariable(CF) then overtlyBound(CF,SS).
	
licenseOperatorPositions in_all_configurations CF where
	domOperator(CF,Op) then opPos(Op,CF).

% let's pretend QR worked for topicalized 
% quantifiers that are normally subject to QR.

cheatQR in_all_configurations CF where
	qInSpecCP(CF,Q) then addFeature(moved(qr),Q).

qInSpecCP(CP,Q) :-
	cat(CP,c2),
	Q specifier_of CP,
	Q has_feature op(+).

% CF = [ ... Op ... ] 
opVarConfig(CF,Op,CCDomain) :-
	CF has_constituents L,
	pick(Op,L,CCDomain),
	operator(Op),
	highestSegment(Op),	% e.g. [NP[NP who] that...], 
	\+ nonBaseAdjunct(Op).

operator(QP) :-	cat(QP,np), QP has_feature op(+). % quantifier
operator(Op) :- emptyOperator(Op).		  % Op
operator(Wh) :-	cat(Wh,np), Wh has_feature wh(+). % overt NP[+wh]
operator(Wh) :-	cat(Wh,adv), Wh has_feature wh(+). % overt adv[+wh]

% [NPi X=[NPj Wh] [NPi Wh]]
nonBaseAdjunct(X) :- 
	X has_feature adjunct, headOfChain(X,X), \+ X has_feature apos.

%% operator must bind at least one variable
%% operator must not bind an overt R-expression

opBindsVar(Op,CCDomain) :-
	operatorsIn(Op,Ops),
	variablesIn(CCDomain,Vars),
	bindVars(Ops,Vars),
	overtRExprsIn(CCDomain,L),
	nonBindExprs(Ops,L).

% [who [that john saw]] 	=> [who [that john saw]]
% [[who] what]			=> [who] [what]
% [who]				=> [who]

operatorsIn(OpComplex,List) :- 
	adjoined(OpComplex,Adjunct,LowerSeg)
	-> (operator(Adjunct) 
	   -> operatorsIn(Adjunct,L1),
	      operatorsIn(LowerSeg,L2),
	      append(L1,L2,List)
	   ;  List = [OpComplex])
	;  List = [OpComplex].

variablesIn collect_all_configurations CF where lfVariable(CF).

boundVars(Vars,Op) those V in Vars satisfying opVar(Op,V).

% each operator identified must bind some variable
bindVars(Ops,Vars) each Op in Ops 
	satisfies boundVars(Vars,Op,BVs), nonEmptySet(BVs).

% strongly bound if Op is overt for Op[i]..x[i]
opVar(Op,Var) :- 
	coindexed(Op,Var), 
	\+ improperOpVar(Op,Var),
	make Var have_feature licensed if \+ ec(Op). 

% Two cases:
% (1) Only the head of its chain can license a variable that's also a trace.
% (2) Quantifiers in [Spec,CP] cannot license a variable.

improperOpVar(Op,Var) :-  partOfChain(Var), \+ partOfMultipleChain(Op,Var).
% improperOpVar(Op,_Var) :- Op has_feature op(+),	\+ Op has_feature adjunct. 

variable(X) :- ec(X), X has_feature apos, X has_feature_set [a(-),p(-)].

% some variables at LF aren't BT-relevant (not functionally determined)

lfVariable(V) :-  
	ec(V), 
	V has_feature apos, 
	V has_feature_set [a(A),p(P)], 
	A =='-', P == '-'.
lfVariable(X)   :- cat(X,np), \+ ec(X), X has_feature var.
lfVariable(Adv) :- cat(Adv,adv), isTrace(Adv).
lfVariable(X)   :- lfTrace(X).

lfTrace(X) :- X has_feature ec(Type), assigned(Type), trLF(Type).

trLF(qr).
trLF(wh).

overtRExprsIn collect_all_configurations CF where overtRExpr(CF).

overtRExpr(X) :- \+ ec(X), rExpr(X).

nonBindExprs(Ops,L) each Op in Ops 
	satisfies \+ (member(RExpr,L), coindexed(Op,RExpr)).

% a variable that isn't strongly bound (yet) because its range has not
% been determined by an overt operator

unlicensedVariable(X) :- lfVariable(X), \+ X has_feature licensed.

% one way to license a variable is to have an overt, non-pleonastic binder

overtlyBound(Item,S) :-
	binds(Binder,Item,opVar,S),
	\+ improperBinder(Binder),
	make Item have_feature licensed.

improperBinder(X) :- ec(X).
% improperBinder(X) :- X has_feature nonarg(+). % prohibits topicalization of expletives
improperBinder(X) :- X has_feature indexed(agr).

domOperator(X,Op) :- X has_constituent Op, highestSegment(Op), operator(Op).

opPos(Op,Dom) :- ec(Op), cat(Dom,c2).
opPos(X,_)    :- X has_feature op(+), X has_feature moved(qr).
opPos(X,Dom)  :- X has_feature wh(+), (cat(Dom,c2) -> true ; Dom has_feature wh(+)).

%%% Declare licenseClausalArguments

licenseClausalArguments parser_operation 'License Clausal Arguments'
	with_components
		io          given_by [ss],
		dep         given_by parseSS,
		controlType given_by filter,
		% optional ...
		sCueFilter,
		skippable.

%%% LICENSING OF CP ARGUMENTS
%%%
%%% Clausal Arguments headed by empty operators must be ruled out:
%%%
%%%	e.g. *John believes [CP Op John is t here]
%%%

licenseClausalArguments in_all_configurations CF
	where clausalArgumentsConfig(CF,Spec) then notEmptyOperator(Spec).

clausalArgumentsConfig(CF,Spec) :-
	\+ adjoined(CF),
	cat(CP,c2),
	CF has_constituent CP,
	Spec specifier_of CP.

notEmptyOperator(X) :-
	X has_feature ec(Type) with_constraint Type \== op  
        if (emptyNP(X), \+ X has_feature op_ok).
	
%%% Declare licenseAdjuncts

licenseAdjuncts parser_operation 'License Syntactic Adjuncts'
	with_components
		io          given_by [ss],
		dep         given_by parseSS,
		controlType given_by filter,
		% optional ...
		sCueFilter,
		skippable.

%%% LICENSING OF S-STRUCTURE ADJUNCTS

licenseAdjuncts in_all_configurations CF
	where lAdjunctsConfig(CF,C,Adjunct) then adjunctLicensed(C,CF,Adjunct).

lAdjunctsConfig(CF,C,Adjunct) :-
	adjoined(CF,Adjunct,CFp),
	cat(CF,C),
	\+ head(C),				% exclude head adjunction
	cat(CFp,Cp),
	\+ head(Cp).				% exclude projected hd adj

%% Cases:
%% 1. VP[aux] can take adjuncts only if it behaves like a real VP, 
%%    e.g. participates in O-role assignment, either regular or to an adjunct.
%%
%% 2. Regular VPs ([-aux]), if adjunct has feature predicate(_).
%%
%% 3. Allow NP scrambling: use theory that the scrambled NP resides
%%    in an adjunct A-position.
%%	- Modified: don't care if it is A or A-bar.
%%
%% 4. Allow restrictive relative clause constructions [NP [NP] [CP]]
%%    CP has "form" (lambda (x) ...x...), 
%%    x an NP: block *the man how fast we ran
%%    lambda (x) represented by wh-in-Comp or an empty operator
%%    Restrictions:
%%	(a) Disallow relativizing of the head NP, i.e. no double relatives.
%%	(b) Term "antecedent" in "Strong Binding" [Chomsky,KofL,pg.85]
%%	    strengthened to mean "local" antecedent (suggested by Pesetsky)
%%	    Implemented by "linking" (or potential coindexation of) 
%%	    [Spec,CP] with head NP.
%%
%% 5. Allow non-maximal adjunction if adjunct has an external O-role to assign.
%% 6. Allow NQ adjuncts to NP
%% 7. Allow degree adverbs (feature deg(int)) to modify APs


adjunctLicensed(vp,VP,Adjunct) :-		% (1) VP[aux] & [-aux]
	VP has_feature grid(_,_),
	(cat(Adjunct,np)
	->  true				% scrambling
	;   Adjunct has_feature predicate(_)).
adjunctLicensed(vp,VP,_) :- 
	VP has_feature aux,
	inheritsFeature(VP,grid([_Role],_)).

adjunctLicensed(ap,_AP,Adjunct) :-		% APs can be modified by
	cat(Adjunct,C),				% CPs or degree advs only
	(C == c2
    	-> true
	;  C == adv).

adjunctLicensed(i2,_IP,Adjunct) :- 
	cat(Adjunct,np)
	-> true					% scrambling
	;  clause(Adjunct).			% clausal extraposition

adjunctLicensed(np,NP,Adjunct) :-
	(cat(Adjunct,nq) ; cat(Adjunct,numP))
	-> true
	;  relClauseConfig(NP,LowerNP),
	   \+ relClauseConfig(LowerNP,_),
	   cat(Spec,np),
	   Spec specifier_of Adjunct,
	   operator(Spec),
	   agreeAGR(Spec,LowerNP), 
	   link(Spec,LowerNP).

% allow [n1 numP n1]
adjunctLicensed(n1,_,Adjunct) :- cat(Adjunct,numP).

relClauseConfig(NP,LowerSeg) :-	cat(CP,c2), adjoined(NP,CP,LowerSeg).

%%% Declare whCompRequirement

whCompRequirement parser_operation 'Wh Comp Requirement'
	with_components
		io          given_by [lf],
		dep         given_by lfMovement,
		controlType given_by filter.

%%% WH COMP REQUIREMENT
%%%	
%%%	Same as whInSyntax, but holds universally.
%%%
%%% NB.	Enforces semantic parallelism for yes/no vs. wh questions

whCompRequirement in_all_configurations CF
	where cat(CF,c2) then whCompFilter(CF), semParallel(CF).

semParallel(CP) :-
	X has_feature Q if (CP has_feature merge(Q), X specifier_of CP).

%%% REANALYZE "BOUND" PROFORMS AS VARIABLES
%%%
%%% Modifications:
%%% (1) Adjunctness, ("A-bar-ness") the criterion
%%%	[NP NP N1] no barrier to "binding" of the variable
%%% (2) Exclude LF QR/Op positions
%%%	e.g. [every man[1]] [some symphony he[1] heard] [QRt[1] liked QRt]
%%%	e.g. [which man[1]] [which symphony he[1] heard] [QRt[1] liked QRt]
%%%     But should include scrambled to IP positions
%%%	e.g. [pro iwus[i]]-nl kim pancang-i nwukwu-eykeyna t[i] sokayhayssta

reanalyzeBoundProforms parser_operation 'FI: Reanalyze Bound Proforms'
	with_components
		io           given_by [lf],
		multiple dep given_by [lfMovement],
		controlType  given_by filter.

%% Reanalyze operator-bound proforms as variables

reanalyzeBoundProforms in_all_configurations CF
	where boundProformConfig(CF,Binder,Dom,P) 
	then tryReanalyzeAsVar(P,Binder,Dom).

% (1) [CP Op[i] X ] when X dominates proform Proform[i]
% (2) [CP [NP Op[i] N1] X ] when X dominates proform Proform[i]

boundProformConfig(CF,Op,CCDomain,Proform) :-
	CF has_constituents Cs,
	pick(OpDom,Cs,CCDomain),
	binderDom(OpDom,Op),
	operator(Op),
	highestSegment(Op),			  % see modification (2)
	member(X,CCDomain),
	domProform(X,Op,Proform).

% (1) X (2) [NP X N1]
binderDom(X,X).
binderDom(Dom,Binder) :-			  % see modification (1)
	cat(Dom,np),
	maximalProj(Dom),			  % needed?
	Dom has_feature adjunct,
	Binder specifier_of Dom.

maximalProj(X) :- cat(X,C), max(C).

domProform(X,Op,Pro) :-
	\+ X has_feature moved(qr),		% see modification (2)
	(coindexedProform(X,Op)
        -> Pro = X
        ;  X has_constituent Y,
	   domProform(Y,Op,Pro)).

coindexedProform(P,Op) :- cat(P,np), coindexed(P,Op), proform(P).

proform(X) :- X has_feature_set [a(A),p(P)], (A == '+' ; P == '+').

tryReanalyzeAsVar(P,Binder,Dom) :-
	notCrossover(Dom,P,Binder,notYet,_),
	reanalyzeAsVar(P).

% t1 ProForm t2, t1 can be coindexed with ProForm, 
% but t2 can't if it is from A-bar-movement at S-structure or LF

notCrossover(Dom,P,A,S,Sp) :-
	sameCategory(Dom,P) 
        -> Sp = found
        ;  (Dom has_feature moved(qr)		% see modification (2)
           -> Sp = S
           ;  ((partOfMultipleChain(Dom,A), aBarMovementTrace(Dom))
              -> S == notYet			% fails if found
	      ;  true),
	      (Dom has_constituents L
	      -> notCrossoverL(L,P,A,S,Sp)
	      ;  (cat(Dom,_)
	         -> Sp = S
	         ;  notCrossoverL(Dom,P,A,S,Sp)))).

notCrossoverL(List,P,A) each X in List thread [S,Sp]
	satisfying notCrossover(X,P,A,S,Sp).

reanalyzeAsVar(X) :- \+ X has_feature notVar, make X have_feature var.

aBarMovementTrace(X) :- isTrace(X), antecedent(X,Y), \+ Y has_feature apos.
aBarMovementTrace(X) :- lfTrace(X).

%%% QUANTIFIER SCOPING
%%%
%%%

quantifierScoping parser_operation 'FI: Quantifier Scoping'
	with_components
		io           given_by [lf],
		multiple dep given_by [lfMovement],
		controlType  given_by filter.

quantifierScoping produces [F,Q,T]
	cases CF where
	CF with_constituents X and Y st
		X produces [XF,XQ,XT],
		Y produces [YF,YQ,YT],
		CF produces [ZF,ZQ,ZT]
	   then \+ crossQS(XF,XQ,YF,YQ), 
	        unionQS(XF,XQ,XT,YF,YQ,YT,ZF,ZQ,ZT)
	finally addIfMaxNP(CF,ZF,ZT,ZQ,F,Q,T)
	else maxNP(CF,I) then initQS(CF,I,F,Q,T).

crossQS(_XF,XQ,YF,_YQ) :- member(X,XQ), varIn(X,YF).
crossQS(XF,_XQ,_YF,YQ) :- member(Y,YQ), varIn(Y,XF).

unionQS(XF,XQ,XT,YF,YQ,YT,ZF,ZQ,ZT) :- 
	unionVars(XF,YF,ZF), 
	unionVars(XQ,YQ,ZQ),
	unionVars(XT,YT,ZT).

addIfMaxNP(X,F,Q,T,Fp,Qp,Tp) :-
	diffVars(F,T,F1),			  % temp Q binds free
	unionVars(T,Q,Qp),			  % Q is old Q + temp Q
	( maxNP(X,I) 
	-> ( X has_feature op(+)		  % quantifier
	   -> Tp=[I], Fp=F1
	   ;  \+ varIn(I,Qp),			  % free
	      unionVars([I],F1,Fp),
	      Tp=[])
	;  Tp=[], Fp=F1).

maxNP(X,I) :- cat(X,np), highestSegment(X), X has_feature index(I).

initQS(X,I,F,[],T) :- X has_feature op(+) -> F=[], T=[I] ; F=[I], T=[].


licenseObjectPro parser_operation 'License Object pro'
	with_components
		io          given_by [ss],
		dep         given_by parseSS,
		controlType given_by filter.

%%% OBJECT SMALL PRO LICENSING
%%%	
%%%	object pro must be licensed (by object clitics)
%%%	for languages with object clitics
%%%	
%%%	Object pro is defined as:
%%%	(1) object small pro
%%%	(2) object pure anaphor (non-trace)

licenseObjectPro parameterized_by clitic(object).

licenseObjectPro in_all_configurations CF where
	objProConfig(CF,List) then isLicensedObjPro(List).

% [VP [V{grid(_,_)}] pro[1] .. pro[n]]
% Identifies all object pro arguments

objProConfig(CF,List) :-
	cat(CF,i1),
	identifyVP(CF,VP),
	identifyThetaVP(VP,ThetaVP),
	findall(XP, (XP complement_of ThetaVP, objectpro(XP)), List).

% Two cases: 
% (1) pro, and 
% (2) empty nontrace anaphor

objectpro(X) :- pro(X).
objectpro(X) :- ec(X), \+ isTrace(X), X has_feature a(+).

% Each pro[i] must have feature licensedPro

isLicensedObjPro(List) each X in List 
	satisfies X has_feature licensedPro.

licenseClitics parser_operation 'License Clitics'
	with_components
		io          given_by [ss],
		dep         given_by resolveTraces,
		controlType given_by filter.

%%% CLITIC LICENSING
%%%
%%%	Subject and object clitics need to be licensed by arguments
%%%
%%% Language parameters:
%%%	clitic(subject)		language has subject clitics
%%%	clitic(object)		language has objects clitics

licenseClitics(X) :-
	licenseSubjectClitics(X) if clitic(subject),
	licenseObjectClitics(X) if clitic(object).

%%% SUBJECT CLITIC LICENSING
%%%	
%%%	A subject clitic must be coindexed with a subject pro

licenseSubjectClitics in_all_configurations CF where
     subjCliticConfig(CF,Cl) then governsSubjectPro(Cl,CF).

% [IP .. [I [Cl] [I]] .. ]

subjCliticConfig(IP,Cl) :-
	cat(IP,i2),
	I head_of IP,
	cat(Cl,cl),
	adjoined(I,Cl),
	Cl has_feature morphC(nom).

% [IP pro .. [I [Cl] [I]] .. ]

governsSubjectPro(Cl,IP) :-
	XP specifier_of IP,
	pro(XP),
	matchSCliticPosition(Cl,XP).
	
%  coindex pro[i] .. [Cl[i]] and agrees

matchSCliticPosition(Cl,XP) :-
	Cl has_feature morphC(nom),
	coindex(Cl,XP),
	agreeAGR(Cl,XP).

%%% OBJECT CLITIC LICENSING
%%%	
%%%	An object clitic must be coindexed with an appropriate matching object
%%%	for languages with object clitics
%%%
%%%	For languages that do not allow clitic doubling:
%%%	
%%%	1. each clitic must be coindexed with a pure empty object
%%%	   (pure = non-trace)
%%%
%%%	For languages that allow clitic doubling:
%%%	
%%%	1. indirect object clitics may be coindexed with:
%%%		a. An overt indirect object
%%%		b. A pro
%%%	2. direct object clitics may be coindexed with:
%%%		a. An overt direct object (marked with accusative Case)
%%%		b. A pro
%%%
%%% NB.	Clitic non-doubling parameter: licenseObjCliticsIfPro

licenseObjectClitics in_all_configurations CF where
	objCliticConfig(CF,Cls,VP) then 
		(licenseObjCliticsIfPro		  % language parameter
		-> governsPro(Cls,VP) 
		;  governsObject(Cls,VP)).
	
objCliticConfig(CF,Cls,ThetaVP) :-
	cat(CF,c2),
	C head_of CF,
	cat(I2,i2),
	I2 complement_of CF,
	cat(I1,i1),
	I2 has_constituent I1,
	identifyVP(I1,VP),
	identifyThetaVP(VP,ThetaVP),
	(\+ adjoined(C) ->
	    identifyVerb(I1,V),
	    identifyClitics(V,Cls)
	; identifyVC(C,V),
	identifyClitics(V,Cls)).

	
identifyVP(CF,VP) :-
	cat(CF,vp) 
	-> VP = CF
	;  CF subcategorizes_for XP,
	   identifyVP(XP,VP).

%% identify the theta-assigning VP, ignores auxiliaries
%%
%% Modification (Martine 8/11/94): 
%% I replaced firstRole(Roles,_) by firstRole(_,_)
%% because with the first version, clitics are not checked for intransitive
%% verbs: so, are always allowed (intransitive verbs do not have internal
%% theta role, so the configuration is not satisfied, so clitics pass
%% through the filter license clitics).
 
identifyThetaVP(VP,ThetaVP) :-
	VP has_feature grid(_,_Roles)
	-> ThetaVP = VP
	;  cat(XP,vp), 
	   VP subcategorizes_for XP,
	   identifyThetaVP(XP,ThetaVP).

%% identifyVerb has to take into consideration infinitive clauses,ie., the
%% verb is not raised, thus not adjoined to I0. The function identifyVerb
%% checks whether the category to identify has feature inf.

identifyVerb(XP,V) :-
	XP has_feature inf(_)
	-> identifyVP(XP,VP),
	   V head_of VP
	;  X head_of XP,
	   identifyAdjoined(v,X,V).

identifyVC(C,V) :- identifyAdjoined(i,C,I), identifyAdjoined(v,I,V).

%% pulls out Y of category C adjoined to X somewhere inside X
%% NB. also used in periphery

identifyAdjoined(C,X,Y) :-
	adjoined(X,Z,Xp),
	(cat(Z,C)
	-> Y = Z
	;  identifyAdjoined(C,Xp,Y)).

identifyClitics(V,Cls) :-
	adjoined(V,X,Vp)
	-> (cat(X,cl), 
	    X has_feature argument  
	   -> Cls = [X|Clsp],
	      identifyClitics(Vp,Clsp)
	   ;  identifyClitics(Vp,Cls))
	;   Cls = [].

%% object clitics select empty arguments

governsPro(List,VP) each Clitic in List
	satisfies uniquelySelectsEC(Clitic,VP).

%% each clitic uniquely selects a non-trace empty complement

uniquelySelectsEC(Cl,VP) :-
	XP complement_of VP,
	ec(XP), 
	\+ isTrace(XP),
	matchCliticPosition(Cl,XP),
	uniquelyLicensePro(XP).

governsObject(List,VP) each Clitic in List
	satisfies selectComplement(Clitic,VP).

selectComplement(Cl,VP) :-
	XP complement_of VP,
	matchCliticComplement(Cl,XP).

matchCliticComplement(Cl,X) :-			  % overt (indirect) object 
	Cl has_feature ido,
	\+ ec(X),
	!,					  % red
	matchCliticPosition(Cl,X).
matchCliticComplement(Cl,X) :-			  % overt accusative pronominal
	\+ ec(X), 
	X has_feature_set [p(+),case(acc)],
	!,					  % green
	matchCliticPosition(Cl,X).
matchCliticComplement(Cl,X) :-			  % pro or anaphora
	ec(X), 
	\+ isTrace(X), 
	matchCliticPosition(Cl,X),
	uniquelyLicensePro(X).

%% object pro must not be multiply licensed

uniquelyLicensePro(XP) :- 
	\+ XP has_feature licensedPro,
	addFeature(licensedPro,XP).

matchCliticPosition(Cl,XP) :-
	Cl has_feature ido iff XP has_feature indirectObject,
	coindex(Cl,XP),
	agreeAGR(Cl,XP),
	XP has_feature a(A) if Cl has_feature a(A).

%%% FOR RECONSTRUCTION
%%%
%%% 1. For scope, long-distance Wh-Chains 
%%% 2. For Binding Theory, Subject Binding

markLDWhChain in_all_configurations CF 
	where ldWhBaseTrace(CF) then markChain(CF).

ldWhBaseTrace(X) :- baseTrace(X), whChain(X), longDistance(X).

whChain(X) :- headOfChain(Head,X), Head has_feature wh(+).

longDistance(X) :- upPath(X,Path), memberchk(c2,Path).

markChain(X) :- addFeature(reconstruct,X), markChain(Y) if antecedent(X,Y).

markSBChain in_all_configurations CF
	where  sbBaseTrace(CF) then markChain(CF).

sbBaseTrace(X) :- baseTrace(X), sbChain(X).

sbChain(X) :- headOfChain(Head,X), Head dominates Y, Y has_feature beta_marked.