| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Rzk.Foil.Convert
Contents
Description
Surface syntax to the free-foil core.
A transcription of toTerm from Language.Rzk.Foil.Names, with the variable
handling replaced. The environment is still a function from a surface
identifier to a term, as before; what changes is what happens at a binder:
- a binder is a fresh
NameBinderrather than the de BruijnZ; - the environment is carried into the binder's scope with
sink, which is a coercion, where the old representation shifted every entry withS <$>and so rebuilt every term it held.
A pattern binder still binds exactly one variable, as before: the components
of \ (t , s) -> … are projections of it, and Binder records the names so
they can be shown back to the user.
Synopsis
- type Env (n :: S) = VarIdent -> Term n
- toTermClosed :: Term -> Term 'VoidS
- toScopedPatternWith :: forall (n :: S). Distinct n => Scope n -> Pattern -> Env n -> (forall (l :: S). Distinct l => Scope l -> Env l -> Term l) -> ScopedTerm n
- toScopedPattern :: forall (n :: S). Distinct n => Scope n -> Pattern -> Env n -> Term -> ScopedTerm n
- toScopedAnon :: forall (n :: S). Distinct n => Scope n -> Env n -> Term -> ScopedTerm n
- bindings :: forall (n :: S). Pattern -> Term n -> [(VarIdent, Term n)]
- toTerm :: forall (n :: S). Distinct n => Scope n -> Env n -> Term -> Term n
- withOpenTerm :: Term -> (forall (n :: S). Distinct n => Scope n -> NameMap n Display -> Term n -> r) -> r
- sinkBound :: forall (n :: S) (l :: S). DExt n l => [(VarIdent, Name n)] -> [(VarIdent, Name l)]
- collectVarIdents :: Data a => a -> [VarIdent]
- nubOrd :: Ord a => [a] -> [a]
Documentation
type Env (n :: S) = VarIdent -> Term n Source #
The environment: what a surface identifier stands for in the current scope. A pattern binder maps its leaves to projections of the single variable it binds, which is why this is a map to terms and not to names.
toScopedPatternWith :: forall (n :: S). Distinct n => Scope n -> Pattern -> Env n -> (forall (l :: S). Distinct l => Scope l -> Env l -> Term l) -> ScopedTerm n Source #
Enter a pattern binder with an explicit continuation for the body: bind one
fresh name, map the pattern's leaves to projections of it, and carry the rest
of the environment in with sink. toScopedPattern is the plain-body
special case; a match branch chains further arms through the continuation.
toScopedPattern :: forall (n :: S). Distinct n => Scope n -> Pattern -> Env n -> Term -> ScopedTerm n Source #
Enter a pattern binder over a surface body.
toScopedAnon :: forall (n :: S). Distinct n => Scope n -> Env n -> Term -> ScopedTerm n Source #
Enter an anonymous binder (a non-dependent function type binds nothing).
bindings :: forall (n :: S). Pattern -> Term n -> [(VarIdent, Term n)] Source #
What each leaf of a pattern stands for: a projection chain over the single variable the pattern binds.
Open terms
withOpenTerm :: Term -> (forall (n :: S). Distinct n => Scope n -> NameMap n Display -> Term n -> r) -> r Source #
Elaborate a surface term whose free identifiers are not known in advance.
Each identifier occurring anywhere in the term gets a name in a fresh scope, so an open term (the annotation of a binder, say, taken out of its context) can be put into the core, transformed, and printed back with the names it came in with. The reference index needs this: it splits the annotation of a pair binder through the core, and has no typing context to hand.
sinkBound :: forall (n :: S) (l :: S). DExt n l => [(VarIdent, Name n)] -> [(VarIdent, Name l)] Source #
Sink an association list of binders by coercion, with no per-entry
rebuild (withOpenTerm calls this at every binder it opens).
sink1 cannot see through the pair (its element must be the
sunk type itself), but the sinkability argument is the same: only the
names mention the scope, and a name sinks by coercion.
collectVarIdents :: Data a => a -> [VarIdent] Source #
Every identifier occurring in a piece of surface syntax, bound or free.