module compbasicecycle[fss,vars,prec]

/* Graph not in transitive closure form */

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


import	
	global  
		strapply[eqconstrainedg]
		cpbasicecycle[fss,vars,prec]
	;
       
        local 
		vars
		fss
		prec
		graph[fss,vars,prec]
		list[eqconstrainedg]
		eq[list[eqconstrainedg]]
		tuple[2,eqconstrainedg,graph]
		tuple[2,list[eqconstrainedg],graph]
		tuple[2,list[eqconstrainedg],list[eqconstrainedg]]
		tuple[3,list[eqconstrainedg],list[eqconstrainedg],graph]
	;
end


operators
  global
	/* ECYCLE SIMPLIFICATION EQ - LISTEQ (1) => EQ */

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

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

	ecycle_simplification_eq_listeq(@,@,@,@,@): (eqconstrainedg graph
	list[eqconstrainedg] list[eqconstrainedg] counter:int) 
	tuple[eqconstrainedg,graph];

	/* ECYCLE SIMPLIFICATION EQ - EQ => EQ */

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

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

	ecycle_simplification_eq_eq(@,@,@,@): (eqconstrainedg graph
	eqconstrainedg counter:int) tuple[eqconstrainedg,graph];

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

	/* Ecycle 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: a graph */
	/* parameter 4: an equation */
	/* parameter 5: a counter */
	/* result : a triplet of lists of equations UQ,PQ and a graph */

	ecycle_simplification_listeq_eq(@,@,@,@,@) : (list[eqconstrainedg]
	list[eqconstrainedg] graph eqconstrainedg counter:int) 
	tuple[list[eqconstrainedg],list[eqconstrainedg],graph];

	/* 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 graph */
	/* parameter 3: a list of equations */
	/* parameter 4: a counter */
	/* result: list[eqconstrainedg] = list of equations */
	/* resulting of the calculus of critical pairs and a graph */

	basic_critical_pair_eq_listeq(@,@,@,@)	: 
	(eqconstrainedg graph list[eqconstrainedg] counter:int) 
	tuple[list[eqconstrainedg],graph];

	/* COMPLETION */

	/* Completion of the list of eqconstrainedg 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 graph */
	/* parameter 4: a counter */
	/* result: a list of processed equations (PQ) */

	completion(@,@,@,@): (list[eqconstrainedg] list[eqconstrainedg] 
	graph counter:int) list[eqconstrainedg];
end


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


rules for tuple[eqconstrainedg,graph]
	counter, newcounter	: int;
	cond1, cond2		: bool;
	lhs, rhs 		: term;
	e, ee, eefin,eqsimpc	: eqconstrainedg;
	esimpg			: tuple[eqconstrainedg,graph];
	l, lorig		: list[eqconstrainedg];
	G 			: graph;
	res			: tuple[eqconstrainedg,graph];
global

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

	[] ecycle_simplification_eq_listeq(e, G, ee.l, lorig, counter)=> 
	res
	where eefin	:= ()translate(normalize(ee),maxvar(e,0))
	where esimpg	:= 
	(Main_ESimp)Ecycle_Simplification_Main(e,eefin,G,counter)
	where cond1	:= ()meqeqconstrainedg(1-th(esimpg),e)
	where eqsimpc	:= (propagate)propagate(1-th(esimpg))
	where cond2 	:= ()eq_term(lhs(equation(eqsimpc)),
	rhs(equation(eqsimpc)))
	where newcounter:= ()maxcounter(1-th(esimpg).nil,counter)
	choose
	try
	if cond1
		where res := 
		()ecycle_simplification_eq_listeq(e, G, l, lorig, counter)
	try
	if not cond1
		choose
		try
		if cond2
			where res := ()esimpg
		try
		if not cond2
			where res := ()ecycle_simplification_eq_listeq(
			1-th(esimpg),2-th(esimpg),lorig,lorig,newcounter+1)
		end
	end
	end
end 


/* ECYCLE SIMPLIFICATION EQ - EQ */

