Packages

package lf

Ordering
  1. Alphabetic
Visibility
  1. Public
  2. All

Type Members

  1. trait ApplySolutionRule extends SolutionRule
  2. abstract class ArgumentChecker extends AnyRef

    common code for rules regarding the elimination-form: inference and reduction

  3. case class AtomicJudgement(rl: String, operator: GlobalName, arguments: List[Term]) extends Product with Serializable

    c(args) where c is a constant with a certain role

  4. class BinaryLFConstantScala extends ConstantScala
  5. case class CompareTo(pattern: Term, position: Int) extends MatchStep with Product with Serializable

    a fixed term in the template, typically an OMS

  6. case class ComplexJudgement(parameters: Context, hypotheses: List[AtomicJudgement], thesis: AtomicJudgement) extends Product with Serializable

    {params} Atomic1 -> ...

    {params} Atomic1 -> ... -> Atomicn -> Atomic

  7. case class DeclarativeRule(arguments: List[RuleArgument], conclusion: AtomicJudgement) extends Product with Serializable

    simplest case: {params} Complex1 -> ...

    simplest case: {params} Complex1 -> ... -> Complexn -> Atomic general case: parameters and assumptions may alternate

  8. case class Fix(name: List[LocalName]) extends ProofStep with Product with Serializable
  9. class FouraryLFConstantScala extends ConstantScala
  10. class GeneratedDepthRule extends MatchingSimplificationRule

    a simplification rule generated by SimplificationRuleGenerator

  11. trait GeneratedRule extends AnyRef
  12. class GeneratedSolutionRule extends ValueSolutionRule

    a solution rule generated by SimplificationRuleGenerator

    a solution rule generated by SimplificationRuleGenerator

    names.inside is such that all variables in names.before and names.after as well as the right hand side (which must be a variable) occur in it positions in names.inside are counted from 0

  13. class GenericApplyTerm extends InferenceAndTypingRule

    Elimination: the type inference rule f : Pi x:A.B , conforms(t,A) ---> f t : B [x/t]

    Elimination: the type inference rule f : Pi x:A.B , conforms(t,A) ---> f t : B [x/t]

    This rule works for B:U for any universe U

    This rule implements currying and all arguments at once

  14. class GenericBeta extends ComputationRule

    the beta-reduction rule reducible(s,A) ---> (lambda x:A.t) s = t [x/s]

    the beta-reduction rule reducible(s,A) ---> (lambda x:A.t) s = t [x/s]

    the reducibility judgment is left abstract, usually the typing judgment s:A

    This rule also normalizes nested applications so that it implicitly implements the currying rule (f s) t = f(s,t).

  15. class Injectivity extends TermBasedEqualityRule
  16. case class LFClassicHOLPreprocessor(ded: GlobalName, and: GlobalName, not: GlobalName, forall: Option[GlobalName] = None, or: Option[GlobalName] = None, implies: Option[GlobalName] = None, equiv: Option[GlobalName] = None, exists: Option[GlobalName] = None, equal: Option[GlobalName] = None) extends Preprocessor with Product with Serializable
  17. case class LFError(msg: String) extends Exception with Product with Serializable
  18. case class LFHOASElim(hoas: ViewFinderHOAS) extends Preprocessor with Product with Serializable
  19. class LFOperator extends Operator

    for LF terms using Apply and Lambda

  20. abstract class LFRealizationInScala extends RealizationInScala

    base class of all realization classes generated by ScalaExporter

  21. class LFSym extends AnyRef
  22. abstract class MatchStep extends AnyRef

    tree structure of a Term optimized for efficient matching

  23. class MatchStepCompiler extends AnyRef
  24. class NotationGenerator extends ChangeListener

    A ChangeListerner that adds notations for constants that are inference rules and do not provide notations.

    A ChangeListerner that adds notations for constants that are inference rules and do not provide notations.

    A constant is an inference rule if it takes some parameters (of non-judgment types) and some hypotheses (of judgment type) and return a judgment types.

    For parsing, it makes the parameters implicit.

    For presentation, it renders a proof tree with the hypotheses above, the infered type below, and the symbol name and the parameters to the left of the horizontal line.

  25. class NullaryLFConstantScala extends ConstantScala
  26. case class OuterInnerNames(outer: GlobalName, implArgsOuter: List[Int], before: List[LocalName], innerPos: Int, inner: GlobalName, implArgsInner: List[Int], inside: List[LocalName], after: List[LocalName]) extends Product with Serializable

    convenience class for storing the names of an OuterInnerTerm

    convenience class for storing the names of an OuterInnerTerm

    outer

    outer operator

    implArgsOuter

    positions of the implicit arguments of 'outer' (counting from 0)

    before

    names of the before arguments (excluding implicit ones)

    innerPos

    of innner term (= before.length)

    implArgsInner

    positions of the implicit arguments of 'inner' (counting from 0)

    inside

    names of the inside-arguments (excluding implicit ones)

    after

    names of the after arguments (excluding implicit ones) this represents a left hand side of the form (excluding implicit arguments) outer(before,inner(inside),after) where before, inside, after do not include the implicit arguments

  27. trait PiOrArrowRule extends AnyRef
  28. class PlainBinderScala extends ConstantScala

    auxiliary con/destructor for plain HOAS binders, e.g., forall [x:a] b with forall : (a -> prop) -> prop

    auxiliary con/destructor for plain HOAS binders, e.g., forall [x:a] b with forall : (a -> prop) -> prop

    See also TypedBinderScala

  29. class Plugin extends api.frontend.Plugin
  30. case class RecurseIntoOMA(children: List[MatchStep], position: Int) extends MatchStep with Product with Serializable

    an OMA whose children must be matched recursively

  31. class RewriteRule extends SimplificationRule
  32. abstract class RuleArgument extends AnyRef

    argument of a declarative rule: a parameter or an assumption

  33. case class RuleAssumption(judgment: ComplexJudgement) extends RuleArgument with Product with Serializable
  34. abstract class RuleGenerator extends ChangeListener

    a first step towards generalizing the SimplificationRuleGenerator towards arbitrary rules

    a first step towards generalizing the SimplificationRuleGenerator towards arbitrary rules

    the usefulness is unclear because such rules usually theorem proving anyway the DeclarativeRule abstractions are very nice though it could also be interesting bootstrap the LF rules this way

  35. class RuleMatcher extends AnyRef

    defines pattern matchers on terms for InferenceRules

  36. case class RuleParameter(name: LocalName, tp: Term) extends RuleArgument with Product with Serializable
  37. class ScalaExporter extends GenericScalaExporter
  38. class SimpleIrrelevanceRule extends TypeBasedSolutionRule

    Irrelevance rules for (usually atomic) types that introduce proof irrelevance (as opposed to complex that happen to be irrelevant because their components are): - terms of these types are always equal - unknowns terms of these types are found using proof search; if provided, a default value is used to recover if search fails

  39. class SimplificationRuleGenerator extends ChangeListener
  40. trait SolutionRules extends LFRealizationInScala

    this can be mixed into Scala-models of MMT theories to simplify adding additional rules

  41. case class SolveVariable(name: LocalName, position: Int) extends MatchStep with Product with Serializable

    a template variable that is to be matched

  42. class TPTPPresenter extends Presenter
  43. class TernaryLFConstantScala extends ConstantScala
  44. class Twelf extends ExternalImporter with ChangeListener

    importer wrapper for Twelf, which starts the catalog

  45. class TwelfParser extends Parser

    A TextReader parses Twelf

  46. class TypedBinderScala extends ConstantScala

    auxiliary con/destructor for plain HOAS binders that take an extra argument for the variable type, e.g., forall S [x:tm S] b with forall {s} (tm s -> prop) -> prop

    auxiliary con/destructor for plain HOAS binders that take an extra argument for the variable type, e.g., forall S [x:tm S] b with forall {s} (tm s -> prop) -> prop

    See also PlainBinderScala

  47. class TypedRelationalExtractor extends RelationalExtractor

    The TypedRelationalExtractor adds a few more typing related informations to the .rel files.

  48. class UnaryLFConstantScala extends ConstantScala
  49. case class ViewFinderHOAS(tpS: GlobalName, exprS: GlobalName, lambdaS: GlobalName, applyS: GlobalName, arrowS: GlobalName) extends Product with Serializable

