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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.CompiledClause.Compile

Contents

- Orphan instances

Synopsis

- data RunRecordPatternTranslation
  - = RunRecordPatternTranslation
  - | DontRunRecordPatternTranslation
- compileClauses' :: QName -> RunRecordPatternTranslation -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses
- compileClauses :: Maybe (QName, Type) -> [Clause] -> TCM (Maybe SplitTree, Bool, CompiledClauses)
- data Cl = Cl {
  - clPats :: [Arg Pattern]
  - clBody :: Maybe Term
  }
- type Cls = [Cl]
- unBruijn :: Clause -> Cl
- compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses
- compile :: Cls -> CompiledClauses
- nextSplit :: Cls -> Maybe (Bool, Arg Int)
- properSplit :: Pattern' a -> Maybe Bool
- isVar :: Pattern' a -> Bool
- splitOn :: Bool -> Int -> Cls -> Case Cls
- splitC :: Int -> Cl -> Case Cl
- expandCatchalls :: Bool -> Int -> Cls -> Cls
- ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl
- substBody :: Subst a => Int -> Int -> SubstArg a -> a -> a

# Documentation

data RunRecordPatternTranslation Source #

Constructors

RunRecordPatternTranslation |
DontRunRecordPatternTranslation |

#### Instances

Instances details

Eq RunRecordPatternTranslation Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause.Compile Methods (==) :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool Source # (/=) :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool Source #

compileClauses' :: QName -> RunRecordPatternTranslation -> [Clause] -> Maybe SplitTree -> TCM CompiledClauses Source #

compileClauses Source #

Arguments

:: Maybe (QName, Type) | Translate record patterns and coverage check with given type?
-> [Clause] |
-> TCM (Maybe SplitTree, Bool, CompiledClauses) | The `Bool` indicates whether we turned a record expression into a copattern match.

Process function clauses into case tree. This involves: 1. Coverage checking, generating a split tree. 2. Translation of lhs record patterns into rhs uses of projection. Update the split tree. 3. Generating a case tree from the split tree. Phases 1. and 2. are skipped if `Nothing`.

data Cl Source #

Stripped-down version of `Clause` used in clause compiler.

Constructors

Cl |

Fields

- clPats :: [Arg Pattern]

  Pattern variables are considered in left-to-right order.

- clBody :: Maybe Term

#### Instances

Instances details

Pretty Cl Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause.Compile Methods pretty :: Cl -> Doc Source # prettyPrec :: Int -> Cl -> Doc Source # prettyList :: [Cl] -> Doc Source #
Show Cl Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause.Compile Methods showsPrec :: Int -> Cl -> ShowS Source # show :: Cl -> String Source # showList :: [Cl] -> ShowS Source #

type Cls = [Cl] Source #

unBruijn :: Clause -> Cl Source #

Strip down a clause. Don't forget to apply the substitution to the dot patterns!

compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses Source #

compile :: Cls -> CompiledClauses Source #

nextSplit :: Cls -> Maybe (Bool, Arg Int) Source #

Get the index of the next argument we need to split on. This the number of the first pattern that does a (non-lazy) match in the first clause. Or the first lazy match where all clauses agree on the constructor, if there are no non-lazy matches.

properSplit :: Pattern' a -> Maybe Bool Source #

Is is not a variable pattern? And if yes, is it a record pattern and/or a fallThrough one?

isVar :: Pattern' a -> Bool Source #

Is this a variable pattern?

Maintain invariant: `isVar = isNothing . properSplit`!

splitOn :: Bool -> Int -> Cls -> Case Cls Source #

`splitOn single n cs` will force expansion of catch-alls if `single`.

splitC :: Int -> Cl -> Case Cl Source #

expandCatchalls :: Bool -> Int -> Cls -> Cls Source #

Expand catch-alls that appear before actual matches.

Example:

       true  y
       x     false
       false y

will expand the catch-all `x` to `false`.

Catch-alls need also to be expanded if they come before/after a record pattern, otherwise we get into trouble when we want to eliminate splits on records later.

Another example (see Issue 1650): `f (x, (y, z)) true = a f _ false = b` Split tree: `0 (first argument of f) - 1 (second component of the pair) - 3 (last argument of f) -- true -> a - false -> b` We would like to get the following case tree: `case 0 of _,_ -> case 1 of _,_ -> case 3 of true -> a; false -> b _ -> case 3 of true -> a; false -> b _ -> case 3 of true -> a; false -> b`

Example from issue #2168: `f x false = a f false = _ -> b f x true = c` case tree: `f x y = case y of true -> case x of true -> c false -> b false -> a`

Example from issue #3628: `f i j k (i = i0)(k = i1) = base f i j k (j = i1) = base` case tree: `f i j k o = case i of i0 -> case k of i1 -> base _ -> case j of i1 -> base _ -> case j of i1 -> base`

ensureNPatterns :: Int -> [ArgInfo] -> Cl -> Cl Source #

Make sure (by eta-expansion) that clause has arity at least `n` where `n` is also the length of the provided list.

substBody :: Subst a => Int -> Int -> SubstArg a -> a -> a Source #

# Orphan instances

PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) Source # |
Instance details Methods precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a) Source #