PatOSystem	Pattern inserted by the system
PatOSplit	Pattern generated by case split
PatOSplitArg ArgName	Argument to pattern generated by case split
PatOVar Name	User wrote a variable pattern
PatODot	User wrote a dot pattern
PatOWild	User wrote a wildcard pattern
PatOCon	User wrote a constructor pattern
PatORec	User wrote a record pattern
PatOLit	User wrote a literal pattern
PatOAbsurd	User wrote an absurd pattern

Instances

Instances details

KillRange PatOrigin Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

killRange :: KillRangeT PatOrigin Source #

EmbPrj PatOrigin Source #

Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: PatOrigin -> S Word32 Source #

icod_ :: PatOrigin -> S Word32 Source #

value :: Word32 -> R PatOrigin Source #

NFData PatOrigin Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

rnf :: PatOrigin -> () #

Generic PatOrigin Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type Rep PatOrigin

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

from :: PatOrigin -> Rep PatOrigin x #

to :: Rep PatOrigin x -> PatOrigin #

Show PatOrigin Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

showsPrec :: Int -> PatOrigin -> ShowS #

show :: PatOrigin -> String #

showList :: [PatOrigin] -> ShowS #

Eq PatOrigin Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

(==) :: PatOrigin -> PatOrigin -> Bool #

(/=) :: PatOrigin -> PatOrigin -> Bool #

type Rep PatOrigin Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

data Pattern' x Source #

Patterns are variables, constructors, or wildcards. QName is used in ConP rather than Name since a constructor might come from a particular namespace. This also meshes well with the fact that values (i.e. the arguments we are matching with) use QName.

Constructors

