% ----------------------------------------------------------------------------------------------------
% -- You may want to adjust this to your Prolog system

:- use_module(library(lists)).
:- use_module(library(system)).

:-op(900,fy,not).

not(X) :- \+ X.


% ----------------------------------------------------------------------------------------------------
% -- major compilation procedures

nlp2dlp(Name):-
        concatenate(Name,'.nlp',FileIn),
        concatenate(Name,'.flp',FileOut1),
        concatenate(Name,'.dlp',FileOut),

        read_rules(FileIn,Program),                    write_program('Original program',Program),

        homogenize_program(Program,Program1),          write_program('Program after':homogenize_program,Program1),
        negation_normalform(Program1,Program2),        write_program('Program after':negation_normalform,Program2),
        flatten_program(Program2,Program3),            write_program('Program after':flatten_program,Program3),
        eliminate_double_negations(Program3,Program4), write_program('Program after':eliminate_double_negations,Program4),
        dehomogenize_program(Program4,ProgramD),       write_program('Program after':dehomogenize_program,ProgramD),
                                                       write_rules(FileOut1,ProgramD),
        make_heads_negationfree(Program4,Program5),    write_program('Program after':make_heads_negationfree,Program5),
        dehomogenize_program(Program5,CompiledProgram),write_program('Program after':dehomogenize_program,CompiledProgram),

        write_rules(FileOut,CompiledProgram).

nlp2str(Name):-
        set_name(Name),
        concatenate(Name,'.nlp',FileIn),
        concatenate(Name,'.str',FileOut),

        read_rules(FileIn,Program),                    write_program('Original program',Program),
        do_labels_beyond_negation,

        homogenize_program(Program,Program1),          write_program('Program after':homogenize_program,Program1),
        structural_normalform(Program1,Program2),      write_program('Program after':structural_normalform,Program2),
        dehomogenize_program(Program2,CompiledProgram),write_program('Program after':dehomogenize_program,CompiledProgram),

        write_rules(FileOut,CompiledProgram).

nlp2htl(Name):-
        set_name(Name),
        concatenate(Name,'.nlp',FileIn),
        concatenate(Name,'.htl',FileOut),

        read_rules(FileIn,Program),                    write_program('Original program',Program),
        no_labels_beyond_negation,

        homogenize_program(Program,Program1),          write_program('Program after':homogenize_program,Program1),
        negation_normalform(Program1,Program2),        write_program('Program after':negation_normalform,Program2),
        structural_normalform(Program2,Program3),      write_program('Program after':structural_normalform,Program3),
        eliminate_double_negations(Program3,Program4), write_program('Program after':eliminate_double_negations,Program4),
        make_heads_negationfree(Program4,Program5),    write_program('Program after':make_heads_negationfree,Program5),
        dehomogenize_program(Program5,CompiledProgram),write_program('Program after':dehomogenize_program,CompiledProgram),

        write_rules(FileOut,CompiledProgram).

nlp2dlp2dlv(Name):-
        nlp2dlp(Name),
        concatenate(Name,'.dlp',FileIn),
        dlp4dlv(Name,FileIn).
nlp2str2dlv(Name):-
        nlp2str(Name),
        concatenate(Name,'.str',FileIn),
        dlp4dlv(Name,FileIn).
nlp2htl2dlv(Name):-
        nlp2htl(Name),
        concatenate(Name,'.htl',FileIn),
        dlp4dlv(Name,FileIn).

dlp4dlv(Name,FileIn) :-
        concatenate(Name,'.dlv',DLVFile),
        read_rules(FileIn,DisjProgram),
        dlp2dlv(DisjProgram,DLVProgram),               write_program('Program after':dlp2dlv,DLVProgram),
        write_rules(DLVFile,DLVProgram),
        dlv(Name).


nlp2dlp2gnt(Name):- 
        nlp2dlp(Name), 
        concatenate(Name,'.dlp',FileIn), 
        dlp4gnt(Name,FileIn). 
nlp2str2gnt(Name):- 
        nlp2str(Name), 
        concatenate(Name,'.str',FileIn), 
        dlp4gnt(Name,FileIn). 
nlp2htl2gnt(Name):- 
        nlp2htl(Name), 
        concatenate(Name,'.htl',FileIn), 
        dlp4gnt(Name,FileIn). 

