ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.Rules.LHS.ProblemRest

6 values

PackageAgda-2.7.0.1
Exports6
LanguageHaskell2010
LicenceMIT
SourceProblemRest.hs

valueuseNamesFromPattern :: [NamedArg Pattern] -> Telescope -> Telescope

Rename the variables in a telescope using the names from a given pattern.

If there are not at least as many patterns as entries as in the telescope, the names of the remaining entries in the telescope are unchanged. If there are too many patterns, there should be a type error later.

valueuseNamesFromProblemEqs

:: PureTCM m
=> [ProblemEq]
-> Telescope
-> m Telescope

valueuseOriginFrom :: (LensOrigin a, LensOrigin b) => [a] -> [b] -> [a]

valuenoProblemRest :: Problem a -> Bool

Are there any untyped user patterns left?

valueinitLHSState

:: Telescope
The initial telescope delta of parameters.
-> [ProblemEq]
The problem equations inherited from the parent clause (living in delta).
-> [NamedArg Pattern]
The user patterns.
-> Type
The type the user patterns eliminate (living in delta).
-> (LHSState a -> TCM a)
Continuation for when checking the patterns is complete.
-> TCM (LHSState a)
The initial LHS state constructed from the user patterns.

Construct an initial LHSState from user patterns. Example: @

Case : {A : Set} → Maybe A → Set → Set → Set Case nothing B C = B Case (just _) B C = C

sample : {A : Set} (m : Maybe A) → Case m Bool (Maybe A → Bool) sample (just a) (just b) = true sample (just a) nothing = false sample nothing = true The problem generated for the first clause ofsamplewith patternsjust a, just bwould be: lhsTel = [A : Set, m : Maybe A] lhsOutPat = [A, "m"] lhsProblem = Problem [A = _, "just a" = "a"] ["_", "just a"] ["just b"] [] lhsTarget = "Case m Bool (Maybe A -> Bool)" @

valueupdateProblemRest

:: (PureTCM m, MonadError TCErr m, MonadTrace m, MonadFresh NameId m)
=> LHSState a
-> m (LHSState a)

Try to move patterns from the problem rest into the problem. Possible if type of problem rest has been updated to a function type.