module eqconstrained[vars,fss,prec]

/* Extension of the sort equation to a constrained equation */
/* In Basic Completion, an equation is extended such that it is */
/* formed of an equation, a constraint and a counter */

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


import	
	global
		constraint[vars,fss,prec]
	;
	local
		vars
		fss
		prec		
		int
		set[variable]
		list[variable]
		list[int]
		lvariables[vars,fss,prec]
		termCommons[fss,vars] /* defined the sort term so variable */
		eqSystem[fss,vars] /* defined the sort eqSystem so equation */
		renaming[vars,fss,prec]
		syntacticUnification[fss,vars]
		applySubstOn[fss,vars,equation]
		applySubstOn[fss,vars,constraint]
		applySubstOn[fss,vars,term]
		applySubstOn[fss,vars,eqconstrained] 
		occur[variable,equation]
                occur[variable,contrainte]
		position[vars,fss,prec]
		;
end

sort 
	eqconstrained;
end

operators
  global
	/* Constructor of the sort eqconstrained */
	@[@]<@>		: (equation constraint int) eqconstrained;

	/* Destructors of an eqconstrained */
    	equation(@)	: (eqconstrained) equation;
	constraint(@)	: (eqconstrained) constraint;
	counter(@)	: (eqconstrained) int;

	/* Test the equality of two objects of type eqconstrained */
	meqeqconstrained(@,@) : (eqconstrained eqconstrained) bool;

	/* Transform a constraint equation to an unconstrained equation */
	propagate(@)	: (eqconstrained) eqconstrained;

	/* List of variables of a constrained equation (with duplication) */
	list_variables1(@)	: (eqconstrained) list[variable];

	/* List of variables of a constrained equation (without duplication) */
	list_variables(@)	: (eqconstrained) list[variable];

	/* Set of variables of a constrained eqaution */
	set_variables(@)	: (eqconstrained) set[variable];

	/* Give the number i of the variable writtem by var(i) such */
	/* that i is maximum in the constrained equation */
	/* or the integer n (second argument) if n > i */
	maxvar(@,@)	: (eqconstrained int) int;

	/* Normalization of a constrained equation by a substitution */
	/* A variable is replaced by another variable in all the term */
	/* The terms do not need to be written using var(i) */
	/* For a term, rename( f(x,y) , x->y o y->x ) ==> f(x,x) */
	/* but normalize( f(x,y) , x->y o y->x ) ==> f(y,x) */
	normalize(@,@)	: (eqconstrained substitution) eqconstrained;

	/* Renaming of a constrained equation starting from var(i) */
	/* even if it is not expressed using var(j) */
	/* The resulted constrained equation is only written using */
	/* var(i) */
	/* For a term, normalize(f(g(x),y),3) => f(g(var(4)),var(3))*/
	normalize(@,@)	: (eqconstrained int) eqconstrained;

	/* Renaming of the constrained equation from var(0) */
	/* For a term, normalize(f(g(x),y))=x => */
	/* f(g(var(1)),var(0))=var(1) */
	normalize(@)	: (eqconstrained) eqconstrained;

	/* Renaming of the constrained equation from var(i) when i = n+1 */
	/* For a term, translate(f(g(var(1)),var(0))=var(1),3) => */
	/* f(g(var(5)),var(4))=var(5) */
	translate(@,@)	: (eqconstrained int) eqconstrained;

	/* Renaming of the constrained equation  containing var(0)... */
	/* var(n) from var(n+1)*/
	/* translate(f(g(var(1)),var(0)) => */
	/* f(g(var(3)),var(2)) */
	translate(@)	: (eqconstrained) eqconstrained;

	/* Size of an eqconstrained w.r.t the size of the equation and */
	/* the size of the constraint */
	size(@)		: (eqconstrained) int;

	/* Computation of the minimal match */

	min_match(@,@,@,@,@,@,@,@): (term constraint substitution term
			constraint substitution list[int]
			substitution) substitution;

	min_match_compute(@,@,@,@,@,@,@,@,@): 
			(term substitution term constraint substitution 
			list[variable] list[int] substitution eqSystem) 
			eqSystem;