Value Members

  1. object Apply extends LFSym

    provides apply/unapply methods for application of a term to a single argument the unapply method transparently handles associativity (currying) of application

  2. object ApplyGeneral

    like ApplySpine, but also covers the case n=0, akin to FunType

    like ApplySpine, but also covers the case n=0, akin to FunType

    note that ApplySpine(f, Nil) != ApplyGeneral(f, Nil)

  3. object ApplySpine

    provides apply/unapply methods for application of a term to a list of arguments the unapply method transparently handles associativity (currying) of application

    provides apply/unapply methods for application of a term to a list of arguments the unapply method transparently handles associativity (currying) of application

    Does *not* handle empty argument lists!

  4. object ApplyTerm extends GenericApplyTerm

    the usual inference rule with conforms(t,A) = t:A

  5. object Arrow extends LFSym

    provides apply/unapply methods for simple function type formation the unapply method does not match a dependent function type, even if the variable does not occur

  6. object BackwardPiElimination extends BackwardSearch

    the proof step ?:A ----> e(?,...?) for e:Pi x1:A1,...,xn:An.A' where A' ^ s = A for some substitution s

    the proof step ?:A ----> e(?,...?) for e:Pi x1:A1,...,xn:An.A' where A' ^ s = A for some substitution s

    This rule works for any universe U and the case n=0. This rule replace ?'s in the result with their terms if they can be inferred through unification.

  7. object Beta extends GenericBeta

    the usual beta-reduction rule s : A ---> (lambda x:A.t) s = t [x/s]

  8. object Binder

    auxiliary con/destructor for HOAS binders, e.g., forall [x:a] b

  9. object Common
  10. object DropTypeAttribution extends ComputationRule

    |- (t:A) = t

  11. object EqualityTerm extends InferenceRule

    the type inference rule |- A : X, |- B : Y, |- X = Y ---> |- (A = B) : kind for identity kinds This rule goes beyond LF but it does not harm because it only adds kinds and thus do not affect types and terms

  12. object ExpandArrow extends ComputationRule

    A simplification rule that implements A -> B = Pi x:A.B for fresh x.

    A simplification rule that implements A -> B = Pi x:A.B for fresh x. LocalName.Anon is used for x

  13. object Extensionality extends ExtensionalityRule with PiOrArrowRule

    equality-checking: the extensionality rule (equivalent to Eta) x:A|-f x = g x : B ---> f = g : Pi x:A.

    equality-checking: the extensionality rule (equivalent to Eta) x:A|-f x = g x : B ---> f = g : Pi x:A. B If possible, the name of the new variable x is taken from f, g, or their type; otherwise, a fresh variable is invented.

  14. object FixRule extends ProofStepRule
  15. object FlattenCurrying extends ComputationRule

    computation rule for apply that normalizes currying by rewriting terms into uncurried form

  16. object ForwardPiElimination extends ForwardSearch
  17. object FunTerm

    Helper object with apply/unapply for matching and constructing LF functions, i.e.

    Helper object with apply/unapply for matching and constructing LF functions, i.e. LF function type *inhabitants*.

    The methods automatically curry and uncurry.

    LF functions:

    // Represent [a1: t1] [a2: t2] ... [an: tn] b
