Safe Haskell	None
Language	Haskell2010

Rzk.TypeCheck.Render

Contents

The subshapes of a cube
Rendering

Description

Drawing a term as an SVG diagram of a cube.

The geometry lives in Rzk.Render.Geometry; what is here is the part that knows about terms: which subshape of the cube a tope carves out, which term inhabits each of them, and what to label it with.

Synopsis

cube2powerT :: forall (n :: S). Int -> TermT n
splits :: [a] -> [([a], [a])]
verticesFrom :: forall (n :: S). [TermT n] -> [(ShapeId, TermT n)]
subTopes2 :: forall (n :: S). Int -> TermT n -> [(ShapeId, TermT n)]
componentWiseEQT :: forall (n :: S). Int -> TermT n -> TermT n -> TermT n
isAnonymous :: forall (n :: S). Name n -> TypeCheck n Bool
ppInContext :: forall (n :: S). TermT n -> TypeCheck n String
renderObjectsFor :: forall (n :: S). Distinct n => String -> Int -> TermT n -> TermT n -> TypeCheck n [(ShapeId, RenderObjectData)]
renderObjectsInSubShapeFor :: forall (n :: S). Distinct n => String -> Int -> [Name n] -> Name n -> TermT n -> TermT n -> TermT n -> TypeCheck n [(ShapeId, RenderObjectData)]
renderForSubShapeSVG :: forall (n :: S). Distinct n => String -> Int -> [Name n] -> Name n -> TermT n -> TermT n -> TermT n -> TypeCheck n String
renderForSVG :: forall (n :: S). Distinct n => String -> Int -> TermT n -> TermT n -> TypeCheck n String
drawCube :: Int -> [(String, RenderObjectData)] -> String
dimOf :: forall (n :: S). TermT n -> Maybe Int
maxRenderDim :: Int
renderTermSVGFor :: forall (n :: S). Distinct n => String -> Int -> (Maybe (TermT n, TermT n), [Name n]) -> TermT n -> TypeCheck n (Maybe String)
inScopeMaybeTope :: forall (n :: S) a. Distinct n => Binder -> TModality -> TermT n -> Maybe (ScopedTermT n) -> (forall (l :: S). (DExt n l, Distinct l) => NameBinder n l -> TypeCheck l a) -> TypeCheck n a
renderTermSVG :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (Maybe String)
renderGoalCellSVG :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (Maybe String)
renderTermSVG' :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (Maybe String)
renderApplied :: forall (n :: S) (l :: S). DExt n l => NameBinder n l -> TermT n -> TermT n -> ScopedTermT n -> TypeCheck l (Maybe String)

The subshapes of a cube

cube2powerT :: forall (n :: S). Int -> TermT n Source #

splits :: [a] -> [([a], [a])] Source #

verticesFrom :: forall (n :: S). [TermT n] -> [(ShapeId, TermT n)] Source #

subTopes2 :: forall (n :: S). Int -> TermT n -> [(ShapeId, TermT n)] Source #

componentWiseEQT :: forall (n :: S). Int -> TermT n -> TermT n -> TermT n Source #

Rendering

isAnonymous :: forall (n :: S). Name n -> TypeCheck n Bool Source #

Is the variable an anonymous one (written _)? Its cells are left unlabelled.

ppInContext :: forall (n :: S). TermT n -> TypeCheck n String Source #

Render a term in the current context.

renderObjectsFor :: forall (n :: S). Distinct n => String -> Int -> TermT n -> TermT n -> TypeCheck n [(ShapeId, RenderObjectData)] Source #

renderObjectsInSubShapeFor :: forall (n :: S). Distinct n => String -> Int -> [Name n] -> Name n -> TermT n -> TermT n -> TermT n -> TypeCheck n [(ShapeId, RenderObjectData)] Source #

renderForSubShapeSVG :: forall (n :: S). Distinct n => String -> Int -> [Name n] -> Name n -> TermT n -> TermT n -> TermT n -> TypeCheck n String Source #

renderForSVG :: forall (n :: S). Distinct n => String -> Int -> TermT n -> TermT n -> TypeCheck n String Source #

drawCube :: Int -> [(String, RenderObjectData)] -> String Source #

dimOf :: forall (n :: S). TermT n -> Maybe Int Source #

The dimension of a cube, if it is a power of the directed interval.

maxRenderDim :: Int Source #

renderTermSVGFor Source #

Arguments

:: forall (n :: S). Distinct n
=> String	main colour
-> Int	dimensions accumulated so far (0 to 3)
-> (Maybe (TermT n, TermT n), [Name n])	the accumulated point, and its cube
-> TermT n	the term to render
-> TypeCheck n (Maybe String)

inScopeMaybeTope :: forall (n :: S) a. Distinct n => Binder -> TModality -> TermT n -> Maybe (ScopedTermT n) -> (forall (l :: S). (DExt n l, Distinct l) => NameBinder n l -> TypeCheck l a) -> TypeCheck n a Source #

Enter a binder and assume the shape tope it carries, if any.

renderTermSVG :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (Maybe String) Source #

renderGoalCellSVG :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (Maybe String) Source #

Render the goal cell for a (shape) type: introduce an abstract inhabitant and render it with the proof term hidden. Under a boundary tope an abstract inhabitant of an extension type reduces to the prescribed face value, so the cell shows its given edges with a blank interior — the shape to inhabit, not an answer. Nothing for a non-shape type (a 0-cell, or a non-cube goal).

renderTermSVG' :: forall (n :: S). Distinct n => TermT n -> TypeCheck n (Maybe String) Source #

renderApplied :: forall (n :: S) (l :: S). DExt n l => NameBinder n l -> TermT n -> TermT n -> ScopedTermT n -> TypeCheck l (Maybe String) Source #

Render a term of a function type by applying it to the variable it abstracts over, and drawing that.