Safe Haskell	None
Language	Haskell98

TCM

Synopsis

traceSig :: String -> a -> a
traceRew :: String -> a -> a
traceRewM :: Monad m => String -> m ()
traceMeta :: String -> a -> a
traceMetaM :: Monad m => String -> m ()
class (MonadCxt m, MonadSig m, MonadMeta m, MonadError TraceError m) => MonadTCM (m :: Type -> Type)
data OneOrTwo a
- = One a
- | Two a a
name12 :: OneOrTwo Name -> Name
oneOrTwo :: (a -> b) -> (a -> a -> b) -> OneOrTwo a -> b
fromOne :: OneOrTwo a -> a
toTwo :: OneOrTwo a -> OneOrTwo a
first12 :: OneOrTwo a -> a
second12 :: OneOrTwo a -> a
mapSecond12 :: (a -> a) -> OneOrTwo a -> OneOrTwo a
zipWith12 :: (a -> b -> c) -> OneOrTwo a -> OneOrTwo b -> OneOrTwo c
zipWith123 :: (a -> b -> c -> d) -> OneOrTwo a -> OneOrTwo b -> OneOrTwo c -> OneOrTwo d
toList12 :: OneOrTwo a -> [a]
fromList12 :: Show a => [a] -> OneOrTwo a
toMaybe12 :: Show a => [a] -> Maybe (OneOrTwo a)
data TCContext = TCContext {
- context :: SemCxt
- renaming :: Ren
- naming :: Map Int Name
- environ :: Env2
- rewrites :: Rewrites
- sizeRels :: TSO Int
- belowInfty :: [Int]
- bounds :: [Bound Val]
- consistencyCheck :: Bool
- checkingConType :: Bool
- assertionHandling :: AssertionHandling
- impredicative :: Bool
- funsTemplate :: Map Name (Kinded Fun)
- mutualFuns :: Map Name SigDef
- mutualCo :: Co
- mutualNames :: [Name]
- checkingMutualName :: Maybe DefId
- callStack :: [QName]
}
emptyContext :: TCContext
data TCState = TCState {
- signature :: Signature
- metaVars :: MetaVars
- constraints :: Constraints
- positivityGraph :: PositivityGraph
}
type MetaVars = Map MVar MetaVar
emptyMetaVars :: MetaVars
type MScope = [Name]
data MetaVar = MetaVar {
- mscope :: MScope
- solution :: Maybe Val
}
type PosConstrnt = Constrnt PPoly DefId ()
type PositivityGraph = [PosConstrnt]
emptyPosGraph :: PositivityGraph
type TypeCheck = StateT TCState (ReaderT TCContext (ExceptT TraceError IO))
data Rewrite = Rewrite {
- lhs :: Val
- rhs :: Val
}
type Rewrites = [Rewrite]
emptyRewrites :: Rewrites
type Ren = Map Name Int
type Env2 = Environ (OneOrTwo Val)
type Context a = Map Int a
type Context2 a = Context (OneOrTwo a)
data CxtE a = CxtEntry {
- domain :: a
- upperDec :: UDec
}
type CxtEntry = CxtE (OneOrTwo Domain)
type CxtEntry1 = CxtE Domain
data SemCxt = SemCxt {
- len :: Int
- cxt :: Context2 Domain
- upperDecs :: Context UDec
}
cxtEmpty :: SemCxt
cxtPush' :: OneOrTwo Domain -> SemCxt -> SemCxt
cxtPushEntry :: OneOrTwo Domain -> SemCxt -> (Int, SemCxt)
cxtPush :: Domain -> SemCxt -> (Int, SemCxt)
cxtPush2 :: Domain -> Domain -> SemCxt -> (Int, SemCxt)
cxtPushGen :: Name -> SemCxt -> (Int, SemCxt)
cxtSetType :: Int -> Domain -> SemCxt -> SemCxt
lookupM :: (MonadError TraceError m, Show k, Ord k) => k -> Map k v -> m v
cxtLookupGen :: MonadError TraceError m => SemCxt -> Int -> m CxtEntry
cxtLookupName :: MonadError TraceError m => SemCxt -> Ren -> Name -> m CxtEntry
cxtApplyDec :: Dec -> SemCxt -> SemCxt
class Monad m => MonadCxt (m :: Type -> Type) where
- newVar :: Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a
- newWithGen :: Name -> Domain -> (Int -> Val -> m a) -> m a
- new2WithGen :: Name -> (Domain, Domain) -> (Int -> (Val, Val) -> m a) -> m a
- new :: Name -> Domain -> (Val -> m a) -> m a
- new2 :: Name -> (Domain, Domain) -> ((Val, Val) -> m a) -> m a
- new' :: Name -> Domain -> m a -> m a
- newIrr :: Name -> m a -> m a
- addName :: Name -> (Val -> m a) -> m a
- addKindedTypeSigs :: [Kinded (TySig TVal)] -> m a -> m a
- setType :: Int -> Domain -> m a -> m a
- setTypeOfName :: Name -> Domain -> m a -> m a
- genOfName :: Name -> m Int
- nameOfGen :: Int -> m Name
- uniqueName :: Name -> Int -> m Name
- lookupGen :: Int -> m CxtEntry
- lookupGenType2 :: Int -> m (TVal, TVal)
- lookupName :: Name -> m CxtEntry
- lookupName1 :: Name -> m CxtEntry1
- getContextTele :: m TeleVal
- getLen :: m Int
- getEnv :: m Env
- getRen :: m Ren
- applyDec :: Dec -> m a -> m a
- resurrect :: m a -> m a
- addRewrite :: Rewrite -> [Val] -> ([Val] -> m a) -> m a
- addPattern :: TVal -> Pattern -> Env -> (TVal -> Val -> Env -> m a) -> m a
- addPatterns :: TVal -> [Pattern] -> Env -> (TVal -> [Val] -> Env -> m a) -> m a
- addSizeRel :: Int -> Int -> Int -> m a -> m a
- addBelowInfty :: Int -> m a -> m a
- addBoundHyp :: Bound Val -> m a -> m a
- isBelowInfty :: Int -> m Bool
- sizeVarBelow :: Int -> Int -> m (Maybe Int)
- getMinSize :: Int -> m (Maybe Int)
- getSizeVarsInScope :: m [Name]
- checkingCon :: Bool -> m a -> m a
- checkingDom :: m a -> m a
- setCo :: Co -> m a -> m a
- installFuns :: Co -> [Kinded Fun] -> m a -> m a
- setMeasure :: Measure Val -> m a -> m a
- activateFuns :: m a -> m a
- goImpredicative :: m a -> m a
- checkingMutual :: Maybe DefId -> m a -> m a
dontCare :: a
underAbs :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a
underAbs_ :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a
noConsistencyChecking :: TypeCheck a -> TypeCheck a
underAbs' :: Name -> FVal -> (Val -> Val -> TypeCheck a) -> TypeCheck a
addBind :: TBind -> TypeCheck a -> TypeCheck a
addBinds :: Telescope -> TypeCheck a -> TypeCheck a
introPatterns :: [Pattern] -> TVal -> ([(Pattern, Val)] -> TVal -> TypeCheck a) -> TypeCheck a
introPatVar :: Pattern -> TypeCheck a -> TypeCheck a
introPatVars :: [Pattern] -> TypeCheck a -> TypeCheck a
introPatType :: (Pattern, Val) -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a
introPatTypes :: [(Pattern, Val)] -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a
matchPatType :: (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a
type Signature = Map QName SigDef
data SigDef
- = FunSig {
  - isCo :: Co
  - symbTyp :: TVal
  - symbolKind :: Kind
  - arity :: Arity
  - clauses :: [Clause]
  - isTypeChecked :: Bool
  - extrTyp :: Expr
  }
- | LetSig {
  - symbTyp :: TVal
  - symbolKind :: Kind
  - definingVal :: Val
  - extrTyp :: Expr
  }
- | PatSig {
  - patVars :: [Name]
  - definingPat :: Pattern
  - definingVal :: Val
  }
- | ConSig {
  - conPars :: ConPars
  - lhsTyp :: LHSType
  - recOccs :: [Bool]
  - symbTyp :: TVal
  - dataName :: Name
  - dataPars :: Int
  - extrTyp :: Expr
  }
- | DataSig {
  - numPars :: Int
  - positivity :: [Pol]
  - isSized :: Sized
  - isCo :: Co
  - symbTyp :: TVal
  - symbolKind :: Kind
  - constructors :: [ConstructorInfo]
  - etaExpand :: Bool
  - isTuple :: Bool
  - extrTyp :: Expr
  }
type ConPars = Maybe ([Name], [Pattern])
type LHSType = Maybe (Name, TVal)
isEmptyData :: QName -> TypeCheck Bool
isUnitData :: QName -> TypeCheck Bool
undefinedFType :: QName -> Expr
symbKind :: SigDef -> Kind
emptySig :: Signature
data DataView
- = Data Name [Clos]
- | NoData
dataView :: TVal -> TypeCheck DataView
disambigCon :: QName -> TVal -> TypeCheck QName
conType :: QName -> TVal -> TypeCheck TVal
conLType :: QName -> TVal -> TypeCheck TVal
instConType :: QName -> ConPars -> TVal -> Name -> Int -> TVal -> TypeCheck TVal
instConLType :: QName -> ConPars -> TVal -> LHSType -> (Val -> Bool) -> Int -> TVal -> TypeCheck TVal
instConLType' :: QName -> ConPars -> TVal -> Maybe ((Name, TVal), Val -> Bool) -> Maybe Name -> Int -> TVal -> TypeCheck TVal
class MonadCxt m => MonadSig (m :: Type -> Type) where
- lookupSymbTypQ :: QName -> m TVal
- lookupSymbQ :: QName -> m SigDef
- addSigQ :: QName -> SigDef -> m ()
- modifySigQ :: QName -> (SigDef -> SigDef) -> m ()
- setExtrTypQ :: QName -> Expr -> m ()
- lookupSymbTyp :: Name -> m TVal
- lookupSymb :: Name -> m SigDef
- addSig :: Name -> SigDef -> m ()
- modifySig :: Name -> (SigDef -> SigDef) -> m ()
- setExtrTyp :: Name -> Expr -> m ()
lookupSymbInSig :: QName -> TypeCheck SigDef
initSt :: TCState
initWithSig :: Signature -> TCState
class Monad m => MonadMeta (m :: Type -> Type) where
- resetConstraints :: m ()
- mkConstraint :: Val -> Val -> m (Maybe Constraint)
- addMeta :: Ren -> MVar -> m ()
- addLeq :: Val -> Val -> m ()
- addLe :: LtLe -> Val -> Val -> m ()
- solveConstraints :: m Solution
- solveAndModify :: [Expr] -> Env -> m [Expr]
nameOf :: EnvMap -> Int -> Maybe Name
vGenSuccs :: Val -> Int -> (Int, Int)
sizeExprToExpr :: Env -> SizeExpr -> Expr
maxExpr :: [Expr] -> Expr
solToSubst :: Solution -> Env -> Subst

Documentation

traceSig :: String -> a -> a Source #

traceRew :: String -> a -> a Source #

traceRewM :: Monad m => String -> m () Source #

traceMeta :: String -> a -> a Source #

traceMetaM :: Monad m => String -> m () Source #

class (MonadCxt m, MonadSig m, MonadMeta m, MonadError TraceError m) => MonadTCM (m :: Type -> Type) Source #

data OneOrTwo a Source #

Constructors

One a
Two a a

Instances

Instances details

Functor OneOrTwo Source #
Instance details Defined in TCM Methods fmap :: (a -> b) -> OneOrTwo a -> OneOrTwo b # (<$) :: a -> OneOrTwo b -> OneOrTwo a #
Foldable OneOrTwo Source #
Instance details Defined in TCM Methods fold :: Monoid m => OneOrTwo m -> m # foldMap :: Monoid m => (a -> m) -> OneOrTwo a -> m # foldMap' :: Monoid m => (a -> m) -> OneOrTwo a -> m # foldr :: (a -> b -> b) -> b -> OneOrTwo a -> b # foldr' :: (a -> b -> b) -> b -> OneOrTwo a -> b # foldl :: (b -> a -> b) -> b -> OneOrTwo a -> b # foldl' :: (b -> a -> b) -> b -> OneOrTwo a -> b # foldr1 :: (a -> a -> a) -> OneOrTwo a -> a # foldl1 :: (a -> a -> a) -> OneOrTwo a -> a # toList :: OneOrTwo a -> [a] # null :: OneOrTwo a -> Bool # length :: OneOrTwo a -> Int # elem :: Eq a => a -> OneOrTwo a -> Bool # maximum :: Ord a => OneOrTwo a -> a # minimum :: Ord a => OneOrTwo a -> a # sum :: Num a => OneOrTwo a -> a # product :: Num a => OneOrTwo a -> a #
Traversable OneOrTwo Source #
Instance details Defined in TCM Methods traverse :: Applicative f => (a -> f b) -> OneOrTwo a -> f (OneOrTwo b) # sequenceA :: Applicative f => OneOrTwo (f a) -> f (OneOrTwo a) # mapM :: Monad m => (a -> m b) -> OneOrTwo a -> m (OneOrTwo b) # sequence :: Monad m => OneOrTwo (m a) -> m (OneOrTwo a) #
PrettyTCM a => PrettyTCM (OneOrTwo a) Source #
Instance details Defined in PrettyTCM Methods prettyTCM :: OneOrTwo a -> TypeCheck Doc Source #
Substitute v => Substitute (OneOrTwo v) Source #
Instance details Defined in TypeChecker Methods substitute :: Substitution -> OneOrTwo v -> TypeCheck (OneOrTwo v) Source #
Show a => Show (OneOrTwo a) Source #
Instance details Defined in TCM Methods showsPrec :: Int -> OneOrTwo a -> ShowS # show :: OneOrTwo a -> String # showList :: [OneOrTwo a] -> ShowS #
Eq a => Eq (OneOrTwo a) Source #
Instance details Defined in TCM Methods (==) :: OneOrTwo a -> OneOrTwo a -> Bool # (/=) :: OneOrTwo a -> OneOrTwo a -> Bool #
Ord a => Ord (OneOrTwo a) Source #
Instance details Defined in TCM Methods compare :: OneOrTwo a -> OneOrTwo a -> Ordering # (<) :: OneOrTwo a -> OneOrTwo a -> Bool # (<=) :: OneOrTwo a -> OneOrTwo a -> Bool # (>) :: OneOrTwo a -> OneOrTwo a -> Bool # (>=) :: OneOrTwo a -> OneOrTwo a -> Bool # max :: OneOrTwo a -> OneOrTwo a -> OneOrTwo a # min :: OneOrTwo a -> OneOrTwo a -> OneOrTwo a #

name12 :: OneOrTwo Name -> Name Source #

oneOrTwo :: (a -> b) -> (a -> a -> b) -> OneOrTwo a -> b Source #

fromOne :: OneOrTwo a -> a Source #

toTwo :: OneOrTwo a -> OneOrTwo a Source #

first12 :: OneOrTwo a -> a Source #

second12 :: OneOrTwo a -> a Source #

mapSecond12 :: (a -> a) -> OneOrTwo a -> OneOrTwo a Source #

zipWith12 :: (a -> b -> c) -> OneOrTwo a -> OneOrTwo b -> OneOrTwo c Source #

zipWith123 :: (a -> b -> c -> d) -> OneOrTwo a -> OneOrTwo b -> OneOrTwo c -> OneOrTwo d Source #

toList12 :: OneOrTwo a -> [a] Source #

fromList12 :: Show a => [a] -> OneOrTwo a Source #

toMaybe12 :: Show a => [a] -> Maybe (OneOrTwo a) Source #

data TCContext Source #

Constructors

TCContext

Fields

context :: SemCxt
renaming :: Ren
naming :: Map Int Name
environ :: Env2
rewrites :: Rewrites
sizeRels :: TSO Int
belowInfty :: [Int]
bounds :: [Bound Val]
consistencyCheck :: Bool
Do we need to check that new size relations are consistent with every valuation of the current sizeRels? [See ICFP 2013 paper]
checkingConType :: Bool
assertionHandling :: AssertionHandling
impredicative :: Bool
funsTemplate :: Map Name (Kinded Fun)
mutualFuns :: Map Name SigDef
mutualCo :: Co
mutualNames :: [Name]
The defined names of the current mutual block (and parents).
checkingMutualName :: Maybe DefId
callStack :: [QName]
Used to avoid looping when going into recursive data definitions.

Instances

Instances details

MonadCxt TypeCheck Source #
Instance details Defined in TCM Methods newVar :: Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> TypeCheck a) -> TypeCheck a Source # newWithGen :: Name -> Domain -> (Int -> Val -> TypeCheck a) -> TypeCheck a Source # new2WithGen :: Name -> (Domain, Domain) -> (Int -> (Val, Val) -> TypeCheck a) -> TypeCheck a Source # new :: Name -> Domain -> (Val -> TypeCheck a) -> TypeCheck a Source # new2 :: Name -> (Domain, Domain) -> ((Val, Val) -> TypeCheck a) -> TypeCheck a Source # new' :: Name -> Domain -> TypeCheck a -> TypeCheck a Source # newIrr :: Name -> TypeCheck a -> TypeCheck a Source # addName :: Name -> (Val -> TypeCheck a) -> TypeCheck a Source # addKindedTypeSigs :: [Kinded (TySig TVal)] -> TypeCheck a -> TypeCheck a Source # setType :: Int -> Domain -> TypeCheck a -> TypeCheck a Source # setTypeOfName :: Name -> Domain -> TypeCheck a -> TypeCheck a Source # genOfName :: Name -> TypeCheck Int Source # nameOfGen :: Int -> TypeCheck Name Source # uniqueName :: Name -> Int -> TypeCheck Name Source # lookupGen :: Int -> TypeCheck CxtEntry Source # lookupGenType2 :: Int -> TypeCheck (TVal, TVal) Source # lookupName :: Name -> TypeCheck CxtEntry Source # lookupName1 :: Name -> TypeCheck CxtEntry1 Source # getContextTele :: TypeCheck TeleVal Source # getLen :: TypeCheck Int Source # getEnv :: TypeCheck Env Source # getRen :: TypeCheck Ren Source # applyDec :: Dec -> TypeCheck a -> TypeCheck a Source # resurrect :: TypeCheck a -> TypeCheck a Source # addRewrite :: Rewrite -> [Val] -> ([Val] -> TypeCheck a) -> TypeCheck a Source # addPattern :: TVal -> Pattern -> Env -> (TVal -> Val -> Env -> TypeCheck a) -> TypeCheck a Source # addPatterns :: TVal -> [Pattern] -> Env -> (TVal -> [Val] -> Env -> TypeCheck a) -> TypeCheck a Source # addSizeRel :: Int -> Int -> Int -> TypeCheck a -> TypeCheck a Source # addBelowInfty :: Int -> TypeCheck a -> TypeCheck a Source # addBoundHyp :: Bound Val -> TypeCheck a -> TypeCheck a Source # isBelowInfty :: Int -> TypeCheck Bool Source # sizeVarBelow :: Int -> Int -> TypeCheck (Maybe Int) Source # getMinSize :: Int -> TypeCheck (Maybe Int) Source # getSizeVarsInScope :: TypeCheck [Name] Source # checkingCon :: Bool -> TypeCheck a -> TypeCheck a Source # checkingDom :: TypeCheck a -> TypeCheck a Source # setCo :: Co -> TypeCheck a -> TypeCheck a Source # installFuns :: Co -> [Kinded Fun] -> TypeCheck a -> TypeCheck a Source # setMeasure :: Measure Val -> TypeCheck a -> TypeCheck a Source # activateFuns :: TypeCheck a -> TypeCheck a Source # goImpredicative :: TypeCheck a -> TypeCheck a Source # checkingMutual :: Maybe DefId -> TypeCheck a -> TypeCheck a Source #
MonadMeta TypeCheck Source #
Instance details Defined in TCM Methods resetConstraints :: TypeCheck () Source # mkConstraint :: Val -> Val -> TypeCheck (Maybe Constraint) Source # addMeta :: Ren -> MVar -> TypeCheck () Source # addLeq :: Val -> Val -> TypeCheck () Source # addLe :: LtLe -> Val -> Val -> TypeCheck () Source # solveConstraints :: TypeCheck Solution Source # solveAndModify :: [Expr] -> Env -> TypeCheck [Expr] Source #
MonadSig TypeCheck Source #
Instance details Defined in TCM Methods lookupSymbTypQ :: QName -> TypeCheck TVal Source # lookupSymbQ :: QName -> TypeCheck SigDef Source # addSigQ :: QName -> SigDef -> TypeCheck () Source # modifySigQ :: QName -> (SigDef -> SigDef) -> TypeCheck () Source # setExtrTypQ :: QName -> Expr -> TypeCheck () Source # lookupSymbTyp :: Name -> TypeCheck TVal Source # lookupSymb :: Name -> TypeCheck SigDef Source # addSig :: Name -> SigDef -> TypeCheck () Source # modifySig :: Name -> (SigDef -> SigDef) -> TypeCheck () Source # setExtrTyp :: Name -> Expr -> TypeCheck () Source #
MonadAssert TypeCheck Source #
Instance details Defined in TCM Methods assert :: Bool -> String -> TypeCheck () Source # assertDoc :: Bool -> TypeCheck Doc -> TypeCheck () Source # newAssertionHandling :: AssertionHandling -> TypeCheck a -> TypeCheck a Source # recoverFail :: String -> TypeCheck () Source # recoverFailDoc :: TypeCheck Doc -> TypeCheck () Source #
Show TCContext Source #
Instance details Defined in TCM Methods showsPrec :: Int -> TCContext -> ShowS # show :: TCContext -> String # showList :: [TCContext] -> ShowS #
Monoid (TypeCheck Bool) Source #
Instance details Defined in Eval Methods mempty :: TypeCheck Bool # mappend :: TypeCheck Bool -> TypeCheck Bool -> TypeCheck Bool # mconcat :: [TypeCheck Bool] -> TypeCheck Bool #
Semigroup (TypeCheck Bool) Source #
Instance details Defined in Eval Methods (<>) :: TypeCheck Bool -> TypeCheck Bool -> TypeCheck Bool # sconcat :: NonEmpty (TypeCheck Bool) -> TypeCheck Bool # stimes :: Integral b => b -> TypeCheck Bool -> TypeCheck Bool #

