Mikan

Safe Haskell	None
Language	Haskell2010

Mikan.Syntax.Internal.Clause

Contents

Clauses
Recursivity marks

Synopsis

data Clause = Clause {
- clauseLHSRange :: Range
- clauseFullRange :: Range
- clauseTel :: Telescope
- namedClausePats :: NAPs
- clauseBody :: Maybe Term
- clauseType :: Maybe (Arg Type)
- clauseCatchall :: Catchall
- clauseRecursive :: ClauseRecursive
- clauseUnreachable :: Maybe Bool
- clauseEllipsis :: ExpandedEllipsis
- clauseWhereModule :: Maybe ModuleName
}
clausePats :: Clause -> [Arg DeBruijnPattern]
clausePerm :: Clause -> Maybe Permutation
clauseArgs :: Clause -> Args
clauseElims :: Clause -> Elims
data ClauseRecursive
- = YesRecursive
- | NotRecursive
- | MaybeRecursive
decideRecursive :: Bool -> ClauseRecursive
couldBeRecursive :: ClauseRecursive -> Bool

Clauses

data Clause Source #

A clause is a list of patterns and the clause body.

The telescope contains the types of the pattern variables and the de Bruijn indices say how to get from the order the variables occur in the patterns to the order they occur in the telescope. The body binds the variables in the order they appear in the telescope.

clauseTel ~ permute clausePerm (patternVars namedClausePats)

Terms in dot patterns are valid in the clause telescope.

For the purpose of the permutation and the body dot patterns count as variables. TODO: Change this!

Constructors

Fields

clauseLHSRange :: Range
clauseFullRange :: Range
clauseTel :: Telescope
Δ: The types of the pattern variables in dependency order.
namedClausePats :: NAPs
Δ ⊢ ps. The de Bruijn indices refer to Δ.
clauseBody :: Maybe Term
Just v with Δ ⊢ v for a regular clause, or Nothing for an absurd one.
clauseType :: Maybe (Arg Type)
Δ ⊢ t. The type of the rhs under clauseTel. Used, e.g., by TermCheck. The ArgInfo remembers whether we are under a copattern for an instance/tactic field, for example.
clauseCatchall :: Catchall
Clause has been labelled as CATCHALL.
clauseRecursive :: ClauseRecursive
clauseBody contains recursive calls? Computed by termination checker.
clauseUnreachable :: Maybe Bool
Clause has been labelled as unreachable by the coverage checker. Nothing means coverage checker has not run yet (clause may be unreachable). Just False means clause is not unreachable. Just True means clause is unreachable.
clauseEllipsis :: ExpandedEllipsis
Was this clause created by expansion of an ellipsis?
clauseWhereModule :: Maybe ModuleName
Keeps track of the module name associate with the clause's where clause.

Instances

Instances details

Pretty Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

pretty :: Clause -> Doc Source #

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

prettyList :: [Clause] -> Doc Source #

GetDefs Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Defs

Methods

getDefs :: (Monoid m, ExpandCase LiftedRep m) => (MetaId -> Maybe Term) -> (QName -> m) -> Clause -> m Source #

NamesIn Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Names

Methods

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

HasDefP Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

hasDefP :: Clause -> Bool Source #

HasRange Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

getRange :: Clause -> Range Source #

KillRange Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

killRange :: KillRangeT Clause Source #

DropArgs Clause Source #

NOTE: does not work for recursive functions.

Instance details

Defined in Mikan.TypeChecking.DropArgs

Methods

dropArgs :: Int -> Clause -> Clause Source #

DropArgs FunctionInverse Source #

Instance details

Defined in Mikan.TypeChecking.DropArgs

Methods

dropArgs :: Int -> FunctionInverse -> FunctionInverse Source #

Free Clause Source #

Instance details

Defined in Mikan.TypeChecking.Free.Generic

Methods

freeVars :: ComputeFree r => Clause -> Reader r (Collect r) Source #

