Agda.TypeChecking.CompiledClause.Compile

Documentation

data RunRecordPatternTranslation

Constructors

RunRecordPatternTranslation

DontRunRecordPatternTranslation

Instances

Eq RunRecordPatternTranslation

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

(==) :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool

(/=) :: RunRecordPatternTranslation -> RunRecordPatternTranslation -> Bool

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

compileClauses

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

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

Pretty Cl

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

pretty :: Cl -> Doc

prettyPrec :: Int -> Cl -> Doc

prettyList :: [Cl] -> Doc

Show Cl

Defined in Agda.TypeChecking.CompiledClause.Compile

Methods

showsPrec :: Int -> Cl -> ShowS

show :: Cl -> String

showList :: [Cl] -> ShowS

type Cls = [Cl]

unBruijn :: Clause -> Cl

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

compileWithSplitTree :: SplitTree -> Cls -> CompiledClauses

compile :: Cls -> CompiledClauses

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

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

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

isVar :: Pattern' a -> Bool

Is this a variable pattern?

Maintain invariant: isVar = isNothing . properSplit!

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

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

splitC :: Int -> Cl -> Case Cl

expandCatchAlls :: Bool -> Int -> Cls -> Cls

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

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

Orphan instances

PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a)

Methods

precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a)