:- dynamic max_depth/1, tr_session/1, init_def/3, mode/3, file_input/1, strat/1.

% max_depth sets the depth at which the derivation must stop even if no
% semi-deterministic program has been derived. The depth value corresponds
% to the number of iteration of the loop strategy.
max_depth(40).

% tr_session allows the user to specify some positions in the transformation
% process where he wants the transformation to stop, until he hits the <CR>
% key.
% Possible positions are after the unfolding steps (unf), case split steps
% (cs), and folding steps (fold).
% tr_session(unf).  % stops after the unfolding steps
% tr_session(cs). % stops after the case-split steps
% tr_session(fold). % stops after the folding steps

% file_input specifies the file which contains the initial program.
% init_def specifies the definition of the clause(s) from which the
% transformation begins.
% init_def has 3 arguments: the first one is the name of the predicate
% in the head of the clause(s) (usually new1), the second one is its arity,
% and the third one is the list of clause(s) that define new1.
% A clause is represented as a pair (Head, Body) where Head is an atom and
% Body a list of atoms. The following two lines specify that the initial
% program is match and the initial definition is the clause
% new1(A) :- match([a,a,b],A), which corresponds
% to the specialization of the predicate match for the input pattern aab.
% The next two commented lines show how to specify that the initial
% program is multi_match and the initial definition is the clause
% new1(A,B) :- m_match([[a,a,a],[a,a,b]],A,B), which corresponds
% to the specialization of the predicate m_match for the two
% input patterns aaa and aab.
% Examples:
%file_input('Progs/match').
%init_def(new1,1,[(new1(A), [match([a,a,b],A)])]).
%file_input('Progs/multi_match').
%init_def(new1,2,[(new1(A,B), [m_match([[a,a,a],[a,a,b]],A,B)])]).
%init_def(new1,2,[(new1(A,B), [m_match([[a,a],[a,b]],A,B)])]).
%init_def(new1,2,[(new1(A,B), [match([a,a,b],A,B)])]).

% strat specifies the value of some parameters for the subsidiary strategies.
% The possible arguments of strat are the following:
% * apply_case_split(global_analysis): case split is applied, according to the
%   global analysis strategy (the whole set of packets is defined in one
%   transformation step only).
% * apply_case_split(binary): binary case split is applied, that is case split
%   is applied as long as there exist two clauses which are not mutually
%   exclusive neither belong to the same packet (that is, have equal heads).
% If none of the above two parameters are selected, the case split rule is
% never applied.
% * apply_subsumption(during_case_split): subsumption is applied after each
%   application of the case split rule. It is meaningful only if the the binary
%   case  split has been selected (since case split by global analysis
%   corresponds to one transformation step only).
% * apply_subsumption(after_case_split): subsumption is applied after all
%   applications of the case split rule (that is, before folding).
% * apply_simplification_eq(separate)
% * after_first_step_unfold_leftmost_det: after the first unfolding step of a
%   new definition clause (which is always done wrt to the leftmost atom of
%   its body), we go on unfolding each of the resulting clauses wrt the leftmost
%   atom of their body which corresponds to a deterministic unfolding (if it
%   exists).
% * after_first_step_unfold_leftmost_consumer: after the first unfolding step
%   of a new definition clause, we go on unfolding each of the resulting clauses
%   wrt the leftmost atom of their body which is a consumer (if it exists),
%   that is, whose input arguments are all instantiated to non variable terms.
% * after_first_step_unfold_leftmost_weak_consumer: same as above, except that
%   the condition of consumer is relaxed to the one of weak consumer, that is,
%   it is enough that at least one of the input argument is instantiated to a
%   non variable term.
% * unfold_only_non_instantiated_head: after the first unfolding step
%   of a new definition clause, we go on unfolding each of the resulting clauses
%   wrt the leftmost atom of their body, if their heads are non instanciated,
%   that is, are of the form p(X1,...,Xn) where X1,...,Xn are dinstinct variables.
% * delete_clauses_with_failing_body: a clause whose body contains an atom which
%   unify with no head of clause is deleted.
%
% The four lines below specify that:
% 1) the case split rule must be applied according to the `global analysis'
% method,
% 2) subsumption must be applied after unfolding (that is, before case split), 
% 3) after the first unfolding step, we go on unfolding each of the resulting
% clause wrt the leftmost consumer (if possible).
% 4) clauses with a failing body body are deleted.
% strat(apply_case_split(global_analysis)).
% strat(apply_subsumption(after_unfolding)).
% strat(after_first_step_unfold_leftmost_consumer).
% strat(delete_clauses_with_failing_body).
% The four lines below show how to specify that:
% 1) the binary case split rule must be applied,
% 2) after the first unfolding step, we go on unfolding each of the resulting
% clause wrt the leftmost weak consumer (if possible).
% 3) clauses with a failing body are deleted.
% strat(apply_case_split(binary)).
% strat(after_first_step_unfold_leftmost_weak_consumer).
% strat(delete_clauses_with_failing_body).

% mode(P,N,L) represents the modes associated to predicate P of arity N. L
% is a list of length N, with elements in {+,-}. The i-th element of L
% corresponds to the i-th argument of P. `+' specifies an input argument, that
% is, an argument which should contain a ground term at runtime.
% Examples:
% Modes for the `match' program:
%mode(match,2,[+,+]).
%mode(app,3,[-,-,+]).
% Modes for the `multi_match' program:
%mode(m_match,3,[+,+,-]).
%mode(match,3,[+,+,-]).
%mode(app,3,[-,-,+]).
%mode(len,2,[+,-]).


