ModuleAgda-2.7.0.1Haskell2010

Agda.TypeChecking.CompiledClause

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.

4 types
9 values

PackageAgda-2.7.0.1
Exports13
LanguageHaskell2010
LicenceMIT
SourceCompiledClause.hs

datadata WithArity c

Constructors

WithArity
- arity :: Int
- content :: c

Instances17Functor, Foldable, Traversable, Show, Generic, Semigroup, …

Functor WithArityDefined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Foldable WithArityDefined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Traversable WithArityDefined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Show c => Show (WithArity c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Generic (WithArity c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Semigroup c => Semigroup (WithArity c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
(Semigroup c, Monoid c) => Monoid (WithArity c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
NFData c => NFData (WithArity c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Pretty a => Pretty (WithArity a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
KillRange c => KillRange (WithArity c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
TermLike a => TermLike (WithArity a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
NamesIn a => NamesIn (WithArity a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Names
Abstract a => Abstract (WithArity a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
InstantiateFull t => InstantiateFull (WithArity t)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
Apply a => Apply (WithArity a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
EmbPrj a => EmbPrj (WithArity a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphan
type Rep (WithArity c) = D1 ('MetaData "WithArity" "Agda.TypeChecking.CompiledClause" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "WithArity" 'PrefixI 'True) (S1 ('MetaSel ('Just "arity") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Int) :*: S1 ('MetaSel ('Just "content") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 c)))Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause

datadata Case c

Branches in a case tree.

Constructors

Branches
- 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.

Instances18Functor, Foldable, Traversable, Show, Generic, Semigroup, …

Functor CaseDefined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Foldable CaseDefined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Traversable CaseDefined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Show c => Show (Case c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Generic (Case c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Semigroup m => Semigroup (Case m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
(Semigroup m, Monoid m) => Monoid (Case m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
NFData a => NFData (Case a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Pretty a => Pretty (Case a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Null (Case m)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
KillRange c => KillRange (Case c)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
TermLike a => TermLike (Case a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
NamesIn a => NamesIn (Case a)Defined in Agda-2.7.0.1 · Agda.Syntax.Internal.Names
Abstract a => Abstract (Case a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
InstantiateFull a => InstantiateFull (Case a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
Apply a => Apply (Case a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
EmbPrj a => EmbPrj (Case a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphan
type Rep (Case c) = D1 ('MetaData "Case" "Agda.TypeChecking.CompiledClause" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "Branches" 'PrefixI 'True) ((S1 ('MetaSel ('Just "projPatterns") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conBranches") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map QName (WithArity c))) :*: S1 ('MetaSel ('Just "etaBranch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (ConHead, WithArity c))))) :*: ((S1 ('MetaSel ('Just "litBranches") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Map Literal c)) :*: S1 ('MetaSel ('Just "catchAllBranch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe c))) :*: (S1 ('MetaSel ('Just "fallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: S1 ('MetaSel ('Just "lazyMatch") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause

datadata CompiledClauses' a

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 [Arg ArgName]
Absurd case. Add the free variables here as well so we can build correct number of lambdas for strict backends. (#4280)

Instances17Functor, Foldable, Traversable, Pretty, KillRange, NamesIn, …

Functor CompiledClauses'Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Foldable CompiledClauses'Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Traversable CompiledClauses'Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Pretty CompiledClausesDefined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
KillRange CompiledClausesDefined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
NamesIn CompiledClausesDefined in Agda-2.7.0.1 · Agda.Syntax.Internal.Names
Abstract CompiledClausesDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
DropArgs CompiledClausesDefined in Agda-2.7.0.1 · Agda.TypeChecking.DropArgs
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.
InstantiateFull CompiledClausesDefined in Agda-2.7.0.1 · Agda.TypeChecking.Reduce
Apply CompiledClausesDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
EmbPrj CompiledClausesDefined in Agda-2.7.0.1 · Agda.TypeChecking.Serialise.Instances.Internal · orphan
Show a => Show (CompiledClauses' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
Generic (CompiledClauses' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
NFData a => NFData (CompiledClauses' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
TermLike a => TermLike (CompiledClauses' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause
PrecomputeFreeVars a => PrecomputeFreeVars (CompiledClauses' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause.Compile · orphan
type Rep (CompiledClauses' a) = D1 ('MetaData "CompiledClauses'" "Agda.TypeChecking.CompiledClause" "Agda-2.7.0.1-DbbZpETDDF1KkwuzEZvfn8" 'False) (C1 ('MetaCons "Case" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Arg Int)) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Case (CompiledClauses' a)))) :+: (C1 ('MetaCons "Done" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg ArgName]) :*: S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 a)) :+: C1 ('MetaCons "Fail" 'PrefixI 'False) (S1 ('MetaSel 'Nothing 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 [Arg ArgName]))))Defined in Agda-2.7.0.1 · Agda.TypeChecking.CompiledClause

typetype CompiledClauses = CompiledClauses' Term

valuelitCase :: Literal -> c -> Case c

valueconCase :: QName -> Bool -> WithArity c -> Case c

valueetaCase :: ConHead -> WithArity c -> Case c

valueprojCase :: QName -> c -> Case c

valuecatchAll :: c -> Case c

valuecheckLazyMatch :: Case c -> Case c

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

valuehasCatchAll :: CompiledClauses -> Bool

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

valuehasProjectionPatterns :: CompiledClauses -> Bool

Check whether a case tree has any projection patterns

Pretty instances.

1 declaration

valueprettyMap_ :: (Pretty k, Pretty v) => Map k v -> [Doc]

KillRange instances.

0 declarations

TermLike instances

0 declarations