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

Agda.TypeChecking.CompiledClause

Synopsis

- type :-> key value = Map key value
- data Case c = Branches {
  - conBranches :: QName :-> c
  - litBranches :: Literal :-> c
  - catchAllBranch :: Maybe c
  }
- data CompiledClauses
  - = Case Int (Case CompiledClauses)
  - | Done Int Term
  - | Fail
- compileClauses :: [Clauses] -> CompiledClauses
- 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

# 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