Agda-2.8.0: A dependently typed functional programming language and proof assistant

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.Conversion.Pure

Synopsis

- data FreshThings = FreshThings {
  - freshInt :: Int
  - freshProblemId :: ProblemId
  - freshNameId :: NameId
  }
- newtype PureConversionT (m :: Type -> Type) a = PureConversionT {
  - unPureConversionT :: ExceptT TCErr (StateT FreshThings m) a
  }
- pureEqualTerm :: (PureTCM m, MonadBlock m) => Type -> Term -> Term -> m Bool
- pureEqualTermB :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool)
- pureEqualType :: (PureTCM m, MonadBlock m) => Type -> Type -> m Bool
- pureEqualTypeB :: PureTCM m => Type -> Type -> m (Either Blocker Bool)
- pureCompareAs :: (PureTCM m, MonadBlock m) => Comparison -> CompareAs -> Term -> Term -> m Bool
- runPureConversion :: (MonadBlock m, PureTCM m) => PureConversionT m a -> m (Maybe a)
- runPureConversionB :: PureTCM m => PureConversionT m a -> m (Either Blocker (Maybe a))

# Documentation

data FreshThings Source #

Constructors

FreshThings |

Fields

- freshInt :: Int
- freshProblemId :: ProblemId
- freshNameId :: NameId

#### Instances

Instances details

