rzk-0.7.5: An experimental proof assistant for synthetic ∞-categories
Safe HaskellNone
LanguageHaskell2010

Rzk.TypeCheck

Synopsis

Documentation

>>> :set -XOverloadedStrings

data Decl var Source #

Constructors

Decl 

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 #

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]) 

data TypeError var Source #

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 #

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

data TypeErrorInScopedContext var Source #

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

data Action var Source #

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 #

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

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

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

data LocationInfo Source #

Instances

Instances details
Eq LocationInfo Source # 
Instance details

Defined in Rzk.TypeCheck

data Verbosity Source #

Constructors

Debug 
Normal 
Silent 

Instances

Instances details
Eq Verbosity Source # 
Instance details

Defined in Rzk.TypeCheck

Ord Verbosity Source # 
Instance details

Defined in Rzk.TypeCheck

data Covariance Source #

Constructors

Covariant

Positive position.

Contravariant

Negative position

data ScopeInfo var Source #

Constructors

ScopeInfo 

Fields

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 #

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 #

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 #

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 #

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

freeVarsT_ :: Eq var => TermT var -> TypeCheck var [var] 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 #

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 #

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 #

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

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 #

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 #

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 #

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 #

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

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

subTopes2 :: Int -> TermT var -> [(ShapeId, TermT var)] 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) 

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 #

data CubeCoords2D a b Source #

Constructors

CubeCoords2D 

Fields

data Matrix3D a Source #

Constructors

Matrix3D a a a a a a a a a 

data Matrix4D a Source #

Constructors

Matrix4D a a a a a a a a a a a a a a a a 

data Vector3D a Source #

Constructors

Vector3D a a a 

data Vector4D a Source #

Constructors

Vector4D a a a a 

data Camera a Source #

Constructors

Camera 

point3Dto2D :: Floating a => Camera a -> a -> Point3D a -> (Point2D a, a) Source #

Orphan instances

IsString TermT' Source #

Parse and unsafeInferStandalone'.

Instance details

Methods

fromString :: String -> TermT' #