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

Safe Haskell | None
Language | Haskell2010

Agda.TypeChecking.CompiledClause

Contents

- Pretty instances.
- KillRange instances.
- TermLike instances

Description

Case trees.

After coverage checking, pattern matching is translated to case trees, i.e., a tree of successive case splits on one variable at a time.

Synopsis

- data WithArity c = WithArity {
  - arity :: Int
  - content :: c
  }
- data Case c = Branches {
  - projPatterns :: Bool
  - conBranches :: Map QName (WithArity c)
  - etaBranch :: Maybe (ConHead, WithArity c)
  - litBranches :: Map Literal c
  - catchAllBranch :: Maybe c
  - fallThrough :: Maybe Bool
  - lazyMatch :: Bool
  }
- data CompiledClauses' a
  - = Case (Arg Int) (Case (CompiledClauses' a))
  - | Done [Arg ArgName] a
  - | Fail
- type CompiledClauses = CompiledClauses' Term
- litCase :: Literal -> c -> Case c
- conCase :: QName -> Bool -> WithArity c -> Case c
- etaCase :: ConHead -> WithArity c -> Case c
- projCase :: QName -> c -> Case c
- catchAll :: c -> Case c
- checkLazyMatch :: Case c -> Case c
- hasCatchAll :: CompiledClauses -> Bool
- hasProjectionPatterns :: CompiledClauses -> Bool
- prettyMap :: (Pretty k, Pretty v) => Map k v -> [Doc]

# Documentation

data WithArity c Source #

Constructors

WithArity |

Fields

- arity :: Int
- content :: c

Instances

Functor WithArity Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> WithArity a -> WithArity b Source # (<$) :: a -> WithArity b -> WithArity a Source #
Foldable WithArity Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

fold :: Monoid m => WithArity m -> m Source #

foldMap :: Monoid m => (a -> m) -> WithArity a -> m Source #

foldr :: (a -> b -> b) -> b -> WithArity a -> b Source #

foldr' :: (a -> b -> b) -> b -> WithArity a -> b Source #

foldl :: (b -> a -> b) -> b -> WithArity a -> b Source #

foldl' :: (b -> a -> b) -> b -> WithArity a -> b Source #

foldr1 :: (a -> a -> a) -> WithArity a -> a Source #

foldl1 :: (a -> a -> a) -> WithArity a -> a Source #

toList :: WithArity a -> [a] Source #

null :: WithArity a -> Bool Source #

length :: WithArity a -> Int Source #

elem :: Eq a => a -> WithArity a -> Bool Source #

maximum :: Ord a => WithArity a -> a Source #

minimum :: Ord a => WithArity a -> a Source #

sum :: Num a => WithArity a -> a Source #

product :: Num a => WithArity a -> a Source #

Traversable WithArity Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverse :: Applicative f => (a -> f b) -> WithArity a -> f (WithArity b) Source # sequenceA :: Applicative f => WithArity (f a) -> f (WithArity a) Source # mapM :: Monad m => (a -> m b) -> WithArity a -> m (WithArity b) Source # sequence :: Monad m => WithArity (m a) -> m (WithArity a) Source #
Data c => Data (WithArity c) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> WithArity c -> c0 (WithArity c) Source #

gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (WithArity c) Source #

toConstr :: WithArity c -> Constr Source #

dataTypeOf :: WithArity c -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (WithArity c)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (WithArity c)) Source #

gmapT :: (forall b. Data b => b -> b) -> WithArity c -> WithArity c Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> WithArity c -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> WithArity c -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> WithArity c -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> WithArity c -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> WithArity c -> m (WithArity c) Source #

Show c => Show (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods showsPrec :: Int -> WithArity c -> ShowS Source # show :: WithArity c -> String Source # showList :: [WithArity c] -> ShowS Source #
Semigroup c => Semigroup (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods (<>) :: WithArity c -> WithArity c -> WithArity c Source # sconcat :: NonEmpty (WithArity c) -> WithArity c Source # stimes :: Integral b => b -> WithArity c -> WithArity c Source #
(Semigroup c, Monoid c) => Monoid (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods mempty :: WithArity c Source # mappend :: WithArity c -> WithArity c -> WithArity c Source # mconcat :: [WithArity c] -> WithArity c Source #
Pretty a => Pretty (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: WithArity a -> Doc Source # prettyPrec :: Int -> WithArity a -> Doc Source # prettyList :: [WithArity a] -> Doc Source #
KillRange c => KillRange (WithArity c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (WithArity c) Source #
Abstract a => Abstract (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> WithArity a -> WithArity a Source #
Apply a => Apply (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: WithArity a -> Args -> WithArity a Source # applyE :: WithArity a -> Elims -> WithArity a Source #
TermLike a => TermLike (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverseTermM :: Monad m => (Term -> m Term) -> WithArity a -> m (WithArity a) Source # foldTerm :: Monoid m => (Term -> m) -> WithArity a -> m Source #
EmbPrj a => EmbPrj (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: WithArity a -> S Int32 Source # icod_ :: WithArity a -> S Int32 Source # value :: Int32 -> R (WithArity a) Source #
NamesIn a => NamesIn (WithArity a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: WithArity a -> Set QName Source #
InstantiateFull a => InstantiateFull (WithArity a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: WithArity a -> ReduceM (WithArity a) Source #

data Case c Source #

Branches in a case tree.

Constructors

Branches |

Fields

- projPatterns :: Bool

  We are constructing a record here (copatterns). `conBranches` lists projections.

- conBranches :: Map QName (WithArity c)

  Map from constructor (or projection) names to their arity and the case subtree. (Projections have arity 0.)

- etaBranch :: Maybe (ConHead, WithArity c)

  Eta-expand with the given (eta record) constructor. If this is present, there should not be any conBranches or litBranches.

- litBranches :: Map Literal c

  Map from literal to case subtree.

- catchAllBranch :: Maybe c

  (Possibly additional) catch-all clause.

- fallThrough :: Maybe Bool

  (if True) In case of non-canonical argument use catchAllBranch.

- lazyMatch :: Bool

  Lazy pattern match. Requires single (non-copattern) branch with no lit branches and no catch-all.

Instances

Functor Case Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> Case a -> Case b Source # (<$) :: a -> Case b -> Case a Source #
Foldable Case Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

fold :: Monoid m => Case m -> m Source #

foldMap :: Monoid m => (a -> m) -> Case a -> m Source #

foldr :: (a -> b -> b) -> b -> Case a -> b Source #

foldr' :: (a -> b -> b) -> b -> Case a -> b Source #

foldl :: (b -> a -> b) -> b -> Case a -> b Source #

foldl' :: (b -> a -> b) -> b -> Case a -> b Source #

foldr1 :: (a -> a -> a) -> Case a -> a Source #

foldl1 :: (a -> a -> a) -> Case a -> a Source #

toList :: Case a -> [a] Source #

null :: Case a -> Bool Source #

length :: Case a -> Int Source #

elem :: Eq a => a -> Case a -> Bool Source #

maximum :: Ord a => Case a -> a Source #

minimum :: Ord a => Case a -> a Source #

sum :: Num a => Case a -> a Source #

product :: Num a => Case a -> a Source #

Traversable Case Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverse :: Applicative f => (a -> f b) -> Case a -> f (Case b) Source # sequenceA :: Applicative f => Case (f a) -> f (Case a) Source # mapM :: Monad m => (a -> m b) -> Case a -> m (Case b) Source # sequence :: Monad m => Case (m a) -> m (Case a) Source #
Data c => Data (Case c) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

gfoldl :: (forall d b. Data d => c0 (d -> b) -> d -> c0 b) -> (forall g. g -> c0 g) -> Case c -> c0 (Case c) Source #

gunfold :: (forall b r. Data b => c0 (b -> r) -> c0 r) -> (forall r. r -> c0 r) -> Constr -> c0 (Case c) Source #

toConstr :: Case c -> Constr Source #

dataTypeOf :: Case c -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c0 (t d)) -> Maybe (c0 (Case c)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c0 (t d e)) -> Maybe (c0 (Case c)) Source #

gmapT :: (forall b. Data b => b -> b) -> Case c -> Case c Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Case c -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Case c -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Case c -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Case c -> m (Case c) Source #

Show c => Show (Case c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods showsPrec :: Int -> Case c -> ShowS Source # show :: Case c -> String Source # showList :: [Case c] -> ShowS Source #
Semigroup m => Semigroup (Case m) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods (<>) :: Case m -> Case m -> Case m Source # sconcat :: NonEmpty (Case m) -> Case m Source # stimes :: Integral b => b -> Case m -> Case m Source #
(Semigroup m, Monoid m) => Monoid (Case m) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods mempty :: Case m Source # mappend :: Case m -> Case m -> Case m Source # mconcat :: [Case m] -> Case m Source #
Null (Case m) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods empty :: Case m Source # null :: Case m -> Bool Source #
Pretty a => Pretty (Case a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: Case a -> Doc Source # prettyPrec :: Int -> Case a -> Doc Source # prettyList :: [Case a] -> Doc Source #
KillRange c => KillRange (Case c) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT (Case c) Source #
Abstract a => Abstract (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> Case a -> Case a Source #
Apply a => Apply (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: Case a -> Args -> Case a Source # applyE :: Case a -> Elims -> Case a Source #
TermLike a => TermLike (Case a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverseTermM :: Monad m => (Term -> m Term) -> Case a -> m (Case a) Source # foldTerm :: Monoid m => (Term -> m) -> Case a -> m Source #
EmbPrj a => EmbPrj (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: Case a -> S Int32 Source # icod_ :: Case a -> S Int32 Source # value :: Int32 -> R (Case a) Source #
NamesIn a => NamesIn (Case a) Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: Case a -> Set QName Source #
InstantiateFull a => InstantiateFull (Case a) Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: Case a -> ReduceM (Case a) Source #

data CompiledClauses' a Source #

Case tree with bodies.

Constructors

Case (Arg Int) (Case (CompiledClauses' a)) | `Case n bs` stands for a match on the `n`-th argument (counting from zero) with `bs` as the case branches. If the `n`-th argument is a projection, we have only `conBranches` with arity 0.
Done [Arg ArgName] a | `Done xs b` stands for the body `b` where the `xs` contains hiding and name suggestions for the free variables. This is needed to build lambdas on the right hand side for partial applications which can still reduce.
Fail | Absurd case.

Instances

Functor CompiledClauses' Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods fmap :: (a -> b) -> CompiledClauses' a -> CompiledClauses' b Source # (<$) :: a -> CompiledClauses' b -> CompiledClauses' a Source #
Foldable CompiledClauses' Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

fold :: Monoid m => CompiledClauses' m -> m Source #

foldMap :: Monoid m => (a -> m) -> CompiledClauses' a -> m Source #

foldr :: (a -> b -> b) -> b -> CompiledClauses' a -> b Source #

foldr' :: (a -> b -> b) -> b -> CompiledClauses' a -> b Source #

foldl :: (b -> a -> b) -> b -> CompiledClauses' a -> b Source #

foldl' :: (b -> a -> b) -> b -> CompiledClauses' a -> b Source #

foldr1 :: (a -> a -> a) -> CompiledClauses' a -> a Source #

foldl1 :: (a -> a -> a) -> CompiledClauses' a -> a Source #

toList :: CompiledClauses' a -> [a] Source #

null :: CompiledClauses' a -> Bool Source #

length :: CompiledClauses' a -> Int Source #

elem :: Eq a => a -> CompiledClauses' a -> Bool Source #

maximum :: Ord a => CompiledClauses' a -> a Source #

minimum :: Ord a => CompiledClauses' a -> a Source #

sum :: Num a => CompiledClauses' a -> a Source #

product :: Num a => CompiledClauses' a -> a Source #

Traversable CompiledClauses' Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

traverse :: Applicative f => (a -> f b) -> CompiledClauses' a -> f (CompiledClauses' b) Source #

sequenceA :: Applicative f => CompiledClauses' (f a) -> f (CompiledClauses' a) Source #

mapM :: Monad m => (a -> m b) -> CompiledClauses' a -> m (CompiledClauses' b) Source #

sequence :: Monad m => CompiledClauses' (m a) -> m (CompiledClauses' a) Source #

Pretty CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods pretty :: CompiledClauses -> Doc Source # prettyPrec :: Int -> CompiledClauses -> Doc Source # prettyList :: [CompiledClauses] -> Doc Source #
KillRange CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods killRange :: KillRangeT CompiledClauses Source #
Abstract CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods abstract :: Telescope -> CompiledClauses -> CompiledClauses Source #
Apply CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods apply :: CompiledClauses -> Args -> CompiledClauses Source # applyE :: CompiledClauses -> Elims -> CompiledClauses Source #
EmbPrj CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Serialise.Instances.Internal Methods icode :: CompiledClauses -> S Int32 Source # icod_ :: CompiledClauses -> S Int32 Source # value :: Int32 -> R CompiledClauses Source #
NamesIn CompiledClauses Source # |
Instance details Defined in Agda.Syntax.Internal.Names Methods namesIn :: CompiledClauses -> Set QName Source #
DropArgs CompiledClauses Source # | To drop the first `n` arguments in a compiled clause, we reduce the split argument indices by `n` and drop `n` arguments from the bodies. NOTE: this only works for non-recursive functions, we are not dropping arguments to recursive calls in bodies.
Instance details Defined in Agda.TypeChecking.DropArgs Methods dropArgs :: Int -> CompiledClauses -> CompiledClauses Source #
InstantiateFull CompiledClauses Source # |
Instance details Defined in Agda.TypeChecking.Reduce Methods instantiateFull' :: CompiledClauses -> ReduceM CompiledClauses Source #
Data a => Data (CompiledClauses' a) Source # |

Instance details

Defined in Agda.TypeChecking.CompiledClause

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> CompiledClauses' a -> c (CompiledClauses' a) Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c (CompiledClauses' a) Source #

toConstr :: CompiledClauses' a -> Constr Source #

dataTypeOf :: CompiledClauses' a -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c (CompiledClauses' a)) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (CompiledClauses' a)) Source #

gmapT :: (forall b. Data b => b -> b) -> CompiledClauses' a -> CompiledClauses' a Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r Source #

gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> CompiledClauses' a -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> CompiledClauses' a -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> CompiledClauses' a -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> CompiledClauses' a -> m (CompiledClauses' a) Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> CompiledClauses' a -> m (CompiledClauses' a) Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> CompiledClauses' a -> m (CompiledClauses' a) Source #

Show a => Show (CompiledClauses' a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods showsPrec :: Int -> CompiledClauses' a -> ShowS Source # show :: CompiledClauses' a -> String Source # showList :: [CompiledClauses' a] -> ShowS Source #
PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause.Compile Methods precomputeFreeVars :: CompiledClauses' a -> FV (CompiledClauses' a) Source #
TermLike a => TermLike (CompiledClauses' a) Source # |
Instance details Defined in Agda.TypeChecking.CompiledClause Methods traverseTermM :: Monad m => (Term -> m Term) -> CompiledClauses' a -> m (CompiledClauses' a) Source # foldTerm :: Monoid m => (Term -> m) -> CompiledClauses' a -> m Source #

type CompiledClauses = CompiledClauses' Term Source #

litCase :: Literal -> c -> Case c Source #

conCase :: QName -> Bool -> WithArity c -> Case c Source #

etaCase :: ConHead -> WithArity c -> Case c Source #

projCase :: QName -> c -> Case c Source #

catchAll :: c -> Case c Source #

checkLazyMatch :: Case c -> Case c Source #

Check that the requirements on lazy matching (single inductive case) are met, and set lazy to False otherwise.

hasCatchAll :: CompiledClauses -> Bool Source #

Check whether a case tree has a catch-all clause.

hasProjectionPatterns :: CompiledClauses -> Bool Source #

Check whether a case tree has any projection patterns

# Pretty instances.

prettyMap :: (Pretty k, Pretty v) => Map k v -> [Doc] Source #

# KillRange instances.

# TermLike instances