// where ai is the bound variable and ti the given type
FunTerm(List((a1, t1), ..., (an, tn)), b)
    Example:

    1. Say you already have a (definiens) term and now want to add an abstraction over the variable x:

      val defComponent: Term = ...

val newTypeComponent = FunTerm(
   List((LocalName("x"), typeOfX)),
   defComponent
)
  18. object FunType

    Helper object with apply/unapply for matching and constructing LF function types.

    Helper object with apply/unapply for matching and constructing LF function types.

    The methods - automaticallycurry and uncurry. - and include the case n=0, in particular, unapply always matches!

    "Normal" LF function type:

    // Represent a1 -> ... -> an -> b
FunType(List((None, a1),...,(None, an)), b)

    Dependently typed LF function type:

    // Pi x1:a1. ... Pi xn:an. b
FunType(List((Some(x1), a1),...,(Some(xn), an)), b)

    You can also mix both styles.

    Examples:

    1. Say you want to check whether a given term (of a type component) is a function type to prop:

      val typeComponent: Term = ...
val propSymbol = GlobalName(...) // Give some specific MPath and LocalName
match typeComponent {
  case FunType(args, OMS(propSymbol)) => ...
  case _ => ...
}
      2. ,

    2. Say you already have a type and now want to add dependent types in front of it

      // We have typeComponent and now want
// {x: S} typeComponent

val typeComponent: Term = ...
val dependentVariableType: Term = ...
val dependentTypes = List((Some(LocalName("x")), dependentVariableType))