emptyContext :: TCContext Source #

data TCState Source #

Constructors

TCState
Fields signature :: Signature metaVars :: MetaVars constraints :: Constraints positivityGraph :: PositivityGraph

Instances

Instances details

MonadCxt TypeCheck Source #
Instance details Defined in TCM Methods newVar :: Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> TypeCheck a) -> TypeCheck a Source # newWithGen :: Name -> Domain -> (Int -> Val -> TypeCheck a) -> TypeCheck a Source # new2WithGen :: Name -> (Domain, Domain) -> (Int -> (Val, Val) -> TypeCheck a) -> TypeCheck a Source # new :: Name -> Domain -> (Val -> TypeCheck a) -> TypeCheck a Source # new2 :: Name -> (Domain, Domain) -> ((Val, Val) -> TypeCheck a) -> TypeCheck a Source # new' :: Name -> Domain -> TypeCheck a -> TypeCheck a Source # newIrr :: Name -> TypeCheck a -> TypeCheck a Source # addName :: Name -> (Val -> TypeCheck a) -> TypeCheck a Source # addKindedTypeSigs :: [Kinded (TySig TVal)] -> TypeCheck a -> TypeCheck a Source # setType :: Int -> Domain -> TypeCheck a -> TypeCheck a Source # setTypeOfName :: Name -> Domain -> TypeCheck a -> TypeCheck a Source # genOfName :: Name -> TypeCheck Int Source # nameOfGen :: Int -> TypeCheck Name Source # uniqueName :: Name -> Int -> TypeCheck Name Source # lookupGen :: Int -> TypeCheck CxtEntry Source # lookupGenType2 :: Int -> TypeCheck (TVal, TVal) Source # lookupName :: Name -> TypeCheck CxtEntry Source # lookupName1 :: Name -> TypeCheck CxtEntry1 Source # getContextTele :: TypeCheck TeleVal Source # getLen :: TypeCheck Int Source # getEnv :: TypeCheck Env Source # getRen :: TypeCheck Ren Source # applyDec :: Dec -> TypeCheck a -> TypeCheck a Source # resurrect :: TypeCheck a -> TypeCheck a Source # addRewrite :: Rewrite -> [Val] -> ([Val] -> TypeCheck a) -> TypeCheck a Source # addPattern :: TVal -> Pattern -> Env -> (TVal -> Val -> Env -> TypeCheck a) -> TypeCheck a Source # addPatterns :: TVal -> [Pattern] -> Env -> (TVal -> [Val] -> Env -> TypeCheck a) -> TypeCheck a Source # addSizeRel :: Int -> Int -> Int -> TypeCheck a -> TypeCheck a Source # addBelowInfty :: Int -> TypeCheck a -> TypeCheck a Source # addBoundHyp :: Bound Val -> TypeCheck a -> TypeCheck a Source # isBelowInfty :: Int -> TypeCheck Bool Source # sizeVarBelow :: Int -> Int -> TypeCheck (Maybe Int) Source # getMinSize :: Int -> TypeCheck (Maybe Int) Source # getSizeVarsInScope :: TypeCheck [Name] Source # checkingCon :: Bool -> TypeCheck a -> TypeCheck a Source # checkingDom :: TypeCheck a -> TypeCheck a Source # setCo :: Co -> TypeCheck a -> TypeCheck a Source # installFuns :: Co -> [Kinded Fun] -> TypeCheck a -> TypeCheck a Source # setMeasure :: Measure Val -> TypeCheck a -> TypeCheck a Source # activateFuns :: TypeCheck a -> TypeCheck a Source # goImpredicative :: TypeCheck a -> TypeCheck a Source # checkingMutual :: Maybe DefId -> TypeCheck a -> TypeCheck a Source #
MonadMeta TypeCheck Source #
Instance details Defined in TCM Methods resetConstraints :: TypeCheck () Source # mkConstraint :: Val -> Val -> TypeCheck (Maybe Constraint) Source # addMeta :: Ren -> MVar -> TypeCheck () Source # addLeq :: Val -> Val -> TypeCheck () Source # addLe :: LtLe -> Val -> Val -> TypeCheck () Source # solveConstraints :: TypeCheck Solution Source # solveAndModify :: [Expr] -> Env -> TypeCheck [Expr] Source #
MonadSig TypeCheck Source #
Instance details Defined in TCM Methods lookupSymbTypQ :: QName -> TypeCheck TVal Source # lookupSymbQ :: QName -> TypeCheck SigDef Source # addSigQ :: QName -> SigDef -> TypeCheck () Source # modifySigQ :: QName -> (SigDef -> SigDef) -> TypeCheck () Source # setExtrTypQ :: QName -> Expr -> TypeCheck () Source # lookupSymbTyp :: Name -> TypeCheck TVal Source # lookupSymb :: Name -> TypeCheck SigDef Source # addSig :: Name -> SigDef -> TypeCheck () Source # modifySig :: Name -> (SigDef -> SigDef) -> TypeCheck () Source # setExtrTyp :: Name -> Expr -> TypeCheck () Source #
MonadAssert TypeCheck Source #
Instance details Defined in TCM Methods assert :: Bool -> String -> TypeCheck () Source # assertDoc :: Bool -> TypeCheck Doc -> TypeCheck () Source # newAssertionHandling :: AssertionHandling -> TypeCheck a -> TypeCheck a Source # recoverFail :: String -> TypeCheck () Source # recoverFailDoc :: TypeCheck Doc -> TypeCheck () Source #
Monoid (TypeCheck Bool) Source #
Instance details Defined in Eval Methods mempty :: TypeCheck Bool # mappend :: TypeCheck Bool -> TypeCheck Bool -> TypeCheck Bool # mconcat :: [TypeCheck Bool] -> TypeCheck Bool #
Semigroup (TypeCheck Bool) Source #
Instance details Defined in Eval Methods (<>) :: TypeCheck Bool -> TypeCheck Bool -> TypeCheck Bool # sconcat :: NonEmpty (TypeCheck Bool) -> TypeCheck Bool # stimes :: Integral b => b -> TypeCheck Bool -> TypeCheck Bool #

