package sequences
- Alphabetic
- Public
- All
Type Members
-
class
Association extends ParametricRule
takes flexary composition operator op: {n} a^n -> a and implements associativity and related simplifications
-
class
ExpandEllipsis extends ComputationRule
the beta-style rule [E(i)]_{i=1}^n ---> E(1),...,E(n)
the beta-style rule [E(i)]_{i=1}^n ---> E(1),...,E(n)
The rule is applied only in argument sequences and contexts. In contexts, it is only applied if the sequence variable occurs only with literal indices, in which case each x.1 is replaced with x/"1" etc. If the sequence variable occurs in any other way (e.g., as x or x.n), it is not expanded.
It would be easier to use the substitution x->Sequence(x/"1",...,x/"n"), but that is not possible because we avoid concatenation here. Typically, sequence variables occur with indices that are index variables of ellipses. Those ellipses must have been previously simplified.
-
class
SequenceEqualityCheck extends ExtensionalityRule
component-wise equality-checking of sequences
component-wise equality-checking of sequences
|s| = |t| = |a| |- s.i = t.i : a.i for all i=1,...,n-1 -------------------------------------- |- s=t : a
applicable only if |a| simplifies to a literal
-
class
SequenceTypeCheck extends TypingRule
component-wise type-checking of a sequence
component-wise type-checking of a sequence
|t| = |a| |- t.i : a.i for all i=0,...,n-1 --------------------------------- |- t : a
applicable only if |a| simplifies to a literal
Value Members
- object Bool
-
object
BoundedSemilattice extends Association
combines monoid and semilattice laws
-
object
ContractRep extends ComplificationRule
inverse of ExpandRep, useful for complification
- object EllipsisEqualityCheck extends SequenceEqualityCheck
-
object
EllipsisInfer extends InferenceRule
i, i/up |- t(i) : a_i : type ---> |- [t(i)] i=0n : [a_i] i=0n i, i/up |- t(i) : type ---> |- [t(i)] i=0n : typen
- object EllipsisInjective extends CongruenceRule
- object EllipsisTypeCheck extends SequenceTypeCheck
- object ExpandEllipsis
-
object
ExpandRep extends ComputationRule
an ---> [a]i=0n for fresh i
-
object
FlatSeqInfer extends InferenceRule
...
... t_i : A_i ... for i = 1,...,n ---------------------------------- t_1,...,t_n : A_1,...,A_n
- object FlatseqInjective extends CongruenceRule
-
object
FlexaryApply extends ExpandEllipsis
expands ellipses in the arguments of an apply
-
object
FlexaryComposition extends ExpandEllipsis
expands ellipses in the arguments of a composition
-
object
FlexaryCompositionInfer extends InferenceRule
s.i : A.i -> B.i for i=0,...,n A_{i+1} = B.i for i=0,...,n-1 ------------------------------ comp(s) : A.0 -> B.n
-
object
FlexaryLambda extends ExpandEllipsis
expands ellipses in the arguments of a lambda
-
object
FlexaryPi extends ExpandEllipsis with PiOrArrowRule
expands ellipses in the arguments of a Pi
- object FoldLeft extends FouraryConstantScala
- object FoldLeftType extends InferenceRule
-
object
IndexCompute extends ComputationRule
([a(i)] i=1n).k ----> a(k) (an).i ----> a (a_1,...,a_n).k ----> a_k if k literal a.0 ----> a if |a|=1 // every plain term can be seen as a sequence of length 1
-
object
IndexInfer extends InferenceRule
|- s : a |- i < |a| ------------- |- s.i : a.i
- object LFS
-
object
Length
auxiliary functions for length-based operations on sequences
- object LengthAwareApplyTerm extends GenericApplyTerm
-
object
LengthAwareArgumentChecker extends ArgumentChecker
Restriction of StandardArgumentChecker that requires that expected and provided length agree
- object LengthAwareBeta extends GenericBeta
-
object
Monoid extends Association
additionally takes a neutral element
-
object
NTypeTerm extends InferenceRule
|- type ^ n : kind
- object Nat
- object NatRules
-
object
NoSeqs
matches argument list without sequences preceded by a NatLit
- object RepEqualityCheck extends SequenceEqualityCheck
- object RepTypeCheck extends SequenceTypeCheck
-
object
Semilattice extends Association
eliminates duplicates among the arguments
- object Sequences
-
object
SolveArity extends InferenceRule
matches an operator that expects sequence arguments against an argument sequence
matches an operator that expects sequence arguments against an argument sequence
this rule is called before ApplyTerm, solves unknown arity arguments, then fails once the arities are solved, ApplyTerm can do the rest
-
object
UniverseNType extends UniverseRule
|- type^n UNIV