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 anonymizeModuleOrLink(solver: CheckingCallback, namedModuleOrLink: ModuleOrLink, initialReferencesToUnqualify: List[GlobalName] = Nil)(implicit stack: Stack, history: History): (List[GlobalName], List[OML])

   Anonymize and flatten a ModuleOrLink, most commonly a Theory or View, to a list of OML declarations.

   Anonymize and flatten a ModuleOrLink, most commonly a Theory or View, to a list of OML declarations.

   Overall, this method will first flatten the ModuleOrLink and then try to translate every obtained declaration to an OML. For that OMSs in declaration components will be replaced by OMLs referencing previous OML declarations. The method basically keeps track of all "previous GlobalNames which have been seen and where references to them should be replaced by LocalName references". If you want to anonymize a Link, this list of "previous things" does not suffice since a Link is naturally to be interpreted in the context of its codomain. Hence, you can use initialReferencesToUnqualify to provide an initial list of "previous things". More precisely, in the case of anonymizing a Link, you should first anonymize the codomain, obtain its list of GlobalName to unqualify (the first component of the return vaue of this method), and then pass this onto the anonmyization call of the Link.

   solver

   Solver instance used for looking up inclusions (before flattening the ModuleOrLink).

   namedModuleOrLink

   A ModuleOrLink to be flattened and anonymized to a list of OMLs.

   initialReferencesToUnqualify

   Read the Scala doc above.

   returns

   A tuple of (global names to unqualify, list of OMLs), where

   • the global names to unqualify are as explained above the "list of previous things"
   • and the list of OMLS the actual anonymized list of declarations

   To do

   Does this work for partial views? I don't think so since we take the view's domain via Link.getAllIncludesWithSelf and translate it via the link. What does solver.lookup.ApplyMorphs(OMS(c.path), df, stack.context) do in case df is not defined on c?

5.  def anonymizeTheory(solver: CheckingCallback, namedTheory: Theory)(implicit stack: Stack, history: History): AnonymousTheory

   turns a declared theory into an anonymous one by dropping all global qualifiers (only defined if names are still unique afterwards)

6.  def anonymizeView(solver: CheckingCallback, namedView: View)(implicit stack: Stack, history: History): AnonymousMorphism

   turns a declared theory into an anonymous one by dropping all global qualifiers (only defined if names are still unique afterwards)

7.  def applySubstitution(decls: List[OML], renames: List[(LocalName, Term)]): List[OML]
8.  def asAnonymousDiagram(solver: CheckingCallback, diag: Term)(implicit stack: Stack, history: History): Option[AnonymousDiagram]

   provides the base case of the function that elaborates a diagram expression (in the form of an AnonymousDiagram)

9.  def asAnonymousMorphism(solver: CheckingCallback, fromTerm: Term, from: AnonymousTheory, toTerm: Term, to: AnonymousTheory, mor: Term)(implicit stack: Stack, history: History): Option[AnonymousMorphism]

   like asAnonymousTheory but for morphisms

10.  def asAnonymousTheory(solver: CheckingCallback, thy: Term)(implicit stack: Stack, history: History): Option[AnonymousTheory]

    provides the base case of the function that elaborates a theory expression (in the form of an AnonymousTheory)

11.  final def asInstanceOf[T0]: T0

    Definition Classes

    Any

12.  def asSubstitution(r: List[Term]): List[(LocalName, Term)]
13.  def clone(): AnyRef

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()

14.  final def eq(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

15.  def equals(arg0: Any): Boolean

    Definition Classes

    AnyRef → Any

16.  def finalize(): Unit

    Attributes

    protected[lang]

    Definition Classes

    AnyRef

    Annotations

    @throws( classOf[java.lang.Throwable] )

17.  final def getClass(): Class[_]

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

18.  def hashCode(): Int

    Definition Classes

    AnyRef → Any

    Annotations

    @native()

19.  final def isInstanceOf[T0]: Boolean

    Definition Classes

    Any

20.  final def ne(arg0: AnyRef): Boolean

    Definition Classes

    AnyRef

21.  final def notify(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

22.  final def notifyAll(): Unit

    Definition Classes

    AnyRef

    Annotations

    @native()

23.  def prefixLabels(ad: AnonymousDiagram, prefix: LocalName): AnonymousDiagram
24.  final def synchronized[T0](arg0: ⇒ T0): T0

    Definition Classes

    AnyRef

25.  def toString(): String

    Definition Classes

    AnyRef → Any

26.  final def wait(): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

27.  final def wait(arg0: Long, arg1: Int): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... )

28.  final def wait(arg0: Long): Unit

    Definition Classes

    AnyRef

    Annotations

    @throws( ... ) @native()

29.  object ExistingName

    apply/unapply functions so that ExistingName(p) is the label of a module with URI p