dlp4gnt(Name,FileIn) :- 
        concatenate(Name,'.gnt',GNTFile), 
        concatenate('cp ',FileIn,CMD0), 
        concatenate(CMD0,' ',CMD), 
        concatenate(CMD,GNTFile,CALL), 
        shell(CALL), 
        gnt(Name).  

% ----------------------------------------------------------------------------------------------------
% -- transformation into negation normalform
%
%    ATTENTION: This yields literals of form L, not L, or not not L (!)

negation_normalform(N,T):-
        N=(N1:-N2) ->
                negation_normalform(N1,T1),
                negation_normalform(N2,T2),
                T=(T1:-T2);
        N=(N1,N2) ->
                negation_normalform(N1,T1),
                negation_normalform(N2,T2),
                T=(T1,T2);
        N=(N1;N2) ->
                negation_normalform(N1,T1),
                negation_normalform(N2,T2),
                T=(T1;T2);
        N=(not F) ->
                (F=(F1,F2) ->
                        negation_normalform((not(F1);not(F2)),T);
                 F=(F1;F2) ->
                        negation_normalform((not(F1),not(F2)),T);
                 F=(not F1) ->
                        (F1 = (not _) ->
                                negation_normalform(F1,T);
                         %true ->
                                (elementary(F1) ->
                                        T=N;
                                 %true ->
                                        negation_normalform(F,F2),
                                        negation_normalform((not F2),T))
                        );
                %true ->
                         T=N);
        %true ->
                T=N.

% ----------------------------------------------------------------------------------------------------
% -- transformation yielding rules consisting of
%       heads  which are disjunctions of literals
% and   bodies which are conjunctions of literals

flatten_program(Program,T):-
        apply_to_conjuncts(Program,flatten_rule,T).

flatten_rule((Head:-Body),List):-
        clausal_normalform(',',Head,Head1),
        clausal_normalform(';',Body,Body1),
        product(',',Head1,';',Body1,',',List,':-').

% ----------------------------------------------------------------------------------------------------
% -- transformation turning a formula in cnf or dnf, respectively,
%                   depending on the given principal connector

clausal_normalform(Functor1,F,T):-
        dual(Functor1,Functor2),
        (F=..[Functor1,F1,F2] ->
                clausal_normalform(Functor1,F1,T1),
                clausal_normalform(Functor1,F2,T2),
                T=..[Functor1,T1,T2];
         F=..[Functor2,Ff1,Ff2] ->
                clausal_normalform(Functor1,Ff1,F1),
                clausal_normalform(Functor1,Ff2,F2),
                product(Functor1,F1,Functor1,F2,Functor1,T,Functor2);
         %true ->
                T=F).

% ----------------------------------------------------------------------------------------------------
% -- cross product of two sets H and B
%          H is connected by FunctorH
%          B is connected by FunctorB
%    the resulting elements are of form FunctorRb(h,b) separated by FunctorRa
%

product(FunctorH,H,FunctorB,B,FunctorRa,R,FunctorRb):-
        H=..[FunctorH,H1,H2] ->
                product(FunctorH,H1,FunctorB,B,FunctorRa,R1,FunctorRb),
                product(FunctorH,H2,FunctorB,B,FunctorRa,R2,FunctorRb),
                R=..[FunctorRa,R1,R2];
        B=..[FunctorB,B1,B2] ->
                product(FunctorH,H,FunctorB,B1,FunctorRa,R1,FunctorRb),
                product(FunctorH,H,FunctorB,B2,FunctorRa,R2,FunctorRb),
                R=..[FunctorRa,R1,R2];
        %true ->
                R=..[FunctorRb,H,B].

%----------------------------------------------------------------------------------------------------
% -- transformation into structural normalform (delta2)

structural_normalform(Program,NewProgram):-
        (labelling(simple);create_dictionary(Program)),
        structural_normalform1(Program,NewProgram),
        (verbose_flag -> write_dictionary; true),
        erase_dictionary.

structural_normalform1(Program,NewProgram):-
        Program=(Program1,Program2) ->
                structural_normalform1(Program1,NewProgram1),
                structural_normalform1(Program2,NewProgram2),
                NewProgram=(NewProgram1,NewProgram2);
        %true ->
                structural_normalform_rule(Program,NewProgram).

