| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Rzk.TypeCheck
Synopsis
- defaultTypeCheck :: TypeCheck VarIdent a -> Either (TypeErrorInScopedContext VarIdent) a
- data Decl var = Decl {}
- type Decl' = Decl VarIdent
- typecheckModulesWithLocation :: [(FilePath, Module)] -> TypeCheck VarIdent ()
- typecheckModules :: [Module] -> TypeCheck VarIdent ()
- typecheckModuleWithLocation :: (FilePath, Module) -> TypeCheck VarIdent [Decl']
- typecheckModule :: Module -> TypeCheck VarIdent [Decl']
- 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
- 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 :: TypeErrorInContext VarIdent -> String
- ppTypeErrorInScopedContextWith' :: [VarIdent] -> [VarIdent] -> TypeErrorInScopedContext VarIdent -> String
- ppTypeErrorInScopedContext' :: TypeErrorInScopedContext VarIdent -> String
- 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)
- 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 {}
- data Verbosity
- 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
- data RenderBackend
- data Context var = Context {
- varTypes :: [(var, TermT var)]
- varValues :: [(var, Maybe (TermT var))]
- varOrigs :: [(var, Maybe VarIdent)]
- 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
- emptyContext :: Context var
- ppContext' :: Context VarIdent -> String
- doesShadowName :: VarIdent -> TypeCheck var Bool
- checkTopLevelDuplicate :: VarIdent -> TypeCheck var ()
- checkNameShadowing :: VarIdent -> TypeCheck var ()
- withLocation :: LocationInfo -> TypeCheck var a -> TypeCheck var a
- withCommand :: Command -> TypeCheck var a -> TypeCheck var a
- 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))
- showSomeTermTs :: Eq var => [TermT var] -> String
- traceStartAndFinish :: Show a => String -> a -> a
- entail :: Eq var => [TermT var] -> TermT 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]
- allTopePoints :: Eq var => TermT var -> [TermT var]
- topePoints :: TermT var -> [TermT var]
- subPoints :: TermT var -> [TermT var]
- simplifyLHS :: Eq var => [TermT var] -> [[TermT var]]
- 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)
- 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 ()
- 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
- 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'
- 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 {}
- 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 {}
- renderCube :: (Floating a, Show a) => Camera a -> a -> (String -> Maybe RenderObjectData) -> String
- defaultCamera :: Floating a => Camera a
Documentation
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 |
Instances
| Foldable TypeError Source # | |
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] # length :: TypeError a -> Int # elem :: Eq a => a -> TypeError a -> Bool # maximum :: Ord a => TypeError a -> a # minimum :: Ord a => TypeError a -> a # | |
| Functor TypeError Source # | |
data TypeErrorInContext var Source #
Constructors
| TypeErrorInContext | |
Fields
| |
Instances
data TypeErrorInScopedContext var Source #
Constructors
| PlainTypeError (TypeErrorInContext var) | |
| ScopedTypeError (Maybe VarIdent) (TypeErrorInScopedContext (Inc var)) |
Instances
type TypeError' = TypeError VarIdent Source #
ppTypeError' :: TypeError' -> String Source #
ppTypeErrorInScopedContextWith' :: [VarIdent] -> [VarIdent] -> TypeErrorInScopedContext VarIdent -> String Source #
issueTypeError :: TypeError var -> TypeCheck var a Source #
panicImpossible :: String -> a 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) |
Instances
| Foldable Action Source # | |
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 # elem :: Eq a => a -> Action a -> Bool # maximum :: Ord a => Action a -> a # minimum :: Ord a => Action a -> a # | |
| Functor Action Source # | |
traceAction' :: Int -> Action' -> a -> a Source #
unsafeTraceAction' :: Int -> Action var -> a -> a Source #
data LocationInfo Source #
Constructors
| LocationInfo | |
Fields | |
Instances
| Eq Verbosity Source # | |
| Ord Verbosity 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 |
Constructors
| Context | |
Fields
| |
Instances
| Foldable Context Source # | |
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 # elem :: Eq a => a -> Context a -> Bool # maximum :: Ord a => Context a -> a # minimum :: Ord a => Context a -> a # | |
| Functor Context Source # | |
emptyContext :: Context var Source #
checkTopLevelDuplicate :: VarIdent -> TypeCheck var () Source #
checkNameShadowing :: VarIdent -> TypeCheck var () Source #
withLocation :: LocationInfo -> TypeCheck var a -> TypeCheck var a Source #
traceStartAndFinish :: Show a => String -> a -> a Source #
saturateWith :: (a -> [a] -> Bool) -> ([a] -> [a] -> [a]) -> [a] -> [a] Source #
topePoints :: TermT var -> [TermT var] Source #
switchVariance :: 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.
whnfT :: Eq var => TermT var -> TypeCheck var (TermT var) Source #
Compute a typed term to its WHNF.
>>>whnfT "(\\p -> first (second p)) (x, (y, z))" :: Term'y
nfT :: Eq var => TermT var -> TypeCheck var (TermT var) Source #
Compute a typed term to its NF.
>>>nfT "(\\p -> first (second p)) (x, (y, z))" :: Term'y
unifyInCurrentContext :: Eq var => Maybe (TermT var) -> TermT var -> TermT var -> TypeCheck var () Source #
cubeUnitStarT :: TermT var Source #
topeBottomT :: TermT var Source #
recBottomT :: TermT var Source #
lambdaT :: TermT var -> Maybe VarIdent -> Maybe (TermT var, Maybe (Scope TermT var)) -> Scope TermT var -> TermT var Source #
typeFunT :: Maybe VarIdent -> TermT var -> Maybe (Scope TermT var) -> Scope TermT var -> TermT var Source #
idJT :: TermT var -> TermT var -> TermT var -> TermT var -> TermT var -> TermT var -> TermT 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 #
cube2powerT :: Int -> TermT var Source #
renderObjectsFor :: Eq var => String -> Int -> TermT var -> TermT var -> TypeCheck var [(ShapeId, RenderObjectData)] 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 #
data CubeCoords2D a b Source #
Constructors
| Camera | |
Fields
| |
fromAffine :: Fractional a => Vector4D a -> (Point2D a, a) Source #
data RenderObjectData Source #
Constructors
| RenderObjectData | |
renderCube :: (Floating a, Show a) => Camera a -> a -> (String -> Maybe RenderObjectData) -> String Source #
defaultCamera :: Floating a => Camera a Source #