Agda-2.6.20240714: A dependently typed functional programming language and proof assistant
Safe HaskellNone
LanguageHaskell2010

Agda.TypeChecking.Rules.LHS.Problem

Synopsis

Documentation

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...

Constructors

RecordFlex [FlexibleVarKind]

From a record pattern (ConP). Saves the FlexibleVarKind of its subpatterns.

ImplicitFlex

From a hidden formal argument or underscore (WildP).

DotFlex

From a dot pattern (DotP).

OtherFlex

From a non-record constructor or literal (ConP or LitP).

Instances

Instances details
ChooseFlex FlexibleVarKind Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Show FlexibleVarKind Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

showsPrec :: Int -> FlexibleVarKind -> ShowS

show :: FlexibleVarKind -> String

showList :: [FlexibleVarKind] -> ShowS

Eq FlexibleVarKind Source # 
Instance details

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.

Instances

Instances details
Functor FlexibleVar Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

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

(<$) :: a -> FlexibleVar b -> FlexibleVar a #

Foldable FlexibleVar Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

fold :: Monoid m => FlexibleVar m -> m

foldMap :: Monoid m => (a -> m) -> FlexibleVar a -> m

foldMap' :: Monoid m => (a -> m) -> FlexibleVar a -> m

foldr :: (a -> b -> b) -> b -> FlexibleVar a -> b

foldr' :: (a -> b -> b) -> b -> FlexibleVar a -> b

foldl :: (b -> a -> b) -> b -> FlexibleVar a -> b

foldl' :: (b -> a -> b) -> b -> FlexibleVar a -> b

foldr1 :: (a -> a -> a) -> FlexibleVar a -> a

foldl1 :: (a -> a -> a) -> FlexibleVar a -> a

toList :: FlexibleVar a -> [a]

null :: FlexibleVar a -> Bool

length :: FlexibleVar a -> Int

elem :: Eq a => a -> FlexibleVar a -> Bool

maximum :: Ord a => FlexibleVar a -> a

minimum :: Ord a => FlexibleVar a -> a

sum :: Num a => FlexibleVar a -> a

product :: Num a => FlexibleVar a -> a

Traversable FlexibleVar Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

traverse :: Applicative f => (a -> f b) -> FlexibleVar a -> f (FlexibleVar b)

sequenceA :: Applicative f => FlexibleVar (f a) -> f (FlexibleVar a)

mapM :: Monad m => (a -> m b) -> FlexibleVar a -> m (FlexibleVar b)

sequence :: Monad m => FlexibleVar (m a) -> m (FlexibleVar a)

LensArgInfo (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensHiding (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensModality (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

LensOrigin (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

ChooseFlex a => ChooseFlex (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Show a => Show (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

showsPrec :: Int -> FlexibleVar a -> ShowS

show :: FlexibleVar a -> String

showList :: [FlexibleVar a] -> ShowS

Eq a => Eq (FlexibleVar a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

(==) :: FlexibleVar a -> FlexibleVar a -> Bool

(/=) :: FlexibleVar a -> FlexibleVar a -> Bool

data FlexChoice Source #

Instances

Instances details
Monoid FlexChoice Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Semigroup FlexChoice Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Show FlexChoice Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

showsPrec :: Int -> FlexChoice -> ShowS

show :: FlexChoice -> String

showList :: [FlexChoice] -> ShowS

Eq FlexChoice Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

(==) :: FlexChoice -> FlexChoice -> Bool

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

class ChooseFlex a where Source #

Methods

chooseFlex :: a -> a -> FlexChoice Source #

data ProblemEq 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. * User pattern is an annotated wildcard: type annotation will be checked after splitting is complete.

Instances

Instances details
KillRange ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

PrettyTCM ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Subst ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

Associated Types

type SubstArg ProblemEq 
Instance details

Defined in Agda.TypeChecking.Substitute

NFData ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

rnf :: ProblemEq -> ()

Generic ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Associated Types

type Rep ProblemEq 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)))))

Methods

from :: ProblemEq -> Rep ProblemEq x

to :: Rep ProblemEq x -> ProblemEq

Show ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

showsPrec :: Int -> ProblemEq -> ShowS

show :: ProblemEq -> String

showList :: [ProblemEq] -> ShowS

Eq ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

Methods

(==) :: ProblemEq -> ProblemEq -> Bool

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

type SubstArg ProblemEq Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

type Rep ProblemEq Source # 
Instance details

Defined in Agda.Syntax.Abstract

type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.6.20240714-inplace" 'False) (C1 ('MetaCons "ProblemEq" 'PrefixI 'True) (S1 ('MetaSel ('Just "problemInPat") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Pattern) :*: (S1 ('MetaSel ('Just "problemInst") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Term) :*: S1 ('MetaSel ('Just "problemType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Dom Type)))))

