Skip to content

Latest commit

 

History

History
416 lines (321 loc) · 16.6 KB

intersection.md

File metadata and controls

416 lines (321 loc) · 16.6 KB
Raw

Module Intersection

This module computes module intersections over ModuleDeclSet. The intersection operation is lifted to Module via asTemplate.

load module-template.maude
load constrained-terms.maude

fmod INTERSECTION is
  protecting MODULE-TEMPLATE * ( op _;;_ to _;;;_ ) .
  protecting RENAMING-EXPR-EVALUATION .

  var B : Bool . vars TL : TypeList . var T : Type . var AS : AttrSet .
  var OPD : OpDecl . var OPDS : OpDeclSet .
  vars MOD MOD' M0 : Module . vars ME ME' : ModuleExpression .
  vars Q Q' : Qid . vars H H' : Header . vars S S' : Sort . vars SS SS' : SortSet .
  vars NeMDS NeMDS' : NeModuleDeclSet . vars MDS MDS' MDS'' : ModuleDeclSet .
  
  var EqC : EqConj . var TM : Term . var TM? : [Term] . vars TML? TML?' : [TermList] .

  op intersect : ModuleDeclSet ModuleDeclSet -> ModuleDeclSet [assoc comm id: none] .
  -----------------------------------------------------------------------------------
  eq intersect( NeMDS     , NeMDS' )     = none [owise] .
  eq intersect( NeMDS MDS , NeMDS MDS' ) = NeMDS intersect( MDS , MDS' ) .
  eq intersect( (sorts S ; SS .) MDS , (sorts S ; SS' .) MDS' )
   = (sorts S .) intersect( (sorts SS .) MDS , (sorts SS' .) MDS' ) .

  op intersect : Module Module -> Module .
  ----------------------------------------
  eq intersect(MOD, MOD') = fromTemplate(resolveNames(getName(MOD) /\ getName(MOD')), intersect(asTemplate(MOD), asTemplate(MOD'))) .
  eq upModule(H /\ H', B) = intersect(upModule(H, B), upModule(H', B)) .

It will often be useful to know if a sort or an operator is in a ModuleDeclSet.

  op _inS_ : Sort ModuleDeclSet -> Bool .
  op _inO_ : Qid  ModuleDeclSet -> Bool .
  --------------------------------------
  eq S inS ( sorts SS . )            MDS = S in SS .
  eq Q inO ( op Q : TL -> T [AS] . ) MDS = true .
  eq S inS MDS = false [owise] .
  eq Q inO MDS = false [owise] .

When purifying we'll generate extra constraints we want to bubble to the top. Allowing QF equality atoms to bubble to the top is safe.

  op _?=_ : CTerm CTerm -> EqConj [ditto] .
  op _!=_ : CTerm CTerm -> EqConj [ditto] .
  -----------------------------------------
  eq TM? ?= (TM | EqC)          = (TM? ?= TM) /\ EqC .
  eq TM? != (TM | EqC)          = (TM? != TM) /\ EqC .
  eq Q[TML?, (TM | EqC), TML?'] = Q[TML?, TM, TML?'] | EqC .

Joint Sorts

Calculating the joint sort of a sort S in connected components C1 and C2 corresponding to modules MOD and MOD':

  • If S is a sort of C1 /\ C2, return S;
  • If not, return the maximal sort in C1 /\ C2.

Right now we just take any maximal sort in C1 /\ C2, but we really need to take the correct maximal sort.

  op joint-sort : Sort ModuleDeclSet ModuleDeclSet -> Sort .
  ----------------------------------------------------------
  ceq joint-sort(S, MDS, MDS') = S if S inS intersect(MDS, MDS') .
  ceq joint-sort(S, MDS, MDS') = joint-sort(S, MDS', MDS) if (not S inS MDS) /\ S inS MDS .
  ceq joint-sort(S, MDS, MDS') = if S inS MDS'' then S else #top-sort(MDS'') fi
                               if S inS MDS /\ MDS'' := intersect(connected-component(MDS, (sorts S .)), MDS') .

  op joint-sort : Sort Module           Module           -> Sort .
  op joint-sort : Sort ModuleExpression ModuleExpression -> Sort .
  ----------------------------------------------------------------
  eq  joint-sort(S, ME,  ME')  = joint-sort(S, upModule(ME /\ ME', true), upModule(ME /\ ME', true)) .
  eq  joint-sort(S, MOD, MOD') = joint-sort(S, asTemplate(MOD), asTemplate(MOD')) .

  op #top-sort : ModuleDeclSet -> [Sort] .
  ----------------------------------------
  eq #top-sort( ( sorts S ; SS . )   MDS ) = top-sort( ( sorts S ; SS . )   MDS , S ) .
  eq #top-sort( ( subsort S < S' . ) MDS ) = top-sort( ( subsort S < S' . ) MDS , S ) .
endfm

Deterministic Variables

Having deterministically calculated variables makes many things much simpler. This module calculates a variable for a given term by simply turning the term into a string. This guarantees that if the same term is encountered twice, the same variable will be generated.

fmod DETERMINISTIC-VARIABLES is
  protecting INTERSECTION .

  var Q : Qid . var Str : String . var S : Sort .
  vars ME ME' : ModuleExpression . vars MOD MOD' : Module . var T : Term .
  vars NeTL NeTL' : NeTermList . var TL : TermList .

  op #string : TermList -> String .
  ---------------------------------
  eq #string(Q)              = string(Q) .
  eq #string(Q[TL])          = #string(Q) + "[" + #string(TL) + "]" .  
  eq #string((NeTL , NeTL')) = #string(NeTL) + "," + #string(NeTL') .

  op #qid : TermList -> Qid .
  ---------------------------
  eq #qid(TL) = qid(#string(TL)) .

  op #makeVariable : Qid    Sort -> Variable .
  op #makeVariable : String Sort -> Variable .
  --------------------------------------------
  eq #makeVariable(Q, S)   = qid("#makeVariable(" + string(Q) + "):" + string(S)) .
  eq #makeVariable(Str, S) = qid("#makeVariable(" + Str + "):" + string(S)) .

  op joint-variable : ModuleExpression ModuleExpression Term -> Variable .
  ------------------------------------------------------------------------
  eq joint-variable(ME, ME', T) = joint-variable(upModule(ME, true), upModule(ME', true), T) .

  op joint-variable : Module Module Term -> Variable .
  ----------------------------------------------------
  ceq joint-variable(MOD, MOD', T) = #makeVariable(#string(T), joint-sort(leastSort(MOD, T),  MOD, MOD')) if wellFormed(MOD, T) .
  ceq joint-variable(MOD, MOD', T) = #makeVariable(#string(T) ,joint-sort(leastSort(MOD', T), MOD', MOD)) if wellFormed(MOD', T) .
endfm

Breaking Equalities

Breaking equality atoms means taking an equality atom between terms of different modules and reforming them:

  • T ?= T' goes to x ?= T /\ x ?= T' for x a variable of sort common to T and T'.
  • T != T' goes to x ?= T /\ x != T' for x a variable of sort greater than that T'.
fmod BREAK-EQATOMS is
    protecting DETERMINISTIC-VARIABLES .

    vars EqC EqC' : EqConj . vars MOD MOD' : Module . vars ME ME' : ModuleExpression .
    vars T T' : Term . var NV : Variable .

    op break-eqatoms : Module Module EqConj -> EqConj .
    op break-eqatoms : ModuleExpression ModuleExpression EqConj -> EqConj .
    -----------------------------------------------------------------------
    eq break-eqatoms(ME,  ME',  EqC)         = break-eqatoms(upModule(ME, true), upModule(ME', true), EqC) .
    eq break-eqatoms(MOD, MOD', EqC /\ EqC') = break-eqatoms(MOD, MOD', EqC) /\ break-eqatoms(MOD, MOD', EqC') .

    ceq break-eqatoms(MOD, MOD', T ?= T') = T ?= NV /\ T' ?= NV if not (T :: Variable or T' :: Variable)
                                                                /\ NV := joint-variable(MOD, MOD', T) .
    ceq break-eqatoms(MOD, MOD', T != T') = T ?= NV /\ T' != NV if not (T :: Variable or T' :: Variable)
                                                                /\ NV := joint-variable(MOD, MOD', T)
                                                                /\ sortLeq(MOD, leastSort(MOD, T), leastSort(MOD, NV)) .
    ceq break-eqatoms(MOD, MOD', T != T') = T ?= NV /\ T' != NV if not (T :: Variable or T' :: Variable)
                                                                /\ NV := joint-variable(MOD, MOD', T) 
                                                                /\ sortLeq(MOD', leastSort(MOD', T), leastSort(MOD', NV)) .
endfm

Variable Abstraction

Input: : One module M, and an Equational Conjunction: a conjunction of equations of the form T ?= T' and T != T'.

Output: : A new Equational Conjunction, where each Equational Atom is of the form T1 = T2, where either T1 or T2 (or both) is a variable, and the other is of the form f(V1, ..., Vn) for variables V1 through Vn.

fmod VABS is
    pr FOFORM .
    pr FOFORMSIMPLIFY-IMPL .
    pr BREAK-EQATOMS .

    vars V FV : Variable . var C : Constant . var Q : Qid . vars T T' T'' : Term .
    vars TL TL' : TermList . vars NeTL NeTL' : NeTermList . 
    var ME : ModuleExpression . var M : Module .
    var EqA : EqAtom . vars EqC EqC' : EqConj . var TA : TruthAtom .

    op vabs : ModuleExpression EqConj -> [EqConj] .
    -----------------------------------------------
    eq vabs(ME, EqC) = vabs(upModule(ME, true), EqC) .

abstracted : Term -> Bool returns true if the current is abstracted.

    op abstracted : Term -> Bool .
    ------------------------------
    eq  abstracted(T)             = true [owise] .
    ceq abstracted(Q[TL, T, TL']) = false if not (T :: Variable) .

The operation vabs : Module EqConj -> EqConj takes in an equational conjunction and variable abstracts all the equational atoms.

    op vabs : Module EqConj -> [EqConj] .
    -------------------------------------
    eq  vabs(M, EqC /\ EqC') = vabs(M, EqC) /\ vabs(M, EqC') .
    ceq vabs(M, V ?= T)      = V ?= T if abstracted(T) .
    ceq vabs(M, V != T)      = V != T if abstracted(T) .

If the top terms in the equality atom are both not variables and abstracted, then break-eqatoms is used to make it a conjunct of simple equalities.

    ceq vabs(M, T ?= T') = break-eqatoms(M, M, T ?= T') if not (T :: Variable or T' :: Variable) /\ abstracted(T) /\ abstracted(T') .
    ceq vabs(M, T != T') = break-eqatoms(M, M, T != T') if not (T :: Variable or T' :: Variable) /\ abstracted(T) /\ abstracted(T') .

If there is a non-variable subterm, it is extracted as an equality. Both the remaining subterms and the new equality are variable abstracted.

    ceq vabs(M, Q[TL, T, TL'] ?= T') = vabs(M, Q[TL, FV, TL'] ?= T') /\ vabs(M, FV ?= T) if not (T :: Variable) /\ FV := joint-variable(M, M, T) .
    ceq vabs(M, Q[TL, T, TL'] != T') = vabs(M, Q[TL, FV, TL'] != T') /\ vabs(M, FV ?= T) if not (T :: Variable) /\ FV := joint-variable(M, M, T) .
endfm

Examples

This is a sampling of the test cases in tests/test-modules.maude with a more human-readable output, using this module:

fmod TEST-MODULE is
  sorts A B .
  subsort A < B .
    
  op a : -> A .
  op b : -> B .
    
  op f : B -> A .
  ---------------
  eq f(b) = a .
endfm

reduce vabs('TEST-MODULE, 'x:A ?= 'f['a.A]) .
Output: V0 ?= a /\ x ?= f(V0)

reduce vabs('TEST-MODULE, 'f['f['a.A]] ?= 'f['b.A]) .
Output: V0 ?= a /\ V1 ?= b /\ V2 ?= f(V0) /\ V3 ?= f(V1) /\ V3 ?= f(V2)

reduce vabs('TEST-MODULE, 'f['f['a.A]] ?= 'f['a.A] /\ 'f['f['f['a.A]]] != 'f['a.A]) .
Output: V0 ?= a /\ V1 ?= f(V0) /\ V1 ?= f(V1) /\ V2 ?= f(V1) /\ V1 != V2

reduce vabs('TEST-MODULE, 'f['f['a.A]] ?= 'f['a.A] /\ 'f['f['a.A]] != 'f['a.A]) .
Output: V0 ?= a /\ V1 ?= f(V0) /\ V1 ?= f(V1) /\ V1 != f(V1)

reduce vabs('TEST-MODULE, 'f['f['a.A]] ?= 'f['a.A] /\ 'f['f'['f['x:A]]] != 'f['a.A]) .
Output: V0 ?= a /\ V1 ?= f(V0) /\ V1 ?= f(V1) /\ V2 ?= f(V3) /\ V3 ?= f(x) /\ V1 != f(V2)

reduce vabs('TEST-MODULE, 'f['b.A] ?= 'f['a.A] /\ 'f['f'['f['x:A]]] != 'f['b.A]) .
Output: V0 ?= a /\ V1 ?= b /\ V2 ?= f(V0) /\ V2 ?= f(V1)
     /\ V3 ?= f(V1) /\ V4 ?= f(V5) /\ V5 ?= f(x) /\ V3 != f(V4)

For more test cases using more complex modules, see tests/test-modules.maude.

Purification

Purification ensures that a conjunction of equational atoms has sub-conjuncts strictly formed of equational atoms from the individual theories. The resulting formulas will always be of the form

  • T ?= T' or T != T' with T and T' in the same signature.
  • x ?= T or x != T with x a variable of appropriate sort in the signature of T.
fmod PURIFICATION is
  protecting META-LEVEL .
  protecting FOFORMSIMPLIFY-IMPL .
  protecting CTERM-SET * ( op _;;_ to _;;;_ ) .
  protecting BREAK-EQATOMS .

  var Q : Qid . var TA : TruthAtom . vars EqC EqC' : EqConj . var QFF : QFForm .
  vars ME ME' : ModuleExpression . vars M M' : Module . 
  vars FV : Variable . vars T T' T1 T2 : Term . var T? : [Term] .
  vars NeTL NeTL' : NeTermList . vars TL TL' : TermList . vars TL? TL?' : [TermList] .

  op _in_ : EqConj Module -> Bool .
  ---------------------------------
  eq TA            in M = true .
  eq (EqC /\ EqC') in M = (EqC in M) and (EqC' in M) .
  eq (T ?= T')     in M = wellFormed(M, T) and wellFormed(M, T') .
  eq (T != T')     in M = wellFormed(M, T) and wellFormed(M, T') .

Purifying Equational Conjunctions

Purification first checks if the conjunction is well-formed in one of the modules. If so, then it leaves it alone, otherwise more work is required on the equational atoms.

  op purify : ModuleExpression ModuleExpression EqConj -> [EqConj] .
  ------------------------------------------------------------------
  eq purify(ME, ME', EqC) = purify(upModule(ME, true), upModule(ME', true), EqC) .

  op purify : Module Module EqConj -> [EqConj] .
  ----------------------------------------------
  ceq purify(M, M', EqC)         = EqC if (EqC in M) or (EqC in M') .
  eq  purify(M, M', EqC /\ EqC') = purify(M, M', EqC) /\ purify(M, M', EqC') .

If one of the sides of the equality is not in the first module, purify it with respect to the first module. Note that the equational atoms are commutative, which handles the reversed case.

  ceq purify(M, M', T1 ?= T2) = purify(M, M', purify(M, M', T1) ?= T2) if not wellFormed(M, T1) .
  ceq purify(M, M', T1 != T2) = purify(M, M', purify(M, M', T1) != T2) if not wellFormed(M, T1) .

Purifying Terms

Purifying a term means finding alien sub-terms and extracting them as equality constraints. This is lifted to TermList in the normal way. Note that we take advantage of the fact that generated constraints will bubble to the top.

  op purify : ModuleExpression ModuleExpression TermList -> [CTerm] .
  -------------------------------------------------------------------
  eq purify(ME, ME', TL) = purify(upModule(ME, true), upModule(ME', true), TL) .

  op purify : Module Module TermList -> [CTerm] .
  -----------------------------------------------
  eq purify(M, M', empty)          = empty .
  eq purify(M, M', (NeTL , NeTL')) = purify(M, M', NeTL) , purify(M, M', NeTL') .

If the term is well-formed in the first module, return it. If the top symbol of the term is from the first module, purify the subterms. Otherwise, generate an equality constraint at the top and purify with respect to the second module.

  ceq purify(M, M', T)     = T                       if wellFormed(M, T) .
  ceq purify(M, M', Q[TL]) = Q[purify(M, M', TL)]    if Q inO asTemplate(M) .
  ceq purify(M, M', Q[TL]) = FV | ((FV ?= T) /\ QFF) if (not Q inO asTemplate(M)) /\ Q inO asTemplate(M')
                                                     /\ T | QFF := purify(M', M, Q[TL])
                                                     /\ FV      := joint-variable(M', M, T) .
endfm

Examples

These are over the following modules:

fmod MYINT is

  sorts N NzN .
  sorts I NzI .
  subsort NzN < NzI N < I .

  op zero : -> N [ctor] .
  op one : -> NzN [ctor] .
  op _+_ : N NzN -> NzN [ctor assoc comm id: zero prec 26] .
  op _+_ : N N   -> N   [ctor ditto] .
  op _+_ : I I   -> I   [ctor ditto] .

  op _*_ : NzN NzN -> NzN [assoc comm id: one prec 24] .
  op _*_ : NzI NzI -> NzI [ditto] .
  op _*_ : N   N   -> N   [ditto] .
  op _*_ : I   I   -> I   [ditto] .
endfm

fmod MYINT-RAT is
  protecting MYINT .

  sorts R NzR .
  subsorts NzI < NzR < R .
  subsort I < R .

  op _+_ : R   R   -> R   [ctor ditto] .
  op _*_ : R   R   -> R   [ditto] .
  op _*_ : NzR NzR -> NzR [ditto] .

  op _/_ : R NzR -> R [ctor right id: one prec 25] .
endfm

fmod MYINT-LIST is
  protecting MYINT .

  sorts NeList List .
  subsort NeList < List .

  op nil : -> List .
  op _,_ : I List -> NeList [ctor prec 27] .
endfm

We've named the resulting variables nicer things for easier reading. Note that the variable V0 generated is pushed down to sort I, even though it is of sort R in the combined module. This is because it is in a List, which only has elements of sort I.

reduce in TESTS : purify('MYINT-LIST, 'MYINT-RAT, TERM 7) .
rewrites: 104 in 69ms cpu (68ms real) (1507 rewrites/second)
result CTerm: 'V0:I | 'V0:I ?= '_/_['one.NzN,'y:NzN]

reduce in TESTS : purify('MYINT-LIST, 'MYINT-RAT, TERM 8) .
rewrites: 6 in 0ms cpu (0ms real) (~ rewrites/second)
result Term: '_*_['zero.N,'x:N]

reduce in TESTS : purify('MYINT-LIST, 'MYINT-RAT, TERM 9) .
rewrites: 123 in 52ms cpu (51ms real) (2365 rewrites/second)
result CTerm: '_`,_['zero.N,'_`,_['V0:I,'nil.List]] | 'V0:I ?= '_/_['one.NzN,'y:NzN]