Safe Haskell	None
Language	Haskell2010

Rzk.TypeCheck

Contents

Orphan instances

Synopsis

defaultTypeCheck :: TypeCheck var a -> Either (TypeErrorInScopedContext var) a
data Decl var = Decl {
- declName :: var
- declType :: TermT var
- declValue :: Maybe (TermT var)
- declIsAssumption :: Bool
- declUsedVars :: [var]
- declLocation :: Maybe LocationInfo
}
type Decl' = Decl VarIdent
typecheckModulesWithLocationIncremental :: [(FilePath, [Decl'])] -> [(FilePath, Module)] -> TypeCheck VarIdent ([(FilePath, [Decl'])], [TypeErrorInScopedContext VarIdent])
typecheckModulesWithLocation' :: [(FilePath, Module)] -> TypeCheck VarIdent ([(FilePath, [Decl'])], [TypeErrorInScopedContext VarIdent])
typecheckModulesWithLocation :: [(FilePath, Module)] -> TypeCheck VarIdent [(FilePath, [Decl'])]
typecheckModules :: [Module] -> TypeCheck VarIdent [Decl']
typecheckModuleWithLocation :: (FilePath, Module) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
countCommands :: Integral a => [Command] -> a
typecheckModule :: Maybe FilePath -> Module -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
splitSectionCommands :: SectionName -> [Command] -> TypeCheck var ([Command], [Command])
setOption :: String -> String -> TypeCheck var a -> TypeCheck var a
unsetOption :: String -> TypeCheck var a -> TypeCheck var a
paramToParamDecl :: Param -> TypeCheck var [ParamDecl]
addParamDecls :: [ParamDecl] -> Term -> Term
addParams :: [Param] -> Term -> Term
data TypeError var
- = TypeErrorOther String
- | TypeErrorUnify (TermT var) (TermT var) (TermT var)
- | TypeErrorUnifyTerms (TermT var) (TermT var)
- | TypeErrorNotPair (TermT var) (TermT var)
- | TypeErrorNotFunction (TermT var) (TermT var)
- | TypeErrorUnexpectedLambda (Term var) (TermT var)
- | TypeErrorUnexpectedPair (Term var) (TermT var)
- | TypeErrorUnexpectedRefl (Term var) (TermT var)
- | TypeErrorCannotInferBareLambda (Term var)
- | TypeErrorCannotInferBareRefl (Term var)
- | TypeErrorUndefined var
- | TypeErrorTopeNotSatisfied [TermT var] (TermT var)
- | TypeErrorTopesNotEquivalent (TermT var) (TermT var)
- | TypeErrorInvalidArgumentType (Term var) (TermT var)
- | TypeErrorDuplicateTopLevel [VarIdent] VarIdent
- | TypeErrorUnusedVariable var (TermT var)
- | TypeErrorUnusedUsedVariables [var] var
- | TypeErrorImplicitAssumption (var, TermT var) var
data TypeErrorInContext var = TypeErrorInContext {
- typeErrorError :: TypeError var
- typeErrorContext :: Context var
}
data TypeErrorInScopedContext var
- = PlainTypeError (TypeErrorInContext var)
- | ScopedTypeError (Maybe VarIdent) (TypeErrorInScopedContext (Inc var))
type TypeError' = TypeError VarIdent
ppTypeError' :: TypeError' -> String
ppTypeErrorInContext :: OutputDirection -> TypeErrorInContext VarIdent -> String
ppTypeErrorInScopedContextWith' :: OutputDirection -> [VarIdent] -> [VarIdent] -> TypeErrorInScopedContext VarIdent -> String
ppTypeErrorInScopedContext' :: OutputDirection -> TypeErrorInScopedContext VarIdent -> String
issueWarning :: String -> TypeCheck var ()
fromTypeError :: TypeError var -> TypeCheck var (TypeErrorInScopedContext var)
issueTypeError :: TypeError var -> TypeCheck var a
panicImpossible :: String -> a
data Action var
- = ActionTypeCheck (Term var) (TermT var)
- | ActionUnify (TermT var) (TermT var) (TermT var)
- | ActionUnifyTerms (TermT var) (TermT var)
- | ActionInfer (Term var)
- | ActionContextEntailedBy [TermT var] (TermT var)
- | ActionContextEntails [TermT var] (TermT var)
- | ActionContextEquiv [TermT var] [TermT var]
- | ActionWHNF (TermT var)
- | ActionNF (TermT var)
- | ActionCheckCoherence (TermT var, TermT var) (TermT var, TermT var)
- | ActionCloseSection (Maybe SectionName)
type Action' = Action VarIdent
ppTermInContext :: Eq var => TermT var -> TypeCheck var String
ppSomeAction :: Eq var => [(var, Maybe VarIdent)] -> Int -> Action var -> String
ppAction :: Int -> Action' -> String
traceAction' :: Int -> Action' -> a -> a
unsafeTraceAction' :: Int -> Action var -> a -> a
data LocationInfo = LocationInfo {
- locationFilePath :: Maybe FilePath
- locationLine :: Maybe Int
}
data Verbosity
- = Debug
- | Normal
- | Silent
trace' :: Verbosity -> Verbosity -> String -> a -> a
traceTypeCheck :: Verbosity -> String -> TypeCheck var a -> TypeCheck var a
localVerbosity :: Verbosity -> TypeCheck var a -> TypeCheck var a
localRenderBackend :: Maybe RenderBackend -> TypeCheck var a -> TypeCheck var a
data Covariance
- = Covariant
- | Contravariant
data RenderBackend
- = RenderSVG
- | RenderLaTeX
data ScopeInfo var = ScopeInfo {
- scopeName :: Maybe SectionName
- scopeVars :: [(var, VarInfo var)]
}
addVarToScope :: var -> VarInfo var -> ScopeInfo var -> ScopeInfo var
data VarInfo var = VarInfo {
- varType :: TermT var
- varValue :: Maybe (TermT var)
- varOrig :: Maybe VarIdent
- varIsAssumption :: Bool
- varDeclaredAssumptions :: [var]
- varLocation :: Maybe LocationInfo
}
data Context var = Context {
- localScopes :: [ScopeInfo var]
- localTopes :: [TermT var]
- localTopesNF :: [TermT var]
- localTopesNFUnion :: [[TermT var]]
- localTopesEntailBottom :: Bool
- actionStack :: [Action var]
- currentCommand :: Maybe Command
- location :: Maybe LocationInfo
- verbosity :: Verbosity
- covariance :: Covariance
- renderBackend :: Maybe RenderBackend
}
addVarInCurrentScope :: var -> VarInfo var -> Context var -> Context var
emptyContext :: Context var
askCurrentScope :: TypeCheck var (ScopeInfo var)
varInfos :: Context var -> [(var, VarInfo var)]
varTypes :: Context var -> [(var, TermT var)]
varValues :: Context var -> [(var, Maybe (TermT var))]
varOrigs :: Context var -> [(var, Maybe VarIdent)]
withPartialDecls :: TypeCheck VarIdent ([Decl'], [err]) -> TypeCheck VarIdent ([Decl'], [err]) -> TypeCheck VarIdent ([Decl'], [err])
withSection :: Maybe SectionName -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent]) -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent]) -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent])
startSection :: Maybe SectionName -> TypeCheck VarIdent a -> TypeCheck VarIdent a
endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
scopeToDecls :: Eq var => [TypeErrorInScopedContext var] -> ScopeInfo var -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var])
insertExplicitAssumptionFor :: Eq var => var -> (var, VarInfo var) -> TermT var -> TermT var
insertExplicitAssumptionFor' :: Eq var => var -> (var, VarInfo var) -> VarInfo var -> VarInfo var
makeAssumptionExplicit :: Eq var => (var, VarInfo var) -> [(var, VarInfo var)] -> TypeCheck var (Bool, [(var, VarInfo var)])
collectScopeDecls :: Eq var => [TypeErrorInScopedContext var] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var])
abstractAssumption :: Eq var => (var, VarInfo var) -> Decl var -> Decl var
data OutputDirection
- = TopDown
- | BottomUp
block :: OutputDirection -> [String] -> String
namedBlock :: OutputDirection -> String -> [String] -> String
ppContext' :: OutputDirection -> Context VarIdent -> String
doesShadowName :: VarIdent -> TypeCheck var [VarIdent]
checkTopLevelDuplicate :: VarIdent -> TypeCheck var ()
checkNameShadowing :: VarIdent -> TypeCheck var ()
withLocation :: LocationInfo -> TypeCheck var a -> TypeCheck var a
withCommand :: Command -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent])
localDecls :: [Decl VarIdent] -> TypeCheck VarIdent a -> TypeCheck VarIdent a
localDeclsPrepared :: [Decl VarIdent] -> TypeCheck VarIdent a -> TypeCheck VarIdent a
localDecl :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a
localDeclPrepared :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a
type TypeCheck var = ReaderT (Context var) (Except (TypeErrorInScopedContext var))
freeVarsT_ :: Eq var => TermT var -> TypeCheck var [var]
traceStartAndFinish :: Show a => String -> a -> a
entail :: Eq var => [TermT var] -> TermT var -> Bool
entailM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool
entailTraceM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool
nubTermT :: Eq var => [TermT var] -> [TermT var]
saturateTopes :: Eq var => [TermT var] -> [TermT var] -> [TermT var]
saturateWith :: (a -> [a] -> Bool) -> ([a] -> [a] -> [a]) -> [a] -> [a]
generateTopes :: Eq var => [TermT var] -> [TermT var] -> [TermT var]
generateTopesForPoints :: Eq var => [TermT var] -> [TermT var]
generateTopesForPointsM :: Eq var => [TermT var] -> TypeCheck var [TermT var]
allTopePoints :: Eq var => TermT var -> [TermT var]
topePoints :: TermT var -> [TermT var]
subPoints :: TermT var -> [TermT var]
simplifyLHSwithDisjunctions :: Eq var => [TermT var] -> [[TermT var]]
simplifyLHS :: Eq var => [TermT var] -> [TermT var]
solveRHSM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool
solveRHS :: Eq var => [TermT var] -> TermT var -> Bool
checkTope :: Eq var => TermT var -> TypeCheck var Bool
checkTopeEntails :: Eq var => TermT var -> TypeCheck var Bool
checkEntails :: Eq var => TermT var -> TermT var -> TypeCheck var Bool
contextEntailedBy :: Eq var => TermT var -> TypeCheck var ()
contextEntails :: Eq var => TermT var -> TypeCheck var ()
topesEquiv :: Eq var => TermT var -> TermT var -> TypeCheck var Bool
contextEquiv :: Eq var => [TermT var] -> TypeCheck var ()
switchVariance :: TypeCheck var a -> TypeCheck var a
enterScopeContext :: Maybe VarIdent -> TermT var -> Context var -> Context (Inc var)
enterScope :: Maybe VarIdent -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b
performing :: Eq var => Action var -> TypeCheck var a -> TypeCheck var a
stripTypeRestrictions :: TermT var -> TermT var
etaMatch :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var (TermT var, TermT var)
etaExpand :: Eq var => TermT var -> TypeCheck var (TermT var)
inCubeLayer :: Eq var => TermT var -> TypeCheck var Bool
inTopeLayer :: Eq var => TermT var -> TypeCheck var Bool
tryRestriction :: Eq var => TermT var -> TypeCheck var (Maybe (TermT var))
whnfT :: Eq var => TermT var -> TypeCheck var (TermT var)
nfTope :: Eq var => TermT var -> TypeCheck var (TermT var)
nfT :: Eq var => TermT var -> TypeCheck var (TermT var)
checkDefinedVar :: VarIdent -> TypeCheck VarIdent ()
valueOfVar :: Eq var => var -> TypeCheck var (Maybe (TermT var))
typeOfVar :: Eq var => var -> TypeCheck var (TermT var)
typeOfUncomputed :: Eq var => TermT var -> TypeCheck var (TermT var)
typeOf :: Eq var => TermT var -> TypeCheck var (TermT var)
unifyTopes :: Eq var => TermT var -> TermT var -> TypeCheck var ()
inAllSubContexts :: TypeCheck var () -> TypeCheck var () -> TypeCheck var ()
unify :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var ()
unifyViaDecompose :: Eq var => TermT var -> TermT var -> TypeCheck var ()
unifyInCurrentContext :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var ()
unifyTypes :: Eq var => TermT var -> TermT var -> TermT var -> TypeCheck var ()
unifyTerms :: Eq var => TermT var -> TermT var -> TypeCheck var ()
localTope :: Eq var => TermT var -> TypeCheck var a -> TypeCheck var a
universeT :: TermT var
cubeT :: TermT var
topeT :: TermT var
topeEQT :: TermT var -> TermT var -> TermT var
topeLEQT :: TermT var -> TermT var -> TermT var
topeOrT :: TermT var -> TermT var -> TermT var
topeAndT :: TermT var -> TermT var -> TermT var
cubeProductT :: TermT var -> TermT var -> TermT var
cubeUnitT :: TermT var
cubeUnitStarT :: TermT var
typeUnitT :: TermT var
unitT :: TermT var
cube2T :: TermT var
cube2_0T :: TermT var
cube2_1T :: TermT var
topeTopT :: TermT var
topeBottomT :: TermT var
recBottomT :: TermT var
typeRestrictedT :: TermT var -> [(TermT var, TermT var)] -> TermT var
lambdaT :: TermT var -> Maybe VarIdent -> Maybe (TermT var, Maybe (Scope TermT var)) -> Scope TermT var -> TermT var
appT :: TermT var -> TermT var -> TermT var -> TermT var
pairT :: TermT var -> TermT var -> TermT var -> TermT var
firstT :: TermT var -> TermT var -> TermT var
secondT :: TermT var -> TermT var -> TermT var
reflT :: TermT var -> Maybe (TermT var, Maybe (TermT var)) -> TermT var
typeFunT :: Maybe VarIdent -> TermT var -> Maybe (Scope TermT var) -> Scope TermT var -> TermT var
typeSigmaT :: Maybe VarIdent -> TermT var -> Scope TermT var -> TermT var
recOrT :: TermT var -> [(TermT var, TermT var)] -> TermT var
typeIdT :: TermT var -> Maybe (TermT var) -> TermT var -> TermT var
idJT :: TermT var -> TermT var -> TermT var -> TermT var -> TermT var -> TermT var -> TermT var -> TermT var
typeAscT :: TermT var -> TermT var -> TermT var
typecheck :: Eq var => Term var -> TermT var -> TypeCheck var (TermT var)
inferAs :: Eq var => TermT var -> Term var -> TypeCheck var (TermT var)
infer :: Eq var => Term var -> TypeCheck var (TermT var)
checkCoherence :: Eq var => (TermT var, TermT var) -> (TermT var, TermT var) -> TypeCheck var ()
inferStandalone :: Eq var => Term var -> Either (TypeErrorInScopedContext var) (TermT var)
unsafeInferStandalone' :: Term' -> TermT'
unsafeTypeCheck' :: TypeCheck VarIdent a -> a
type PointId = String
type ShapeId = [PointId]
cube2powerT :: Int -> TermT var
splits :: [a] -> [([a], [a])]
verticesFrom :: [TermT var] -> [(ShapeId, TermT var)]
subTopes2 :: Int -> TermT var -> [(ShapeId, TermT var)]
cubeSubTopes :: [(ShapeId, TermT (Inc var))]
limitLength :: Int -> String -> String
renderObjectsFor :: Eq var => String -> Int -> TermT var -> TermT var -> TypeCheck var [(ShapeId, RenderObjectData)]
componentWiseEQT :: Int -> TermT var -> TermT var -> TermT var
renderObjectsInSubShapeFor :: Eq var => String -> Int -> [var] -> var -> TermT var -> TermT var -> TermT var -> TypeCheck var [(ShapeId, RenderObjectData)]
renderForSubShapeSVG :: Eq var => String -> Int -> [var] -> var -> TermT var -> TermT var -> TermT var -> TypeCheck var String
renderForSVG :: Eq var => String -> Int -> TermT var -> TermT var -> TypeCheck var String
renderTermSVGFor :: Eq var => String -> Int -> (Maybe (TermT var, TermT var), [var]) -> TermT var -> TypeCheck var (Maybe String)
renderTermSVG :: Eq var => TermT var -> TypeCheck var (Maybe String)
renderTermSVG' :: Eq var => TermT var -> TypeCheck var (Maybe String)
type Point2D a = (a, a)
type Point3D a = (a, a, a)
type Edge3D a = (Point3D a, Point3D a)
type Face3D a = (Point3D a, Point3D a, Point3D a)
type Volume3D a = (Point3D a, Point3D a, Point3D a, Point3D a)
data CubeCoords2D a b = CubeCoords2D {
- vertices :: [(Point3D a, Point2D b)]
- edges :: [(Edge3D a, (Point2D b, Point2D b))]
- faces :: [(Face3D a, (Point2D b, Point2D b, Point2D b))]
- volumes :: [(Volume3D a, (Point2D b, Point2D b, Point2D b, Point2D b))]
}
data Matrix3D a = Matrix3D a a a a a a a a a
data Matrix4D a = Matrix4D a a a a a a a a a a a a a a a a
data Vector3D a = Vector3D a a a
data Vector4D a = Vector4D a a a a
rotateX :: Floating a => a -> Matrix3D a
rotateY :: Floating a => a -> Matrix3D a
rotateZ :: Floating a => a -> Matrix3D a
data Camera a = Camera {
- cameraPos :: Point3D a
- cameraFoV :: a
- cameraAspectRatio :: a
- cameraAngleY :: a
- cameraAngleX :: a
}
viewRotateX :: Floating a => Camera a -> Matrix4D a
viewRotateY :: Floating a => Camera a -> Matrix4D a
viewTranslate :: Num a => Camera a -> Matrix4D a
project2D :: Floating a => Camera a -> Matrix4D a
matrixVectorMult4D :: Num a => Matrix4D a -> Vector4D a -> Vector4D a
matrix3Dto4D :: Num a => Matrix3D a -> Matrix4D a
fromAffine :: Fractional a => Vector4D a -> (Point2D a, a)
point3Dto2D :: Floating a => Camera a -> a -> Point3D a -> (Point2D a, a)
data RenderObjectData = RenderObjectData {
- renderObjectDataLabel :: String
- renderObjectDataFullLabel :: String
- renderObjectDataColor :: String
}
renderCube :: (Floating a, Show a) => Camera a -> a -> (String -> Maybe RenderObjectData) -> String
defaultCamera :: Floating a => Camera a

