mgci.maude

--- name: mgci.maude
--- desc: This module has methods such that, given a module
---       without memberships and where no sorts have
---       a reserved name, it will compute the constructor
---       sort refinement of that module according to the
---       definition sketched in "Metalevel algorithms for
---       Variant Satisfiability."
---
---       This module also contains functionality to take
---       a term in the extended signature and convert it
---       into one in the original signature---and then
---       lifts operation to substitutions.

fmod CTOR-REFINE is
  pr META-LEVEL .
  pr KIND-CHECK .    --- for kind checks
  pr UNIT-FM .       --- for module operations
  pr UNIQUE-PREFIX . --- to generate unique prefixes for sorts

  op ctor-refine    : Module ~> Module [memo] .
  op $ctor-refine   : Module ~> Module .
  op ctor-sort      : Module Sort -> Sort .
  op ctor-sort      : Module SortSet -> SortSet .
  op ctor-subsorts1 : Module SortSet -> SubsortDeclSet .
  op ctor-subsorts2 : Module SubsortDeclSet -> SubsortDeclSet .
  --- these operators are partial because they might fail
  --- due to the presence of kinds; that is why the kind
  --- check is performed in the initial call ctor-refine()
  op ctor-sort      : Module TypeListSet ~> TypeListSet .
  op ctor-ops       : Module OpDeclSet ~> OpDeclSet .
  ---
  op ctor-term      : Module TermList -> TermList .
  op ctor-term      : Module OpDeclSet TermList -> TermList .
  op has-ctr-const  : OpDeclSet Qid Sort -> Bool .

  var M   : Module .
  var X Y : Sort .
  var S   : SortSet .
  var Q   : Qid .
  var LS  : TypeListSet .
  var AS  : AttrSet .
  var L L'  : TypeList .
  var O O' : OpDecl .
  var OS : OpDeclSet .
  var DS : SubsortDeclSet .
  var T : Term .
  var TL : NeTermList .
  var V : Variable .
  var C : Constant .

  ceq ctor-refine(M) = $ctor-refine(M)
  if not kinds?(M,true,getOps(M))
  /\ getMbs(M) == none .

  eq $ctor-refine(M) =
    addOps(ctor-ops(M,getOps(M)),
      addSubsorts(ctor-subsorts1(M,getSorts(M)) ctor-subsorts2(M,getSubsorts(M)),
        addSorts(ctor-sort(M,getSorts(M)),M))) .

  eq ctor-sort(M,X)           = qid(sortPrefix(M) + string(X)) .
  eq ctor-sort(M,X L)         = ctor-sort(M,X) ctor-sort(M,L) .
  eq ctor-sort(M,nil)         = nil .
  eq ctor-sort(M,L ; L' ; LS) = ctor-sort(M,L) ; ctor-sort(M,L' ; LS) .
  eq ctor-sort(M,none)        = none .

  eq ctor-subsorts1(M,X ; S)  = subsort ctor-sort(M,X) < X . ctor-subsorts1(M,S) .
  eq ctor-subsorts1(M,none)   = none .

  eq ctor-subsorts2(M,subsort X < Y . DS) =
    subsort ctor-sort(M,X) < ctor-sort(M,Y) . ctor-subsorts2(M,DS) .
  eq ctor-subsorts2(M,none) = none .

  eq ctor-ops(M,op Q : L -> X [ctor AS].) =
    op Q : ctor-sort(M,L) -> ctor-sort(M,X) [ctor AS]. .
  eq ctor-ops(M,O) = O [owise] .
  eq ctor-ops(M,O O' OS) = ctor-ops(M,O) ctor-ops(M,O' OS) .
  eq ctor-ops(M,none) = none .

  eq ctor-term(M,T) = ctor-term(M,getOps(M),T) .
  eq ctor-term(M,OS,V) = qid(string(getName(V)) + ":" + string(ctor-sort(M,getType(V)))) .
  eq ctor-term(M,OS,C) =
    if has-ctr-const(OS,getName(C),getType(C)) then
      qid(string(getName(C)) + "." + string(ctor-sort(M,getType(C))))
    else
      C
    fi .
  eq ctor-term(M,OS,Q[TL])  = Q[ctor-term(M,OS,TL)] .
  eq ctor-term(M,OS,(T,TL)) = ctor-term(M,OS,T), ctor-term(M,OS,TL) .
  eq ctor-term(M,OS,empty)  = empty .

  eq has-ctr-const(op Q : nil -> X [ctor AS]. OS,Q,X) = true .
  eq has-ctr-const(OS,Q,X) = false [owise] .
