Rzk.TypeCheck

Documentation

defaultTypeCheck :: TypeCheck VarIdent a -> Either (TypeErrorInScopedContext VarIdent) a

data Decl var

Constructors

Decl

Fields

• declName :: var
• declType :: TermT var
• declValue :: Maybe (TermT var)

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

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

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

Defined in Rzk.TypeCheck

Methods

fmap :: (a -> b) -> TypeError a -> TypeError b

(<$) :: a -> TypeError b -> TypeError a

data TypeErrorInContext var

Constructors

TypeErrorInContext

Fields

• typeErrorError :: TypeError var
• typeErrorContext :: Context var

Instances

Foldable TypeErrorInContext

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

Defined in Rzk.TypeCheck

Methods

fmap :: (a -> b) -> TypeErrorInContext a -> TypeErrorInContext b

(<$) :: a -> TypeErrorInContext b -> TypeErrorInContext a

data TypeErrorInScopedContext var

Constructors

PlainTypeError (TypeErrorInContext var)

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

Instances

Foldable TypeErrorInScopedContext

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

Defined in Rzk.TypeCheck

Methods

fmap :: (a -> b) -> TypeErrorInScopedContext a -> TypeErrorInScopedContext b

(<$) :: a -> TypeErrorInScopedContext b -> TypeErrorInScopedContext a

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

Constructors

ActionTypeCheck (Term var) (TermT var)

ActionUnify (TermT var) (TermT var) (TermT var)

ActionUnifyTerms (TermT var) (TermT var)

ActionInfer (Term var)

ActionContextEntailedBy (TermT var)

ActionContextEntails (TermT var)

ActionContextEquiv [TermT var]

ActionWHNF (TermT var)

ActionNF (TermT var)

ActionCheckCoherence (TermT var, TermT var) (TermT var, TermT var)

Instances

Foldable Action

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

Defined in Rzk.TypeCheck

Methods

fmap :: (a -> b) -> Action a -> Action b

(<$) :: a -> Action b -> Action a

type Action' = Action VarIdent

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

Constructors

LocationInfo

Fields

• locationFilePath :: Maybe FilePath
• locationLine :: Maybe Int

data Verbosity

Constructors

Debug

Normal

Silent

Instances

Eq Verbosity

Defined in Rzk.TypeCheck

Methods

(==) :: Verbosity -> Verbosity -> Bool

(/=) :: Verbosity -> Verbosity -> Bool

Ord Verbosity

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

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

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

data Covariance

Constructors

Covariant

Positive position.

Contravariant

Negative position

data Context var

Constructors

Context

Fields

• 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

Instances

Foldable Context

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

Defined in Rzk.TypeCheck

Methods

fmap :: (a -> b) -> Context a -> Context b

(<$) :: a -> Context b -> Context a

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

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)

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

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)

Compute a typed term to its WHNF.

>>> whnfT "(\\p -> first (second p)) (x, (y, z))" :: Term'
y

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

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

Compute a typed term to its NF.

>>> nfT "(\\p -> first (second p)) (x, (y, z))" :: Term'
y

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'