structural_normalform_rule((Head:-Body),List):-
        structural_normalform_wff(Head,HeadList),
        structural_normalform_wff(Body,BodyList),
        label(Head,HLabel),
        label(Body,BLabel),
        List=((HLabel:-BLabel),HeadList,BodyList).

structural_normalform_wff(Wff,List):-
        Wff=(Wff1,Wff2) ->
                structural_normalform_wff(Wff1,List1),
                structural_normalform_wff(Wff2,List2),
                label(Wff,Label),
                label(Wff1,Label1),
                label(Wff2,Label2),
                List=((Label:-Label1,Label2),(Label1:-Label),(Label2:-Label),List1,List2);
        Wff=(Wff1;Wff2) ->
                structural_normalform_wff(Wff1,List1),
                structural_normalform_wff(Wff2,List2),
                label(Wff,Label),
                label(Wff1,Label1),
                label(Wff2,Label2),
                List=((Label1;Label2:-Label),(Label:-Label1),(Label:-Label2),List1,List2);
        Wff=(not Wff1),labels_beyond_negation  ->
                structural_normalform_wff(Wff1,List1),
                label(Wff,Label),
                label(Wff1,Label1),
                List=((Label:-not(Label1)),(false:-Label,Label1),List1);
        %true ->
                label(Wff,Label),
                List=((Label:-Wff),(Wff:-Label)).

% ----------------------------------------------------------------------------------------------------
% -- label assignment
% ---  depending on value of 'labelling/1'

label(X,Label):-
        (X=true;X=false) ->
                Label=X;
        (labelling(simple) ->
                 Label=label(X);
         %true ->
                 dictionary(X,Label)).
% ----------------------------------------------------------------------------------------------------
% -- transformation eliminating negation as failure from rule heads
% --    new symbols are obtained by prefixing the old ones by 'not_'

make_heads_negationfree(Program,NewProgram):-
        all_nots_in_heads(Program,NewProgram1,Nots),
        (Nots=true ->
                NewProgram=NewProgram1;
        %true ->
                new_rules(Nots,Rules),
                NewProgram=(NewProgram1,Rules)).

all_nots_in_heads(Program,NewProgram,Nots):-
        Program=(Program1,Program2) ->
                all_nots_in_heads(Program1,NewProgram1,Nots1),
                all_nots_in_heads(Program2,NewProgram2,Nots2),
                NewProgram=(NewProgram1,NewProgram2),
                conjoin(Nots1,Nots2,Nots);
        Program=(Head:-Body) ->
                eliminate_not_in_head(Head,NewHead,Nots),
                NewProgram=(NewHead:-Body).

eliminate_not_in_head(Head,NewHead,Nots):-
        Head=(Head1;Head2) ->
                eliminate_not_in_head(Head1,NewHead1,Nots1),
                eliminate_not_in_head(Head2,NewHead2,Nots2),
                NewHead=(NewHead1;NewHead2),
                conjoin(Nots1,Nots2,Nots);
        Head=not(Wff) ->
                naf_name(Wff,NewHead),
                Nots=Wff;
        %true ->
                NewHead=Head,
                Nots=true.

new_rules(Atoms,Rules):-
        apply_to_conjuncts(Atoms,elim_not,Rules1),
        list2conjunction(Rules2,Rules1),
        list2conjunction(Rules2,Rules).

elim_not(Atom,TwoRules):-
        naf_name(Atom,NotAtom),
        TwoRules=((NotAtom:-not(Atom)),(false:-Atom,NotAtom)).

% ---------------------------------------------------------------------------------------------------
% -- elimination of double negation

eliminate_double_negations(Program,T):-
        apply_to_conjuncts(Program,eliminate_double_negations_rule,T).

eliminate_double_negations_rule((Head:-Body),T):-
        eliminate_notnot_in_head(Head,Head1,HNotnots),
        eliminate_notnot_in_body(Body,Body1,BNotnots),
        disjoin(Head1,BNotnots,Head2),
        conjoin(Body1,HNotnots,Body2),
        T=(Head2:-Body2).

eliminate_notnot_in_head(Wff,Result,Notnots):-
        Wff=(Wff1;Wff2) ->
                eliminate_notnot_in_head(Wff1,Result1,Notnots1),
                eliminate_notnot_in_head(Wff2,Result2,Notnots2),
                disjoin(Result1,Result2,Result),
                conjoin(Notnots1,Notnots2,Notnots);
        Wff=(not not Wff1) ->
                Result=false,
                Notnots=(not Wff1);
        %true ->
                Result=Wff,
                Notnots=true.

