Agda.TypeChecking.CompiledClause

Documentation

type :-> key value = Map key value

data Case c

Constructors

Branches

Fields

conBranches :: QName :-> c

litBranches :: Literal :-> c

catchAllBranch :: Maybe c

Instances

Functor Case

Typeable1 Case

Data c => Data (Case c)

Pretty a => Show (Case a)

Monoid m => Monoid (Case m)

Pretty a => Pretty (Case a)

Abstract a => Abstract (Case a)

Apply a => Apply (Case a)

EmbPrj a => EmbPrj (Case a)

InstantiateFull a => InstantiateFull (Case a)

data CompiledClauses

Constructors

Case Int (Case CompiledClauses)

Done Int Term

Fail

Instances

Data CompiledClauses

Show CompiledClauses

Typeable CompiledClauses

Pretty CompiledClauses

Abstract CompiledClauses

Apply CompiledClauses

EmbPrj CompiledClauses

InstantiateFull CompiledClauses

compileClauses :: [Clauses] -> CompiledClauses

Note that it is the translated clauses which are compiled, not the original ones.

type Cl = ([Arg Pattern], ClauseBody)

type Cls = [Cl]

compile :: Cls -> CompiledClauses

nextSplit :: Cls -> Maybe Int

splitOn :: Int -> Cls -> Case Cls

splitC :: Int -> Cl -> Case Cl