PrettyTCM Clause Source #

Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

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

NormaliseProjP Clause Source #

Instance details

Defined in Mikan.TypeChecking.Records

Methods

normaliseProjP :: HasConstInfo m => Clause -> m Clause Source #

InstantiateFull Clause Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: Clause -> ReduceM Clause Source #

InstantiateFull FunctionInverse Source #

Instance details

Defined in Mikan.TypeChecking.Reduce

Methods

instantiateFull' :: FunctionInverse -> ReduceM FunctionInverse Source #

EmbPrj Clause Source #

Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: Clause -> S Word32 Source #

icod_ :: Clause -> S Word32 Source #

value :: Word32 -> R Clause Source #

Abstract Clause Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

abstract :: Telescope -> Clause -> Clause Source #

Abstract FunctionInverse Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

abstract :: Telescope -> FunctionInverse -> FunctionInverse Source #

Apply Clause Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

apply :: Clause -> Args -> Clause Source #

applyE :: Clause -> Elims -> Clause Source #

Apply FunctionInverse Source #

Instance details

Defined in Mikan.TypeChecking.Substitute

Methods

apply :: FunctionInverse -> Args -> FunctionInverse Source #

applyE :: FunctionInverse -> Elims -> FunctionInverse Source #

Null Clause Source #

A null clause is one with no patterns and no rhs. Should not exist in practice.

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

empty :: Clause Source #

null :: Clause -> Bool Source #

NFData Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

rnf :: Clause -> () #

Generic Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Associated Types

type Rep Clause

Instance details

Defined in Mikan.Syntax.Internal.Clause