type MetaVars = Map MVar MetaVar Source #

emptyMetaVars :: MetaVars Source #

type MScope Source #

Arguments

= [Name]

names of size variables which are in scope of mvar

data MetaVar Source #

Constructors

MetaVar
Fields mscope :: MScope solution :: Maybe Val

type PosConstrnt = Constrnt PPoly DefId () Source #

type PositivityGraph = [PosConstrnt] Source #

emptyPosGraph :: PositivityGraph Source #

type TypeCheck = StateT TCState (ReaderT TCContext (ExceptT TraceError IO)) Source #

data Rewrite Source #

Constructors

Rewrite
Fields lhs :: Val rhs :: Val

Instances

Instances details

Show Rewrite Source #
Instance details Defined in TCM Methods showsPrec :: Int -> Rewrite -> ShowS # show :: Rewrite -> String # showList :: [Rewrite] -> ShowS #

type Rewrites = [Rewrite] Source #

emptyRewrites :: Rewrites Source #

type Ren = Map Name Int Source #

type Env2 = Environ (OneOrTwo Val) Source #

type Context a = Map Int a Source #

type Context2 a = Context (OneOrTwo a) Source #

data CxtE a Source #

Constructors

CxtEntry
Fields domain :: a upperDec :: UDec

type CxtEntry = CxtE (OneOrTwo Domain) Source #

