| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Rzk.TypeCheck.Decl.Data
Description
The surface-syntax scaffolding of #data declarations, kept separate from
the monadic checker in Rzk.TypeCheck.Decl.
Two things live here, both pure. First, small builders over the surface
syntax (surfaceApps, surfacePi, …) and the preprocessed forms of a
declaration (the SortIndex telescope and the DataConSurface
constructors). Second, the construction of the generated eliminators: given
an ElimSpec — the declaration's data together with the fresh binders of the
generated types and the validated endpoint images — elimTerms produces the
surface types of ind-D and rec-D and the path computation rules. The
checker then pushes those surface terms through the ordinary elaborator, so
nothing here constructs core terms or touches the type-checking monad.
Synopsis
- addParamDecls :: [ParamDecl] -> Term -> Term
- data SortIndex = SortIndex {}
- data DataConSort
- data DataConSurface = DataConSurface {
- dataConName :: VarIdent
- dataConFields :: [ParamDecl]
- dataConFieldPats :: [Term]
- dataConRecursive :: [(Int, [Term])]
- dataConRetIndices :: [Term]
- dataConType :: Term
- dataConProbe :: Term
- dataConNonRec :: [Term]
- dataConLocalNames :: [VarIdentToken]
- dataConSort :: DataConSort
- surfacePatternVars :: Pattern -> [VarIdent]
- identTokenOf :: VarIdent -> VarIdentToken
- surfaceVar :: VarIdent -> Term
- surfaceLambda :: [VarIdent] -> Term -> Term
- underscoreIdent :: VarIdent
- surfaceVarTokens :: Data a => a -> [VarIdentToken]
- surfaceApps :: Term -> [Term] -> Term
- surfaceAppSpine :: Term -> (Term, [Term])
- surfaceArrow :: Term -> Term -> Term
- surfacePiSpine :: Term -> ([Term], Term)
- dataAppliedIndices :: VarIdent -> [VarIdent] -> Int -> Term -> Maybe [Term]
- matchesDataApplied :: VarIdent -> [VarIdent] -> Int -> Term -> Bool
- surfacePi :: VarIdent -> Term -> Term -> Term
- prefixedIdent :: Text -> VarIdent -> VarIdent
- nthByConstruction :: String -> [a] -> Int -> a
- recPositionsOf :: DataConSurface -> [Int]
- data ElimSpec = ElimSpec {
- esName :: VarIdent
- esParamVars :: [VarIdent]
- esParamDecls :: [ParamDecl]
- esIndexVars :: [VarIdent]
- esIndexDecls :: [ParamDecl]
- esMotiveV :: VarIdent
- esScrutV :: VarIdent
- esIhNames :: [VarIdent]
- esMethodVars :: Maybe [VarIdent]
- esEndpointV :: VarIdent
- esPathV :: VarIdent
- esTransportV :: VarIdent
- esConsData :: [DataConSurface]
- esPathData :: [Maybe ((Term, Term), (Term, Term))]
- data ElimTerms = ElimTerms {
- indTypeTerm :: Term
- recTypeTerm :: Term
- computeRules :: [(VarIdent, Term)]
- elimTerms :: ElimSpec -> ElimTerms
Surface-syntax builders and preprocessed forms
One index of a family, as declared in the sort: its binder (when the
sort names it, as in (n : nat) → U) and its type.
Constructors
| SortIndex | |
Fields | |
data DataConSort Source #
The sort of a constructor: a point constructor returns the declared
type; a path constructor returns an identity type over it (spelled
l =_{D …} r), declaring an identification between the two endpoint
terms. Path β-rules are propositional (the generated compute- lemmas),
following the HoTT-book treatment of higher inductive types.
Constructors
| DataConPoint | |
| DataConPath Term Term | the endpoints of the declared identification, as written |
data DataConSurface Source #
A constructor, preprocessed at the surface level.
Constructors
| DataConSurface | |
Fields
| |
surfacePatternVars :: Pattern -> [VarIdent] Source #
identTokenOf :: VarIdent -> VarIdentToken Source #
surfaceVar :: VarIdent -> Term Source #
surfaceLambda :: [VarIdent] -> Term -> Term Source #
A λ over plain (untyped) variable patterns; only ever used in checking position, where the domains come from the expected type.
underscoreIdent :: VarIdent Source #
The wildcard binder, for a generated λ that ignores an argument.
surfaceVarTokens :: Data a => a -> [VarIdentToken] Source #
Every variable-occurrence token in a surface term, collected generically. Used for the endpoint well-formedness check of path constructors, which is deliberately syntactic.
surfacePiSpine :: Term -> ([Term], Term) Source #
The domains and codomain of a surface Π-chain (domain types only; for the shaped and modal parameter forms the carrier is what matters here).
dataAppliedIndices :: VarIdent -> [VarIdent] -> Int -> Term -> Maybe [Term] Source #
Is the term the given name applied to exactly the given parameter
variables (in order, the uniformity requirement) and then exactly
arity index terms? Returns those index terms. A syntactic check: this
is how constructor return types and directly recursive fields are
recognised.
nthByConstruction :: String -> [a] -> Int -> a Source #
Index into a list that is long enough by construction, panicking with a
label instead of the opaque Prelude.!! message if that invariant is ever
broken. Used where an index is derived from the same data as the list (the
induction-hypothesis binders, a constructor's field patterns).
recPositionsOf :: DataConSurface -> [Int] Source #
The 0-based positions of a constructor's directly recursive fields.
Eliminator construction
Everything the pure construction of the eliminators closes over: the declaration's name, its parameters and index telescope, the fresh binders of the generated types (the motive, the scrutinee, the induction hypotheses, the path-method names, and the binders of the inlined transport), the preprocessed constructors, and — for each path constructor — the images of its endpoints under the section being defined. Assembled by Rzk.TypeCheck.Decl once the fresh names are allocated and the endpoints validated.
Constructors
| ElimSpec | |
Fields
| |
The generated surface types of a declaration's eliminators and the path computation rules, all as surface terms for the ordinary elaborator.
Constructors
| ElimTerms | |
Fields
| |