% Un traducteur de la syntaxe XML-Prolog vers la représentation MIL-2H "avec listes" + assertions
%------------------------------------------------------------------------------------------------

:- use_module(library(sgml)).
:- use_module('mil_H.pl').

%--- utilisation pour exporter en XML un programme écrit en MIL-Prolog
:- use_module(library(sgml_write)).

export(NomFich, Prog) :- 
	tradXML(XT, Prog),
	open(NomFich, write, Str), xml_write(Str, XT, []), close(Str).

%=======================================================================================

%--- le prédicat-maître "réversible" tradXML(XMLterm, MILterm)

tradXML([element('Triple', [], [
             element('Prog', [], [element('Variables', [], XLV), element('Main', [], XLInst)]), 
             element('Precondition', [], [XPre]), 
             element('Postcondition', [], [XPost])
             ])], 
		triplet(progMIL(MLV, MLInst), pre(Pre), post(Post))
) :- 
	tradDecl(XLV, MLV), tradSeq(XLInst, MLInst), tradAss(XPre, Pre), tradAss(XPost, Post).
		
%--- tradDecl(XLV, MLV)

tradDecl([], []).

tradDecl([element('Var',[name=A],[]) | XSLV], [A | MSLV]) :- atom(A), tradDecl(XSLV, MSLV).
	
%--- tradSeq([LInst, MILterm)

tradSeq([], []).

tradSeq([XInst | XSInst], [MInst | MSInst]) :- tradInst(XInst, MInst), tradSeq(XSInst, MSInst).

%--- tradInst(XInst, MInst)

tradInst(element('Read', [], [element('Var', [name=A], [])]), 
	lire A
).

tradInst(element('Assignment', [], [element('Var', [name=A], []), XExpAr]), 
	A := MExpAr
) :-	tradExpAr(XExpAr, MExpAr).

tradInst(element('Write', [], [XExpAr]), 
	ecrire MExpAr
) :- tradExpAr(XExpAr, MExpAr).

tradInst(element('Space', [], []), espace).

tradInst(element('Newline', [], []), ligne).

tradInst(element('Loop', [], [XTest, element('Invariant', [], [XInv]), element('Sequence', [], XCorps)]), 
	tantque(MTest, invariant(MInv), MCorps)
) :- tradExpBool(XTest, MTest), tradAss(XInv, MInv), tradSeq(XCorps, MCorps).

tradInst(element('Conditional', [], [XTest, 
				element('Sequence', [], XLVrai), 
				element('Sequence', [], XLFaux) ]
				), 
		si(MTest, MLVrai, MLFaux)
) :- tradExpBool(XTest, MTest), tradSeq(XLVrai, MLVrai), tradSeq(XLFaux, MLFaux).

%--- tradExpAr(XExpAr, MExpAr)

tradExpAr(element('Cst', [val=XV], []), V) :- var(V), atom_number(XV, V).
tradExpAr(element('Cst', [val=XV], []), V) :- number(V), atom_number(XV, V).

tradExpAr(element('VarExp', [], [element('Var', [name=N], [])]), N) :- atom(N).

% énumération des opérateurs en vue de la réversibilité
tradExpAr(element('Bin', [op= '+'], [XG, XD]), G+D) :- tradExpAr(XG, G), tradExpAr(XD, D).
tradExpAr(element('Bin', [op= '*'], [XG, XD]), G*D) :- tradExpAr(XG, G), tradExpAr(XD, D).
tradExpAr(element('Bin', [op= '-'], [XG, XD]), G-D) :- tradExpAr(XG, G), tradExpAr(XD, D).
tradExpAr(element('Bin', [op= '/'], [XG, XD]), G/D) :- tradExpAr(XG, G), tradExpAr(XD, D).

%--- tradExpBool(XExpBool, ExpBool) - idem
tradExpBool(element('Test', [op='='], [XG, XD]), G=D) :- tradExpAr(XG, G), tradExpAr(XD, D).
tradExpBool(element('Test', [op='<'], [XG, XD]), G<D) :- tradExpAr(XG, G), tradExpAr(XD, D).
tradExpBool(element('Test', [op='>'], [XG, XD]), G>D) :- tradExpAr(XG, G), tradExpAr(XD, D).
tradExpBool(element('Test', [op='<='], [XG, XD]), G<=D) :- tradExpAr(XG, G), tradExpAr(XD, D).
tradExpBool(element('Test', [op='>='], [XG, XD]), G>=D) :- tradExpAr(XG, G), tradExpAr(XD, D).
tradExpBool(element('Test', [op='<>'], [XG, XD]), G<>D) :- tradExpAr(XG, G), tradExpAr(XD, D).

%--- tradAss(XAss, MAss) - idem avec traduction des connecteurs

tradAss(element('Conj', [], [XG, XD]), (MG et MD)) :- tradAss(XG, MG), tradAss(XD, MD).

tradAss(element('Disj', [], [XG, XD]), (MG ou MD)) :- tradAss(XG, MG), tradAss(XD, MD).

tradAss(element('Imp', [], [XG, XD]), (MG imp MD)) :- tradAss(XG, MG), tradAss(XD, MD).

tradAss(element('Neg', [], [XA]), non MA) :- tradAss(XA, MA).

tradAss(element('Predicate', [name=N], XLArgs), T) :-  var(T), !, % N et supposé instancié
	estMaj(N), tradLExpAr(XLArgs, MLArgs), T =.. [N | MLArgs]. 
tradAss(element('Predicate', [name=N], XLArgs), T) :- % T est supposé instancié
	T =.. [N | MLArgs], estMaj(N), tradLExpAr(XLArgs, MLArgs).

tradAss(XB, MB) :- tradExpBool(XB, MB).

tradLExpAr([], []).
tradLExpAr([XA|XS], [MA|MS]) :- tradExpAr(XA, MA),tradLExpAr(XS, MS).

estMaj(C) :- atom_length(C, 1), char_code(C, N), N>64, N<91.

% =================================================================================

ttr :- load_structure('qr.xml', XmlSource, [dialect(xml),space(remove)]), tradXML(XmlSource, T), write(T), nl.

ttd :- load_structure('qrd.xml', XmlSource, [dialect(xml),space(remove)]), tradXML(XmlSource, T), write(T), nl.