type CxtEntry1 = CxtE Domain Source #

data SemCxt Source #

Constructors

SemCxt
Fields len :: Int cxt :: Context2 Domain upperDecs :: Context UDec

Instances

Instances details

Substitute SemCxt Source #
Instance details Defined in TypeChecker Methods substitute :: Substitution -> SemCxt -> TypeCheck SemCxt Source #
Show SemCxt Source #
Instance details Defined in TCM Methods showsPrec :: Int -> SemCxt -> ShowS # show :: SemCxt -> String # showList :: [SemCxt] -> ShowS #

cxtEmpty :: SemCxt Source #

cxtPush' :: OneOrTwo Domain -> SemCxt -> SemCxt Source #

cxtPushEntry :: OneOrTwo Domain -> SemCxt -> (Int, SemCxt) Source #

cxtPush :: Domain -> SemCxt -> (Int, SemCxt) Source #

cxtPush2 :: Domain -> Domain -> SemCxt -> (Int, SemCxt) Source #

cxtPushGen :: Name -> SemCxt -> (Int, SemCxt) Source #

cxtSetType :: Int -> Domain -> SemCxt -> SemCxt Source #

lookupM :: (MonadError TraceError m, Show k, Ord k) => k -> Map k v -> m v Source #

Version of lookup that throws TraceError.

