| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Rzk.TypeCheck.BinderTypes
Description
The elaborated types of a declaration's local binders, for LSP hover.
Every node of a typed term carries its type, so even a bare λ's binder is typed — by the domain of the λ's own Π-type.
The old version threaded a BinderNames environment down through the term, to
say what each variable it met was called. There is no need: entering a binder
puts it in the context, and the context already knows what everything in it is
called (see Rzk.TypeCheck.Display).
Synopsis
- data BinderTypeView
- renderHere :: forall (n :: S). TermT n -> TypeCheck n Rendered
- memoWHNF :: forall (n :: S). TermT n -> TermT n
- binderTypeEntries :: forall (n :: S). Distinct n => Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
- splitViewM :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (Maybe (TermT n))
- binderTypesOfTerm :: forall (n :: S). Distinct n => TermT n -> TypeCheck n [(VarIdent, BinderTypeView)]
- declBinderTypes :: forall (n :: S). Distinct n => Decl n -> TypeCheck n [(VarIdent, BinderTypeView)]
- binderTypesOfFile :: Checked -> FilePath -> [(VarIdent, BinderTypeView)]
Documentation
data BinderTypeView Source #
A binder's displayed type: a plain type, or a cube together with a tope, for a
shaped binder like (t : I | φ t).
Instances
| Show BinderTypeView Source # | |
Defined in Rzk.TypeCheck.BinderTypes Methods showsPrec :: Int -> BinderTypeView -> ShowS # show :: BinderTypeView -> String # showList :: [BinderTypeView] -> ShowS # | |
| Eq BinderTypeView Source # | |
Defined in Rzk.TypeCheck.BinderTypes Methods (==) :: BinderTypeView -> BinderTypeView -> Bool # (/=) :: BinderTypeView -> BinderTypeView -> Bool # | |
renderHere :: forall (n :: S). TermT n -> TypeCheck n Rendered Source #
Render a term with the names of the context it is in.
memoWHNF :: forall (n :: S). TermT n -> TermT n Source #
The memoised weak head normal form of a typed term, if present.
binderTypeEntries :: forall (n :: S). Distinct n => Binder -> TermT n -> TypeCheck n [(VarIdent, BinderTypeView)] Source #
The variables a binder introduces, with their rendered types.
A pair binder splits its type along Σ-types and cube products; when the shape is
not syntactic (the type is a defined name applied to arguments, as in
((η , (ϵ , (α , β))) : has-quasi-diagrammatic-adj A B f u)), the type is put in
weak head normal form first, which needs the top-level definitions in scope. The
dependent part is rendered under the earlier component's display name, giving
q : B p.
splitViewM :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (Maybe (TermT n)) Source #
View a type as a Σ-type or a cube product: syntactically, or through the memoised WHNF if possible, computing the WHNF otherwise. Never throws.
binderTypesOfTerm :: forall (n :: S). Distinct n => TermT n -> TypeCheck n [(VarIdent, BinderTypeView)] Source #
The elaborated types of the local binders of a typed term, keyed by the binder's original identifier (whose position points at its defining occurrence).
declBinderTypes :: forall (n :: S). Distinct n => Decl n -> TypeCheck n [(VarIdent, BinderTypeView)] Source #
All the local binder types of a declaration: Π and Σ binders from its type, λ and let binders from its value.
binderTypesOfFile :: Checked -> FilePath -> [(VarIdent, BinderTypeView)] Source #
The elaborated types of the local binders of one file's declarations, with the
rest of the run's declarations in scope so that whnfT can unfold definitions
when splitting pair binders.
Pure at the interface: it runs the checker silently and returns no entries where it fails.