val newTypeComponent = FunType(dependentTypes, typeComponent)
  19. object JudgmentTypes
  20. object KindInhabitable extends InhabitableRule
  21. object LF
  22. object LFConstantScala
  23. object LFEquality

    provides apply/unapply methods for the LF equality symbol

  24. object LFHOAS extends HOASNotation

    added by rule in LF theory

  25. object Lambda extends LFSym

    provides apply/unapply methods for lambda abstraction

    provides apply/unapply methods for lambda abstraction

    for example, it permits constructing and pattern-matching terms as Lambda(variable-name, type, scope)

    unapply curries automatically

  26. object LambdaCongruence extends TermHeadBasedEqualityRule

    Congruence for Lambda

    Congruence for Lambda

    We cannot use CongruenceRule here because we have to flatten nested lambdas in addition.

    This rule is a special case of Extensionality, but it does not make use of the type.

  27. object LambdaTerm extends IntroductionRule

    Introduction: the type inference rule x:A|-t:B ---> lambda x:A.t : Pi x:A.B This rule works for B:U for any universe U

  28. object NormalizeCurrying extends TermBasedEqualityRule

    equality rule for apply that only considers currying

  29. object OfType
  30. object PLF

    helper object for polymorphic LF

  31. object Pi extends LFSym

    provides apply/unapply methods for dependent function type formation

    provides apply/unapply methods for dependent function type formation

    the unapply method also matches a simple function type

    unapply curries automatically

  32. object PiCongruence extends TermBasedEqualityRule with PiOrArrowRule

    Congruence for Pi

    Congruence for Pi

    We cannot use HeadBasedEqualityRule here because we have to flatten nested Pis and consider -> in addition.

  33. object PiIntroduction extends BackwardInvertible

    the proof step ?:Pi x:A.B ----> lambda x:A.(?:B)

    the proof step ?:Pi x:A.B ----> lambda x:A.(?:B)

    This rule works for any universe U

  34. object PiIrrelevanceRule extends TypeBasedSolutionRule with PiOrArrowRule

    x:A |- ? : B ---> |- ? : Pi x:A.B

  35. object PiTerm extends FormationRule with PiOrArrowRule

    Formation: the type inference rule x:A:type|-B:U ---> Pi x:A.B : U This rule works for any universe U

  36. object PiType extends TypingRule with PiOrArrowRule

    type-checking: the type checking rule x:A|-f x:B ---> f : Pi x:A.B

  37. object PolymorphicApplyTerm extends EliminationRule

    infers the type of a beta-redex whose lambda is not well-typed by itself because it quantifies over too large a universe

  38. object Realize extends ParametricRule

    realize an LF-type/function as a SemanticType or SemanticOperator

  39. object ShallowPolymorphism extends InhabitableRule with PiOrArrowRule

    A:U for some universe U ---> c: {x:A} B allowed

    A:U for some universe U ---> c: {x:A} B allowed

    This allows, e.g., declaring list: type -> type or id: {a:type} a -> a

  40. object SimplificationRuleGenerator
  41. object Skip extends MatchStep with Product with Serializable

    an object that does not have to be compared, typically an implicit argument

  42. object Solve extends ValueSolutionRule with ApplySolutionRule

    solution: This rule tries to solve for an unknown by applying lambda-abstraction on both sides and eta-reduction on the left.

    solution: This rule tries to solve for an unknown by applying lambda-abstraction on both sides and eta-reduction on the left. Its effect is, for example, that X x = t is reduced to X = lambda x.t where X is a meta- and x an object variable.

  43. object SolveMultiple extends ValueSolutionRule
  44. object SolveType extends TypeSolutionRule with ApplySolutionRule

    This rule tries to solve for an unknown by applying lambda-abstraction on both sides and eta-reduction on the left.

    This rule tries to solve for an unknown by applying lambda-abstraction on both sides and eta-reduction on the left. Its effect is, for example, that X x = t is reduced to X = lambda x.t where X is a meta- and x an object variable.

  45. object StandardArgumentChecker extends ArgumentChecker

    default implementation: type-check against expected type if not covered; skip if covered

  46. object TPTP
  47. object TPTPObjectPresenter extends ObjectPresenter
  48. object TermIrrelevanceRule extends ParametricRule
  49. object TheoryTypeWithLF extends ComputationRule
  50. object Twelf

    helper methods for Twelf

  51. object TypeAttribution extends BinaryConstantScala
  52. object TypeAttributionTerm extends InferenceRule

    |- t:A ---> |- (t:A) : A

  53. object TypeInhabitable extends InhabitableRule
  54. object Typed
  55. object Univ

    provides apply/unapply methods for a universes in particular, Univ(1), Univ(2) are type and kind, respectively

  56. object UnivTerm extends InferenceRule

    the type inference rule type:kind

  57. object UniverseKind extends UniverseRule

    the rule that makes kind a valid universe

  58. object UniverseType extends UniverseRule

    the rule that makes type a valid universe

Ungrouped