/*EXAMPLES*/

/*Match*/

% %%% INITIAL PROGRAM
% file_input('Progs/match').
%
% %%% INITIAL DEFINITION
% %init_def(new1,1,[(new1(A), [match([a,a,b],A)])]).
% init_def(new1,1,[(new1(A), [match([a,a,a,a,a,a,a,a,a,b],A)])]).
%
% %%% SUBSIDIARY STRATEGIES
% strat(after_first_step_unfold_leftmost_weak_consumer).
% strat(apply_subsumption(after_unfolding)).
% strat(delete_clauses_with_failing_body).
% strat(apply_case_split(binary)).
%
% %%% MODES
% %mode(match,2,[+,+]).
% mode(match,2,[-,+]).  % simulate lazy unfolding
% mode(app,3,[-,-,+]).


/*Match and compute position*/

% %%% INITIAL PROGRAM
% file_input('Progs/match_pos').
%
% %%% INITIAL DEFINITION
% %init_def(new1,2,[(new1(A,B), [match([a,a,b],A,B)])]).
% init_def(new1,2,[(new1(A,B), [match([a,a,a],A,B)])]).
% %init_def(new1,2,[(new1(A,B), [match([a,a,a,a,a,a,a,a,b],A,B)])]).
%
% %%% SUBSIDIARY STRATEGIES
% strat(after_first_step_unfold_leftmost_weak_consumer).
% strat(apply_subsumption(after_unfolding)).
% strat(delete_clauses_with_failing_body).
% strat(apply_case_split(binary)).
%
% %%% MODES
% mode(match,3,[-,-,-]).   %simulate lazy unfolding
% mode(app,3,[-,-,+]).
% mode(len,2,[+,-]).



/*Multiple Match (and compute position)*/

% %%% INITIAL PROGRAM
% file_input('Progs/multi_match').
%
% %%% INITIAL DEFINITION
% % init_def(new1,2,[(new1(A,B), [m_match([[a,a,a],[a,a,b]],A,B)])]).
% % init_def(new1,2,[(new1(A,B), [m_match([[a,a],[a,b]],A,B)])]).
% init_def(new1,2,[(new1(A,B), [m_match([[a,a],[a,a,a],[a,a,b]],A,B)])]).
%
% %%% SUBSIDIARY STRATEGIES
% %strat(after_first_step_unfold_leftmost_weak_consumer).
% strat(after_first_step_unfold_leftmost_consumer).
% strat(apply_subsumption(after_unfolding)).
% strat(delete_clauses_with_failing_body).
% strat(apply_case_split(binary)).
%
% %%% MODES
% %mode(m_match,3,[+,+,-]).  %NON-TERMINATING WITH unfold_leftmost_consumer
% mode(m_match,3,[+,-,-]).   %Simulate lazy unfolding
% % mode(match,3,[+,+,-]).
% mode(match,3,[-,-,-]).     %Simulate lazy unfolding
% mode(app,3,[-,-,+]).
% mode(len,2,[+,-]).


