-------------------------------------------------------------------------------
---- file: crchc2b.maude
---- author: Francisco Durán
---- last modified by Francisco Durán on Nov 6th, 2006
-------------------------------------------------------------------------------

set show loop stats off .
set show loop timing off .
set show advisories off .

fmod CRCHC-BANNER is 
  pr STRING .
  op crchc-banner : -> String .
  eq crchc-banner = "Church-Rosser and Coherence Checker 2b (November 6th, 2006)" .
endfm

---- ChC: Equational conditions may possibly be discharged. Currently they are left 
---- unreduced.

**** The module EXT-TERM extends META-LEVEL with definitions of several 
**** operations that manipulate terms: definitions for positions and operations
**** to get the subterm of a given term at a given position, to replace the
**** subterm of a term at a given position by another term, to get all the
**** nonvariable positions in a term, to apply a substitution to a term, and to
**** get a copy of a term in which all the variables in it have been renamed.

fmod EXT-TERM is
  pr META-LEVEL .
  pr EXT-BOOL .
  pr EXT-DECL .

  sorts Position PositionSet .
  subsorts Nat < Position < PositionSet .

  op emptyPos : -> Position .
  op pos : Position Position -> Position [assoc] .
  op nullPos : -> Position .

  op emptyPosSet : -> PositionSet .
  op posSet : PositionSet PositionSet -> PositionSet 
       [assoc comm id: emptyPosSet] .

  var  G : Bool .
  var  P : Position .
  var  PS : PositionSet .
  vars T T' : Term .
  vars F X : Qid .
  var  TL : TermList .
  var  N : Nat .
  vars NL NL' : NatList .
  vars V V' W : Variable .
  var  Subst : Substitution .
  vars C Ct : Constant .
  var  NTL : NeTermList .
  var  M : Module .
  var  Tp : Type .
  vars TpL TpL' : TypeList .
  vars AtS AtS' : AttrSet .
  var  OPDS : OpDeclSet .

  eq pos(emptyPos, P) = P .

  **** vars returns the set of variables in a term
  op vars : Term -> QidSet .
  op vars : TermList -> QidSet .

  eq vars(V) = V .
  eq vars(C) = none .
  eq vars(F[TL]) = vars(TL) .
  eq vars(empty) = none .
  eq vars((T, TL)) = vars(T) ; vars(TL) .

  **** occurs? checks whether a variable name occurs in a term or not.
  op occurs? : Variable Term -> Bool .
  op occurs? : Variable TermList -> Bool .
  eq occurs?(V, V') = V == V' .
  eq occurs?(V, C) = false .
  eq occurs?(V, F[TL]) = occurs?(V, TL) .
  eq occurs?(V, (T, TL)) = occurs?(V, T) or-else  occurs?(V, TL) .

**** The partial function \texttt{getSubterm} takes a term $t$ and a position 
**** $p$ and returns $t|_{p}$ if $p\in \mathcal{P}(t)$.

  op getSubterm : Term Position -> [Term] .
  op getSubterm1 : TermList Nat -> [Term] .

  eq getSubterm(T, emptyPos) = T .
  eq getSubterm(F[TL], N) = getSubterm1(TL, N) .
  eq getSubterm(F[TL], pos(N, P)) = getSubterm(getSubterm1(TL, N), P) .
  
  eq getSubterm1((T, TL), N)
    = if N == 1 
      then T 
      else getSubterm1(TL, sd(N, 1)) 
      fi .

**** The partial function \texttt{replace} takes terms $t$ and $t'$ and a 
**** position $p$ as input and returns the term $t[t']_{p}$ if 
**** $p\in \mathcal{P}(t)$.

  op replace : Term Term Position -> [Term] .
  op replace1 : TermList Term Position -> [TermList] .
  
  eq replace(T, T', emptyPos) = T' .
  eq replace(F[TL], T', N) = F[replace1(TL, T', N)] .
  eq replace(F[TL], T', pos(N, P)) = F[replace1(TL, T', pos(N, P))] .   
  
  eq replace1((T, TL), T', N) 
    = if N == 1 
      then (T', TL) 
      else (T, replace1(TL, T', sd(N, 1))) 
      fi .
  eq replace1((T, TL), T', pos(N, P))
    = if N == 1 
      then (replace(T, T', P), TL)
      else (T, replace1(TL, T', pos(sd(N, 1), P))) 
      fi .

**** The function \texttt{allNonVarPos} takes a term $t$ and
**** returns the set $\mathcal{P}(t)$ of all nonvariable positions of $t$.

  op allNonVarPos : Term -> PositionSet [memo] .
  op allNonVarPos : Term Position PositionSet -> PositionSet .
  op nextNonVarPos : Term Position -> Position .
  op nextNonVarPosUp : Term Position -> Position .

----  eq allNonVarPos(T)
----    = posSet(emptyPos, allNonVarPos(T, emptyPos, emptyPosSet)) .
----
----  eq allNonVarPos(T, P, PS)
----    = if nextPos(T, P) == nullPos 
----      then PS
----      else if getSubterm(T, nextPos(T, P)) :: Variable
----           then allNonVarPos(T, nextPos(T, P), PS)
----           else allNonVarPos(T, nextPos(T, P), posSet(nextPos(T, P), PS))
----           fi
----      fi .
----
----  eq nextPos(T, P)
----    = if getSubterm(T, pos(P, 1)) :: Term
----      then pos(P, 1) 
----      else nextPosUp(T, P)
----      fi .
----
----  eq nextPosUp(T, emptyPos) = nullPos .
----  eq nextPosUp(T, N) 
----    = if getSubterm(T, (N + 1)) :: Term
----      then (N + 1) 
----      else nullPos
----      fi .
----  eq nextPosUp(T, pos(P, N))
----    = if getSubterm(T, pos(P, (N + 1))) :: Term
----      then pos(P, (N + 1))  
----      else nextPosUp(T, P)
----      fi .

  eq allNonVarPos(T)
    = posSet(emptyPos, allNonVarPos(T, emptyPos, emptyPosSet)) .

  eq allNonVarPos(T, P, PS)
    = if nextNonVarPos(T, P) == nullPos 
      then PS
      else allNonVarPos(T, nextNonVarPos(T, P), posSet(nextNonVarPos(T, P), PS))
      fi .

  eq nextNonVarPos(T, P)
    = if getSubterm(T, pos(P, 1)) :: Term
         and-then not getSubterm(T, pos(P, 1)) :: Variable
      then pos(P, 1) 
      else nextNonVarPosUp(T, P)
      fi .

  eq nextNonVarPosUp(T, emptyPos) = nullPos .
  eq nextNonVarPosUp(T, N) 
    = if getSubterm(T, (N + 1)) :: Term
         and-then not getSubterm(T, (N + 1)) :: Variable
      then (N + 1) 
      else nullPos
      fi .
  eq nextNonVarPosUp(T, pos(P, N))
    = if getSubterm(T, pos(P, (N + 1))) :: Term
         and-then not getSubterm(T, pos(P, (N + 1))) :: Variable
      then pos(P, (N + 1))  
      else nextNonVarPosUp(T, P)
      fi .

**** The function \texttt{allNonVarNonFrozenPos} takes a term $t$ and
**** returns the set $\mathcal{P}(t)$ of all nonvariable and nonfrozen
**** positions of $t$.

  op allNonVarNonFrozenPos : Module Term Bool -> PositionSet [memo] .
  op allNonVarNonFrozenPos : Module Term Position PositionSet Bool -> PositionSet .
  op nextNonVarNonFrozenPos : Module Term Position Bool -> Position .
  op nextNonVarNonFrozenPosUp : Module Term Position Bool -> Position .

  eq allNonVarNonFrozenPos(M, T, G)
    = posSet(emptyPos, allNonVarNonFrozenPos(M, T, emptyPos, emptyPosSet, G)) .

  eq allNonVarNonFrozenPos(M, T, P, PS, G)
    = if nextNonVarNonFrozenPos(M, T, P, G) == nullPos 
      then PS
      else allNonVarNonFrozenPos(M, T, nextNonVarNonFrozenPos(M, T, P, G), 
             posSet(nextNonVarNonFrozenPos(M, T, P, G), PS), G)
      fi .

  eq nextNonVarNonFrozenPos(M, T, P, G)
    = if getSubterm(T, pos(P, 1)) :: Term
         and-then not getSubterm(T, pos(P, 1)) :: Variable
         and-then not frozen(M, getSubterm(T, P), 1, G)
      then pos(P, 1) 
      else nextNonVarNonFrozenPosUp(M, T, P, G)
      fi .

  eq nextNonVarNonFrozenPosUp(M, T, emptyPos, G) = nullPos .
  eq nextNonVarNonFrozenPosUp(M, T, N, G) 
    = if getSubterm(T, (N + 1)) :: Term
         and-then not getSubterm(T, (N + 1)) :: Variable
         and-then not frozen(M, T, N + 1, G)
      then (N + 1) 
      else nullPos
      fi .
  eq nextNonVarNonFrozenPosUp(M, T, pos(P, N), G)
    = if getSubterm(T, pos(P, (N + 1))) :: Term
         and-then not getSubterm(T, pos(P, (N + 1))) :: Variable
         and-then not frozen(M, getSubterm(T, P), N + 1, G)
      then pos(P, (N + 1))  
      else nextNonVarNonFrozenPosUp(M, T, P, G)
      fi .
      
  op frozen : Module Term Nat Bool -> Bool .
  op frozen : Module OpDeclSet Qid TypeList Nat Bool -> Bool .
  
  eq frozen(M, F[TL], N, G) 
    = frozen(M, getOps(M), F, leastSort(M, TL), N, G) .
    
  ceq frozen(M, op F : TpL -> Tp [AtS] . OPDS, F, TpL', N, true)
    ---- for ground confluence we assume all non-ctor operators are frozen
    = true
    if sameKind(M, TpL, TpL') 
       /\ not ctor(M, op F : TpL -> Tp [AtS] . OPDS, F, TpL') .
  ceq frozen(M, op F : TpL -> Tp [AtS] . OPDS, F, TpL', N, G)
    = true
    if sameKind(M, TpL, TpL') 
       /\ frozen(NL N NL') AtS' := AtS .
  eq frozen(M, OPDS, F, TpL, N, G) = false [owise] .

  ---- ctor check whether the operator at the top is a constructor
  ---- in any of its overloadings 
  op ctor : Module OpDeclSet Term -> Bool .
  op ctor : Module OpDeclSet Qid TypeList -> Bool .

  eq ctor(M, OPDS, Ct) = ctor(M, OPDS, Ct, nil) .
  eq ctor(M, OPDS, F[TL]) = ctor(M, OPDS, F, leastSort(M, TL)) .
  eq ctor(M, OPDS, T) = false [owise] .

  ceq ctor(M, op F : TpL -> Tp [AtS] . OPDS, F, TpL')
    = ctor in AtS or-else ctor(M, OPDS, F, TpL') 
    if sameKind(M, TpL, TpL') .
  eq ctor(M, OPDS, F, TpL) = false [owise] .

**** The function \texttt{substitute} takes a term $t$ and a substitution 
**** $\sigma$ and returns the term $t\sigma$. 

  op substitute : Term Substitution -> Term .
  op substitute : TermList Substitution -> TermList .

  eq substitute(T, none) = T .
  eq substitute(V, ((W <- T) ; Subst)) 
    **** WE MAY HAVE TO CHECK SOMETHING LIKE
    ****      getName(V) == getName(W) and sameKind(V, W)
    = if V == W then T else substitute(V, Subst) fi .
  eq substitute(C, ((W <- T); Subst)) = C .
  eq substitute(F[TL], Subst) = F[substitute(TL, Subst)] .
  eq substitute((T, TL), Subst)
    = (substitute(T, Subst), substitute(TL, Subst)) .

**** Finally, we define the function \texttt{rename}, which takes a term and
**** renames all the variables appearing in it. The renaming is done by 
**** replacing each of the variables in the term by another variable with its 
**** name concatenated with the character \texttt{@}, that is, each variable 
**** $V$ is replaced by $V$\texttt{@}.

  op rename : Term -> Term .
  op rename : TermList -> TermList .

  eq rename(F[TL]) = F[rename(TL)] .
  eq rename((T, NTL)) = (rename(T), rename(NTL)) .
  eq rename(V) = qid(string(getName(V)) + "*:" + string(getType(V))) .
  eq rename(C) = C .

  **** length of term lists
  op length : TermList -> Nat .  
  op lengthAux : TermList Nat -> Nat .  
  eq length(TL) = lengthAux(TL, 0) .
  eq lengthAux((T, TL), N) = lengthAux(TL, s N) .
  eq lengthAux(empty, N) = N .
endfm

***(
red substitute('f['X:Foo, 'g['Y:Foo, 'Z:Foo]], ('Y:Foo <- 'h['W:Foo])) .
red rename('f['X:Foo, 'g['Y:Foo, 'Z:Foo]]) .
red allNonVarPos(
      substitute('f['X:Foo, 'g['Y:Foo, 'Z:Foo]], ('Y:Foo <- 'h['W:Foo]))) .
)

**** We first introduce some basic functions for the manipulation of terms, and 
**** then we present the unification and matching functions.

fmod AUXILIARY-FUNCTIONS is
  pr META-LEVEL .
  pr EXT-BOOL .
  pr EXT-DECL .
  pr EXT-TERM .
  pr INT .

  vars T T' : Term .
  var  TL : TermList .
  vars Tp Tp' Tp'' Tp''' : Type .
  vars TpL TpL' : TypeList .
  var  M : Module .
  var  At : Attr .
  var  AtS : AttrSet .
  vars L F G : Qid .
  var  ODS : OpDeclSet .

  *** some built-in sort operations on lists
  op sortLeq : Module TypeList TypeList ~> Bool [ditto] . 
  eq sortLeq(M, (Tp Tp' TpL), (Tp'' Tp''' TpL')) 
    = sortLeq(M, Tp, Tp'') and-then sortLeq(M, Tp' TpL, Tp''' TpL') .
  eq sortLeq(M, nil, nil) = true .  
  eq sortLeq(M, TpL, TpL') = false [owise] .
  
  op sameKind : Module TypeList TypeList ~> Bool [ditto] . 
  eq sameKind(M, (Tp Tp' TpL), (Tp'' Tp''' TpL')) 
    = sameKind(M, Tp, Tp'') and-then sameKind(M, Tp' TpL, Tp''' TpL') .
  eq sameKind(M, nil, nil) = true .  
  eq sameKind(M, TpL, TpL') = false [owise] .

  op leastSort : Module TermList ~> TypeList [ditto] .
  eq leastSort(M, (T, T', TL)) = leastSort(M, T) leastSort(M, (T', TL)) .
  eq leastSort(M, empty) = nil .
  
  op getLabel : AttrSet -> Qid .
  eq getLabel(label(L) AtS) = L .
  eq getLabel(AtS) = 'no-label [owise] .

  **** hasAttr checks whether the given operator has the given attribute
  **** in its declaration in the given module

  op hasAttr : Module Qid TypeList Attr -> Bool .
  op hasAttr : Module OpDeclSet Qid TypeList Attr -> Bool .

  eq hasAttr(M, G, TpL, At) = hasAttr(M, getOps(M), G, TpL, At) .
  eq hasAttr(M, op F : TpL -> Tp [AtS] . ODS, G, TpL', At) 
    = if (F == G) and-then sameKind(M, TpL, TpL')
      then At in AtS
      else hasAttr(M, ODS, G, TpL', At)
      fi .
  eq hasAttr(M, none, G, TpL, At) = false .

endfm

*** We get the variables from the terms, but we don't use them for getting
*** their sorts. Variables are already of the form X:S, and we get their
*** sorts from them.
*** Variables are collected to be able to complete the substitutions at the
*** end of the process. 
*** We use V to refer to variables and X to refer to variable names. 

fmod UNIFICATION is
  pr META-LEVEL .
  pr EXT-BOOL .
  pr AUXILIARY-FUNCTIONS .

  vars QI F G X Y : Qid .
  vars S S' : Sort .
  vars Tp Tp' : Type .
  vars TpL TpL' : TypeList .
  var  TpS : TypeSet .
  vars TpLS TpLS' : TypeListSet .
  var  M : Module .
  vars T T' T'' T''' T1 T1' : Term .
  vars TL TL' : TermList .
  var  CEqS : CommEqSet .
  var  D : Disjunction .
  var  UT : UnifTuple .
  var  VDS : VarDeclSet .
  vars Subst Subst' : Substitution .
  var  SubstS : SubstitutionSet .
  var  MAS : MembAxSet .
  vars N I : Nat .
  var  AtS : AttrSet .
  var  IL : ImportList .
  var  SS : SortSet .
  var  SSDS : SubsortDeclSet .
  var  ODS : OpDeclSet .
  var  EqS : EquationSet .
  var  RlS : RuleSet .
  vars V W : Variable .
  vars C C' : Constant .
  var  EqC : EqCondition .
  var  Cd : Condition .

  **** a few declarations for manipulating variables.

  sorts VarDecl VarDeclSet .
  subsort VarDecl < VarDeclSet .

  op var_:_. : Variable Type -> VarDecl .
  op none : -> VarDeclSet .
  op __ : VarDeclSet VarDeclSet -> VarDeclSet [assoc comm id: none] .
  eq VD:VarDecl VD:VarDecl = VD:VarDecl .

  **** varDecls returns the set of variables in a term

  op varDecls : Term -> VarDeclSet [memo] .
  op varDecls : TermList -> VarDeclSet [memo] .

  eq varDecls(V) = (var V : getType(V) .) .
  eq varDecls(C) = none .
  eq varDecls(F[TL]) = varDecls(TL) .
  eq varDecls(empty) = none .
  eq varDecls((T, T', TL)) = varDecls(T) varDecls((T', TL)) .

  *** The solution of a unification problem will be given as a set of
  *** substitutions.

  sort SubstitutionSet .
  subsort Substitution < SubstitutionSet .
  op emptySubstitutionSet : -> SubstitutionSet .
  op substitutionSet : SubstitutionSet SubstitutionSet -> SubstitutionSet 
          [assoc comm id: emptySubstitutionSet] .

  *** unification tuples and disjunction of unification tuples

  sorts UnifPair UnifTuple Disjunction .
  subsort UnifTuple < Disjunction .

  op failure : -> Disjunction .
  op _\/_ : Disjunction Disjunction -> Disjunction [assoc comm id: failure] .
  op unifPair : Module Disjunction -> UnifPair .

  op <_;_;_> : VarDeclSet CommEqSet Substitution -> UnifTuple .
  op [_;_;_;_] : VarDeclSet MembAxSet Substitution Substitution -> UnifTuple .

  **** (commutative) equations

  sorts CommEq CommEqSet .
  subsort CommEq < CommEqSet .
  op _=?_ : Term Term -> CommEq [comm] .
  op none : -> CommEqSet .
  op __ : CommEqSet CommEqSet -> CommEqSet [assoc comm id: none] .

  **** tuple disjunction for the solving (x : s) rule

  op unifTuplesVar : Module Variable Type Type UnifTuple -> Disjunction .
  op unifTuplesVarAux : TypeSet Qid UnifTuple -> Disjunction .
  eq unifTuplesVar(M, V, Tp, Tp', UT)
    = unifTuplesVarAux(glbSorts(M, Tp, Tp'), V, UT) .

  eq unifTuplesVarAux((Tp ; TpS), V, [VDS ; MAS ; Subst ; Subst'])
    = ([var V : Tp . VDS ; MAS ; Subst ; Subst']
       \/
       unifTuplesVarAux(TpS, V, [VDS ; MAS ; Subst ; Subst'])) .
  eq unifTuplesVarAux(none, V, UT) = failure .

  **** tuple disjunction for the solving (f(t1,...,tn) : s) rule

  op unifTuplesNonVar : Module MembAx UnifTuple -> Disjunction .
  op unifTuplesNonVarAux : TypeListSet TermList UnifTuple -> Disjunction .
  op unifTuplesNonVarAux2 : TypeList TermList UnifTuple -> UnifTuple .

  eq unifTuplesNonVar(M, (mb F[TL] : S [AtS].), UT)
    = unifTuplesNonVarAux(maximalAritySet(M, F, leastSort(M, TL), S), TL, UT) .

  eq unifTuplesNonVarAux(TpL ; TpLS, TL, UT)
    = (unifTuplesNonVarAux2(TpL, TL, UT)
       \/
       unifTuplesNonVarAux(TpLS, TL, UT)) .
  eq unifTuplesNonVarAux(none, TL, UT) = failure .

  eq unifTuplesNonVarAux2((Tp TpL), (T, TL), [VDS ; MAS ; Subst ; Subst'])
    = unifTuplesNonVarAux2(TpL, TL,
        [VDS ; mb T : Tp [none] . MAS ; Subst ; Subst']) .
  eq unifTuplesNonVarAux2(nil, empty, UT) = UT .

  op commUnifTupleSet : VarDeclSet Qid TermList TermList CommEqSet Substitution 
       -> Disjunction .
  op substMembAxSet : Module VarDeclSet -> Substitution .

  op size : Module TermList -> Int .
  op greaterCommEq : Module CommEq CommEq -> Bool .

  op unify : Module Term Term -> SubstitutionSet .

  op commEqBreak : TermList TermList -> CommEqSet .  
  op substituteCommEqs : CommEqSet Substitution -> CommEqSet .
  op substituteEqs : EquationSet Substitution -> EquationSet .
  op substituteSubstitution : Substitution Substitution  -> Substitution .
  op getUnifSolution : UnifPair -> SubstitutionSet .

  eq unify(M, T, T') 
    = getUnifSolution(
        unifPair(M, < varDecls(T) varDecls(T') ; (T =? T') ; none >)) .

*** deletion of trivial equation

  eq unifPair(M, (< VDS ; (T =? T) CEqS ; Subst > \/ D))
    = unifPair(M, (< VDS ; CEqS ; Subst > \/ D)) .

*** decomposition
*** all subsort overloaded symbols have the same attributes

  eq unifPair(M, (< VDS ; (F[TL] =? G[TL']) CEqS ; Subst > \/ D))
    = if (F =/= G) 
         or-else (length(TL) =/= length(TL'))
         ----or-else not sameKind(M, leastSort(M, TL), leastSort(M, TL'))
      then unifPair(M, D)
      else if (length(TL) == 2) and-then hasAttr(M, F, leastSort(M, TL), comm)
           then unifPair(M, 
                  (commUnifTupleSet(VDS, F, TL, TL', CEqS, Subst) \/ D))
           else unifPair(M, 
                  (< VDS ; commEqBreak(TL, TL') CEqS ; Subst > \/ D))
           fi
      fi .

  eq commUnifTupleSet(VDS, F, (T, T'), (T'', T'''), CEqS, Subst)
    = (< VDS ; (T =? T'') (T' =? T''') CEqS ; Subst >
       \/
       < VDS ; (T =? T''') (T' =? T'') CEqS ; Subst >) .
         
*** clash of symbols

  ceq unifPair(M, (< VDS ; (C =? C') CEqS ; Subst > \/ D))
    = unifPair(M, D)
    if C =/= C' .
  **** WE MAY NEED TO CONSIDER
  ****    getName(C) = getName(C') /\ sameKind(getSort(C), getSort(C')
  eq unifPair(M, (< VDS ; (C =? F[TL]) CEqS ; Subst > \/ D))
    = unifPair(M, D) .

*** merging

  ceq unifPair(M, (< VDS ; (V =? T) (V =? T') CEqS ; Subst > \/ D))
    = unifPair(M, (< VDS ; (V =? T) (T =? T') CEqS ; Subst > \/ D))
    if greaterCommEq(M, (V =? T'), (T =? T')) .

*** check / eliminate

  ceq unifPair(M, (< VDS ; (V =? T) CEqS ; Subst > \/ D))
    = if occurs?(V, T)
      then unifPair(M, D)
      else if glbSorts(M, leastSort(M, T), getType(V)) == none
           then unifPair(M, D)
           else unifPair(M, 
                  (< VDS ; 
                     substituteCommEqs(CEqS, V <- T) ;
                     (substituteSubstitution(Subst, V <- T) ; 
                      V <- T) > \/ D))
           fi
      fi
    if V =/= T .

*** order-sorted checking

*** transition 

  eq unifPair(M, (< VDS ; none ; Subst > \/ D))
    = unifPair(M, ([VDS ; none ; Subst ; Subst] \/ D)) .
  
*** solving (V <- T)

  eq unifPair(M, 
       ([var V : S . VDS ; MAS ; (V <- T ; Subst) ; Subst'] \/ D))
    = unifPair(M, 
        ([VDS ; mb T : S [none] . MAS ; Subst ; Subst'] \/ D)) .

*** solving (X : S) 

  eq unifPair(M, [var V : S . VDS ; mb V : S' [none] . MAS ; none ; Subst] \/ D)
    = unifPair(M, unifTuplesVar(M, V, S, S', [VDS ; MAS ; none ; Subst]) \/ D) .

*** solving (f(t1, ..., tn) : S)

  eq unifPair(M, [VDS ; mb C : S [none] . MAS ; none ; Subst] \/ D)
    = if sortLeq(M, getType(C), S)
      then unifPair(M, [VDS ; MAS ; none ; Subst] \/ D)
      else unifPair(M, D)
      fi .
  eq unifPair(M, [VDS ; mb F[TL] : S [AtS] . MAS ; none ; Subst] \/ D)
    = unifPair(M, 
        unifTuplesNonVar(M, (mb F[TL] : S [AtS] .), [VDS ; MAS ; none ; Subst]) 
        \/ D) .

*** unification auxiliary functions

  eq getUnifSolution(unifPair(M, [VDS ; none ; none ; Subst] \/ D))
    = substitutionSet(
        (substituteSubstitution(Subst, substMembAxSet(M, VDS)) ; 
         substMembAxSet(M, VDS)), 
        getUnifSolution(unifPair(M, D))) .
  eq getUnifSolution(unifPair(M, failure)) = emptySubstitutionSet .

  eq substMembAxSet(M, (var V : S . VDS))
    = ((V <- qid(string(getName(V)) + "@:" + string(S))) ; 
       substMembAxSet(M, VDS)) .
  eq substMembAxSet(M, none) = none .

  eq commEqBreak(T, T') = (T =? T') .
  eq commEqBreak((T, TL), (T', TL')) = ((T =? T') commEqBreak(TL, TL')) .
  
  **** well-founded order on equations

  eq greaterCommEq(M, (T =? T'), _=?_(T1, T1'))
    = (max(size(M, T), size(M, T')) > max(size(M, T1), size(M, T1')))
      or-else
      (max(size(M, T), size(M, T')) == max(size(M, T1), size(M, T1')))
       and-then
       _>_(_-_(max(size(M, T), size(M, T')),
               min(size(M, T), size(M, T'))),
           _-_(max(size(M, T1), size(M, T1')),
               min(size(M, T1), size(M, T1')))) .

  eq size(M, V) = 0 .
  eq size(M, C) = 1 .
  eq size(M, F[TL]) = (1 + size(M, TL)) .
  eq size(M, (T, TL)) = (size(M, T) + size(M, TL)) .

  **** substitute for commutative equations and for substitutions

  eq substituteCommEqs(none, Subst) = none .
  eq substituteCommEqs(((T =? T') CEqS), Subst)  
    = ((substitute(T, Subst) =? substitute(T', Subst))
       substituteCommEqs(CEqS, Subst)) .

  eq substituteSubstitution(none, Subst) = none .
  eq substituteSubstitution(((V <- T); Subst'), Subst)  
    = ((V <- substitute(T, Subst));
       substituteSubstitution(Subst', Subst)) .

endfm

fmod MATCHING is
  pr UNIFICATION .

  sorts MatchTuple .
  subsort MatchTuple < Disjunction .

  op match : Module Term Term -> Bool .
  op match : Module EquationSet -> Bool .

  op matchTuple : VarDeclSet EquationSet Substitution -> MatchTuple .
  op eqBreak : TermList TermList -> EquationSet .  
  op greaterEq : Module Equation Equation -> Bool .
  op getMatchSolution : UnifPair -> SubstitutionSet .
  op commMatchTupleSet : VarDeclSet Qid TermList TermList EquationSet 
          Substitution -> Disjunction .

  var  M : Module .
  vars S S' : Sort .
  vars F G X : Qid .
  var  EqS : EquationSet .
  vars T T' T'' T''' T1 T1' : Term .
  vars TL TL' : TermList .
  var  D : Disjunction .
  var  V : Variable .
  var  VDS : VarDeclSet .
  var  Subst : Substitution .
  vars AtS AtS' : AttrSet .
  vars C C' : Constant .
  var  Cd : EqCondition .

  eq match(M, T, T') = match(M, eq T = T' [none] .) . 

  eq match(M, EqS) 
    = getMatchSolution(unifPair(M, matchTuple(varDecls(EqS), EqS, none)))
        =/= emptySubstitutionSet .

*** deletion of trivial equation

  eq unifPair(M, (matchTuple(VDS, ((eq T = T [AtS].) EqS), Subst) \/ D))
    = unifPair(M, (matchTuple(VDS, EqS, Subst) \/ D)) .

*** decomposition
*** all subsort overloaded symbols have the same attributes

  eq unifPair(M, 
       (matchTuple(VDS, ((eq F[TL] = G[TL'] [AtS].) EqS), Subst) \/ D))
    = if (F =/= G) or-else (length(TL) =/= length(TL'))
      then unifPair(M, D)
      else if (length(TL) == 2) and-then hasAttr(M, F, leastSort(M, TL), comm)
           then unifPair(M, 
                  (commMatchTupleSet(VDS, F, TL, TL', EqS, Subst) \/ D))
           else unifPair(M, 
                  (matchTuple(VDS, (eqBreak(TL, TL') EqS), Subst) \/ D))
           fi
      fi .

  eq commMatchTupleSet(VDS, F, (T, T'), (T'', T'''), EqS, Subst)
    = (matchTuple(VDS, eq T = T'' [none] . eq T' = T''' [none] . EqS, Subst)
       \/
       matchTuple(VDS, eq T = T''' [none] . eq T' = T'' [none] . EqS, Subst)) .

*** clash of symbols

  ceq unifPair(M, (matchTuple(VDS, (eq C = C' [AtS] . EqS), Subst) \/ D))
    = unifPair(M, D)
    if C =/= C' .

  eq unifPair(M, (matchTuple(VDS, (eq C = F[TL] [AtS] . EqS), Subst) \/ D))
    = unifPair(M, D) .

  eq unifPair(M, (matchTuple(VDS, (eq F[TL] = C [none] . EqS), Subst) \/ D)) 
    = unifPair(M, D) .

*** merging

  ceq unifPair(M, 
        (matchTuple(VDS, eq V = T [AtS] . eq V = T' [AtS'] . EqS, Subst) \/ D))
    = unifPair(M, 
        (matchTuple(VDS, eq V = T [none] . eq T = T' [none] . EqS, Subst) \/ D))
    if greaterEq(M, eq V = T' [none] ., eq T = T' [none] .) .

*** check / eliminate

  ceq unifPair(M, (matchTuple(VDS, eq V = T [AtS] . EqS, Subst) \/ D))
    = if occurs?(V, T)
      then unifPair(M, D)
      else if sortLeq(M, leastSort(M, T), getType(V)) 
           then unifPair(M, 
                  (matchTuple(VDS, 
                     substituteEqs(EqS, (V <- T)),
                     (substituteSubstitution(Subst, (V <- T)) ; (V <- T)))
                  \/ D))
           else unifPair(M, D)
           fi
      fi
    if V =/= T .

*** matching auxiliary functions

  eq getMatchSolution(unifPair(M, (matchTuple(VDS, none, Subst) \/ D)))
    = substitutionSet(
        (substituteSubstitution(Subst, substMembAxSet(M, VDS)) ;
         substMembAxSet(M, VDS)), 
        getMatchSolution(unifPair(M, D))) .
  eq getMatchSolution(unifPair(M, failure)) = emptySubstitutionSet .

  eq eqBreak(T, T') = (eq T = T' [none].) .
  eq eqBreak((T, TL), (T', TL')) = ((eq T = T' [none].) eqBreak(TL, TL')) .

  eq greaterEq(M, (eq T = T' [none].), (eq T1 = T1' [none].))
    = (max(size(M, T), size(M, T')) > max(size(M, T1), size(M, T1')))
      or-else
      (max(size(M, T), size(M, T')) == max(size(M, T1), size(M, T1')))
       and-then
       _>_(_-_(max(size(M, T), size(M, T')),
               min(size(M, T), size(M, T'))),
           _-_(max(size(M, T1), size(M, T1')),
               min(size(M, T1), size(M, T1')))) .

  eq substituteEqs(((eq T = T' [AtS].) EqS), Subst)  
    = ((eq substitute(T, Subst) = substitute(T', Subst) [AtS].)
       substituteEqs(EqS, Subst)) .
  eq substituteEqs(none, Subst) = none .

  op varDecls : EquationSet -> VarDeclSet .
  op varDecls : EqCondition -> VarDeclSet .

  eq varDecls(eq T = T' [AtS] . EqS) = varDecls(T) varDecls(T') varDecls(EqS) .
  eq varDecls(ceq T = T' if Cd [AtS] . EqS) 
    = varDecls(T) varDecls(T') varDecls(EqS) .
  eq varDecls((none).EquationSet) = none .

  eq varDecls(T = T' /\ Cd) = varDecls(Cd) .
  eq varDecls(T := T' /\ Cd) = varDecls(T) varDecls(Cd) .
  eq varDecls(T : S /\ Cd) = varDecls(T) varDecls(Cd) .
  eq varDecls((nil).EqCondition) = none .

endfm

fmod CRITICAL-PAIR is
  pr MATCHING .
  pr DECL-META-PRETTY-PRINT .

  sort CritPair .
  op cp : Qid Qid Term Term -> CritPair .
  op ccp : Qid Qid Term Term EqCondition -> CritPair .

  sort CritPairSet .
  subsort CritPair < CritPairSet .
  op none : -> CritPairSet .
  op __ : CritPairSet CritPairSet -> CritPairSet [assoc comm id: none] .

  vars T T' T'' T''' T1 T1' T1'' T1''' T2 T2' T2'' T2''' : Term .
  vars L L' L1 L1' L2 L2' QI : Qid .
  var  CP CP' : CritPair .
  vars CPS CPS' : CritPairSet .
  var  M : Module .
  vars Cd Cd1 Cd2 : EqCondition .
  var  S : Sort .
  var  Subst : Substitution .

  eq CP CP = CP .

  op delete : CritPairSet -> CritPairSet .

  eq delete(cp(L, L', T, T') CPS)
    = if T == T'
      then delete(CPS)
      else cp(L, L', T, T') delete(CPS)
      fi .
  eq delete(ccp(L, L', T, T', Cd) CPS)
    = if T == T'
      then delete(CPS)
      else ccp(L, L', T, T', Cd) delete(CPS)
      fi .
  eq delete(none) = none .

  op simplify : CritPairSet Module -> CritPairSet .

  eq simplify(cp(L, L', T, T') CPS, M)
    = cp(L, L', getTerm(metaReduce(M, T)), getTerm(metaReduce(M, T')))
      simplify(CPS, M) .
  eq simplify(ccp(L, L', T, T', Cd) CPS, M)
    = ccp(L, L', getTerm(metaReduce(M, T)), getTerm(metaReduce(M, T')), Cd)
      simplify(CPS, M) .
  eq simplify(none, M) = none .

  op maximalCPSet : CritPairSet Module -> CritPairSet .
  op maximalCPSetAux : CritPair CritPairSet CritPairSet Module -> CritPairSet .
  op moreGeneralCP : CritPair CritPair Module -> Bool .

  eq maximalCPSet(CP CPS, M)
    = maximalCPSetAux(CP, CPS, none, M) .
  eq maximalCPSet(none, M) = none .

  eq maximalCPSetAux(CP, CP' CPS, CPS', M)
    = if moreGeneralCP(CP, CP', M)
      then maximalCPSetAux(CP, CPS, CPS', M)
      else if moreGeneralCP(CP', CP, M)
           then maximalCPSetAux(CP', CPS CPS', none, M)
           else maximalCPSetAux(CP, CPS, CP' CPS', M)
           fi
      fi .
  eq maximalCPSetAux(CP, none, CP' CPS, M)
    = CP maximalCPSetAux(CP', CPS, none, M) .
  eq maximalCPSetAux(CP, none, none, M) = CP .

  eq moreGeneralCP(cp(L1, L1', T1, T1'), cp(L2, L2', T2, T2'), M)
    = match(M, ((eq T1 = T2 [none].) (eq T1' = T2' [none].)))
      or-else
      match(M, ((eq T1 = T2' [none] .) (eq T1' = T2 [none] .))) .
  eq moreGeneralCP(cp(L1, L1', T1, T1'), ccp(L2, L2', T2, T2', Cd2), M)
    = match(M, ((eq T1 = T2 [none].) (eq T1' = T2' [none] .)))
      or-else
      match(M, ((eq T1 = T2' [none] .) (eq T1' = T2 [none] .))) .
  eq moreGeneralCP(ccp(L1, L1', T1, T1', Cd1), cp(L2, L2', T2, T2'), M)
    = false .
  eq moreGeneralCP(ccp(L1, L1', T1, T1', Cd1), 
                   ccp(L2, L2', T2, T2', Cd2), M)
    = match(M, ((eq T1 = T2 [none].) (eq T1' = T2' [none].) mgcpme(Cd1, Cd2)))
      or-else
      match(M, ((eq T1 = T2' [none].) (eq T1' = T2 [none].) mgcpme(Cd1, Cd2))) .

  op mgcpme : EqCondition EqCondition -> EquationSet .
  eq mgcpme(T1 = T1' /\ Cd1, T2 = T2' /\ Cd2) 
    = ((eq T1 = T2 [none] .) (eq T1' = T2' [none] .) mgcpme(Cd1, Cd2)) .
  eq mgcpme(T1 := T1' /\ Cd1, T2 := T2' /\ Cd2) 
    = ((eq T1 = T2 [none] .) (eq T1' = T2' [none] .) mgcpme(Cd1, Cd2)) .
  eq mgcpme(T1 : S /\ Cd1, T2 : S /\ Cd2) 
    = ((eq T1 = T2 [none] .) mgcpme(Cd1, Cd2)) .
  eq mgcpme(nil, nil) = none .
  eq mgcpme(Cd1, Cd2) = (eq 'true.Bool = 'false.Bool [none] .) [owise] .

  op rename : CritPair -> CritPair .
  op rename : EqCondition -> EqCondition .

  eq rename(cp(L, L', T, T')) = cp(L, L', rename(T), rename(T')) .
  eq rename(ccp(L, L', T, T', Cd)) 
    = ccp(L, L', rename(T), rename(T'), rename(Cd)) .

  eq rename(T = T' /\ Cd) = rename(T) = rename(T') /\ rename(Cd) .
  eq rename(T := T' /\ Cd) = rename(T) := rename(T') /\ rename(Cd) .
  eq rename(T : S /\ Cd) = rename(T) : S /\ rename(Cd) .
  eq rename((nil).EqCondition) = nil .

  op substitute : EqCondition Substitution -> EqCondition .
  eq substitute(T = T' /\ Cd, Subst) 
    = substitute(T, Subst) = substitute(T', Subst) /\ substitute(Cd, Subst) .
  eq substitute(T := T' /\ Cd, Subst) 
    = substitute(T, Subst) := substitute(T', Subst) /\ substitute(Cd, Subst) .
  eq substitute(T : S /\ Cd, Subst) 
    = substitute(T, Subst) : S /\ substitute(Cd, Subst) .
  eq substitute((nil).EqCondition, Subst) = nil .

  op eMetaPrettyPrint : Module Qid CritPairSet -> QidList .

  eq eMetaPrettyPrint(M, QI, cp(L, L', T, T') CPS)
    = ('\n '\s '\s '\b 'cp '\o
       (if L =/= 'no-label and L' =/= 'no-label 
        then '\b 'for '\o L '\b 'and '\o L' '\n '\s '\s '\s 
        else nil
        fi)
       '\s metaPrettyPrint(M, T) 
       '\n '\s '\s '\s '\s QI '\o metaPrettyPrint(M, T') '. '\o 
       eMetaPrettyPrint(M, QI, CPS)) .
  eq eMetaPrettyPrint(M, QI, ccp(L, L', T, T', Cd) CPS)
    = ('\n '\s '\s '\b 'ccp '\o
       (if L =/= 'no-label and L' =/= 'no-label 
        then '\b 'for '\o L '\b 'and '\o L' '\n '\s '\s '\s
        else nil
        fi)
       '\s metaPrettyPrint(M, T) 
       '\n '\s '\s '\s '\s '\b QI '\o metaPrettyPrint(M, T') 
       '\n '\s '\s '\s '\s '\b 'if '\o eMetaPrettyPrint(M, Cd) '\b '. '\o 
       eMetaPrettyPrint(M, QI, CPS)) .
  eq eMetaPrettyPrint(M, QI, (none).CritPairSet) = nil .

endfm


fmod 2TUPLE{X :: TRIV, Y :: TRIV} is
  sort Tuple{X, Y} .
  op ((_,_)) : X$Elt Y$Elt -> Tuple{X, Y} .
  op p1_ : Tuple{X, Y} -> X$Elt .
  op p2_ : Tuple{X, Y} -> Y$Elt .
  eq p1((A:X$Elt, B:Y$Elt)) = A:X$Elt .
  eq p2((A:X$Elt, B:Y$Elt)) = B:Y$Elt .
endfm

view CritPairSet from TRIV to CRITICAL-PAIR is
  sort Elt to CritPairSet .
endv

-------------------------------------------------------------------------------
---- confluence check
-------------------------------------------------------------------------------

**** The \texttt{confluenceCheck} function does the confluence check.

**** The unification function may generate new variables, which will be of 
**** the form X@:S for a variable X:S and X@S':S' for a variable X:S with
**** S' each of the subsorts of S. We assume that these variables are not
**** used in the original module. 

**** Since to check the overlappings there cannot be common variables 
**** between the terms, we generate a renamed copy of one of the
**** equations just by renaming each variable using the \texttt{rename} 
**** function presented in~\ref{basic-stuff}.

fmod CONFLUENCE-CHECK is
  pr CRITICAL-PAIR .
  pr 2TUPLE{CritPairSet, CritPairSet} .

  var  M : Module .
  vars T T' T'' T1 T1' T2 T2' T1'' T2'' : Term .
  vars CP CP' : CritPair .
  vars CPS CPS' : CritPairSet .
  vars Eq Eq' : Equation .
  vars EqS EqS' EqS'' : EquationSet .
  var  P : Position .
  var  PS : PositionSet .
  var  Subst : Substitution .
  var  SubstS : SubstitutionSet .
  vars AtS AtS' : AttrSet .
  var  M' : Module .
  vars X F S L L' L1 L1' L2 L2' : Qid .
  var  TL : TermList .
  vars Cd Cd1 Cd2 : EqCondition .

**** We declare sorts for critical pairs (\texttt{CritPair}) and for sets of
**** critical pairs (\texttt{CritPairSet}), and constructors for them.  The
**** constructors for critical pairs (\texttt{cp}) and for conditional critical
**** pairs (\texttt{ccp}) have, respectively, two and four arguments. The two
**** arguments of \texttt{cp} and the first two of \texttt{ccp} are the terms
**** forming the critical pair. The two last arguments in a conditional critical
**** pair correspond to the condition, which is given following the conventions
**** for conditions in membership axioms, equations, and rules in the
**** \texttt{META-LEVEL} module.

**** Given a specification $\mathcal{S}$, the \texttt{critPairs} function finds
**** all the critical pairs between the equations in $\mathcal{S}$ considered
**** as rules, oriented from left to right. 

**** One critical pair is generated for each unifier for each of the possible
**** nonvariable overlappings of the lefthand sides of any two equations in the
**** module. These critical pairs are calculated by finding all the possible 
**** such pairs for each of the equations in the module (\texttt{critPairs1}) 
**** with a renamed copy of each one of the other equations in the module 
**** (including itself \texttt{critPairs2}). For each pair of equations, their 
**** left sides are unified at any nonvariable position of the term of the 
**** (first equation \texttt{critPairs3}), and then a critical pair is 
**** constructed for each one of the solutions of the unification problem 
**** (\texttt{critPairs4}).

**** As said above, the critical pair is formed by \texttt{critPairs4} for a 
**** pair of equations with an overlapping at some position with some 
**** substitution. In the cases when one or both of the equations involved are
**** conditional, then the conjunction of the conditions with the substitution 
**** applied to them is placed as the condition of the critical pair.

  op critPairs : Module -> CritPairSet .
  op critPairs1 : Module EquationSet EquationSet -> CritPairSet .
  op critPairs2 : Module Equation EquationSet -> CritPairSet .
  op critPairs3 : Module Equation Equation PositionSet -> CritPairSet .
  op critPairs4 : 
       Module Equation Equation Position SubstitutionSet -> CritPairSet .

  eq critPairs(M) = critPairs1(M, getEqs(M), getEqs(M)) .

  eq critPairs1(M, (ceq T = T' if Cd [AtS]. EqS), EqS')
    = critPairs1(M, EqS, EqS')
      critPairs2(M, ceq rename(T) = rename(T') if rename(Cd) [AtS] ., EqS') .
  eq critPairs1(M, (eq T = T' [AtS] . EqS), EqS')
    = critPairs1(M, EqS, EqS')
      critPairs2(M, eq rename(T) = rename(T') [AtS] ., EqS') .
  eq critPairs1(M, none, EqS) = none .

  eq critPairs2(M, (ceq T = T' if Cd [AtS].), (Eq EqS))
    = critPairs2(M, (ceq T = T' if Cd [AtS] .), EqS)
      critPairs3(M, (ceq T = T' if Cd [AtS] .), Eq, allNonVarPos(T)) .
  eq critPairs2(M, (eq T = T' [AtS] .), (Eq EqS))
    = critPairs2(M, (eq T = T' [AtS].), EqS)
      critPairs3(M, (eq T = T' [AtS].), Eq, allNonVarPos(T)) .
  eq critPairs2(M, Eq, none) = none .

  eq critPairs3(M, (ceq T1 = T1' if Cd1 [AtS] .), 
       (ceq T2 = T2' if Cd2 [AtS'] .), posSet(P, PS))
    = critPairs3(M, ceq T1 = T1' if Cd1[AtS]., ceq T2 = T2' if Cd2[AtS']., PS)
      critPairs4(M, ceq T1 = T1' if Cd1[AtS]., ceq T2 = T2' if Cd2[AtS']., 
          P, unify(M, getSubterm(T1, P), T2)) .
  eq critPairs3(M, (eq T1 = T1' [AtS] .), 
       (ceq T2 = T2' if Cd2 [AtS'].), posSet(P, PS))
    = critPairs3(M, (eq T1 = T1' [AtS].), 
          (ceq T2 = T2' if Cd2 [AtS'].), PS)
      critPairs4(M, (eq T1 = T1' [AtS].), 
                    (ceq T2 = T2' if Cd2 [AtS'].),
          P, unify(M, getSubterm(T1, P), T2)) .
  eq critPairs3(M, (ceq T1 = T1' if Cd1 [AtS].), 
        (eq T2 = T2' [AtS'].), posSet(P, PS))
    = critPairs3(M, (ceq T1 = T1' if Cd1 [AtS].), 
          (eq T2 = T2' [AtS'].), PS)
      critPairs4(M, (ceq T1 = T1' if Cd1 [AtS].), 
          (eq T2 = T2' [AtS'].), P, unify(M, getSubterm(T1, P), T2)) .
  eq critPairs3(M, (eq T1 = T1' [AtS].), (eq T2 = T2' [AtS'].), posSet(P, PS))
    = critPairs3(M, (eq T1 = T1' [AtS].), (eq T2 = T2' [AtS'].), PS)
      critPairs4(M, (eq T1 = T1' [AtS].), (eq T2 = T2' [AtS'].), 
          P, unify(M, getSubterm(T1, P), T2)) .
  eq critPairs3(M, Eq, Eq', emptyPosSet) = none .

  eq critPairs4(M, (ceq T1 = T1' if Cd1 [AtS] .), 
       (ceq T2 = T2' if Cd2 [AtS'] .), P, 
       substitutionSet(Subst, SubstS))
    = ccp(getLabel(AtS), getLabel(AtS'),
          substitute(T1', Subst), 
          replace(substitute(T1, Subst), substitute(T2', Subst), P), 
          substitute(Cd1 /\ Cd2, Subst))
      critPairs4(M, (ceq T1 = T1' if Cd1 [AtS] .), 
        (ceq T2 = T2' if Cd2 [AtS'] .), P, SubstS) .
  eq critPairs4(M, (ceq T1 = T1' if Cd1 [AtS] .), (eq T2 = T2' [AtS'] .), P,
        substitutionSet(Subst, SubstS))
    = ccp(getLabel(AtS), getLabel(AtS'),
          substitute(T1', Subst), 
          replace(substitute(T1, Subst), substitute(T2', Subst), P), 
          substitute(Cd1, Subst))
      critPairs4(M, (ceq T1 = T1' if Cd1 [AtS] .), 
        (eq T2 = T2' [AtS'] .), P, SubstS) .
  eq critPairs4(M, (eq T1 = T1' [AtS].), (ceq T2 = T2' if Cd2 [AtS'] .), P,
        substitutionSet(Subst, SubstS))
    = ccp(getLabel(AtS), getLabel(AtS'),
          substitute(T1', Subst), 
          replace(substitute(T1, Subst), substitute(T2', Subst), P), 
          substitute(Cd2, Subst))
      critPairs4(M, (eq T1 = T1' [AtS].), 
        (ceq T2 = T2' if Cd2 [AtS'].), P, SubstS) .
  eq critPairs4(M, (eq T1 = T1' [AtS].), (eq T2 = T2' [AtS'].), P, 
       substitutionSet(Subst, SubstS))
    = cp(getLabel(AtS), getLabel(AtS'),
         substitute(T1', Subst), replace(substitute(T1, Subst), 
           substitute(T2', Subst), P))
      critPairs4(M, (eq T1 = T1' [AtS].), (eq T2 = T2' [AtS'].), P, SubstS) .
  eq critPairs4(M, Eq, Eq', P, emptySubstitutionSet) = none .

  op confluenceCheck : Module -> Tuple{CritPairSet, CritPairSet} .

  eq confluenceCheck(M)
    = (critPairs(M), 
       maximalCPSet(delete(simplify(delete(critPairs(M)), M)), M)) .
endfm

-------------------------------------------------------------------------------
---- descent-check.maude
-------------------------------------------------------------------------------

fmod DESCENT-CHECK is
  pr MATCHING .
  pr EXT-BOOL .

  inc META-LEVEL .

  var  M : Module .
  vars T T' T'' T1 T2 T1' T2' : Term .
  var  EqS : EquationSet .
  vars MA MA' : MembAx .
  vars MAS MAS' : MembAxSet .
  vars S S1 S2 : Sort .
  var  Eq : Equation .
  var  X : Qid .
  var  Tp : Type .
  var  TpS : TypeSet .
  var  V : Variable .
  var  VS : QidSet .
  var  Subst : Substitution .
  var  SubstS : SubstitutionSet .
  vars AtS AtS' : AttrSet .
  var  Cd : EqCondition .

  op eqInstanceSet : Module EquationSet -> EquationSet .

  op instanceSet : Module Equation SubstitutionSet -> EquationSet .
  op genSubstSet : Module QidSet Substitution -> SubstitutionSet .
  op genSubstSetAux : Module Qid TypeSet QidSet Substitution -> SubstitutionSet .

  eq eqInstanceSet(M, ((eq T = T' [AtS].) EqS))
    = (instanceSet(M, (eq T = T' [AtS].), genSubstSet(M, vars(T), none))
       eqInstanceSet(M, EqS)) .
  eq eqInstanceSet(M, ((ceq T = T' if Cd [AtS].) EqS))
    = (instanceSet(M, (ceq T = T' if Cd [AtS].), genSubstSet(M, vars(T), none))
       eqInstanceSet(M, EqS)) .
  eq eqInstanceSet(M, none) = none .

  eq instanceSet(M, (eq T = T' [AtS].), substitutionSet(Subst, SubstS))
    = ((eq substitute(T, Subst) = substitute(T', Subst) [AtS].)
       instanceSet(M, (eq T = T' [AtS].), SubstS)) .
  eq instanceSet(M, (ceq T = T' if Cd [AtS].), 
       substitutionSet(Subst, SubstS))
    = ((ceq substitute(T, Subst) = substitute(T', Subst)
          if substitute(Cd, Subst) [AtS].)
       instanceSet(M, (ceq T = T' if Cd [AtS].), SubstS)) .
  eq instanceSet(M, Eq, emptySubstitutionSet) = none .

  op substitute : EqCondition Substitution -> EqCondition .
  eq substitute(T = T' /\ Cd, Subst) 
    = substitute(T, Subst) = substitute(T', Subst) /\ substitute(Cd, Subst) .
  eq substitute(T := T' /\ Cd, Subst) 
    = substitute(T, Subst) := substitute(T', Subst) /\ substitute(Cd, Subst) .
  eq substitute(T : S /\ Cd, Subst) 
    = substitute(T, Subst) : S /\ substitute(Cd, Subst) .
  eq substitute((nil).EqCondition, Subst) = nil .

  eq genSubstSet(M, V ; VS, Subst)
    = genSubstSetAux(M, V, getType(V) ; lesserSorts(M, getType(V)), VS, Subst) .
  eq genSubstSet(M, none, Subst) = Subst .

  eq genSubstSetAux(M, V, (Tp ; TpS), VS, Subst)
   = if getType(V) == Tp
     then substitutionSet(
            genSubstSet(M, VS, Subst),
            genSubstSetAux(M, V, TpS, VS, Subst))
     else substitutionSet(
            genSubstSet(M, VS, 
              ((V <- qid(string(getName(V)) + "@" + string(getType(V)) 
                       + ":" + string(getType(V)))) ; Subst)),
            genSubstSetAux(M, V, TpS, VS, Subst)) 
     fi .     
  eq genSubstSetAux(M, V, none, VS, Subst) = emptySubstitutionSet .

  op maximalMASet : MembAxSet Module -> MembAxSet .
  op maximalMASetAux : MembAx MembAxSet MembAxSet Module -> MembAxSet .
  op moreGeneralMA? : MembAx MembAx Module -> Bool .

  eq maximalMASet((MA MAS), M) = maximalMASetAux(MA, MAS, none, M) .
  eq maximalMASet(none, M) = none .
  
  eq maximalMASetAux(MA, (MA' MAS), MAS', M)
    = if moreGeneralMA?(MA, MA', M)
      then maximalMASetAux(MA, MAS, MAS', M)
      else if moreGeneralMA?(MA', MA, M)
           then maximalMASetAux(MA', (MAS MAS'), none, M)
           else maximalMASetAux(MA, MAS, (MA' MAS'), M)
           fi
      fi .
  eq maximalMASetAux(MA, none, (MA' MAS), M)
    = (MA maximalMASetAux(MA', MAS, none, M)) .
  eq maximalMASetAux(MA, none, none, M) = MA .

  eq moreGeneralMA?((mb T1 : S1 [AtS].), (mb T2 : S2 [AtS'].), M)
    = match(M, (eq T1 = T2 [none].)) and-then sortLeq(M, S1, S2) .

  eq moreGeneralMA?((mb T1 : S1 [AtS].),  
                    (cmb T2 : S2 if T2' = 'true.Bool [AtS'].), M)
    = sortLeq(M, S1, S2) and-then match(M, (eq T1 = T2 [none].)) .
  eq moreGeneralMA?((cmb T1 : S1 if T1' = 'true.Bool [AtS].), 
                    (mb T2 : S2 [AtS'].), M)
    = (T1' == 'true.Bool)
      and-then
      (sortLeq(M, S1, S2) and-then match(M, (eq T1 = T2 [none].))) .

  eq moreGeneralMA?((cmb T1 : S1 if T1' = 'true.Bool [AtS].),
                    (cmb T2 : S2 if T2' = 'true.Bool [AtS'].), M)
    = (T1' == 'true.Bool)
      and-then
      (sortLeq(M, S1, S2)
       and-then
       match(M, ((eq T1 = T2 [none].) (eq T1' = T2 [none].)))) .

  op descentCheck : Module -> MembAxSet .
  op descentCheck1 : Module EquationSet -> MembAxSet .

  eq descentCheck(M)
    = maximalMASet(descentCheck1(M, eqInstanceSet(M, getEqs(M))), M) .

  eq descentCheck1(M, ((eq T = T' [AtS].) EqS))
    = if sortLeq(M, leastSort(M, getTerm(metaReduce(M, T'))), leastSort(M, T))
      then descentCheck1(M, EqS)
      else ((mb T' : (leastSort(M, T)) [(none).AttrSet].)) 
           descentCheck1(M, EqS)
      fi .
  eq descentCheck1(M, none) = none .

  eq descentCheck1(M, ((ceq T = T' if Cd [AtS].) EqS))
    = if sortLeq(M, leastSort(M, getTerm(metaReduce(M, T'))), leastSort(M, T))
      then descentCheck1(M, EqS)
      else ((cmb T' : leastSort(M, T) if Cd [(none).AttrSet].)
            descentCheck1(M, EqS))
      fi .
endfm

-------------------------------------------------------------------------------
---- crc.maude
-------------------------------------------------------------------------------

view Tuple`{CritPairSet`,CritPairSet`} 
    from TRIV to 2TUPLE{CritPairSet, CritPairSet} is
  sort Elt to Tuple{CritPairSet, CritPairSet} .
endv

view MembAxSet from TRIV to META-LEVEL is 
  sort Elt to MembAxSet .
endv

fmod CRC is
  pr CONFLUENCE-CHECK .
  pr DESCENT-CHECK .
  pr 2TUPLE{Tuple`{CritPairSet`,CritPairSet`}, MembAxSet}
       * (sort Tuple{Tuple`{CritPairSet`,CritPairSet`}, MembAxSet} 
            to CRCCheckingSolution) .
        
  var  M : Module . 

  op checking : Module -> CRCCheckingSolution .

  eq checking(M) = (confluenceCheck(M), descentCheck(M)) .
endfm

-------------------------------------------------------------------------------
---- coherence check
-------------------------------------------------------------------------------

**** CoherenceCheck 
**** local coherence properties reduces to ensuring that the
**** property is verified for all critical pairs\footnote{Note that we only
**** check equational coherence, and thus the non-superposition case is
**** verified.}. 

fmod COHERENCE-CHECK is
  pr CRITICAL-PAIR .
  pr 2TUPLE{CritPairSet, CritPairSet} .

  sort TermSet .
  subsort Term < TermSet .
  op emptyTS : -> TermSet .
  op _#_ : TermSet TermSet -> TermSet [assoc comm id: emptyTS] .
  eq T # T = T .

  var  G : Bool .
  var  M : Module .
  vars T T' T'' T1 T1' T2 T2' T1'' T2'' : Term .
  vars CP CP' : CritPair .
  vars CPS CPS' : CritPairSet .
  vars Eq Eq' : Equation .
  vars EqS EqS' EqS'' : EquationSet .
  vars Rl : Rule .
  var  RlS : RuleSet .
  var  P : Position .
  var  PS : PositionSet .
  var  Subst : Substitution .
  var  SubstS : SubstitutionSet .
  vars AtS AtS' AtS1 AtS2 : AttrSet .
  var  M' : Module .
  vars X F S L L' L1 L1' L2 L2' : Qid .
  var  TL : TermList .
  vars Cd Cd1 Cd2 : EqCondition .
  var  TS : TermSet .
  var  N : Nat .
  var  RST? : [ResultTriple] .

  ops lhs rhs : Equation -> Term .
  ops lhs rhs : Rule -> Term .
  op condition : Equation ~> EqCondition .
  op condition : Rule ~> Condition .
  eq lhs(eq T = T' [AtS] .) = T .
  eq lhs(ceq T = T' if Cd [AtS] .) = T .
  eq lhs(rl T => T' [AtS] .) = T .
  eq lhs(crl T => T' if Cd [AtS] .) = T .
  eq rhs(eq T = T' [AtS] .) = T' .
  eq rhs(ceq T = T' if Cd [AtS] .) = T' .
  eq rhs(rl T => T' [AtS] .) = T' .
  eq rhs(crl T => T' if Cd [AtS] .) = T' .
  eq condition(eq T = T' [AtS] .) = nil .
  eq condition(ceq T = T' if Cd [AtS] .) = Cd .
  eq condition(rl T => T' [AtS] .) = nil .
  eq condition(crl T => T' if Cd [AtS] .) = Cd .

  ---- crcCritPairs returns the critical pairs between equations and
  ---- rules in the module given as argument
  ---- The Bool value given as second argument indicates whether the 
  ---- critical pairs are for ground coherence or for coherence
  ---- true means ground coherence, false means coherence
  op chcCritPairs : Module Bool -> CritPairSet .
  op chcCritPairs1 : Module EquationSet RuleSet Bool -> CritPairSet .
  op chcCritPairs2 : Module Equation RuleSet Bool -> CritPairSet .
  op chcCritPairs3-1 : Module Equation Rule PositionSet -> CritPairSet .
  op chcCritPairs3-2 : Module Equation Rule PositionSet -> CritPairSet .
  op chcCritPairs4-1 : Module Equation Rule Position SubstitutionSet -> CritPair .
  op chcCritPairs4-2 : Module Equation Rule Position SubstitutionSet -> CritPair .
  op chcCritPairs5 : Module Equation Rule Term TermSet Term SubstitutionSet -> CritPair .
  op chcCritPairs6 : Module Equation Rule Term Term SubstitutionSet -> CritPair .

  eq chcCritPairs(M, G) = chcCritPairs1(M, getEqs(M), getRls(M), G) .

  eq chcCritPairs1(M, (ceq T = T' if Cd [AtS]. EqS), RlS, G)
    = chcCritPairs1(M, EqS, RlS, G)
      chcCritPairs2(M, ceq rename(T) = rename(T') if rename(Cd) [AtS] ., RlS, G) .
  eq chcCritPairs1(M, (eq T = T' [AtS] . EqS), RlS, G)
    = chcCritPairs1(M, EqS, RlS, G)
      chcCritPairs2(M, eq rename(T) = rename(T') [AtS] ., RlS, G) .
  eq chcCritPairs1(M, none, RlS, G) = none .

  eq chcCritPairs2(M, Eq, (Rl RlS), G)
    = chcCritPairs2(M, Eq, RlS, G)
      chcCritPairs3-1(M, Eq, Rl, allNonVarNonFrozenPos(M, lhs(Eq), G))
      chcCritPairs3-2(M, Eq, Rl, allNonVarPos(lhs(Rl))) .
  eq chcCritPairs2(M, Eq, none, G) = none .

  eq chcCritPairs3-1(M, Eq, Rl, posSet(P, PS))
    = chcCritPairs3-1(M, Eq, Rl, PS)
      chcCritPairs4-1(M, Eq, Rl, P, unify(M, getSubterm(lhs(Eq), P), lhs(Rl))) .
  eq chcCritPairs3-1(M, Eq, Rl, emptyPosSet) = none .

  eq chcCritPairs3-2(M, Eq, Rl, posSet(P, PS))
    = chcCritPairs3-2(M, Eq, Rl, PS)
      chcCritPairs4-2(M, Eq, Rl, P, unify(M, lhs(Eq), getSubterm(lhs(Rl), P))) .
  eq chcCritPairs3-2(M, Eq, Rl, emptyPosSet) = none .

  eq chcCritPairs4-1(M, Eq, Rl, P, substitutionSet(Subst, SubstS))
    = chcCritPairs5(M, Eq, Rl,
        getTerm(metaReduce(M, substitute(lhs(Eq), Subst))),
        getAllOneStepRewrites(M, getTerm(metaReduce(M, substitute(lhs(Eq), Subst)))),
        replace(substitute(lhs(Eq), Subst), substitute(rhs(Rl), Subst), P),
        Subst) 
      chcCritPairs4-1(M, Eq, Rl, P, SubstS) .
  eq chcCritPairs4-1(M, Eq, Rl, P, emptySubstitutionSet) = none .

  eq chcCritPairs4-2(M, Eq, Rl, P, substitutionSet(Subst, SubstS))
    = chcCritPairs5(M, Eq, Rl,
        getTerm(metaReduce(M, substitute(lhs(Rl), Subst))),
        getAllOneStepRewrites(M, getTerm(metaReduce(M, substitute(lhs(Rl), Subst)))),
        substitute(rhs(Rl), Subst),
        Subst)
      chcCritPairs4-2(M, Eq, Rl, P, SubstS) .
  eq chcCritPairs4-2(M, Eq, Rl, P, emptySubstitutionSet) = none .

  eq chcCritPairs5(M, Eq, Rl, T1, T # TS, T2, Subst) 
    ----= if getTerm(metaReduce(M, '_==_[T, T2])) == 'true.Bool 
    = if getTerm(metaReduce(M, T)) == getTerm(metaReduce(M, T2))
      then none
      else chcCritPairs5(M, Eq, Rl, T1, TS, T2, Subst)
      fi .
  eq chcCritPairs5(M, Eq, Rl, T1, emptyTS, T2, Subst) 
    ----= if getTerm(metaReduce(M, '_==_[T1, T2])) == 'true.Bool 
    = if getTerm(metaReduce(M, T1)) == getTerm(metaReduce(M, T2))
      then none
      else chcCritPairs6(M, Eq, Rl, T1, T2, Subst) 
      fi .

  eq chcCritPairs6(M, (eq T1 = T1' [AtS1] .), (rl T2 => T2' [AtS2] .), T, T', Subst) 
    = cp(getLabel(AtS1), getLabel(AtS2), T, T') .
  eq chcCritPairs6(M, (ceq T1 = T1' if Cd1 [AtS1] .), (rl T2 => T2' [AtS2] .), T, T', Subst) 
    = ccp(getLabel(AtS1), getLabel(AtS2), T, T', substitute(Cd1, Subst)) .
  eq chcCritPairs6(M, (eq T1 = T1' [AtS1] .), (crl T2 => T2' if Cd2 [AtS2] .), T, T', Subst) 
    = ccp(getLabel(AtS1), getLabel(AtS2), T, T', substitute(Cd2, Subst)) .
  eq chcCritPairs6(M, (ceq T1 = T1' if Cd1 [AtS1].), (crl T2 => T2' if Cd2 [AtS2].), T, T', Subst) 
    = ccp(getLabel(AtS1), getLabel(AtS2), T, T', substitute(Cd1 /\ Cd2, Subst)) .

  op getAllOneStepRewrites : Module Term -> TermSet .
  op getAllOneStepRewrites : Module Term Nat -> TermSet .

  eq getAllOneStepRewrites(M, T) = getAllOneStepRewrites(M, T, 0) .
  ceq getAllOneStepRewrites(M, T, N) 
    = if RST? == (failure).ResultTriple?
      then emptyTS
      else getTerm(RST?) # getAllOneStepRewrites(M, T, N + 1)
      fi
    if RST? := metaSearch(M, T, qid("V:" + string(getKind(M, leastSort(M, T)))), nil, '+, 1, N) .

**** As for the Church-Rosser checker, the critical pairs generated may use new 
**** variables. For each variable V:S in the original module a variable 
**** V@:S \footnote{These and other variables may be used for the unification 
**** algorithm, namely, for each variable V:S in the original module a variable 
**** V@@S':S' for each subsort S' of S is also added.}---used in the generation of 
**** critical pairs---and a variable V@S':S' for each subsort S' of S---used in the 
**** descent coherenceCheck---are created.

  ---- The Bool value given as second argument indicates whether the 
  ---- critical pairs are for ground coherence or for coherence
  ---- true means ground coherence, false means coherence
  op coherenceCheck : Module Bool -> Tuple{CritPairSet, CritPairSet} .

  eq coherenceCheck(M, G)
    = (chcCritPairs(M, G),
       maximalCPSet(delete(simplify(delete(chcCritPairs(M, G)), M)), M)) .

endfm

-------------------
------SIGN
-------------------

fmod CRC-SIGN is
  including FULL-MAUDE-SIGN .

  op check`Church-Rosser`. : -> @Command@ .
  op check`Church-Rosser_. : @ModExp@ -> @Command@ .
endfm

fmod CHC-SIGN is
  including FULL-MAUDE-SIGN .

  op check coherence . : -> @Command@ .
  op check coherence_. : @ModExp@ -> @Command@ .
  op check ground coherence . : -> @Command@ .
  op check ground coherence_. : @ModExp@ -> @Command@ .
endfm


fmod META-CRCHC-SIGN is
  inc META-LEVEL .
  pr META-FULL-MAUDE-SIGN .
  pr UNIT .

  op CRCHC-GRAMMAR : -> FModule .
  eq CRCHC-GRAMMAR 
    = addImports((including 'CRC-SIGN .) (including 'CHC-SIGN .), GRAMMAR) .
endfm


mod CRC-DATABASE-HANDLING is
  pr DATABASE-HANDLING .
  pr CRC .
 
  vars ME MN : ModuleExpression .
  var  DB : Database .
  var  M : Module .
  var  VS : QidSet .
  vars CPS CPS' : CritPairSet .
  var  MAS : MembAxSet .
  var  QIL : QidList .
  var  V : Variable .
  var  S : Sort .
  vars L L' : Qid .
  vars T T' T'' T''' : Term .

  sort CRC .
  subsort CRC < DatabaseClass .

  op CRC : -> CRC .

  var  Atts : AttributeSet .
  var  X@CRC : CRC .
  var  O : Oid .

  op processCRChecking : ModuleExpression Database -> QidList .
  op processCRCheckingAux : Module CRCCheckingSolution -> QidList .

  eq processCRChecking(ME, DB)
    = ('\n '\b 'Church-Rosser 'checking 'of '\o eMetaPrettyPrint(ME)
       processCRCheckingAux(getFlatModule(ME, DB), 
         checking(getFlatModule(ME, DB)))) .

  eq processCRCheckingAux(M, ((CPS, CPS'), MAS))
    = '\n '\b 'Checking 'solution: '\o
      if CPS == none 
      then '\b '\n '\s '\s 
           'There 'are 'no 'critical 'pairs.
           'The 'specification 'is 'confluent. '\o
      else if CPS' == none 
           then '\b '\n '\s '\s 
                'All 'critical 'pairs 'have 'been 'joined. 'The 'specification 'is 
                '\n '\s '\s '\s '\s 
                'locally-confluent. '\o
           else 'The 'following 'critical 'pairs 'cannot 'be 'joined: '\o
                eMetaPrettyPrint(M, '=, CPS') 
           fi
      fi
      if MAS == none
      then '\b '\n '\s '\s 
           'The 'specification 'is 'sort-decreasing. '\o
      else 'There 'are 'non-sort-decreasing 'equations. 'The 'following 'proof 
           '\n '\s '\s '\s '\s 
           'obligations 'must 'be 'checked:
           eMetaPrettyPrint(M, MAS)
      fi .

  rl [CRChecking] :
     < O : X@CRC | db : DB, input : 'check`Church-Rosser`..@Command@, 
        output : QIL, default : MN, Atts >
     => < O : X@CRC | db : DB, input : nilTermList, 
           output : processCRChecking(MN, DB), 
           default : MN, Atts > .
  rl [CRChecking] :
     < O : X@CRC | db : DB, input : ('check`Church-Rosser_.[T]), 
        output : QIL, default : MN, Atts >
     => < O : X@CRC | db : DB, input : nilTermList, 
           output : processCRChecking(parseModExp(T), DB), 
           default : MN, Atts > .
endm

mod CRCHC-DATABASE-HANDLING is
  pr CRC-DATABASE-HANDLING .
  pr COHERENCE-CHECK .
  pr LIST-AND-SET{Qid} 
       * (op empty to none, op _,_ to _;_ [prec 43],
          sort NeList{Qid} to NeQidList, sort List{Qid} to QidList,
          sort NeSet{Qid} to NeQidSet, sort Set{Qid} to QidSet) .

  var  G : Bool .
  vars ME MN : ModuleExpression .
  var  DB : Database .
  var  M : Module .
  var  VDS : VarDeclSet .
  vars CPS CPS' : CritPairSet .
  var  MAS : MembAxSet .
  var  QIL : QidList .
  var  Atts : AttributeSet .
  var  X@CRChC : CRChC .
  var  O : Oid .
  vars T T' T'' T''' : Term .
  var  TL : TermList .
  var  OPDS : OpDeclSet .
  var  Eq : Equation .
  var  EqS : EquationSet .
  var  Ct : Constant .
  vars QI F : Qid .
  var  Vb : Variable .
  var  Tp : Type .
  var  TpL : TypeList .
  var  AtS : AttrSet .
 
  sort CRChC .
  subsort CRChC < CRC .

  op CRChC : -> CRChC .

**** The processing of the checking commands is handled by the following function
**** \texttt{processCohChecking}. Given a module
**** expression and a database, it just calls the \texttt{checking} function
**** presented in Section~\ref{CohCh-specification} with the flat form of the
**** specified module in the database, and then gives the output as a list of
**** quoted identifiers ready to be passed to the read-eval-print loop.

  ---- The Bool value given as second argument indicates whether the 
  ---- critical pairs are for ground coherence or for coherence
  ---- true means ground coherence, false means coherence

  op processCohChecking : ModuleExpression Database Bool -> QidList .
  op processCohCheckingAux : Module Tuple{CritPairSet, CritPairSet} Bool -> QidList .

  eq processCohChecking(ME, DB, G)
    = ('\n 'Coherence 'checking 'of eMetaPrettyPrint(ME)
       processCohCheckingAux(getFlatModule(ME, DB), 
         coherenceCheck(getFlatModule(ME, DB), G), G)) .

  eq processCohCheckingAux(M, (CPS, CPS'), false) ---- (nonground) coherence
    = '\b '\n 'Coherence 'checking 'solution: 
      if CPS' == none
      then if chReq(getEqs(M)) == none
           then '\n '\s '\s 
                'All 'critical 'pairs 'have 'been 'rewritten 'and 'all 
                '\n '\s '\s '\s '\s 
                'equations 'are 'left- 'and 'right-linear 'and 
                'regular.
                '\n '\s '\s 
                if CPS == none
                then 'The 'specification 'is 'coherent. '\o
                else 'The 'specification 'is 'ground 'coherent. '\o
                fi
           else '\n '\s '\s 
                'All 'critical 'pairs 'have 'been 'rewritten. 'However`, 'the 
                '\n '\s '\s '\s '\s 
                'specification 'might 'fail 'to 'be 'ground 'coherent 'if 
                '\n '\s '\s '\s '\s 
                'there 'exist 'non-overlap 'situations 'rewriting 'at 'the 
                '\n '\s '\s '\s '\s 
                'top 'with 'the 'equations: '\o
                eMetaPrettyPrint(M, chReq(getEqs(M)))
                '\b 'and 'below 'with 'rules 'in 'the 'module 'can 'take 'place. 
           fi
      else '\n '\s '\s 
           'The 'following 'critical 'pairs 'cannot 'be 'rewritten: '\o
           eMetaPrettyPrint(M, '=>, CPS')
      fi .

  eq processCohCheckingAux(M, (CPS, CPS'), true) ---- ground coherence
    = '\b '\n 'Ground 'coherence 'checking 'solution: 
      if CPS' == none
      then if ctorEqs(M) == none
           then '\n '\s '\s 
                'All 'critical 'pairs 'have 'been 'rewritten 'and 'all 'equations 
                '\n '\s '\s '\s '\s 
                'are 'non-constructor.
                '\n '\s '\s 
                if CPS == none
                then 'The 'specification 'is 'coherent. '\o
                else 'The 'specification 'is 'ground 'coherent. '\o
                fi
           else if chReq(ctorEqs(M)) == none
                then '\n '\s '\s 
                     'All 'critical 'pairs 'have 'been 'rewritten 'and 'all 
                     '\n '\s '\s '\s '\s 
                     'equations 'with 'a 'constructor 'symbol 'at 'the 'top 'of 
                     '\n '\s '\s '\s '\s 
                     'their 'lefthand 'side 'are 'left- 'and 'right-linear 'and 
                     'regular.
                     '\n '\s '\s 
                     if CPS == none
                     then 'The 'specification 'is 'coherent. '\o
                     else 'The 'specification 'is 'ground 'coherent. '\o
                     fi
                else '\n '\s '\s 
                     'All 'critical 'pairs 'have 'been 'rewritten. 'However`, 'the 
                     '\n '\s '\s '\s '\s 
                     'specification 'might 'fail 'to 'be 'ground 'coherent 'if 
                     '\n '\s '\s '\s '\s 
                     'there 'exist 'non-overlap 'situations 'rewriting 'at 'the 
                     '\n '\s '\s '\s '\s 
                     'top 'with 'the 'equations: '\o
                     eMetaPrettyPrint(M, chReq(ctorEqs(M)))
                     '\b 'and 'below 'with 'rules 'in 'the 'module 'can 'take 'place. 
                fi
           fi
      else '\n '\s '\s 
           'The 'following 'critical 'pairs 'cannot 'be 'rewritten: '\o
           eMetaPrettyPrint(M, '=>, CPS')
      fi .

**** Finally, we give the rules describing the behavior of the \texttt{ChC} object
**** associated to the new commands. In both cases the processing is carried out by
**** the \texttt{processCohChecking} function, which is called with the specified
**** module name, in the case of the \verb~check`coherence_.~ command, or with the name 
**** of the default module, for the \verb~check`coherence .~ command.

  rl [CohChecking] :
     < O : X@CRChC | db : DB, input : ('check`coherence`..@Command@), 
        output : QIL, default : MN, Atts >
     => < O : X@CRChC | db : DB, input : nilTermList, 
           output : processCohChecking(MN, DB, false), 
           default : MN, Atts > .
  rl [CohChecking] :
     < O : X@CRChC | db : DB, input : ('check`coherence_.[T]), 
        output : QIL, default : MN, Atts >
     => < O : X@CRChC | db : DB, input : nilTermList, 
           output : processCohChecking(parseModExp(T), DB, false), 
           default : MN, Atts > .

  rl [CohChecking] :
     < O : X@CRChC | db : DB, input : ('check`ground`coherence`..@Command@), 
        output : QIL, default : MN, Atts >
     => < O : X@CRChC | db : DB, input : nilTermList, 
           output : processCohChecking(MN, DB, true), 
           default : MN, Atts > .
  rl [CohChecking] :
     < O : X@CRChC | db : DB, input : ('check`ground`coherence_.[T]), 
        output : QIL, default : MN, Atts >
     => < O : X@CRChC | db : DB, input : nilTermList, 
           output : processCohChecking(parseModExp(T), DB, true), 
           default : MN, Atts > .

  ---- ctorEqs returns those equations with a constructor at the top
  op ctorEqs : Module -> EquationSet .
  op ctorEqs : Module EquationSet -> EquationSet .
 
  eq ctorEqs(M) = ctorEqs(M, getEqs(M)) .

  eq ctorEqs(M, Eq EqS) 
    = if ctor(M, getOps(M), lhs(Eq)) 
      then Eq 
      else none
      fi
      ctorEqs(M, EqS) .
  eq ctorEqs(M, none) = none .
  
  ---- chReq returns those equations that are not either left-linear, 
  ---- right-linear, or regular.  
  op chReq : EquationSet -> EquationSet .
  ---- left-linear checks whether the equation is left-linear
  op left-linear : Equation -> Bool .
  ---- left-linear checks whether the equation is right-linear
  op right-linear : Equation -> Bool .
  ---- left-linear checks whether the equation is regular
  op regular : Equation -> Bool .
  ---- linear checks whether there are vbles repeated in the term
  op linear : Term -> Bool .
  ---- vbList returns a list with the variables in the term 
  ---- the order is not important, a multiset could be used.
  op vbList : Term -> QidList .
  ---- repeated checks whether there are repeated qids in the given list.
  op repeated : QidList -> Bool .
  
  eq chReq(Eq EqS) 
    = if left-linear(Eq) and-then right-linear(Eq) and-then regular(Eq) 
      then none
      else Eq
      fi
      chReq(EqS) .
  eq chReq(none) = none .
 
  eq left-linear(Eq) = linear(lhs(Eq)) . 
  eq right-linear(Eq) = linear(rhs(Eq)) . 
  eq regular(Eq) = makeSet(vbList(lhs(Eq))) == makeSet(vbList(rhs(Eq))) . 

  eq linear(T) = not repeated(vbList(T)) .
  
  eq vbList(Vb) = Vb . 
  eq vbList(Ct) = nil .
  eq vbList(F[TL]) = vbList(TL) .
  eq vbList((T, TL)) = vbList(T) vbList(TL) .
  
  eq repeated(QI QIL) = occurs(QI, QIL) or-else repeated(QIL) .
  eq repeated(nil) = false .
endm

*** Redefinition of the FULL-MAUDE module. The init rule now creates an 
*** instance of class CRChC. The init rule now takes CRChC objects, and for them 
*** it uses CRCHC-GRAMMAR instead of GRAMMAR to parse inputs. 

mod CRCHC-FULL-MAUDE is
  pr META-CRCHC-SIGN .
  pr CRCHC-DATABASE-HANDLING .
  inc LOOP-MODE .
  pr BANNER .
  pr CRCHC-BANNER .

  subsort Object < State .

  op o : -> Oid .
  op init : -> System .

  var  Atts : AttributeSet .
  var  X@CRChC : DatabaseClass .
  var  O : Oid .
  var  DB : Database .
  var  ME : Header .
  var  QI : Qid .
  vars QIL QIL' QIL'' : QidList .
  var  TL : TermList .
  var  N : Nat .
  vars RP RP' : ResultPair .

  rl [init] :
     init
     => [nil,
         < o : CRChC | 
            db : initialDatabase,
            input : nilTermList, output : nil, 
            default : 'CONVERSION >,
         ('\s '\s '\s '\s string2qidList(crchc-banner) '\n)] .

  rl [in] :
    [QI QIL, 
     < O : X@CRChC | 
         db : DB, input : nilTermList, output : nil, default : ME, Atts >, 
     QIL']
    => if metaParse(CRCHC-GRAMMAR, QI QIL, '@Input@) :: ResultPair
       then [nil, 
             < O : X@CRChC | db : DB, 
                 input : getTerm(metaParse(CRCHC-GRAMMAR, QI QIL, '@Input@)),
                 output : nil, default : ME, Atts >, 
              QIL'] 
       else [nil, 
             < O : X@CRChC | db : DB, input : nilTermList, 
                 output : ('\r 'Warning: 
                           printSyntaxError(
                             metaParse(CRCHC-GRAMMAR, QI QIL, '@Input@), 
                             QI QIL) 
                           '\n
                           '\r 'Error: '\o 'No 'parse 'for 'input. '\n), 
                 default : ME, Atts >, 
             QIL'] 
       fi .

  rl [out] :
    [QIL, 
     < O : X@CRChC | 
         db : DB, input : TL, output : (QI QIL'), default : ME, Atts >, 
     QIL'']
    => [QIL, 
        < O : X@CRChC | 
            db : DB, input : TL, output : nil, default : ME, Atts >, 
        (QI QIL' QIL'')] .
endm

loop init .

trace exclude CRCHC-FULL-MAUDE .

set show loop stats on .
set show loop timing on .
set show advisories on .