module compbasicbasic[vars,fss,prec]

/* Basic Completion with Basic Simplification retraction max */


/* vars : variables, 
   fss  : operators,
   prec : precedence */


import	
	global  
		strapply[eqconstrained]
		cpbasicbasic[vars,fss,prec]
		eqSystem[fss,vars]
	;
       
        local 
		vars
		fss
		prec
		list[eqconstrained]
		tuple[2,eqconstrained,list[eqconstrained]]
		tuple[2,eqconstrained,eqconstrained]
		tuple[2,list[eqconstrained],list[eqconstrained]]
		eq[list[eqconstrained]]
		tuple[3,list[eqconstrained],list[eqconstrained],eqconstrained]
	;
end


operators
  global

	/* BASIC SIMPLIFICATION EQ - LISTEQ (1) => EQ */

	/* Basic simplification of an equation by a list of equations */
	/* (in fact PQ) at all positions*/

	/* parameter 1: an equation */
	/* parameter 2: a list of equations (initially PQ) */
	/* parameter 3: a list of equations (always PQ) */
	/* parameter 4: a counter */
	/* result: an equation (the simplified equation) and */
	/* 	   the new PQ list */

	basic_simplification_eq_listeq(@,@,@,@): (eqconstrained 
		list[eqconstrained] list[eqconstrained] counter:int) 
		tuple[eqconstrained,list[eqconstrained]];

	/* BASIC SIMPLIFICATION EQ - EQ => EQ */

	/* Basic Simplification of an equation by another */
	/* equation at all positions */

	/* parameter 1: an equation (of PQ) */
	/* parameter 2: an equation */
	/* parameter 3: a counter */
	/* result : an equation and a new PQ list */

	basic_simplification_eq_eq(@,@,@): (eqconstrained 
		eqconstrained counter:int) 
		tuple[eqconstrained,list[eqconstrained]];

	/* BASIC SIMPLIFICATION LISTEQ (PQ) - EQ (2) => UQ,PQ */

	/* Basic Simplification of a list of equations (in fact PQ) by an */
	/* equation at all positions */

	/* parameter 1: a list of equations (UQ) */
	/* parameter 2: a list of equations (PQ) */
	/* parameter 3: an equation */
	/* parameter 4: a counter */
	/* result : a triplet of lists of equations UQ,PQ and */
	/* the deduced equation */

	basic_simplification_listeq_eq(@,@,@,@) : (list[eqconstrained]
	list[eqconstrained] eqconstrained counter:int) tuple[list[eqconstrained], 
	list[eqconstrained],eqconstrained];

	/* BASIC CRITICAL PAIR EQ - LISTEQ => UQ,PQ (3) */

	/* Calculus of the basic critical pair between an equation and */
	/* a list of equation (in fact this equation + PQ) at all positions */
	/* parameter 1: an equation */
	/* parameter 2: a list of equations */
	/* parameter 3: a counter */
	/* result: list[eqconstrained] = list of (ext)equation(1)s resulting */
	/* of the calculus of critical pairs */

	basic_critical_pair_eq_listeq(@,@,@)	: 
	(eqconstrained list[eqconstrained] counter:int) list[eqconstrained];

	/* COMPLETION */

	/* Completion of the list of extquation1 given as argument (UQ) */
	/* The result is in PQ */
	/* parameter 1: a list of equations (UQ) */
	/* parameter 2: a list of equations (PQ) */
	/* parameter 3: a counter */
	/* result: a list of processed equations (PQ) */

	completion(@,@,@): (list[eqconstrained] list[eqconstrained] counter:int) 
	list[eqconstrained];

	/* INTERMEDIARY FUNCTIONS */

	/* maximal counter of a list of eqconstrained */
	maxcounter(@,@)	: (list[eqconstrained] int) int;
	maxcounter1(@,@): (list[eqconstrained] int) int;

	/* Given a list of eqconstraineds and a counter, the counters of */
	/* each element of the list are changed from counter */
	/* This was useful because the dedstrat stategie is a dk and */
	/* all the equations have the same counter */

	chgtcounter(@,@) : (list[eqconstrained] counter:int) list[eqconstrained];

	/* sort of a list[eqconstrained] */ 
	sortinter(@)	: (list[eqconstrained])	list[eqconstrained];

	/* interclassment of two sorted list[eqconstrained] */
	interclass(@,@)	: (list[eqconstrained] list[eqconstrained]) 
	list[eqconstrained];

	/* Given the list[eqconstrained] li containing an object eqconstrained */
	/* eq11 = eq,num,...and an extequation eq12 = eq,num,... */
	/* The result of replacel is li where eq11 is */
	/* replaced by eq12 */
	replacel(@,@)	: (list[eqconstrained] eqconstrained) 
	list[eqconstrained];