end


stratop
global
    propagate		: <eqconstrained>               builtin;

    delete_variables	: <eqconstrained>               builtin;
end


/* Regles de simplification */

rules for eqconstrained
	eq	: equation;
	c	: constraint;
	v1,v2	: variable;
	t	: term;
	counter	: int;
	var_t	: list[variable];
global
	/* v1 not in eq */
	[var_elim] eq[c & v1=?t]<counter> => 
				eq[apply(v1->t,c)]<counter>
				if not(occurs(v1,eq))
	end

	/* v1 in eq and v2 not in eq */
	[var_elim] eq[c & v1=?v2]<counter> => 
				eq[apply(v2->v1,c)]<counter>
				if not(occurs(v2,eq))
	end

	/* v1 in eq */
/*	[var_elim] eq[c & v1=?t]<counter> => 
				apply(v1->t,eq[c]<counter>)
				if not isvar(t)
				where var_t:= ()list_variables(t)
				where v2 := (listExtract)elem(var_t)
				if not occurs v2 in eq
	end
*/

	/* v1 in eq and v2 in eq and v1 is not in c and v2 is in c */
	[var_elim] eq[c & v1=?v2]<counter> => 
				apply(v1->v2,eq[c]<counter>)
	end

	[trueadd_ve] eq[c]<counter> => eq[c & true]<counter>
	end
	
	[trueelim_ve] eq[c & true]<counter> => eq[c]<counter>
	end
end


/* equation */

rules for equation
	eq	: equation;
	C	: constraint;
	counter	: int;
global
	[] equation(eq[C]<counter>)	=> eq
	end
end

/* constraint */

rules for constraint
	eq	: equation;
	C	: constraint;
	counter	: int;
global
	[] constraint(eq[C]<counter>)	=> C
	end
end

/* counter */

rules for int
	eq	: equation;
	C	: constraint;
	counter	: int;
global
	[] counter(eq[C]<counter>)	=> counter
	end
end


/* meqeqconstrained */

rules for bool
	eq1, eq2		: equation;
	C1, C2			: constraint;
	counter1, counter2	: int;
global
	[] meqeqconstrained(eq1[C1]<counter1>,eq2[C2]<counter1>)=> true
	end

	[] meqeqconstrained(eq1[C1]<counter1>,eq2[C2]<counter2>)=> false
	end
end



/* propagate */

rules for eqconstrained
	eq	: equation;
	C	: constraint;
	sigma	: substitution;
	counter	: int;
global
	[propage] propagate(eq[C]<counter>) => 
		sigma(eq)[true]<counter>
		where sigma:= ()constraint_to_subst(C)
	end
end


/* list_variables1 */

rules for list[variable]
	eq	: equation;
	C 	: constraint;
	counter	: int;
global
	[] list_variables1(eq[C]<counter>) => 
		list_variables1(eq) @@ list_variables1(C)
	end
end


/* list_variables */

rules for list[variable]
	eq	: eqconstrained;
global
	[] list_variables(eq) => simple_list(list_variables1(eq))
	end
end


/* set_variables */

rules for set[variable]
	eq 	: equation;
	C 	: constraint;
	counter	: int;
global
	[] set_variables(eq[C]<counter>) => 
		set_variables(eq) u set_variables(C)
	end
end


/* maxvar */

rules for int
	eq	 	: equation;
	C		: constraint;
	counter, n	: int;
global
	[] maxvar(eq[C]<counter>,n)	=> maxvar(eq,maxvar(C,n))
	end
end


/* normalize w.r.t substitution */

rules for eqconstrained
	eq 	: equation;
	C	: constraint;
	counter	: int;
	sigma	: substitution;
global
	[] normalize(eq[C]<counter>,sigma)	=> 
		normalize(eq,sigma)[normalize(C,sigma)]<counter>
	end