cxtLookupGen :: MonadError TraceError m => SemCxt -> Int -> m CxtEntry Source #

cxtLookupName :: MonadError TraceError m => SemCxt -> Ren -> Name -> m CxtEntry Source #

cxtApplyDec :: Dec -> SemCxt -> SemCxt Source #

class Monad m => MonadCxt (m :: Type -> Type) where Source #

Minimal complete definition

newVar, newIrr, addName, setType, setTypeOfName, genOfName, nameOfGen, lookupGen, lookupName, getContextTele, getLen, getEnv, getRen, applyDec, addRewrite, addPattern, addPatterns, addSizeRel, addBelowInfty, addBoundHyp, isBelowInfty, sizeVarBelow, getMinSize, getSizeVarsInScope, checkingCon, checkingDom, setCo, installFuns, setMeasure, activateFuns, goImpredicative, checkingMutual

Methods

newVar :: Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> m a) -> m a Source #

newWithGen :: Name -> Domain -> (Int -> Val -> m a) -> m a Source #

new2WithGen :: Name -> (Domain, Domain) -> (Int -> (Val, Val) -> m a) -> m a Source #

new :: Name -> Domain -> (Val -> m a) -> m a Source #

new2 :: Name -> (Domain, Domain) -> ((Val, Val) -> m a) -> m a Source #

