fmod BASICS is
  pr META-LEVEL .

  var AS       : AttrSet .
  var C C'     : Constant .
  var EqCond   : EqCondition .
  var K K'     : Kind .
  var Im       : Import .
  var ImL      : ImportList .
  var M        : Module .
  var Mb       : MembAx .
  var ME       : ModuleExpression .
  var Op       : OpDecl .
  var Q        : Qid .
  var S        : Sort .
  var St       : String .
  var T T'     : Term .
  var TL TL'   : TermList .
  var NTL NTL' : NeTermList .
  var Tp Tp'   : Type .
  var TpL TpL' : TypeList .
  var V V'     : Variable .

  --- Converts Maude variables into a "canonical" representation.  The way
  --- Maude distinguished between two variables is that two variables are
  --- equal if they have the same name and type associated with them.  If the
  --- type is a kind, then the representation of the Kind does not matter,
  --- e.g. [Foo] and [Bar] are equivalent if Foo and Bar are sorts in the
  --- same kind.  On the other hand X:Foo and X:Bar are never equivalent,
  --- even if Foo and Bar are in the same kind.
  op canonize : Module Variable -> Variable .
  eq canonize(M, V)
   = if getType(V) :: Sort then
       V
     else
       qid(string(getName(V)) + ":" + string(getKind(M, getType(V))))
     fi .

  --- Returns true if objects are of same type.
  --- Used because kind may be the same, but have different representations.
  op type= : Module Type Type ~> Bool .
  eq type=(M, K, K') = sameKind(M, K, K') .
  eq type=(M, Tp, Tp') = (Tp == Tp') [owise].

  --- Returns true if the two terms are syntactically equal.
  --- As an alternative we could  look into converting terms into syntatic
  --- canonical form and just using ==.  Note this assumes terms are linear.
  op terms= : Module TermList TermList -> Bool .
  eq terms=(M, (T, NTL), (T', NTL')) 
   = terms=(M, T, T') and terms=(M, NTL, NTL') .
  eq terms=(M, C, C')
   = (getName(C) == getName(C')) and
     sameKind(M, leastSort(M, C), leastSort(M, C')) .
  eq terms=(M, V, V') = type=(M, getType(V), getType(V')) .
  eq terms=(M, Q[TL], Q[TL']) = terms=(M, TL, TL') .
  eq terms=(M, empty, empty) = true .
  eq terms=(M, TL, TL') = false [owise].

  --- Returns the kinds of given a list of types.
  op get-kinds : Module TypeList -> TypeList .
  eq get-kinds(M, Tp TpL) = getKind(M, Tp) get-kinds(M, TpL) .
  eq get-kinds(M, nil) = nil .

  --- Returns the least sorts of a list of terms.
  op least-sort-list : Module TermList ~> TypeList .
  eq least-sort-list(M, (T, TL)) = leastSort(M, T) least-sort-list(M, TL) .
  eq least-sort-list(M, empty) = nil .
 
  --- Returns true if the type is in the type is in the list.
  op in-list : Type TypeList -> Bool .
  eq in-list(Tp, TpL Tp TpL') = true .
  eq in-list(Tp, TpL) = false [owise].

  op id : OpDecl -> Qid .
  eq id((op Q : TpL -> Tp [AS].)) = Q .

  op inputs : OpDecl -> TypeList .
  eq inputs((op Q : TpL -> Tp [AS].)) = TpL .

  op output : OpDecl -> Type .
  eq output((op Q : TpL -> Tp [AS].)) = Tp .

  op is-special : OpDecl -> Bool .
  eq is-special((op Q : TpL -> Tp [special(HL:HookList) AS].)) = true .
  eq is-special(Op) = false [owise].

  op is-ctor : OpDecl -> Bool .
  eq is-ctor((op Q : TpL -> Tp [ctor AS].)) = true .
  eq is-ctor(Op) = false [owise].

  op lhs : Equation -> Term .
  eq lhs(eq T = T' [AS].) = T .
  eq lhs(ceq T = T' if EqCond [AS].) = T .

  op lhs : MembAx -> Term .
  eq lhs(mb  T : S[AS].) = T .
  eq lhs(cmb T : S if EqCond[AS].) = T .

  op rhs : MembAx -> Sort .
  eq rhs(mb  T : S[AS].) = S .
  eq rhs(cmb T : S if EqCond[AS].) = S .

  op has-dfn : AttrSet -> Bool .
  eq has-dfn(metadata(St) AS) = (St == "dfn") or has-dfn(AS) .
  eq has-dfn(AS) = false [owise].

  op is-ctor : MembAx -> Bool .
  eq is-ctor((mb T : S [AS].)) = has-dfn(AS) .
  eq is-ctor((cmb T : S if EqCond [AS].)) = has-dfn(AS) .
  eq is-ctor(Mb) = false [owise].

  --- Returns the module expression from an inport list.
  op getExpression : Import -> ModuleExpression .
  eq getExpression(protecting ME .) = ME .
  eq getExpression(extending ME .) = ME .
  eq getExpression(including ME .) = ME .

  op importSorts : ImportList ~> SortSet .
  eq importSorts(Im ImL)
   = upSorts(getExpression(Im), true) ; importSorts(ImL) .
  eq importSorts(ImL) = none .

  op importSubsorts : ImportList ~> SubsortDeclSet .
  eq importSubsorts(Im ImL)
   = upSubsortDecls(getExpression(Im), true) importSubsorts(ImL) .
  eq importSubsorts(nil) = none .

  op importOps : ImportList ~> OpDeclSet .
  eq importOps(Im ImL)
   = upOpDecls(getExpression(Im), true) importOps(ImL) .
  eq importOps(nil) = none .

  op import-mbs : ImportList ~> MembAxSet .
  eq import-mbs(Im ImL)
   = upMbs(getExpression(Im), true) import-mbs(ImL) .
  eq import-mbs(nil) = none .

  op importEqs : ImportList ~> EquationSet .
  eq importEqs(Im ImL)
   = upEqs(getExpression(Im), true) importEqs(ImL) .
  eq importEqs(nil) = none .

  op importRls : ImportList ~> RuleSet .
  eq importRls(Im ImL)
   = upRls(getExpression(Im), true) importRls(ImL) .
  eq importRls(nil) = none .

  op get-sorts : Module Bool -> SortSet .
  eq get-sorts(M, false) = getSorts(M) .
  eq get-sorts(M, true) = getSorts(M) ; importSorts(getImports(M)) .

  op get-subsorts : Module Bool -> SubsortDeclSet .
  eq get-subsorts(M, false) = getSubsorts(M) .
  eq get-subsorts(M, true) = getSubsorts(M) importSubsorts(getImports(M)) .

  op get-ops : Module Bool -> OpDeclSet .
  eq get-ops(M, false) = getOps(M) .
  eq get-ops(M, true) = getOps(M) importOps(getImports(M)) .

  op get-mbs : Module Bool -> MembAxSet .
  eq get-mbs(M, false) = getMbs(M) .
  eq get-mbs(M, true) = getMbs(M) import-mbs(getImports(M)) .

  op get-eqs : Module Bool -> EquationSet .
  eq get-eqs(M, false) = getEqs(M) .
  eq get-eqs(M, true) = getEqs(M) importEqs(getImports(M)) .
endfm

fmod AUTOMATA-STATE is
  pr BASICS .
  pr CONVERSION .

  var K  : Kind .
  var M  : Module .
  var N  : Nat .
  var S  : Sort .
  var T  : Term .
  var Tp : Type .

  --- Return a short name for a kind taken from first maximal sort.
  op kind-name : Kind ~> String .
  ceq kind-name(K) = substr(string(K), 2, N)
   if s(s(N)) := find(string(K), "`,", 0) .
  ceq kind-name(K) = substr(string(K), 2, N)
   if s(s(s(s(N)))) := length(string(K)) [owise].

  op kind-name : Module Type ~> String .
  eq kind-name(M, Tp) = kind-name(getKind(M, Tp)) .

  op state-name : Kind ~> String .
  eq state-name(K) = kind-name(K) + "State" .

  op state-name : Module Type ~> String .
  eq state-name(M, Tp) = kind-name(M, Tp) + "State" .

  --- Returns the automaton state for kind of terms with type.
  op kind-state : Module Type ~> Constant .
  eq kind-state(M, Tp)
   = qid("k[" + kind-name(M, Tp) + "]." + state-name(M, Tp)) .

  --- Returns the automaton state for constructor terms with type.
  op ctor-state : Module Type ~> Constant .
  eq ctor-state(M, S) = qid("c" + string(S) + "." + state-name(M, S)) .
  eq ctor-state(M, K) = kind-state(M, K) .

  --- Returns the automaton state for defined terms with sort.
  op def-state : Module Sort ~> Constant .
  eq def-state(M, S) = qid("d" + string(S) + "." + state-name(M, S)) .

  --- Returns the automaton state for reducible terms of type.
  op red-state : Module Type ~> Constant .
  eq red-state(M, Tp)
   = qid("r[" + kind-name(M, Tp) + "]." + state-name(M, Tp)) .

  --- Returns the term state for a given number.
  op term-state : Kind Nat ~> Constant .
  eq term-state(K, N)
   = qid(kind-name(K) + "Term" + string(N, 10) + "." + state-name(K)) .

  --- Returns the term state for a term assigned a specific number.
  op term-state : Module Term Nat ~> Constant .
  eq term-state(M, T, N) = term-state(getKind(M, leastSort(M, T)), N) .
endfm

fmod TERM-STATE-MAP is
  pr BASICS .
  pr AUTOMATA-STATE .

  sort TermStateMap .
  op nil : -> TermStateMap [ctor].
  op term : Term -> TermStateMap [ctor].
  op __ : TermStateMap TermStateMap -> TermStateMap [ctor assoc id: nil].

  var C    : Constant .
  var M    : Module .
  var N    : Nat .
  var Q    : Qid .
  var T T' : Term .
  var TL TL' : TermList .
  var TSM  : TermStateMap .
  var V    : Variable .

  op find-term : Module TermStateMap Term Nat ~> FindResult .
  eq find-term(M, term(T) TSM, T', N)
   = if terms=(M, T, T') then
       N
     else
       find-term(M, TSM, T', s N)
     fi .
  eq find-term(M, nil, T, N) = notFound .

  op register-term : Module TermList TermStateMap ~> TermStateMap .
  eq register-term(M, (V, TL), TSM) = register-term(M, TL, TSM) .
  eq register-term(M, (Q[TL], TL'), TSM)
   = if find-term(M, TSM, Q[TL], 0) == notFound then
       register-term(M, (TL, TL'), TSM term(Q[TL]))
     else
       register-term(M, TL', TSM)
     fi .
  eq register-term(M, (C, TL), TSM)
   = if find-term(M, TSM, C, 0) == notFound then
       register-term(M, TL, TSM term(C))
     else
       register-term(M, TL, TSM)
     fi .
  eq register-term(M, empty, TSM) = TSM .

  --- Given a module and termstate map, returns the appropriate state
  --- constant for a term (variables are assumed to be in ctor subsignature).
  op term-state : Module TermStateMap Term ~> Constant .
  eq term-state(M, TSM, T)
   = if T :: Variable then
       ctor-state(M, getType(T))
     else
       term-state(M, T, find-term(M, TSM, T, 0))
     fi .

  op term-states : Module TermStateMap Nat ~> QidList .
  eq term-states(M, term(T) TSM, N)
   = term-state(M, T, N) term-states(M, TSM, s N) .
  eq term-states(M, nil, N) = nil .
endfm

fmod PTA is
  pr META-LEVEL .
  sort EmptinessResult .
  op empty : -> EmptinessResult [ctor].
  op accepting : Term QidSet -> EmptinessResult [ctor].
  op invalid-input : -> EmptinessResult [ctor].

  op test-emptiness : Module ~> EmptinessResult
	[special (
	   id-hook CompletenessCheckerSymbol
           op-hook shareWith (metaReduce : Module Term ~> ResultPair)
           op-hook emptySymbol (empty : ~> EmptinessResult)
           op-hook acceptingTermSymbol
                   (accepting : Term Term ~> EmptinessResult)
           op-hook invalidInputSymbol (invalid-input : ~> EmptinessResult)
           op-hook qidSetSymbol (_;_ : QidSet QidSet ~> QidSet))] .
endfm

fmod SCC is
  pr PTA .
  pr BASICS .
  pr TERM-STATE-MAP .

  var AS        : AttrSet .
  var C C'      : Constant .
  var CL        : QidList .
  var Eq        : Equation .
  var Eqs       : EquationSet .
  var K K'      : Kind .
  var KS        : KindSet .
  var M         : Module .
  var Mb        : MembAx .
  var Mbs       : MembAxSet .
  var N         : Nat .
  var Op        : OpDecl .
  var Ops       : OpDeclSet .
  var Q         : Qid .
  var QL        : QidList .
  var QS QS'    : QidSet .
  var S S'      : Sort .
  var SS        : SortSet .
  var SSDS      : SubsortDeclSet .
  var St        : String .
  var NeTL      : NeTermList .
  var T         : Term .
  var Tp Tp'    : Type .
  var TpL TpL'  : TypeList .
  var TpS       : TypeSet .
  var TSM  TSM' : TermStateMap .
  var TL        : TermList .
  var V         : Variable .

  --- Returns the name of the tree sort for kind in the automaton.
  op tree-name : Kind -> String .
  eq tree-name(K) = kind-name(K) + "Tree" .

  op tree-sort : Kind -> Sort .
  eq tree-sort(K) = qid(tree-name(K)) .

  op tree-sorts : TypeList ~> TypeList .
  eq tree-sorts(K TpL) = tree-sort(K) tree-sorts(TpL) .
  eq tree-sorts(nil) = nil .

  --- Returns a variable with a name "X"N with the tree sort for kind.
  op tree-var : Kind Nat -> Variable .
  eq tree-var(K, N) = qid("X" + string(N, 10) + ":" + tree-name(K)) .

  op tree-constant : Module Qid Type -> Constant .
  eq tree-constant(M, Q, Tp)
   = qid(string(Q) + "." + tree-name(getKind(M, Tp))) .

  --- Returns the equational axioms in a set of attributes.
  op axioms : Module AttrSet -> AttrSet .
  eq axioms(M, assoc AS) = assoc axioms(M, AS) .
  eq axioms(M, comm AS) = comm axioms(M, AS) .
  eq axioms(M, id(C) AS)
   = id(tree-constant(M, getName(C), getType(C))) axioms(M, AS) .
  eq axioms(M, left-id(C) AS)
   = left-id(tree-constant(M, getName(C), getType(C))) axioms(M, AS) .
  eq axioms(M, right-id(C) AS)
   = right-id(tree-constant(M, getName(C), getType(C))) axioms(M, AS) .
  eq axioms(M, AS) = none [owise].

  op lit-name : Kind ~> String .
  eq lit-name(K) = kind-name(K) + "Lit" .

  op state-sort : Kind ~> Sort .
  eq state-sort(K) = qid(state-name(K)) .

  op lit-sort : Kind ~> Sort .
  eq lit-sort(K) = qid(lit-name(K)) .

  op lit-set-name : Kind ~> String .
  eq lit-set-name(K) = kind-name(K) + "LitSet" .

  op lit-set-sort : Kind ~> Sort .
  eq lit-set-sort(K) = qid(lit-set-name(K)) .

  op lit-set-var : String Kind ~> Variable .
  eq lit-set-var(St, K) = qid(St + ":" + lit-set-name(K)) .

  --- Returns the constructor automaton states for all types in list.
  op ctor-state-list : Module TypeList ~> QidList .
  eq ctor-state-list(M, Tp TpL)
   = ctor-state(M, Tp) ctor-state-list(M, TpL) .
  eq ctor-state-list(M, nil) = nil .

  op kind-state-list : Module TypeList ~> QidList .
  eq kind-state-list(M, Tp TpL)
   = kind-state(M, Tp) kind-state-list(M, TpL) .
  eq kind-state-list(M, nil) = nil .

  op term-state-list : Module TermStateMap TermList ~> QidList .
  eq term-state-list(M, TSM, (T, TL)) 
   = term-state(M, TSM, T) term-state-list(M, TSM, TL) .
  eq term-state-list(M, TSM, empty) = nil .

  op sca-sorts : KindSet -> SortSet .
  eq sca-sorts(K ; KS) 
   = tree-sort(K) ; state-sort(K) ; lit-sort(K) ; lit-set-sort(K) ;
     sca-sorts(KS) .
  eq sca-sorts(none) = none .

  op sca-subsorts : KindSet -> SubsortDeclSet .
  eq sca-subsorts(K ; KS)
   = (subsort state-sort(K) < lit-sort(K) .)
     (subsort   lit-sort(K) < lit-set-sort(K) .)
     sca-subsorts(KS) .
  eq sca-subsorts(none) = none .

  --- Returns the operator declarations for each kind.
  op sca-kind-ops : KindSet -> OpDeclSet .
  eq sca-kind-ops(K ; KS)
   = (op '_:_ : tree-sort(K) state-sort(K) -> tree-sort(K) [ctor frozen(1)].)
     (op '!_ : state-sort(K) -> lit-sort(K) [ctor].)
     (op 'none : nil -> lit-set-sort(K) [ctor].)
     (op '_;_ : lit-set-sort(K) lit-set-sort(K) -> lit-set-sort(K)
         [ctor assoc comm id(qid("none." + lit-set-name(K)))].)
     (op 'accept : lit-set-sort(K) -> '`[Bool`] [none].)
     sca-kind-ops(KS) .
  eq sca-kind-ops(none) = none .

  --- Returns the operator declartion for each operator in the set.
  op sca-op-decls : Module OpDeclSet ~> OpDeclSet .
  eq sca-op-decls(M, (op Q : TpL -> Tp [AS].) Ops)
   = (op Q : tree-sorts(get-kinds(M, TpL)) -> tree-sort(getKind(M, Tp)) 
         [ctor axioms(M, AS)].)
     sca-op-decls(M, Ops) .
  eq sca-op-decls(M, none) = none .

  op sca-state-decl : Constant -> OpDecl .
  eq sca-state-decl(C)
   = (op getName(C) : nil -> getType(C) [ctor].) .

  --- Returns a set of state operator declarations given a list of constant
  --- states.
  op sca-state-decls : QidList ~> OpDeclSet .
  eq sca-state-decls(C QL) = sca-state-decl(C) sca-state-decls(QL) .
  eq sca-state-decls(nil) = none .

  op sca-kind-state-decls : Module TypeSet ~> OpDeclSet .
  eq sca-kind-state-decls(M, Tp ; TpS)
   = sca-state-decl(kind-state(M, Tp))
     sca-state-decl(red-state(M, Tp))
     sca-kind-state-decls(M, TpS) .
  eq sca-kind-state-decls(M, none) = none .
  
  op sca-sort-state-decls : Module TypeSet ~> OpDeclSet .
  eq sca-sort-state-decls(M, Tp ; TpS)
   = sca-state-decl(ctor-state(M, Tp))
     sca-state-decl( def-state(M, Tp))
     sca-sort-state-decls(M, TpS) .
  eq sca-sort-state-decls(M, none) = none .

  op sca-term-state-decls : Module TermStateMap ~> OpDeclSet .
  eq sca-term-state-decls(M, TSM)
   = sca-state-decls(term-states(M, TSM, 0)) .

  --- Returns the equations for the accept operation given the sorts in
  --- the specification.
  op sca-accept-eqs : Module SortSet -> EquationSet .
  eq sca-accept-eqs(M, S ; SS) 
   = (eq 'accept['_;_['!_[red-state(M, S)],
                      '!_[ctor-state(M, S)],
                      def-state(M, S),
                      lit-set-var("X", getKind(M, S))]]
       = 'true.Bool [none].)
     sca-accept-eqs(M, SS) .
  eq sca-accept-eqs(M, none) = none .

  op varStateList : TypeList QidList Nat ~> TermList .
  eq varStateList(K TpL, C C' CL, N)
   = (varStateList(K, C, N), varStateList(TpL, C' CL, N)) .
  eq varStateList(K, C, N) = '_:_[tree-var(K, N), C] .

  op varList : TypeList Nat ~> TermList .
  eq varList(K K' TpL, N) = (tree-var(K, N), varList(K' TpL, N)) .
  eq varList(K, N) = tree-var(K, N) .

  --- Returns a tree automata rule, given the qid of the operator, it's
  --- input kinds, and its output type, along with a list of constants in a
  --- QidList for the lhs and the result kind.
  op sca-rule : Module Qid TypeList Type QidList Constant ~> Rule .
  eq sca-rule(M, Q, TpL, Tp, CL, C)
   = if TpL == nil then
       (rl tree-constant(M, Q, Tp)
           => '_:_[tree-constant(M, Q, Tp), C] [none].)
     else
       (rl Q[varStateList(get-kinds(M, TpL), CL, 0)]
        => '_:_[Q[varList(get-kinds(M, TpL), 0)], C] [none].)
     fi .

  --- Returns the rules generated by subsort declarations in the
  --- specification.
  op sca-subsort-rules : Module SubsortDeclSet ~> RuleSet .
  eq sca-subsort-rules(M, (subsort S < S' .) SSDS)
   = (rl ctor-state(M, S) => ctor-state(M, S') [none].)
     sca-subsort-rules(M, SSDS) .
  eq sca-subsort-rules(M, none) = none .

  --- Returns the rules to close the operator under context.
  op sca-red-rules : Module Qid TypeList TypeList Type ~> RuleSet .
  eq sca-red-rules(M, Q, TpL, Tp TpL', Tp')
   = sca-rule(M, Q, TpL Tp TpL', Tp', 
              kind-state-list(M, TpL) red-state(M, Tp)
                 kind-state-list(M, TpL'),
              red-state(M, Tp'))
     sca-red-rules(M, Q, TpL Tp, TpL', Tp') .
  eq sca-red-rules(M, Q, TpL, nil, Tp) = none .


  --- Returns the rules generated by op declarations in the specification.
  op sca-op-rules : Module OpDeclSet ~> RuleSet .
  eq sca-op-rules(M, Op Ops)
   = if output(Op) :: Sort then
       sca-rule(M,
                id(Op),
                inputs(Op),
                output(Op),
                ctor-state-list(M, inputs(Op)),
                if is-ctor(Op) then
                  ctor-state(M, output(Op))
                else
                  if is-special(Op) then
                    red-state(M, output(Op))
                  else
                    def-state(M, output(Op))
                  fi
                fi)
     else
       none
     fi
     sca-rule(M, id(Op), inputs(Op), output(Op),
              kind-state-list(M, inputs(Op)),
              kind-state(M, output(Op)))
     sca-red-rules(M, id(Op), nil, inputs(Op), output(Op))
     sca-op-rules(M, Ops) .
  eq sca-op-rules(M, none) = none .

  --- Returns rule 
  op sca-term-rule : Module TermStateMap GroundTerm Constant -> Rule .
  eq sca-term-rule(M, TSM, Q[TL], C)
   = sca-rule(M, Q, least-sort-list(M, TL), leastSort(M, Q[TL]),
              term-state-list(M, TSM, TL),
              C) .
  eq sca-term-rule(M, TSM, C', C)
   = sca-rule(M, getName(C'), nil, getType(C'), nil, C) .

  --- Returns the transitions in an sca automata for recognizing terms of a
  --- particular pattern.
  op sca-term-rules : Module TermStateMap TermStateMap ~> RuleSet .
  eq sca-term-rules(M, TSM, term(T) TSM')
   = sca-term-rule(M, TSM, T, term-state(M, TSM, T))
     sca-term-rules(M, TSM, TSM') .
  eq sca-term-rules(M, TSM, nil) = none .

  --- Adds subterms appearing the lhs of memberships to term state map.
  op sca-mb-statemap : Module MembAxSet TermStateMap -> TermStateMap .
  ceq sca-mb-statemap(M, Mb Mbs, TSM) =
      sca-mb-statemap(M, Mbs, register-term(M, TL, TSM))
   if Q[TL] := lhs(Mb) .
  eq sca-mb-statemap(M, Mbs, TSM) = TSM [owise].

  --- Adds subterms appearing in the lhs of equations to term state map.
  op sca-eq-statemap : Module EquationSet TermStateMap -> TermStateMap .
  ceq sca-eq-statemap(M, Eq Eqs, TSM) =
      sca-eq-statemap(M, Eqs, register-term(M, TL, TSM))
   if Q[TL] := lhs(Eq) .
  eq sca-eq-statemap(M, Eqs, TSM) = TSM [owise].

  op sca-mb-rules : Module TermStateMap MembAxSet ~> RuleSet .
  eq sca-mb-rules(M, TSM, Mb Mbs)
   = if lhs(Mb) :: Variable then
       sca-subsort-rules(M, (subsort getType(lhs(Mb)) < rhs(Mb) .))
     else
       sca-term-rule(M, TSM, lhs(Mb),
                     if is-ctor(Mb) then
                       ctor-state(M, rhs(Mb))
                     else
                       def-state(M, rhs(Mb))
                     fi)
     fi
     sca-mb-rules(M, TSM, Mbs) .
  eq sca-mb-rules(M, TSM, none) = none .

  --- Returns rules for each equation.
  op sca-eq-rules : Module TermStateMap EquationSet -> RuleSet .
  eq sca-eq-rules(M, TSM, Eq Eqs)
   = sca-term-rule(M, TSM, lhs(Eq), red-state(M, leastSort(M, lhs(Eq))))
     sca-eq-rules(M, TSM, Eqs) .
  eq sca-eq-rules(M, TSM, none) = none .

  --- Removes operators from consideration that have "Universal" inputs or
  --- outputs.
  op remove-universal-ops : OpDeclSet -> OpDeclSet .
  ceq remove-universal-ops(Op Ops) = remove-universal-ops(Ops)
   if in-list('Universal, inputs(Op)) or (output(Op) == 'Universal) .
  eq remove-universal-ops(Ops) = Ops [owise].

  op sca : Module ~> Module .
  ceq sca(M)
    = (mod qid(string(getName(M)) + "-STA") is
         protecting 'BOOL .
         sorts sca-sorts(getKinds(M)) .
         sca-subsorts(getKinds(M))
         sca-kind-ops(getKinds(M))
         sca-op-decls(M, remove-universal-ops(get-ops(M, true)))
         sca-kind-state-decls(M, getKinds(M))
         sca-sort-state-decls(M, get-sorts(M, true))
         sca-term-state-decls(M, TSM)
         (none).MembAxSet
         sca-accept-eqs(M, get-sorts(M, true))
         sca-subsort-rules(M, get-subsorts(M, true))
         sca-term-rules(M, TSM, TSM)
         sca-op-rules(M, remove-universal-ops(get-ops(M, true)))
         sca-mb-rules(M, TSM, get-mbs(M, true))
         sca-eq-rules(M, TSM, get-eqs(M, true))
       endm)
   if TSM := sca-eq-statemap(M, get-eqs(M, true),
               sca-mb-statemap(M, get-mbs(M, true), nil)) .

  --- Converts a term in the tree automaton representation back to the
  --- original module representation. 
  op scc-parse : GroundTermList ~> GroundTermList .
  eq scc-parse((T, NeTL)) = scc-parse(T), scc-parse(NeTL) .
  eq scc-parse(Q[TL]) = Q[scc-parse(TL)] .
  eq scc-parse(C) = qid(substr(string(C), 0, length(string(C)) + -4)) .

  --- Converts a constant for a "defined" state into a constant for a
  --- "constructor" state.
  op to-ctor : Constant -> Constant .
  eq to-ctor(C) 
   = qid("c" + substr(string(C), 1, length(string(C)))) .

  --- Searches for a constant identifying a defined symbol in the first
  --- qid set for which the constructor state is not in the second set.
  --- Returns anytype if not found.
  op scc-parse : NeQidSet QidSet ~> Sort . 
  eq scc-parse(C ; QS, QS') 
   = if (substr(string(C), 0, 1) == "d")
             and not (to-ctor(C) in QS') then
       qid(substr(string(C), 1,
         _-_(rfind(string(C), ".", length(string(C))), 1)))
     else
       scc-parse(QS, QS')
     fi .

  op scc-result : EmptinessResult -> SCCResult .
  eq scc-result(empty) = complete .
  eq scc-result(accepting(T, QS))
   = counterexample(scc-parse(T), scc-parse(QS, QS)) .
  eq scc-result(invalid-input) = invalid-input .

  sort SCCResult .
  op complete : -> SCCResult [ctor].
  op counterexample : Term Sort -> SCCResult [ctor].
  op invalid-input : -> SCCResult [ctor].

  --- Checks the sufficient completeness of a module.
  op scc : Module ~> SCCResult .
  eq scc(M)
   = if wellFormed(M) then
       scc-result(test-emptiness(sca(M)))
     else
       invalid-input
     fi .

endfm

--- Provides operations for checking a module to see if it does not satisfy
--- the requirements of the sufficient completeness checker.
fmod SCC-CHECKER is
  pr SCC .

  var AS : AttrSet .
  var Cond : EqCondition .
  var Eq : Equation .
  var Eqs : EquationSet .
  var GT : GroundTerm .
  var M : Module .
  var Mb : MembAx .
  var Mbs : MembAxSet .
  var Ops : OpDeclSet .
  var NL : NatList .
  var Q : Qid .
  var QL : QidList .
  var QS : QidSet .
  var S : Sort .
  var T T' : Term .
  var TL TL' : TermList .
  var Tp : Type .
  var TpL : TypeList .
  var V : Variable .

  op warning : QidList -> QidList .
  eq warning(QL) = '\! '\y 'Warning: '\o QL '\n .

  --- Checks for attributes that are not compatible with scc. The QidList
  --- refers to the operator name.
  op check-attrs : AttrSet QidList ~> QidList .
  eq check-attrs(strat(NL) AS, QL)
   = warning('Ignoring 'strategy 'for QL '.)
     check-attrs(AS, QL) .
  eq check-attrs(idem AS, QL)
   = warning('Ignoring 'idempotence 'for QL '.)
     check-attrs(AS, QL) .
  eq check-attrs(AS, QL) = nil [owise].

  --- Checks that operators have attributes that are compatible with scc.
  op check-ops : OpDeclSet ~> QidList .
  eq check-ops((op Q : TpL -> Tp[AS].) Ops) 
   = check-attrs(AS, Q ': TpL '-> Tp)
     check-ops(Ops) .
  eq check-ops(none) = nil .

  --- Returns true if term is linear and variables in set do not overlap
  --- given set.
  op non-overlapping? : Module TermList QidSet -> Bool .
  eq non-overlapping?(M, (GT, TL), QS) 
   = non-overlapping?(M, TL, QS) .
  eq non-overlapping?(M, (Q[TL], TL'), QS)
   = non-overlapping?(M, (TL, TL'), QS) .
  eq non-overlapping?(M, (V, TL), QS)
   = if canonize(M, V) in QS then
       false
     else
       non-overlapping?(M, TL, canonize(M, V) ; QS)
     fi .
  eq non-overlapping?(M, empty, QS) = true .

  --- Returns true if a membership in set is conditional.
  op has-condition? : MembAxSet -> Bool .
  eq has-condition?((cmb T : S if Cond [AS].) Mbs) = true .
  eq has-condition?(Mbs) = false [owise].

  --- Returns true if all memberships in set are left-linear.
  op left-linear? : Module MembAxSet -> Bool .
  eq left-linear?(M, Mb Mbs)
   = non-overlapping?(M, lhs(Mb), none) and left-linear?(M, Mbs) .
  eq left-linear?(M, (none).MembAxSet) = true .

  --- Checks that memberships are left-linear and unconditional.
  op check-mbs : Module MembAxSet ~> QidList .
  eq check-mbs(M, Mbs)
   = if has-condition?(Mbs) then
       warning('This 'module 'has 'conditional 'memberships. 'The 'sufficient
         'completeness 'checker 'will 'treat 'these 'as 'unconditional.)
     else
       nil
     fi
     if not left-linear?(M, Mbs) then
      warning('This 'module 'has 'memberships 'that 'are 'not 'left-linear.
        'The 'sufficient 'completeness 'checker 'will 'rename 'variables 'as
        'needed 'to 'drop 'the 'non-linearity 'conditions.)
     else
       nil
     fi .

  --- Returns true if a equation in set is conditional.
  op has-condition? : EquationSet -> Bool .
  eq has-condition?((ceq T = T' if Cond [AS].) Eqs) = true .
  eq has-condition?(Eqs) = false [owise].

  --- Returns true if all memberships in set are left-linear.
  op left-linear? : Module EquationSet -> Bool .
  eq left-linear?(M, Eq Eqs)
   = non-overlapping?(M, lhs(Eq), none) and left-linear?(M, Eqs) .
  eq left-linear?(M, (none).EquationSet) = true .

  --- Checks that equations are left-linear and unconditional.
  op check-eqs : Module EquationSet ~> QidList .
  eq check-eqs(M, Eqs)
   = if has-condition?(Eqs) then
       warning('This 'module 'has 'conditional 'equations. 'The 'sufficient
         'completeness 'checker 'will 'treat 'these 'as 'unconditional.)
     else
       nil
     fi
     if not left-linear?(M, Eqs) then
      warning('This 'module 'has 'equations 'that 'are 'not 'left-linear.
        'The 'sufficient 'completeness 'checker 'will 'rename 'variables 'as
        'needed 'to 'drop 'the 'non-linearity 'conditions.)
     else
       nil
     fi .

  --- Checks a module for ways in which it does not satisfy the requirements
  --- of the sufficient completeness checker.
  op check-module : Module ~> QidList .
  eq check-module(M)
   = check-ops(get-ops(M, true))
     check-mbs(M, get-mbs(M, true))
     check-eqs(M, get-eqs(M, true)) .
endfm

fmod SCC-GRAMMAR is
  pr QID .
  sorts Input Token .
  op token : Qid -> Token 
               [ctor
                special (
                 id-hook Bubble (1 1)
                 op-hook qidSymbol (<Qids> : ~> Qid))] .
  op scc_. : Token -> Input [ctor].
endfm

mod SCC-LOOP is
  pr SCC .
  pr SCC-CHECKER .
  inc LOOP-MODE .

  op scc : -> State [ctor].
  
  var C : Constant .
  var M : Module .
  var N : Nat .
  var Q : Qid .
  var QL : QidList .
  var NeQL : NeQidList .
  var RP RP' : ResultPair .
  var S : Sort .
  var T T' : Term .
  var Tp : Type .

  op get-module-name : Constant ~> Qid .
  eq get-module-name(C)
   = qid(substr(string(C), 1,
                rfind(string(C), ".", length(string(C))) + -1)) .

  --- Returns the qid at the given index or nil if the integer is greater 
  --- than the lenght of the list.
  op at : Nat QidList ~> Qid .
  eq at(0, Q QL) = Q .
  eq at(s N, Q QL) = at(N, QL) .
  eq at(N, QL) = nil [owise]. 

  op error : QidList -> QidList .
  eq error(QL) = '\! '\r 'ERROR: '\o QL .
  
  op scan-result : Module SCCResult -> QidList .
  eq scan-result(M, complete) 
   = '\! '\g 'Success: '\o getName(M) 'is 'sufficiently 'complete 'under 'the
     'assumption 'that 'it 'is 'weakly-normalizing '`, ' 'confluent '`, '
     'and 'sort-decreasing. .
  eq scan-result(M, counterexample(T, S))
   = '\! '\r 'Failure: '\o 'The 'term '\m metaPrettyPrint(M, T, mixfix) '\o
     'is 'a 'counterexample 'as 'it 'is 'a 'irreducible 'term 'with 'sort
     '\m S '\o 'in '\c getName(M) '\o 'that 'does 'not 'have 'sort '\m S '\o
     'in 'the 'constructor 'subsignature. .
  eq scan-result(M, invalid-input) 
   = error('Could 'not 'parse 'module.) .

  op scan-parse : QidList ResultPair? -> QidList .
  eq scan-parse(QL, {'scc_.['token[C]], Tp})  
   = 'Checking 'sufficient 'completeness 'of '\c get-module-name(C) '\o
     '... '\n
     if upModule(get-module-name(C), true) :: Module then
       check-module(upModule(get-module-name(C), true))
       scan-result(upModule(get-module-name(C), true),
                   scc(upModule(get-module-name(C), true)))
     else
       error('The 'module get-module-name(C) 'could 'not 'be 'found.)
     fi .
  eq scan-parse(QL, noParse(N)) 
   = error(
     if size(QL) <= N then
       'Unexpected 'end 'of 'command.
       if (size(QL) > 0) and last(QL) =/= '. then
         'Perhaps 'a 'terminating 'period 'was 'omitted?
       else
         nil
       fi
     else
       'The 'command 'could 'not 'be 'parsed '-- 'starting 'with 'the
       'word at(N, QL) '.
     fi) .
     
  eq scan-parse(QL, ambiguity(RP, RP')) 
   = 'ERROR: 'The 'command 'is 'ambiguous. .

  op init-scc : -> System [ctor].
  rl [init] :
     init-scc
     =>
     [nil, scc, 'Starting 'the 'Maude 'Sufficient 'Completeness 'Checker.] .

  rl [check] :
    [NeQL, scc, nil] 
    =>
    [nil, scc, scan-parse(NeQL, metaParse(['SCC-GRAMMAR], NeQL, 'Input))] .
endm

loop init-scc .

---a set include BOOL off .
---a fmod TEST is
---a   sort S .
---a   op a : -> S .
---a   op f : S -> S .
---a endfm
---a 
---a select SCC-LOOP .
---a (scc TEST .)
---a (scc QID .)

---a time: (scc META-LEVEL .) = 8.18 seconds