VarP PatternInfo x	x
DotP PatternInfo Term	.t
ConP ConHead ConPatternInfo [NamedArg (Pattern' x)]	`c ps` The subpatterns do not contain any projection copatterns.
LitP PatternInfo Literal	E.g. `5`, `"hello"`.
ProjP ProjOrigin QName	Projection copattern. Can only appear by itself.
IApplyP PatternInfo Term Term x	Path elimination pattern, like `VarP` but keeps track of endpoints.
DefP PatternInfo QName [NamedArg (Pattern' x)]	Used for HITs, the QName should be the one from primHComp.
MaskP (Pattern' x)	Only used during termination checking of clause right-hand sides: a pattern guarded by `MaskP` is not usable for structural recursion. `MaskP` should be `__IMPOSSIBLE__` everywhere outside of the termination checker and the structural functions on patterns (e.g. applySubst).

Instances

Instances details

Reduce DeBruijnPattern Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source #

reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source #

Subst DeBruijnPattern Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern
Instance details Defined in Mikan.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source #

Subst Pattern Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Associated Types

type SubstArg Pattern
Instance details Defined in Mikan.TypeChecking.Substitute type SubstArg Pattern = Term

Methods

applySubst :: Substitution' (SubstArg Pattern) -> Pattern -> Pattern Source #

Subst SplitPattern Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.SplitPattern

Associated Types

type SubstArg SplitPattern
Instance details Defined in Mikan.TypeChecking.Coverage.SplitPattern type SubstArg SplitPattern = SplitPattern

Methods

applySubst :: Substitution' (SubstArg SplitPattern) -> SplitPattern -> SplitPattern Source #

Functor Pattern' Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

fmap :: (a -> b) -> Pattern' a -> Pattern' b #

(<$) :: a -> Pattern' b -> Pattern' a #

Foldable Pattern' Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

fold :: Monoid m => Pattern' m -> m #

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

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

foldr :: (a -> b -> b) -> b -> Pattern' a -> b #

foldr' :: (a -> b -> b) -> b -> Pattern' a -> b #

foldl :: (b -> a -> b) -> b -> Pattern' a -> b #

foldl' :: (b -> a -> b) -> b -> Pattern' a -> b #

foldr1 :: (a -> a -> a) -> Pattern' a -> a #

foldl1 :: (a -> a -> a) -> Pattern' a -> a #

toList :: Pattern' a -> [a] #

null :: Pattern' a -> Bool #

length :: Pattern' a -> Int #

elem :: Eq a => a -> Pattern' a -> Bool #

maximum :: Ord a => Pattern' a -> a #

minimum :: Ord a => Pattern' a -> a #

sum :: Num a => Pattern' a -> a #

product :: Num a => Pattern' a -> a #

Traversable Pattern' Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

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

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

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

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

MapNamedArgPattern a (NamedArg (Pattern' a)) Source #

Modify the content of VarP, and the closest surrounding NamedArg.

Note: the mapNamedArg for Pattern' is not expressible simply by fmap or traverse etc., since ConP has NamedArg subpatterns, which are taken into account by mapNamedArg.

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) Source #

PatternLike a (Pattern' a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m Source #

traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) Source #

DeBruijn (Pattern' a) => TermToPattern Term (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Patterns.Internal

Methods

termToPattern :: Term -> TCM (Pattern' a) Source #

IsProjP (Pattern' a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

isProjP :: Pattern' a -> Maybe (ProjOrigin, AmbiguousQName) Source #

Pretty a => Pretty (Pattern' a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

pretty :: Pattern' a -> Doc Source #

prettyPrec :: Int -> Pattern' a -> Doc Source #

prettyList :: [Pattern' a] -> Doc Source #

NamesIn (Pattern' a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> Pattern' a -> m Source #

CountPatternVars (Pattern' x) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

countPatternVars :: Pattern' x -> Int Source #

HasDefP (Pattern' a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

hasDefP :: Pattern' a -> Bool Source #

PatternVars (Arg (Pattern' a)) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type PatternVarOut (Arg (Pattern' a))
Instance details Defined in Mikan.Syntax.Internal.Pattern type PatternVarOut (Arg (Pattern' a)) = a

Methods

patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source #

PatternVars (NamedArg (Pattern' a)) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type PatternVarOut (NamedArg (Pattern' a))
Instance details Defined in Mikan.Syntax.Internal.Pattern type PatternVarOut (NamedArg (Pattern' a)) = a

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source #

KillRange a => KillRange (Pattern' a) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

killRange :: KillRangeT (Pattern' a) Source #

PrettyTCM a => PrettyTCM (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => Pattern' a -> m Doc Source #

NormaliseProjP (Pattern' x) Source #

Instance details

Defined in Mikan.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Pattern' x -> m (Pattern' x) Source #

InstantiateFull a => InstantiateFull (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: Pattern' a -> ReduceM (Pattern' a) Source #

Normalise a => Normalise (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

normalise' :: Pattern' a -> ReduceM (Pattern' a) Source #

IsFlexiblePattern (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Rules.LHS

Methods

maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => Pattern' a -> MaybeT m FlexibleVarKind Source #

isFlexiblePattern :: HasConstInfo m => Pattern' a -> m Bool Source #

EmbPrj a => EmbPrj (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Pattern' a -> S Word32 Source #

icod_ :: Pattern' a -> S Word32 Source #

value :: Word32 -> R (Pattern' a) Source #

Apply [NamedArg (Pattern' a)] Source #

Make sure we only drop variable patterns.

Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

apply :: [NamedArg (Pattern' a)] -> Args -> [NamedArg (Pattern' a)] Source #

applyE :: [NamedArg (Pattern' a)] -> Elims -> [NamedArg (Pattern' a)] Source #

DeBruijn a => DeBruijn (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

deBruijnVar :: Int -> Pattern' a Source #

deBruijnNamedVar :: ShortText -> Int -> Pattern' a Source #

deBruijnView :: Pattern' a -> Maybe Int Source #

DeBruijn a => IApplyVars (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Telescope.Path

Methods

iApplyVars :: Pattern' a -> [Int] Source #

NFData x => NFData (Pattern' x) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

rnf :: Pattern' x -> () #

Generic (Pattern' x) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type Rep (Pattern' x)

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

from :: Pattern' x -> Rep (Pattern' x) x0 #

to :: Rep (Pattern' x) x0 -> Pattern' x #

Show x => Show (Pattern' x) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

showsPrec :: Int -> Pattern' x -> ShowS #

show :: Pattern' x -> String #

showList :: [Pattern' x] -> ShowS #

Eq a => Eq (Pattern' a) Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

(==) :: Pattern' a -> Pattern' a -> Bool #

(/=) :: Pattern' a -> Pattern' a -> Bool #

type SubstArg DeBruijnPattern Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg DeBruijnPattern = DeBruijnPattern

type SubstArg Pattern Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg Pattern = Term

type SubstArg SplitPattern Source #

Instance details

Defined in Mikan.TypeChecking.Coverage.SplitPattern

type SubstArg SplitPattern = SplitPattern

type PatternVarOut (Arg (Pattern' a)) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

type PatternVarOut (Arg (Pattern' a)) = a

type PatternVarOut (NamedArg (Pattern' a)) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

type PatternVarOut (NamedArg (Pattern' a)) = a

type Rep (Pattern' x) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

type Pattern Source #

Arguments

= Pattern' PatVarName

The PatVarName is a name suggestion.

varP :: a -> Pattern' a Source #

dotP :: Term -> Pattern' a Source #

litP :: Literal -> Pattern' a Source #

data DBPatVar Source #

Type used when numbering pattern variables.

Constructors

DBPatVar
Fields dbPatVarName :: PatVarName dbPatVarIndex :: !Int

Instances

Instances details

Pretty DBPatVar Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

pretty :: DBPatVar -> Doc Source #

prettyPrec :: Int -> DBPatVar -> Doc Source #

prettyList :: [DBPatVar] -> Doc Source #

KillRange DBPatVar Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

killRange :: KillRangeT DBPatVar Source #

PrettyTCM DBPatVar Source #

Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => DBPatVar -> m Doc Source #

InstantiateFull DBPatVar Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: DBPatVar -> ReduceM DBPatVar Source #

Normalise DBPatVar Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

normalise' :: DBPatVar -> ReduceM DBPatVar Source #

Reduce DeBruijnPattern Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

reduce' :: DeBruijnPattern -> ReduceM DeBruijnPattern Source #

reduceB' :: DeBruijnPattern -> ReduceM (Blocked DeBruijnPattern) Source #

EmbPrj DBPatVar Source #

Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: DBPatVar -> S Word32 Source #

icod_ :: DBPatVar -> S Word32 Source #

value :: Word32 -> R DBPatVar Source #

Subst DeBruijnPattern Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Associated Types

type SubstArg DeBruijnPattern
Instance details Defined in Mikan.TypeChecking.Substitute type SubstArg DeBruijnPattern = DeBruijnPattern

Methods

applySubst :: Substitution' (SubstArg DeBruijnPattern) -> DeBruijnPattern -> DeBruijnPattern Source #

DeBruijn DBPatVar Source #

Instance details

Defined in Mikan.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> DBPatVar Source #

deBruijnNamedVar :: ShortText -> Int -> DBPatVar Source #

deBruijnView :: DBPatVar -> Maybe Int Source #

NFData DBPatVar Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

rnf :: DBPatVar -> () #

Generic DBPatVar Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type Rep DBPatVar

Instance details

Defined in Mikan.Syntax.Internal.Pattern

type Rep DBPatVar = D1 ('MetaData "DBPatVar" "Mikan.Syntax.Internal.Pattern" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "DBPatVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "dbPatVarName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatVarName) :*: S1 ('MetaSel ('Just "dbPatVarIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

Methods

from :: DBPatVar -> Rep DBPatVar x #

to :: Rep DBPatVar x -> DBPatVar #

Show DBPatVar Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

showsPrec :: Int -> DBPatVar -> ShowS #

show :: DBPatVar -> String #

showList :: [DBPatVar] -> ShowS #

Eq DBPatVar Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

(==) :: DBPatVar -> DBPatVar -> Bool #

(/=) :: DBPatVar -> DBPatVar -> Bool #

type SubstArg DeBruijnPattern Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg DeBruijnPattern = DeBruijnPattern

type Rep DBPatVar Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

type Rep DBPatVar = D1 ('MetaData "DBPatVar" "Mikan.Syntax.Internal.Pattern" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "DBPatVar" 'PrefixI 'True) (S1 ('MetaSel ('Just "dbPatVarName") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatVarName) :*: S1 ('MetaSel ('Just "dbPatVarIndex") 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 Int)))

type DeBruijnPattern = Pattern' DBPatVar Source #

type PatternSubstitution = Substitution' DeBruijnPattern Source #

type NAPs = [NamedArg DeBruijnPattern] Source #

Named pattern arguments.

namedVarP :: PatVarName -> Named_ Pattern Source #

namedDBVarP :: Int -> PatVarName -> Named_ DeBruijnPattern Source #

absurdP :: Int -> DeBruijnPattern Source #

Make an absurd pattern with the given de Bruijn index.

data ConPatternInfo Source #

The ConPatternInfo states whether the constructor belongs to a record type (True) or data type (False). In the former case, the PatOrigin of the conPInfo says whether the record pattern orginates from the expansion of an implicit pattern. The Type is the type of the whole record pattern. The scope used for the type is given by any outer scope plus the clause's telescope (clauseTel).

Constructors

ConPatternInfo

Fields

conPInfo :: PatternInfo
Information on the origin of the pattern.
conPRecord :: Bool
False if data constructor. True if record constructor.
conPFallThrough :: Bool
Should the match block on non-canonical terms or can it proceed to the catch-all clause?
conPType :: Maybe (Arg Type)
The type of the whole constructor pattern. Should be present (Just) if constructor pattern is is generated ordinarily by type-checking. Could be absent (Nothing) if pattern comes from some plugin (like Agsy). Needed e.g. for with-clause stripping.
conPLazy :: Bool
Lazy patterns are generated by the forcing translation in the unifier (unifyStep) and are dropped by the clause compiler (TODO: not yet) (compileClauses) when the variables they bind are unused.

Instances

Instances details

NamesIn ConPatternInfo Source #

Instance details

Defined in Mikan.Syntax.Internal.Names

Methods

namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> ConPatternInfo -> m Source #

KillRange ConPatternInfo Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

killRange :: KillRangeT ConPatternInfo Source #

InstantiateFull ConPatternInfo Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: ConPatternInfo -> ReduceM ConPatternInfo Source #

Normalise ConPatternInfo Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

normalise' :: ConPatternInfo -> ReduceM ConPatternInfo Source #

EmbPrj ConPatternInfo Source #

Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ConPatternInfo -> S Word32 Source #

icod_ :: ConPatternInfo -> S Word32 Source #

value :: Word32 -> R ConPatternInfo Source #

Subst ConPatternInfo Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Associated Types

type SubstArg ConPatternInfo
Instance details Defined in Mikan.TypeChecking.Substitute type SubstArg ConPatternInfo = Term

Methods

applySubst :: Substitution' (SubstArg ConPatternInfo) -> ConPatternInfo -> ConPatternInfo Source #

NFData ConPatternInfo Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

rnf :: ConPatternInfo -> () #

Generic ConPatternInfo Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type Rep ConPatternInfo

Instance details

Defined in Mikan.Syntax.Internal.Pattern

type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Mikan.Syntax.Internal.Pattern" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "ConPatternInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conPInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Just "conPRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "conPFallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conPType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: S1 ('MetaSel ('Just "conPLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

Methods

from :: ConPatternInfo -> Rep ConPatternInfo x #

to :: Rep ConPatternInfo x -> ConPatternInfo #

Show ConPatternInfo Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Methods

showsPrec :: Int -> ConPatternInfo -> ShowS #

show :: ConPatternInfo -> String #

showList :: [ConPatternInfo] -> ShowS #

type SubstArg ConPatternInfo Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

type SubstArg ConPatternInfo = Term

type Rep ConPatternInfo Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

type Rep ConPatternInfo = D1 ('MetaData "ConPatternInfo" "Mikan.Syntax.Internal.Pattern" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "ConPatternInfo" 'PrefixI 'True) ((S1 ('MetaSel ('Just "conPInfo") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 PatternInfo) :*: S1 ('MetaSel ('Just "conPRecord") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)) :*: (S1 ('MetaSel ('Just "conPFallThrough") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool) :*: (S1 ('MetaSel ('Just "conPType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: S1 ('MetaSel ('Just "conPLazy") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Bool)))))

noConPatternInfo :: ConPatternInfo Source #

toConPatternInfo :: ConInfo -> ConPatternInfo Source #

Build partial ConPatternInfo from ConInfo

fromConPatternInfo :: ConPatternInfo -> ConInfo Source #

Build ConInfo from ConPatternInfo.

class PatternVars a where Source #

Extract pattern variables in left-to-right order. A DotP is also treated as variable (see docu for Clause).

Associated Types

type PatternVarOut a Source #

Methods

patternVars :: a -> [Arg (Either (PatternVarOut a) Term)] Source #

Instances

Instances details

PatternVars (Arg (Pattern' a)) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type PatternVarOut (Arg (Pattern' a))
Instance details Defined in Mikan.Syntax.Internal.Pattern type PatternVarOut (Arg (Pattern' a)) = a

Methods

patternVars :: Arg (Pattern' a) -> [Arg (Either (PatternVarOut (Arg (Pattern' a))) Term)] Source #

PatternVars (NamedArg (Pattern' a)) Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type PatternVarOut (NamedArg (Pattern' a))
Instance details Defined in Mikan.Syntax.Internal.Pattern type PatternVarOut (NamedArg (Pattern' a)) = a

Methods

patternVars :: NamedArg (Pattern' a) -> [Arg (Either (PatternVarOut (NamedArg (Pattern' a))) Term)] Source #

PatternVars a => PatternVars [a] Source #

Instance details

Defined in Mikan.Syntax.Internal.Pattern

Associated Types

type PatternVarOut [a]
Instance details Defined in Mikan.Syntax.Internal.Pattern type PatternVarOut [a] = PatternVarOut a

Methods

patternVars :: [a] -> [Arg (Either (PatternVarOut [a]) Term)] Source #

patternInfo :: Pattern' x -> Maybe PatternInfo Source #

Retrieve the PatternInfo from a pattern

patternOrigin :: Pattern' x -> Maybe PatOrigin Source #

Retrieve the origin of a pattern

Absurd Lambda

absurdPatternName :: PatVarName Source #

Tools for patterns

dbPatPerm :: [NamedArg DeBruijnPattern] -> Maybe Permutation Source #

dbPatPerm' :: Bool -> [NamedArg DeBruijnPattern] -> Maybe Permutation Source #

Computes the permutation from the clause telescope to the pattern variables.

Use as fromMaybe IMPOSSIBLE . dbPatPerm to crash in a controlled way if a de Bruijn index is out of scope here.

The first argument controls whether dot patterns counts as variables or not.

patternToElim :: Arg DeBruijnPattern -> Elim Source #

Turn a pattern into a term. Projection patterns are turned into projection eliminations, other patterns into apply elimination.

patternsToElims :: [NamedArg DeBruijnPattern] -> [Elim] Source #

patternToTerm :: DeBruijnPattern -> Term Source #

class MapNamedArgPattern a p where Source #

Minimal complete definition

Nothing

Methods

mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p Source #

default mapNamedArgPattern :: forall (f :: Type -> Type) p'. (Functor f, MapNamedArgPattern a p', p ~ f p') => (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> p -> p Source #

Instances

Instances details

MapNamedArgPattern a (NamedArg (Pattern' a)) Source #	Modify the content of `VarP`, and the closest surrounding `NamedArg`. Note: the `mapNamedArg` for `Pattern'` is not expressible simply by `fmap` or `traverse` etc., since `ConP` has `NamedArg` subpatterns, which are taken into account by `mapNamedArg`.
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> NamedArg (Pattern' a) -> NamedArg (Pattern' a) Source #
MapNamedArgPattern a p => MapNamedArgPattern a [p] Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods mapNamedArgPattern :: (NamedArg (Pattern' a) -> NamedArg (Pattern' a)) -> [p] -> [p] Source #

class PatternLike a b where Source #

Generic pattern traversal.

Pre-applies a pattern modification, recurses, and post-applies another one.

Minimal complete definition

Nothing

Methods

foldrPattern Source #

Arguments

:: Monoid m
=> (Pattern' a -> m -> m)	Combine a pattern and the value computed from its subpatterns.
-> b
-> m

Fold pattern.

default foldrPattern :: forall m (f :: Type -> Type) p. (Monoid m, Foldable f, PatternLike a p, f p ~ b) => (Pattern' a -> m -> m) -> b -> m Source #

traversePatternM Source #

Arguments

:: Monad m
=> (Pattern' a -> m (Pattern' a))	`pre`: Modification before recursion.
-> (Pattern' a -> m (Pattern' a))	`post`: Modification after recursion.
-> b
-> m b

Traverse pattern.

default traversePatternM :: forall (f :: Type -> Type) p m. (Traversable f, PatternLike a p, f p ~ b, Monad m) => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> b -> m b Source #

Instances

Instances details

PatternLike a b => PatternLike a (Arg b) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Arg b -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Arg b -> m (Arg b) Source #
PatternLike a (Pattern' a) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Pattern' a -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Pattern' a -> m (Pattern' a) Source #
PatternLike a b => PatternLike a [b] Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> [b] -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> [b] -> m [b] Source #
PatternLike a b => PatternLike a (Named x b) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods foldrPattern :: Monoid m => (Pattern' a -> m -> m) -> Named x b -> m Source # traversePatternM :: Monad m => (Pattern' a -> m (Pattern' a)) -> (Pattern' a -> m (Pattern' a)) -> Named x b -> m (Named x b) Source #

foldPattern :: (PatternLike a b, Monoid m) => (Pattern' a -> m) -> b -> m Source #

Compute from each subpattern a value and collect them all in a monoid.

preTraversePatternM Source #

Arguments

:: (PatternLike a b, Monad m)
=> (Pattern' a -> m (Pattern' a))	`pre`: Modification before recursion.
-> b
-> m b

Traverse pattern(s) with a modification before the recursive descent.

postTraversePatternM Source #

Arguments

:: (PatternLike a b, Monad m)
=> (Pattern' a -> m (Pattern' a))	`post`: Modification after recursion.
-> b
-> m b

Traverse pattern(s) with a modification after the recursive descent.

class CountPatternVars a where Source #

Minimal complete definition

Nothing

Methods

countPatternVars :: a -> Int Source #

default countPatternVars :: forall (f :: Type -> Type) b. (Foldable f, CountPatternVars b, f b ~ a) => a -> Int Source #

Instances

Instances details

CountPatternVars a => CountPatternVars (Arg a) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods countPatternVars :: Arg a -> Int Source #
CountPatternVars (Pattern' x) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods countPatternVars :: Pattern' x -> Int Source #
CountPatternVars a => CountPatternVars [a] Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods countPatternVars :: [a] -> Int Source #
CountPatternVars a => CountPatternVars (Named x a) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods countPatternVars :: Named x a -> Int Source #

class HasDefP a where Source #

Minimal complete definition

Nothing

Methods

hasDefP :: a -> Bool Source #

Check whether any of the patterns in the given thing are DefPs.

default hasDefP :: forall (f :: Type -> Type) b. (Foldable f, HasDefP b, a ~ f b) => a -> Bool Source #

Instances

Instances details

HasDefP Clause Source #
Instance details Defined in Mikan.Syntax.Internal.Clause Methods hasDefP :: Clause -> Bool Source #
HasDefP a => HasDefP (Arg a) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods hasDefP :: Arg a -> Bool Source #
HasDefP a => HasDefP (Named_ a) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods hasDefP :: Named_ a -> Bool Source #
HasDefP (Pattern' a) Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods hasDefP :: Pattern' a -> Bool Source #
HasDefP a => HasDefP [a] Source #
Instance details Defined in Mikan.Syntax.Internal.Pattern Methods hasDefP :: [a] -> Bool Source #