| Safe Haskell | None |
|---|---|
| Language | Haskell98 |
TypeChecker
Synopsis
- traceCheck :: String -> a -> a
- traceCheckM :: Monad m => String -> m ()
- traceSing :: String -> a -> a
- traceSingM :: Monad m => String -> m ()
- traceAdm :: String -> a -> a
- traceAdmM :: Monad m => String -> m ()
- doNf :: Signature -> Expr -> IO (Either TraceError (Expr, TCState))
- doWhnf :: Signature -> Expr -> IO (Either TraceError (Val, TCState))
- runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a, TCState))
- typeCheck :: [Declaration] -> IO (Either TraceError ([EDeclaration], TCState))
- echo :: MonadIO m => String -> m ()
- echoR :: MonadIO m => String -> m ()
- echoTySig :: (Show n, MonadIO m) => n -> Expr -> m ()
- echoKindedTySig :: (Show n, MonadIO m) => Kind -> n -> Expr -> m ()
- echoKindedDef :: (Show n, MonadIO m) => Kind -> n -> Expr -> m ()
- echoEPrefix :: String
- echoTySigE :: (Show n, MonadIO m) => n -> Expr -> m ()
- echoDefE :: (Show n, MonadIO m) => n -> Expr -> m ()
- typeCheckDecls :: [Declaration] -> TypeCheck [EDeclaration]
- typeCheckDeclaration :: Declaration -> TypeCheck [EDeclaration]
- typeCheckMutualSigs :: [Declaration] -> TypeCheck [Kinded (TySig TVal)]
- typeCheckSignature :: TySig Type -> TypeCheck (Kinded (TySig TVal))
- typeCheckMutualSig :: Declaration -> TypeCheck (Kinded (TySig TVal))
- typeCheckMutualBody :: Bool -> Kind -> Declaration -> TypeCheck [EDeclaration]
- typeCheckDataDecl :: Name -> Sized -> Co -> [Pol] -> Telescope -> Type -> [Constructor] -> [Name] -> TypeCheck [EDeclaration]
- insertConstructorTele :: Telescope -> Type -> Constructor -> TypeCheck Constructor
- computeConstructorTele :: Telescope -> Type -> Type -> TypeCheck (Telescope, [Pattern])
- checkConstructorParams :: [Expr] -> TVal -> TypeCheck (TCContext, [Pattern])
- contextToTele :: TCContext -> TypeCheck Telescope
- typeCheckConstructor :: Name -> Type -> Sized -> Co -> [Pol] -> Telescope -> Constructor -> TypeCheck (Bool, Kinded EConstructor)
- typeCheckMeasuredFuns :: Co -> [Fun] -> TypeCheck [EFun]
- typeCheckFunBody :: Co -> Kind -> Fun -> TypeCheck EFun
- typeCheckFuns :: Co -> [Fun] -> TypeCheck [EFun]
- addFunSig :: Co -> Kinded Fun -> TypeCheck ()
- admCheckFunSig :: Co -> [Name] -> TypeSig -> [Clause] -> TypeCheck [Clause]
- enableSig :: Kind -> Fun -> TypeCheck ()
- typeCheckFunSig :: Fun -> TypeCheck (Kinded ETypeSig)
- typeCheckFunClauses :: Fun -> TypeCheck (Kinded [EClause])
- checkConType :: Sized -> Expr -> TypeCheck (Kinded Extr)
- checkConType' :: Expr -> TypeCheck (Kinded Extr)
- checkTarget :: Name -> TVal -> Telescope -> Type -> TypeCheck ()
- checkDataType :: Int -> Expr -> TypeCheck (Kinded (Sort Expr, Extr))
- checkSize :: Expr -> TypeCheck Extr
- inferSize :: Expr -> TypeCheck Extr
- checkBelow :: Expr -> LtLe -> Val -> TypeCheck Extr
- checkLevel :: Expr -> TypeCheck (Val, Extr)
- checkExpr :: Expr -> TVal -> TypeCheck (Kinded Extr)
- checkLet :: Dec -> Name -> Telescope -> Maybe Type -> Expr -> Expr -> TVal -> TypeCheck (Kinded Extr)
- checkLetDef :: Dec -> Telescope -> Maybe Type -> Expr -> TypeCheck (TVal, EType, Kinded Extr)
- checkLetBody :: Name -> EType -> TVal -> Kind -> Dec -> Extr -> Expr -> TVal -> TypeCheck (Kinded Extr)
- checkPair :: Expr -> Expr -> Name -> Domain -> FVal -> TypeCheck (Kinded Expr)
- checkForced :: Expr -> TVal -> TypeCheck (Kinded Expr)
- checkConTerm :: ConK -> QName -> [Expr] -> TVal -> TypeCheck (Kinded Extr)
- checkSpine :: [Expr] -> TVal -> TypeCheck ([Kinded (Name, Extr)], TVal)
- maybeErase :: Polarity pol => pol -> Expr -> Expr
- checkApp :: Expr -> TVal -> TypeCheck (Kinded (Name, Extr), TVal)
- checkSubtype :: Expr -> TVal -> TVal -> TypeCheck ()
- ptsRule :: Bool -> Sort Val -> Sort Val -> TypeCheck (Sort Val)
- checkOrInfer :: Dec -> Expr -> Maybe Type -> TypeCheck (TVal, EType, Kinded Extr)
- inferType :: Expr -> TypeCheck (Sort Val, Kinded Extr)
- inferExpr :: Expr -> TypeCheck (TVal, Kinded Extr)
- inferProj :: Expr -> PrePost -> Name -> TypeCheck (TVal, Kinded Extr)
- inferExpr' :: Expr -> TypeCheck (TVal, Kinded Extr)
- checkType :: Expr -> TypeCheck (Kinded Extr)
- checkSmallType :: Expr -> TypeCheck (Kinded Extr)
- checkTele :: Telescope -> TypeCheck a -> TypeCheck (ETelescope, a)
- checkCases :: Val -> TVal -> [Clause] -> TypeCheck (Kinded [EClause])
- checkCases' :: Int -> Val -> TVal -> [Clause] -> TypeCheck (Kinded [EClause])
- checkCase :: Int -> Val -> TVal -> Clause -> TypeCheck (Kinded EClause)
- checkFun :: Type -> [Clause] -> TypeCheck (Kinded [EClause])
- checkClauses :: TVal -> [Clause] -> TypeCheck (Kinded [EClause])
- checkClauses' :: Int -> TVal -> [Clause] -> TypeCheck (Kinded [EClause])
- checkClause :: Int -> TVal -> Clause -> TypeCheck (Kinded EClause)
- type Substitution = Valuation
- emptySub :: Substitution
- sgSub :: Int -> Val -> Substitution
- lookupSub :: Int -> Substitution -> Maybe Val
- type DotFlex = (Int, (Expr, Domain))
- data Goal
- checkPatterns :: Dec -> [Goal] -> Substitution -> TVal -> [Pattern] -> TypeCheck ([Goal], Substitution, TCContext, TVal, [EPattern], [Val], Bool)
- checkPattern :: Dec -> [Goal] -> Substitution -> TVal -> Pattern -> TypeCheck ([Goal], Substitution, TCContext, TVal, EPattern, Val, Bool)
- turnIntoVarPatAtUnitType :: TVal -> Pattern -> TypeCheck Pattern
- checkPattern' :: [Goal] -> Substitution -> Domain -> Pattern -> TypeCheck ([Goal], Substitution, TCContext, EPattern, Val, Bool)
- checkGoal :: Substitution -> Goal -> TypeCheck ()
- checkRHS :: Substitution -> Expr -> TVal -> TypeCheck (Kinded Extr)
- unifyIndices :: [Int] -> Val -> Val -> TypeCheck Substitution
- instWh :: Pol -> [Int] -> TVal -> Val -> Val -> TypeCheck Substitution
- assignFlex :: Int -> Val -> TypeCheck Substitution
- inst :: Pol -> [Int] -> TVal -> Val -> Val -> TypeCheck Substitution
- instList :: [Pol] -> [Int] -> TVal -> [Val] -> [Val] -> TypeCheck Substitution
- instList' :: Int -> [Pol] -> [Int] -> TVal -> [Val] -> [Val] -> TypeCheck Substitution
- headPosl :: [Pol] -> Pol
- tailPosl :: [Pol] -> [Pol]
- isMeta :: [Int] -> Val -> Bool
- class Substitute a where
- substitute :: Substitution -> a -> TypeCheck a
- compSubst :: Substitution -> Substitution -> TypeCheck Substitution
- mkConLType :: Int -> Expr -> (Name, Expr)
- szType :: Co -> Int -> TVal -> TypeCheck ()
- szConstructor :: Name -> Co -> Int -> TVal -> TypeCheck ()
- szSizeVarUsage :: Name -> Co -> Int -> Int -> TVal -> TypeCheck ()
- szSizeVarTarget :: Int -> Int -> TVal -> TypeCheck ()
- szSizeVarDataArgs :: Name -> Int -> Int -> TVal -> TypeCheck ()
- doVParams :: Int -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a
- admFunDef :: Co -> [Clause] -> TVal -> TypeCheck [Clause]
- admClauses :: [Clause] -> TVal -> TypeCheck ([Clause], [Co])
- admClause :: Clause -> TVal -> TypeCheck (Clause, [Co])
- admPatterns :: [(Pattern, Val)] -> TVal -> TypeCheck ([Pattern], [Co])
- lowerSemiCont :: Int -> TVal -> TypeCheck Bool
- docNotLowerSemi :: Int -> TVal -> TypeCheck Doc
- lowerSemiContinuous :: Int -> TVal -> TypeCheck ()
- upperSemiCont :: Int -> TVal -> TypeCheck Bool
- endsInSizedCo :: Int -> TVal -> TypeCheck ()
- endsInSizedCo' :: Bool -> Int -> TVal -> TypeCheck ()
- allTypesOfTuple :: TVal -> [Val] -> TVal -> [ConstructorInfo] -> (TVal -> TypeCheck ()) -> TypeCheck ()
- allComponentTypes :: [FieldInfo] -> Env -> (TVal -> TypeCheck ()) -> TypeCheck ()
- endsInCo :: TVal -> TypeCheck Bool
- admPattern :: Pattern -> TVal -> TypeCheck (Pattern, [Co])
- cannotMatchDeep :: Pattern -> TVal -> TypeCheck ()
- admType :: Int -> TVal -> TypeCheck [Co]
- szUsed :: Co -> Int -> TVal -> TypeCheck Bool
- szCheckIndFun :: [Int] -> TVal -> TypeCheck ()
- szCheckIndFunSize :: Int -> TVal -> TypeCheck ()
- szLowerSemiCont :: Int -> TVal -> TypeCheck ()
- data CoFunType
- = CoFun
- | SizedCoFun Int
- admCoFun :: TVal -> TypeCheck CoFunType
- admEndsInCo :: TVal -> Int -> (Int -> TypeCheck ()) -> TypeCheck CoFunType
- addJob :: Int -> TVal -> (Int -> TypeCheck ()) -> Int -> TypeCheck ()
- szMono :: Co -> Int -> TVal -> TypeCheck ()
- szMonotone :: Int -> TVal -> TypeCheck ()
- szAntitone :: Int -> TVal -> TypeCheck ()
- szInductive :: Int -> TVal -> TypeCheck ()
- szCoInductive :: Int -> TVal -> TypeCheck ()
- szUsed' :: Co -> Int -> TVal -> TypeCheck ()
Documentation
traceCheck :: String -> a -> a Source #
traceCheckM :: Monad m => String -> m () Source #
traceSingM :: Monad m => String -> m () Source #
runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a, TCState)) Source #
typeCheck :: [Declaration] -> IO (Either TraceError ([EDeclaration], TCState)) Source #
echoEPrefix :: String Source #
typeCheckDecls :: [Declaration] -> TypeCheck [EDeclaration] Source #
typeCheckMutualSigs :: [Declaration] -> TypeCheck [Kinded (TySig TVal)] Source #
typeCheckMutualSig :: Declaration -> TypeCheck (Kinded (TySig TVal)) Source #
typeCheckMutualBody :: Bool -> Kind -> Declaration -> TypeCheck [EDeclaration] Source #
typeCheckDataDecl :: Name -> Sized -> Co -> [Pol] -> Telescope -> Type -> [Constructor] -> [Name] -> TypeCheck [EDeclaration] Source #
insertConstructorTele :: Telescope -> Type -> Constructor -> TypeCheck Constructor Source #
computeConstructorTele :: Telescope -> Type -> Type -> TypeCheck (Telescope, [Pattern]) Source #
computeConstructorTele dtel t = return ctel
Computes the constructor telescope from the target.
checkConstructorParams :: [Expr] -> TVal -> TypeCheck (TCContext, [Pattern]) Source #
checkConstructorParams pars tv = return cxt
Checks that parameters pars are patterns elimating the datatype tv.
Returns a context cxt that binds the pattern variables in
left-to-right order.
contextToTele :: TCContext -> TypeCheck Telescope Source #
Precondition: ce is included in the current context.
typeCheckConstructor :: Name -> Type -> Sized -> Co -> [Pol] -> Telescope -> Constructor -> TypeCheck (Bool, Kinded EConstructor) Source #
typeCheckConstructor d dt sz co pols tel (TypeSig c t)
returns True if constructor has recursive argument
checkLet :: Dec -> Name -> Telescope -> Maybe Type -> Expr -> Expr -> TVal -> TypeCheck (Kinded Extr) Source #
checkLet let .x tel : t = e1 in e2
checkLetDef :: Dec -> Telescope -> Maybe Type -> Expr -> TypeCheck (TVal, EType, Kinded Extr) Source #
checkLetDef .x tel : t = e becomes .x : tel -> t = tel -> e
checkLetBody :: Name -> EType -> TVal -> Kind -> Dec -> Extr -> Expr -> TVal -> TypeCheck (Kinded Extr) Source #
checkPair :: Expr -> Expr -> Name -> Domain -> FVal -> TypeCheck (Kinded Expr) Source #
checkPair e1 e2 y dom env b checks Pair e1 e2 against
VQuant Sigma y dom env b.
checkConTerm :: ConK -> QName -> [Expr] -> TVal -> TypeCheck (Kinded Extr) Source #
Check (partially applied) constructor term, eta-expand it and turn it into a named record.
checkApp :: Expr -> TVal -> TypeCheck (Kinded (Name, Extr), TVal) Source #
checking e against (x : A) -> B returns (x,e) and B[e/x]
Pattern checking ------------------------------------------------
type Substitution = Valuation Source #
checkPatterns :: Dec -> [Goal] -> Substitution -> TVal -> [Pattern] -> TypeCheck ([Goal], Substitution, TCContext, TVal, [EPattern], [Val], Bool) Source #
checkPattern :: Dec -> [Goal] -> Substitution -> TVal -> Pattern -> TypeCheck ([Goal], Substitution, TCContext, TVal, EPattern, Val, Bool) Source #
checkPattern' :: [Goal] -> Substitution -> Domain -> Pattern -> TypeCheck ([Goal], Substitution, TCContext, EPattern, Val, Bool) Source #
unifyIndices :: [Int] -> Val -> Val -> TypeCheck Substitution Source #
assignFlex :: Int -> Val -> TypeCheck Substitution Source #
Check occurrence and return singleton substitution.
Substitution into values
class Substitute a where Source #
Overloaded substitution of values for generic values (free variables).
Methods
substitute :: Substitution -> a -> TypeCheck a Source #
Instances
compSubst :: Substitution -> Substitution -> TypeCheck Substitution Source #
"merge" substitutions by first applying the second to the first, then
appending them t[sigma][tau] = t[sigma . tau]
Size checking
check wether the data type is sized type
constructors of sized type
lowerSemiCont :: Int -> TVal -> TypeCheck Bool Source #
Check whether a type is upper semi-continuous.
upperSemiCont :: Int -> TVal -> TypeCheck Bool Source #
Check whether a type is upper semi-continuous.
endsInSizedCo :: Int -> TVal -> TypeCheck () Source #
endsInSizedCo i tv checks that tv is lower semi-continuous in i
and that tv[0/i] = Top.
endsInSizedCo' :: Bool -> Int -> TVal -> TypeCheck () Source #
endsInSizedCo' False i tv checks that tv is lower semi-continuous in i.
endsInSizedCo' True i tv additionally checks that tv[0/i] = Top.
allTypesOfTuple :: TVal -> [Val] -> TVal -> [ConstructorInfo] -> (TVal -> TypeCheck ()) -> TypeCheck () Source #
allTypesOfTyples args dv cis check performs check on all component
types of tuple type tv = d args where dv is the type of d.