endfm

fmod CTOR-LIFT is
  pr META-LEVEL .
  pr QID-JOIN .
  pr SUBSTITUTIONSET .
  pr UNIQUE-PREFIX .

  op lift-sort : Module Sort -> Sort .
  op lift-sort : Module String -> Sort .
  op lift-term : Module TermList -> TermList .
  op lift-sub  : Module SubstitutionSet -> SubstitutionSet .

  var M : Module .
  var S : Sort .
  var R : String .
  var C : Constant .
  var V : Variable .
  var Q : Qid .
  var T : Term .
  var L : NeTermList .
  var B B' : Substitution .
  var BS : SubstitutionSet .

  eq lift-sort(M,S)     = lift-sort(M,string(S)) .
  eq lift-sort(M,R)     = qid(if substr(R,0,length(sortPrefix(M))) == sortPrefix(M) then substr(R,length(sortPrefix(M)),length(R)) else R fi) .

  eq lift-term(M,C)     = join(getName(C) '. lift-sort(M,getType(C))) .
  eq lift-term(M,V)     = join(getName(V) ': lift-sort(M,getType(V))) .
  eq lift-term(M,Q[L])  = Q[lift-term(M,L)] .
  eq lift-term(M,(T,L)) = lift-term(M,T), lift-term(M,L) .
  eq lift-term(M,empty) = empty .

  eq lift-sub(M,V <- T ; B)  = lift-term(M,V) <- lift-term(M,T) ; lift-sub(M,B) .
  eq lift-sub(M,none)        = none .
  eq lift-sub(M,B | B' | BS) = lift-sub(M,B) | lift-sub(M,B' | BS) .
  eq lift-sub(M,empty)       = empty .
endfm

--- this module computes most general constructor instances;
--- since this module relies on ctor-refine, the module to be
--- analyzed should make any use of kinds!
fmod MGCI is
  pr META-LEVEL .
  pr CTOR-REFINE .
  pr CTOR-LIFT .
  pr QID-JOIN .
  pr TERMSET-FM .
  pr SUBSTITUTIONSET .
  pr SUBSTITUTIONSETPAIR .
  pr SUBSTITUTION-REFINEMENT .

  var M CM : Module .
  var I J N : Nat .
  var S S' S1 S2 : Substitution .
  var SS : SubstitutionSet .
  var T : Term .
  var UP : UnificationProblem .
  var V : Variable .

  --- OUT: generate a set of most general constructor instances
  ---      where there are no bad variables in the initial term
  op mgci : Module Term -> SubstitutionSet .
  eq mgci(M,T) = mgci(M,T,0) .

  --- OUT: generate a set of most general constructor instances
  ---      where Nat is greater than the index of all bad variables
  ---      inside of the term to be analyzed
  op mgci : Module Term Nat -> SubstitutionSet .
  eq mgci(M,T,I) = $mgci(M,ctor-refine(M),T =? join('X ': ctor-sort(M,leastSort(M,T))),I) .

  --- PRE: [1] CM is the constructor refinement of M
  ---      [2] UP is a unification problem in the signature CM
  --- OUT: the solutions of the unification problem in CM lifted up
  ---      into corresponding substitutions in M
  op $mgci : Module Module UnificationProblem Nat -> SubstitutionSet .
  eq $mgci(M,CM,UP,I) = $mgci(M,CM,UP,0,metaDisjointUnify(CM,UP,I,0),empty) .

  ---  NB: this implements the function above, looping over each
  ---      generated unifier in the signature in CM
  op $mgci : Module Module UnificationProblem Nat UnificationTriple SubstitutionSet -> SubstitutionSet .
  eq $mgci(M,CM,UP,N,noUnifier,SS) = lift-sub(M,SS) .
  eq $mgci(M,CM,UP,N,{S,S',I},SS)  = $mgci(M,CM,UP,s(N),metaDisjointUnify(CM,UP,s(I),s(N)),SS | S) .

  --- OUT: return true iff the term is a constructor term
  op ctor-term? : Module Term -> [Bool] .
  eq ctor-term?(M,T) = $ctor-term?(ctor-term-witness(M,T)) .

  op $ctor-term? : Substitution? ~> Bool .
  eq $ctor-term?(S) = true .
  eq $ctor-term?(noMatch) = false .

  op ctor-term-witness : Module Term -> [Substitution?] .
  eq ctor-term-witness(M,T) =
    if wellFormed(ctor-refine(M))
      then metaMatch(ctor-refine(M),
                     join('X ': ctor-sort(M,leastSort(M,T))),
                     ctor-term(M,T),
                     nil,
                     0)
      else errsub('Constructor 'Module 'Refinement 'Failed)
    fi .

  --- OUT: a SubstitutionSetPair where the constructor assignments
  ---      are in the first slot, and the non-constructors are in the
  ---      second slot
  op ctor-split-sub : Module Substitution ~> SubstitutionPair .
  eq ctor-split-sub(M,S) = ctor-split-sub(M,S,none,none) .

  op ctor-split-sub : Module Substitution Substitution Substitution -> SubstitutionPair .
  eq ctor-split-sub(M,V <- T ; S,S1,S2) = if ctor-term?(M,T)
                                            then ctor-split-sub(M,S,V <- T ; S1,S2)
                                            else ctor-split-sub(M,S,S1,V <- T ; S2)
                                          fi .
  eq ctor-split-sub(M,none,S1,S2) = (S1,S2) .

  --- OUT: return the subset of a substitution that is constructor terms
  op ctor-sub : Module Substitution -> Substitution .
  eq ctor-sub(M,S) = p1(ctor-split-sub(M,S)) .

  --- OUT: return true iff a substitution is only constructor terms
  op ctor-sub? : Module Substitution -> Bool .
  eq ctor-sub?(M,S) = p2(ctor-split-sub(M,S)) == none .
endfm

--- this module uses functionality above to compute defined subterms of terms
fmod DEFINED-SUBTERMS is
  pr META-LEVEL .
  pr MGCI .         --- used to find ctor subterms
  pr GEN-VARNAMES . --- used to generate fresh variables
  pr QID-JOIN .

  --- used for term abstraction
  sort AbstractionData .
  op ((_,_,_)) : Nat Term Substitution -> AbstractionData [ctor] .

  op  defined-abs : Module Term -> AbstractionData .
  op $dabs        : Module AbstractionData -> AbstractionData .
  op $dabsL       : Module Qid AbstractionData TermList TermList -> AbstractionData .
  op $bind        : Nat Module Term Substitution -> AbstractionData .
  op $bind        : Nat Variable Term Substitution -> AbstractionData .
  op tl2Vars      : Module TermList -> TermList .

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

  --- INP: Module Term
  --- PRE: Term is well-defined in Module
  --- OUT: AbstractionData (Nat,Term,Substitution) where
  ---      all minimal defined subterms have been extracted
  ---      and replaced by tmp variables; the substitution
  ---      maps each new tmp variable to its original removed subterm
  eq  defined-abs(M,T)      = $dabs(M,(0,T,none)) .
  eq $dabs(M,(N,V,S))       =  (N,V,S) .
  eq $dabs(M,(N,C,S))       =  if N == 0 and-then not ctor-term?(M,C) then $bind(N,M,C,S) else (N,C,S) fi .
  eq $dabs(M,(N,Q[(T,TL)],S)) =
        if not ctor-term?(M,Q[tl2Vars(M,(T,TL))]) then
          $bind(N,M,Q[(T,TL)],S)
        else
          $dabsL(M,Q,$dabs(M,(N,T,S)),TL,empty)
        fi .
  eq $dabsL(M,Q,(N,T,S),(T',TL),TL') = $dabsL(M,Q,$dabs(M,(N,T',S)),TL,(TL',T)) .
  eq $dabsL(M,Q,(N,T,S),empty,TL')   = (N,Q[TL',T],S) .

  eq $bind(N,M,T,S) = $bind(N,tmpvar(N,M,T),T,S) .
  eq $bind(N,V,T,S) = (s(N),V,V <- T ; S) .

  eq  tl2Vars(M,(T,TL)) = join('X: leastSort(M,T)),tl2Vars(M,TL) .
  eq  tl2Vars(M,empty)  = empty .
endfm