/*REGULAR EXPRESSIONS*/

% %%% INITIAL PROGRAM
% file_input('Progs/reg_expr').
%
% %%% INITIAL DEFINITION
% init_def(new1,2,[(new1(W), [in_language((a,(star(a),b))+(a,star(a)),W)])]).
% %init_def(new1,2,[(new1(W), [in_language((a,(star(a),b)),W)])]).
% %init_def(new1,2,[(new1(W), [in_language((a,(star(a+b),b)),W)])]).
% %init_def(new1,2,[(new1(W), [in_language(star(star(a)),W)])]).
% %init_def(new1,2,[(new1(W), [in_language(star((a,(star(a),b))),W)])]).
%
% %%% SUBSIDIARY STRATEGIES
% %strat(after_first_step_unfold_leftmost_weak_consumer).  %NON-TERMINATING
% strat(after_first_step_unfold_leftmost_consumer).
% strat(apply_subsumption(after_unfolding)).
% strat(delete_clauses_with_failing_body).
% strat(apply_case_split(binary)).
%
% %%% MODES
% mode(in_language,2,[+,+]).
% mode(accepts,2,[+,+]).
% mode(app,3,[-,-,+]).
% mode(ne_app,3,[-,-,+]).
% mode(symbol,1,[+]).
% mode(string,1,[+]).


/*REGULAR EXPRESSION MATCHING*/

% %%% INITIAL PROGRAM
% file_input('Progs/reg_expr_match').
%
% %%% INITIAL DEFINITION
% %init_def(new1,1,[(new1(W), [match((a,(star(a),b))+(a,star(a)),W)])]).
% %init_def(new1,1,[(new1(W), [match((a,(star(a),b)),W)])]).
% %init_def(new1,1,[(new1(W), [match(star(star(a)),W)])]).
% %init_def(new1,1,[(new1(W), [match(((a,star(a))+(star(a),b)),W)])]).
% init_def(new1,1,[(new1(W), [match(((a,a)+(star(a),b)),W)])]).
%
% %%% SUBSIDIARY STRATEGIES
% %strat(after_first_step_unfold_leftmost_weak_consumer).  %NON-TERMINATING
% strat(after_first_step_unfold_leftmost_consumer).
% strat(apply_subsumption(after_unfolding)).
% strat(delete_clauses_with_failing_body).
% strat(apply_case_split(binary)).
%
% %%% MODES
% %mode(match,2,[+,+]).
% mode(match,2,[-,-]).      % simulate lazy unfolding
% mode(accepts,2,[+,+]).
% mode(app,3,[-,-,+]).
% mode(ne_app,3,[-,-,+]).
% mode(symbol,1,[+]).

/*REGULAR EXPRESSIONS (DIFF-LISTS)*/

% %%% INITIAL PROGRAM
% file_input('Progs/reg_expr_diff').
%
% %%% INITIAL DEFINITION
% init_def(new1,3,[(new1(W), [accepts((a,(star(a),b))+(a,star(a)),W,[])])]).
%
% %%% SUBSIDIARY STRATEGIES
% %strat(after_first_step_unfold_leftmost_weak_consumer).
% strat(after_first_step_unfold_leftmost_consumer). %NOT-TERMINATING
% strat(apply_subsumption(after_unfolding)).
% strat(delete_clauses_with_failing_body).
% strat(apply_case_split(binary)).
%
% %%% MODES
% mode(accepts,3,[+,+,+]).
% mode(symbol,1,[+]).


/* CONTEXT-FREE PARSER */

