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

Agda.TypeChecking.CompiledClause.Compile

Synopsis

# Documentation

Arguments

 :: Maybe (QName, Type) Translate record patterns and coverage check with given type? -> [Clause] -> TCM CompiledClauses

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 FieldsclPats :: [Arg Pattern] clBody :: ClauseBody

Instances

 Source # MethodsshowsPrec :: Int -> Cl -> ShowS #show :: Cl -> String #showList :: [Cl] -> ShowS # Source # Methods

type Cls = [Cl] Source #

Get the index of the next argument we need to split on. This the number of the first pattern that does a match in the first clause.

Is is not a variable pattern? And if yes, is it a record pattern?

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.

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