new' :: Name -> Domain -> m a -> m a Source #

newIrr :: Name -> m a -> m a Source #

addName :: Name -> (Val -> m a) -> m a Source #

addKindedTypeSigs :: [Kinded (TySig TVal)] -> m a -> m a Source #

setType :: Int -> Domain -> m a -> m a Source #

setTypeOfName :: Name -> Domain -> m a -> m a Source #

genOfName :: Name -> m Int Source #

nameOfGen :: Int -> m Name Source #

uniqueName :: Name -> Int -> m Name Source #

lookupGen :: Int -> m CxtEntry Source #

lookupGenType2 :: Int -> m (TVal, TVal) Source #

lookupName :: Name -> m CxtEntry Source #

lookupName1 :: Name -> m CxtEntry1 Source #

getContextTele :: m TeleVal Source #

getLen :: m Int Source #

getEnv :: m Env Source #

getRen :: m Ren Source #

applyDec :: Dec -> m a -> m a Source #

resurrect :: m a -> m a Source #

addRewrite :: Rewrite -> [Val] -> ([Val] -> m a) -> m a Source #

addPattern :: TVal -> Pattern -> Env -> (TVal -> Val -> Env -> m a) -> m a Source #

addPatterns :: TVal -> [Pattern] -> Env -> (TVal -> [Val] -> Env -> m a) -> m a Source #

