Safe Haskell	None
Language	Haskell2010

Rzk.TypeCheck.Display

Description

Showing a term to the user.

A term of the core names its variables by Name (an Int), so anything user-facing — an error, a trace of a judgement, a hole's goal — has to say what each name is called. That is a Naming: a display name and a display binder per name in scope, plus the supply of fresh names for the binders the printer meets on the way down.

This replaces the old var -> VarIdent threading (name, nameInc, BinderNames, ppTermInContext — four copies of the same idea), and with it the unwinding loop that rebuilt those names one binder at a time.

Synopsis

data Naming (n :: S) = Naming {
- namingOf :: NameMap n Display
- namingUsed :: [VarIdent]
- namingSupply :: [VarIdent]
}
namingOfContext :: forall (n :: S). Context n -> Naming n
newtype Rendered = Rendered {
- getRendered :: Term
}
renderTerm :: forall (n :: S). Naming n -> Term n -> Rendered
ppTerm :: forall (n :: S). Naming n -> Term n -> String
ppTermT :: forall (n :: S). Naming n -> TermT n -> String
displayOf :: forall (n :: S). Naming n -> Name n -> Display
ppName :: forall (n :: S). Naming n -> Name n -> String
panicImpossible :: String -> a

Documentation

data Naming (n :: S) Source #

What every name in scope is called, and what the printer may call the binders it has yet to meet.

Constructors

Naming
Fields namingOf :: NameMap n Display namingUsed :: [VarIdent] the display names taken, so a bound binder is refreshed away from them namingSupply :: [VarIdent] the names left over, for anonymous binders

namingOfContext :: forall (n :: S). Context n -> Naming n Source #

Read the naming off a context.

A named binder keeps its name, refreshed only if an outer name has already taken it. An anonymous one draws from the supply. A pattern binder has its component names freshened as a group, so that the pattern shown in the context and the projections folded inside a term agree on them.

Entries are named oldest binding first (see ctxBound), so an outer binder keeps its name and an inner one is the one refreshed away from it.

newtype Rendered Source #

A term already rendered for the user, kept as surface syntax rather than a string so that a consumer may still inspect it.

Its Show prints the surface syntax, which is what the old Term' did, so a rendered goal or candidate reads the same as it always has (\ (t, s) → ?).

Constructors

Rendered
Fields getRendered :: Term

Instances

Instances details

Show Rendered Source #
Instance details Defined in Rzk.TypeCheck.Display Methods showsPrec :: Int -> Rendered -> ShowS # show :: Rendered -> String # showList :: [Rendered] -> ShowS #
Eq Rendered Source #	Two rendered terms are equal when they read the same. (The surface AST carries source positions, which a rendered term should not be judged by.)
Instance details Defined in Rzk.TypeCheck.Display Methods (==) :: Rendered -> Rendered -> Bool # (/=) :: Rendered -> Rendered -> Bool #

renderTerm :: forall (n :: S). Naming n -> Term n -> Rendered Source #

A term as surface syntax, with the context's names.

A binder inside the term is freshened only against the names the term itself mentions — not against everything in scope. A type shows the binder it was written with (Σ (a : A), B a), even where the context happens to have an a of its own: the two are different variables, and shadowing is what binders are for.

ppTerm :: forall (n :: S). Naming n -> Term n -> String Source #

A term shown to the user.

ppTermT :: forall (n :: S). Naming n -> TermT n -> String Source #

A typed term shown as term : type, as the old ppFoldT did. A variable is shown bare: its type is in the context, not on the node.

displayOf :: forall (n :: S). Naming n -> Name n -> Display Source #

What a name is called, and the (freshened) binder it was introduced by.

ppName :: forall (n :: S). Naming n -> Name n -> String Source #

A variable as the user sees it: a pattern binder shows as its pattern ((t, s)), anything else by its display name.

panicImpossible :: String -> a Source #