eliminate_notnot_in_body(Wff,Result,Notnots):-
        Wff=(Wff1,Wff2) ->
                eliminate_notnot_in_body(Wff1,Result1,Notnots1),
                eliminate_notnot_in_body(Wff2,Result2,Notnots2),
                conjoin(Result1,Result2,Result),
                disjoin(Notnots1,Notnots2,Notnots);
        Wff=(not not Wff1) ->
                Result=true,
                Notnots=(not Wff1);
        %true ->
                Result=Wff,
                Notnots=false.

% ---------------------------------------------------------------------------------------------------
% -- auxiliary predicates

variables(G,Variables):-
        (atomic(G);var(G)) ->
                (var(G) -> Variables=[G];
                 Variables=[]);
        G=[G1] ->
                variables(G1,Variables);
        G=..[_,Argument1|Arguments] ->
                variables(Argument1,Variables1),
                variables(Arguments,Variables2),
                union1(Variables1,Variables2,Variables).

% -------------------------------------------------------------------------------------------------
% -- Basename of current file
%    needed for dictonary

:-dynamic(name/1).
set_name(Name):-
        retract(name(_)),fail;
        assert(name(Name)).
:-set_name(noname).

%--------------------------------------------------------------------------------------------------
% -- dictionary predicates
% --

:-dynamic(dictionary/2).

create_dictionary(Program):-
        dictionary1(Program,1,_),
        (dictionary_file ->
                name(Name),concatenate(Name,'.dic',DicName),
                tell(DicName),
                write_dictionary,
                told;
         true).

write_dictionary:-
%        dictionary(X,Y),write('dictionary(('),write(X),write('),'),write(Y),write('). \n'),fail;true.
	dictionary(X,Y),
	write(dictionary(X,Y)),
	write('.\n'),
	fail;true.

dictionary1(Program,InArg,OutArg):-
        Program=(P1,P2) ->
                dictionary1(P1,InArg,OutArg1),
                dictionary1(P2,OutArg1,OutArg);
        Program=(Head:-Body) ->
                (labelling(number) ->
                        labels4wff(Head,InArg,OutArg1),
                        labels4wff(Body,OutArg1,OutArg);
                 labelling(formula) ->
                        concatenate(InArg,'h',Argh),labels4wff(Head,Argh,_),
                        concatenate(InArg,'b',Argb),labels4wff(Body,Argb,_),
                        OutArg is InArg+1).

labels4wff(Wff,InArg,OutArg):-
        (Wff=true;
         Wff=false;
         dictionary(Wff,_)) ->
                OutArg=InArg.

labels4wff(Wff,InArg,OutArg):-
        labelling(number),
	!,
        ((Wff=(A,B);
          Wff=(A;B)) ->
                labels4wff(A,InArg,OutArg1),
                labels4wff(B,OutArg1,OutArg2),
                give_label(Wff,OutArg2),
                OutArg is OutArg2+1;
         Wff=(not A),labels_beyond_negation ->
                labels4wff(A,InArg,OutArg1),
                give_label(Wff,OutArg1),
                OutArg is OutArg1+1;
         %true ->
                give_label(Wff,InArg),
                OutArg is InArg+1).

labels4wff(Wff,InArg,_):-
        labelling(formula),
	!,
        (Wff=(A,B) ->
                concatenate('_and_',InArg,Arg),
                give_label(Wff,Arg),
                concatenate(InArg,1,InArg1),labels4wff(A,InArg1,_),
                concatenate(InArg,2,InArg2),labels4wff(B,InArg2,_);
         Wff=(A;B) ->
                concatenate('_or_',InArg,Arg),
                give_label(Wff,Arg),
                concatenate(InArg,1,InArg1),labels4wff(A,InArg1,_),
                concatenate(InArg,2,InArg2),labels4wff(B,InArg2,_);
         Wff=not(A) ->
                concatenate('_not_',InArg,Arg),
                give_label(Wff,Arg),
                (labels_beyond_negation -> concatenate(InArg,n,InArgn),labels4wff(A,InArgn,_);true);
         Wff=..[F|Args] ->
                label_string(LabelString),
                concatenate(LabelString,F,LabelFunctor),
                Label=..[LabelFunctor|Args],
                assert(dictionary(Wff,Label)) ).

