module compbasicstandard[vars,fss,prec]

/* Basic Completion with Standard Simplification */
/* version1 of sorting without using too much interclassment */
/* using constrained equations */

/* vars : les variables, 
   fss  : les operateurs,
   prec : la precedence */


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


operators
  global

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

	/* Standard 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 */

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

	/* STANDARD SIMPLIFICATION EQ - EQ => EQ */

	/* Standard 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 */

	standard_simplification_eq_eq(@,@,@): (eqconstrained 
		eqconstrained counter:int) eqconstrained;

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

	/* Standard 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 tuple of lists of equations [UQ,PQ] */

	standard_simplification_listeq_eq(@,@,@,@) : (list[eqconstrained]
	list[eqconstrained] eqconstrained counter:int) 
	tuple[list[eqconstrained], list[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 constrained equations */
	/* 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 equation 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];
end


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

rules for eqconstrained
	counter, newcounter		: int;
	e, ee, esimp, eefin, eqesimp	: eqconstrained;
	l, lorig			: list[eqconstrained];
	res				: eqconstrained;
	cond1, cond2			: bool;
	eq				: equation;
global

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

	[] standard_simplification_eq_listeq(e, ee.l, lorig, counter)=> 
		res
		where eefin	:= ()translate(normalize(ee),maxvar(e,0))
		where esimp	:= (Main_SSimp)Standard_Simplification_Main(e,eefin,
				counter)
		where cond1	:= ()meqeqconstrained(esimp,e)
		where eqesimp	:= (propagate)propagate(esimp)
		where eq	:= ()equation(eqesimp)
		where cond2 	:= ()eq_term(lhs(eq), rhs(eq))
		where newcounter:= ()maxcounter(esimp.nil,counter)
		choose
		try
		if cond1
			where res := 
			()standard_simplification_eq_listeq(e, l, 
			lorig, counter)
		try
		if not cond1
			choose
			try
			if cond2
				where res := ()esimp
			try
			if not cond2
				where res := 
				()standard_simplification_eq_listeq(esimp,
				lorig,lorig,newcounter+1)
			end
		end
	end
end 


/* STANDARD SIMPLIFICATION EQ - EQ */

rules for eqconstrained
	e, ee		: eqconstrained;
	counter		: int;
global

	[] standard_simplification_eq_eq(e, ee, counter)	=> 
		standard_simplification_eq_listeq(e,ee.nil,ee.nil,counter)
	end
end


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

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

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

	[] standard_simplification_listeq_eq(UQ, ee.PQ, e, counter)	=> 
		res
		where esimp 	:= 
			()standard_simplification_eq_eq(ee,e,counter)
		where cond1 	:= ()meqeqconstrained(esimp,ee)
		where newcounter:= ()maxcounter(esimp.nil,counter)
		where eqesimp	:= (propagate)propagate(esimp)
		where cond2 	:= ()eq_term(lhs(equation(eqesimp)),
		rhs(equation(eqesimp)))
		choose
		try
		if cond1
			where p		:= 
			()standard_simplification_listeq_eq(UQ,PQ,e,counter)
			where res 	:= ()[1-th(p),ee.2-th(p)]
		try
		if not cond1
			choose
			try
			if cond2
				where cond3 := ()eq_term(tempty,
				lhs(equation(eqesimp)))
				choose
				try
				if cond3
					where p		:= 
					()standard_simplification_listeq_eq(UQ,
					PQ,e,newcounter-1)
					where res := ()[1-th(p),2-th(p)]
				try
				if not cond3
					where p		:= 
					()standard_simplification_listeq_eq(UQ,
					PQ,e,newcounter+1)
					where res := ()[1-th(p),2-th(p)]
				end
			try
			if not cond2
				where p		:= 
				()standard_simplification_listeq_eq(UQ,PQ,e,
				newcounter+1)
				where res := ()[append(1-th(p),esimp.nil),
				2-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;
	lhs, rhs 			: term;
	e, ee, esimp, eqesimp		: eqconstrained;
	PQ, UQ, UQ0, PQ0, UQ1, UQ2s, PQ2s, res : list[eqconstrained];
	pUQPQ 				: 
		tuple[list[eqconstrained],list[eqconstrained]];
	cond1, cond2, cond3		: bool;
global

	[] completion(nil, PQ, counter)		=> PQ
	end

	[] completion(e.UQ, PQ, counter) 	=> 
		res
		where esimp 	:= 
			()standard_simplification_eq_listeq(e, PQ, PQ,counter)
		where eqesimp	:= (propagate)propagate(esimp)
		where lhs 	:= ()lhs(equation(eqesimp))
		where rhs 	:= ()rhs(equation(eqesimp))
		where newcounter1:= ()maxcounter(esimp.nil,counter)
		where cond1	:= ()$lhs == $rhs
		where cond2	:= ()meqeqconstrained(e, esimp)
		choose
		try
		if cond1
			where cond3 := ()$lhs == tempty
			choose
			try
			if cond3
				where res := ()completion(UQ,PQ,newcounter1-1)
			try
			if not cond3
				where res := ()completion(UQ,PQ,newcounter1)
			end
		try
		if not cond1
			choose
			try
			if cond2
				where pUQPQ 	:= 
				()standard_simplification_listeq_eq(UQ,PQ,
				esimp,counter)
				where UQ0 	:= ()1-th (pUQPQ)
				where PQ0 	:= ()2-th(pUQPQ)
				where newcounter2:=()maxcounter(UQ0,counter)
				where UQ1 	:= 
				()basic_critical_pair_eq_listeq(esimp,
				esimp.PQ0,newcounter2)
				where newcounter3:= ()maxcounter(UQ1,
				newcounter2)
				where UQ2s 	:= ()sortinter(append(UQ0,UQ1))
				where PQ2s 	:= ()sortinter(append(PQ0,
				esimp.nil))
				where res := ()completion(UQ2s,PQ2s,
				newcounter3)
			try
			if not cond2
				where pUQPQ 	:= 
				()standard_simplification_listeq_eq(UQ,PQ,
				esimp,newcounter1)
				where UQ0 	:= ()1-th (pUQPQ)
				where PQ0 	:= ()2-th(pUQPQ)
				where newcounter2:=()maxcounter(UQ0,
				newcounter1)
				where UQ1 	:= 
				()basic_critical_pair_eq_listeq(esimp,
				esimp.PQ0,newcounter2)
				where newcounter3:= ()maxcounter(UQ1,
				newcounter2)
				where UQ2s 	:= ()sortinter(append(UQ0,UQ1))
				where PQ2s 	:= ()sortinter(append(PQ0,
				esimp.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


end