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

Safe HaskellNone

Agda.TypeChecking.Rules.LHS.Problem

Synopsis

Documentation

type FlexibleVars = [Nat]

data Problem' p

State of typechecking a LHS; input to split. [Ulf Norell's PhD, page. 35]

In Problem ps p delta, ps are the user patterns of supposed type delta. p is the pattern resulting from the splitting.

Instances

data ProblemRest

User patterns that could not be given a type yet.

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 problemInPat = [false] problemTel = (b : Bool) problemRest.restPats = [zero] problemRest.restType = if b then Nat else Nat -> Nat As we instantiate b to false, the restType reduces to Nat -> Nat and we can move pattern zero over to problemInPat.

Constructors

ProblemRest 

Fields

restPats :: [NamedArg Pattern]

non-empty list of user patterns which could not yet be typed

restType :: Type

type eliminated by restPats

Instances

Monoid ProblemRest

ProblemRest is a right dominant monoid. pr1 `mappend` pr2 = pr2 unless pr2 = mempty, then it is pr1. Basically, this means that the left ProblemRest is discarded, so use it wisely!

Subst ProblemRest 

data Focus

Constructors

Focus 

Fields

focusCon :: QName
 
focusConArgs :: [NamedArg Pattern]
 
focusRange :: Range
 
focusOutPat :: OneHolePatterns
 
focusHoleIx :: Int

Index of focused variable in the out patterns.

focusDatatype :: QName
 
focusParams :: [Arg Term]
 
focusIndices :: [Arg Term]
 
focusType :: Type

Type of variable we are splitting, kept for record patterns.

LitFocus Literal OneHolePatterns Int Type 

data SplitProblem

Constructors

Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)

the [Name]s give the as-bindings for the focus

type Problem = Problem' (Permutation, [Arg Pattern])

The permutation should permute allHoles of the patterns to correspond to the abstract patterns in the problem.

data AsBinding

Constructors

AsB Name Term Type 

data LHSState

State worked on during the main loop of checking a lhs.