case class IncludeData(home: Term, from: MPath, args: List[Term], df: Option[Term], total: Boolean) extends Product with Serializable
Auxiliary class that collects information about a structure that acts like an include.
- home
The module in which this include is declared (e.g. a theory T, view V, etc.)
- from
The domain D of the included theory (into T, or into domain of V)
- args
Instantiations of the parameters of from (if any, e.g. for parametric theories)
- df
Definiens (of type D(args) -> T, or D(args) -> codomain of V)
- total
A total include is one that must be implemented by the containing theory this becomes available as a morphism only at the end of the containing theory (even if there is a definiens, which can happen, e.g., if the definiens refers to other total includes) invariants: if df contains mor then args.isEmpty && from is domain of df else OMPMOD(from,args) is included theory Note that concrete syntax may allow "include df" because D because can be infered; in a theory, "include D" is the standard for includes without definiens; in a view, we may also allow "include D" for the case where df is the identity of D. See the examples below!
- Source
- Structure.scala
A Theory T includes a theory S in the usual way: theory S : ?someMetaTheory = ... ❚ theory T : ?someMetaTheory = include ?S ❙ ❚ Both theories are non-parametric, i.e. as usual. Then T.getAllIncludes will contain an
IncludeData(T.path, S.path, Nil, None, false). , Assume S, T as above, as well as a View v: T -> R including another view w: S -> R: view w : S -> R = ... ❚ view v : T -> R = include ?S ❘ = ?w ❙ ❚ Then v.getAllIncludes will contain an
IncludeData(v.path, S.path, Nil, w.path, false). , Let R, S, T be as below: theory R : ?someMetaTheory = ... ❚ theory S : ?someMetaTheory = include ?R❙ ... ❚ theory T : ?someMetaTheory = include ?R ❙ ... ❚ Pictorially, this is an inclusion triangle (with one missing edge): R / \ T S Now suppose we want a View v: T -> S which is the identity on R, i.e. v_R = id_R. In surface syntax we can do this as follows: view v: T -> S = include ?R❙ ❚ With this v.getAllIncludes will contain an
IncludeData(v.path, R.path, Nil, Some(OMIDENT(R.path)), false). , If you have a View v: T -> S between two theories with the same meta theory mt, then v.getAllIncludes will automatically include
IncludeData(v.path, mt.path, Nil, Some(OMIDENT(mt.path)), false)similar to the previous example where the view is the identity on the included theory.- See also
- Alphabetic
- By Inheritance
- IncludeData
- Serializable
- Serializable
- Product
- Equals
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
-
new
IncludeData(home: Term, from: MPath, args: List[Term], df: Option[Term], total: Boolean)
- home
The module in which this include is declared (e.g. a theory T, view V, etc.)
- from
The domain D of the included theory (into T, or into domain of V)
- args
Instantiations of the parameters of from (if any, e.g. for parametric theories)
- df
Definiens (of type D(args) -> T, or D(args) -> codomain of V)
- total
A total include is one that must be implemented by the containing theory this becomes available as a morphism only at the end of the containing theory (even if there is a definiens, which can happen, e.g., if the definiens refers to other total includes) invariants: if df contains mor then args.isEmpty && from is domain of df else OMPMOD(from,args) is included theory Note that concrete syntax may allow "include df" because D because can be infered; in a theory, "include D" is the standard for includes without definiens; in a view, we may also allow "include D" for the case where df is the identity of D. See the examples below!
Value Members
-
final
def
!=(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
final
def
##(): Int
- Definition Classes
- AnyRef → Any
-
final
def
==(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
- val args: List[Term]
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
def
asMorphism: Term
OMIDENT(from) or OMINST(from, args) or OMCOMP(the-former, df); OMStructuralInclude for realizations
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
- val df: Option[Term]
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
- val from: MPath
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
- val home: Term
- def isDefined: Option[(MPath, Term)]
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
- def isPlain: Option[(MPath, MPath)]
-
def
isRealization: Boolean
true if this represents a realization
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
- def toStructure: Structure
- val total: Boolean
-
final
def
wait(): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long, arg1: Int): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... )
-
final
def
wait(arg0: Long): Unit
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()