Documentation

>>> :set -XOverloadedStrings

defaultTypeCheck :: TypeCheck var a -> Either (TypeErrorInScopedContext var) a Source #

data Decl var Source #

Constructors

Decl
Fields declName :: var declType :: TermT var declValue :: Maybe (TermT var) declIsAssumption :: Bool declUsedVars :: [var] declLocation :: Maybe LocationInfo

Instances

Instances details

Eq var => Eq (Decl var) Source #
Instance details Defined in Rzk.TypeCheck Methods (==) :: Decl var -> Decl var -> Bool # (/=) :: Decl var -> Decl var -> Bool #

type Decl' = Decl VarIdent Source #

typecheckModulesWithLocationIncremental Source #

Arguments

:: [(FilePath, [Decl'])]	Cached declarations (only those that do not need rechecking).
-> [(FilePath, Module)]	New modules to check
-> TypeCheck VarIdent ([(FilePath, [Decl'])], [TypeErrorInScopedContext VarIdent])

typecheckModulesWithLocation' :: [(FilePath, Module)] -> TypeCheck VarIdent ([(FilePath, [Decl'])], [TypeErrorInScopedContext VarIdent]) Source #

typecheckModulesWithLocation :: [(FilePath, Module)] -> TypeCheck VarIdent [(FilePath, [Decl'])] Source #

typecheckModules :: [Module] -> TypeCheck VarIdent [Decl'] Source #

typecheckModuleWithLocation :: (FilePath, Module) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) Source #

countCommands :: Integral a => [Command] -> a Source #

typecheckModule :: Maybe FilePath -> Module -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) Source #

splitSectionCommands :: SectionName -> [Command] -> TypeCheck var ([Command], [Command]) Source #

setOption :: String -> String -> TypeCheck var a -> TypeCheck var a Source #

unsetOption :: String -> TypeCheck var a -> TypeCheck var a Source #

paramToParamDecl :: Param -> TypeCheck var [ParamDecl] Source #

addParamDecls :: [ParamDecl] -> Term -> Term Source #

addParams :: [Param] -> Term -> Term Source #

data TypeError var Source #

Constructors

TypeErrorOther String
TypeErrorUnify (TermT var) (TermT var) (TermT var)
TypeErrorUnifyTerms (TermT var) (TermT var)
TypeErrorNotPair (TermT var) (TermT var)
TypeErrorNotFunction (TermT var) (TermT var)
TypeErrorUnexpectedLambda (Term var) (TermT var)
TypeErrorUnexpectedPair (Term var) (TermT var)
TypeErrorUnexpectedRefl (Term var) (TermT var)
TypeErrorCannotInferBareLambda (Term var)
TypeErrorCannotInferBareRefl (Term var)
TypeErrorUndefined var
TypeErrorTopeNotSatisfied [TermT var] (TermT var)
TypeErrorTopesNotEquivalent (TermT var) (TermT var)
TypeErrorInvalidArgumentType (Term var) (TermT var)
TypeErrorDuplicateTopLevel [VarIdent] VarIdent
TypeErrorUnusedVariable var (TermT var)
TypeErrorUnusedUsedVariables [var] var
TypeErrorImplicitAssumption (var, TermT var) var

Instances

Instances details

Foldable TypeError Source #
Instance details Defined in Rzk.TypeCheck Methods fold :: Monoid m => TypeError m -> m # foldMap :: Monoid m => (a -> m) -> TypeError a -> m # foldMap' :: Monoid m => (a -> m) -> TypeError a -> m # foldr :: (a -> b -> b) -> b -> TypeError a -> b # foldr' :: (a -> b -> b) -> b -> TypeError a -> b # foldl :: (b -> a -> b) -> b -> TypeError a -> b # foldl' :: (b -> a -> b) -> b -> TypeError a -> b # foldr1 :: (a -> a -> a) -> TypeError a -> a # foldl1 :: (a -> a -> a) -> TypeError a -> a # toList :: TypeError a -> [a] # null :: TypeError a -> Bool # length :: TypeError a -> Int # elem :: Eq a => a -> TypeError a -> Bool # maximum :: Ord a => TypeError a -> a # minimum :: Ord a => TypeError a -> a # sum :: Num a => TypeError a -> a # product :: Num a => TypeError a -> a #
Functor TypeError Source #
Instance details Defined in Rzk.TypeCheck Methods fmap :: (a -> b) -> TypeError a -> TypeError b # (<$) :: a -> TypeError b -> TypeError a #

data TypeErrorInContext var Source #

Constructors

TypeErrorInContext
Fields typeErrorError :: TypeError var typeErrorContext :: Context var

Instances

Instances details

Foldable TypeErrorInContext Source #
Instance details Defined in Rzk.TypeCheck Methods fold :: Monoid m => TypeErrorInContext m -> m # foldMap :: Monoid m => (a -> m) -> TypeErrorInContext a -> m # foldMap' :: Monoid m => (a -> m) -> TypeErrorInContext a -> m # foldr :: (a -> b -> b) -> b -> TypeErrorInContext a -> b # foldr' :: (a -> b -> b) -> b -> TypeErrorInContext a -> b # foldl :: (b -> a -> b) -> b -> TypeErrorInContext a -> b # foldl' :: (b -> a -> b) -> b -> TypeErrorInContext a -> b # foldr1 :: (a -> a -> a) -> TypeErrorInContext a -> a # foldl1 :: (a -> a -> a) -> TypeErrorInContext a -> a # toList :: TypeErrorInContext a -> [a] # null :: TypeErrorInContext a -> Bool # length :: TypeErrorInContext a -> Int # elem :: Eq a => a -> TypeErrorInContext a -> Bool # maximum :: Ord a => TypeErrorInContext a -> a # minimum :: Ord a => TypeErrorInContext a -> a # sum :: Num a => TypeErrorInContext a -> a # product :: Num a => TypeErrorInContext a -> a #
Functor TypeErrorInContext Source #
Instance details Defined in Rzk.TypeCheck Methods fmap :: (a -> b) -> TypeErrorInContext a -> TypeErrorInContext b # (<$) :: a -> TypeErrorInContext b -> TypeErrorInContext a #

data TypeErrorInScopedContext var Source #

Constructors

PlainTypeError (TypeErrorInContext var)
ScopedTypeError (Maybe VarIdent) (TypeErrorInScopedContext (Inc var))

Instances

Instances details

Foldable TypeErrorInScopedContext Source #
Instance details Defined in Rzk.TypeCheck Methods fold :: Monoid m => TypeErrorInScopedContext m -> m # foldMap :: Monoid m => (a -> m) -> TypeErrorInScopedContext a -> m # foldMap' :: Monoid m => (a -> m) -> TypeErrorInScopedContext a -> m # foldr :: (a -> b -> b) -> b -> TypeErrorInScopedContext a -> b # foldr' :: (a -> b -> b) -> b -> TypeErrorInScopedContext a -> b # foldl :: (b -> a -> b) -> b -> TypeErrorInScopedContext a -> b # foldl' :: (b -> a -> b) -> b -> TypeErrorInScopedContext a -> b # foldr1 :: (a -> a -> a) -> TypeErrorInScopedContext a -> a # foldl1 :: (a -> a -> a) -> TypeErrorInScopedContext a -> a # toList :: TypeErrorInScopedContext a -> [a] # null :: TypeErrorInScopedContext a -> Bool # length :: TypeErrorInScopedContext a -> Int # elem :: Eq a => a -> TypeErrorInScopedContext a -> Bool # maximum :: Ord a => TypeErrorInScopedContext a -> a # minimum :: Ord a => TypeErrorInScopedContext a -> a # sum :: Num a => TypeErrorInScopedContext a -> a # product :: Num a => TypeErrorInScopedContext a -> a #
Functor TypeErrorInScopedContext Source #
Instance details Defined in Rzk.TypeCheck Methods fmap :: (a -> b) -> TypeErrorInScopedContext a -> TypeErrorInScopedContext b # (<$) :: a -> TypeErrorInScopedContext b -> TypeErrorInScopedContext a #

type TypeError' = TypeError VarIdent Source #

ppTypeError' :: TypeError' -> String Source #

ppTypeErrorInContext :: OutputDirection -> TypeErrorInContext VarIdent -> String Source #

ppTypeErrorInScopedContextWith' :: OutputDirection -> [VarIdent] -> [VarIdent] -> TypeErrorInScopedContext VarIdent -> String Source #

ppTypeErrorInScopedContext' :: OutputDirection -> TypeErrorInScopedContext VarIdent -> String Source #

issueWarning :: String -> TypeCheck var () Source #

fromTypeError :: TypeError var -> TypeCheck var (TypeErrorInScopedContext var) Source #

issueTypeError :: TypeError var -> TypeCheck var a Source #

panicImpossible :: String -> a Source #

data Action var Source #

Constructors

ActionTypeCheck (Term var) (TermT var)
ActionUnify (TermT var) (TermT var) (TermT var)
ActionUnifyTerms (TermT var) (TermT var)
ActionInfer (Term var)
ActionContextEntailedBy [TermT var] (TermT var)
ActionContextEntails [TermT var] (TermT var)
ActionContextEquiv [TermT var] [TermT var]
ActionWHNF (TermT var)
ActionNF (TermT var)
ActionCheckCoherence (TermT var, TermT var) (TermT var, TermT var)
ActionCloseSection (Maybe SectionName)

Instances

Instances details

Foldable Action Source #
Instance details Defined in Rzk.TypeCheck Methods fold :: Monoid m => Action m -> m # foldMap :: Monoid m => (a -> m) -> Action a -> m # foldMap' :: Monoid m => (a -> m) -> Action a -> m # foldr :: (a -> b -> b) -> b -> Action a -> b # foldr' :: (a -> b -> b) -> b -> Action a -> b # foldl :: (b -> a -> b) -> b -> Action a -> b # foldl' :: (b -> a -> b) -> b -> Action a -> b # foldr1 :: (a -> a -> a) -> Action a -> a # foldl1 :: (a -> a -> a) -> Action a -> a # toList :: Action a -> [a] # null :: Action a -> Bool # length :: Action a -> Int # elem :: Eq a => a -> Action a -> Bool # maximum :: Ord a => Action a -> a # minimum :: Ord a => Action a -> a # sum :: Num a => Action a -> a # product :: Num a => Action a -> a #
Functor Action Source #
Instance details Defined in Rzk.TypeCheck Methods fmap :: (a -> b) -> Action a -> Action b # (<$) :: a -> Action b -> Action a #

type Action' = Action VarIdent Source #

ppTermInContext :: Eq var => TermT var -> TypeCheck var String Source #

ppSomeAction :: Eq var => [(var, Maybe VarIdent)] -> Int -> Action var -> String Source #

ppAction :: Int -> Action' -> String Source #

traceAction' :: Int -> Action' -> a -> a Source #

unsafeTraceAction' :: Int -> Action var -> a -> a Source #

data LocationInfo Source #

Constructors

LocationInfo
Fields locationFilePath :: Maybe FilePath locationLine :: Maybe Int

Instances

Instances details

Eq LocationInfo Source #
Instance details Defined in Rzk.TypeCheck Methods (==) :: LocationInfo -> LocationInfo -> Bool # (/=) :: LocationInfo -> LocationInfo -> Bool #

data Verbosity Source #

Constructors

Debug
Normal
Silent

Instances

Instances details

Eq Verbosity Source #
Instance details Defined in Rzk.TypeCheck Methods (==) :: Verbosity -> Verbosity -> Bool # (/=) :: Verbosity -> Verbosity -> Bool #
Ord Verbosity Source #
Instance details Defined in Rzk.TypeCheck Methods compare :: Verbosity -> Verbosity -> Ordering # (<) :: Verbosity -> Verbosity -> Bool # (<=) :: Verbosity -> Verbosity -> Bool # (>) :: Verbosity -> Verbosity -> Bool # (>=) :: Verbosity -> Verbosity -> Bool # max :: Verbosity -> Verbosity -> Verbosity # min :: Verbosity -> Verbosity -> Verbosity #

trace' :: Verbosity -> Verbosity -> String -> a -> a Source #

traceTypeCheck :: Verbosity -> String -> TypeCheck var a -> TypeCheck var a Source #

localVerbosity :: Verbosity -> TypeCheck var a -> TypeCheck var a Source #

localRenderBackend :: Maybe RenderBackend -> TypeCheck var a -> TypeCheck var a Source #

data Covariance Source #

Constructors

Covariant	Positive position.
Contravariant	Negative position

data RenderBackend Source #

Constructors

RenderSVG
RenderLaTeX

data ScopeInfo var Source #

Constructors

ScopeInfo
Fields scopeName :: Maybe SectionName scopeVars :: [(var, VarInfo var)]

Instances

Instances details

Foldable ScopeInfo Source #
Instance details Defined in Rzk.TypeCheck Methods fold :: Monoid m => ScopeInfo m -> m # foldMap :: Monoid m => (a -> m) -> ScopeInfo a -> m # foldMap' :: Monoid m => (a -> m) -> ScopeInfo a -> m # foldr :: (a -> b -> b) -> b -> ScopeInfo a -> b # foldr' :: (a -> b -> b) -> b -> ScopeInfo a -> b # foldl :: (b -> a -> b) -> b -> ScopeInfo a -> b # foldl' :: (b -> a -> b) -> b -> ScopeInfo a -> b # foldr1 :: (a -> a -> a) -> ScopeInfo a -> a # foldl1 :: (a -> a -> a) -> ScopeInfo a -> a # toList :: ScopeInfo a -> [a] # null :: ScopeInfo a -> Bool # length :: ScopeInfo a -> Int # elem :: Eq a => a -> ScopeInfo a -> Bool # maximum :: Ord a => ScopeInfo a -> a # minimum :: Ord a => ScopeInfo a -> a # sum :: Num a => ScopeInfo a -> a # product :: Num a => ScopeInfo a -> a #
Functor ScopeInfo Source #
Instance details Defined in Rzk.TypeCheck Methods fmap :: (a -> b) -> ScopeInfo a -> ScopeInfo b # (<$) :: a -> ScopeInfo b -> ScopeInfo a #

addVarToScope :: var -> VarInfo var -> ScopeInfo var -> ScopeInfo var Source #

data VarInfo var Source #

Constructors

VarInfo
Fields varType :: TermT var varValue :: Maybe (TermT var) varOrig :: Maybe VarIdent varIsAssumption :: Bool varDeclaredAssumptions :: [var] varLocation :: Maybe LocationInfo

Instances

Instances details

Foldable VarInfo Source #
Instance details Defined in Rzk.TypeCheck Methods fold :: Monoid m => VarInfo m -> m # foldMap :: Monoid m => (a -> m) -> VarInfo a -> m # foldMap' :: Monoid m => (a -> m) -> VarInfo a -> m # foldr :: (a -> b -> b) -> b -> VarInfo a -> b # foldr' :: (a -> b -> b) -> b -> VarInfo a -> b # foldl :: (b -> a -> b) -> b -> VarInfo a -> b # foldl' :: (b -> a -> b) -> b -> VarInfo a -> b # foldr1 :: (a -> a -> a) -> VarInfo a -> a # foldl1 :: (a -> a -> a) -> VarInfo a -> a # toList :: VarInfo a -> [a] # null :: VarInfo a -> Bool # length :: VarInfo a -> Int # elem :: Eq a => a -> VarInfo a -> Bool # maximum :: Ord a => VarInfo a -> a # minimum :: Ord a => VarInfo a -> a # sum :: Num a => VarInfo a -> a # product :: Num a => VarInfo a -> a #
Functor VarInfo Source #
Instance details Defined in Rzk.TypeCheck Methods fmap :: (a -> b) -> VarInfo a -> VarInfo b # (<$) :: a -> VarInfo b -> VarInfo a #

data Context var Source #

Constructors

Context
Fields localScopes :: [ScopeInfo var] localTopes :: [TermT var] localTopesNF :: [TermT var] localTopesNFUnion :: [[TermT var]] localTopesEntailBottom :: Bool actionStack :: [Action var] currentCommand :: Maybe Command location :: Maybe LocationInfo verbosity :: Verbosity covariance :: Covariance renderBackend :: Maybe RenderBackend

Instances

Instances details

Foldable Context Source #
Instance details Defined in Rzk.TypeCheck Methods fold :: Monoid m => Context m -> m # foldMap :: Monoid m => (a -> m) -> Context a -> m # foldMap' :: Monoid m => (a -> m) -> Context a -> m # foldr :: (a -> b -> b) -> b -> Context a -> b # foldr' :: (a -> b -> b) -> b -> Context a -> b # foldl :: (b -> a -> b) -> b -> Context a -> b # foldl' :: (b -> a -> b) -> b -> Context a -> b # foldr1 :: (a -> a -> a) -> Context a -> a # foldl1 :: (a -> a -> a) -> Context a -> a # toList :: Context a -> [a] # null :: Context a -> Bool # length :: Context a -> Int # elem :: Eq a => a -> Context a -> Bool # maximum :: Ord a => Context a -> a # minimum :: Ord a => Context a -> a # sum :: Num a => Context a -> a # product :: Num a => Context a -> a #
Functor Context Source #
Instance details Defined in Rzk.TypeCheck Methods fmap :: (a -> b) -> Context a -> Context b # (<$) :: a -> Context b -> Context a #

addVarInCurrentScope :: var -> VarInfo var -> Context var -> Context var Source #

emptyContext :: Context var Source #

askCurrentScope :: TypeCheck var (ScopeInfo var) Source #

varInfos :: Context var -> [(var, VarInfo var)] Source #

varTypes :: Context var -> [(var, TermT var)] Source #

varValues :: Context var -> [(var, Maybe (TermT var))] Source #

varOrigs :: Context var -> [(var, Maybe VarIdent)] Source #

withPartialDecls :: TypeCheck VarIdent ([Decl'], [err]) -> TypeCheck VarIdent ([Decl'], [err]) -> TypeCheck VarIdent ([Decl'], [err]) Source #

withSection :: Maybe SectionName -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent]) -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent]) -> TypeCheck VarIdent ([Decl VarIdent], [TypeErrorInScopedContext VarIdent]) Source #

startSection :: Maybe SectionName -> TypeCheck VarIdent a -> TypeCheck VarIdent a Source #

endSection :: [TypeErrorInScopedContext VarIdent] -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) Source #

scopeToDecls :: Eq var => [TypeErrorInScopedContext var] -> ScopeInfo var -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var]) Source #

