| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.Syntax.Common
Contents
Description
Some common syntactic entities are defined in this module.
Synopsis
- pattern IsRecord_ :: DataOrRecord_
- _fixityAssoc :: Lens' Fixity Associativity
- _fixityLevel :: Lens' Fixity FixityLevel
- appendArgNames :: ArgName -> ArgName -> ArgName
- argNameToString :: ArgName -> ShortText
- bareNameOf :: (LensNamed a, NameOf a ~ NamedName) => a -> Maybe ArgName
- bareNameWithDefault :: (LensNamed a, NameOf a ~ NamedName) => ArgName -> a -> ArgName
- bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin
- defaultArg :: a -> Arg a
- defaultArgInfo :: ArgInfo
- defaultFixity :: Fixity
- defaultImportDir :: ImportDirective' n m
- defaultNamedArg :: a -> NamedArg a
- emptyRecordDirectives :: Null a => RecordDirectives' a
- fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool
- freeVariablesFromList :: [Int] -> FreeVariables
- fromImportedName :: ImportedName' a a -> a
- getFreeVariablesArgInfo :: LensArgInfo a => LensGet a FreeVariables
- getHidingArgInfo :: LensArgInfo a => LensGet a Hiding
- getNameOf :: LensNamed a => a -> Maybe (NameOf a)
- getOriginArgInfo :: LensArgInfo a => LensGet a Origin
- hasNoFreeVariables :: LensFreeVariables a => a -> Bool
- hidden :: LensHiding a => a -> Bool
- hide :: LensHiding a => a -> a
- hideExplicit :: LensHiding a => a -> a
- hidingToString :: Hiding -> String
- isDefaultImportDir :: ImportDirective' n m -> Bool
- isIncoherent :: HasOverlapMode a => a -> Bool
- isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool
- isInstance :: LensHiding a => a -> Bool
- isKindPattern :: ExprKind -> Bool
- isOverlappable :: HasOverlapMode a => a -> Bool
- isOverlapping :: HasOverlapMode a => a -> Bool
- isUnnamed :: Named name a -> Maybe a
- isYesOverlap :: LensHiding a => a -> Bool
- itsRange :: HasRange a => a -> Ranged a
- makeInstance :: LensHiding a => a -> a
- makeInstance' :: LensHiding a => Overlappable -> a -> a
- mapFreeVariablesArgInfo :: LensArgInfo a => LensMap a FreeVariables
- mapHidingArgInfo :: LensArgInfo a => LensMap a Hiding
- mapNameOf :: LensNamed a => (Maybe (NameOf a) -> Maybe (NameOf a)) -> a -> a
- mapOriginArgInfo :: LensArgInfo a => LensMap a Origin
- mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2
- named :: name -> a -> Named name a
- namedArg :: NamedArg a -> a
- namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool
- noFixity :: Fixity
- noFixity' :: Fixity'
- noFreeVariables :: FreeVariables
- noNotation :: Notation
- noPlaceholder :: e -> MaybePlaceholder e
- notVisible :: LensHiding a => a -> Bool
- oneFreeVariable :: Int -> FreeVariables
- pDom :: LensHiding a => a -> Doc -> Doc
- partitionImportedNames :: [ImportedName' n m] -> ([n], [m])
- prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc
- privateAccessInserted :: Access
- rawNameToString :: RawName -> ShortText
- sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool
- sameName :: NamedName -> NamedName -> Bool
- setFreeVariablesArgInfo :: LensArgInfo a => LensSet a FreeVariables
- setHidingArgInfo :: LensArgInfo a => LensSet a Hiding
- setImportedName :: ImportedName' a a -> a -> ImportedName' a a
- setNameOf :: LensNamed a => Maybe (NameOf a) -> a -> a
- setNamedArg :: NamedArg a -> b -> NamedArg b
- setOriginArgInfo :: LensArgInfo a => LensSet a Origin
- stringToArgName :: ShortText -> ArgName
- stringToRawName :: ShortText -> RawName
- unArgKeepHiding :: Arg a -> WithHiding a
- unknownFreeVariables :: FreeVariables
- unnamed :: a -> Named name a
- unnamedArg :: ArgInfo -> a -> NamedArg a
- unranged :: a -> Ranged a
- updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b
- updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b)
- userNamed :: Ranged ArgName -> a -> Named_ a
- visible :: LensHiding a => a -> Bool
- withArgsFrom :: [a] -> [Arg b] -> [Arg a]
- withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a]
- data Access
- class AllAreOpaque a where
- jointOpacity :: a -> JointOpacity
- class AnyIsAbstract a where
- anyIsAbstract :: a -> IsAbstract
- data Arg e = Arg {}
- data ArgInfo = ArgInfo {}
- type ArgName = ShortText
- type Arity = Nat
- data Associativity
- type BackendName = ShortText
- data BinderNameOrigin
- data BoundVariablePosition = BoundVariablePosition {
- holeNumber :: !Int
- varNumber :: !Int
- data Catchall
- data ConOrigin
- newtype Constr a = Constr a
- data ConstructorOrPatternSynonym
- class CopatternMatchingAllowed a where
- copatternMatchingAllowed :: a -> Bool
- data CoverageCheck
- type DataOrRecord = DataOrRecord' PatternOrCopattern
- data DataOrRecord' p
- type DataOrRecord_ = DataOrRecord' ()
- data DisplayLHS
- data ExpandedEllipsis
- = ExpandedEllipsis { }
- | NoEllipsis
- data ExprKind
- data FileType
- data Fixity = Fixity {}
- data Fixity' = Fixity' {
- theFixity :: !Fixity
- theNotation :: Notation
- theNameRange :: Range
- data FixityLevel
- data FreeVariables
- = UnknownFVs
- | KnownFVs !VarSet
- type HasEta = HasEta' PatternOrCopattern
- data HasEta' a
- type HasEta0 = HasEta' ()
- class HasOverlapMode a where
- data Hiding
- type HidingDirective' n m = [ImportedName' n m]
- data ImportDirective' n m = ImportDirective {
- importDirRange :: Range
- using :: Using' n m
- hiding :: HidingDirective' n m
- impRenaming :: RenamingDirective' n m
- publicOpen :: Maybe KwRange
- data ImportedName' n m
- = ImportedModule m
- | ImportedName n
- newtype InteractionId = InteractionId {
- interactionId :: Nat
- data IsAbstract
- data IsInfix
- data IsInstance
- class IsInstanceDef a where
- isInstanceDef :: a -> Maybe KwRange
- data IsMacro
- data IsMain
- data IsOpaque
- data JointOpacity
- class LensArgInfo a where
- getArgInfo :: a -> ArgInfo
- setArgInfo :: ArgInfo -> a -> a
- mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a
- class LensFixity a where
- lensFixity :: Lens' a Fixity
- class LensFixity' a where
- lensFixity' :: Lens' a Fixity'
- class LensFreeVariables a where
- getFreeVariables :: a -> FreeVariables
- setFreeVariables :: FreeVariables -> a -> a
- mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a
- class LensHiding a where
- class LensIsAbstract a where
- class LensIsOpaque a where
- lensIsOpaque :: Lens' a IsOpaque
- class LensNamed a where
- class LensOrigin a where
- data MaybePlaceholder e
- data MetaId = MetaId {
- metaId :: !Word64
- metaModule :: !ModuleNameHash
- data NameId = NameId !Word64 !ModuleNameHash
- type family NameOf a
- data Named name a = Named {
- nameOf :: Maybe name
- namedThing :: a
- type NamedArg a = Arg (Named_ a)
- type NamedName = WithOrigin (Ranged ArgName)
- type Named_ = Named NamedName
- type Nat = Int
- type Nat1 = Nat
- type Notation = [NotationPart]
- data NotationPart
- data OpaqueId = OpaqueId !Word64 !ModuleNameHash
- data Origin
- data OverlapMode
- data Overlappable
- class PatternMatchingAllowed a where
- patternMatchingAllowed :: a -> Bool
- data PatternOrCopattern
- data PositionInName
- data PositivityCheck
- type PrecedenceLevel = Double
- newtype ProblemId = ProblemId Word64
- data ProjOrigin
- type RString = Ranged RawName
- data Ranged a = Ranged {
- rangeOf :: Range
- rangedThing :: a
- type RawName = ShortText
- data RecordDirectives' a = RecordDirectives {
- recInductive :: Maybe (Ranged Induction)
- recHasEta :: Maybe (Ranged HasEta0)
- recPattern :: Maybe Range
- recConstructor :: a
- data Renaming' n m = Renaming {
- renFrom :: ImportedName' n m
- renTo :: ImportedName' n m
- renFixity :: Maybe Fixity
- renToRange :: Range
- type RenamingDirective' n m = [Renaming' n m]
- data RewriteEqn' qn nm p e
- data TerminationCheck
- class Eq a => Underscore a where
- underscore :: a
- isUnderscore :: a -> Bool
- data UniverseCheck
- data Using' n m
- = UseEverything
- | Using [ImportedName' n m]
- data WithHiding a = WithHiding {}
- data WithOrigin a = WithOrigin {}
- module Mikan.Syntax.Common.KeywordRange
- module Mikan.Syntax.TopLevelModuleName.Boot
- data Induction
Documentation
pattern IsRecord_ :: DataOrRecord_ Source #
argNameToString :: ArgName -> ShortText Source #
bestConInfo :: ConOrigin -> ConOrigin -> ConOrigin Source #
Prefer user-written over system-inserted.
defaultArg :: a -> Arg a Source #
defaultImportDir :: ImportDirective' n m Source #
Default is directive is private (use everything, but do not export).
defaultNamedArg :: a -> NamedArg a Source #
emptyRecordDirectives :: Null a => RecordDirectives' a Source #
fittingNamedArg :: (LensNamed arg, NameOf arg ~ NamedName, LensHiding arg, LensNamed dom, NameOf dom ~ NamedName, LensHiding dom) => arg -> dom -> Maybe Bool Source #
Does an argument arg fit the shape dom of the next expected argument?
The hiding has to match, and if the argument has a name, it should match the name of the domain.
Nothing should be __IMPOSSIBLE__, so use as
@
fromMaybe IMPOSSIBLE $ fittingNamedArg arg dom
@
freeVariablesFromList :: [Int] -> FreeVariables Source #
fromImportedName :: ImportedName' a a -> a Source #
getHidingArgInfo :: LensArgInfo a => LensGet a Hiding Source #
getOriginArgInfo :: LensArgInfo a => LensGet a Origin Source #
hasNoFreeVariables :: LensFreeVariables a => a -> Bool Source #
:: LensHiding a => a -> Bool Source #
Hidden arguments are hidden.
hide :: LensHiding a => a -> a Source #
hideExplicit :: LensHiding a => a -> a Source #
Hide a NotHidden thing.
hidingToString :: Hiding -> String Source #
isDefaultImportDir :: ImportDirective' n m -> Bool Source #
isDefaultImportDir implies null, but not the other way round.
isIncoherent :: HasOverlapMode a => a -> Bool Source #
isInsertedHidden :: (LensHiding a, LensOrigin a) => a -> Bool Source #
isInstance :: LensHiding a => a -> Bool Source #
isKindPattern :: ExprKind -> Bool Source #
isOverlappable :: HasOverlapMode a => a -> Bool Source #
isOverlapping :: HasOverlapMode a => a -> Bool Source #
isYesOverlap :: LensHiding a => a -> Bool Source #
makeInstance :: LensHiding a => a -> a Source #
makeInstance' :: LensHiding a => Overlappable -> a -> a Source #
mapHidingArgInfo :: LensArgInfo a => LensMap a Hiding Source #
mapOriginArgInfo :: LensArgInfo a => LensMap a Origin Source #
mapUsing :: ([ImportedName' n1 m1] -> [ImportedName' n2 m2]) -> Using' n1 m1 -> Using' n2 m2 Source #
namedSame :: (LensNamed a, LensNamed b, NameOf a ~ NamedName, NameOf b ~ NamedName) => a -> b -> Bool Source #
noPlaceholder :: e -> MaybePlaceholder e Source #
An abbreviation: noPlaceholder = .NoPlaceholder
Nothing
notVisible :: LensHiding a => a -> Bool Source #
oneFreeVariable :: Int -> FreeVariables Source #
partitionImportedNames :: [ImportedName' n m] -> ([n], [m]) Source #
Like partitionEithers.
prettyHiding :: LensHiding a => a -> (Doc -> Doc) -> Doc -> Doc Source #
prettyHiding info visible doc puts the correct braces
around doc according to info info and returns
visible doc if the we deal with a visible thing.
rawNameToString :: RawName -> ShortText Source #
sameHiding :: (LensHiding a, LensHiding b) => a -> b -> Bool Source #
Ignores Overlappable.
setHidingArgInfo :: LensArgInfo a => LensSet a Hiding Source #
setImportedName :: ImportedName' a a -> a -> ImportedName' a a Source #
setNamedArg :: NamedArg a -> b -> NamedArg b Source #
setNamedArg a b = updateNamedArg (const b) a
setOriginArgInfo :: LensArgInfo a => LensSet a Origin Source #
stringToArgName :: ShortText -> ArgName Source #
stringToRawName :: ShortText -> RawName Source #
unArgKeepHiding :: Arg a -> WithHiding a Source #
unnamedArg :: ArgInfo -> a -> NamedArg a Source #
updateNamedArg :: (a -> b) -> NamedArg a -> NamedArg b Source #
The functor instance for NamedArg would be ambiguous,
so we give it another name here.
updateNamedArgA :: Applicative f => (a -> f b) -> NamedArg a -> f (NamedArg b) Source #
withArgsFrom :: [a] -> [Arg b] -> [Arg a] Source #
withNamedArgsFrom :: [a] -> [NamedArg b] -> [NamedArg a] Source #
Access modifier.
Constructors
| PrivateAccess KwRange Origin | Store the |
| PublicAccess |
class AllAreOpaque a where Source #
Minimal complete definition
Nothing
Methods
jointOpacity :: a -> JointOpacity Source #
default jointOpacity :: forall (t :: Type -> Type) b. (Foldable t, AllAreOpaque b, t b ~ a) => a -> JointOpacity Source #
Instances
| AllAreOpaque IsOpaque Source # | |
Defined in Mikan.Syntax.Common Methods jointOpacity :: IsOpaque -> JointOpacity Source # | |
| AllAreOpaque (DefInfo' t) Source # | |
Defined in Mikan.Syntax.Info Methods jointOpacity :: DefInfo' t -> JointOpacity Source # | |
| AllAreOpaque a => AllAreOpaque (Maybe a) Source # | |
Defined in Mikan.Syntax.Common Methods jointOpacity :: Maybe a -> JointOpacity Source # | |
| AllAreOpaque a => AllAreOpaque [a] Source # | |
Defined in Mikan.Syntax.Common Methods jointOpacity :: [a] -> JointOpacity Source # | |
class AnyIsAbstract a where Source #
Is any element of a collection an AbstractDef.
Minimal complete definition
Nothing
Methods
anyIsAbstract :: a -> IsAbstract Source #
default anyIsAbstract :: forall (t :: Type -> Type) b. (Foldable t, AnyIsAbstract b, t b ~ a) => a -> IsAbstract Source #
Instances
| AnyIsAbstract IsAbstract Source # | |
Defined in Mikan.Syntax.Common Methods anyIsAbstract :: IsAbstract -> IsAbstract Source # | |
| AnyIsAbstract (DefInfo' t) Source # | |
Defined in Mikan.Syntax.Info Methods anyIsAbstract :: DefInfo' t -> IsAbstract Source # | |
| AnyIsAbstract a => AnyIsAbstract (Maybe a) Source # | |
Defined in Mikan.Syntax.Common Methods anyIsAbstract :: Maybe a -> IsAbstract Source # | |
| AnyIsAbstract a => AnyIsAbstract [a] Source # | |
Defined in Mikan.Syntax.Common Methods anyIsAbstract :: [a] -> IsAbstract Source # | |
Instances
A function argument can be hidden.
Constructors
| ArgInfo | |
Fields | |
Instances
| LensArgInfo ArgInfo Source # | |
Defined in Mikan.Syntax.Common | |
| LensFreeVariables ArgInfo Source # | |
Defined in Mikan.Syntax.Common Methods getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source # | |
| LensHiding ArgInfo Source # | |
| LensOrigin ArgInfo Source # | |
| HasRange ArgInfo Source # | |
| KillRange ArgInfo Source # | |
Defined in Mikan.Syntax.Common Methods | |
| EqualSy ArgInfo Source # | Ignore origin and free variables. |
| ToTerm ArgInfo Source # | |
| ChooseFlex ArgInfo Source # | |
Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: ArgInfo -> ArgInfo -> FlexChoice Source # | |
| EmbPrj ArgInfo Source # | |
| SynEq ArgInfo Source # | |
Defined in Mikan.TypeChecking.SyntacticEquality | |
| Unquote ArgInfo Source # | |
| Null ArgInfo Source # | |
| NFData ArgInfo Source # | |
Defined in Mikan.Syntax.Common | |
| Show ArgInfo Source # | |
| Eq ArgInfo Source # | |
| Ord ArgInfo Source # | |
data Associativity Source #
Associativity.
Constructors
| NonAssoc | |
| LeftAssoc | |
| RightAssoc |
Instances
| Pretty Associativity Source # | |
Defined in Mikan.Syntax.Common Methods pretty :: Associativity -> Doc Source # prettyPrec :: Int -> Associativity -> Doc Source # prettyList :: [Associativity] -> Doc Source # | |
| ToTerm Associativity Source # | |
Defined in Mikan.TypeChecking.Primitive | |
| EmbPrj Associativity Source # | |
| Show Associativity Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> Associativity -> ShowS # show :: Associativity -> String # showList :: [Associativity] -> ShowS # | |
| Eq Associativity Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: Associativity -> Associativity -> Bool # (/=) :: Associativity -> Associativity -> Bool # | |
| Ord Associativity Source # | |
Defined in Mikan.Syntax.Common Methods compare :: Associativity -> Associativity -> Ordering # (<) :: Associativity -> Associativity -> Bool # (<=) :: Associativity -> Associativity -> Bool # (>) :: Associativity -> Associativity -> Bool # (>=) :: Associativity -> Associativity -> Bool # max :: Associativity -> Associativity -> Associativity # min :: Associativity -> Associativity -> Associativity # | |
type BackendName = ShortText Source #
data BinderNameOrigin Source #
Constructors
| UserBinderName | |
| InsertedBinderName |
Instances
| KillRange BinderNameOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| NFData BinderNameOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: BinderNameOrigin -> () # | |||||
| Generic BinderNameOrigin Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
Methods from :: BinderNameOrigin -> Rep BinderNameOrigin x # to :: Rep BinderNameOrigin x -> BinderNameOrigin # | |||||
| Show BinderNameOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> BinderNameOrigin -> ShowS # show :: BinderNameOrigin -> String # showList :: [BinderNameOrigin] -> ShowS # | |||||
| Eq BinderNameOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: BinderNameOrigin -> BinderNameOrigin -> Bool # (/=) :: BinderNameOrigin -> BinderNameOrigin -> Bool # | |||||
| type Rep BinderNameOrigin Source # | |||||
Defined in Mikan.Syntax.Common | |||||
data BoundVariablePosition Source #
Positions of variables in syntax declarations.
Constructors
| BoundVariablePosition | |
Fields
| |
Instances
| EmbPrj BoundVariablePosition Source # | |
| NFData BoundVariablePosition Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: BoundVariablePosition -> () # | |
| Show BoundVariablePosition Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> BoundVariablePosition -> ShowS # show :: BoundVariablePosition -> String # showList :: [BoundVariablePosition] -> ShowS # | |
| Eq BoundVariablePosition Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: BoundVariablePosition -> BoundVariablePosition -> Bool # (/=) :: BoundVariablePosition -> BoundVariablePosition -> Bool # | |
| Ord BoundVariablePosition Source # | |
Defined in Mikan.Syntax.Common Methods compare :: BoundVariablePosition -> BoundVariablePosition -> Ordering # (<) :: BoundVariablePosition -> BoundVariablePosition -> Bool # (<=) :: BoundVariablePosition -> BoundVariablePosition -> Bool # (>) :: BoundVariablePosition -> BoundVariablePosition -> Bool # (>=) :: BoundVariablePosition -> BoundVariablePosition -> Bool # max :: BoundVariablePosition -> BoundVariablePosition -> BoundVariablePosition # min :: BoundVariablePosition -> BoundVariablePosition -> BoundVariablePosition # | |
Constructors
| YesCatchall Range | |
| NoCatchall |
Instances
| KillRange Catchall Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| EmbPrj Catchall Source # | |||||
| Null Catchall Source # | |||||
| NFData Catchall Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Monoid Catchall Source # | |||||
| Semigroup Catchall Source # | Composition is left-biased, taking the left | ||||
| Generic Catchall Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show Catchall Source # | |||||
| Eq Catchall Source # | |||||
| type Rep Catchall Source # | |||||
Defined in Mikan.Syntax.Common type Rep Catchall = D1 ('MetaData "Catchall" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "YesCatchall" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Range)) :+: C1 ('MetaCons "NoCatchall" 'PrefixI 'False) (U1 :: Type -> Type)) | |||||
Where does the ConP or Con come from?
Constructors
| ConOSystem | Inserted by system or expanded from an implicit pattern. |
| ConOCon | User wrote a constructor (pattern). |
| ConORec | User wrote a record (pattern). |
| ConOSplit | Generated by interactive case splitting. |
| ConORecWhere | User wrote a |
Instances
| KillRange ConOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| EmbPrj ConOrigin Source # | |||||
| NFData ConOrigin Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Bounded ConOrigin Source # | |||||
| Enum ConOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods succ :: ConOrigin -> ConOrigin # pred :: ConOrigin -> ConOrigin # fromEnum :: ConOrigin -> Int # enumFrom :: ConOrigin -> [ConOrigin] # enumFromThen :: ConOrigin -> ConOrigin -> [ConOrigin] # enumFromTo :: ConOrigin -> ConOrigin -> [ConOrigin] # enumFromThenTo :: ConOrigin -> ConOrigin -> ConOrigin -> [ConOrigin] # | |||||
| Generic ConOrigin Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show ConOrigin Source # | |||||
| Eq ConOrigin Source # | |||||
| Ord ConOrigin Source # | |||||
| type Rep ConOrigin Source # | |||||
Defined in Mikan.Syntax.Common type Rep ConOrigin = D1 ('MetaData "ConOrigin" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((C1 ('MetaCons "ConOSystem" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConOCon" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "ConORec" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ConOSplit" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ConORecWhere" 'PrefixI 'False) (U1 :: Type -> Type)))) | |||||
Constructors
| Constr a |
Instances
| ToConcrete (Constr Constructor) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => Constr Constructor -> m (ConOfAbs (Constr Constructor)) Source # bindToConcrete :: MonadToConcrete m => Constr Constructor -> (ConOfAbs (Constr Constructor) -> m b) -> m b Source # | |||||
| type ConOfAbs (Constr Constructor) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
data ConstructorOrPatternSynonym Source #
Distinguish constructors from pattern synonyms.
Constructors
| IsConstructor | |
| IsPatternSynonym |
Instances
| Pretty ConstructorOrPatternSynonym Source # | |||||
Defined in Mikan.Syntax.Common Methods pretty :: ConstructorOrPatternSynonym -> Doc Source # prettyPrec :: Int -> ConstructorOrPatternSynonym -> Doc Source # prettyList :: [ConstructorOrPatternSynonym] -> Doc Source # | |||||
| EmbPrj ConstructorOrPatternSynonym Source # | |||||
| NFData ConstructorOrPatternSynonym Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: ConstructorOrPatternSynonym -> () # | |||||
| Bounded ConstructorOrPatternSynonym Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum ConstructorOrPatternSynonym Source # | |||||
Defined in Mikan.Syntax.Common Methods succ :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym # pred :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym # toEnum :: Int -> ConstructorOrPatternSynonym # fromEnum :: ConstructorOrPatternSynonym -> Int # enumFrom :: ConstructorOrPatternSynonym -> [ConstructorOrPatternSynonym] # enumFromThen :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym -> [ConstructorOrPatternSynonym] # enumFromTo :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym -> [ConstructorOrPatternSynonym] # enumFromThenTo :: ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym -> ConstructorOrPatternSynonym -> [ConstructorOrPatternSynonym] # | |||||
| Generic ConstructorOrPatternSynonym Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
Methods from :: ConstructorOrPatternSynonym -> Rep ConstructorOrPatternSynonym x # to :: Rep ConstructorOrPatternSynonym x -> ConstructorOrPatternSynonym # | |||||
| Show ConstructorOrPatternSynonym Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> ConstructorOrPatternSynonym -> ShowS # show :: ConstructorOrPatternSynonym -> String # showList :: [ConstructorOrPatternSynonym] -> ShowS # | |||||
| type Rep ConstructorOrPatternSynonym Source # | |||||
Defined in Mikan.Syntax.Common | |||||
class CopatternMatchingAllowed a where Source #
Can we construct a record by copattern matching?
Methods
copatternMatchingAllowed :: a -> Bool Source #
Instances
| CopatternMatchingAllowed ConHead Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| CopatternMatchingAllowed DataOrRecord Source # | |
Defined in Mikan.Syntax.Common Methods | |
| CopatternMatchingAllowed HasEta Source # | |
Defined in Mikan.Syntax.Common Methods | |
| CopatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods copatternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| CopatternMatchingAllowed EtaEquality Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
data CoverageCheck Source #
Coverage check? (Default is yes).
Constructors
| YesCoverageCheck | |
| NoCoverageCheck |
Instances
| KillRange CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| NFData CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: CoverageCheck -> () # | |||||
| Monoid CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods mempty :: CoverageCheck # mappend :: CoverageCheck -> CoverageCheck -> CoverageCheck # mconcat :: [CoverageCheck] -> CoverageCheck # | |||||
| Semigroup CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods (<>) :: CoverageCheck -> CoverageCheck -> CoverageCheck # sconcat :: NonEmpty CoverageCheck -> CoverageCheck # stimes :: Integral b => b -> CoverageCheck -> CoverageCheck # | |||||
| Bounded CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods succ :: CoverageCheck -> CoverageCheck # pred :: CoverageCheck -> CoverageCheck # toEnum :: Int -> CoverageCheck # fromEnum :: CoverageCheck -> Int # enumFrom :: CoverageCheck -> [CoverageCheck] # enumFromThen :: CoverageCheck -> CoverageCheck -> [CoverageCheck] # enumFromTo :: CoverageCheck -> CoverageCheck -> [CoverageCheck] # enumFromThenTo :: CoverageCheck -> CoverageCheck -> CoverageCheck -> [CoverageCheck] # | |||||
| Generic CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> CoverageCheck -> ShowS # show :: CoverageCheck -> String # showList :: [CoverageCheck] -> ShowS # | |||||
| Eq CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: CoverageCheck -> CoverageCheck -> Bool # (/=) :: CoverageCheck -> CoverageCheck -> Bool # | |||||
| Ord CoverageCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods compare :: CoverageCheck -> CoverageCheck -> Ordering # (<) :: CoverageCheck -> CoverageCheck -> Bool # (<=) :: CoverageCheck -> CoverageCheck -> Bool # (>) :: CoverageCheck -> CoverageCheck -> Bool # (>=) :: CoverageCheck -> CoverageCheck -> Bool # max :: CoverageCheck -> CoverageCheck -> CoverageCheck # min :: CoverageCheck -> CoverageCheck -> CoverageCheck # | |||||
| type Rep CoverageCheck Source # | |||||
data DataOrRecord' p Source #
Instances
| CopatternMatchingAllowed DataOrRecord Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| PatternMatchingAllowed DataOrRecord Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| KillRange DataOrRecord Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| PrettyTCM DataOrRecord_ Source # | |||||
Defined in Mikan.TypeChecking.Pretty.Warning Methods prettyTCM :: MonadPretty m => DataOrRecord_ -> m Doc Source # | |||||
| Boolean DataOrRecord_ Source # | |||||
Defined in Mikan.Syntax.Common Methods fromBool :: Bool -> DataOrRecord_ Source # true :: DataOrRecord_ Source # false :: DataOrRecord_ Source # not :: DataOrRecord_ -> DataOrRecord_ Source # (&&) :: DataOrRecord_ -> DataOrRecord_ -> DataOrRecord_ Source # (||) :: DataOrRecord_ -> DataOrRecord_ -> DataOrRecord_ Source # implies :: DataOrRecord_ -> DataOrRecord_ -> DataOrRecord_ Source # butNot :: DataOrRecord_ -> DataOrRecord_ -> DataOrRecord_ Source # | |||||
| IsBool DataOrRecord_ Source # | |||||
Defined in Mikan.Syntax.Common Methods toBool :: DataOrRecord_ -> Bool Source # ifThenElse :: DataOrRecord_ -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> DataOrRecord_ -> DataOrRecord_ Source # fromBool2 :: (Bool -> Bool -> Bool) -> DataOrRecord_ -> DataOrRecord_ -> DataOrRecord_ Source # | |||||
| EmbPrj a => EmbPrj (DataOrRecord' a) Source # | |||||
| NFData a => NFData (DataOrRecord' a) Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: DataOrRecord' a -> () # | |||||
| Generic (DataOrRecord' p) Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
Methods from :: DataOrRecord' p -> Rep (DataOrRecord' p) x # to :: Rep (DataOrRecord' p) x -> DataOrRecord' p # | |||||
| Show p => Show (DataOrRecord' p) Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> DataOrRecord' p -> ShowS # show :: DataOrRecord' p -> String # showList :: [DataOrRecord' p] -> ShowS # | |||||
| Eq p => Eq (DataOrRecord' p) Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: DataOrRecord' p -> DataOrRecord' p -> Bool # (/=) :: DataOrRecord' p -> DataOrRecord' p -> Bool # | |||||
| type Rep (DataOrRecord' p) Source # | |||||
Defined in Mikan.Syntax.Common type Rep (DataOrRecord' p) = D1 ('MetaData "DataOrRecord'" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "IsData" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "IsRecord" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 p))) | |||||
type DataOrRecord_ = DataOrRecord' () Source #
data DisplayLHS Source #
Distinguish parsing a DISPLAY pragma from an ordinary left hand side.
Constructors
| YesDisplayLHS | |
| NoDisplayLHS |
Instances
| Boolean DisplayLHS Source # | |||||
Defined in Mikan.Syntax.Common Methods fromBool :: Bool -> DisplayLHS Source # true :: DisplayLHS Source # false :: DisplayLHS Source # not :: DisplayLHS -> DisplayLHS Source # (&&) :: DisplayLHS -> DisplayLHS -> DisplayLHS Source # (||) :: DisplayLHS -> DisplayLHS -> DisplayLHS Source # implies :: DisplayLHS -> DisplayLHS -> DisplayLHS Source # butNot :: DisplayLHS -> DisplayLHS -> DisplayLHS Source # | |||||
| IsBool DisplayLHS Source # | |||||
Defined in Mikan.Syntax.Common Methods toBool :: DisplayLHS -> Bool Source # ifThenElse :: DisplayLHS -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> DisplayLHS -> DisplayLHS Source # fromBool2 :: (Bool -> Bool -> Bool) -> DisplayLHS -> DisplayLHS -> DisplayLHS Source # | |||||
| Bounded DisplayLHS Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum DisplayLHS Source # | |||||
Defined in Mikan.Syntax.Common Methods succ :: DisplayLHS -> DisplayLHS # pred :: DisplayLHS -> DisplayLHS # toEnum :: Int -> DisplayLHS # fromEnum :: DisplayLHS -> Int # enumFrom :: DisplayLHS -> [DisplayLHS] # enumFromThen :: DisplayLHS -> DisplayLHS -> [DisplayLHS] # enumFromTo :: DisplayLHS -> DisplayLHS -> [DisplayLHS] # enumFromThenTo :: DisplayLHS -> DisplayLHS -> DisplayLHS -> [DisplayLHS] # | |||||
| Generic DisplayLHS Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show DisplayLHS Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> DisplayLHS -> ShowS # show :: DisplayLHS -> String # showList :: [DisplayLHS] -> ShowS # | |||||
| Eq DisplayLHS Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| type Rep DisplayLHS Source # | |||||
data ExpandedEllipsis Source #
Constructors
| ExpandedEllipsis | |
Fields | |
| NoEllipsis | |
Instances
| KillRange ExpandedEllipsis Source # | |
Defined in Mikan.Syntax.Common Methods | |
| EmbPrj ExpandedEllipsis Source # | |
| Null ExpandedEllipsis Source # | |
Defined in Mikan.Syntax.Common | |
| NFData ExpandedEllipsis Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: ExpandedEllipsis -> () # | |
| Monoid ExpandedEllipsis Source # | |
Defined in Mikan.Syntax.Common Methods mappend :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis # mconcat :: [ExpandedEllipsis] -> ExpandedEllipsis # | |
| Semigroup ExpandedEllipsis Source # | |
Defined in Mikan.Syntax.Common Methods (<>) :: ExpandedEllipsis -> ExpandedEllipsis -> ExpandedEllipsis # sconcat :: NonEmpty ExpandedEllipsis -> ExpandedEllipsis # stimes :: Integral b => b -> ExpandedEllipsis -> ExpandedEllipsis # | |
| Show ExpandedEllipsis Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> ExpandedEllipsis -> ShowS # show :: ExpandedEllipsis -> String # showList :: [ExpandedEllipsis] -> ShowS # | |
| Eq ExpandedEllipsis Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool # (/=) :: ExpandedEllipsis -> ExpandedEllipsis -> Bool # | |
Instances
| Pretty FileType Source # | |||||
| EmbPrj FileType Source # | |||||
| NFData FileType Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Generic FileType Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show FileType Source # | |||||
| Eq FileType Source # | |||||
| Ord FileType Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| type Rep FileType Source # | |||||
Defined in Mikan.Syntax.Common type Rep FileType = D1 ('MetaData "FileType" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((C1 ('MetaCons "AgdaFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "MdFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "RstFileType" 'PrefixI 'False) (U1 :: Type -> Type))) :+: ((C1 ('MetaCons "TexFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "OrgFileType" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "TypstFileType" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "TreeFileType" 'PrefixI 'False) (U1 :: Type -> Type)))) | |||||
Fixity of operators.
Constructors
| Fixity | |
Fields
| |
Instances
| LensFixity Fixity Source # | |
Defined in Mikan.Syntax.Common | |
| Pretty Fixity Source # | |
| HasRange Fixity Source # | |
| KillRange Fixity Source # | |
Defined in Mikan.Syntax.Common Methods | |
| ToTerm Fixity Source # | |
| EmbPrj Fixity Source # | |
| Null Fixity Source # | |
| NFData Fixity Source # | |
Defined in Mikan.Syntax.Common | |
| Show Fixity Source # | |
| Eq Fixity Source # | |
| Ord Fixity Source # | |
The notation is handled as the fixity in the renamer. Hence, they are grouped together in this type.
Constructors
| Fixity' | |
Fields
| |
Instances
| LensFixity Fixity' Source # | |
Defined in Mikan.Syntax.Common | |
| LensFixity' Fixity' Source # | |
Defined in Mikan.Syntax.Common | |
| Pretty Fixity' Source # | |
| HasRange Fixity' Source # | |
| KillRange Fixity' Source # | |
Defined in Mikan.Syntax.Common Methods | |
| PrimTerm Fixity' Source # | |
| PrimType Fixity' Source # | |
| ToTerm Fixity' Source # | |
| EmbPrj Fixity' Source # | |
| Null Fixity' Source # | |
| NFData Fixity' Source # | |
Defined in Mikan.Syntax.Common | |
| Show Fixity' Source # | |
| Eq Fixity' Source # | |
data FixityLevel Source #
Constructors
| Unrelated | No fixity declared. |
| Related !PrecedenceLevel | Fixity level declared as the number. |
Instances
| Pretty FixityLevel Source # | |
Defined in Mikan.Syntax.Common Methods pretty :: FixityLevel -> Doc Source # prettyPrec :: Int -> FixityLevel -> Doc Source # prettyList :: [FixityLevel] -> Doc Source # | |
| ToTerm FixityLevel Source # | |
Defined in Mikan.TypeChecking.Primitive | |
| EmbPrj FixityLevel Source # | |
| Null FixityLevel Source # | |
Defined in Mikan.Syntax.Common | |
| NFData FixityLevel Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: FixityLevel -> () # | |
| Show FixityLevel Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> FixityLevel -> ShowS # show :: FixityLevel -> String # showList :: [FixityLevel] -> ShowS # | |
| Eq FixityLevel Source # | |
Defined in Mikan.Syntax.Common | |
| Ord FixityLevel Source # | |
Defined in Mikan.Syntax.Common Methods compare :: FixityLevel -> FixityLevel -> Ordering # (<) :: FixityLevel -> FixityLevel -> Bool # (<=) :: FixityLevel -> FixityLevel -> Bool # (>) :: FixityLevel -> FixityLevel -> Bool # (>=) :: FixityLevel -> FixityLevel -> Bool # max :: FixityLevel -> FixityLevel -> FixityLevel # min :: FixityLevel -> FixityLevel -> FixityLevel # | |
data FreeVariables Source #
Constructors
| UnknownFVs | |
| KnownFVs !VarSet |
Instances
| LensFreeVariables FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods getFreeVariables :: FreeVariables -> FreeVariables Source # setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables Source # | |
| KillRange FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods | |
| EmbPrj FreeVariables Source # | |
| NFData FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: FreeVariables -> () # | |
| Monoid FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods mempty :: FreeVariables # mappend :: FreeVariables -> FreeVariables -> FreeVariables # mconcat :: [FreeVariables] -> FreeVariables # | |
| Semigroup FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods (<>) :: FreeVariables -> FreeVariables -> FreeVariables # sconcat :: NonEmpty FreeVariables -> FreeVariables # stimes :: Integral b => b -> FreeVariables -> FreeVariables # | |
| Show FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> FreeVariables -> ShowS # show :: FreeVariables -> String # showList :: [FreeVariables] -> ShowS # | |
| Eq FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: FreeVariables -> FreeVariables -> Bool # (/=) :: FreeVariables -> FreeVariables -> Bool # | |
| Ord FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods compare :: FreeVariables -> FreeVariables -> Ordering # (<) :: FreeVariables -> FreeVariables -> Bool # (<=) :: FreeVariables -> FreeVariables -> Bool # (>) :: FreeVariables -> FreeVariables -> Bool # (>=) :: FreeVariables -> FreeVariables -> Bool # max :: FreeVariables -> FreeVariables -> FreeVariables # min :: FreeVariables -> FreeVariables -> FreeVariables # | |
type HasEta = HasEta' PatternOrCopattern Source #
Pattern and copattern matching is allowed in the presence of eta.
In the absence of eta, we have to choose whether we want to allow matching on the constructor or copattern matching with the projections. Having both leads to breakage of subject reduction (issue #4560).
Does a record come with eta-equality?
Instances
| CopatternMatchingAllowed HasEta Source # | |
Defined in Mikan.Syntax.Common Methods | |
| PatternMatchingAllowed HasEta Source # | |
Defined in Mikan.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
| Functor HasEta' Source # | |
| Foldable HasEta' Source # | |
Defined in Mikan.Syntax.Common Methods fold :: Monoid m => HasEta' m -> m # foldMap :: Monoid m => (a -> m) -> HasEta' a -> m # foldMap' :: Monoid m => (a -> m) -> HasEta' a -> m # foldr :: (a -> b -> b) -> b -> HasEta' a -> b # foldr' :: (a -> b -> b) -> b -> HasEta' a -> b # foldl :: (b -> a -> b) -> b -> HasEta' a -> b # foldl' :: (b -> a -> b) -> b -> HasEta' a -> b # foldr1 :: (a -> a -> a) -> HasEta' a -> a # foldl1 :: (a -> a -> a) -> HasEta' a -> a # elem :: Eq a => a -> HasEta' a -> Bool # maximum :: Ord a => HasEta' a -> a # minimum :: Ord a => HasEta' a -> a # | |
| Traversable HasEta' Source # | |
| HasRange a => HasRange (HasEta' a) Source # | |
| KillRange a => KillRange (HasEta' a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (HasEta' a) Source # | |
| EmbPrj a => EmbPrj (HasEta' a) Source # | |
| NFData a => NFData (HasEta' a) Source # | |
Defined in Mikan.Syntax.Common | |
| Show a => Show (HasEta' a) Source # | |
| Eq a => Eq (HasEta' a) Source # | |
| Ord a => Ord (HasEta' a) Source # | |
class HasOverlapMode a where Source #
Methods
Instances
| HasOverlapMode OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods | |
| HasOverlapMode Candidate Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
Constructors
| Hidden | |
| Instance Overlappable | |
| NotHidden |
Instances
| LensHiding Hiding Source # | |||||
| Pretty Hiding Source # | |||||
| HasRange Hiding Source # | |||||
| KillRange Hiding Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| Verbalize Hiding Source # | |||||
| ChooseFlex Hiding Source # | |||||
Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Hiding -> Hiding -> FlexChoice Source # | |||||
| EmbPrj Hiding Source # | |||||
| Unquote Hiding Source # | |||||
| Null Hiding Source # | |||||
| NFData Hiding Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Monoid Hiding Source # | |||||
| Semigroup Hiding Source # |
| ||||
| Bounded Hiding Source # | |||||
| Enum Hiding Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Generic Hiding Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show Hiding Source # | |||||
| Eq Hiding Source # | |||||
| Ord Hiding Source # | |||||
| type Rep Hiding Source # | |||||
Defined in Mikan.Syntax.Common type Rep Hiding = D1 ('MetaData "Hiding" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "Hidden" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "Instance" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 Overlappable)) :+: C1 ('MetaCons "NotHidden" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
type HidingDirective' n m = [ImportedName' n m] Source #
data ImportDirective' n m Source #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import, namespace, or open declarations).
Constructors
| ImportDirective | |
Fields
| |
Instances
| (Pretty a, Pretty b) => Pretty (ImportDirective' a b) Source # | |
Defined in Mikan.Syntax.Common Methods pretty :: ImportDirective' a b -> Doc Source # prettyPrec :: Int -> ImportDirective' a b -> Doc Source # prettyList :: [ImportDirective' a b] -> Doc Source # | |
| HasRange (ImportDirective' a b) Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: ImportDirective' a b -> Range Source # | |
| (KillRange a, KillRange b) => KillRange (ImportDirective' a b) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (ImportDirective' a b) Source # | |
| Null (ImportDirective' n m) Source # |
|
Defined in Mikan.Syntax.Common | |
| (NFData a, NFData b) => NFData (ImportDirective' a b) Source # | Ranges are not forced. |
Defined in Mikan.Syntax.Common Methods rnf :: ImportDirective' a b -> () # | |
| Monoid (ImportDirective' n m) Source # | |
Defined in Mikan.Syntax.Common Methods mempty :: ImportDirective' n m # mappend :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m # mconcat :: [ImportDirective' n m] -> ImportDirective' n m # | |
| Semigroup (ImportDirective' n m) Source # | |
Defined in Mikan.Syntax.Common Methods (<>) :: ImportDirective' n m -> ImportDirective' n m -> ImportDirective' n m # sconcat :: NonEmpty (ImportDirective' n m) -> ImportDirective' n m # stimes :: Integral b => b -> ImportDirective' n m -> ImportDirective' n m # | |
| (Show m, Show n) => Show (ImportDirective' n m) Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> ImportDirective' n m -> ShowS # show :: ImportDirective' n m -> String # showList :: [ImportDirective' n m] -> ShowS # | |
| (Eq m, Eq n) => Eq (ImportDirective' n m) Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: ImportDirective' n m -> ImportDirective' n m -> Bool # (/=) :: ImportDirective' n m -> ImportDirective' n m -> Bool # | |
data ImportedName' n m Source #
An imported name can be a module or a defined name.
Constructors
| ImportedModule m | Imported module name of type |
| ImportedName n | Imported name of type |
Instances
| PrettyTCM ImportedName Source # | |
Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => ImportedName -> m Doc Source # | |
| (Pretty a, Pretty b) => Pretty (ImportedName' a b) Source # | |
Defined in Mikan.Syntax.Common Methods pretty :: ImportedName' a b -> Doc Source # prettyPrec :: Int -> ImportedName' a b -> Doc Source # prettyList :: [ImportedName' a b] -> Doc Source # | |
| (HasRange a, HasRange b) => HasRange (ImportedName' a b) Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: ImportedName' a b -> Range Source # | |
| (KillRange a, KillRange b) => KillRange (ImportedName' a b) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (ImportedName' a b) Source # | |
| (EmbPrj a, EmbPrj b) => EmbPrj (ImportedName' a b) Source # | |
| (NFData a, NFData b) => NFData (ImportedName' a b) Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: ImportedName' a b -> () # | |
| (Show m, Show n) => Show (ImportedName' n m) Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> ImportedName' n m -> ShowS # show :: ImportedName' n m -> String # showList :: [ImportedName' n m] -> ShowS # | |
| (Eq m, Eq n) => Eq (ImportedName' n m) Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: ImportedName' n m -> ImportedName' n m -> Bool # (/=) :: ImportedName' n m -> ImportedName' n m -> Bool # | |
| (Ord m, Ord n) => Ord (ImportedName' n m) Source # | |
Defined in Mikan.Syntax.Common Methods compare :: ImportedName' n m -> ImportedName' n m -> Ordering # (<) :: ImportedName' n m -> ImportedName' n m -> Bool # (<=) :: ImportedName' n m -> ImportedName' n m -> Bool # (>) :: ImportedName' n m -> ImportedName' n m -> Bool # (>=) :: ImportedName' n m -> ImportedName' n m -> Bool # max :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m # min :: ImportedName' n m -> ImportedName' n m -> ImportedName' n m # | |
newtype InteractionId Source #
Constructors
| InteractionId | |
Fields
| |
Instances
| EncodeTCM InteractionId Source # | |||||
Defined in Mikan.Interaction.JSONTop | |||||
| Pretty InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods pretty :: InteractionId -> Doc Source # prettyPrec :: Int -> InteractionId -> Doc Source # prettyList :: [InteractionId] -> Doc Source # | |||||
| KillRange InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| ToConcrete InteractionId Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => InteractionId -> m (ConOfAbs InteractionId) Source # bindToConcrete :: MonadToConcrete m => InteractionId -> (ConOfAbs InteractionId -> m b) -> m b Source # | |||||
| HasFresh InteractionId Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base | |||||
| PrettyTCM InteractionId Source # | |||||
Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => InteractionId -> m Doc Source # | |||||
| ToJSON InteractionId Source # | |||||
Defined in Mikan.Interaction.JSONTop Methods toJSON :: InteractionId -> Value # toEncoding :: InteractionId -> Encoding # toJSONList :: [InteractionId] -> Value # toEncodingList :: [InteractionId] -> Encoding # omitField :: InteractionId -> Bool # | |||||
| NFData InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: InteractionId -> () # | |||||
| NFData InteractionPoints Source # | |||||
Defined in Mikan.TypeChecking.Monad.Base Methods rnf :: InteractionPoints -> () # | |||||
| Enum InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods succ :: InteractionId -> InteractionId # pred :: InteractionId -> InteractionId # toEnum :: Int -> InteractionId # fromEnum :: InteractionId -> Int # enumFrom :: InteractionId -> [InteractionId] # enumFromThen :: InteractionId -> InteractionId -> [InteractionId] # enumFromTo :: InteractionId -> InteractionId -> [InteractionId] # enumFromThenTo :: InteractionId -> InteractionId -> InteractionId -> [InteractionId] # | |||||
| Num InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods (+) :: InteractionId -> InteractionId -> InteractionId # (-) :: InteractionId -> InteractionId -> InteractionId # (*) :: InteractionId -> InteractionId -> InteractionId # negate :: InteractionId -> InteractionId # abs :: InteractionId -> InteractionId # signum :: InteractionId -> InteractionId # fromInteger :: Integer -> InteractionId # | |||||
| Read InteractionId Source # | |||||
Defined in Mikan.Interaction.Base Methods readsPrec :: Int -> ReadS InteractionId # readList :: ReadS [InteractionId] # | |||||
| Integral InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods quot :: InteractionId -> InteractionId -> InteractionId # rem :: InteractionId -> InteractionId -> InteractionId # div :: InteractionId -> InteractionId -> InteractionId # mod :: InteractionId -> InteractionId -> InteractionId # quotRem :: InteractionId -> InteractionId -> (InteractionId, InteractionId) # divMod :: InteractionId -> InteractionId -> (InteractionId, InteractionId) # toInteger :: InteractionId -> Integer # | |||||
| Real InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods toRational :: InteractionId -> Rational # | |||||
| Show InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> InteractionId -> ShowS # show :: InteractionId -> String # showList :: [InteractionId] -> ShowS # | |||||
| Eq InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: InteractionId -> InteractionId -> Bool # (/=) :: InteractionId -> InteractionId -> Bool # | |||||
| Ord InteractionId Source # | |||||
Defined in Mikan.Syntax.Common Methods compare :: InteractionId -> InteractionId -> Ordering # (<) :: InteractionId -> InteractionId -> Bool # (<=) :: InteractionId -> InteractionId -> Bool # (>) :: InteractionId -> InteractionId -> Bool # (>=) :: InteractionId -> InteractionId -> Bool # max :: InteractionId -> InteractionId -> InteractionId # min :: InteractionId -> InteractionId -> InteractionId # | |||||
| type ConOfAbs InteractionId Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
data IsAbstract Source #
Abstract or concrete.
Constructors
| AbstractDef | |
| ConcreteDef |
Instances
| AnyIsAbstract IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Methods anyIsAbstract :: IsAbstract -> IsAbstract Source # | |||||
| LensIsAbstract IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| KillRange IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| EmbPrj IsAbstract Source # | |||||
| Boolean IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Methods fromBool :: Bool -> IsAbstract Source # true :: IsAbstract Source # false :: IsAbstract Source # not :: IsAbstract -> IsAbstract Source # (&&) :: IsAbstract -> IsAbstract -> IsAbstract Source # (||) :: IsAbstract -> IsAbstract -> IsAbstract Source # implies :: IsAbstract -> IsAbstract -> IsAbstract Source # butNot :: IsAbstract -> IsAbstract -> IsAbstract Source # | |||||
| IsBool IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Methods toBool :: IsAbstract -> Bool Source # ifThenElse :: IsAbstract -> b -> b -> b Source # fromBool1 :: (Bool -> Bool) -> IsAbstract -> IsAbstract Source # fromBool2 :: (Bool -> Bool -> Bool) -> IsAbstract -> IsAbstract -> IsAbstract Source # | |||||
| NFData IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: IsAbstract -> () # | |||||
| Monoid IsAbstract Source # | Default is | ||||
Defined in Mikan.Syntax.Common Methods mempty :: IsAbstract # mappend :: IsAbstract -> IsAbstract -> IsAbstract # mconcat :: [IsAbstract] -> IsAbstract # | |||||
| Semigroup IsAbstract Source # | Semigroup computes if any of several is an | ||||
Defined in Mikan.Syntax.Common Methods (<>) :: IsAbstract -> IsAbstract -> IsAbstract # sconcat :: NonEmpty IsAbstract -> IsAbstract # stimes :: Integral b => b -> IsAbstract -> IsAbstract # | |||||
| Generic IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> IsAbstract -> ShowS # show :: IsAbstract -> String # showList :: [IsAbstract] -> ShowS # | |||||
| Eq IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Ord IsAbstract Source # | |||||
Defined in Mikan.Syntax.Common Methods compare :: IsAbstract -> IsAbstract -> Ordering # (<) :: IsAbstract -> IsAbstract -> Bool # (<=) :: IsAbstract -> IsAbstract -> Bool # (>) :: IsAbstract -> IsAbstract -> Bool # (>=) :: IsAbstract -> IsAbstract -> Bool # max :: IsAbstract -> IsAbstract -> IsAbstract # min :: IsAbstract -> IsAbstract -> IsAbstract # | |||||
| type Rep IsAbstract Source # | |||||
Functions can be defined in both infix and prefix style. See
LHS.
data IsInstance Source #
Is this definition eligible for instance search?
Constructors
| InstanceDef KwRange | Range of the |
| NotInstanceDef |
Instances
| IsInstanceDef IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods isInstanceDef :: IsInstance -> Maybe KwRange Source # | |
| HasRange IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: IsInstance -> Range Source # | |
| KillRange IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods | |
| EmbPrj IsInstance Source # | |
| Null IsInstance Source # | |
Defined in Mikan.Syntax.Common | |
| NFData IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: IsInstance -> () # | |
| Show IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> IsInstance -> ShowS # show :: IsInstance -> String # showList :: [IsInstance] -> ShowS # | |
| Eq IsInstance Source # | |
Defined in Mikan.Syntax.Common | |
| Ord IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods compare :: IsInstance -> IsInstance -> Ordering # (<) :: IsInstance -> IsInstance -> Bool # (<=) :: IsInstance -> IsInstance -> Bool # (>) :: IsInstance -> IsInstance -> Bool # (>=) :: IsInstance -> IsInstance -> Bool # max :: IsInstance -> IsInstance -> IsInstance # min :: IsInstance -> IsInstance -> IsInstance # | |
class IsInstanceDef a where Source #
Methods
isInstanceDef :: a -> Maybe KwRange Source #
Instances
| IsInstanceDef AbstractName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods isInstanceDef :: AbstractName -> Maybe KwRange Source # | |
| IsInstanceDef NameMetadata Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods isInstanceDef :: NameMetadata -> Maybe KwRange Source # | |
| IsInstanceDef IsInstance Source # | |
Defined in Mikan.Syntax.Common Methods isInstanceDef :: IsInstance -> Maybe KwRange Source # | |
| IsInstanceDef a => IsInstanceDef (PrettyWithBindingSite a) Source # | |
Defined in Mikan.Syntax.Scope.Base Methods isInstanceDef :: PrettyWithBindingSite a -> Maybe KwRange Source # | |
Is this a macro definition?
Constructors
| MacroDef | |
| NotMacroDef |
Instances
| HasRange IsMacro Source # | |
| KillRange IsMacro Source # | |
Defined in Mikan.Syntax.Common Methods | |
| NFData IsMacro Source # | |
Defined in Mikan.Syntax.Common | |
| Generic IsMacro Source # | |
Defined in Mikan.Syntax.Common | |
| Show IsMacro Source # | |
| Eq IsMacro Source # | |
| Ord IsMacro Source # | |
| type Rep IsMacro Source # | |
Opaque or transparent.
Constructors
| OpaqueDef !OpaqueId | This definition is opaque, and it is guarded by the given opaque block. |
| TransparentDef |
Instances
| AllAreOpaque IsOpaque Source # | |||||
Defined in Mikan.Syntax.Common Methods jointOpacity :: IsOpaque -> JointOpacity Source # | |||||
| LensIsOpaque IsOpaque Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| KillRange IsOpaque Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| EmbPrj IsOpaque Source # | |||||
| NFData IsOpaque Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Generic IsOpaque Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show IsOpaque Source # | |||||
| Eq IsOpaque Source # | |||||
| Ord IsOpaque Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| type Rep IsOpaque Source # | |||||
Defined in Mikan.Syntax.Common type Rep IsOpaque = D1 ('MetaData "IsOpaque" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "OpaqueDef" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 OpaqueId)) :+: C1 ('MetaCons "TransparentDef" 'PrefixI 'False) (U1 :: Type -> Type)) | |||||
data JointOpacity Source #
Monoid representing the combined opaque blocks of a Foldable
containing possibly-opaque declarations.
Constructors
| UniqueOpaque !OpaqueId | Every definition agrees on what opaque block they belong to. |
| DifferentOpaque !(HashSet OpaqueId) | More than one opaque block was found. |
| NoOpaque | Nothing here is opaque. |
Instances
| Monoid JointOpacity Source # | |
Defined in Mikan.Syntax.Common Methods mempty :: JointOpacity # mappend :: JointOpacity -> JointOpacity -> JointOpacity # mconcat :: [JointOpacity] -> JointOpacity # | |
| Semigroup JointOpacity Source # | |
Defined in Mikan.Syntax.Common Methods (<>) :: JointOpacity -> JointOpacity -> JointOpacity # sconcat :: NonEmpty JointOpacity -> JointOpacity # stimes :: Integral b => b -> JointOpacity -> JointOpacity # | |
class LensArgInfo a where Source #
Minimal complete definition
Methods
getArgInfo :: a -> ArgInfo Source #
setArgInfo :: ArgInfo -> a -> a Source #
mapArgInfo :: (ArgInfo -> ArgInfo) -> a -> a Source #
Instances
| LensArgInfo ArgInfo Source # | |
Defined in Mikan.Syntax.Common | |
| LensArgInfo Definition Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods getArgInfo :: Definition -> ArgInfo Source # setArgInfo :: ArgInfo -> Definition -> Definition Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> Definition -> Definition Source # | |
| LensArgInfo ContextEntry Source # | |
Defined in Mikan.TypeChecking.Monad.Base.Types Methods getArgInfo :: ContextEntry -> ArgInfo Source # setArgInfo :: ArgInfo -> ContextEntry -> ContextEntry Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> ContextEntry -> ContextEntry Source # | |
| LensArgInfo (Arg a) Source # | |
Defined in Mikan.Syntax.Common | |
| LensArgInfo (FlexibleVar a) Source # | |
Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods getArgInfo :: FlexibleVar a -> ArgInfo Source # setArgInfo :: ArgInfo -> FlexibleVar a -> FlexibleVar a Source # mapArgInfo :: (ArgInfo -> ArgInfo) -> FlexibleVar a -> FlexibleVar a Source # | |
| LensArgInfo (Dom' t e) Source # | |
Defined in Mikan.Syntax.Internal.Dom | |
class LensFixity a where Source #
Methods
lensFixity :: Lens' a Fixity Source #
Instances
| LensFixity AbstractName Source # | |
Defined in Mikan.Syntax.Abstract.Name Methods | |
| LensFixity Name Source # | |
Defined in Mikan.Syntax.Abstract.Name | |
| LensFixity QName Source # | |
Defined in Mikan.Syntax.Abstract.Name | |
| LensFixity Fixity Source # | |
Defined in Mikan.Syntax.Common | |
| LensFixity Fixity' Source # | |
Defined in Mikan.Syntax.Common | |
| LensFixity NewNotation Source # | |
Defined in Mikan.Syntax.Notation Methods | |
| LensFixity (ThingWithFixity a) Source # | |
Defined in Mikan.Syntax.Fixity Methods lensFixity :: Lens' (ThingWithFixity a) Fixity Source # | |
class LensFixity' a where Source #
Methods
lensFixity' :: Lens' a Fixity' Source #
Instances
| LensFixity' Name Source # | |
Defined in Mikan.Syntax.Abstract.Name | |
| LensFixity' QName Source # | |
Defined in Mikan.Syntax.Abstract.Name | |
| LensFixity' Fixity' Source # | |
Defined in Mikan.Syntax.Common | |
| LensFixity' (ThingWithFixity a) Source # | |
Defined in Mikan.Syntax.Fixity Methods lensFixity' :: Lens' (ThingWithFixity a) Fixity' Source # | |
class LensFreeVariables a where Source #
A lens to access the FreeVariables attribute in data structures.
Minimal implementation: getFreeVariables and mapFreeVariables or LensArgInfo.
Minimal complete definition
Nothing
Methods
getFreeVariables :: a -> FreeVariables Source #
default getFreeVariables :: LensArgInfo a => a -> FreeVariables Source #
setFreeVariables :: FreeVariables -> a -> a Source #
mapFreeVariables :: (FreeVariables -> FreeVariables) -> a -> a Source #
default mapFreeVariables :: LensArgInfo a => (FreeVariables -> FreeVariables) -> a -> a Source #
Instances
| LensFreeVariables ArgInfo Source # | |
Defined in Mikan.Syntax.Common Methods getFreeVariables :: ArgInfo -> FreeVariables Source # setFreeVariables :: FreeVariables -> ArgInfo -> ArgInfo Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> ArgInfo -> ArgInfo Source # | |
| LensFreeVariables FreeVariables Source # | |
Defined in Mikan.Syntax.Common Methods getFreeVariables :: FreeVariables -> FreeVariables Source # setFreeVariables :: FreeVariables -> FreeVariables -> FreeVariables Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> FreeVariables -> FreeVariables Source # | |
| LensFreeVariables (Arg e) Source # | |
Defined in Mikan.Syntax.Common Methods getFreeVariables :: Arg e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Arg e -> Arg e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Arg e -> Arg e Source # | |
| LensFreeVariables (Dom' t e) Source # | |
Defined in Mikan.Syntax.Internal.Dom Methods getFreeVariables :: Dom' t e -> FreeVariables Source # setFreeVariables :: FreeVariables -> Dom' t e -> Dom' t e Source # mapFreeVariables :: (FreeVariables -> FreeVariables) -> Dom' t e -> Dom' t e Source # | |
class LensHiding a where Source #
A lens to access the Hiding attribute in data structures.
Minimal implementation: getHiding and mapHiding or LensArgInfo.
Minimal complete definition
Nothing
Methods
getHiding :: a -> Hiding Source #
default getHiding :: LensArgInfo a => a -> Hiding Source #
Instances
| LensHiding LamBinding Source # | |
Defined in Mikan.Syntax.Abstract Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |
| LensHiding TypedBinding Source # | |
Defined in Mikan.Syntax.Abstract Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source # | |
| LensHiding ArgInfo Source # | |
| LensHiding Hiding Source # | |
| LensHiding LamBinding Source # | |
Defined in Mikan.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |
| LensHiding TypedBinding Source # | |
Defined in Mikan.Syntax.Concrete Methods getHiding :: TypedBinding -> Hiding Source # setHiding :: Hiding -> TypedBinding -> TypedBinding Source # mapHiding :: (Hiding -> Hiding) -> TypedBinding -> TypedBinding Source # | |
| LensHiding ContextEntry Source # | |
Defined in Mikan.TypeChecking.Monad.Base.Types Methods getHiding :: ContextEntry -> Hiding Source # setHiding :: Hiding -> ContextEntry -> ContextEntry Source # mapHiding :: (Hiding -> Hiding) -> ContextEntry -> ContextEntry Source # | |
| LensHiding (Arg e) Source # | |
| LensHiding (WithHiding a) Source # | |
Defined in Mikan.Syntax.Common Methods getHiding :: WithHiding a -> Hiding Source # setHiding :: Hiding -> WithHiding a -> WithHiding a Source # mapHiding :: (Hiding -> Hiding) -> WithHiding a -> WithHiding a Source # | |
| LensHiding (FlexibleVar a) Source # | |
Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods getHiding :: FlexibleVar a -> Hiding Source # setHiding :: Hiding -> FlexibleVar a -> FlexibleVar a Source # mapHiding :: (Hiding -> Hiding) -> FlexibleVar a -> FlexibleVar a Source # | |
| LensHiding a => LensHiding (Named nm a) Source # | |
| LensHiding (Dom' t e) Source # | |
class LensIsAbstract a where Source #
Methods
lensIsAbstract :: Lens' a IsAbstract Source #
Instances
| LensIsAbstract IsAbstract Source # | |
Defined in Mikan.Syntax.Common Methods | |
| LensIsAbstract MetaInfo Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| LensIsAbstract TCEnv Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
| LensIsAbstract (DefInfo' t) Source # | |
Defined in Mikan.Syntax.Info Methods lensIsAbstract :: Lens' (DefInfo' t) IsAbstract Source # | |
| LensIsAbstract (Closure a) Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods lensIsAbstract :: Lens' (Closure a) IsAbstract Source # | |
class LensIsOpaque a where Source #
Methods
lensIsOpaque :: Lens' a IsOpaque Source #
Instances
| LensIsOpaque IsOpaque Source # | |
Defined in Mikan.Syntax.Common | |
| LensIsOpaque MetaInfo Source # | |
Defined in Mikan.TypeChecking.Monad.Base | |
| LensIsOpaque TCEnv Source # | |
Defined in Mikan.TypeChecking.Monad.Base | |
| LensIsOpaque (DefInfo' t) Source # | |
Defined in Mikan.Syntax.Info | |
| LensIsOpaque (Closure a) Source # | |
Defined in Mikan.TypeChecking.Monad.Base | |
class LensNamed a where Source #
Accessor/editor for the nameOf component.
Minimal complete definition
Nothing
Methods
class LensOrigin a where Source #
A lens to access the Origin attribute in data structures.
Minimal implementation: getOrigin and mapOrigin or LensArgInfo.
Minimal complete definition
Nothing
Methods
getOrigin :: a -> Origin Source #
default getOrigin :: LensArgInfo a => a -> Origin Source #
Instances
| LensOrigin ArgInfo Source # | |
| LensOrigin Origin Source # | |
| LensOrigin AppInfo Source # | |
| LensOrigin ContextEntry Source # | |
Defined in Mikan.TypeChecking.Monad.Base.Types Methods getOrigin :: ContextEntry -> Origin Source # setOrigin :: Origin -> ContextEntry -> ContextEntry Source # mapOrigin :: (Origin -> Origin) -> ContextEntry -> ContextEntry Source # | |
| LensOrigin (Arg e) Source # | |
| LensOrigin (WithOrigin a) Source # | |
Defined in Mikan.Syntax.Common Methods getOrigin :: WithOrigin a -> Origin Source # setOrigin :: Origin -> WithOrigin a -> WithOrigin a Source # mapOrigin :: (Origin -> Origin) -> WithOrigin a -> WithOrigin a Source # | |
| LensOrigin (Elim' a) Source # | This instance cheats on |
| LensOrigin (FlexibleVar a) Source # | |
Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods getOrigin :: FlexibleVar a -> Origin Source # setOrigin :: Origin -> FlexibleVar a -> FlexibleVar a Source # mapOrigin :: (Origin -> Origin) -> FlexibleVar a -> FlexibleVar a Source # | |
| LensOrigin (Dom' t e) Source # | |
data MaybePlaceholder e Source #
Placeholders are used to represent the underscores in a section.
Constructors
| Placeholder !PositionInName | |
| NoPlaceholder !(Maybe PositionInName) e | The second argument is used only (but not always) for name parts other than underscores. |
Instances
| Functor MaybePlaceholder Source # | |
Defined in Mikan.Syntax.Common Methods fmap :: (a -> b) -> MaybePlaceholder a -> MaybePlaceholder b # (<$) :: a -> MaybePlaceholder b -> MaybePlaceholder a # | |
| Foldable MaybePlaceholder Source # | |
Defined in Mikan.Syntax.Common Methods fold :: Monoid m => MaybePlaceholder m -> m # foldMap :: Monoid m => (a -> m) -> MaybePlaceholder a -> m # foldMap' :: Monoid m => (a -> m) -> MaybePlaceholder a -> m # foldr :: (a -> b -> b) -> b -> MaybePlaceholder a -> b # foldr' :: (a -> b -> b) -> b -> MaybePlaceholder a -> b # foldl :: (b -> a -> b) -> b -> MaybePlaceholder a -> b # foldl' :: (b -> a -> b) -> b -> MaybePlaceholder a -> b # foldr1 :: (a -> a -> a) -> MaybePlaceholder a -> a # foldl1 :: (a -> a -> a) -> MaybePlaceholder a -> a # toList :: MaybePlaceholder a -> [a] # null :: MaybePlaceholder a -> Bool # length :: MaybePlaceholder a -> Int # elem :: Eq a => a -> MaybePlaceholder a -> Bool # maximum :: Ord a => MaybePlaceholder a -> a # minimum :: Ord a => MaybePlaceholder a -> a # sum :: Num a => MaybePlaceholder a -> a # product :: Num a => MaybePlaceholder a -> a # | |
| Traversable MaybePlaceholder Source # | |
Defined in Mikan.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> MaybePlaceholder a -> f (MaybePlaceholder b) # sequenceA :: Applicative f => MaybePlaceholder (f a) -> f (MaybePlaceholder a) # mapM :: Monad m => (a -> m b) -> MaybePlaceholder a -> m (MaybePlaceholder b) # sequence :: Monad m => MaybePlaceholder (m a) -> m (MaybePlaceholder a) # | |
| Pretty a => Pretty (MaybePlaceholder a) Source # | |
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: MaybePlaceholder a -> Doc Source # prettyPrec :: Int -> MaybePlaceholder a -> Doc Source # prettyList :: [MaybePlaceholder a] -> Doc Source # | |
| ExprLike a => ExprLike (MaybePlaceholder a) Source # | |
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> MaybePlaceholder a -> MaybePlaceholder a Source # foldExpr :: Monoid m => (Expr -> m) -> MaybePlaceholder a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> MaybePlaceholder a -> m (MaybePlaceholder a) Source # | |
| HasRange a => HasRange (MaybePlaceholder a) Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: MaybePlaceholder a -> Range Source # | |
| KillRange a => KillRange (MaybePlaceholder a) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (MaybePlaceholder a) Source # | |
| NFData a => NFData (MaybePlaceholder a) Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: MaybePlaceholder a -> () # | |
| Show e => Show (MaybePlaceholder e) Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> MaybePlaceholder e -> ShowS # show :: MaybePlaceholder e -> String # showList :: [MaybePlaceholder e] -> ShowS # | |
| Eq e => Eq (MaybePlaceholder e) Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (/=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # | |
| Ord e => Ord (MaybePlaceholder e) Source # | |
Defined in Mikan.Syntax.Common Methods compare :: MaybePlaceholder e -> MaybePlaceholder e -> Ordering # (<) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (<=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (>) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # (>=) :: MaybePlaceholder e -> MaybePlaceholder e -> Bool # max :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e # min :: MaybePlaceholder e -> MaybePlaceholder e -> MaybePlaceholder e # | |
Meta-variable identifiers use the same structure as NameIds.
Constructors
| MetaId | |
Fields
| |
Instances
| EncodeTCM MetaId Source # | |||||
| Pretty MetaId Source # | |||||
| GetDefs MetaId Source # | |||||
| NamesIn MetaId Source # | |||||
Defined in Mikan.Syntax.Internal.Names | |||||
| Reify MetaId Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| HasFresh MetaId Source # | |||||
| UnFreezeMeta MetaId Source # | |||||
Defined in Mikan.TypeChecking.Monad.MetaVars Methods unfreezeMeta :: MonadMetaSolver m => MetaId -> m () Source # | |||||
| PrettyTCM MetaId Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| FromTerm MetaId Source # | |||||
Defined in Mikan.TypeChecking.Primitive | |||||
| PrimTerm MetaId Source # | |||||
| PrimType MetaId Source # | |||||
| ToTerm MetaId Source # | |||||
| EmbPrj MetaId Source # | |||||
| Unquote MetaId Source # | |||||
| ToJSON MetaId Source # | |||||
| NFData MetaId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum MetaId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Generic MetaId Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show MetaId Source # | The record selectors are not included in the resulting strings. | ||||
| Eq MetaId Source # | |||||
| Ord MetaId Source # | |||||
| Hashable MetaId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Singleton MetaId MetaSet Source # | |||||
| InstantiateFull (Judgement MetaId) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| type ReifiesTo MetaId Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract | |||||
| type Rep MetaId Source # | |||||
Defined in Mikan.Syntax.Common type Rep MetaId = D1 ('MetaData "MetaId" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "MetaId" 'PrefixI 'True) (S1 ('MetaSel ('Just "metaId") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Just "metaModule") 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) | |||||
The unique identifier of a name. Second argument is the top-level module identifier.
Constructors
| NameId !Word64 !ModuleNameHash |
Instances
| Pretty NameId Source # | |||||
| KillRange NameId Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| HasFresh NameId Source # | |||||
| EmbPrj NameId Source # | |||||
| Null NameId Source # | |||||
| NFData NameId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum NameId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Generic NameId Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show NameId Source # | |||||
| Eq NameId Source # | |||||
| Ord NameId Source # | |||||
| Hashable NameId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| type Rep NameId Source # | |||||
Defined in Mikan.Syntax.Common type Rep NameId = D1 ('MetaData "NameId" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "NameId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) | |||||
The type of the name
Instances
| type NameOf (Arg a) Source # | |
Defined in Mikan.Syntax.Common | |
| type NameOf (Maybe a) Source # | |
Defined in Mikan.Syntax.Common | |
| type NameOf (Named name a) Source # | |
Defined in Mikan.Syntax.Common | |
| type NameOf (Dom' t e) Source # | |
Defined in Mikan.Syntax.Internal.Dom | |
Something potentially carrying a name.
Constructors
| Named | |
Fields
| |
Instances
| MapNamedArgPattern NAP Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern | |||||
| MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
| PatternLike a b => PatternLike a (Named x b) Source # | |||||
| Pretty e => Pretty (Named_ e) Source # | |||||
| HasDefP a => HasDefP (Named_ a) Source # | |||||
| PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Mikan.Syntax.Internal.Pattern Associated Types
| |||||
| PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM (NamedArg Term) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM (Named_ Term) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |||||
Defined in Mikan.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |||||
| Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
| DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute.DeBruijn | |||||
| IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Mikan.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source # | |||||
| Decoration (Named name) Source # | |||||
| Functor (Named name) Source # | |||||
| Foldable (Named name) Source # | |||||
Defined in Mikan.Syntax.Common Methods fold :: Monoid m => Named name m -> m # foldMap :: Monoid m => (a -> m) -> Named name a -> m # foldMap' :: Monoid m => (a -> m) -> Named name a -> m # foldr :: (a -> b -> b) -> b -> Named name a -> b # foldr' :: (a -> b -> b) -> b -> Named name a -> b # foldl :: (b -> a -> b) -> b -> Named name a -> b # foldl' :: (b -> a -> b) -> b -> Named name a -> b # foldr1 :: (a -> a -> a) -> Named name a -> a # foldl1 :: (a -> a -> a) -> Named name a -> a # toList :: Named name a -> [a] # null :: Named name a -> Bool # length :: Named name a -> Int # elem :: Eq a => a -> Named name a -> Bool # maximum :: Ord a => Named name a -> a # minimum :: Ord a => Named name a -> a # | |||||
| Traversable (Named name) Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| SubstExpr a => SubstExpr (Named name a) Source # | |||||
| IsProjP a => IsProjP (Named n a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Name Methods isProjP :: Named n a -> Maybe (ProjOrigin, AmbiguousQName) Source # | |||||
| APatternLike a => APatternLike (Named n a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern Associated Types
Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (Named n a)) -> m -> m) -> Named n a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> (Pattern' (ADotT (Named n a)) -> m (Pattern' (ADotT (Named n a)))) -> Named n a -> m (Named n a) Source # | |||||
| DeclaredNames a => DeclaredNames (Named name a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => Named name a -> m Source # | |||||
| ExprLike a => ExprLike (Named x a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Named x a) Source # foldExpr :: FoldExprFn m (Named x a) Source # traverseExpr :: TraverseExprFn m (Named x a) Source # mapExpr :: (Expr -> Expr) -> Named x a -> Named x a Source # | |||||
| LensHiding a => LensHiding (Named nm a) Source # | |||||
| LensNamed (Named name a) Source # | |||||
| ExprLike a => ExprLike (Named name a) Source # | |||||
| CPatternLike p => CPatternLike (Named n p) Source # | |||||
Defined in Mikan.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> Named n p -> m Source # traverseCPatternA :: Applicative m => (Pattern -> m Pattern -> m Pattern) -> Named n p -> m (Named n p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> Named n p -> m (Named n p) Source # | |||||
| IsWithP p => IsWithP (Named n p) Source # | |||||
| NamesIn a => NamesIn (Named n a) Source # | |||||
Defined in Mikan.Syntax.Internal.Names | |||||
| CountPatternVars a => CountPatternVars (Named x a) Source # | |||||
Defined in Mikan.Syntax.Internal.Pattern Methods countPatternVars :: Named x a -> Int Source # | |||||
| HasRange a => HasRange (Named name a) Source # | |||||
| (KillRange name, KillRange a) => KillRange (Named name a) Source # | |||||
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Named name a) Source # | |||||
| SetRange a => SetRange (Named name a) Source # | |||||
| ToConcrete a => ToConcrete (Named name a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
| |||||
| ToAbstract c => ToAbstract (Named name c) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| Reify i => Reify (Named n i) Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract Associated Types
| |||||
| ToAbstract r => ToAbstract (Named name r) Source # | |||||
Defined in Mikan.Syntax.Translation.ReflectedToAbstract Associated Types
Methods toAbstract :: MonadReflectedToAbstract m => Named name r -> m (AbsOfRef (Named name r)) Source # | |||||
| AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # | |||||
| AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
| ExpandPatternSynonyms a => ExpandPatternSynonyms (Named n a) Source # | |||||
Defined in Mikan.TypeChecking.Patterns.Abstract | |||||
| InstantiateFull t => InstantiateFull (Named name t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Normalise t => Normalise (Named name t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| Simplify t => Simplify (Named name t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| IsFlexiblePattern a => IsFlexiblePattern (Named name a) Source # | |||||
Defined in Mikan.TypeChecking.Rules.LHS Methods maybeFlexiblePattern :: forall (m :: Type -> Type). HasConstInfo m => Named name a -> MaybeT m FlexibleVarKind Source # isFlexiblePattern :: HasConstInfo m => Named name a -> m Bool Source # | |||||
| (EmbPrj s, EmbPrj t) => EmbPrj (Named s t) Source # | |||||
| Subst a => Subst (Named name a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Named name a)) -> Named name a -> Named name a Source # | |||||
| PiApplyArgs a => PiApplyArgs (Named n a) Source # | |||||
| (NFData name, NFData a) => NFData (Named name a) Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| (Show name, Show a) => Show (Named name a) Source # | |||||
| (Eq name, Eq a) => Eq (Named name a) Source # | |||||
| (Ord name, Ord a) => Ord (Named name a) Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| PatternToExpr p e => PatternToExpr (Named n p) (Named n e) Source # | |||||
| TermToPattern a b => TermToPattern (Named c a) (Named c b) Source # | |||||
Defined in Mikan.TypeChecking.Patterns.Internal | |||||
| type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Mikan.Syntax.Internal.Pattern | |||||
| type ADotT (Named n a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern | |||||
| type NameOf (Named name a) Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| type ConOfAbs (Named name a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
| type AbsOfCon (Named name c) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
| type ReifiesTo (Named n i) Source # | |||||
Defined in Mikan.Syntax.Translation.InternalToAbstract | |||||
| type AbsOfRef (Named name r) Source # | |||||
Defined in Mikan.Syntax.Translation.ReflectedToAbstract | |||||
| type SubstArg (Named name a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
type Notation = [NotationPart] Source #
Notation as provided by the syntax declaration.
data NotationPart Source #
Notation parts.
Constructors
| IdPart RString | An identifier part. For instance, for |
| HolePart Range (NamedArg (Ranged Int)) | A hole: a place where argument expressions can be written.
For instance, for |
| VarPart Range (Ranged BoundVariablePosition) | A bound variable. The first range is the range of the variable in the right-hand side of the syntax declaration, and the second range is the range of the variable in the left-hand side. |
| WildPart (Ranged BoundVariablePosition) | A wildcard (an underscore in binding position). |
Instances
| Pretty NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods pretty :: NotationPart -> Doc Source # prettyPrec :: Int -> NotationPart -> Doc Source # prettyList :: [NotationPart] -> Doc Source # | |
| HasRange NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: NotationPart -> Range Source # | |
| KillRange NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods | |
| SetRange NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods setRange :: Range -> NotationPart -> NotationPart Source # | |
| EmbPrj NotationPart Source # | |
| NFData NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: NotationPart -> () # | |
| Show NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> NotationPart -> ShowS # show :: NotationPart -> String # showList :: [NotationPart] -> ShowS # | |
| Eq NotationPart Source # | |
Defined in Mikan.Syntax.Common | |
| Ord NotationPart Source # | |
Defined in Mikan.Syntax.Common Methods compare :: NotationPart -> NotationPart -> Ordering # (<) :: NotationPart -> NotationPart -> Bool # (<=) :: NotationPart -> NotationPart -> Bool # (>) :: NotationPart -> NotationPart -> Bool # (>=) :: NotationPart -> NotationPart -> Bool # max :: NotationPart -> NotationPart -> NotationPart # min :: NotationPart -> NotationPart -> NotationPart # | |
The unique identifier of an opaque block. Second argument is the top-level module identifier.
Constructors
| OpaqueId !Word64 !ModuleNameHash |
Instances
| Pretty OpaqueId Source # | |||||
| KillRange OpaqueId Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| HasFresh OpaqueId Source # | |||||
| EmbPrj OpaqueId Source # | |||||
| NFData OpaqueId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum OpaqueId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Generic OpaqueId Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show OpaqueId Source # | |||||
| Eq OpaqueId Source # | |||||
| Ord OpaqueId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Hashable OpaqueId Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| type Rep OpaqueId Source # | |||||
Defined in Mikan.Syntax.Common type Rep OpaqueId = D1 ('MetaData "OpaqueId" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "OpaqueId" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 Word64) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'SourceUnpack 'SourceStrict 'DecidedStrict) (Rec0 ModuleNameHash))) | |||||
Origin of arguments.
Constructors
| UserWritten | From the source file / user input. (Preserve!) |
| Inserted | E.g. inserted hidden arguments. |
| Reflected | Produced by the reflection machinery. |
| CaseSplit | Produced by an interactive case split. |
| Substitution | Named application produced to represent a substitution. E.g. "?0 (x = n)" instead of "?0 n" |
| ExpandedPun | An expanded hidden argument pun. |
| Generalization | Inserted by the generalization process |
| ConversionFail | Inserted by the conversion checker in an argument spine at the position where they differ. Indicates that the argument at this position should always be reified, even if the visibility would be skipped with the current flags. |
| RecordSelf | Inserted to stand for the record "self" variable when checking a declaration inside a record module. |
Instances
| LensOrigin Origin Source # | |
| HasRange Origin Source # | |
| KillRange Origin Source # | |
Defined in Mikan.Syntax.Common Methods | |
| ChooseFlex Origin Source # | |
Defined in Mikan.TypeChecking.Rules.LHS.Problem Methods chooseFlex :: Origin -> Origin -> FlexChoice Source # | |
| EmbPrj Origin Source # | |
| NFData Origin Source # | |
Defined in Mikan.Syntax.Common | |
| Show Origin Source # | |
| Eq Origin Source # | |
| Ord Origin Source # | |
data OverlapMode Source #
The possible overlap modes for an instance, also used for instance candidates.
Constructors
| Overlappable | User-written OVERLAPPABLE pragma: this candidate can *be removed* by a more specific candidate. |
| Overlapping | User-written OVERLAPPING pragma: this candidate can *remove* a less specific candidate. |
| Overlaps | User-written OVERLAPS pragma: both overlappable and overlapping. |
| DefaultOverlap | No user-written overlap pragma. This instance can be overlapped by an OVERLAPPING instance, and it can overlap OVERLAPPABLE instances. |
| Incoherent | User-written INCOHERENT pragma: both overlappable and overlapping; and, if there are multiple candidates after all overlap has been handled, make an arbitrary choice. |
| FieldOverlap | Overlapping instances in record fields. |
Instances
| HasOverlapMode OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods | |
| Pretty OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods pretty :: OverlapMode -> Doc Source # prettyPrec :: Int -> OverlapMode -> Doc Source # prettyList :: [OverlapMode] -> Doc Source # | |
| KillRange OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods | |
| EmbPrj OverlapMode Source # | |
| NFData OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: OverlapMode -> () # | |
| Bounded OverlapMode Source # | |
Defined in Mikan.Syntax.Common | |
| Enum OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods succ :: OverlapMode -> OverlapMode # pred :: OverlapMode -> OverlapMode # toEnum :: Int -> OverlapMode # fromEnum :: OverlapMode -> Int # enumFrom :: OverlapMode -> [OverlapMode] # enumFromThen :: OverlapMode -> OverlapMode -> [OverlapMode] # enumFromTo :: OverlapMode -> OverlapMode -> [OverlapMode] # enumFromThenTo :: OverlapMode -> OverlapMode -> OverlapMode -> [OverlapMode] # | |
| Show OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> OverlapMode -> ShowS # show :: OverlapMode -> String # showList :: [OverlapMode] -> ShowS # | |
| Eq OverlapMode Source # | |
Defined in Mikan.Syntax.Common | |
| Ord OverlapMode Source # | |
Defined in Mikan.Syntax.Common Methods compare :: OverlapMode -> OverlapMode -> Ordering # (<) :: OverlapMode -> OverlapMode -> Bool # (<=) :: OverlapMode -> OverlapMode -> Bool # (>) :: OverlapMode -> OverlapMode -> Bool # (>=) :: OverlapMode -> OverlapMode -> Bool # max :: OverlapMode -> OverlapMode -> OverlapMode # min :: OverlapMode -> OverlapMode -> OverlapMode # | |
data Overlappable Source #
Constructors
| YesOverlap | |
| NoOverlap |
Instances
| NFData Overlappable Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: Overlappable -> () # | |
| Monoid Overlappable Source # | |
Defined in Mikan.Syntax.Common Methods mempty :: Overlappable # mappend :: Overlappable -> Overlappable -> Overlappable # mconcat :: [Overlappable] -> Overlappable # | |
| Semigroup Overlappable Source # | Just for the |
Defined in Mikan.Syntax.Common Methods (<>) :: Overlappable -> Overlappable -> Overlappable # sconcat :: NonEmpty Overlappable -> Overlappable # stimes :: Integral b => b -> Overlappable -> Overlappable # | |
| Bounded Overlappable Source # | |
Defined in Mikan.Syntax.Common | |
| Enum Overlappable Source # | |
Defined in Mikan.Syntax.Common Methods succ :: Overlappable -> Overlappable # pred :: Overlappable -> Overlappable # toEnum :: Int -> Overlappable # fromEnum :: Overlappable -> Int # enumFrom :: Overlappable -> [Overlappable] # enumFromThen :: Overlappable -> Overlappable -> [Overlappable] # enumFromTo :: Overlappable -> Overlappable -> [Overlappable] # enumFromThenTo :: Overlappable -> Overlappable -> Overlappable -> [Overlappable] # | |
| Show Overlappable Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> Overlappable -> ShowS # show :: Overlappable -> String # showList :: [Overlappable] -> ShowS # | |
| Eq Overlappable Source # | |
Defined in Mikan.Syntax.Common | |
| Ord Overlappable Source # | |
Defined in Mikan.Syntax.Common Methods compare :: Overlappable -> Overlappable -> Ordering # (<) :: Overlappable -> Overlappable -> Bool # (<=) :: Overlappable -> Overlappable -> Bool # (>) :: Overlappable -> Overlappable -> Bool # (>=) :: Overlappable -> Overlappable -> Bool # max :: Overlappable -> Overlappable -> Overlappable # min :: Overlappable -> Overlappable -> Overlappable # | |
class PatternMatchingAllowed a where Source #
Can we pattern match on the record constructor?
Methods
patternMatchingAllowed :: a -> Bool Source #
Instances
| PatternMatchingAllowed DataOrRecord Source # | |
Defined in Mikan.Syntax.Common Methods | |
| PatternMatchingAllowed HasEta Source # | |
Defined in Mikan.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
| PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| PatternMatchingAllowed Induction Source # | |
Defined in Mikan.Syntax.Common Methods | |
| PatternMatchingAllowed EtaEquality Source # | |
Defined in Mikan.TypeChecking.Monad.Base Methods | |
data PatternOrCopattern Source #
For a record without eta, which type of matching do we allow?
Constructors
| PatternMatching | Can match on the record constructor. |
| CopatternMatching | Can copattern match using the projections. (Default.) |
Instances
| CopatternMatchingAllowed DataOrRecord Source # | |
Defined in Mikan.Syntax.Common Methods | |
| CopatternMatchingAllowed HasEta Source # | |
Defined in Mikan.Syntax.Common Methods | |
| CopatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods copatternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| PatternMatchingAllowed DataOrRecord Source # | |
Defined in Mikan.Syntax.Common Methods | |
| PatternMatchingAllowed HasEta Source # | |
Defined in Mikan.Syntax.Common Methods patternMatchingAllowed :: HasEta -> Bool Source # | |
| PatternMatchingAllowed PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods patternMatchingAllowed :: PatternOrCopattern -> Bool Source # | |
| HasRange PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods getRange :: PatternOrCopattern -> Range Source # | |
| KillRange DataOrRecord Source # | |
Defined in Mikan.Syntax.Common Methods | |
| KillRange PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods | |
| EmbPrj PatternOrCopattern Source # | |
| NFData PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods rnf :: PatternOrCopattern -> () # | |
| Bounded PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common | |
| Enum PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods succ :: PatternOrCopattern -> PatternOrCopattern # pred :: PatternOrCopattern -> PatternOrCopattern # toEnum :: Int -> PatternOrCopattern # fromEnum :: PatternOrCopattern -> Int # enumFrom :: PatternOrCopattern -> [PatternOrCopattern] # enumFromThen :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] # enumFromTo :: PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] # enumFromThenTo :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern -> [PatternOrCopattern] # | |
| Show PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> PatternOrCopattern -> ShowS # show :: PatternOrCopattern -> String # showList :: [PatternOrCopattern] -> ShowS # | |
| Eq PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: PatternOrCopattern -> PatternOrCopattern -> Bool # (/=) :: PatternOrCopattern -> PatternOrCopattern -> Bool # | |
| Ord PatternOrCopattern Source # | |
Defined in Mikan.Syntax.Common Methods compare :: PatternOrCopattern -> PatternOrCopattern -> Ordering # (<) :: PatternOrCopattern -> PatternOrCopattern -> Bool # (<=) :: PatternOrCopattern -> PatternOrCopattern -> Bool # (>) :: PatternOrCopattern -> PatternOrCopattern -> Bool # (>=) :: PatternOrCopattern -> PatternOrCopattern -> Bool # max :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern # min :: PatternOrCopattern -> PatternOrCopattern -> PatternOrCopattern # | |
data PositionInName Source #
The position of a name part or underscore in a name.
Constructors
| Beginning | The following underscore is at the beginning of the name:
|
| Middle | The following underscore is in the middle of the name:
|
| End | The following underscore is at the end of the name: |
Instances
| Show PositionInName Source # | |
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> PositionInName -> ShowS # show :: PositionInName -> String # showList :: [PositionInName] -> ShowS # | |
| Eq PositionInName Source # | |
Defined in Mikan.Syntax.Common Methods (==) :: PositionInName -> PositionInName -> Bool # (/=) :: PositionInName -> PositionInName -> Bool # | |
| Ord PositionInName Source # | |
Defined in Mikan.Syntax.Common Methods compare :: PositionInName -> PositionInName -> Ordering # (<) :: PositionInName -> PositionInName -> Bool # (<=) :: PositionInName -> PositionInName -> Bool # (>) :: PositionInName -> PositionInName -> Bool # (>=) :: PositionInName -> PositionInName -> Bool # max :: PositionInName -> PositionInName -> PositionInName # min :: PositionInName -> PositionInName -> PositionInName # | |
data PositivityCheck Source #
Positivity check? (Default = True).
Constructors
| YesPositivityCheck | |
| NoPositivityCheck |
Instances
| KillRange PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| EmbPrj PositivityCheck Source # | |||||
| Null PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| NFData PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: PositivityCheck -> () # | |||||
| Monoid PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods mappend :: PositivityCheck -> PositivityCheck -> PositivityCheck # mconcat :: [PositivityCheck] -> PositivityCheck # | |||||
| Semigroup PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods (<>) :: PositivityCheck -> PositivityCheck -> PositivityCheck # sconcat :: NonEmpty PositivityCheck -> PositivityCheck # stimes :: Integral b => b -> PositivityCheck -> PositivityCheck # | |||||
| Bounded PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods succ :: PositivityCheck -> PositivityCheck # pred :: PositivityCheck -> PositivityCheck # toEnum :: Int -> PositivityCheck # fromEnum :: PositivityCheck -> Int # enumFrom :: PositivityCheck -> [PositivityCheck] # enumFromThen :: PositivityCheck -> PositivityCheck -> [PositivityCheck] # enumFromTo :: PositivityCheck -> PositivityCheck -> [PositivityCheck] # enumFromThenTo :: PositivityCheck -> PositivityCheck -> PositivityCheck -> [PositivityCheck] # | |||||
| Generic PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
Methods from :: PositivityCheck -> Rep PositivityCheck x # to :: Rep PositivityCheck x -> PositivityCheck # | |||||
| Show PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> PositivityCheck -> ShowS # show :: PositivityCheck -> String # showList :: [PositivityCheck] -> ShowS # | |||||
| Eq PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: PositivityCheck -> PositivityCheck -> Bool # (/=) :: PositivityCheck -> PositivityCheck -> Bool # | |||||
| Ord PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods compare :: PositivityCheck -> PositivityCheck -> Ordering # (<) :: PositivityCheck -> PositivityCheck -> Bool # (<=) :: PositivityCheck -> PositivityCheck -> Bool # (>) :: PositivityCheck -> PositivityCheck -> Bool # (>=) :: PositivityCheck -> PositivityCheck -> Bool # max :: PositivityCheck -> PositivityCheck -> PositivityCheck # min :: PositivityCheck -> PositivityCheck -> PositivityCheck # | |||||
| type Rep PositivityCheck Source # | |||||
Defined in Mikan.Syntax.Common | |||||
type PrecedenceLevel = Double Source #
Precedence levels for operators.
A "problem" consists of a set of constraints and the same constraint can be part of multiple problems.
Instances
| EncodeTCM ProblemId Source # | |
| Pretty ProblemId Source # | |
| HasFresh ProblemId Source # | |
| PrettyTCM ProblemId Source # | |
Defined in Mikan.TypeChecking.Pretty | |
| EmbPrj ProblemId Source # | |
| ToJSON ProblemId Source # | |
| NFData ProblemId Source # | |
Defined in Mikan.Syntax.Common | |
| Enum ProblemId Source # | |
Defined in Mikan.Syntax.Common Methods succ :: ProblemId -> ProblemId # pred :: ProblemId -> ProblemId # fromEnum :: ProblemId -> Int # enumFrom :: ProblemId -> [ProblemId] # enumFromThen :: ProblemId -> ProblemId -> [ProblemId] # enumFromTo :: ProblemId -> ProblemId -> [ProblemId] # enumFromThenTo :: ProblemId -> ProblemId -> ProblemId -> [ProblemId] # | |
| Num ProblemId Source # | |
Defined in Mikan.Syntax.Common | |
| Integral ProblemId Source # | |
Defined in Mikan.Syntax.Common Methods quot :: ProblemId -> ProblemId -> ProblemId # rem :: ProblemId -> ProblemId -> ProblemId # div :: ProblemId -> ProblemId -> ProblemId # mod :: ProblemId -> ProblemId -> ProblemId # quotRem :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # divMod :: ProblemId -> ProblemId -> (ProblemId, ProblemId) # | |
| Real ProblemId Source # | |
Defined in Mikan.Syntax.Common Methods toRational :: ProblemId -> Rational # | |
| Show ProblemId Source # | |
| Eq ProblemId Source # | |
| Ord ProblemId Source # | |
data ProjOrigin Source #
Where does a projection come from?
Constructors
| ProjPrefix | User wrote a prefix projection. |
| ProjPostfix | User wrote a postfix projection. |
| ProjSystem | Projection was generated by the system. |
Instances
| KillRange ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| EmbPrj ProjOrigin Source # | |||||
| NFData ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: ProjOrigin -> () # | |||||
| Bounded ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods succ :: ProjOrigin -> ProjOrigin # pred :: ProjOrigin -> ProjOrigin # toEnum :: Int -> ProjOrigin # fromEnum :: ProjOrigin -> Int # enumFrom :: ProjOrigin -> [ProjOrigin] # enumFromThen :: ProjOrigin -> ProjOrigin -> [ProjOrigin] # enumFromTo :: ProjOrigin -> ProjOrigin -> [ProjOrigin] # enumFromThenTo :: ProjOrigin -> ProjOrigin -> ProjOrigin -> [ProjOrigin] # | |||||
| Generic ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> ProjOrigin -> ShowS # show :: ProjOrigin -> String # showList :: [ProjOrigin] -> ShowS # | |||||
| Eq ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Ord ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods compare :: ProjOrigin -> ProjOrigin -> Ordering # (<) :: ProjOrigin -> ProjOrigin -> Bool # (<=) :: ProjOrigin -> ProjOrigin -> Bool # (>) :: ProjOrigin -> ProjOrigin -> Bool # (>=) :: ProjOrigin -> ProjOrigin -> Bool # max :: ProjOrigin -> ProjOrigin -> ProjOrigin # min :: ProjOrigin -> ProjOrigin -> ProjOrigin # | |||||
| type Rep ProjOrigin Source # | |||||
Defined in Mikan.Syntax.Common type Rep ProjOrigin = D1 ('MetaData "ProjOrigin" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "ProjPrefix" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "ProjPostfix" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "ProjSystem" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
Thing with range info.
Constructors
| Ranged | |
Fields
| |
Instances
| MapNamedArgPattern NAP Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern | |||||
| Decoration Ranged Source # | |||||
| Functor Ranged Source # | |||||
| Foldable Ranged Source # | |||||
Defined in Mikan.Syntax.Common Methods fold :: Monoid m => Ranged m -> m # foldMap :: Monoid m => (a -> m) -> Ranged a -> m # foldMap' :: Monoid m => (a -> m) -> Ranged a -> m # foldr :: (a -> b -> b) -> b -> Ranged a -> b # foldr' :: (a -> b -> b) -> b -> Ranged a -> b # foldl :: (b -> a -> b) -> b -> Ranged a -> b # foldl' :: (b -> a -> b) -> b -> Ranged a -> b # foldr1 :: (a -> a -> a) -> Ranged a -> a # foldl1 :: (a -> a -> a) -> Ranged a -> a # elem :: Eq a => a -> Ranged a -> Bool # maximum :: Ord a => Ranged a -> a # minimum :: Ord a => Ranged a -> a # | |||||
| Traversable Ranged Source # | |||||
| MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
| ExprLike a => ExprLike (Ranged a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (Ranged a) Source # foldExpr :: FoldExprFn m (Ranged a) Source # traverseExpr :: TraverseExprFn m (Ranged a) Source # | |||||
| Pretty e => Pretty (Named_ e) Source # | |||||
| Pretty a => Pretty (Ranged a) Source # | Ignores range. | ||||
| ExprLike a => ExprLike (Ranged a) Source # | |||||
| IsNoName a => IsNoName (Ranged a) Source # | |||||
| HasDefP a => HasDefP (Named_ a) Source # | |||||
| PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Mikan.Syntax.Internal.Pattern Associated Types
| |||||
| HasRange (Ranged a) Source # | |||||
| KillRange (Ranged a) Source # | |||||
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Ranged a) Source # | |||||
| ToConcrete a => ToConcrete (Ranged a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
| |||||
| ToAbstract c => ToAbstract (Ranged c) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM (NamedArg Term) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM (Named_ Term) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |||||
Defined in Mikan.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |||||
| Normalise t => Normalise (Ranged t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce | |||||
| EmbPrj a => EmbPrj (Ranged a) Source # | |||||
| Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
| Subst a => Subst (Ranged a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (Ranged a)) -> Ranged a -> Ranged a Source # | |||||
| DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute.DeBruijn | |||||
| IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Mikan.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source # | |||||
| NFData a => NFData (Ranged a) Source # | Ranges are not forced. | ||||
Defined in Mikan.Syntax.Common | |||||
| Show a => Show (Ranged a) Source # | |||||
| Eq a => Eq (Ranged a) Source # | Ignores range. | ||||
| Ord a => Ord (Ranged a) Source # | Ignores range. | ||||
Defined in Mikan.Syntax.Common | |||||
| AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # | |||||
| AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
| type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Mikan.Syntax.Internal.Pattern | |||||
| type ConOfAbs (Ranged a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
| type AbsOfCon (Ranged c) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
| type SubstArg (Ranged a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
data RecordDirectives' a Source #
Constructors
| RecordDirectives | |
Fields
| |
Instances
| DeclaredNames RecordDirectives Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => RecordDirectives -> m Source # | |||||
| ToConcrete RecordDirectives Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => RecordDirectives -> m (ConOfAbs RecordDirectives) Source # bindToConcrete :: MonadToConcrete m => RecordDirectives -> (ConOfAbs RecordDirectives -> m b) -> m b Source # | |||||
| Functor RecordDirectives' Source # | |||||
Defined in Mikan.Syntax.Common Methods fmap :: (a -> b) -> RecordDirectives' a -> RecordDirectives' b # (<$) :: a -> RecordDirectives' b -> RecordDirectives' a # | |||||
| Foldable RecordDirectives' Source # | |||||
Defined in Mikan.Syntax.Common Methods fold :: Monoid m => RecordDirectives' m -> m # foldMap :: Monoid m => (a -> m) -> RecordDirectives' a -> m # foldMap' :: Monoid m => (a -> m) -> RecordDirectives' a -> m # foldr :: (a -> b -> b) -> b -> RecordDirectives' a -> b # foldr' :: (a -> b -> b) -> b -> RecordDirectives' a -> b # foldl :: (b -> a -> b) -> b -> RecordDirectives' a -> b # foldl' :: (b -> a -> b) -> b -> RecordDirectives' a -> b # foldr1 :: (a -> a -> a) -> RecordDirectives' a -> a # foldl1 :: (a -> a -> a) -> RecordDirectives' a -> a # toList :: RecordDirectives' a -> [a] # null :: RecordDirectives' a -> Bool # length :: RecordDirectives' a -> Int # elem :: Eq a => a -> RecordDirectives' a -> Bool # maximum :: Ord a => RecordDirectives' a -> a # minimum :: Ord a => RecordDirectives' a -> a # sum :: Num a => RecordDirectives' a -> a # product :: Num a => RecordDirectives' a -> a # | |||||
| Traversable RecordDirectives' Source # | |||||
Defined in Mikan.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> RecordDirectives' a -> f (RecordDirectives' b) # sequenceA :: Applicative f => RecordDirectives' (f a) -> f (RecordDirectives' a) # mapM :: Monad m => (a -> m b) -> RecordDirectives' a -> m (RecordDirectives' b) # sequence :: Monad m => RecordDirectives' (m a) -> m (RecordDirectives' a) # | |||||
| HasRange a => HasRange (RecordDirectives' a) Source # | |||||
Defined in Mikan.Syntax.Common Methods getRange :: RecordDirectives' a -> Range Source # | |||||
| KillRange a => KillRange (RecordDirectives' a) Source # | |||||
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (RecordDirectives' a) Source # | |||||
| EmbPrj a => EmbPrj (RecordDirectives' a) Source # | |||||
| Null a => Null (RecordDirectives' a) Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| NFData a => NFData (RecordDirectives' a) Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: RecordDirectives' a -> () # | |||||
| Show a => Show (RecordDirectives' a) Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> RecordDirectives' a -> ShowS # show :: RecordDirectives' a -> String # showList :: [RecordDirectives' a] -> ShowS # | |||||
| Eq a => Eq (RecordDirectives' a) Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: RecordDirectives' a -> RecordDirectives' a -> Bool # (/=) :: RecordDirectives' a -> RecordDirectives' a -> Bool # | |||||
| type ConOfAbs RecordDirectives Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
Constructors
| Renaming | |
Fields
| |
Instances
| (Pretty a, Pretty b) => Pretty (Renaming' a b) Source # | |
| (HasRange a, HasRange b) => HasRange (Renaming' a b) Source # | |
| (KillRange a, KillRange b) => KillRange (Renaming' a b) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Renaming' a b) Source # | |
| (NFData a, NFData b) => NFData (Renaming' a b) Source # | Ranges are not forced. |
Defined in Mikan.Syntax.Common | |
| (Show m, Show n) => Show (Renaming' n m) Source # | |
| (Eq m, Eq n) => Eq (Renaming' n m) Source # | |
type RenamingDirective' n m = [Renaming' n m] Source #
data RewriteEqn' qn nm p e Source #
RewriteEqn' qn p e represents the rewrite and irrefutable with
clauses of the LHS.
qn stands for the QName of the auxiliary function generated to implement the feature
nm is the type of names for pattern variables
p is the type of patterns
e is the type of expressions
Constructors
| Rewrite (List1 (qn, e)) | rewrite e |
| Invert qn (List1 (Named nm (p, e))) | with p <- e in eq |
| LeftLet (List1 (p, e)) | using p <- e |
Instances
| ToAbstract RewriteEqn Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source # | |||||
| Functor (RewriteEqn' qn nm p) Source # | |||||
Defined in Mikan.Syntax.Common Methods fmap :: (a -> b) -> RewriteEqn' qn nm p a -> RewriteEqn' qn nm p b # (<$) :: a -> RewriteEqn' qn nm p b -> RewriteEqn' qn nm p a # | |||||
| Foldable (RewriteEqn' qn nm p) Source # | |||||
Defined in Mikan.Syntax.Common Methods fold :: Monoid m => RewriteEqn' qn nm p m -> m # foldMap :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m # foldMap' :: Monoid m => (a -> m) -> RewriteEqn' qn nm p a -> m # foldr :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b # foldr' :: (a -> b -> b) -> b -> RewriteEqn' qn nm p a -> b # foldl :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b # foldl' :: (b -> a -> b) -> b -> RewriteEqn' qn nm p a -> b # foldr1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a # foldl1 :: (a -> a -> a) -> RewriteEqn' qn nm p a -> a # toList :: RewriteEqn' qn nm p a -> [a] # null :: RewriteEqn' qn nm p a -> Bool # length :: RewriteEqn' qn nm p a -> Int # elem :: Eq a => a -> RewriteEqn' qn nm p a -> Bool # maximum :: Ord a => RewriteEqn' qn nm p a -> a # minimum :: Ord a => RewriteEqn' qn nm p a -> a # sum :: Num a => RewriteEqn' qn nm p a -> a # product :: Num a => RewriteEqn' qn nm p a -> a # | |||||
| Traversable (RewriteEqn' qn nm p) Source # | |||||
Defined in Mikan.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> RewriteEqn' qn nm p a -> f (RewriteEqn' qn nm p b) # sequenceA :: Applicative f => RewriteEqn' qn nm p (f a) -> f (RewriteEqn' qn nm p a) # mapM :: Monad m => (a -> m b) -> RewriteEqn' qn nm p a -> m (RewriteEqn' qn nm p b) # sequence :: Monad m => RewriteEqn' qn nm p (m a) -> m (RewriteEqn' qn nm p a) # | |||||
| (ExprLike qn, ExprLike p, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (RewriteEqn' qn nm p e) Source # foldExpr :: FoldExprFn m (RewriteEqn' qn nm p e) Source # traverseExpr :: TraverseExprFn m (RewriteEqn' qn nm p e) Source # mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source # | |||||
| (Pretty nm, Pretty p, Pretty e) => Pretty (RewriteEqn' qn nm p e) Source # | |||||
Defined in Mikan.Syntax.Common Methods pretty :: RewriteEqn' qn nm p e -> Doc Source # prettyPrec :: Int -> RewriteEqn' qn nm p e -> Doc Source # prettyList :: [RewriteEqn' qn nm p e] -> Doc Source # | |||||
| (ExprLike qn, ExprLike e) => ExprLike (RewriteEqn' qn nm p e) Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e Source # foldExpr :: Monoid m => (Expr -> m) -> RewriteEqn' qn nm p e -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> RewriteEqn' qn nm p e -> m (RewriteEqn' qn nm p e) Source # | |||||
| (HasRange qn, HasRange p, HasRange e) => HasRange (RewriteEqn' qn nm p e) Source # | |||||
Defined in Mikan.Syntax.Common Methods getRange :: RewriteEqn' qn nm p e -> Range Source # | |||||
| (KillRange qn, KillRange nm, KillRange e, KillRange p) => KillRange (RewriteEqn' qn nm p e) Source # | |||||
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (RewriteEqn' qn nm p e) Source # | |||||
| (ToConcrete p, ToConcrete a) => ToConcrete (RewriteEqn' qn BindName p a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => RewriteEqn' qn BindName p a -> m (ConOfAbs (RewriteEqn' qn BindName p a)) Source # bindToConcrete :: MonadToConcrete m => RewriteEqn' qn BindName p a -> (ConOfAbs (RewriteEqn' qn BindName p a) -> m b) -> m b Source # | |||||
| ToAbstract (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: RewriteEqn' () BindName Pattern Expr -> ScopeM (AbsOfCon (RewriteEqn' () BindName Pattern Expr)) Source # | |||||
| (NFData qn, NFData nm, NFData p, NFData e) => NFData (RewriteEqn' qn nm p e) Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: RewriteEqn' qn nm p e -> () # | |||||
| (Show e, Show qn, Show nm, Show p) => Show (RewriteEqn' qn nm p e) Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> RewriteEqn' qn nm p e -> ShowS # show :: RewriteEqn' qn nm p e -> String # showList :: [RewriteEqn' qn nm p e] -> ShowS # | |||||
| (Eq e, Eq qn, Eq nm, Eq p) => Eq (RewriteEqn' qn nm p e) Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool # (/=) :: RewriteEqn' qn nm p e -> RewriteEqn' qn nm p e -> Bool # | |||||
| type AbsOfCon RewriteEqn Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
| type ConOfAbs (RewriteEqn' qn BindName p a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
| type AbsOfCon (RewriteEqn' () BindName Pattern Expr) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
data TerminationCheck Source #
Termination check? (Default = TerminationCheck).
Constructors
| TerminationCheck | Run the termination checker. |
| NoTerminationCheck | Skip termination checking (unsafe). |
| NonTerminating | Treat as non-terminating. |
| Terminating | Treat as terminating (unsafe). Same effect as |
Instances
| NFData TerminationCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: TerminationCheck -> () # | |||||
| Generic TerminationCheck Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
Methods from :: TerminationCheck -> Rep TerminationCheck x # to :: Rep TerminationCheck x -> TerminationCheck # | |||||
| Show TerminationCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> TerminationCheck -> ShowS # show :: TerminationCheck -> String # showList :: [TerminationCheck] -> ShowS # | |||||
| Eq TerminationCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: TerminationCheck -> TerminationCheck -> Bool # (/=) :: TerminationCheck -> TerminationCheck -> Bool # | |||||
| type Rep TerminationCheck Source # | |||||
Defined in Mikan.Syntax.Common type Rep TerminationCheck = D1 ('MetaData "TerminationCheck" "Mikan.Syntax.Common" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) ((C1 ('MetaCons "TerminationCheck" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NoTerminationCheck" 'PrefixI 'False) (U1 :: Type -> Type)) :+: (C1 ('MetaCons "NonTerminating" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "Terminating" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
class Eq a => Underscore a where Source #
Minimal complete definition
Instances
| Underscore Expr Source # | |
Defined in Mikan.Syntax.Abstract | |
| Underscore Doc Source # | |
Defined in Mikan.Syntax.Common | |
| Underscore Name Source # | |
Defined in Mikan.Syntax.Concrete.Name | |
| Underscore QName Source # | |
Defined in Mikan.Syntax.Concrete.Name | |
| Underscore ByteString Source # | |
Defined in Mikan.Syntax.Common | |
| Underscore Text Source # | |
Defined in Mikan.Syntax.Common | |
| Underscore ShortText Source # | |
Defined in Mikan.Syntax.Common | |
| Underscore String Source # | |
Defined in Mikan.Syntax.Common | |
data UniverseCheck Source #
Universe check? (Default is yes).
Constructors
| YesUniverseCheck | |
| NoUniverseCheck |
Instances
| KillRange UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods | |||||
| Null UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| NFData UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: UniverseCheck -> () # | |||||
| Monoid UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods mempty :: UniverseCheck # mappend :: UniverseCheck -> UniverseCheck -> UniverseCheck # mconcat :: [UniverseCheck] -> UniverseCheck # | |||||
| Semigroup UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods (<>) :: UniverseCheck -> UniverseCheck -> UniverseCheck # sconcat :: NonEmpty UniverseCheck -> UniverseCheck # stimes :: Integral b => b -> UniverseCheck -> UniverseCheck # | |||||
| Bounded UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Enum UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods succ :: UniverseCheck -> UniverseCheck # pred :: UniverseCheck -> UniverseCheck # toEnum :: Int -> UniverseCheck # fromEnum :: UniverseCheck -> Int # enumFrom :: UniverseCheck -> [UniverseCheck] # enumFromThen :: UniverseCheck -> UniverseCheck -> [UniverseCheck] # enumFromTo :: UniverseCheck -> UniverseCheck -> [UniverseCheck] # enumFromThenTo :: UniverseCheck -> UniverseCheck -> UniverseCheck -> [UniverseCheck] # | |||||
| Generic UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Associated Types
| |||||
| Show UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> UniverseCheck -> ShowS # show :: UniverseCheck -> String # showList :: [UniverseCheck] -> ShowS # | |||||
| Eq UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods (==) :: UniverseCheck -> UniverseCheck -> Bool # (/=) :: UniverseCheck -> UniverseCheck -> Bool # | |||||
| Ord UniverseCheck Source # | |||||
Defined in Mikan.Syntax.Common Methods compare :: UniverseCheck -> UniverseCheck -> Ordering # (<) :: UniverseCheck -> UniverseCheck -> Bool # (<=) :: UniverseCheck -> UniverseCheck -> Bool # (>) :: UniverseCheck -> UniverseCheck -> Bool # (>=) :: UniverseCheck -> UniverseCheck -> Bool # max :: UniverseCheck -> UniverseCheck -> UniverseCheck # min :: UniverseCheck -> UniverseCheck -> UniverseCheck # | |||||
| type Rep UniverseCheck Source # | |||||
The using clause of import directive.
Constructors
| UseEverything | No |
| Using [ImportedName' n m] |
|
Instances
| (Pretty a, Pretty b) => Pretty (Using' a b) Source # | |
| (HasRange a, HasRange b) => HasRange (Using' a b) Source # | |
| (KillRange a, KillRange b) => KillRange (Using' a b) Source # | |
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (Using' a b) Source # | |
| Null (Using' n m) Source # | |
| (NFData a, NFData b) => NFData (Using' a b) Source # | |
Defined in Mikan.Syntax.Common | |
| Monoid (Using' n m) Source # | |
| Semigroup (Using' n m) Source # | |
| (Show m, Show n) => Show (Using' n m) Source # | |
| (Eq m, Eq n) => Eq (Using' n m) Source # | |
data WithHiding a Source #
Decorating something with Hiding information.
Constructors
| WithHiding | |
Instances
| Decoration WithHiding Source # | |||||
Defined in Mikan.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> WithHiding a -> m (WithHiding b) Source # distributeF :: Functor m => WithHiding (m a) -> m (WithHiding a) Source # | |||||
| Applicative WithHiding Source # | |||||
Defined in Mikan.Syntax.Common Methods pure :: a -> WithHiding a # (<*>) :: WithHiding (a -> b) -> WithHiding a -> WithHiding b # liftA2 :: (a -> b -> c) -> WithHiding a -> WithHiding b -> WithHiding c # (*>) :: WithHiding a -> WithHiding b -> WithHiding b # (<*) :: WithHiding a -> WithHiding b -> WithHiding a # | |||||
| Functor WithHiding Source # | |||||
Defined in Mikan.Syntax.Common Methods fmap :: (a -> b) -> WithHiding a -> WithHiding b # (<$) :: a -> WithHiding b -> WithHiding a # | |||||
| Foldable WithHiding Source # | |||||
Defined in Mikan.Syntax.Common Methods fold :: Monoid m => WithHiding m -> m # foldMap :: Monoid m => (a -> m) -> WithHiding a -> m # foldMap' :: Monoid m => (a -> m) -> WithHiding a -> m # foldr :: (a -> b -> b) -> b -> WithHiding a -> b # foldr' :: (a -> b -> b) -> b -> WithHiding a -> b # foldl :: (b -> a -> b) -> b -> WithHiding a -> b # foldl' :: (b -> a -> b) -> b -> WithHiding a -> b # foldr1 :: (a -> a -> a) -> WithHiding a -> a # foldl1 :: (a -> a -> a) -> WithHiding a -> a # toList :: WithHiding a -> [a] # null :: WithHiding a -> Bool # length :: WithHiding a -> Int # elem :: Eq a => a -> WithHiding a -> Bool # maximum :: Ord a => WithHiding a -> a # minimum :: Ord a => WithHiding a -> a # sum :: Num a => WithHiding a -> a # product :: Num a => WithHiding a -> a # | |||||
| Traversable WithHiding Source # | |||||
Defined in Mikan.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithHiding a -> f (WithHiding b) # sequenceA :: Applicative f => WithHiding (f a) -> f (WithHiding a) # mapM :: Monad m => (a -> m b) -> WithHiding a -> m (WithHiding b) # sequence :: Monad m => WithHiding (m a) -> m (WithHiding a) # | |||||
| ExprLike a => ExprLike (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (WithHiding a) Source # foldExpr :: FoldExprFn m (WithHiding a) Source # traverseExpr :: TraverseExprFn m (WithHiding a) Source # mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source # | |||||
| LensHiding (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common Methods getHiding :: WithHiding a -> Hiding Source # setHiding :: Hiding -> WithHiding a -> WithHiding a Source # mapHiding :: (Hiding -> Hiding) -> WithHiding a -> WithHiding a Source # | |||||
| Pretty a => Pretty (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common Methods pretty :: WithHiding a -> Doc Source # prettyPrec :: Int -> WithHiding a -> Doc Source # prettyList :: [WithHiding a] -> Doc Source # | |||||
| ExprLike a => ExprLike (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WithHiding a -> WithHiding a Source # foldExpr :: Monoid m => (Expr -> m) -> WithHiding a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WithHiding a -> m (WithHiding a) Source # | |||||
| TermLike a => TermLike (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Internal.Generic Methods traverseTermM :: Monad m => (Term -> m Term) -> WithHiding a -> m (WithHiding a) Source # foldTerm :: Monoid m => (Term -> m) -> WithHiding a -> m Source # | |||||
| HasRange a => HasRange (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common Methods getRange :: WithHiding a -> Range Source # | |||||
| KillRange a => KillRange (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (WithHiding a) Source # | |||||
| SetRange a => SetRange (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common Methods setRange :: Range -> WithHiding a -> WithHiding a Source # | |||||
| ToConcrete a => ToConcrete (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => WithHiding a -> m (ConOfAbs (WithHiding a)) Source # bindToConcrete :: MonadToConcrete m => WithHiding a -> (ConOfAbs (WithHiding a) -> m b) -> m b Source # | |||||
| ToAbstract c => ToAbstract (WithHiding c) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: WithHiding c -> ScopeM (AbsOfCon (WithHiding c)) Source # | |||||
| PrettyTCM a => PrettyTCM (WithHiding a) Source # | |||||
Defined in Mikan.TypeChecking.Pretty Methods prettyTCM :: MonadPretty m => WithHiding a -> m Doc Source # | |||||
| Normalise t => Normalise (WithHiding t) Source # | |||||
Defined in Mikan.TypeChecking.Reduce Methods normalise' :: WithHiding t -> ReduceM (WithHiding t) Source # | |||||
| EmbPrj a => EmbPrj (WithHiding a) Source # | |||||
| Subst a => Subst (WithHiding a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute Associated Types
Methods applySubst :: Substitution' (SubstArg (WithHiding a)) -> WithHiding a -> WithHiding a Source # | |||||
| NFData a => NFData (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: WithHiding a -> () # | |||||
| Show a => Show (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> WithHiding a -> ShowS # show :: WithHiding a -> String # showList :: [WithHiding a] -> ShowS # | |||||
| Eq a => Eq (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Ord a => Ord (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Common Methods compare :: WithHiding a -> WithHiding a -> Ordering # (<) :: WithHiding a -> WithHiding a -> Bool # (<=) :: WithHiding a -> WithHiding a -> Bool # (>) :: WithHiding a -> WithHiding a -> Bool # (>=) :: WithHiding a -> WithHiding a -> Bool # max :: WithHiding a -> WithHiding a -> WithHiding a # min :: WithHiding a -> WithHiding a -> WithHiding a # | |||||
| AddContext (List1 (WithHiding Name), Dom Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (WithHiding Name), Dom Type) -> m a -> m a Source # | |||||
| AddContext ([WithHiding Name], Dom Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([WithHiding Name], Dom Type) -> m a -> m a Source # | |||||
| type ConOfAbs (WithHiding a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
| type AbsOfCon (WithHiding c) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
| type SubstArg (WithHiding a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute | |||||
data WithOrigin a Source #
Decorating something with Origin information.
Constructors
| WithOrigin | |
Instances
| MapNamedArgPattern NAP Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern | |||||
| Decoration WithOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods traverseF :: Functor m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) Source # distributeF :: Functor m => WithOrigin (m a) -> m (WithOrigin a) Source # | |||||
| Functor WithOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods fmap :: (a -> b) -> WithOrigin a -> WithOrigin b # (<$) :: a -> WithOrigin b -> WithOrigin a # | |||||
| Foldable WithOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods fold :: Monoid m => WithOrigin m -> m # foldMap :: Monoid m => (a -> m) -> WithOrigin a -> m # foldMap' :: Monoid m => (a -> m) -> WithOrigin a -> m # foldr :: (a -> b -> b) -> b -> WithOrigin a -> b # foldr' :: (a -> b -> b) -> b -> WithOrigin a -> b # foldl :: (b -> a -> b) -> b -> WithOrigin a -> b # foldl' :: (b -> a -> b) -> b -> WithOrigin a -> b # foldr1 :: (a -> a -> a) -> WithOrigin a -> a # foldl1 :: (a -> a -> a) -> WithOrigin a -> a # toList :: WithOrigin a -> [a] # null :: WithOrigin a -> Bool # length :: WithOrigin a -> Int # elem :: Eq a => a -> WithOrigin a -> Bool # maximum :: Ord a => WithOrigin a -> a # minimum :: Ord a => WithOrigin a -> a # sum :: Num a => WithOrigin a -> a # product :: Num a => WithOrigin a -> a # | |||||
| Traversable WithOrigin Source # | |||||
Defined in Mikan.Syntax.Common Methods traverse :: Applicative f => (a -> f b) -> WithOrigin a -> f (WithOrigin b) # sequenceA :: Applicative f => WithOrigin (f a) -> f (WithOrigin a) # mapM :: Monad m => (a -> m b) -> WithOrigin a -> m (WithOrigin b) # sequence :: Monad m => WithOrigin (m a) -> m (WithOrigin a) # | |||||
| MapNamedArgPattern a (NamedArg (Pattern' a)) Source # | Modify the content of Note: the | ||||
| LensOrigin (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common Methods getOrigin :: WithOrigin a -> Origin Source # setOrigin :: Origin -> WithOrigin a -> WithOrigin a Source # mapOrigin :: (Origin -> Origin) -> WithOrigin a -> WithOrigin a Source # | |||||
| Pretty e => Pretty (Named_ e) Source # | |||||
| Pretty a => Pretty (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common Methods pretty :: WithOrigin a -> Doc Source # prettyPrec :: Int -> WithOrigin a -> Doc Source # prettyList :: [WithOrigin a] -> Doc Source # | |||||
| IsNoName a => IsNoName (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Concrete.Name Methods isNoName :: WithOrigin a -> Bool Source # | |||||
| HasDefP a => HasDefP (Named_ a) Source # | |||||
| PatternVars (NamedArg (Pattern' a)) Source # | |||||
Defined in Mikan.Syntax.Internal.Pattern Associated Types
| |||||
| HasRange a => HasRange (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common Methods getRange :: WithOrigin a -> Range Source # | |||||
| KillRange a => KillRange (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common Methods killRange :: KillRangeT (WithOrigin a) Source # | |||||
| SetRange a => SetRange (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common Methods setRange :: Range -> WithOrigin a -> WithOrigin a Source # | |||||
| PrettyTCM (NamedArg Expr) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM (NamedArg Term) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| PrettyTCM (Named_ Term) Source # | |||||
Defined in Mikan.TypeChecking.Pretty | |||||
| NormaliseProjP a => NormaliseProjP (Named_ a) Source # | |||||
Defined in Mikan.TypeChecking.Records Methods normaliseProjP :: HasConstInfo m => Named_ a -> m (Named_ a) Source # | |||||
| EmbPrj a => EmbPrj (WithOrigin a) Source # | |||||
| Apply [NamedArg (Pattern' a)] Source # | Make sure we only drop variable patterns. | ||||
| DeBruijn a => DeBruijn (Named_ a) Source # | |||||
Defined in Mikan.TypeChecking.Substitute.DeBruijn | |||||
| IApplyVars p => IApplyVars (NamedArg p) Source # | |||||
Defined in Mikan.TypeChecking.Telescope.Path Methods iApplyVars :: NamedArg p -> [Int] Source # | |||||
| NFData a => NFData (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common Methods rnf :: WithOrigin a -> () # | |||||
| Show a => Show (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common Methods showsPrec :: Int -> WithOrigin a -> ShowS # show :: WithOrigin a -> String # showList :: [WithOrigin a] -> ShowS # | |||||
| Eq a => Eq (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common | |||||
| Ord a => Ord (WithOrigin a) Source # | |||||
Defined in Mikan.Syntax.Common Methods compare :: WithOrigin a -> WithOrigin a -> Ordering # (<) :: WithOrigin a -> WithOrigin a -> Bool # (<=) :: WithOrigin a -> WithOrigin a -> Bool # (>) :: WithOrigin a -> WithOrigin a -> Bool # (>=) :: WithOrigin a -> WithOrigin a -> Bool # max :: WithOrigin a -> WithOrigin a -> WithOrigin a # min :: WithOrigin a -> WithOrigin a -> WithOrigin a # | |||||
| AddContext (List1 (NamedArg Name), Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => (List1 (NamedArg Name), Type) -> m a -> m a Source # | |||||
| AddContext ([NamedArg Name], Type) Source # | |||||
Defined in Mikan.TypeChecking.Monad.Context Methods addContext :: MonadAddContext m => ([NamedArg Name], Type) -> m a -> m a Source # | |||||
| type PatternVarOut (NamedArg (Pattern' a)) Source # | |||||
Defined in Mikan.Syntax.Internal.Pattern | |||||
Constructors
| Inductive | |
| CoInductive |
Instances
| PatternMatchingAllowed Induction Source # | |
Defined in Mikan.Syntax.Common Methods | |
| Pretty Induction Source # | |
| HasRange Induction Source # | |
| KillRange Induction Source # | |
Defined in Mikan.Syntax.Common Methods | |
| EmbPrj Induction Source # | |
| NFData Induction Source # | |
Defined in Mikan.Syntax.Common.Aspect | |
| Generic Induction Source # | |
Defined in Mikan.Syntax.Common.Aspect | |
| Show Induction Source # | |
| Eq Induction Source # | |
| Ord Induction Source # | |
| type Rep Induction Source # | |