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

Safe Haskell | None

Agda.TypeChecking.Rules.LHS.Problem

Synopsis

- type Substitution = [Maybe Term]
- type FlexibleVars = [Nat]
- data Problem' p = Problem {
  - problemInPat :: [NamedArg Pattern]
  - problemOutPat :: p
  - problemTel :: Telescope
  - problemRest :: ProblemRest
  }
- data ProblemRest = ProblemRest {
  - restPats :: [NamedArg Pattern]
  - restType :: Type
  }
- data Focus
  - = Focus {
    - focusCon :: QName
    - focusConArgs :: [NamedArg Pattern]
    - focusRange :: Range
    - focusOutPat :: OneHolePatterns
    - focusHoleIx :: Int
    - focusDatatype :: QName
    - focusParams :: [Arg Term]
    - focusIndices :: [Arg Term]
    - focusType :: Type
    }
  - | LitFocus Literal OneHolePatterns Int Type
- data SplitProblem = Split ProblemPart [Name] (Arg Focus) (Abs ProblemPart)
- data SplitError
  - = NothingToSplit
  - | SplitPanic String
- type Problem = Problem' (Permutation, [Arg Pattern])
- type ProblemPart = Problem' ()
- data DotPatternInst = DPI Expr Term (Dom Type)
- data AsBinding = AsB Name Term Type
- data LHSState = LHSState {
  - lhsProblem :: Problem
  - lhsSubst :: Substitution
  - lhsDPI :: [DotPatternInst]
  - lhsAsB :: [AsBinding]
  }

# Documentation

type Substitution = [Maybe Term]

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.

Constructors

Problem |

Fields

problemInPat :: [NamedArg Pattern]
problemOutPat :: p
problemTel :: Telescope
problemRest :: ProblemRest

Instances

Monoid p => Monoid (Problem' p) |
Subst (Problem' p) |

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

data SplitError

Constructors

NothingToSplit |
SplitPanic String |

Instances

Error SplitError |

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

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

type ProblemPart = Problem' ()

data DotPatternInst

Constructors

DPI Expr Term (Dom Type) |

Instances

Subst DotPatternInst |
PrettyTCM DotPatternInst |

data AsBinding

Constructors

AsB Name Term Type |

Instances

Subst AsBinding |
PrettyTCM AsBinding |

data LHSState

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

Constructors

LHSState |

Fields

lhsProblem :: Problem
lhsSubst :: Substitution
lhsDPI :: [DotPatternInst]
lhsAsB :: [AsBinding]