:- dynamic cf_rule0/1,cf_ruleL/3,cf_ruleR/3.

parse(DepthLimit,G1,G2,NTSofar,NT,S) :-			% Inductive
	parse(DepthLimit,s,S,[],G1,G2,NTSofar,NT).

parse(DepthLimit,S,[],[],G1,G2,N,N) :-
	!,abduce(cf_rule0(S),G1,G2).

parse(s(DepthLimit),S,[H|T],V,G1,G2,NT1,NT2) :-			% S -> AB where A,B non-terminal
	terminal(H),new_nt(B,NT1,NT3),
	abduce(cf_ruleL(S,H,B),G1,G3),
	parse(DepthLimit,B,T,V,G3,G2,NT3,NT2).


parse(s(DepthLimit),S,Seq,V,G1,G2,NT1,NT2) :-			% S -> AB where A,B non-terminal
	\+set(grammar_type,regularOnly),
	last_ele(Seq,PreSeq,H),
	terminal(H),new_nt(A,NT1,NT3),
	abduce(cf_ruleR(S,A,H),G1,G3),
	parse(DepthLimit,A,PreSeq,V,G3,G2,NT3,NT2).



parse_usingLearnedTheory(DepthLimit,G,S) :-				% Deductive
	parse_usingLearnedTheory(DepthLimit,s,S,[],G).

parse_usingLearnedTheory(DepthLimit,S,[],[],G) :-
	!,member(cf_rule0(S),G).

parse_usingLearnedTheory(s(DepthLimit),S,[H|T],V,G) :-			% S -> AB where A,B non-terminal
	member(cf_ruleL(S,H,B),G),
	parse_usingLearnedTheory(DepthLimit,B,T,V,G).

parse_usingLearnedTheory(s(DepthLimit),S,Seq,V,G) :-			% S -> AB where A,B non-terminal
	\+set(grammar_type,regularOnly),
	last_ele(Seq,PreSeq,H),
	member(cf_ruleR(S,A,H),G),
	parse_usingLearnedTheory(DepthLimit,A,PreSeq,V,G).


abduce(X,G,G) :- member(X,G).
abduce(X,G,[X|G]) :- 
	length(G,GrammarSize),set(kBound,KBound),GrammarSize=<KBound,
	not(member(X,G)).
	%not(disobey_constraint(X,G)).

% bottom up, invent new non-terminals first
% new_nt(NT,NewNTsSofar,NewNTs)
new_nt(s(1),[],[s(1)]).
new_nt(s(NewNT),[s(TopNTIndex)|NewNTsSofar],[s(NewNT),s(TopNTIndex)|NewNTsSofar]):-
	set(newNTLimit,Limit),TopNTIndex<Limit,
	NewNT is TopNTIndex+1. 
new_nt(NT,NewNTs,NewNTs):- member(NT,NewNTs).
new_nt(s,NewNTs,NewNTs).


terminal(a).
terminal(b).




disobey_constraint(cf_rule0(End),G):-
	set(grammar_type,regularOnly),
	member(cf_rule0(End1),G),End\==End1.

disobey_constraint(cf_ruleL(Q1,Terminal,Q2),G):-
	set(grammar_type,regularOnly),
	member(cf_ruleL(Q1,Terminal,Q3),G),Q2\==Q3.