end


/* BASIC SIMPLIFICATION EQ - LISTEQ  (1) */

rules for tuple[eqconstrained,list[eqconstrained]]
	counter, newcounter	: int;
	e, ee, eefin, eqesimp	: eqconstrained;
	l, lorig, lorig1	: list[eqconstrained];
	tupsimplr		: tuple[eqconstrained,eqconstrained];
	res			: tuple[eqconstrained,list[eqconstrained]];
	cond1, cond2		: bool;
global

	[] basic_simplification_eq_listeq(e, nil, lorig, counter) => 
		[e,lorig]
	end 

	[] basic_simplification_eq_listeq(e, ee.l, lorig, counter)=> 
	res
	where eefin	:= ()translate(normalize(ee),maxvar(e,0))
	where tupsimplr	:= 
	(Main_BSimp)Basic_Simplification_Main(e,eefin,counter)
	where cond1	:= ()meqeqconstrained(2-th(tupsimplr),e)
	where eqesimp	:= (propagate)propagate(2-th(tupsimplr))
	where cond2	:= 
	()eq_term(lhs(equation(eqesimp)),rhs(equation(eqesimp)))
	where newcounter:= ()maxcounter(2-th(tupsimplr).nil,counter)
	choose
	try
	if cond1
		where res := 
		()basic_simplification_eq_listeq(e, l, lorig, counter)
	try
	if not cond1
		choose
		try
		if cond2
			where lorig1 := ()replacel(lorig,1-th(tupsimplr))
			where res := ()[2-th(tupsimplr),lorig1]
		try
		if not cond2
			where lorig1 := ()replacel(lorig,1-th(tupsimplr))
			where res := 
			()basic_simplification_eq_listeq(2-th(tupsimplr),
			lorig1,lorig1,newcounter+1)
		end
	end
	end
end 


/* BASIC SIMPLIFICATION EQ - EQ */

rules for tuple[eqconstrained,list[eqconstrained]]
	e, ee		: eqconstrained;
	counter		: int;
global

	[] basic_simplification_eq_eq(e, ee, counter)	=> 
		basic_simplification_eq_listeq(e,ee.nil,ee.nil,counter)
	end
end


/* BASIC SIMPLIFICATION LISTEQ - EQ (2) */

rules for tuple[list[eqconstrained],list[eqconstrained],eqconstrained]
	counter, newcounter	: int;
	e, ee, eqesimp		: eqconstrained;
	PQ, UQ			: list[eqconstrained];
	p, res 			: 
	tuple[list[eqconstrained],list[eqconstrained],eqconstrained];
	tupsimplr			: tuple[eqconstrained,list[eqconstrained]];
	cond1, cond2, cond3	: bool;
global

	[] basic_simplification_listeq_eq(UQ, nil, e, counter)	=> 
		[UQ,nil,e]
	end

	[] basic_simplification_listeq_eq(UQ, ee.PQ, e, counter)	=> 
	res
	where tupsimplr 	:= ()basic_simplification_eq_eq(ee,e,counter)
	where cond1	:= ()meqeqconstrained(1-th(tupsimplr),ee)
	where newcounter:= ()maxcounter(1-th(tupsimplr).nil,counter)
	where eqesimp	:= (propagate)propagate(1-th(tupsimplr))
	where cond2	:= ()eq_term(lhs(equation(eqesimp)),rhs(equation(eqesimp)))
	choose
	try
	if cond1
		where p		:= 
		()basic_simplification_listeq_eq(UQ,PQ,e,counter)
		where res := ()[1-th(p),ee.2-th(p),3-th(p)]
	try
	if not cond1
		choose
		try
		if cond2
			where cond3 := ()eq_term(tempty,lhs(equation(eqesimp)))
			choose
			try
			if cond3	/* blocking */
				where p		:= 
				()basic_simplification_listeq_eq(UQ,PQ,
				1-th elem(2-th(tupsimplr)),newcounter-1)
				where res := 
				()[1-th(p),2-th(p),3-th(p)]
			try
			if not cond3
				where p		:= 
				()basic_simplification_listeq_eq(UQ,PQ,
				1-th elem(2-th(tupsimplr)),newcounter+1)
				where res := 
				()[1-th(p),2-th(p),3-th(p)]
			end
		try
		if not cond2	
			where p		:= 
			()basic_simplification_listeq_eq(UQ,PQ,
			1-th elem(2-th(tupsimplr)),newcounter+1)
			where res := ()[append(1-th(p),
			1-th(tupsimplr).nil),2-th(p),3-th(p)]
		end
	end
	end