insertExplicitAssumptionFor :: Eq var => var -> (var, VarInfo var) -> TermT var -> TermT var Source #

insertExplicitAssumptionFor' :: Eq var => var -> (var, VarInfo var) -> VarInfo var -> VarInfo var Source #

makeAssumptionExplicit :: Eq var => (var, VarInfo var) -> [(var, VarInfo var)] -> TypeCheck var (Bool, [(var, VarInfo var)]) Source #

collectScopeDecls :: Eq var => [TypeErrorInScopedContext var] -> [(var, VarInfo var)] -> [(var, VarInfo var)] -> TypeCheck var ([Decl var], [TypeErrorInScopedContext var]) Source #

abstractAssumption :: Eq var => (var, VarInfo var) -> Decl var -> Decl var Source #

data OutputDirection Source #

Constructors

TopDown
BottomUp

Instances

Instances details

Eq OutputDirection Source #
Instance details Defined in Rzk.TypeCheck Methods (==) :: OutputDirection -> OutputDirection -> Bool # (/=) :: OutputDirection -> OutputDirection -> Bool #

block :: OutputDirection -> [String] -> String Source #

namedBlock :: OutputDirection -> String -> [String] -> String Source #

ppContext' :: OutputDirection -> Context VarIdent -> String Source #

doesShadowName :: VarIdent -> TypeCheck var [VarIdent] Source #

