| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Rzk.Foil.Print
Description
The free-foil core back to surface syntax.
A transcription of fromTermWith' from Language.Rzk.Foil.Names. The
structure is the same, and so are the display rules:
- a binder's user-written name is kept, refreshed only against names already
in use; an anonymous binder draws from
defaultVarIdents; - a pattern binder is shown as the pattern, and projections of the variable
it binds are folded back to the component names, so a goal reads
\ (t , s) -> …and not\ x -> … π₁ x …; - an anonymous binder the codomain does not use is not shown at all, so
(x₁ : A) → Bprints asA → B.
What changes is the bookkeeping: a variable is a Name, so the display
names live in a NameMap keyed by name, rather than being threaded
through de Bruijn shifts.
Synopsis
- fromTermClosed :: Term 'VoidS -> Term
- fromTerm :: forall (n :: S). [VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term
- matchArms :: forall (n :: S). [VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> ([Pattern], Term)
- displayNameOf :: Binder -> [VarIdent] -> VarIdent
- freshenBinder :: [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent])
- scopeUsesItsBinder :: forall (n :: S). ScopedTerm n -> Bool
- nameIdsOf :: forall (l :: S). Term l -> [Int]
Documentation
fromTerm :: forall (n :: S). [VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> Term Source #
matchArms :: forall (n :: S). [VarIdent] -> [VarIdent] -> NameMap n Display -> Term n -> ([Pattern], Term) Source #
displayNameOf :: Binder -> [VarIdent] -> VarIdent Source #
The name standing for the variable itself. A single-variable binder uses its own name; a pattern binder needs a placeholder, which is only shown if the whole point is used (in a shape tope, say), and then it is printed as the pattern anyway.
freshenBinder :: [VarIdent] -> [VarIdent] -> Binder -> (Binder, [VarIdent]) Source #
Refresh a binder's named leaves against the names already in use; draw fresh names for anonymous leaves from the remaining supply.
scopeUsesItsBinder :: forall (n :: S). ScopedTerm n -> Bool Source #
Does a scope actually use the variable it binds?
Compares name ids rather than names, which sidesteps having to unsink the inner scopes' names back into this one. Ids are unique per binder, so a hit is an occurrence of exactly this binder's variable.
(free-foil's own freeVarsOf would do, but it is not in the 0.2.0 release --
it is one of the unreleased helpers on free-foil's main.)