Automatic principal arguments in eqchk

[anjapetkovic]

Principal (normalizing) arguments of constructors are determined automatically, when computational rules are installed. But if more than one rule in installed for some constructor S, only the principal arguments from the last rule are normalized, so previous rules may not even apply?

Here is an example, that illustrates the problem:

require eq ;;

rule A type ;;
rule S (X type) (Y type) type ;;
rule H (X type) type ;;
rule H1 (X type) type ;;

rule H1_eq_H (X type) : H1 X ≡ H X ;;
eq.add_rule H1_eq_H ;;

rule S_eq1 (X type) (Y type) : (S Y (H X)) ≡ Y ;;

rule S_eq2 (X type) (Y type) : (S (H X) Y) ≡ Y ;;

eq.add_rule S_eq1 ;;

eq.normalize (S (H A) A) ;;
eq.normalize (S A (H A)) ;;

eq.normalize (S (H1 A) A) ;;
eq.normalize (S A (H1 A)) ;;

eq.add_rule S_eq2 ;;

eq.normalize (S (H A) A) ;;
eq.normalize (S A (H A)) ;;
(* Both get normalized to A *)

eq.normalize (S (H1 A) A) ;;
eq.normalize (S A (H1 A)) ;;
(* The last one does not get normalized to A,
   because S_eq2 does not declare the second
   argument to be principal argument *)