rules for tuple[eqconstrainedg,graph]
	e, ee		: eqconstrainedg;
	counter		: int;
	G		: graph;
global

	[] ecycle_simplification_eq_eq(e, G, ee, counter)	=> 
	ecycle_simplification_eq_listeq(e,G,ee.nil,ee.nil,counter)
	end
end


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


rules for tuple[list[eqconstrainedg],list[eqconstrainedg],graph]
	counter, newcounter	: int;
	lhs, rhs		: term;
	e, ee, esimpg,eqsimpc	: eqconstrainedg;
	esimpg			: tuple[eqconstrainedg,graph];
	PQ, UQ, PQ1, UQ1	: list[eqconstrainedg];
	p 			: tuple[list[eqconstrainedg],
				list[eqconstrainedg],graph];
	G			: graph;
	res			: tuple[list[eqconstrainedg],
				list[eqconstrainedg],graph];
	cond1, cond2, cond3	: bool;
global

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

	[] ecycle_simplification_listeq_eq(UQ, ee.PQ, G, e, counter)	=> 
	res
	where esimpg 	:= ()ecycle_simplification_eq_eq(ee,G,e,counter)
	where cond1	:= ()meqeqconstrainedg(1-th(esimpg),ee)
	where eqsimpc	:= (propagate)propagate(1-th(esimpg))
	where cond2	:= ()eq_term(lhs(equation(eqsimpc)),
	rhs(equation(eqsimpc)))
	where newcounter := ()maxcounter(1-th(esimpg).nil,counter)
	choose
	try
	if cond1 
		where p	:= ()ecycle_simplification_listeq_eq(UQ,PQ,
		G,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(lhs(equation(1-th(esimpg))),tempty)
			choose
			try
			if cond3	/* blocking */
				where p	:= 
				()ecycle_simplification_listeq_eq(UQ,PQ,
				2-th(esimpg),e,newcounter-1)
				where res := ()[1-th(p),2-th(p),3-th(p)]
			try
			if not cond3
				where p	:= 
				()ecycle_simplification_listeq_eq(UQ,PQ,
				2-th(esimpg),e,newcounter+1)
				where res := ()[1-th(p),2-th(p),3-th(p)]
			end
		try
		if not cond2
			where p	:= ()ecycle_simplification_listeq_eq(UQ,PQ,
			2-th(esimpg),e,newcounter+1)
			where res := ()[append(1-th(p),1-th(esimpg).nil),
			2-th(p),3-th(p)]
		end
	end
	end
end


/* BASIC CRITICAL PAIR (3) */


rules for tuple[list[eqconstrainedg],graph]
	counter, newcounter		: int;
	e, ee, eefin			: eqconstrainedg;
	l, leqres0s			: list[eqconstrainedg];
	leqres0, leqres1		: tuple[list[eqconstrainedg],graph];
	G				: graph;
	cond				: bool;
	res				: tuple[list[eqconstrainedg],graph];
global

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


	[] basic_critical_pair_eq_listeq(e, G, ee.l, counter)	
	=> 
	res
	where eefin	:= ()translate(normalize(ee),maxvar(e,0))
	where cond 	:= ()meqeqconstrainedg(e,eefin)
	choose
	try
	if cond
		/* first round, because of the algorithm */
		where leqres0 	:= ()Basic_Critical_Pair_a(e,eefin,G,counter)
		where leqres0s	:= ()sortinter(1-th(leqres0))
		where newcounter:= ()maxcounter(1-th(leqres0),counter)
		where leqres1   := 
		()basic_critical_pair_eq_listeq(e,2-th(leqres0),l,newcounter)
		where res := 
		()[interclass(leqres0s,1-th(leqres1)),2-th(leqres1)] 
	try
	if not cond
		where leqres0 	:= ()Basic_Critical_Pair_b(e,eefin,G,counter)
		where leqres0s	:= ()sortinter(1-th(leqres0))
		where newcounter:= ()maxcounter(1-th(leqres0),counter)
		where leqres1   := 
		()basic_critical_pair_eq_listeq(e,2-th(leqres0), 
		l,newcounter)
		where res := 
		()[interclass(leqres0s,1-th(leqres1)),2-th(leqres1)]
	end
	end
end


/* COMPLETION */


rules for list[eqconstrainedg]
	counter, newcounter1, newcounter2, newcounter3: int;
	lhs, rhs 			: term;
	e, ee, eqsimpc			: eqconstrainedg;
	esimpg				: tuple[eqconstrainedg, graph];
	PQ, UQ, UQ0, PQ0, UQ1, UQ2s, PQ2s : list[eqconstrainedg];
	pUQPQG 				: 
		tuple[list[eqconstrainedg],list[eqconstrainedg],graph];
	pUQG				: tuple[list[eqconstrainedg],graph];
	G, G0, G1			: graph;
	cond1, cond2, cond3		: bool;
	res				: list[eqconstrainedg];
global

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

	[] completion(e.UQ, PQ, G, counter) 		=> res
	where esimpg 	:= 
		()ecycle_simplification_eq_listeq(e, G, PQ, PQ, counter)
	where eqsimpc	:= (propagate)propagate(1-th(esimpg))
	where newcounter1:= ()maxcounter(1-th(esimpg).nil,counter) 	
	where lhs	:= ()lhs(equation(eqsimpc))
	where rhs	:= ()rhs(equation(eqsimpc))
	where cond1 	:= ()$lhs == $rhs
	where cond2 	:= ()meqeqconstrainedg(e,1-th(esimpg))
	choose
	try 
	if cond1
		where cond3	:= ()$lhs == tempty
		choose
		try
		if cond3
			where res := 
			()completion(UQ,PQ,2-th(esimpg),newcounter1-1)
		try
		if not cond3
			where res := 
			()completion(UQ,PQ,2-th(esimpg),newcounter1)
		end
	try
	if not cond1
		choose 
		try
		if cond2
			where pUQPQG 	:= 
			()ecycle_simplification_listeq_eq(UQ,PQ,2-th(esimpg),
			1-th(esimpg),counter) 
			where UQ0 	:= ()1-th(pUQPQG)
			where PQ0 	:= ()2-th(pUQPQG)
			where G0	:= ()3-th(pUQPQG)
			where newcounter2:=()maxcounter(UQ0,counter)	
			where pUQG 	:= 
			()basic_critical_pair_eq_listeq(1-th(esimpg),G0,
			1-th(esimpg).PQ0,newcounter2) 
			where UQ1	:= ()1-th(pUQG)
			where G1	:= ()2-th(pUQG)
			where newcounter3:= ()maxcounter(UQ1,newcounter2)
			where UQ2s 	:= ()sortinter(append(UQ0,UQ1))
			where PQ2s 	:= 
			()sortinter(append(PQ0,1-th(esimpg).nil))
			where res	:= 
			()completion(UQ2s,PQ2s,G1,newcounter3)
		try
		if not cond2
			where pUQPQG 	:=
 			()ecycle_simplification_listeq_eq(UQ,PQ,
			2-th(esimpg),1-th(esimpg),newcounter1) 
			where UQ0 	:= ()1-th(pUQPQG)
			where PQ0 	:= ()2-th(pUQPQG)
			where G0	:= ()3-th(pUQPQG)
			where newcounter2:=()maxcounter(UQ0,newcounter1)
			where pUQG 	:= 
			()basic_critical_pair_eq_listeq(1-th(esimpg),G0,
			1-th(esimpg).PQ0,newcounter2) 
			where UQ1	:= ()1-th(pUQG)
			where G1	:= ()2-th(pUQG)
			where newcounter3:= ()maxcounter(UQ1,newcounter2)
			where UQ2s 	:= ()sortinter(append(UQ0,UQ1))
			where PQ2s 	:= 
			()sortinter(append(PQ0,1-th(esimpg).nil))
			where res	:= 
			()completion(UQ2s,PQ2s,G1,newcounter3)
		end
	end
	end

end


end