end


/* BASIC CRITICAL PAIR (3) */


rules for list[eqconstrained]
	counter, newcounter				: int;
	e, ee, eefin					: eqconstrained;
	l, leqres, leqres0, leqres1, leqres2, res	: list[eqconstrained];
	cond						: bool;
global

	[] basic_critical_pair_eq_listeq(e, nil, counter)	
		=> nil
	end

	[] basic_critical_pair_eq_listeq(e, ee.l, counter)	
		=>  res
		where eefin	:= ()translate(normalize(ee),maxvar(e,0))
		where cond	:= ()meqeqconstrained(e,ee)
		choose
		try
		if cond
			/* first round, because of the algorithm */
			where leqres0 	:= ()setof(Main_BCP_b,
			Basic_Critical_Pair_Main(e,eefin,counter))
			where leqres1	:= ()chgtcounter(leqres0,counter)
			where newcounter:= ()maxcounter(leqres1,counter)
			where leqres2   := 
			()basic_critical_pair_eq_listeq(e, l, newcounter)
			where res 	:= ()append(leqres1,leqres2) 
		try
		if not cond
			where leqres0 	:= 
			()setof(Main_BCP_a,Basic_Critical_Pair_Main(e,eefin,counter))
			where leqres1	:= ()chgtcounter(leqres0,counter)
			where newcounter:= ()maxcounter(leqres1,counter)
			where leqres2   := 
			()basic_critical_pair_eq_listeq(e, l, newcounter)
			where res	:= ()append(leqres1,leqres2) 
		end
	end
end


/* COMPLETION */


rules for list[eqconstrained]
	counter, newcounter1, newcounter2, newcounter3	: int;
	e, ee, eqesimp					: eqconstrained;
	PQ, UQ, UQ0, PQ0, UQ1, UQ2s, PQ2s, res		: list[eqconstrained];
	pUQPQ 						: 
				tuple[list[eqconstrained],list[eqconstrained]];
	tUQPQ 						: 
				tuple[list[eqconstrained],list[eqconstrained],
				eqconstrained];
	tupsimplr						: 
				tuple[eqconstrained,list[eqconstrained]];
	cond1, cond2, cond3				: bool;
global
	[] completion(nil, PQ, counter)		=> PQ
	end

	[] completion(e.UQ, PQ, counter) 	=> res
		where tupsimplr 	:= 
			()basic_simplification_eq_listeq(e, PQ, PQ,counter)
		where eqesimp	:= (propagate)propagate(1-th(tupsimplr))
		where newcounter1:= ()maxcounter(1-th(tupsimplr).nil,counter)
		where cond1	:= ()eq_term(lhs(equation(eqesimp)),rhs(equation(eqesimp)))
		where cond2	:= ()meqeqconstrained(e,1-th(tupsimplr))
		choose
		try
		if cond1
			where cond3 := ()eq_term(lhs(equation(eqesimp)),tempty)
			choose
			try
			if cond3
				where res := ()completion(UQ,2-th(tupsimplr),
				newcounter1-1)
			try
			if not cond3
				where res := ()completion(UQ,2-th(tupsimplr),
				newcounter1)
			end
		try
		if not cond1
			choose
			try
			if cond2
				where tUQPQ 	:= 
				()basic_simplification_listeq_eq(UQ,
				2-th(tupsimplr),1-th(tupsimplr),counter)
				where UQ0 	:= ()1-th(tUQPQ)
				where PQ0 	:= ()2-th(tUQPQ)
				where newcounter2:=
				()maxcounter(UQ0,counter)
				where UQ1 	:= 
				()basic_critical_pair_eq_listeq(3-th(tUQPQ),
				3-th(tUQPQ).PQ0,newcounter2)
				where newcounter3:= 
				()maxcounter(UQ1,newcounter2)
				where UQ2s 	:= ()sortinter(append(UQ0,UQ1))
				where PQ2s 	:= 
				()sortinter(append(PQ0,3-th(tUQPQ).nil))
				where res := 
				()completion(UQ2s,PQ2s,newcounter3)
			try
			if not cond2
				where tUQPQ 	:= 
				()basic_simplification_listeq_eq(UQ,
				2-th(tupsimplr),1-th(tupsimplr),newcounter1)
				where UQ0 	:= ()1-th(tUQPQ)
				where PQ0 	:= ()2-th(tUQPQ)
				where newcounter2:=
				()maxcounter(UQ0,newcounter1)
				where UQ1 	:= 
				()basic_critical_pair_eq_listeq(3-th(tUQPQ),
				3-th(tUQPQ).PQ0,newcounter2)
				where newcounter3:= 
				()maxcounter(UQ1,newcounter2)
				where UQ2s 	:= ()sortinter(append(UQ0,UQ1))
				where PQ2s 	:= 
				()sortinter(append(PQ0,3-th(tUQPQ).nil))
				where res := 
				()completion(UQ2s,PQ2s,newcounter3)
			end

		end
	end

