class InductiveTypes extends StructuralFeature with ParametricTheoryLike
- Alphabetic
- By Inheritance
- InductiveTypes
- ParametricTheoryLike
- StructuralFeature
- GeneralStructuralFeature
- FormatBasedExtension
- Extension
- Logger
- AnyRef
- Any
- Hide All
- Show All
- Public
- All
Instance Constructors
- new InductiveTypes()
Type Members
-
case class
LocalError(s: String) extends ExtensionError with Product with Serializable
a custom error class for this extension
a custom error class for this extension
- Definition Classes
- Extension
Value Members
-
object
noLookupPresenter extends NotationBasedPresenter
- Definition Classes
- ParametricTheoryLike
-
object
VarDeclFeature extends DerivedVarDeclFeature
for creating/matching variable declarations of this feature
for creating/matching variable declarations of this feature
- Definition Classes
- StructuralFeature
-
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
Type: Type
- Definition Classes
- ParametricTheoryLike
-
final
def
asInstanceOf[T0]: T0
- Definition Classes
- Any
-
val
bodyDelim: String
- Definition Classes
- GeneralStructuralFeature
-
def
catchErrors[A](msg: String, recoverWith: ⇒ A)(code: ⇒ A): A
like its partner but with return value
like its partner but with return value
- Attributes
- protected
- Definition Classes
- Extension
-
def
catchErrors(msg: String)(code: ⇒ Unit): Unit
convenience method for wrapping code in error handler that throws LocalError
convenience method for wrapping code in error handler that throws LocalError
- Attributes
- protected
- Definition Classes
- Extension
-
def
check(dd: DerivedDeclaration)(implicit env: ExtendedCheckingEnvironment): Unit
Checks the validity of the inductive type(s) to be constructed
Checks the validity of the inductive type(s) to be constructed
- dd
the derived declaration from which the inductive type(s) are to be constructed
- Definition Classes
- InductiveTypes → ParametricTheoryLike → GeneralStructuralFeature
-
def
checkInContext(prev: Context, dv: VarDecl): Unit
- Definition Classes
- StructuralFeature
-
def
checkTermLevel(tc: TermLevel, types: List[GlobalName]): AnyVal
Check whether the TermLevel has a higher order argument of an inductively defined type In that case an error is thrown
-
def
clone(): AnyRef
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( ... ) @native()
-
val
controller: Controller
the controller that this extension is added to; only valid after creation of the extension, i.e., will return null if used in a non-lazy val-field
the controller that this extension is added to; only valid after creation of the extension, i.e., will return null if used in a non-lazy val-field
- Attributes
- protected
- Definition Classes
- Extension
-
lazy val
defaultPrefix: String
- Definition Classes
- Extension
-
def
defaultPresenter(c: Constant)(implicit con: Controller): String
- Definition Classes
- ParametricTheoryLike
-
def
destroy: Unit
extension-specific cleanup (override as needed, empty by default)
extension-specific cleanup (override as needed, empty by default)
Extensions may create persistent data structures and threads, but they must clean up after themselves in this method
- Definition Classes
- Extension
-
def
destroyWhenRemainingTasksFinished: Unit
convenience for calling waitUntilRemainingTasksFinished and then destroy
convenience for calling waitUntilRemainingTasksFinished and then destroy
- Definition Classes
- Extension
-
def
elaborate(parent: ModuleOrLink, dd: DerivedDeclaration)(implicit env: Option[ExtendedSimplificationEnvironment] = None): Elaboration
Elaborates an declaration of one or multiple mutual inductive types into their declaration, as well as the corresponding no confusion and no junk axioms Constructs a structure whose models are exactly the (not necessarily initial) models of the declared inductive types
Elaborates an declaration of one or multiple mutual inductive types into their declaration, as well as the corresponding no confusion and no junk axioms Constructs a structure whose models are exactly the (not necessarily initial) models of the declared inductive types
- parent
The parent module of the declared inductive types
- dd
the derived declaration to be elaborated
- Definition Classes
- InductiveTypes → StructuralFeature
-
def
elaborateDeclarations(context: Context, decls: List[InternalDeclaration], logger: Option[(Constant) ⇒ Unit] = None)(implicit parentTerm: GlobalName): Elaboration
Elaborates an derived declaration D using the inductive feature.
Elaborates an derived declaration D using the inductive feature. This is used to reuse the functionality of this feature in different features, speciafically the reflection feature.
- context
The context of D
- decls
The internal declaration of the D
- parentTerm
The path to D, used as prefix for the external declarations
-
def
elaborateInContext(prev: Context, dv: VarDecl): Context
- Definition Classes
- StructuralFeature
-
final
def
eq(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
equals(arg0: Any): Boolean
- Definition Classes
- AnyRef → Any
-
def
expectedComponents: List[(String, ObjComponentKey)]
the term components that declarations of this feature must provide and strings for parsing/presenting them
the term components that declarations of this feature must provide and strings for parsing/presenting them
also defines the order of the components
- Definition Classes
- GeneralStructuralFeature
-
def
expectedType(dd: DerivedDeclaration, c: Constant): Option[Term]
compute the expected type of a constant inside a derived element of this feature none by default, override as needed
compute the expected type of a constant inside a derived element of this feature none by default, override as needed
- Definition Classes
- GeneralStructuralFeature
-
val
feature: String
- Definition Classes
- GeneralStructuralFeature
-
def
finalize(): Unit
- Attributes
- protected[lang]
- Definition Classes
- AnyRef
- Annotations
- @throws( classOf[java.lang.Throwable] )
-
final
def
getClass(): Class[_]
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
getFromFirstArgOrEnvvar(args: List[String], name: String, default: String = ""): String
- Attributes
- protected
- Definition Classes
- Extension
-
def
getHeaderNotation: List[Product with Serializable with Marker { def toString: String }]
the notation for the header
the notation for the header
- Definition Classes
- ParametricTheoryLike → GeneralStructuralFeature
-
def
getHeaderRule: ParsingRule
the parse rule for the header
the parse rule for the header
- Definition Classes
- GeneralStructuralFeature
-
def
getInnerContext(dd: DerivedDeclaration): Context
additional context relative to which to interpret the body of a derived declaration
additional context relative to which to interpret the body of a derived declaration
- Definition Classes
- ParametricTheoryLike → StructuralFeature
-
def
getRule: StructuralFeatureRule
returns the rule constant for using this feature in a theory
returns the rule constant for using this feature in a theory
- Definition Classes
- StructuralFeature
-
def
hashCode(): Int
- Definition Classes
- AnyRef → Any
- Annotations
- @native()
-
def
indProofs(tpdecls: List[TypeLevel], tmdecls: List[TermLevel], context: Context)(implicit parent: GlobalName): List[Constant]
Generate inductive proof declarations for an inductive type declaration I
Generate inductive proof declarations for an inductive type declaration I
- tpdecls
all Type-Level declarations in I
- tmdecls
all constructor declarations in I
- context
the parameters of I
- parent
the URI of I
-
def
initOther(e: Extension): Unit
any extension can initialize other extensions if those are not meant to be added to the ExtensionManager
any extension can initialize other extensions if those are not meant to be added to the ExtensionManager
- Attributes
- protected
- Definition Classes
- Extension
-
def
isApplicable(s: String): Boolean
- returns
true if this extension is applicable
- Definition Classes
- GeneralStructuralFeature → FormatBasedExtension
-
final
def
isInstanceOf[T0]: Boolean
- Definition Classes
- Any
-
def
log(e: Error): Unit
logs an error - always logged
logs an error - always logged
- Attributes
- protected
- Definition Classes
- Logger
-
def
log(s: ⇒ String, subgroup: Option[String] = None): Unit
logs a message with this logger's logprefix
logs a message with this logger's logprefix
- Attributes
- protected
- Definition Classes
- Logger
-
def
logError(s: ⇒ String): Unit
log as an error message
log as an error message
- Attributes
- protected
- Definition Classes
- Logger
-
def
logGroup[A](a: ⇒ A): A
wraps around a group to create nested logging
wraps around a group to create nested logging
- Attributes
- protected
- Definition Classes
- Logger
-
def
logPrefix: String
the prefix used to identify this extension for logging, by default the class name
-
def
logTemp(s: ⇒ String): Unit
temporary logging - always logged
temporary logging - always logged
- Attributes
- protected
- Definition Classes
- Logger
-
def
makeErrorThrower(msg: String): ErrorHandler
an ErrorHandler that wraps an error in a LocalError and throws it
an ErrorHandler that wraps an error in a LocalError and throws it
- Attributes
- protected
- Definition Classes
- Extension
-
def
makeHeader(dd: DerivedDeclaration): Term
inverse of processHeader
inverse of processHeader
- Definition Classes
- ParametricTheoryLike → GeneralStructuralFeature
-
def
matchTypeParametersInReturnType(a: TermLevel, b: TermLevel): (Boolean, List[(OMV, OMV)])
Check whether the return types match for some parametric type parameters and if so determine the necessary parameters that need to match
Check whether the return types match for some parametric type parameters and if so determine the necessary parameters that need to match
- a
the first termlevel whoose return type is to be matched against the one of the second
- b
the second termlevel whoose return type is to be matched against the return type of a
- Note
postcondition: If the types match for certain arguments, a list of tuples with arguments that need to match is returned if those arguments passed to the termlevels are the same, the return types will both equal a.externalRet
-
def
modules(dd: DerivedDeclaration): List[Module]
override as needed
override as needed
- Definition Classes
- GeneralStructuralFeature
-
lazy val
mpath: MPath
- Definition Classes
- GeneralStructuralFeature
-
final
def
ne(arg0: AnyRef): Boolean
- Definition Classes
- AnyRef
-
def
noConf(a: TermLevel, tmdecls: List[TermLevel], types: List[GlobalName])(implicit parent: GlobalName): List[Constant]
Generate no confusion/injectivity declaration for term constructor d and all term constructors of the same return type
Generate no confusion/injectivity declaration for term constructor d and all term constructors of the same return type
- tmdecls
all term level declarations
- parent
the derived declaration to elaborate
-
def
noJunks(decls: List[InternalDeclaration], context: Context)(implicit parent: GlobalName): List[Constant]
Generate no junk declarations for an inductive type declaration I
Generate no junk declarations for an inductive type declaration I
- decls
all declarations in I
- context
the parameters of I for type level declarations c: {G} type induct_c: {M,G} c g -> c_M (g map induct) for term level declaration c: {G} A induct_c: {M,G} induct(c g) = c_M (g map induct) where * M declares one (primed) variable for every declaration in I * c_M is the variable in M corresponding to c * g is the list of varibles declared in G * induct(t) is the inductive translation of t, defined in terms of the induct function corresponding to the type of t, e.g., induct_a(m,t) if t has type a for some a: type in I or induct_a(m,h,t) if t has type (a h) for some a: {H}type in I
- parent
the URI of I
-
final
def
notify(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
final
def
notifyAll(): Unit
- Definition Classes
- AnyRef
- Annotations
- @native()
-
def
processHeader(header: Term): (LocalName, Term)
parses the header term of a derived declaration into its name and type by default it is interpreted as OMA(mpath, name :: args) where OMA(mpath, args) is the type
parses the header term of a derived declaration into its name and type by default it is interpreted as OMA(mpath, name :: args) where OMA(mpath, args) is the type
- Definition Classes
- ParametricTheoryLike → GeneralStructuralFeature
- val report: Report
-
def
start(args: List[String]): Unit
extension-specific initialization (override as needed, empty by default)
extension-specific initialization (override as needed, empty by default)
- Definition Classes
- ParametricTheoryLike → Extension
-
final
def
synchronized[T0](arg0: ⇒ T0): T0
- Definition Classes
- AnyRef
-
def
testers(tmdecls: List[TermLevel], tpdecls: List[TypeLevel], decls: List[InternalDeclaration], context: Context)(implicit parent: GlobalName): List[Constant]
Generate tester declarations for all constructors of an inductive type declaration I
Generate tester declarations for all constructors of an inductive type declaration I
- tmdecls
the termlevel declarations in I
- tpdecls
the typelevel declarations in I
- decls
all internal declarations in I
- context
the context of I
-
def
toString(): String
- Definition Classes
- AnyRef → Any
-
def
unappliers(constrdecls: List[Constructor], tpdecls: List[TypeLevel], decls: List[InternalDeclaration], context: Context)(implicit parent: GlobalName): List[Constant]
Generate unapply declarations for all constructors of an inductive type declaration I
Generate unapply declarations for all constructors of an inductive type declaration I
- constrdecls
the constructors of I
- tpdecls
the typelevel declarations in I
- decls
all internal declarations in I
- context
the context of I
-
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()
-
def
waitUntilRemainingTasksFinished: Unit
extensions that process tasks in separate threads should override this and wait until those threads are done
extensions that process tasks in separate threads should override this and wait until those threads are done
- Definition Classes
- Extension