give_label(Wff,Arg):-
        label_string(LabelString),
        concatenate(LabelString,Arg,LabelFunctor),
        variables(Wff,Variables),
        Label=..[LabelFunctor|Variables],
        assert(dictionary(Wff,Label)).

erase_dictionary:-
        retract(dictionary(_,_)),fail;
        true.

% ----------------------------------------------------------------------------------------------------
% -- transformation turning facts into rules and for undoing this

homogenize_program(Program,T):-
        apply_to_conjuncts(Program,homogenize,T).

dehomogenize_program(Program,T):-
        apply_to_conjuncts(Program,dehomogenize,T1),
        eliminate_redundancies(T1,T).

homogenize(Rule,(Head:-Body)):-
        Rule=(Head:-Body) ->
                true;
        Rule=(:-Body) ->
                Head=false;
        %true->
                Head=Rule,
                Body=true.

dehomogenize((Head:-Body),Rule1):-
        adjust(Head,Head1),
        adjust(Body,Body1),
        (Body1=true ->
                 Rule1=Head1;
         Body1=false ->
                 Rule1=true;
         Head1=true ->
                 Rule1=true;
         Head1=false ->
                 Rule1=(:-Body1);
          %true ->
                 Rule1=(Head1:-Body1)).

% ----------------------------------------------------------------------------------------------------
% --  gnt specific stuff

gnt(Name) :-
	gnt(Name,' 0 ').

gnt(Name,Options) :-
        concatenate(Name,'.gnt',FileGNT),
        concatenate('lparse --dlp ',FileGNT,CMD0),
        concatenate(CMD0,' | gnt2 ',CMD),
        concatenate(CMD,Options,CALL),
        write('Calling ':CALL),nl,write('--'),
        shell(CALL).

% ----------------------------------------------------------------------------------------------------
% --  dlv specific stuff

dlv(Name) :-
	dlv(Name,'').

dlv(Name,Options) :-
        concatenate(Name,'.dlv',FileDLV),
        concatenate('dlv ',Options,CMD0),
        concatenate(CMD0,' ',CMD),
        concatenate(CMD,FileDLV,CALL),
        write('Calling ':CALL),nl,write('--'),
        shell(CALL).

dlp2dlv(Program,T):-
        apply_to_conjuncts(Program,dlv_rule,T1),
        T=(true,(:-false),T1).

dlv_rule(Rule,(Head1:-Body1)):-
        Rule=(Head:-Body) ->
                list2disjunction(H,Head),
                list2disjunction(H,Head1),
                list2conjunction(B,Body),
                list2conjunction(B,Body1);
        Rule=(:-Body) ->
                Head1=false,
                list2conjunction(B,Body),
                list2conjunction(B,Body1);
        %true ->
                list2disjunction(H,Rule),
                list2disjunction(H,Head1),
                Body1=true.

%----------------------------------------------------------------------------------------------------
% -- logical connectives and more

conjoin(A,B,C) :-
        A == true ->
                C = B;
        B == true ->
                C = A;
        A == false ->
                C = false;
        B == false ->
                C = false;
        A == B ->
                C = A;
        %true ->
                C = (A , B).

disjoin(A,B,C) :-
        A == true ->
                C = true;
        B == true ->
                C = true;
        A == false ->
                C = B;
        B == false ->
                C = A;
        A == B ->
                C = A;
        %true ->
                C = (A ; B).

adjust( Wff, AWff ) :-
        Wff = (Wff1, Wff2) ->
                adjust(Wff1,Wff3),
                adjust(Wff2,Wff4),
                conjoin(Wff3,Wff4,AWff);
        Wff = (Wff1; Wff2) ->
                adjust(Wff1,Wff3),
                adjust(Wff2,Wff4),
                disjoin(Wff3,Wff4,AWff);
        %true ->
                AWff = Wff.

apply_to_conjuncts(Wff,P,Wff1):-
        Wff=(A,B) ->
                apply_to_conjuncts(A,P,A1),
                apply_to_conjuncts(B,P,B1),
                Wff1=(A1,B1);
        %true ->
                T1=..[P,Wff,Wff1],
                call(T1).