end


/* INTERMEDIARY FUNCTIONS */


/* chgtcounter */

rules for list[eqconstrained]
	counter1, counter 	: int;
	eq1	 		: equation;
	c1			: constraint;
	leqc			: list[eqconstrained];
global
	[] chgtcounter(nil,counter)			=> nil
	end

	[] chgtcounter(eq1[c1]<counter1>.leqc, counter)	=> 
		eq1[c1]<counter>.chgtcounter(leqc,counter+1)
	end
end


/* maxcounter1 */

rules for int
        eqc     : eqconstrained;
        leqc    : list[eqconstrained];
        counter : int;
global
        [] maxcounter1(nil,counter)             => 
                        counter
        end 

        [] maxcounter1(eqc.leqc,counter)        => 
                        maxcounter1(leqc,counter(eqc))
                        if counter(eqc) >= counter
        end

        [] maxcounter1(eqc.leqc,counter)        => 
                        maxcounter1(leqc,counter)
        end
end


/* maxcounter */

rules for int
        eqc                     : eqconstrained;
        leqc                    : list[eqconstrained];
        counter, counter1, res  : int;
        cond                    : bool;
global
        [] maxcounter(nil,counter)              => 
                        counter
        end 

        [] maxcounter(eqc.leqc,counter)         => 
		res
		where counter1  := ()maxcounter1(eqc.leqc,0)
		where cond      := ()counter1 >= counter
		choose
		try
                        
		if cond
			where res := ()counter1 + 1
		try
		if not cond
			where res := ()counter
		end        
		end
end


/* interclass */

rules for list[eqconstrained]
        leqc1, leqc2, res       : list[eqconstrained];
        eqc1, eqc2              : eqconstrained;
        cond                    : bool;
global
        [] interclass(nil, leqc2)               => leqc2
        end

        [] interclass(leqc1, nil)               => leqc1
        end

        [] interclass(eqc1.leqc1,eqc2.leqc2)    => res
		where cond      := ()size(eqc1) <= size(eqc2)
		choose
		try
		if cond
			where res := ()eqc1.interclass(leqc1,eqc2.leqc2)
		try
		if not cond
			where res := ()eqc2.interclass(eqc1.leqc1,leqc2)
		end
	end
end


/* sortinter */

rules for list[eqconstrained]
        eqc 			: eqconstrained;
        leqc, leqc1, leqc2	: list[eqconstrained];
global
        [] sortinter(nil) => nil
        end

        [] sortinter(eqc.nil) => eqc.nil
        end

        [] sortinter(eqc.leqc) => leqc2
                if not eq_list[eqconstrained](leqc, nil)
                where leqc2 := () interclass(eqc.nil,sortinter(leqc))
        end
end


/* replacel */

rules for list[eqconstrained]
	eqc			: eqconstrained;
	c1, c2			: constraint;
	eq1, eq2		: equation;
	leqc			: list[eqconstrained];
	counter1, counter2	: int;
global
	[] replacel(nil,eqc)	=> nil
	end

	[] replacel(eq1[c1]<counter1>.leqc,eq2[c2]<counter2>)=> 
			eq2[c2]<counter2>.leqc
			if eq_int(counter1,counter2)
	end

	[] replacel(eq1[c1]<counter1>.leqc,eq2[c2]<counter2>) => 
			eq1[c1]<counter1>.replacel(leqc,eq2[c2]<counter2>)
	end
end


end