Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- type FlexibleVars = [FlexibleVar Nat]
- data FlexibleVarKind
- data FlexibleVar a = FlexibleVar {
- flexHiding :: Hiding
- flexOrigin :: Origin
- flexKind :: FlexibleVarKind
- flexPos :: Maybe Int
- flexVar :: a
- allFlexVars :: Telescope -> FlexibleVars
- data FlexChoice
- class ChooseFlex a where
- chooseFlex :: a -> a -> FlexChoice
- data ProblemEq = ProblemEq {
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type
- data Problem a = Problem {
- _problemEqs :: [ProblemEq]
- _problemRestPats :: [NamedArg Pattern]
- _problemCont :: LHSState a -> TCM a
- problemEqs :: Lens' [ProblemEq] (Problem a)
- problemRestPats :: Lens' [NamedArg Pattern] (Problem a)
- problemCont :: Lens' (LHSState a -> TCM a) (Problem a)
- problemInPats :: Problem a -> [Pattern]
- data AsBinding = AsB Name Term Type
- data DotPattern = Dot Expr Term (Dom Type)
- data AbsurdPattern = Absurd Range Type
- data LHSState a = LHSState {
- _lhsTel :: Telescope
- _lhsOutPat :: [NamedArg DeBruijnPattern]
- _lhsProblem :: Problem a
- _lhsTarget :: Arg Type
- _lhsPartialSplit :: ![Maybe Int]
- lhsTel :: Lens' Telescope (LHSState a)
- lhsOutPat :: Lens' [NamedArg DeBruijnPattern] (LHSState a)
- lhsProblem :: Lens' (Problem a) (LHSState a)
- lhsTarget :: Lens' (Arg Type) (LHSState a)
Documentation
type FlexibleVars = [FlexibleVar Nat] Source #
data FlexibleVarKind Source #
When we encounter a flexible variable in the unifier, where did it come from?
The alternatives are ordered such that we will assign the higher one first,
i.e., first we try to assign a DotFlex
, then...
RecordFlex [FlexibleVarKind] | From a record pattern ( |
ImplicitFlex | From a hidden formal argument or underscore ( |
DotFlex | From a dot pattern ( |
OtherFlex |
Instances
Eq FlexibleVarKind Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem (==) :: FlexibleVarKind -> FlexibleVarKind -> Bool # (/=) :: FlexibleVarKind -> FlexibleVarKind -> Bool # | |
Show FlexibleVarKind Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem showsPrec :: Int -> FlexibleVarKind -> ShowS # show :: FlexibleVarKind -> String # showList :: [FlexibleVarKind] -> ShowS # | |
ChooseFlex FlexibleVarKind Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem |
data FlexibleVar a Source #
Flexible variables are equipped with information where they come from, in order to make a choice which one to assign when two flexibles are unified.
FlexibleVar | |
|
Instances
allFlexVars :: Telescope -> FlexibleVars Source #
data FlexChoice Source #
Instances
Eq FlexChoice Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem (==) :: FlexChoice -> FlexChoice -> Bool # (/=) :: FlexChoice -> FlexChoice -> Bool # | |
Show FlexChoice Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem showsPrec :: Int -> FlexChoice -> ShowS # show :: FlexChoice -> String # showList :: [FlexChoice] -> ShowS # | |
Semigroup FlexChoice Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem (<>) :: FlexChoice -> FlexChoice -> FlexChoice # sconcat :: NonEmpty FlexChoice -> FlexChoice # stimes :: Integral b => b -> FlexChoice -> FlexChoice # | |
Monoid FlexChoice Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem mempty :: FlexChoice # mappend :: FlexChoice -> FlexChoice -> FlexChoice # mconcat :: [FlexChoice] -> FlexChoice # |
class ChooseFlex a where Source #
chooseFlex :: a -> a -> FlexChoice Source #
Instances
ChooseFlex Int Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: Int -> Int -> FlexChoice Source # | |
ChooseFlex Origin Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: Origin -> Origin -> FlexChoice Source # | |
ChooseFlex Hiding Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: Hiding -> Hiding -> FlexChoice Source # | |
ChooseFlex FlexibleVarKind Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem | |
ChooseFlex a => ChooseFlex [a] Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: [a] -> [a] -> FlexChoice Source # | |
ChooseFlex a => ChooseFlex (Maybe a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: Maybe a -> Maybe a -> FlexChoice Source # | |
ChooseFlex a => ChooseFlex (FlexibleVar a) Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem chooseFlex :: FlexibleVar a -> FlexibleVar a -> FlexChoice Source # |
A user pattern together with an internal term that it should be equal to after splitting is complete. Special cases: * User pattern is a variable but internal term isn't: this will be turned into an as pattern. * User pattern is a dot pattern: this pattern won't trigger any splitting but will be checked for equality after all splitting is complete and as patterns have been bound. * User pattern is an absurd pattern: emptiness of the type will be checked after splitting is complete.
ProblemEq | |
|
Instances
Eq ProblemEq Source # | |
Data ProblemEq Source # | |
Defined in Agda.Syntax.Abstract gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> ProblemEq -> c ProblemEq # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c ProblemEq # toConstr :: ProblemEq -> Constr # dataTypeOf :: ProblemEq -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c ProblemEq) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c ProblemEq) # gmapT :: (forall b. Data b => b -> b) -> ProblemEq -> ProblemEq # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> ProblemEq -> r # gmapQ :: (forall d. Data d => d -> u) -> ProblemEq -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> ProblemEq -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> ProblemEq -> m ProblemEq # | |
Show ProblemEq Source # | |
KillRange ProblemEq Source # | |
Defined in Agda.Syntax.Abstract | |
PrettyTCM ProblemEq Source # | |
Subst Term ProblemEq Source # | |
Defined in Agda.TypeChecking.Substitute applySubst :: Substitution' Term -> ProblemEq -> ProblemEq Source # |
The user patterns we still have to split on.
Problem | |
|
problemInPats :: Problem a -> [Pattern] Source #
data DotPattern Source #
Instances
PrettyTCM DotPattern Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem | |
Subst Term DotPattern Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem applySubst :: Substitution' Term -> DotPattern -> DotPattern Source # |
data AbsurdPattern Source #
Instances
PrettyTCM AbsurdPattern Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem | |
Subst Term AbsurdPattern Source # | |
Defined in Agda.TypeChecking.Rules.LHS.Problem applySubst :: Substitution' Term -> AbsurdPattern -> AbsurdPattern Source # |
State worked on during the main loop of checking a lhs. [Ulf Norell's PhD, page. 35]
LHSState | |
|