end


/* normalize w.r.t int */

rules for eqconstrained
	eqc 	: eqconstrained;
	n 	: int;
	sigma	: substitution;
	lv	: list[variable];
global
	[] normalize(eqc,n)			=> 
		normalize(eqc,sigma)
		where lv	:= ()list_variables(eqc)
		where sigma 	:= ()rename_subst(lv,n)
	end
end


/* normalize - main */

rules for eqconstrained
	eqc 	: eqconstrained;
global
	[] normalize(eqc)	=> normalize(eqc,0)
	end
end


/* translate w.r.t int */

rules for eqconstrained
	eqc 	: eqconstrained;
	n	: int;
	sigma	: substitution;
global
	[] translate(eqc,n)	=> normalize(eqc,sigma)
		where sigma := ()rename_subst(maxvar(eqc,0),n+1)
	end
end


/* translate - main */

rules for eqconstrained
	eqc 	: eqconstrained;
	n	: int;
	sigma	: substitution;
global
	[] translate(eqc)	=> normalize(eqc,sigma)
				where n:= ()maxvar(eqc,0)
				where sigma := ()rename_subst(n,n+1)
	end
end


/* size */

rules for int
	eq, eqnonc 	: equation;
	C		: constraint;
	counter		: int;
	sigma		: substitution;
global
	[] size(eq[C]<counter>)		=> 
//		size(eq)+size(C)
		size(eqnonc)
		where sigma	:= ()constraint_to_subst(C)
		where eqnonc	:= ()sigma(eq)
	end
end


/* min_match_compute */

rules for eqSystem
	g,l			: term;
	c1			: constraint;
	sigma1, match, sigma2	: substitution;
	newmatch, newminmatch, newminmatch1 	: eqSystem;
	omega			: list[int];
	var			: variable;
	list_var		: list[variable];
	listposvar		: list[list[int]];
	all_subst_pos		: bool;
global
	[] min_match_compute(l,sigma2,g,c1,sigma1,nil,omega,match,newmatch)
	=>
	newmatch
	end

	[] min_match_compute(l,sigma2,g,c1,sigma1,var.list_var,omega,match,
	newmatch)
	=>
	newminmatch
//	where listposvar	:= ()listpos2(g at omega,var)
	where listposvar	:= ()listpos2(sigma2(l),var)
	where all_subst_pos	:= ()all_subst_pos(g at omega,listposvar,sigma1)
	choose
	try
		if all_subst_pos
		where newminmatch := 
		()min_match_compute(l,sigma2,g,c1,sigma1,list_var,omega,match,newmatch)
		
	try
		if not all_subst_pos
		where newminmatch1 := ()newmatch 
		& var = 
		generalization(1-th elem(list_terms_wrt_pos(g at omega,listposvar)),
		tail(list_terms_wrt_pos(g at omega,listposvar)))
		where newminmatch	:= 
		()min_match_compute(l,sigma2,g,c1,sigma1,list_var,omega,
		match,newminmatch1)
	end
	end	
end


rules for substitution
	g, l				: term;
	c1, c2				: constraint;
	sigma1, sigma2, match, newmatch	: substitution;
	omega				: list[int];
	eqsys, neweqsys			: eqSystem;
	list_var			: list[variable];
global
	[] min_match(g,c1,sigma1,l,c2,sigma2,omega,match)
	=>
	newmatch
	where list_var	:= ()list_variables(sigma2(l))
	where eqsys	:= 
	()min_match_compute(l,sigma2,g,c1,sigma1,list_var,omega,match,
	true)
	where neweqsys	:= (unifys)eqsys
	where newmatch	:= ()system_to_subst(neweqsys)
	end
end


/* strategies */

strategies for eqconstrained
implicit
	[.] propagate	=> first one(propage)
	end

	[.] delete_variables =>
		first one(trueadd_ve);
		repeat*(first one(var_elim));
		repeat*(first one(trueelim_ve))
	end
end


end