% 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],G1,G2,S1,S2,K1,K2), parseR([0,0],G2,G3,S2,S3,K2,K3), parseR([1,1],G3,G4,S3,S4,K3,K4),
parseR([0,0,0],G4,G5,S4,S5,K4,K5), parseR([0,1,1],G5,G6,S5,S6,K5,K6), parseR([1,0,1],G6,G,S6,S,K6,K),
not(parseR([1],G,G,S,S,K,K)), not(parseR([0,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), 
	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), 
	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],G1,G2,S1,S2,K1,K2), parseCF([0,0],G2,G3,S2,S3,K2,K3), parseCF([1,1],G3,G4,S3,S4,K3,K4),
parseCF([0,0,0],G4,G5,S4,S5,K4,K5), parseCF([0,1,1],G5,G6,S5,S6,K5,K6), parseCF([1,0,1],G6,G,S6,S,K6,K),
not(parseCF([1],G,G,S,S,K,K)), not(parseCF([0,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)).

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