naf_name(Wff,NotWff):-
        Wff=..[F|Args],
        concatenate('not_',F,NotF),
        NotWff=..[NotF|Args].

dual(';',',').
dual(',',';').

elementary(F):-
        (F = (_,_)  ) -> fail;
        (F = (_;_)  ) -> fail;
        (F = (not _)) -> fail;
        true.

list2conjunction(List,Conjunction):-
        var(List) ->
                (not(var(Conjunction)), Conjunction=(A,B) ->
                         list2conjunction(ListA,A),
                         list2conjunction(ListB,B),
                         union1(ListA,ListB,List);
                 List=[Conjunction]);
        List=[X] ->
                Conjunction=X;
        List=[X,Y|Rest] ->
                list2conjunction([Y|Rest],ConjunctionR),
                Conjunction=(X,ConjunctionR).

list2disjunction(List,Disjunction):-
        var(List) ->
                (not(var(Disjunction)), Disjunction=(A;B) ->
                         list2disjunction(ListA,A),
                         list2disjunction(ListB,B),
                         union1(ListA,ListB,List);
                 List=[Disjunction]);
        List=[X] ->
                Disjunction=X;
        List=[X,Y|Rest] ->
                list2disjunction([Y|Rest],DisjunctionR),
                Disjunction=(X;DisjunctionR).

% ----------------------------------------------------------------------------------------------------
% -- Basic procedures

member1(X,Y):-
        Y=[F|R] ->
                (X==F;member1(X,R)).

union1(X,Y,Z):-
        X=[] ->
                Z=Y;
        X=[F|R] ->
                (member1(F,Y) ->
                         union1(R,Y,Z);
                 %true ->
                         union1(R,Y,Z1),
                         Z=[F|Z1]).

concatenate(Name1,Name2,Name):-
        name(Name1,Set1),
        name(Name2,Set2),
        append(Set1,Set2,Set),
        name(Name,Set).

% ----------------------------------------------------------------------------------------------------
% -- Conjoin two conjunctions, eliminating redundancies

eliminate_redundancies(T1,T2):-
        member_of_conjunction(Wfr,T1),
        conj1(T1,Wfr,T2).

conj(C1,C2,R):-
        C1=(A,B) ->
                conj(B,C2,R2),
                conj(A,R2,R);
        C1==false ->
                R=false;
        (C1==true;
         member_of_conjunction1(C1,C2)) ->
                R=C2;
        %true ->
                R=(C1,C2).

member_of_conjunction(X,Conjunction):-
        Conjunction=(A,B) ->
                (member_of_conjunction(X,B);
                 member_of_conjunction(X,A));
        %true ->
                Conjunction=X.

member_of_conjunction1(X,Conjunction):-
        Conjunction=(A,B) ->
                (member_of_conjunction1(X,A);
                 member_of_conjunction1(X,B));
        %true ->
                Conjunction==X.

%---
conj1(C,_,R):-
        conj11(C,R),
        (retract(rule(_)),fail;true).

conj11(C,R):-
        C=(A,B) ->
                conj11(A,A1),
                conj11(B,B1),
                conjoin(A1,B1,R);
        C==false ->
                R=false;
        (C==true;
        rule(C)) ->
                R=true;
        %true ->
                R=C,assert(rule(C)).


:-dynamic(rule/1).

% ----------------------------------------------------------------------
% -- label style
%
%    This is only relavent for structural transformations
%
%    'simple'  X obtains label(X) as label
%    'number'  formulas are labelled consecutively by numbers
%              this option relies on an underlying dictionary
%    'formula' formulas are labelled by formula descriptors
%              eg
%                  p(X) is labelled label_p(X)
%                  label_and_3b21 tells us that
%                                 X is a conjunction
%                                 inside the body of the third rule
%                             and the body is of form
%                                 ( _ ; ( X , _ ) ),
%                              or ( _ , ( X ; _ ) )
%                              or ( _ , ( X , _ ) )

:- dynamic(labelling/1).

set_labelling(_) :-
        retract(labelling(_)),
        fail.
set_labelling(Label) :-
        (Label = simple;
         Label = formula;
         Label = number)   ->
                 assert(labelling(Label));
        %true ->
                 write('No valid labelling! Using numbers!'),
                 assert(labelling(number)).

:- set_labelling(number).                            % Make 'number' the default