data Problem a Source #

The user patterns we still have to split on.

Constructors

Problem 

Fields

  • _problemEqs :: [ProblemEq]

    User patterns which are typed (including the ones generated from implicit arguments).

  • _problemRestPats :: [NamedArg Pattern]

    List of user patterns which could not yet be typed. Example: f : (b : Bool) -> if b then Nat else Nat -> Nat f true = zero f false zero = zero f false (suc n) = n In this sitation, for clause 2, we construct an initial problem problemEqs = [false = b] problemRestPats = [zero] As we instantiate b to false, the targetType reduces to Nat -> Nat and we can move pattern zero over to problemEqs.

  • _problemCont :: LHSState a -> TCM a

    The code that checks the RHS.

Instances

Instances details
Subst (Problem a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Associated Types

type SubstArg (Problem a) 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg (Problem a) = Term
Show (Problem a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

showsPrec :: Int -> Problem a -> ShowS

show :: Problem a -> String

showList :: [Problem a] -> ShowS

type SubstArg (Problem a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

type SubstArg (Problem a) = Term

problemEqs :: forall a f. Functor f => ([ProblemEq] -> f [ProblemEq]) -> Problem a -> f (Problem a) Source #

problemRestPats :: forall a f. Functor f => ([NamedArg Pattern] -> f [NamedArg Pattern]) -> Problem a -> f (Problem a) Source #

problemCont :: forall a f. Functor f => ((LHSState a -> TCM a) -> f (LHSState a -> TCM a)) -> Problem a -> f (Problem a) Source #

data DotPattern Source #

Constructors

Dot Expr Term (Dom Type) 

data AnnotationPattern Source #

Constructors

Ann Expr Type 

Instances

Instances details
PrettyTCM AnnotationPattern Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

data LHSState a Source #

State worked on during the main loop of checking a lhs. [Ulf Norell's PhD, page. 35]

Constructors

LHSState 

Fields

Instances

Instances details
PrettyTCM (LHSState a) Source # 
Instance details

Defined in Agda.TypeChecking.Rules.LHS.Problem

Methods

prettyTCM :: MonadPretty m => LHSState a -> m Doc Source #

lhsTel :: forall a f. Functor f => (Telescope -> f Telescope) -> LHSState a -> f (LHSState a) Source #

lhsOutPat :: forall a f. Functor f => ([NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]) -> LHSState a -> f (LHSState a) Source #

lhsProblem :: forall a f. Functor f => (Problem a -> f (Problem a)) -> LHSState a -> f (LHSState a) Source #

lhsTarget :: forall a f. Functor f => (Arg Type -> f (Arg Type)) -> LHSState a -> f (LHSState a) Source #

getLeftoverPatterns :: PureTCM m => [ProblemEq] -> m LeftoverPatterns Source #

Classify remaining patterns after splitting is complete into pattern variables, as patterns, dot patterns, and absurd patterns. Precondition: there are no more constructor patterns.

getUserVariableNames Source #

Arguments

:: Telescope

The telescope of pattern variables

-> IntMap [(Name, PatVarPosition)]

The list of user names for each pattern variable

-> ([Maybe Name], [AsBinding]) 

Build a renaming for the internal patterns using variable names from the user patterns. If there are multiple user names for the same internal variable, the unused ones are returned as as-bindings. Names that are not also module parameters are preferred over those that are.

Orphan instances

PrettyTCM ProblemEq Source # 
Instance details