addSizeRel :: Int -> Int -> Int -> m a -> m a Source #

addBelowInfty :: Int -> m a -> m a Source #

addBoundHyp :: Bound Val -> m a -> m a Source #

isBelowInfty :: Int -> m Bool Source #

sizeVarBelow :: Int -> Int -> m (Maybe Int) Source #

getMinSize :: Int -> m (Maybe Int) Source #

getSizeVarsInScope :: m [Name] Source #

checkingCon :: Bool -> m a -> m a Source #

checkingDom :: m a -> m a Source #

setCo :: Co -> m a -> m a Source #

installFuns :: Co -> [Kinded Fun] -> m a -> m a Source #

setMeasure :: Measure Val -> m a -> m a Source #

activateFuns :: m a -> m a Source #

goImpredicative :: m a -> m a Source #

checkingMutual :: Maybe DefId -> m a -> m a Source #

Instances

Instances details

MonadCxt TypeCheck Source #

Instance details

Defined in TCM

Methods

newVar :: Name -> OneOrTwo Domain -> (Int -> OneOrTwo Val -> TypeCheck a) -> TypeCheck a Source #

newWithGen :: Name -> Domain -> (Int -> Val -> TypeCheck a) -> TypeCheck a Source #

new2WithGen :: Name -> (Domain, Domain) -> (Int -> (Val, Val) -> TypeCheck a) -> TypeCheck a Source #

new :: Name -> Domain -> (Val -> TypeCheck a) -> TypeCheck a Source #

new2 :: Name -> (Domain, Domain) -> ((Val, Val) -> TypeCheck a) -> TypeCheck a Source #

new' :: Name -> Domain -> TypeCheck a -> TypeCheck a Source #

newIrr :: Name -> TypeCheck a -> TypeCheck a Source #

addName :: Name -> (Val -> TypeCheck a) -> TypeCheck a Source #

addKindedTypeSigs :: [Kinded (TySig TVal)] -> TypeCheck a -> TypeCheck a Source #

setType :: Int -> Domain -> TypeCheck a -> TypeCheck a Source #

setTypeOfName :: Name -> Domain -> TypeCheck a -> TypeCheck a Source #

genOfName :: Name -> TypeCheck Int Source #

nameOfGen :: Int -> TypeCheck Name Source #

uniqueName :: Name -> Int -> TypeCheck Name Source #

lookupGen :: Int -> TypeCheck CxtEntry Source #

lookupGenType2 :: Int -> TypeCheck (TVal, TVal) Source #

lookupName :: Name -> TypeCheck CxtEntry Source #

lookupName1 :: Name -> TypeCheck CxtEntry1 Source #

getContextTele :: TypeCheck TeleVal Source #

getLen :: TypeCheck Int Source #

getEnv :: TypeCheck Env Source #

getRen :: TypeCheck Ren Source #

applyDec :: Dec -> TypeCheck a -> TypeCheck a Source #

resurrect :: TypeCheck a -> TypeCheck a Source #

addRewrite :: Rewrite -> [Val] -> ([Val] -> TypeCheck a) -> TypeCheck a Source #

addPattern :: TVal -> Pattern -> Env -> (TVal -> Val -> Env -> TypeCheck a) -> TypeCheck a Source #

addPatterns :: TVal -> [Pattern] -> Env -> (TVal -> [Val] -> Env -> TypeCheck a) -> TypeCheck a Source #

addSizeRel :: Int -> Int -> Int -> TypeCheck a -> TypeCheck a Source #

addBelowInfty :: Int -> TypeCheck a -> TypeCheck a Source #

addBoundHyp :: Bound Val -> TypeCheck a -> TypeCheck a Source #

isBelowInfty :: Int -> TypeCheck Bool Source #

sizeVarBelow :: Int -> Int -> TypeCheck (Maybe Int) Source #

getMinSize :: Int -> TypeCheck (Maybe Int) Source #

getSizeVarsInScope :: TypeCheck [Name] Source #

checkingCon :: Bool -> TypeCheck a -> TypeCheck a Source #

checkingDom :: TypeCheck a -> TypeCheck a Source #

setCo :: Co -> TypeCheck a -> TypeCheck a Source #

installFuns :: Co -> [Kinded Fun] -> TypeCheck a -> TypeCheck a Source #

setMeasure :: Measure Val -> TypeCheck a -> TypeCheck a Source #

activateFuns :: TypeCheck a -> TypeCheck a Source #