% ----------------------------------------------------------------------
% -- label layout

:- dynamic(label_string/1).

set_label_string(_) :-
        retract(label_string(_)),
        fail.
set_label_string(Label) :-
        assert(label_string(Label)).

% :- set_label_string('label_').                     % Make 'label_' the default
:- set_label_string('l').                            % Make 'l' the default

% ----------------------------------------------------------------------
% -- labels beyond negation

:- dynamic(labels_beyond_negation/0).

do_labels_beyond_negation :-                         % enable labels beyond negation
        retract(labels_beyond_negation),
        fail.
do_labels_beyond_negation :-
        assert(labels_beyond_negation).

no_labels_beyond_negation :-                         % labels beyond negation
        retract(labels_beyond_negation),
        fail.
no_labels_beyond_negation.

:- no_labels_beyond_negation.                        % default is to have labels beyond negation

% ----------------------------------------------------------------------
% --

:- dynamic(dictionary_file/0).

do_dictionary_file :-
        retract(dictionary_file),
        fail.
do_dictionary_file :-
        assert(dictionary_file).

no_dictionary_file :-
        retract(dictionary_file),
        fail.
no_dictionary_file.

:- do_dictionary_file.

% ----------------------------------------------------------------------
% -- verbose predicates, chatting if verbose_mode is turned on

:- dynamic(verbose_flag/0).

verbose_mode :-                          % enable verbose mode
        retract(verbose_flag),
        fail.
verbose_mode :-
        assert(verbose_flag).

no_verbose_mode :-                       % disable verbose mode
        retract(verbose_flag),
        fail.
no_verbose_mode.

:- verbose_mode.                         % default is verbose mode

writeln_verbosely(X) :-
        verbose_flag ->
                write(X),nl;
        %true->
                true.
% ----------------------------------------------------------------------
% -- i/o predicates

write_program(String,Program) :-
        verbose_flag ->
                write('--'),nl,
                write(String),nl,
                write('--'),
                apply_to_conjuncts(Program,write_clause,_),
                nl,write('=='),nl;
        %true->
                true.

write_clause(A) :-
        nl,
        write(A),
        write(.).

write_clause(A,_) :-                    % 2-ary predicate can be used as
        write_clause(A).                % argument of apply_to_conjuncts

read_rules(File,Wff):-
        open(File,read,Stream),
        read(Stream,Wff1),
        read_wff_loop(Stream,Wff1,Wff),
        close(Stream).

read_wff_loop(Stream,Wff1,Wff):-
        read(Stream,Wff2),
        (Wff2==end_of_file ->
                 Wff=Wff1;
         %true->
                 read_wff_loop(Stream,Wff2,Wff3),
                 Wff=(Wff1,Wff3)).

write_rules(File,Program):-
        tell(File),
        print3(Program),
        told.

print1(T):-
        T=(T1,T2) ->
                print1(T1),
                print1(T2);
        print_rule1(T).

print2(T):-
        T=(T1,T2) ->
                print2(T1),
                print2(T2);
        print_rule2(T).

print3(T):-
        T=(T1,T2) ->
                print3(T1),
                print3(T2);
        print_rule3(T).

print_rule1(Rule):-
        write(Rule),
        write('. '),nl.

print_rule2(Rule):-
        Rule=(Head:-Body) ->
                write(Head),write(':- \n'),
                write_list(Body),write('. \n');
        Rule=(:-Body) ->
                write(':- \n'),
                write_list(Body),write('. \n');
        %true ->
                write(Rule),write('. \n').

print_rule3(Rule):-
        Rule=(Head:-Body) ->
                write_head(Head,'|'),
                write(':-'),
                write_body(Body,','),
                write('. '),nl;
        Rule=(:-Body) ->
                write(':-'),
                write_body(Body,','),
                write('. '),nl;
        %true ->
                write_head(Rule,'|'),
                write('. '),nl.

write_head(A,S):-
        A=(B;C) ->
                write_head(B,S),
                write(S),
                write_head(C,S);
        %true ->
                write(A).

write_body(A,S):-
        A=(B,C) ->
                write_body(B,S),
                write(S),
                write_body(C,S);
        %true ->
                write(A).

write_list(A):-
        A=(B,C) ->
                write_list(B),
                write(', \n'),
                write_list(C);
        %true ->
                write(' '),
                write(A).