ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Rules.LHS.Problem

12 types
1 class
11 values

PackageAgda-2.7.0.1
Exports24
LanguageHaskell2010
LicenceMIT
SourceProblem.hs

typetype FlexibleVars = [FlexibleVar Nat]

datadata FlexibleVarKind

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

Instances3Eq, Show, ChooseFlex

Eq FlexibleVarKindDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Show FlexibleVarKindDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex FlexibleVarKindDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

datadata FlexibleVar a

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.

Constructors

FlexibleVar
- flexArgInfo :: ArgInfo
- flexForced :: IsForced
- flexKind :: FlexibleVarKind
- flexPos :: Maybe Int
- flexVar :: a

Instances10Functor, Foldable, Traversable, Eq, Show, LensHiding, …

Functor FlexibleVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Foldable FlexibleVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Traversable FlexibleVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Eq a => Eq (FlexibleVar a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Show a => Show (FlexibleVar a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
LensHiding (FlexibleVar a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
LensArgInfo (FlexibleVar a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
LensModality (FlexibleVar a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
LensOrigin (FlexibleVar a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex a => ChooseFlex (FlexibleVar a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

valueallFlexVars :: [IsForced] -> Telescope -> FlexibleVars

datadata FlexChoice

ChooseLeft ChooseRight ChooseEither ExpandBoth

Instances4Eq, Show, Semigroup, Monoid

Eq FlexChoiceDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Show FlexChoiceDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Semigroup FlexChoiceDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Monoid FlexChoiceDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

classclass ChooseFlex a where

Methods

chooseFlex :: a -> a -> FlexChoice

Instances9ChooseFlex, …

ChooseFlex ArgInfoDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex HidingDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex OriginDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex IsForcedDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex FlexibleVarKindDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex IntDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex a => ChooseFlex (FlexibleVar a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex a => ChooseFlex (Maybe a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
ChooseFlex a => ChooseFlex [a]Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

datadata ProblemEq

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.

Constructors

ProblemEq
- problemInPat :: Pattern
- problemInst :: Term
- problemType :: Dom Type

Instances11Eq, Show, Generic, NFData, Subst, PrettyTCM, …

Eq ProblemEqDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
Show ProblemEqDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
Generic ProblemEqDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
NFData ProblemEqDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
Subst ProblemEqDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
PrettyTCM ProblemEqDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem · orphan
Hilite ProblemEqDefined in Agda-2.7.0.1 · Agda.Interaction.Highlighting.FromAbstract
KillRange ProblemEqDefined in Agda-2.7.0.1 · Agda.Syntax.Abstract
BlankVars ProblemEqDefined in Agda-2.7.0.1 · Agda.Syntax.Translation.InternalToAbstract
type Rep ProblemEq = D1 ('MetaData "ProblemEq" "Agda.Syntax.Abstract" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" '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)))))Defined in Agda-2.7.0.1 · Agda.Syntax.Abstract
type SubstArg ProblemEq = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan

datadata Problem a

The user patterns we still have to split on.

Constructors

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

Instances3Show, Subst, SubstArg

Show (Problem a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Subst (Problem a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
type SubstArg (Problem a) = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

valueproblemEqs

:: Functor f
=> [ProblemEq] -> f [ProblemEq]
-> Problem a
-> f (Problem a)

valueproblemRestPats

:: Functor f
=> [NamedArg Pattern] -> f [NamedArg Pattern]
-> Problem a
-> f (Problem a)

valueproblemCont

:: Functor f
=> (LHSState a -> TCM a) -> f (LHSState a -> TCM a)
-> Problem a
-> f (Problem a)

valueproblemInPats :: Problem a -> [Pattern]

datadata AsBinding

Constructors

AsB Name Term Type Modality

Instances5Pretty, Subst, PrettyTCM, InstantiateFull, SubstArg

Pretty AsBindingDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Subst AsBindingDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM AsBindingDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
InstantiateFull AsBindingDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
type SubstArg AsBinding = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

datadata DotPattern

Constructors

Dot Expr Term (Dom Type)

Instances3Subst, PrettyTCM, SubstArg

Subst DotPatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM DotPatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
type SubstArg DotPattern = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

datadata AbsurdPattern

Constructors

Absurd Range Type

Instances3Subst, PrettyTCM, SubstArg

Subst AbsurdPatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM AbsurdPatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
type SubstArg AbsurdPattern = TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

datadata AnnotationPattern

Constructors

Ann Expr Type

Instances1PrettyTCM

PrettyTCM AnnotationPatternDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

datadata LHSState a

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

Constructors

LHSState
- _lhsTel :: Telescope
  The types of the pattern variables.
- _lhsOutPat :: [NamedArg DeBruijnPattern]
  Patterns after splitting. The de Bruijn indices refer to positions in the list of abstract syntax patterns in the problem, counted from the back (right-to-left).
- _lhsProblem :: Problem a
  User patterns of supposed type delta.
- _lhsTarget :: Arg Type
  Type eliminated by problemRestPats in the problem. Can be Irrelevant to indicate that we came by an irrelevant projection and, hence, the rhs must be type-checked in irrelevant mode.
- _lhsPartialSplit :: ![Maybe Int]
  have we splitted with a PartialFocus?
- _lhsIndexedSplit :: !Bool
  Have we split on any indexed inductive types?

Instances1PrettyTCM

PrettyTCM (LHSState a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

valuelhsTel

:: Functor f
=> Telescope -> f Telescope
-> LHSState a
-> f (LHSState a)

valuelhsOutPat

:: Functor f
=> [NamedArg DeBruijnPattern] -> f [NamedArg DeBruijnPattern]
-> LHSState a
-> f (LHSState a)

valuelhsProblem

:: Functor f
=> Problem a -> f (Problem a)
-> LHSState a
-> f (LHSState a)

valuelhsTarget

:: Functor f
=> Arg Type -> f (Arg Type)
-> LHSState a
-> f (LHSState a)

datadata LeftoverPatterns

Constructors

LeftoverPatterns
- patternVariables :: IntMap [(Name, PatVarPosition)]
- asPatterns :: [AsBinding]
- dotPatterns :: [DotPattern]
- absurdPatterns :: [AbsurdPattern]
- typeAnnotations :: [AnnotationPattern]
- otherPatterns :: [Pattern]

Instances4Semigroup, Monoid, PrettyTCM, Null

Semigroup LeftoverPatternsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Monoid LeftoverPatternsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
PrettyTCM LeftoverPatternsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem
Null LeftoverPatternsDefined in Agda-2.7.0.1 · Agda.TypeChecking.Rules.LHS.Problem

valuegetLeftoverPatterns :: PureTCM m => [ProblemEq] -> m LeftoverPatterns

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

valuegetUserVariableNames

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

1 instance

PrettyTCM ProblemEq