checkTopLevelDuplicate :: VarIdent -> TypeCheck var () Source #

checkNameShadowing :: VarIdent -> TypeCheck var () Source #

withLocation :: LocationInfo -> TypeCheck var a -> TypeCheck var a Source #

withCommand :: Command -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) -> TypeCheck VarIdent ([Decl'], [TypeErrorInScopedContext VarIdent]) Source #

localDecls :: [Decl VarIdent] -> TypeCheck VarIdent a -> TypeCheck VarIdent a Source #

localDeclsPrepared :: [Decl VarIdent] -> TypeCheck VarIdent a -> TypeCheck VarIdent a Source #

localDecl :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a Source #

localDeclPrepared :: Decl VarIdent -> TypeCheck VarIdent a -> TypeCheck VarIdent a Source #

type TypeCheck var = ReaderT (Context var) (Except (TypeErrorInScopedContext var)) Source #

freeVarsT_ :: Eq var => TermT var -> TypeCheck var [var] Source #

traceStartAndFinish :: Show a => String -> a -> a Source #

entail :: Eq var => [TermT var] -> TermT var -> Bool Source #

entailM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool Source #

entailTraceM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool Source #

nubTermT :: Eq var => [TermT var] -> [TermT var] Source #

saturateTopes :: Eq var => [TermT var] -> [TermT var] -> [TermT var] Source #

saturateWith :: (a -> [a] -> Bool) -> ([a] -> [a] -> [a]) -> [a] -> [a] Source #

generateTopes :: Eq var => [TermT var] -> [TermT var] -> [TermT var] Source #

generateTopesForPoints :: Eq var => [TermT var] -> [TermT var] Source #

generateTopesForPointsM :: Eq var => [TermT var] -> TypeCheck var [TermT var] Source #

allTopePoints :: Eq var => TermT var -> [TermT var] Source #

topePoints :: TermT var -> [TermT var] Source #

subPoints :: TermT var -> [TermT var] Source #

simplifyLHSwithDisjunctions :: Eq var => [TermT var] -> [[TermT var]] Source #

Simplify the context, including disjunctions. See also simplifyLHS.

simplifyLHS :: Eq var => [TermT var] -> [TermT var] Source #

Simplify the context, except disjunctions. See also simplifyLHSwithDisjunctions.

solveRHSM :: Eq var => [TermT var] -> TermT var -> TypeCheck var Bool Source #

solveRHS :: Eq var => [TermT var] -> TermT var -> Bool Source #

checkTope :: Eq var => TermT var -> TypeCheck var Bool Source #

checkTopeEntails :: Eq var => TermT var -> TypeCheck var Bool Source #

checkEntails :: Eq var => TermT var -> TermT var -> TypeCheck var Bool Source #

contextEntailedBy :: Eq var => TermT var -> TypeCheck var () Source #

contextEntails :: Eq var => TermT var -> TypeCheck var () Source #

topesEquiv :: Eq var => TermT var -> TermT var -> TypeCheck var Bool Source #

contextEquiv :: Eq var => [TermT var] -> TypeCheck var () Source #

switchVariance :: TypeCheck var a -> TypeCheck var a Source #

enterScopeContext :: Maybe VarIdent -> TermT var -> Context var -> Context (Inc var) Source #

enterScope :: Maybe VarIdent -> TermT var -> TypeCheck (Inc var) b -> TypeCheck var b Source #

performing :: Eq var => Action var -> TypeCheck var a -> TypeCheck var a Source #

stripTypeRestrictions :: TermT var -> TermT var Source #

etaMatch :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var (TermT var, TermT var) Source #

Perform at most one $\eta$-expansion at the top-level to assist unification.

etaExpand :: Eq var => TermT var -> TypeCheck var (TermT var) Source #

inCubeLayer :: Eq var => TermT var -> TypeCheck var Bool Source #

inTopeLayer :: Eq var => TermT var -> TypeCheck var Bool Source #

tryRestriction :: Eq var => TermT var -> TypeCheck var (Maybe (TermT var)) Source #

whnfT :: Eq var => TermT var -> TypeCheck var (TermT var) Source #

Compute a typed term to its WHNF.

>>> unsafeTypeCheck' $ whnfT "(\\ (x : Unit) -> x) unit"
unit : Unit

nfTope :: Eq var => TermT var -> TypeCheck var (TermT var) Source #

nfT :: Eq var => TermT var -> TypeCheck var (TermT var) Source #

Compute a typed term to its NF.

>>> unsafeTypeCheck' $ nfT "(\\ (x : Unit) -> x) unit"
unit : Unit

checkDefinedVar :: VarIdent -> TypeCheck VarIdent () Source #

valueOfVar :: Eq var => var -> TypeCheck var (Maybe (TermT var)) Source #

typeOfVar :: Eq var => var -> TypeCheck var (TermT var) Source #

typeOfUncomputed :: Eq var => TermT var -> TypeCheck var (TermT var) Source #

typeOf :: Eq var => TermT var -> TypeCheck var (TermT var) Source #

unifyTopes :: Eq var => TermT var -> TermT var -> TypeCheck var () Source #

inAllSubContexts :: TypeCheck var () -> TypeCheck var () -> TypeCheck var () Source #

unify :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var () Source #

unifyViaDecompose :: Eq var => TermT var -> TermT var -> TypeCheck var () Source #

unifyInCurrentContext :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var () Source #

unifyTypes :: Eq var => TermT var -> TermT var -> TermT var -> TypeCheck var () Source #

unifyTerms :: Eq var => TermT var -> TermT var -> TypeCheck var () Source #

localTope :: Eq var => TermT var -> TypeCheck var a -> TypeCheck var a Source #

universeT :: TermT var Source #

cubeT :: TermT var Source #

topeT :: TermT var Source #

topeEQT :: TermT var -> TermT var -> TermT var Source #

topeLEQT :: TermT var -> TermT var -> TermT var Source #

topeOrT :: TermT var -> TermT var -> TermT var Source #

topeAndT :: TermT var -> TermT var -> TermT var Source #

cubeProductT :: TermT var -> TermT var -> TermT var Source #

cubeUnitT :: TermT var Source #

cubeUnitStarT :: TermT var Source #

typeUnitT :: TermT var Source #

unitT :: TermT var Source #

cube2T :: TermT var Source #

cube2_0T :: TermT var Source #

cube2_1T :: TermT var Source #

topeTopT :: TermT var Source #

topeBottomT :: TermT var Source #

recBottomT :: TermT var Source #

typeRestrictedT :: TermT var -> [(TermT var, TermT var)] -> TermT var Source #

lambdaT :: TermT var -> Maybe VarIdent -> Maybe (TermT var, Maybe (Scope TermT var)) -> Scope TermT var -> TermT var Source #

appT :: TermT var -> TermT var -> TermT var -> TermT var Source #

pairT :: TermT var -> TermT var -> TermT var -> TermT var Source #

firstT :: TermT var -> TermT var -> TermT var Source #

secondT :: TermT var -> TermT var -> TermT var Source #

reflT :: TermT var -> Maybe (TermT var, Maybe (TermT var)) -> TermT var Source #

typeFunT :: Maybe VarIdent -> TermT var -> Maybe (Scope TermT var) -> Scope TermT var -> TermT var Source #

typeSigmaT :: Maybe VarIdent -> TermT var -> Scope TermT var -> TermT var Source #

recOrT :: TermT var -> [(TermT var, TermT var)] -> TermT var Source #

typeIdT :: TermT var -> Maybe (TermT var) -> TermT var -> TermT var Source #

idJT :: TermT var -> TermT var -> TermT var -> TermT var -> TermT var -> TermT var -> TermT var -> TermT var Source #

typeAscT :: TermT var -> TermT var -> TermT var Source #

typecheck :: Eq var => Term var -> TermT var -> TypeCheck var (TermT var) Source #

inferAs :: Eq var => TermT var -> Term var -> TypeCheck var (TermT var) Source #

infer :: Eq var => Term var -> TypeCheck var (TermT var) Source #

checkCoherence :: Eq var => (TermT var, TermT var) -> (TermT var, TermT var) -> TypeCheck var () Source #

inferStandalone :: Eq var => Term var -> Either (TypeErrorInScopedContext var) (TermT var) Source #

unsafeInferStandalone' :: Term' -> TermT' Source #

unsafeTypeCheck' :: TypeCheck VarIdent a -> a Source #

type PointId = String Source #

type ShapeId = [PointId] Source #

cube2powerT :: Int -> TermT var Source #

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

verticesFrom :: [TermT var] -> [(ShapeId, TermT var)] Source #

subTopes2 :: Int -> TermT var -> [(ShapeId, TermT var)] Source #

cubeSubTopes :: [(ShapeId, TermT (Inc var))] Source #

limitLength :: Int -> String -> String Source #

renderObjectsFor :: Eq var => String -> Int -> TermT var -> TermT var -> TypeCheck var [(ShapeId, RenderObjectData)] Source #

componentWiseEQT :: Int -> TermT var -> TermT var -> TermT var Source #

renderObjectsInSubShapeFor :: Eq var => String -> Int -> [var] -> var -> TermT var -> TermT var -> TermT var -> TypeCheck var [(ShapeId, RenderObjectData)] Source #

renderForSubShapeSVG :: Eq var => String -> Int -> [var] -> var -> TermT var -> TermT var -> TermT var -> TypeCheck var String Source #

renderForSVG :: Eq var => String -> Int -> TermT var -> TermT var -> TypeCheck var String Source #

renderTermSVGFor Source #

Arguments

:: Eq var
=> String	Main color.
-> Int	Accumulated dimensions so far (from 0 to 3).
-> (Maybe (TermT var, TermT var), [var])	Accumulated point term (and its time).
-> TermT var	Term to render.
-> TypeCheck var (Maybe String)

renderTermSVG :: Eq var => TermT var -> TypeCheck var (Maybe String) Source #

renderTermSVG' :: Eq var => TermT var -> TypeCheck var (Maybe String) Source #

type Point2D a = (a, a) Source #

type Point3D a = (a, a, a) Source #

type Edge3D a = (Point3D a, Point3D a) Source #

type Face3D a = (Point3D a, Point3D a, Point3D a) Source #

type Volume3D a = (Point3D a, Point3D a, Point3D a, Point3D a) Source #

data CubeCoords2D a b Source #

Constructors

CubeCoords2D
Fields vertices :: [(Point3D a, Point2D b)] edges :: [(Edge3D a, (Point2D b, Point2D b))] faces :: [(Face3D a, (Point2D b, Point2D b, Point2D b))] volumes :: [(Volume3D a, (Point2D b, Point2D b, Point2D b, Point2D b))]