goImpredicative :: TypeCheck a -> TypeCheck a Source #

checkingMutual :: Maybe DefId -> TypeCheck a -> TypeCheck a Source #

dontCare :: a Source #

underAbs :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a Source #

Go into the codomain of a Pi-type or open an abstraction.

underAbs_ :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a Source #

Do not check consistency preservation of context.

noConsistencyChecking :: TypeCheck a -> TypeCheck a Source #

underAbs' :: Name -> FVal -> (Val -> Val -> TypeCheck a) -> TypeCheck a Source #

No eta, no hypotheses. First returned val is a VGen i.

addBind :: TBind -> TypeCheck a -> TypeCheck a Source #

addBinds :: Telescope -> TypeCheck a -> TypeCheck a Source #

introPatterns :: [Pattern] -> TVal -> ([(Pattern, Val)] -> TVal -> TypeCheck a) -> TypeCheck a Source #

introPatVar :: Pattern -> TypeCheck a -> TypeCheck a Source #

introPatVars :: [Pattern] -> TypeCheck a -> TypeCheck a Source #

introPatType :: (Pattern, Val) -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a Source #

introPatTypes :: [(Pattern, Val)] -> TVal -> (TVal -> TypeCheck a) -> TypeCheck a Source #

matchPatType :: (Pattern, Val) -> Domain -> TypeCheck a -> TypeCheck a Source #

type Signature = Map QName SigDef Source #

data SigDef Source #

Constructors

FunSig
Fields isCo :: Co symbTyp :: TVal (RHS) type, includs parameter tel. symbolKind :: Kind arity :: Arity clauses :: [Clause] isTypeChecked :: Bool extrTyp :: Expr Fomega type.
LetSig
Fields symbTyp :: TVal (RHS) type, includs parameter tel. symbolKind :: Kind definingVal :: Val extrTyp :: Expr Fomega type.
PatSig
Fields patVars :: [Name] definingPat :: Pattern definingVal :: Val
ConSig
Fields conPars :: ConPars Parameter patterns and no. of variable they bind. `Nothing` if old-style parameters. lhsTyp :: LHSType LHS type of constructor for pattern matching, e.g. rhs `cons : [A : Set] [i : Size] -> A -> List A i -> List A $i` lhs `cons : [A : Set] [i : Size] [j - A -> List A j -> List A i` `Name` is the name of the size parameter. recOccs :: [Bool] `True` if argument contains rec.occs.of the (co)data type? symbTyp :: TVal (RHS) type, includs parameter tel. dataName :: Name Its datatype. dataPars :: Int No. of parameters of its datatype. extrTyp :: Expr Fomega type.
DataSig
Fields numPars :: Int positivity :: [Pol] isSized :: Sized isCo :: Co symbTyp :: TVal (RHS) type, includs parameter tel. symbolKind :: Kind constructors :: [ConstructorInfo] etaExpand :: Bool isTuple :: Bool extrTyp :: Expr Fomega type.

Instances

Instances details

Show SigDef Source #
Instance details Defined in TCM Methods showsPrec :: Int -> SigDef -> ShowS # show :: SigDef -> String # showList :: [SigDef] -> ShowS #

type ConPars = Maybe ([Name], [Pattern]) Source #

Parameter patterns and no. of variables they bind.

type LHSType = Maybe (Name, TVal) Source #

LHS type plus name of size index.

isEmptyData :: QName -> TypeCheck Bool Source #

isUnitData :: QName -> TypeCheck Bool Source #

undefinedFType :: QName -> Expr Source #

symbKind :: SigDef -> Kind Source #

emptySig :: Signature Source #

data DataView Source #

Constructors

Data Name [Clos]
NoData

dataView :: TVal -> TypeCheck DataView Source #

Check if type tv is a datatype D vs.

disambigCon :: QName -> TVal -> TypeCheck QName Source #

Disambiguate possibly overloaded constructor c at given type tv.

conType :: QName -> TVal -> TypeCheck TVal Source #

conType c tv returns the type of constructor c at datatype tv with parameters instantiated.

conLType :: QName -> TVal -> TypeCheck TVal Source #

Get LHS type of constructor.

Constructors or sized data types internally have a lhs type that differs from its rhs type. E.g., rhs suc : [i : Size] -> Nat i -> Nat $i lhs suc : [i : Size] [j - Nat j -> Nat i. In the lhs type, i turns into an additional parameter.

instConType :: QName -> ConPars -> TVal -> Name -> Int -> TVal -> TypeCheck TVal Source #

Instantiate type of constructor to parameters obtained from the data type.

instConType c n symbTyp dataName tv instantiates type symbTyp of constructor c with first n arguments that dataName is applied to in tv. @instConType c n ((x1:A1..xn:An) -> B) d (d v1..vn ws) = B[vs/xs]@

instConLType :: QName -> ConPars -> TVal -> LHSType -> (Val -> Bool) -> Int -> TVal -> TypeCheck TVal Source #

Get correct lhs type for constructor pattern.

instConLType c numPars symbTyp Nothing isFlex tv behaves like instConLType c numPars symbType _ tv.

But if the data types is sized and the constructor has a lhs type, instConLType c numPars symbTyp (Just ltv) isFlex tv uses the lhs type ltv unless the variable instantiated for the size argument is flexible (because then it wants to be unified with the successor pattern of the rhs type.

instConLType' :: QName -> ConPars -> TVal -> Maybe ((Name, TVal), Val -> Bool) -> Maybe Name -> Int -> TVal -> TypeCheck TVal Source #