Packages

class OMStoOML extends AnyRef

A _stateful_ translator to translate OMS' to OMLs to un-fully-qualify declarations and their interdependent dependencies, say in a Theory or Link, but generally in a ModuleOrLink.

Source
Common.scala
Linear Supertypes
AnyRef, Any
Ordering
  1. Alphabetic
  2. By Inheritance
Inherited
  1. OMStoOML
  2. AnyRef
  3. Any
  1. Hide All
  2. Show All
Visibility
  1. Public
  2. All

Instance Constructors

  1. new OMStoOML(ctx: Context, initialReferencesToUnqualify: List[GlobalName] = Nil)

    ctx

    A Context object passed to the underlying OMSReplacer, actually unused.

    initialReferencesToUnqualify

    As we go through constant declaratiosn using apply(Constant), we keep track of the GlobalNames of these constant. Namely, to replace subsequent references to them by the un-fully-qualified references. You may here pass an initial list of such GlobalNames. This may be useful when processing a View, namely in that case you want to pass all GlobalNames of the codomain.

Value Members

  1. final def !=(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  2. final def ##(): Int
    Definition Classes
    AnyRef → Any
  3. final def ==(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  4. def apply(c: Constant, unqualifyLater: Boolean): (OML, Boolean)

    Un-fully-qualifies a Constant and return an OML for that together with a boolean flag determining if the name of the new OML is a duplicate within the previous constants encountered using this method.

    Un-fully-qualifies a Constant and return an OML for that together with a boolean flag determining if the name of the new OML is a duplicate within the previous constants encountered using this method.

    This might happen if a theory includes two unrelated theories both declaring a symbol with the same LocalName, but of course with different GlobalName as they stem from two unrelated theories. In that case un-fully-qualifiying yields a duplicate as signalled by this method.

    unqualifyLater

    Signal whether we should unqualify references to c.path later by replacing them by c.name.

    returns

    The new un-fully-qualified OML and a Boolean "wasDuplicate" indicate whether we had a name clash.

  5. def apply(tm: Term): Term
  6. final def asInstanceOf[T0]: T0
    Definition Classes
    Any
  7. def clone(): AnyRef
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()
  8. final def eq(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  9. def equals(arg0: Any): Boolean
    Definition Classes
    AnyRef → Any
  10. def finalize(): Unit
    Attributes
    protected[lang]
    Definition Classes
    AnyRef
    Annotations
    @throws( classOf[java.lang.Throwable] )
  11. final def getClass(): Class[_]
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  12. def getGlobalNamesWhoseReferencesToUnqualify: List[GlobalName]
  13. def hashCode(): Int
    Definition Classes
    AnyRef → Any
    Annotations
    @native()
  14. final def isInstanceOf[T0]: Boolean
    Definition Classes
    Any
  15. final def ne(arg0: AnyRef): Boolean
    Definition Classes
    AnyRef
  16. final def notify(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  17. final def notifyAll(): Unit
    Definition Classes
    AnyRef
    Annotations
    @native()
  18. final def synchronized[T0](arg0: ⇒ T0): T0
    Definition Classes
    AnyRef
  19. def toString(): String
    Definition Classes
    AnyRef → Any
  20. final def wait(): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  21. final def wait(arg0: Long, arg1: Int): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... )
  22. final def wait(arg0: Long): Unit
    Definition Classes
    AnyRef
    Annotations
    @throws( ... ) @native()

Inherited from AnyRef

Inherited from Any

Ungrouped