Monad m => MonadState FreshThings (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods get :: PureConversionT m FreshThings Source # put :: FreshThings -> PureConversionT m () Source # state :: (FreshThings -> (a, FreshThings)) -> PureConversionT m a Source #

newtype PureConversionT (m :: Type -> Type) a Source #

Constructors

PureConversionT |

Fields

- unPureConversionT :: ExceptT TCErr (StateT FreshThings m) a

#### Instances

Instances details

MonadTrans PureConversionT Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods lift :: Monad m => m a -> PureConversionT m a Source #
Monad m => MonadFresh NameId (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m NameId Source #
Monad m => MonadFresh ProblemId (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m ProblemId Source #
Monad m => MonadFresh Int (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fresh :: PureConversionT m Int Source #
Monad m => MonadError TCErr (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods throwError :: TCErr -> PureConversionT m a Source # catchError :: PureConversionT m a -> (TCErr -> PureConversionT m a) -> PureConversionT m a Source #
Monad m => MonadState FreshThings (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods get :: PureConversionT m FreshThings Source # put :: FreshThings -> PureConversionT m () Source # state :: (FreshThings -> (a, FreshThings)) -> PureConversionT m a Source #
HasOptions m => HasOptions (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods pragmaOptions :: PureConversionT m PragmaOptions Source # commandLineOptions :: PureConversionT m CommandLineOptions Source #
Monad m => MonadBlock (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods patternViolation :: Blocker -> PureConversionT m a Source # catchPatternErr :: (Blocker -> PureConversionT m a) -> PureConversionT m a -> PureConversionT m a Source #
MonadReduce m => MonadReduce (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods liftReduce :: ReduceM a -> PureConversionT m a Source #
ReadTCState m => MonadStConcreteNames (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods runStConcreteNames :: StateT ConcreteNames (PureConversionT m) a -> PureConversionT m a Source # useConcreteNames :: PureConversionT m ConcreteNames Source # modifyConcreteNames :: (ConcreteNames -> ConcreteNames) -> PureConversionT m () Source #
MonadTCEnv m => MonadTCEnv (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods askTC :: PureConversionT m TCEnv Source # localTC :: (TCEnv -> TCEnv) -> PureConversionT m a -> PureConversionT m a Source #
ReadTCState m => ReadTCState (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods getTCState :: PureConversionT m TCState Source # locallyTCState :: Lens' TCState a -> (a -> a) -> PureConversionT m b -> PureConversionT m b Source # withTCState :: (TCState -> TCState) -> PureConversionT m a -> PureConversionT m a Source #
HasBuiltins m => HasBuiltins (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods getBuiltinThing :: SomeBuiltin -> PureConversionT m (Maybe (Builtin PrimFun)) Source #
PureTCM m => MonadConstraint (PureConversionT m) Source # |

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addConstraint :: Blocker -> Constraint -> PureConversionT m () Source #

addAwakeConstraint :: Blocker -> Constraint -> PureConversionT m () Source #

solveConstraint :: Constraint -> PureConversionT m () Source #

solveSomeAwakeConstraints :: (ProblemConstraint -> Bool) -> Bool -> PureConversionT m () Source #

wakeConstraints :: (ProblemConstraint -> WakeUp) -> PureConversionT m () Source #

stealConstraints :: ProblemId -> PureConversionT m () Source #

modifyAwakeConstraints :: (Constraints -> Constraints) -> PureConversionT m () Source #

modifySleepingConstraints :: (Constraints -> Constraints) -> PureConversionT m () Source #

MonadAddContext m => MonadAddContext (PureConversionT m) Source # |

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

addCtx :: Name -> Dom Type -> PureConversionT m a -> PureConversionT m a Source #

addLetBinding' :: Origin -> Name -> Term -> Dom Type -> PureConversionT m a -> PureConversionT m a Source #

updateContext :: Substitution -> (Context -> Context) -> PureConversionT m a -> PureConversionT m a Source #

withFreshName :: Range -> ArgName -> (Name -> PureConversionT m a) -> PureConversionT m a Source #

MonadDebug m => MonadDebug (PureConversionT m) Source # |

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

formatDebugMessage :: VerboseKey -> VerboseLevel -> TCM Doc -> PureConversionT m String Source #

traceDebugMessage :: VerboseKey -> VerboseLevel -> String -> PureConversionT m a -> PureConversionT m a Source #

verboseBracket :: VerboseKey -> VerboseLevel -> String -> PureConversionT m a -> PureConversionT m a Source #

getVerbosity :: PureConversionT m Verbosity Source #

getProfileOptions :: PureConversionT m ProfileOptions Source #

isDebugPrinting :: PureConversionT m Bool Source #

nowDebugPrinting :: PureConversionT m a -> PureConversionT m a Source #

PureTCM m => MonadInteractionPoints (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods freshInteractionId :: PureConversionT m InteractionId Source # modifyInteractionPoints :: (InteractionPoints -> InteractionPoints) -> PureConversionT m () Source #
PureTCM m => MonadMetaSolver (PureConversionT m) Source # |

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

newMeta' :: MetaInstantiation -> Frozen -> MetaInfo -> MetaPriority -> Permutation -> Judgement a -> PureConversionT m MetaId Source #

assignV :: CompareDirection -> MetaId -> Args -> Term -> CompareAs -> PureConversionT m () Source #

assignTerm' :: MetaId -> [Arg ArgName] -> Term -> PureConversionT m () Source #

etaExpandMeta :: [MetaClass] -> MetaId -> PureConversionT m () Source #

updateMetaVar :: MetaId -> (MetaVariable -> MetaVariable) -> PureConversionT m () Source #

speculateMetas :: PureConversionT m () -> PureConversionT m KeepMetas -> PureConversionT m () Source #

(HasBuiltins m, HasConstInfo m, MonadAddContext m, MonadReduce m) => PureTCM (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure
HasConstInfo m => HasConstInfo (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods getConstInfo :: QName -> PureConversionT m Definition Source # getConstInfo' :: QName -> PureConversionT m (Either SigError Definition) Source # getRewriteRulesFor :: QName -> PureConversionT m RewriteRules Source #
ReadTCState m => MonadStatistics (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods modifyCounter :: String -> (Integer -> Integer) -> PureConversionT m () Source #
PureTCM m => MonadWarning (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods addWarning :: Bool -> TCWarning -> PureConversionT m () Source #
Monad m => Applicative (PureConversionT m) Source # |

Instance details

Defined in Agda.TypeChecking.Conversion.Pure

Methods

pure :: a -> PureConversionT m a Source #

(<*>) :: PureConversionT m (a -> b) -> PureConversionT m a -> PureConversionT m b Source #

liftA2 :: (a -> b -> c) -> PureConversionT m a -> PureConversionT m b -> PureConversionT m c Source #

(*>) :: PureConversionT m a -> PureConversionT m b -> PureConversionT m b Source #

(<*) :: PureConversionT m a -> PureConversionT m b -> PureConversionT m a Source #

Functor m => Functor (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fmap :: (a -> b) -> PureConversionT m a -> PureConversionT m b Source # (<$) :: a -> PureConversionT m b -> PureConversionT m a Source #
Monad m => Monad (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods (>>=) :: PureConversionT m a -> (a -> PureConversionT m b) -> PureConversionT m b Source # (>>) :: PureConversionT m a -> PureConversionT m b -> PureConversionT m b Source # return :: a -> PureConversionT m a Source #
MonadFail m => MonadFail (PureConversionT m) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fail :: String -> PureConversionT m a Source #
Monad m => Null (PureConversionT m Doc) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods empty :: PureConversionT m Doc Source # null :: PureConversionT m Doc -> Bool Source #
(Monad m, Semigroup a) => Semigroup (PureConversionT m a) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods (<>) :: PureConversionT m a -> PureConversionT m a -> PureConversionT m a Source # sconcat :: NonEmpty (PureConversionT m a) -> PureConversionT m a Source # stimes :: Integral b => b -> PureConversionT m a -> PureConversionT m a Source #
(IsString a, Monad m) => IsString (PureConversionT m a) Source # |
Instance details Defined in Agda.TypeChecking.Conversion.Pure Methods fromString :: String -> PureConversionT m a Source #

pureEqualTerm :: (PureTCM m, MonadBlock m) => Type -> Term -> Term -> m Bool Source #

pureEqualTermB :: PureTCM m => Type -> Term -> Term -> m (Either Blocker Bool) Source #

Return the blocker instead of throwing a `patternViolation`.

pureEqualType :: (PureTCM m, MonadBlock m) => Type -> Type -> m Bool Source #

pureEqualTypeB :: PureTCM m => Type -> Type -> m (Either Blocker Bool) Source #

Return the blocker instead of throwing a `patternViolation`.

pureCompareAs :: (PureTCM m, MonadBlock m) => Comparison -> CompareAs -> Term -> Term -> m Bool Source #

runPureConversion :: (MonadBlock m, PureTCM m) => PureConversionT m a -> m (Maybe a) Source #

runPureConversionB :: PureTCM m => PureConversionT m a -> m (Either Blocker (Maybe a)) Source #