% % INITIAL PROGRAM
% file_input('Progs/cfg_parse.pl').
%
% %%% INITIAL DEFINITION
% %init_def(new1,1,[(new1(W),
% %[parse([(s,[0]),(s,[1,s])],[s],W)])]).
%
% % init_def(new1,1,[(new1(W),
% % [parse([(s,[0]),(s,[1,s,0])],[s],W)])]). %not regular (does not terminate)
%
% % init_def(new1,1,[(new1(W),
% % [parse([(s,[0]),(s,[s,0])],[s],W)])]). %left recursive (does not terminate)
%
% init_def(new1,1,[(new1(W),
% [string_parse([(s,[0,u]),
%         (s,[0,v]),
%         (s,[0,w]),
%         (u,[0]),
%         (u,[0,u]),
%         (u,[0,v]),
%         (v,[0]),
%         (v,[0,v]),
%         (v,[0,u]),
%         (w,[1]),
%         (w,[0,w])
%         ],[s],W)])]).
%
% % init_def(new1,1,[(new1(W),
% % [string_parse([(s,[0,u]),
% %         (s,[1,v]),
% %         (u,[0]),
% %         (u,[0,v]),
% %         (u,[0,w]),
% %         (v,[1]),
% %         (v,[0,v]),
% %         (v,[1,u]),
% %         (w,[1]),
% %         (w,[1,w])
% %         ],[s],W)])]).
%
% %%% SUBSIDIARY STRATEGIES
% %strat(after_first_step_unfold_leftmost_weak_consumer). %NON-TERMINATING
% strat(after_first_step_unfold_leftmost_consumer).
% strat(apply_subsumption(after_unfolding)).
% strat(delete_clauses_with_failing_body).
% strat(apply_case_split(binary)).
%
% %%% MODES
% %mode(parse,3,[+,+,+]).
% mode(parse,3,[-,+,+]).     %simulate lazy unfolding
% mode(member,2,[-,+]).
% %mode(app,3,[+,+,-]).
% mode(app,3,[+,-,-]).       %simulate lazy unfolding
% mode(terminal,1,[+]).
% mode(nonterminal,1,[+]).
% mode(string_parse,3,[+,+,+]).
% mode(string,1,[+]).


/* CONTEXT-FREE PARSER (DIFF-LISTS) */

% %% INITIAL PROGRAM
% file_input('Progs/cfg_parse_diff.pl').
%
% %%% INITIAL DEFINITION
% %init_def(new1,1,[(new1(W),
% %[parse([(s,[0]),(s,[1,s])],[s],W,[])])]).
% init_def(new1,3,[(new1(W),
% [parse([(s,[0,u]),
%         (s,[0,v]),
%         (s,[0,w]),
%         (u,[0]),
%         (u,[0,u]),
%         (u,[0,v]),
%         (v,[0]),
%         (v,[0,v]),
%         (v,[0,u]),
%         (w,[1]),
%         (w,[0,w])
%         ],[s],W,[])])]).
%
% %%% SUBSIDIARY STRATEGIES
% %strat(after_first_step_unfold_leftmost_weak_consumer). %NON-TERMINATING
% strat(after_first_step_unfold_leftmost_consumer).
% strat(apply_subsumption(after_unfolding)).
% strat(delete_clauses_with_failing_body).
% strat(apply_case_split(binary)).
%
% %%% MODES
% % mode(parse,4,[+,+,+,+]).
% mode(parse,4,[+,+,+,-]).   % satisfied ?
% mode(member,2,[-,+]).
% mode(terminal,1,[+]).
% mode(nonterminal,1,[+]).


/* Approximate Matching */

%% INITIAL PROGRAM
file_input('Progs/approx_match.pl').

%%% INITIAL DEFINITION
%init_def(new1,2,[(new1(A,B), [a_match([a,a,b],A,B)])]).
init_def(new1,1,[(new1(A), [a_match([a,a,b],A,s(s(0)))])]).
%init_def(new1,1,[(new1(A), [a_match([a,a,a,a,b],A,s(s(0)))])]).

%%% SUBSIDIARY STRATEGIES
%strat(after_first_step_unfold_leftmost_weak_consumer). %NON-TERMINATING
strat(after_first_step_unfold_leftmost_consumer).
strat(apply_subsumption(after_unfolding)).
strat(delete_clauses_with_failing_body).
strat(apply_case_split(binary)).
%strat(apply_case_split(global_analysis)).

%%% MODES
mode(a_match,3,[+,+,+]).
mode(app,3,[-,-,+]).
mode(dist,3,[+,+,-]).
mode(leq,2,[+,+]).

