% Prolog Implementation of MIL for learning Regular grammars or Context-free grammars. 
% Allow representation change: a Regular grammar is searched first before a Context-free one
% Figure 6: Metagol_RCF
% To run, please download yap6.0


:-use_module(library(lists)). 


/****************** Fig.6 MetagolRCF *********************/
metagolRCF(G):-
	member(K0,[s(0),s(s(0)),s(s(s(0))),s(s(s(s(0)))),s(s(s(s(s(0)))))]), % iterative deepening bound
	metagolRCF(G,K0).

metagolRCF(G,K0):-metagolR(G,K0).
metagolRCF(G,K0):-metagolCF(G,K0).


/****************** Fig.5 MetagolR *********************/
parseR(S,G1,G2,S1,S2,K1,K2) :- parseR(s(0),S,[],G1,G2,S1,S2,K1,K2).
parseR(Q,X,X,G1,G2,S,S,K1,K2) :- abduce(acceptor(Q),G1,G2,K1,K2).
parseR(Q,[C|X],Y,G1,G2,S1,S2,K1,K2) :- 
	skolem(P,S1,S3),
	abduce(delta1(Q,C,P),G1,G3,K1,K3), 
	parseR(P,X,Y,G3,G2,S3,S2,K3,K2).


metagolR(G,K0):-
parseR([],[],G1,[s(0)],S1,K0,K1), parseR([0,1],G1,G2,S1,S2,K1,K2), parseR([0,0,1,1],G2,G3,S2,S3,K2,K3), parseR([0,0,0,1,1,1],G3,G,S3,S,K3,K),
not(parseR([0],G,G,S,S,K,K)),not(parseR([1],G,G,S,S,K,K)),not(parseR([1,0],G,G,S,S,K,K)), not(parseR([0,0],G,G,S,S,K,K)), not(parseR([1,1],G,G,S,S,K,K)).


/*********************** MetagolCF **********************/
parseCF(S,G1,G2,S1,S2,K1,K2) :- parseCF(s(0),S,[],G1,G2,S1,S2,K1,K2).
parseCF(Q,X,X,G1,G2,S,S,K1,K2) :- abduce(acceptor(Q),G1,G2,K1,K2).
parseCF(Q,[C|X],Y,G1,G2,S1,S2,K1,K2) :- 
	skolem(P,S1,S3),
	abduce(delta1(Q,C,P),G1,G3,K1,K3), 
	parseCF(P,X,Y,G3,G2,S3,S2,K3,K2).
parseCF(Q,X,Y,G1,G2,S1,S2,K1,K2) :- 
	skolem(P,S1,S3),
	abduce(delta2(Q,P,C),G1,G3,K1,K3), 
	suffix([C|Y],X),[C|Y]\==X,
	parseCF(P,X,[C|Y],G3,G2,S3,S2,K3,K2).

parseCF(Q,X,Y,G1,G2,S1,S2,K1,K2) :- 
	skolem(P,S1,S3),skolem(R,S1,S3),
	abduce(delta3(Q,P,R),G1,G3,K1,K3), 
	suffix(Z,X),Z\==X,
	parseCF(P,X,Z,G3,G4,S3,S4,K3,K4),
	parseCF(P,Z,Y,G4,G2,S4,S2,K4,K2).


metagolCF(G,K0):-
parseCF([],[],G1,[s(0)],S1,K0,K1), parseCF([0,1],G1,G2,S1,S2,K1,K2), parseCF([0,0,1,1],G2,G3,S2,S3,K2,K3), parseCF([0,0,0,1,1,1],G3,G,S3,S,K3,K),
not(parseCF([0],G,G,S,S,K,K)),not(parseCF([1],G,G,S,S,K,K)),not(parseCF([1,0],G,G,S,S,K,K)), not(parseCF([0,0],G,G,S,S,K,K)), not(parseCF([1,1],G,G,S,S,K,K)).


/************************Common Utilities between MetagolR and MetagolCF ***********************/
abduce(X,G,G,K,K) :- member(X,G).
abduce(X,G,[X|G],s(K),K) :- not(member(X,G)),\+break_constraint(X,G).

%break_constraint(delta,G):-
      

skolem(s(N),[s(Pre)|SkolemConsts],[s(N),s(Pre)|SkolemConsts]):- N is Pre+1.
skolem(S,SkolemConsts,SkolemConsts):-member(S,SkolemConsts).