type Rep Clause = D1 ('MetaData "Clause" "Mikan.Syntax.Internal.Clause" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) (((S1 ('MetaSel ('Just "clauseLHSRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "clauseFullRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "clauseTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Just "namedClausePats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAPs) :*: S1 ('MetaSel ('Just "clauseBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Term))))) :*: ((S1 ('MetaSel ('Just "clauseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: (S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Just "clauseRecursive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ClauseRecursive))) :*: (S1 ('MetaSel ('Just "clauseUnreachable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: (S1 ('MetaSel ('Just "clauseEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis) :*: S1 ('MetaSel ('Just "clauseWhereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)))))))

Methods

from :: Clause -> Rep Clause x #

to :: Rep Clause x -> Clause #

Show Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

showsPrec :: Int -> Clause -> ShowS #

show :: Clause -> String #

showList :: [Clause] -> ShowS #

Reify (QNamed Clause) Source #

Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

Associated Types

type ReifiesTo (QNamed Clause)
Instance details Defined in Mikan.Syntax.Translation.InternalToAbstract type ReifiesTo (QNamed Clause) = Clause

Methods

reify :: MonadReify m => QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #

reifyWhen :: MonadReify m => Bool -> QNamed Clause -> m (ReifiesTo (QNamed Clause)) Source #

PrettyTCM (QNamed Clause) Source #

Instance details

Defined in Mikan.TypeChecking.Pretty

Methods

prettyTCM :: MonadPretty m => QNamed Clause -> m Doc Source #

type Rep Clause Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

type Rep Clause = D1 ('MetaData "Clause" "Mikan.Syntax.Internal.Clause" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Clause" 'PrefixI 'True) (((S1 ('MetaSel ('Just "clauseLHSRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range) :*: S1 ('MetaSel ('Just "clauseFullRange") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :*: (S1 ('MetaSel ('Just "clauseTel") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Telescope) :*: (S1 ('MetaSel ('Just "namedClausePats") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 NAPs) :*: S1 ('MetaSel ('Just "clauseBody") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Term))))) :*: ((S1 ('MetaSel ('Just "clauseType") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe (Arg Type))) :*: (S1 ('MetaSel ('Just "clauseCatchall") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Catchall) :*: S1 ('MetaSel ('Just "clauseRecursive") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ClauseRecursive))) :*: (S1 ('MetaSel ('Just "clauseUnreachable") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe Bool)) :*: (S1 ('MetaSel ('Just "clauseEllipsis") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 ExpandedEllipsis) :*: S1 ('MetaSel ('Just "clauseWhereModule") 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 (Maybe ModuleName)))))))

type ReifiesTo (QNamed Clause) Source #

Instance details

Defined in Mikan.Syntax.Translation.InternalToAbstract

type ReifiesTo (QNamed Clause) = Clause

clausePats :: Clause -> [Arg DeBruijnPattern] Source #

clausePerm :: Clause -> Maybe Permutation Source #

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

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

clauseArgs :: Clause -> Args Source #

Translate the clause patterns to terms with free variables bound by the clause telescope.

Precondition: no projection patterns.

clauseElims :: Clause -> Elims Source #

Translate the clause patterns to an elimination spine with free variables bound by the clause telescope.

Recursivity marks

data ClauseRecursive Source #

Does the clause body contain calls to any of the mutually recursive functions?

Constructors

YesRecursive	Definitely a call to a mutually recursive function.
NotRecursive	Definitely no call to a mutually recursive function.
MaybeRecursive	Don't know because the analysis has not run yet.

Instances

Instances details

Pretty ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

pretty :: ClauseRecursive -> Doc Source #

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

prettyList :: [ClauseRecursive] -> Doc Source #

KillRange ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

killRange :: KillRangeT ClauseRecursive Source #

EmbPrj ClauseRecursive Source #

Instance details

Defined in Mikan.TypeChecking.Serialise.Instances.Internal

Methods

icode :: ClauseRecursive -> S Word32 Source #

icod_ :: ClauseRecursive -> S Word32 Source #

value :: Word32 -> R ClauseRecursive Source #

Null ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

empty :: ClauseRecursive Source #

null :: ClauseRecursive -> Bool Source #

NFData ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

rnf :: ClauseRecursive -> () #

Bounded ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

minBound :: ClauseRecursive #

maxBound :: ClauseRecursive #

Enum ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

succ :: ClauseRecursive -> ClauseRecursive #

pred :: ClauseRecursive -> ClauseRecursive #

toEnum :: Int -> ClauseRecursive #

fromEnum :: ClauseRecursive -> Int #

enumFrom :: ClauseRecursive -> [ClauseRecursive] #

enumFromThen :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive] #

enumFromTo :: ClauseRecursive -> ClauseRecursive -> [ClauseRecursive] #

enumFromThenTo :: ClauseRecursive -> ClauseRecursive -> ClauseRecursive -> [ClauseRecursive] #

Generic ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Associated Types

type Rep ClauseRecursive

Instance details

Defined in Mikan.Syntax.Internal.Clause

type Rep ClauseRecursive = D1 ('MetaData "ClauseRecursive" "Mikan.Syntax.Internal.Clause" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "YesRecursive" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotRecursive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MaybeRecursive" 'PrefixI 'False) (U1 :: Type -> Type)))

Methods

from :: ClauseRecursive -> Rep ClauseRecursive x #

to :: Rep ClauseRecursive x -> ClauseRecursive #

Show ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

showsPrec :: Int -> ClauseRecursive -> ShowS #

show :: ClauseRecursive -> String #

showList :: [ClauseRecursive] -> ShowS #

Eq ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

Methods

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

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

type Rep ClauseRecursive Source #

Instance details

Defined in Mikan.Syntax.Internal.Clause

type Rep ClauseRecursive = D1 ('MetaData "ClauseRecursive" "Mikan.Syntax.Internal.Clause" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "YesRecursive" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "NotRecursive" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "MaybeRecursive" 'PrefixI 'False) (U1 :: Type -> Type)))

decideRecursive :: Bool -> ClauseRecursive Source #

couldBeRecursive :: ClauseRecursive -> Bool Source #