| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Mikan.Syntax.Concrete
Contents
Description
The concrete syntax is a raw representation of the program text without any desugaring at all. This is what the parser produces. The idea is that if we figure out how to keep the concrete syntax around, it can be printed exactly as the user wrote it.
Synopsis
- data Expr
- = Ident QName
- | Lit Range Literal
- | QuestionMark Range (Maybe Nat)
- | Underscore Range (Maybe ShortText)
- | RawApp Range (List2 Expr)
- | App Range Expr (NamedArg Expr)
- | OpApp Range QName (Set1 Name) OpAppArgs
- | WithApp Range Expr (List1 Expr)
- | HiddenArg Range (Named_ Expr)
- | InstanceArg Range (Named_ Expr)
- | Lam Range (List1 LamBinding) Expr
- | AbsurdLam Range Hiding
- | ExtendedLam Range (List1 LamClause)
- | Fun Range Expr Expr
- | Pi Telescope1 Expr
- | Rec KwRange Range RecordAssignments
- | RecUpdate KwRange Range Expr [FieldAssignment]
- | RecWhere KwRange Range [Declaration]
- | RecUpdateWhere KwRange Range Expr [Declaration]
- | Let Range (List1 Declaration) (Maybe Expr)
- | Paren Range Expr
- | IdiomBrackets Range (Maybe QName) [Expr]
- | DoBlock KwRange (Maybe QName) (List1 DoStmt)
- | Absurd Range
- | As Range Name Expr
- | Dot KwRange Expr
- | Quote Range
- | QuoteTerm Range
- | Tactic Range Expr
- | Unquote Range
- | DontCare Expr
- | Equal Range Expr Expr
- | Ellipsis Range
- | KnownIdent Aspects QName
- | KnownOpApp Aspects Range QName (Set1 Name) OpAppArgs
- | Highlighted Aspects Expr
- | Generalized Expr
- data OpApp e
- = SyntaxBindingLambda Range (List1 LamBinding) e
- | Ordinary e
- fromOrdinary :: e -> OpApp e -> e
- type OpAppArgs = OpAppArgs' Expr
- type OpAppArgs' e = List1 (NamedArg (MaybePlaceholder (OpApp e)))
- type OpAppArgs0 e = [NamedArg (MaybePlaceholder (OpApp e))]
- module Mikan.Syntax.Concrete.Name
- data AppView = AppView Expr [NamedArg Expr]
- appView :: Expr -> AppView
- unAppView :: AppView -> Expr
- toNamedArg :: Expr -> NamedArg Expr
- unNamedArg :: NamedArg Expr -> Expr
- rawApp :: List1 Expr -> Expr
- rawAppP :: List1 Pattern -> Pattern
- isSingleIdentifierP :: Pattern -> Maybe Name
- removeParenP :: Pattern -> Pattern
- isPattern :: Expr -> Maybe Pattern
- isAbsurdP :: Pattern -> Maybe (Range, Hiding)
- isBinderP :: Pattern -> Maybe Binder
- data PossiblyProjectionPattern
- observeHiding :: Expr -> WithHiding Expr
- observeModifiers :: Expr -> Arg Expr
- exprToPatternWithHoles :: Expr -> Pattern
- returnExpr :: Expr -> Maybe Expr
- data Binder' a = Binder {}
- type Binder = Binder' BoundName
- mkBinder_ :: Name -> Binder
- mkBinder :: a -> Binder' a
- type LamBinding = LamBinding' TypedBinding
- data LamBinding' a
- = DomainFree (NamedArg Binder)
- | DomainFull a
- type DefParameters = [WithHiding (Named_ Name)]
- parametersToDefParameters :: Parameters -> DefParameters
- defParametersToParameters :: DefParameters -> Parameters
- type TypedBinding = TypedBinding' Expr
- data TypedBinding' e
- type RecordAssignment = Either FieldAssignment ModuleAssignment
- type RecordAssignments = [RecordAssignment]
- type FieldAssignment = FieldAssignment' Expr
- data FieldAssignment' a = FieldAssignment {
- _nameFieldA :: Name
- _exprFieldA :: a
- nameFieldA :: forall a f. Functor f => (Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a)
- exprFieldA :: forall a f. Functor f => (a -> f a) -> FieldAssignment' a -> f (FieldAssignment' a)
- data ModuleAssignment = ModuleAssignment {}
- data BoundName = BName {}
- mkBoundName_ :: Name -> BoundName
- mkBoundName :: Name -> Fixity' -> BoundName
- type TacticAttribute = TacticAttribute' Expr
- newtype TacticAttribute' a = TacticAttribute {
- theTacticAttribute :: Maybe (Ranged a)
- type Telescope = [TypedBinding]
- type Telescope1 = List1 TypedBinding
- type Parameters = [LamBinding]
- parametersToTelescope :: Range -> Parameters -> Telescope
- makePi :: Telescope -> Expr -> Expr
- mkLam :: Range -> [LamBinding] -> Expr -> Expr
- mkLet :: Range -> [Declaration] -> Expr -> Expr
- mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e)
- data Declaration
- = TypeSig ArgInfo TacticAttribute Name Expr
- | FieldSig IsInstance TacticAttribute Name (Arg Expr)
- | Generalize KwRange [TypeSignature]
- | Field KwRange [FieldSignature]
- | FunClause LHS RHS WhereClause Catchall
- | DataSig Range Name Parameters Expr
- | Data Range Name Parameters Expr [TypeSignatureOrInstanceBlock]
- | DataDef Range Name Parameters [TypeSignatureOrInstanceBlock]
- | RecordSig Range Name Parameters Expr
- | RecordDef Range Name [RecordDirective] Parameters [Declaration]
- | Record Range Name [RecordDirective] Parameters Expr [Declaration]
- | Infix Fixity (List1 Name)
- | Syntax Name Notation
- | PatternSyn Range Name [WithHiding Name] Pattern
- | Mutual KwRange [Declaration]
- | InterleavedMutual KwRange [Declaration]
- | Abstract KwRange [Declaration]
- | Private KwRange Origin [Declaration]
- | InstanceB KwRange [Declaration]
- | LoneConstructor KwRange [Declaration]
- | Macro KwRange [Declaration]
- | Postulate KwRange [TypeSignatureOrInstanceBlock]
- | Primitive KwRange [TypeSignature]
- | Open KwRange QName ImportDirective
- | Import OpenShortHand KwRange QName (Either AsName RawOpenArgs) ImportDirective
- | ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective
- | Module Range QName Telescope [Declaration]
- | UnquoteDecl Range [Name] Expr
- | UnquoteDef Range [Name] Expr
- | UnquoteData Range Name [Name] Expr
- | Pragma Pragma
- | Opaque KwRange [Declaration]
- | Unfolding KwRange [QName]
- isPragma :: CMaybe Pragma m => Declaration -> m
- data RecordDirective
- type RecordDirectives = RecordDirectives' (Maybe (Name, IsInstance))
- data ModuleApplication
- type TypeSignature = Declaration
- type TypeSignatureOrInstanceBlock = Declaration
- type ImportDirective = ImportDirective' Name Name
- type Using = Using' Name Name
- type ImportedName = ImportedName' Name Name
- type Renaming = Renaming' Name Name
- type RenamingDirective = RenamingDirective' Name Name
- type HidingDirective = HidingDirective' Name Name
- data AsName' a = AsName {}
- type AsName = AsName' Name
- type RawOpenArgs = [Expr]
- data OpenShortHand
- type RewriteEqn = RewriteEqn' () Name Pattern Expr
- type WithExpr = Named Name (Arg Expr)
- data LHS = LHS {}
- data Pattern
- = IdentP Bool QName
- | QuoteP Range
- | AppP Pattern (NamedArg Pattern)
- | RawAppP Range (List2 Pattern)
- | OpAppP Range QName (Set1 Name) (List1 (NamedArg Pattern))
- | HiddenP Range (Named_ Pattern)
- | InstanceP Range (Named_ Pattern)
- | ParenP Range Pattern
- | WildP Range
- | AbsurdP Range
- | AsP Range Name Pattern
- | DotP KwRange Range !PossiblyProjectionPattern Expr
- | LitP Range Literal
- | RecP KwRange Range [FieldAssignment' Pattern]
- | EqualP Range (List1 (Expr, Expr))
- | EllipsisP Range (Maybe Pattern)
- | WithP Range Pattern
- data LHSCore
- = LHSHead {
- lhsDefName :: QName
- lhsPats :: [NamedArg Pattern]
- | LHSProj { }
- | LHSWith { }
- | LHSEllipsis { }
- = LHSHead {
- data LamClause = LamClause {}
- type RHS = RHS' Expr
- data RHS' e
- type WhereClause = WhereClause' [Declaration]
- data WhereClause' decls
- = NoWhere
- | LocalWhere Range decls
- | NonLocalWhere Range Name Access decls
- data WhereClause_
- data ExprWhere = ExprWhere Expr WhereClause
- whereClause_ :: WhereClause' a -> WhereClause_
- data DoStmt
- data Pragma
- = OptionsPragma Range [ShortText]
- | BuiltinPragma Range RString QName
- | ForeignPragma Range (Ranged BackendName) ShortText
- | CompilePragma Range (Ranged BackendName) QName ShortText
- | InlinePragma Range Bool QName
- | ImpossiblePragma Range [ShortText]
- | EtaPragma Range QName
- | WarningOnUsage Range QName ShortText
- | WarningOnImport Range ShortText
- | InjectivePragma Range QName
- | InjectiveForInferencePragma Range QName
- | DisplayPragma Range Pattern Expr
- | CatchallPragma Range
- | TerminationCheckPragma Range TerminationCheck
- | NoCoverageCheckPragma Range
- | NoPositivityCheckPragma Range
- | PolarityPragma Range Name [Ranged Occurrence]
- | NoUniverseCheckPragma Range
- | NotProjectionLikePragma Range QName
- | OverlapPragma Range [QName] OverlapMode
- data Module = Mod {
- modName :: QName
- modPragmas :: [Pragma]
- modDecls :: [Declaration]
- data ThingWithFixity x = ThingWithFixity x Fixity'
- type HoleContent = HoleContent' () Name Pattern Expr
- data HoleContent' qn nm p e
- = HoleContentExpr e
- | HoleContentRewrite [RewriteEqn' qn nm p e]
- spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])
- ungatherRecordDirectives :: RecordDirectives -> [RecordDirective]
Expressions
Concrete expressions. Should represent exactly what the user wrote.
Constructors
| Ident QName | ex: |
| Lit Range Literal | ex: |
| QuestionMark Range (Maybe Nat) | ex: |
| Underscore Range (Maybe ShortText) | ex: |
| RawApp Range (List2 Expr) | before parsing operators |
| App Range Expr (NamedArg Expr) | ex: |
| OpApp Range QName (Set1 Name) OpAppArgs | ex: |
| WithApp Range Expr (List1 Expr) | ex: |
| HiddenArg Range (Named_ Expr) | ex: |
| InstanceArg Range (Named_ Expr) | ex: |
| Lam Range (List1 LamBinding) Expr | ex: |
| AbsurdLam Range Hiding | ex: |
| ExtendedLam Range (List1 LamClause) | ex: |
| Fun Range Expr Expr | ex: |
| Pi Telescope1 Expr | ex: |
| Rec KwRange Range RecordAssignments | ex: |
| RecUpdate KwRange Range Expr [FieldAssignment] | ex: |
| RecWhere KwRange Range [Declaration] | ex: |
| RecUpdateWhere KwRange Range Expr [Declaration] | ex: |
| Let Range (List1 Declaration) (Maybe Expr) | ex: |
| Paren Range Expr | ex: |
| IdiomBrackets Range (Maybe QName) [Expr] | ex: |
| DoBlock KwRange (Maybe QName) (List1 DoStmt) | ex: |
| Absurd Range | ex: |
| As Range Name Expr | ex: |
| Dot KwRange Expr | ex: |
| Quote Range | ex: |
| QuoteTerm Range | ex: |
| Tactic Range Expr | ex: |
| Unquote Range | ex: |
| DontCare Expr | to print irrelevant things |
| Equal Range Expr Expr | ex: |
| Ellipsis Range |
|
| KnownIdent Aspects QName | An identifier coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing). |
| KnownOpApp Aspects Range QName (Set1 Name) OpAppArgs | An operator application coming from abstract syntax, for which we know a precise syntactic highlighting class (used in printing). |
| Highlighted Aspects Expr | An arbitrary expression bundled with highlighting information from abstract (or internal) syntax |
| Generalized Expr |
Instances
Constructors
| SyntaxBindingLambda Range (List1 LamBinding) e | An abstraction inside a special syntax declaration (see Issue 358 why we introduce this). |
| Ordinary e |
Instances
| Functor OpApp Source # | |
| Foldable OpApp Source # | |
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => OpApp m -> m # foldMap :: Monoid m => (a -> m) -> OpApp a -> m # foldMap' :: Monoid m => (a -> m) -> OpApp a -> m # foldr :: (a -> b -> b) -> b -> OpApp a -> b # foldr' :: (a -> b -> b) -> b -> OpApp a -> b # foldl :: (b -> a -> b) -> b -> OpApp a -> b # foldl' :: (b -> a -> b) -> b -> OpApp a -> b # foldr1 :: (a -> a -> a) -> OpApp a -> a # foldl1 :: (a -> a -> a) -> OpApp a -> a # elem :: Eq a => a -> OpApp a -> Bool # maximum :: Ord a => OpApp a -> a # minimum :: Ord a => OpApp a -> a # | |
| Traversable OpApp Source # | |
| Pretty (OpApp Expr) Source # | |
| ExprLike a => ExprLike (OpApp a) Source # | |
| HasRange e => HasRange (OpApp e) Source # | |
| KillRange e => KillRange (OpApp e) Source # | |
Defined in Mikan.Syntax.Concrete Methods killRange :: KillRangeT (OpApp e) Source # | |
| NFData a => NFData (OpApp a) Source # | Ranges are not forced. |
Defined in Mikan.Syntax.Concrete | |
| Show a => Show (OpApp a) Source # | |
| Eq e => Eq (OpApp e) Source # | |
fromOrdinary :: e -> OpApp e -> e Source #
type OpAppArgs = OpAppArgs' Expr Source #
type OpAppArgs' e = List1 (NamedArg (MaybePlaceholder (OpApp e))) Source #
type OpAppArgs0 e = [NamedArg (MaybePlaceholder (OpApp e))] Source #
module Mikan.Syntax.Concrete.Name
removeParenP :: Pattern -> Pattern Source #
isPattern :: Expr -> Maybe Pattern Source #
Turn an expression into a pattern. Fails if the expression is not a valid pattern.
data PossiblyProjectionPattern Source #
Can a dot pattern be interpreted as projection pattern?
Constructors
| CouldBeProjectionPattern | Yes. |
| CannotBeProjectionPattern | No. |
Instances
| Show PossiblyProjectionPattern Source # | |
Defined in Mikan.Syntax.Concrete Methods showsPrec :: Int -> PossiblyProjectionPattern -> ShowS # show :: PossiblyProjectionPattern -> String # showList :: [PossiblyProjectionPattern] -> ShowS # | |
| Eq PossiblyProjectionPattern Source # | |
Defined in Mikan.Syntax.Concrete Methods (==) :: PossiblyProjectionPattern -> PossiblyProjectionPattern -> Bool # (/=) :: PossiblyProjectionPattern -> PossiblyProjectionPattern -> Bool # | |
observeHiding :: Expr -> WithHiding Expr Source #
Observe the hiding status of an expression
exprToPatternWithHoles :: Expr -> Pattern Source #
Turn an expression into a pattern, turning non-pattern subexpressions into WildP.
Bindings
A Binder x@p, the pattern is optional
Constructors
| Binder | |
Fields | |
Instances
| HasRange Binder Source # | |
| KillRange Binder Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| NFData Binder Source # | |
Defined in Mikan.Syntax.Concrete | |
| Functor Binder' Source # | |
| Foldable Binder' Source # | |
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => Binder' m -> m # foldMap :: Monoid m => (a -> m) -> Binder' a -> m # foldMap' :: Monoid m => (a -> m) -> Binder' a -> m # foldr :: (a -> b -> b) -> b -> Binder' a -> b # foldr' :: (a -> b -> b) -> b -> Binder' a -> b # foldl :: (b -> a -> b) -> b -> Binder' a -> b # foldl' :: (b -> a -> b) -> b -> Binder' a -> b # foldr1 :: (a -> a -> a) -> Binder' a -> a # foldl1 :: (a -> a -> a) -> Binder' a -> a # elem :: Eq a => a -> Binder' a -> Bool # maximum :: Ord a => Binder' a -> a # minimum :: Ord a => Binder' a -> a # | |
| Traversable Binder' Source # | |
| Pretty a => Pretty (Binder' a) Source # | |
| Show a => Show (Binder' a) Source # | |
| Eq a => Eq (Binder' a) Source # | |
type LamBinding = LamBinding' TypedBinding Source #
A lambda binding is either untyped (domain free) or typed (TypedBinding).
data LamBinding' a Source #
Constructors
| DomainFree (NamedArg Binder) | . |
| DomainFull a | . |
Instances
| LensHiding LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getHiding :: LamBinding -> Hiding Source # setHiding :: Hiding -> LamBinding -> LamBinding Source # mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding Source # | |||||
| Pretty LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source # | |||||
| ExprLike LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source # | |||||
| HasRange LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: LamBinding -> Range Source # | |||||
| KillRange LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| ToAbstract LamBinding Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source # | |||||
| Functor LamBinding' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fmap :: (a -> b) -> LamBinding' a -> LamBinding' b # (<$) :: a -> LamBinding' b -> LamBinding' a # | |||||
| Foldable LamBinding' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => LamBinding' m -> m # foldMap :: Monoid m => (a -> m) -> LamBinding' a -> m # foldMap' :: Monoid m => (a -> m) -> LamBinding' a -> m # foldr :: (a -> b -> b) -> b -> LamBinding' a -> b # foldr' :: (a -> b -> b) -> b -> LamBinding' a -> b # foldl :: (b -> a -> b) -> b -> LamBinding' a -> b # foldl' :: (b -> a -> b) -> b -> LamBinding' a -> b # foldr1 :: (a -> a -> a) -> LamBinding' a -> a # foldl1 :: (a -> a -> a) -> LamBinding' a -> a # toList :: LamBinding' a -> [a] # null :: LamBinding' a -> Bool # length :: LamBinding' a -> Int # elem :: Eq a => a -> LamBinding' a -> Bool # maximum :: Ord a => LamBinding' a -> a # minimum :: Ord a => LamBinding' a -> a # sum :: Num a => LamBinding' a -> a # product :: Num a => LamBinding' a -> a # | |||||
| Traversable LamBinding' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> LamBinding' a -> f (LamBinding' b) # sequenceA :: Applicative f => LamBinding' (f a) -> f (LamBinding' a) # mapM :: Monad m => (a -> m b) -> LamBinding' a -> m (LamBinding' b) # sequence :: Monad m => LamBinding' (m a) -> m (LamBinding' a) # | |||||
| Show LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS # | |||||
| NFData a => NFData (LamBinding' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods rnf :: LamBinding' a -> () # | |||||
| Eq a => Eq (LamBinding' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods (==) :: LamBinding' a -> LamBinding' a -> Bool # (/=) :: LamBinding' a -> LamBinding' a -> Bool # | |||||
| type AbsOfCon LamBinding Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
type DefParameters = [WithHiding (Named_ Name)] Source #
Parameters supplied to data and record definitions (as opposed to their signatures)
are stripped of their type information.
They also cannot contain let or pattern bindings or tactic attributes.
parametersToDefParameters :: Parameters -> DefParameters Source #
Drop type annotations from bindings. Also drop let, patterns, fixity, and tactics, but those should not be present in the first place when using this function, because all such cannot occur in data and record parameters.
type TypedBinding = TypedBinding' Expr Source #
A typed binding.
data TypedBinding' e Source #
Constructors
| TBind Range (List1 (NamedArg Binder)) e | Binding |
| TLet Range (List1 Declaration) | Let binding |
Instances
| 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 # | |||||
| Pretty LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: LamBinding -> Doc Source # prettyPrec :: Int -> LamBinding -> Doc Source # prettyList :: [LamBinding] -> Doc Source # | |||||
| Pretty TypedBinding Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: TypedBinding -> Doc Source # prettyPrec :: Int -> TypedBinding -> Doc Source # prettyList :: [TypedBinding] -> Doc Source # | |||||
| ExprLike LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding Source # foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding Source # | |||||
| HasRange LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: LamBinding -> Range Source # | |||||
| HasRange TypedBinding Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: TypedBinding -> Range Source # | |||||
| KillRange LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| KillRange TypedBinding Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| SetRange TypedBinding Source # | |||||
Defined in Mikan.Syntax.Concrete Methods setRange :: Range -> TypedBinding -> TypedBinding Source # | |||||
| ToAbstract LamBinding Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: LamBinding -> ScopeM (AbsOfCon LamBinding) Source # | |||||
| ToAbstract TypedBinding Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: TypedBinding -> ScopeM (AbsOfCon TypedBinding) Source # | |||||
| Functor TypedBinding' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fmap :: (a -> b) -> TypedBinding' a -> TypedBinding' b # (<$) :: a -> TypedBinding' b -> TypedBinding' a # | |||||
| Foldable TypedBinding' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => TypedBinding' m -> m # foldMap :: Monoid m => (a -> m) -> TypedBinding' a -> m # foldMap' :: Monoid m => (a -> m) -> TypedBinding' a -> m # foldr :: (a -> b -> b) -> b -> TypedBinding' a -> b # foldr' :: (a -> b -> b) -> b -> TypedBinding' a -> b # foldl :: (b -> a -> b) -> b -> TypedBinding' a -> b # foldl' :: (b -> a -> b) -> b -> TypedBinding' a -> b # foldr1 :: (a -> a -> a) -> TypedBinding' a -> a # foldl1 :: (a -> a -> a) -> TypedBinding' a -> a # toList :: TypedBinding' a -> [a] # null :: TypedBinding' a -> Bool # length :: TypedBinding' a -> Int # elem :: Eq a => a -> TypedBinding' a -> Bool # maximum :: Ord a => TypedBinding' a -> a # minimum :: Ord a => TypedBinding' a -> a # sum :: Num a => TypedBinding' a -> a # product :: Num a => TypedBinding' a -> a # | |||||
| Traversable TypedBinding' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> TypedBinding' a -> f (TypedBinding' b) # sequenceA :: Applicative f => TypedBinding' (f a) -> f (TypedBinding' a) # mapM :: Monad m => (a -> m b) -> TypedBinding' a -> m (TypedBinding' b) # sequence :: Monad m => TypedBinding' (m a) -> m (TypedBinding' a) # | |||||
| Show LamBinding Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods showsPrec :: Int -> LamBinding -> ShowS # show :: LamBinding -> String # showList :: [LamBinding] -> ShowS # | |||||
| Show TypedBinding Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods showsPrec :: Int -> TypedBinding -> ShowS # show :: TypedBinding -> String # showList :: [TypedBinding] -> ShowS # | |||||
| ExprLike a => ExprLike (TypedBinding' a) Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a Source # foldExpr :: Monoid m => (Expr -> m) -> TypedBinding' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding' a -> m (TypedBinding' a) Source # | |||||
| NFData a => NFData (TypedBinding' a) Source # | Ranges are not forced. | ||||
Defined in Mikan.Syntax.Concrete Methods rnf :: TypedBinding' a -> () # | |||||
| Eq e => Eq (TypedBinding' e) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods (==) :: TypedBinding' e -> TypedBinding' e -> Bool # (/=) :: TypedBinding' e -> TypedBinding' e -> Bool # | |||||
| type AbsOfCon LamBinding Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
| type AbsOfCon TypedBinding Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
type RecordAssignments = [RecordAssignment] Source #
type FieldAssignment = FieldAssignment' Expr Source #
data FieldAssignment' a Source #
Constructors
| FieldAssignment | |
Fields
| |
Instances
| ExprLike FieldAssignment Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment Source # | |||||
| Functor FieldAssignment' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fmap :: (a -> b) -> FieldAssignment' a -> FieldAssignment' b # (<$) :: a -> FieldAssignment' b -> FieldAssignment' a # | |||||
| Foldable FieldAssignment' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => FieldAssignment' m -> m # foldMap :: Monoid m => (a -> m) -> FieldAssignment' a -> m # foldMap' :: Monoid m => (a -> m) -> FieldAssignment' a -> m # foldr :: (a -> b -> b) -> b -> FieldAssignment' a -> b # foldr' :: (a -> b -> b) -> b -> FieldAssignment' a -> b # foldl :: (b -> a -> b) -> b -> FieldAssignment' a -> b # foldl' :: (b -> a -> b) -> b -> FieldAssignment' a -> b # foldr1 :: (a -> a -> a) -> FieldAssignment' a -> a # foldl1 :: (a -> a -> a) -> FieldAssignment' a -> a # toList :: FieldAssignment' a -> [a] # null :: FieldAssignment' a -> Bool # length :: FieldAssignment' a -> Int # elem :: Eq a => a -> FieldAssignment' a -> Bool # maximum :: Ord a => FieldAssignment' a -> a # minimum :: Ord a => FieldAssignment' a -> a # sum :: Num a => FieldAssignment' a -> a # product :: Num a => FieldAssignment' a -> a # | |||||
| Traversable FieldAssignment' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> FieldAssignment' a -> f (FieldAssignment' b) # sequenceA :: Applicative f => FieldAssignment' (f a) -> f (FieldAssignment' a) # mapM :: Monad m => (a -> m b) -> FieldAssignment' a -> m (FieldAssignment' b) # sequence :: Monad m => FieldAssignment' (m a) -> m (FieldAssignment' a) # | |||||
| SubstExpr a => SubstExpr (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Abstract Methods substExpr :: [(Name, Expr)] -> FieldAssignment' a -> FieldAssignment' a Source # | |||||
| APatternLike a => APatternLike (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern Associated Types
Methods foldrAPattern :: Monoid m => (Pattern' (ADotT (FieldAssignment' a)) -> m -> m) -> FieldAssignment' a -> m Source # traverseAPatternM :: Monad m => (Pattern' (ADotT (FieldAssignment' a)) -> m (Pattern' (ADotT (FieldAssignment' a)))) -> (Pattern' (ADotT (FieldAssignment' a)) -> m (Pattern' (ADotT (FieldAssignment' a)))) -> FieldAssignment' a -> m (FieldAssignment' a) Source # | |||||
| MapNamedArgPattern a => MapNamedArgPattern (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern Methods mapNamedArgPattern :: (NAP -> NAP) -> FieldAssignment' a -> FieldAssignment' a Source # | |||||
| DeclaredNames a => DeclaredNames (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods declaredNames :: Collection KName m => FieldAssignment' a -> m Source # | |||||
| ExprLike a => ExprLike (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (FieldAssignment' a) Source # foldExpr :: FoldExprFn m (FieldAssignment' a) Source # traverseExpr :: TraverseExprFn m (FieldAssignment' a) Source # mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a Source # | |||||
| Pretty a => Pretty (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: FieldAssignment' a -> Doc Source # prettyPrec :: Int -> FieldAssignment' a -> Doc Source # prettyList :: [FieldAssignment' a] -> Doc Source # | |||||
| CPatternLike p => CPatternLike (FieldAssignment' p) Source # | |||||
Defined in Mikan.Syntax.Concrete.Pattern Methods foldrCPattern :: Monoid m => (Pattern -> m -> m) -> FieldAssignment' p -> m Source # traverseCPatternA :: Applicative m => (Pattern -> m Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source # traverseCPatternM :: Monad m => (Pattern -> m Pattern) -> (Pattern -> m Pattern) -> FieldAssignment' p -> m (FieldAssignment' p) Source # | |||||
| NamesIn a => NamesIn (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Internal.Names Methods namesAndMetasIn' :: Monoid m => (Either QName MetaId -> m) -> FieldAssignment' a -> m Source # | |||||
| HasRange a => HasRange (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: FieldAssignment' a -> Range Source # | |||||
| KillRange a => KillRange (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods killRange :: KillRangeT (FieldAssignment' a) Source # | |||||
| ToConcrete a => ToConcrete (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => FieldAssignment' a -> m (ConOfAbs (FieldAssignment' a)) Source # bindToConcrete :: MonadToConcrete m => FieldAssignment' a -> (ConOfAbs (FieldAssignment' a) -> m b) -> m b Source # | |||||
| ToAbstract c => ToAbstract (FieldAssignment' c) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: FieldAssignment' c -> ScopeM (AbsOfCon (FieldAssignment' c)) Source # | |||||
| ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a) Source # | |||||
Defined in Mikan.TypeChecking.Patterns.Abstract Methods expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a) Source # | |||||
| EmbPrj a => EmbPrj (FieldAssignment' a) Source # | |||||
| NFData a => NFData (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods rnf :: FieldAssignment' a -> () # | |||||
| Show a => Show (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods showsPrec :: Int -> FieldAssignment' a -> ShowS # show :: FieldAssignment' a -> String # showList :: [FieldAssignment' a] -> ShowS # | |||||
| Eq a => Eq (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods (==) :: FieldAssignment' a -> FieldAssignment' a -> Bool # (/=) :: FieldAssignment' a -> FieldAssignment' a -> Bool # | |||||
| PatternToExpr p e => PatternToExpr (FieldAssignment' p) (FieldAssignment' e) Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern Methods patToExpr :: FieldAssignment' p -> Reader Hiding (FieldAssignment' e) Source # | |||||
| type ADotT (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Pattern | |||||
| type ConOfAbs (FieldAssignment' a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
| type AbsOfCon (FieldAssignment' c) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
nameFieldA :: forall a f. Functor f => (Name -> f Name) -> FieldAssignment' a -> f (FieldAssignment' a) Source #
exprFieldA :: forall a f. Functor f => (a -> f a) -> FieldAssignment' a -> f (FieldAssignment' a) Source #
data ModuleAssignment Source #
Constructors
| ModuleAssignment | |
Fields
| |
Instances
| Pretty ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: ModuleAssignment -> Doc Source # prettyPrec :: Int -> ModuleAssignment -> Doc Source # prettyList :: [ModuleAssignment] -> Doc Source # | |||||
| ExprLike ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleAssignment -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment Source # | |||||
| HasRange ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: ModuleAssignment -> Range Source # | |||||
| KillRange ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| ToAbstract ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: ModuleAssignment -> ScopeM (AbsOfCon ModuleAssignment) Source # | |||||
| NFData ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Concrete Methods rnf :: ModuleAssignment -> () # | |||||
| Show ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ModuleAssignment -> ShowS # show :: ModuleAssignment -> String # showList :: [ModuleAssignment] -> ShowS # | |||||
| Eq ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Concrete Methods (==) :: ModuleAssignment -> ModuleAssignment -> Bool # (/=) :: ModuleAssignment -> ModuleAssignment -> Bool # | |||||
| type AbsOfCon ModuleAssignment Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
Constructors
| BName | |
Fields
| |
Instances
| Pretty BoundName Source # | |
| HasRange Binder Source # | |
| HasRange BoundName Source # | |
| KillRange Binder Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| KillRange BoundName Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| NFData Binder Source # | |
Defined in Mikan.Syntax.Concrete | |
| NFData BoundName Source # | |
Defined in Mikan.Syntax.Concrete | |
| Show BoundName Source # | |
| Eq BoundName Source # | |
mkBoundName_ :: Name -> BoundName Source #
type TacticAttribute = TacticAttribute' Expr Source #
newtype TacticAttribute' a Source #
Constructors
| TacticAttribute | |
Fields
| |
Instances
| Functor TacticAttribute' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fmap :: (a -> b) -> TacticAttribute' a -> TacticAttribute' b # (<$) :: a -> TacticAttribute' b -> TacticAttribute' a # | |||||
| Foldable TacticAttribute' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => TacticAttribute' m -> m # foldMap :: Monoid m => (a -> m) -> TacticAttribute' a -> m # foldMap' :: Monoid m => (a -> m) -> TacticAttribute' a -> m # foldr :: (a -> b -> b) -> b -> TacticAttribute' a -> b # foldr' :: (a -> b -> b) -> b -> TacticAttribute' a -> b # foldl :: (b -> a -> b) -> b -> TacticAttribute' a -> b # foldl' :: (b -> a -> b) -> b -> TacticAttribute' a -> b # foldr1 :: (a -> a -> a) -> TacticAttribute' a -> a # foldl1 :: (a -> a -> a) -> TacticAttribute' a -> a # toList :: TacticAttribute' a -> [a] # null :: TacticAttribute' a -> Bool # length :: TacticAttribute' a -> Int # elem :: Eq a => a -> TacticAttribute' a -> Bool # maximum :: Ord a => TacticAttribute' a -> a # minimum :: Ord a => TacticAttribute' a -> a # sum :: Num a => TacticAttribute' a -> a # product :: Num a => TacticAttribute' a -> a # | |||||
| Traversable TacticAttribute' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> TacticAttribute' a -> f (TacticAttribute' b) # sequenceA :: Applicative f => TacticAttribute' (f a) -> f (TacticAttribute' a) # mapM :: Monad m => (a -> m b) -> TacticAttribute' a -> m (TacticAttribute' b) # sequence :: Monad m => TacticAttribute' (m a) -> m (TacticAttribute' a) # | |||||
| ExprLike a => ExprLike (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Abstract.Views Methods recurseExpr :: RecurseExprFn m (TacticAttribute' a) Source # foldExpr :: FoldExprFn m (TacticAttribute' a) Source # traverseExpr :: TraverseExprFn m (TacticAttribute' a) Source # mapExpr :: (Expr -> Expr) -> TacticAttribute' a -> TacticAttribute' a Source # | |||||
| Pretty a => Pretty (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: TacticAttribute' a -> Doc Source # prettyPrec :: Int -> TacticAttribute' a -> Doc Source # prettyList :: [TacticAttribute' a] -> Doc Source # | |||||
| ExprLike a => ExprLike (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> TacticAttribute' a -> TacticAttribute' a Source # foldExpr :: Monoid m => (Expr -> m) -> TacticAttribute' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> TacticAttribute' a -> m (TacticAttribute' a) Source # | |||||
| HasRange (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: TacticAttribute' a -> Range Source # | |||||
| KillRange (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods killRange :: KillRangeT (TacticAttribute' a) Source # | |||||
| ToConcrete a => ToConcrete (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete Associated Types
Methods toConcrete :: MonadToConcrete m => TacticAttribute' a -> m (ConOfAbs (TacticAttribute' a)) Source # bindToConcrete :: MonadToConcrete m => TacticAttribute' a -> (ConOfAbs (TacticAttribute' a) -> m b) -> m b Source # | |||||
| Null (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Concrete | |||||
| NFData a => NFData (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods rnf :: TacticAttribute' a -> () # | |||||
| Show a => Show (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods showsPrec :: Int -> TacticAttribute' a -> ShowS # show :: TacticAttribute' a -> String # showList :: [TacticAttribute' a] -> ShowS # | |||||
| Eq a => Eq (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods (==) :: TacticAttribute' a -> TacticAttribute' a -> Bool # (/=) :: TacticAttribute' a -> TacticAttribute' a -> Bool # | |||||
| type ConOfAbs (TacticAttribute' a) Source # | |||||
Defined in Mikan.Syntax.Translation.AbstractToConcrete | |||||
type Telescope = [TypedBinding] Source #
type Telescope1 = List1 TypedBinding Source #
A telescope is a sequence of typed bindings. Bound variables are in scope in later types.
type Parameters = [LamBinding] Source #
Parameters are sequences of typed or untyped bindings.
parametersToTelescope :: Range -> Parameters -> Telescope Source #
We can get a Telescope from Parameters.
If we have a type annotation already, we're happy.
Otherwise we manufacture a binder with an underscore for the type.
makePi :: Telescope -> Expr -> Expr Source #
Smart constructor for Pi: check whether the Telescope is empty
mkLam :: Range -> [LamBinding] -> Expr -> Expr Source #
Smart constructor for Lam: check for non-zero bindings.
mkLet :: Range -> [Declaration] -> Expr -> Expr Source #
Smart constructor for Let: check for non-zero let bindings.
mkTLet :: Range -> [Declaration] -> Maybe (TypedBinding' e) Source #
Smart constructor for TLet: check for non-zero let bindings.
Declarations
data Declaration Source #
The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.
Constructors
| TypeSig ArgInfo TacticAttribute Name Expr |
|
| FieldSig IsInstance TacticAttribute Name (Arg Expr) | |
| Generalize KwRange [TypeSignature] | Variables to be generalized, can be hidden. |
| Field KwRange [FieldSignature] | |
| FunClause LHS RHS WhereClause Catchall | |
| DataSig Range Name Parameters Expr | lone data signature in mutual block |
| Data Range Name Parameters Expr [TypeSignatureOrInstanceBlock] | |
| DataDef Range Name Parameters [TypeSignatureOrInstanceBlock] | |
| RecordSig Range Name Parameters Expr | lone record signature in mutual block |
| RecordDef Range Name [RecordDirective] Parameters [Declaration] | |
| Record Range Name [RecordDirective] Parameters Expr [Declaration] | |
| Infix Fixity (List1 Name) | |
| Syntax Name Notation | notation declaration for a name |
| PatternSyn Range Name [WithHiding Name] Pattern | |
| Mutual KwRange [Declaration] | |
| InterleavedMutual KwRange [Declaration] | |
| Abstract KwRange [Declaration] | |
| Private KwRange Origin [Declaration] | In Agda.Syntax.Concrete.Definitions we generate private blocks
temporarily, which should be treated different that user-declared
private blocks. Thus the |
| InstanceB KwRange [Declaration] | The |
| LoneConstructor KwRange [Declaration] | |
| Macro KwRange [Declaration] | |
| Postulate KwRange [TypeSignatureOrInstanceBlock] | |
| Primitive KwRange [TypeSignature] | |
| Open KwRange QName ImportDirective |
|
| Import OpenShortHand KwRange QName (Either AsName RawOpenArgs) ImportDirective | |
| ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective | |
| Module Range QName Telescope [Declaration] | |
| UnquoteDecl Range [Name] Expr | unquoteDecl xs = e |
| UnquoteDef Range [Name] Expr | unquoteDef xs = e |
| UnquoteData Range Name [Name] Expr | unquoteDecl data d constructor xs = e |
| Pragma Pragma | |
| Opaque KwRange [Declaration] | opaque ... |
| Unfolding KwRange [QName] | unfolding ... |
Instances
| Pretty Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: Declaration -> Doc Source # prettyPrec :: Int -> Declaration -> Doc Source # prettyList :: [Declaration] -> Doc Source # | |||||
| Pretty WhereClause Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source # | |||||
| ExprLike Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> Declaration -> Declaration Source # foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration Source # | |||||
| FoldDecl Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> Declaration -> m Source # | |||||
| TraverseDecl Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> Declaration -> m Declaration Source # | |||||
| HasRange Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: Declaration -> Range Source # | |||||
| HasRange WhereClause Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: WhereClause -> Range Source # | |||||
| KillRange Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| KillRange WhereClause Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| NFData Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete Methods rnf :: Declaration -> () # | |||||
| Show Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods showsPrec :: Int -> Declaration -> ShowS # show :: Declaration -> String # showList :: [Declaration] -> ShowS # | |||||
| Show WhereClause Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS # show :: WhereClause -> String # showList :: [WhereClause] -> ShowS # | |||||
| Eq Declaration Source # | |||||
Defined in Mikan.Syntax.Concrete | |||||
| ToAbstract (TopLevel [Declaration]) Source # | Top-level declarations are always
| ||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: TopLevel [Declaration] -> ScopeM (AbsOfCon (TopLevel [Declaration])) Source # | |||||
| type AbsOfCon (TopLevel [Declaration]) Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
isPragma :: CMaybe Pragma m => Declaration -> m Source #
Return Pragma if Declaration is Pragma.
data RecordDirective Source #
Isolated record directives parsed as Declarations
Constructors
| Induction (Ranged Induction) | Range of keyword |
| Constructor Name IsInstance | |
| Eta (Ranged HasEta0) | Range of |
| PatternOrCopattern Range | If declaration |
Instances
| Pretty RecordDirective Source # | |
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: RecordDirective -> Doc Source # prettyPrec :: Int -> RecordDirective -> Doc Source # prettyList :: [RecordDirective] -> Doc Source # | |
| HasRange RecordDirective Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: RecordDirective -> Range Source # | |
| KillRange RecordDirective Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| EmbPrj RecordDirective Source # | |
| NFData RecordDirective Source # | Ranges are not forced. |
Defined in Mikan.Syntax.Concrete Methods rnf :: RecordDirective -> () # | |
| Show RecordDirective Source # | |
Defined in Mikan.Syntax.Concrete Methods showsPrec :: Int -> RecordDirective -> ShowS # show :: RecordDirective -> String # showList :: [RecordDirective] -> ShowS # | |
| Eq RecordDirective Source # | |
Defined in Mikan.Syntax.Concrete Methods (==) :: RecordDirective -> RecordDirective -> Bool # (/=) :: RecordDirective -> RecordDirective -> Bool # | |
type RecordDirectives = RecordDirectives' (Maybe (Name, IsInstance)) Source #
data ModuleApplication Source #
Constructors
| SectionApp Range Telescope QName [Expr] |
|
| RecordModuleInstance Range QName | M {{...}} |
Instances
| Pretty ModuleApplication Source # | |
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: ModuleApplication -> Doc Source # prettyPrec :: Int -> ModuleApplication -> Doc Source # prettyList :: [ModuleApplication] -> Doc Source # | |
| ExprLike ModuleApplication Source # | |
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication Source # foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication Source # | |
| HasRange ModuleApplication Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: ModuleApplication -> Range Source # | |
| KillRange ModuleApplication Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| NFData ModuleApplication Source # | Ranges are not forced. |
Defined in Mikan.Syntax.Concrete Methods rnf :: ModuleApplication -> () # | |
| Show ModuleApplication Source # | |
Defined in Mikan.Syntax.Concrete.Pretty Methods showsPrec :: Int -> ModuleApplication -> ShowS # show :: ModuleApplication -> String # showList :: [ModuleApplication] -> ShowS # | |
| Eq ModuleApplication Source # | |
Defined in Mikan.Syntax.Concrete Methods (==) :: ModuleApplication -> ModuleApplication -> Bool # (/=) :: ModuleApplication -> ModuleApplication -> Bool # | |
type TypeSignature = Declaration Source #
Just type signatures.
type TypeSignatureOrInstanceBlock = Declaration Source #
Just type signatures or instance blocks.
type ImportDirective = ImportDirective' Name Name Source #
The things you are allowed to say when you shuffle names between name
spaces (i.e. in import, namespace, or open declarations).
type ImportedName = ImportedName' Name Name Source #
An imported name can be a module or a defined name.
type HidingDirective = HidingDirective' Name Name Source #
The content of the as-clause of the import statement.
Constructors
| AsName | |
Instances
| HasRange AsName Source # | |
| KillRange AsName Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| NFData AsName Source # | Ranges are not forced. |
Defined in Mikan.Syntax.Concrete | |
| Functor AsName' Source # | |
| Foldable AsName' Source # | |
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => AsName' m -> m # foldMap :: Monoid m => (a -> m) -> AsName' a -> m # foldMap' :: Monoid m => (a -> m) -> AsName' a -> m # foldr :: (a -> b -> b) -> b -> AsName' a -> b # foldr' :: (a -> b -> b) -> b -> AsName' a -> b # foldl :: (b -> a -> b) -> b -> AsName' a -> b # foldl' :: (b -> a -> b) -> b -> AsName' a -> b # foldr1 :: (a -> a -> a) -> AsName' a -> a # foldl1 :: (a -> a -> a) -> AsName' a -> a # elem :: Eq a => a -> AsName' a -> Bool # maximum :: Ord a => AsName' a -> a # minimum :: Ord a => AsName' a -> a # | |
| Traversable AsName' Source # | |
| Show a => Show (AsName' a) Source # | |
| Eq a => Eq (AsName' a) Source # | |
type RawOpenArgs = [Expr] Source #
Expressions usually instantiating module parameters as in
open import Monoid Carrier _==_
that might also code an as clause e.g. in
open import File as M
The parser does not distinguish these so we do it in the nicifier.
data OpenShortHand Source #
Instances
| Pretty OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: OpenShortHand -> Doc Source # prettyPrec :: Int -> OpenShortHand -> Doc Source # prettyList :: [OpenShortHand] -> Doc Source # | |||||
| HasRange OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete Methods getRange :: OpenShortHand -> Range Source # | |||||
| KillRange OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| Null OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete | |||||
| NFData OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete Methods rnf :: OpenShortHand -> () # | |||||
| Generic OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete Associated Types
| |||||
| Show OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete Methods showsPrec :: Int -> OpenShortHand -> ShowS # show :: OpenShortHand -> String # showList :: [OpenShortHand] -> ShowS # | |||||
| Eq OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete Methods (==) :: OpenShortHand -> OpenShortHand -> Bool # (/=) :: OpenShortHand -> OpenShortHand -> Bool # | |||||
| type Rep OpenShortHand Source # | |||||
Defined in Mikan.Syntax.Concrete type Rep OpenShortHand = D1 ('MetaData "OpenShortHand" "Mikan.Syntax.Concrete" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "DoOpen" 'PrefixI 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rec0 KwRange)) :+: C1 ('MetaCons "DontOpen" 'PrefixI 'False) (U1 :: Type -> Type)) | |||||
type RewriteEqn = RewriteEqn' () Name Pattern Expr Source #
Left hand sides can be written in infix style. For example:
n + suc m = suc (n + m) (f ∘ g) x = f (g x)
We use fixity information to see which name is actually defined.
Constructors
| LHS | Original pattern (including with-patterns), rewrite equations and with-expressions. |
Fields
| |
Instances
| Pretty LHS Source # | |
| ExprLike LHS Source # | |
| HasEllipsis LHS Source # | Does the lhs contain an ellipsis? |
Defined in Mikan.Syntax.Concrete.Pattern Methods hasEllipsis :: LHS -> Bool Source # | |
| HasRange LHS Source # | |
| KillRange LHS Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| PrettyTCM LHS Source # | |
Defined in Mikan.TypeChecking.Pretty | |
| NFData LHS Source # | Ranges are not forced. |
Defined in Mikan.Syntax.Concrete | |
| Show LHS Source # | |
| Eq LHS Source # | |
Concrete patterns. No literals in patterns at the moment.
Constructors
| IdentP Bool QName |
If the boolean is
|
| QuoteP Range | quote |
| AppP Pattern (NamedArg Pattern) |
|
| RawAppP Range (List2 Pattern) |
|
| OpAppP Range QName (Set1 Name) (List1 (NamedArg Pattern)) | eg: |
| HiddenP Range (Named_ Pattern) |
|
| InstanceP Range (Named_ Pattern) |
|
| ParenP Range Pattern | (p) |
| WildP Range | _ |
| AbsurdP Range | () |
| AsP Range Name Pattern | x@p |
| DotP KwRange Range !PossiblyProjectionPattern Expr |
|
| LitP Range Literal |
|
| RecP KwRange Range [FieldAssignment' Pattern] |
|
| EqualP Range (List1 (Expr, Expr)) |
|
| EllipsisP Range (Maybe Pattern) |
|
| WithP Range Pattern |
|
Instances
| Pretty Pattern Source # | |||||
| IsExpr Pattern Source # | |||||
| CPatternLike Pattern Source # | |||||
Defined in Mikan.Syntax.Concrete.Pattern | |||||
| HasEllipsis Pattern Source # | |||||
Defined in Mikan.Syntax.Concrete.Pattern Methods hasEllipsis :: Pattern -> Bool Source # | |||||
| IsEllipsis Pattern Source # | Is the pattern just | ||||
Defined in Mikan.Syntax.Concrete.Pattern Methods isEllipsis :: Pattern -> Bool Source # | |||||
| IsWithP Pattern Source # | |||||
| HasRange Pattern Source # | |||||
| KillRange Pattern Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| SetRange Pattern Source # | |||||
| ToAbstract HoleContent Source # | Content of interaction hole. | ||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source # | |||||
| ToAbstract Pattern Source # | Scope check a | ||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| ToAbstract RewriteEqn Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: RewriteEqn -> ScopeM (AbsOfCon RewriteEqn) Source # | |||||
| NFData Pattern Source # | Ranges are not forced. | ||||
Defined in Mikan.Syntax.Concrete | |||||
| Show Pattern Source # | |||||
| Eq Pattern Source # | |||||
| type AbsOfCon HoleContent Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
| type AbsOfCon Pattern Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
| type AbsOfCon RewriteEqn Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
Processed (operator-parsed) intermediate form of the core f ps of LHS.
Corresponds to lhsOriginalPattern.
Constructors
| LHSHead | |
Fields
| |
| LHSProj | |
| LHSWith | |
| LHSEllipsis | |
Fields
| |
Instances
| Pretty LHSCore Source # | |||||
| HasRange LHSCore Source # | |||||
| ToAbstract LHSCore Source # | Scope-check a | ||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| Show LHSCore Source # | |||||
| Eq LHSCore Source # | |||||
| type AbsOfCon LHSCore Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
Constructors
| LamClause | |
Instances
| Pretty RHS Source # | |||||
| HasRange RHS Source # | |||||
| KillRange RHS Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| ToAbstract RHS Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| Functor RHS' Source # | |||||
| Foldable RHS' Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => RHS' m -> m # foldMap :: Monoid m => (a -> m) -> RHS' a -> m # foldMap' :: Monoid m => (a -> m) -> RHS' a -> m # foldr :: (a -> b -> b) -> b -> RHS' a -> b # foldr' :: (a -> b -> b) -> b -> RHS' a -> b # foldl :: (b -> a -> b) -> b -> RHS' a -> b # foldl' :: (b -> a -> b) -> b -> RHS' a -> b # foldr1 :: (a -> a -> a) -> RHS' a -> a # foldl1 :: (a -> a -> a) -> RHS' a -> a # elem :: Eq a => a -> RHS' a -> Bool # maximum :: Ord a => RHS' a -> a # | |||||
| Traversable RHS' Source # | |||||
| Show RHS Source # | |||||
| ExprLike a => ExprLike (RHS' a) Source # | |||||
| NFData a => NFData (RHS' a) Source # | |||||
Defined in Mikan.Syntax.Concrete | |||||
| Eq e => Eq (RHS' e) Source # | |||||
| type AbsOfCon RHS Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
type WhereClause = WhereClause' [Declaration] Source #
where block following a clause.
data WhereClause' decls Source #
The generalization WhereClause' is for the sake of Agda.Concrete.Generic.
Constructors
| NoWhere | No |
| LocalWhere Range decls | Ordinary |
| NonLocalWhere Range Name Access decls | Non-local where: |
Instances
| Pretty WhereClause Source # | |
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: WhereClause -> Doc Source # prettyPrec :: Int -> WhereClause -> Doc Source # prettyList :: [WhereClause] -> Doc Source # | |
| HasRange WhereClause Source # | |
Defined in Mikan.Syntax.Concrete Methods getRange :: WhereClause -> Range Source # | |
| KillRange WhereClause Source # | |
Defined in Mikan.Syntax.Concrete Methods | |
| Functor WhereClause' Source # | |
Defined in Mikan.Syntax.Concrete Methods fmap :: (a -> b) -> WhereClause' a -> WhereClause' b # (<$) :: a -> WhereClause' b -> WhereClause' a # | |
| Foldable WhereClause' Source # | |
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => WhereClause' m -> m # foldMap :: Monoid m => (a -> m) -> WhereClause' a -> m # foldMap' :: Monoid m => (a -> m) -> WhereClause' a -> m # foldr :: (a -> b -> b) -> b -> WhereClause' a -> b # foldr' :: (a -> b -> b) -> b -> WhereClause' a -> b # foldl :: (b -> a -> b) -> b -> WhereClause' a -> b # foldl' :: (b -> a -> b) -> b -> WhereClause' a -> b # foldr1 :: (a -> a -> a) -> WhereClause' a -> a # foldl1 :: (a -> a -> a) -> WhereClause' a -> a # toList :: WhereClause' a -> [a] # null :: WhereClause' a -> Bool # length :: WhereClause' a -> Int # elem :: Eq a => a -> WhereClause' a -> Bool # maximum :: Ord a => WhereClause' a -> a # minimum :: Ord a => WhereClause' a -> a # sum :: Num a => WhereClause' a -> a # product :: Num a => WhereClause' a -> a # | |
| Traversable WhereClause' Source # | |
Defined in Mikan.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> WhereClause' a -> f (WhereClause' b) # sequenceA :: Applicative f => WhereClause' (f a) -> f (WhereClause' a) # mapM :: Monad m => (a -> m b) -> WhereClause' a -> m (WhereClause' b) # sequence :: Monad m => WhereClause' (m a) -> m (WhereClause' a) # | |
| Show WhereClause Source # | |
Defined in Mikan.Syntax.Concrete.Pretty Methods showsPrec :: Int -> WhereClause -> ShowS # show :: WhereClause -> String # showList :: [WhereClause] -> ShowS # | |
| ExprLike a => ExprLike (WhereClause' a) Source # | |
Defined in Mikan.Syntax.Concrete.Generic Methods mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a Source # foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m Source # traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a) Source # | |
| FoldDecl a => FoldDecl (WhereClause' a) Source # | |
Defined in Mikan.Syntax.Concrete.Generic Methods foldDecl :: Monoid m => (Declaration -> m) -> WhereClause' a -> m Source # | |
| TraverseDecl a => TraverseDecl (WhereClause' a) Source # | |
Defined in Mikan.Syntax.Concrete.Generic Methods preTraverseDecl :: Monad m => (Declaration -> m Declaration) -> WhereClause' a -> m (WhereClause' a) Source # | |
| Null (WhereClause' a) Source # | A |
Defined in Mikan.Syntax.Concrete | |
| NFData a => NFData (WhereClause' a) Source # | |
Defined in Mikan.Syntax.Concrete Methods rnf :: WhereClause' a -> () # | |
| Eq decls => Eq (WhereClause' decls) Source # | |
Defined in Mikan.Syntax.Concrete Methods (==) :: WhereClause' decls -> WhereClause' decls -> Bool # (/=) :: WhereClause' decls -> WhereClause' decls -> Bool # | |
data WhereClause_ Source #
Type of where block following a clause.
Constructors
| NoWhere_ | No |
| LocalWhere_ | Ordinary |
| NonLocalWhere_ | Non-local where: |
Instances
| Null WhereClause_ Source # | |||||
Defined in Mikan.Syntax.Concrete | |||||
| NFData WhereClause_ Source # | |||||
Defined in Mikan.Syntax.Concrete Methods rnf :: WhereClause_ -> () # | |||||
| Generic WhereClause_ Source # | |||||
Defined in Mikan.Syntax.Concrete Associated Types
| |||||
| Eq WhereClause_ Source # | |||||
Defined in Mikan.Syntax.Concrete | |||||
| type Rep WhereClause_ Source # | |||||
Defined in Mikan.Syntax.Concrete type Rep WhereClause_ = D1 ('MetaData "WhereClause_" "Mikan.Syntax.Concrete" "Mikan-2.9.0-CZbYRMbHmng2A9zjJ31VFu" 'False) (C1 ('MetaCons "NoWhere_" 'PrefixI 'False) (U1 :: Type -> Type) :+: (C1 ('MetaCons "LocalWhere_" 'PrefixI 'False) (U1 :: Type -> Type) :+: C1 ('MetaCons "NonLocalWhere_" 'PrefixI 'False) (U1 :: Type -> Type))) | |||||
An expression followed by a where clause. Currently only used to give better a better error message in interaction.
Constructors
| ExprWhere Expr WhereClause |
whereClause_ :: WhereClause' a -> WhereClause_ Source #
Constructors
| DoBind Range Pattern Expr [LamClause] | p ← e where cs |
| DoThen Expr | |
| DoLet Range (List1 Declaration) |
Constructors
| OptionsPragma Range [ShortText] | |
| BuiltinPragma Range RString QName | |
| ForeignPragma Range (Ranged BackendName) ShortText | |
| CompilePragma Range (Ranged BackendName) QName ShortText | |
| InlinePragma Range Bool QName | INLINE or NOINLINE |
| ImpossiblePragma Range [ShortText] | Throws an internal error in the scope checker.
The |
| EtaPragma Range QName | For coinductive records, use pragma instead of regular
|
| WarningOnUsage Range QName ShortText | Applies to the named function |
| WarningOnImport Range ShortText | Applies to the current module |
| InjectivePragma Range QName | Mark a definition as injective for the pattern matching unifier. |
| InjectiveForInferencePragma Range QName | Mark a definition as injective for the conversion checker |
| DisplayPragma Range Pattern Expr | Display lhs as rhs (modifies the printer). |
| CatchallPragma Range | Applies to the following function clause. |
| TerminationCheckPragma Range TerminationCheck | Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block. |
| NoCoverageCheckPragma Range | Applies to the following function (and all that are mutually recursive with it) or to the functions in the following mutual block. |
| NoPositivityCheckPragma Range | Applies to the following data/record type or mutual block. |
| PolarityPragma Range Name [Ranged Occurrence] | |
| NoUniverseCheckPragma Range | Applies to the following data/record type. |
| NotProjectionLikePragma Range QName | Applies to the stated function |
| OverlapPragma Range [QName] OverlapMode | Applies to the given name(s), which must be instance names (checked by the type checker). |
Instances
| Pretty Pragma Source # | |||||
| HasRange Pragma Source # | |||||
| KillRange Pragma Source # | |||||
Defined in Mikan.Syntax.Concrete Methods | |||||
| ToAbstract Pragma Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
| |||||
| NFData Pragma Source # | Ranges are not forced. | ||||
Defined in Mikan.Syntax.Concrete | |||||
| Show Pragma Source # | |||||
| Eq Pragma Source # | |||||
| type AbsOfCon Pragma Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
Modules: Top-level pragmas plus other top-level declarations.
Constructors
| Mod | |
Fields
| |
data ThingWithFixity x Source #
Decorating something with Fixity'.
Constructors
| ThingWithFixity x Fixity' |
Instances
| Functor ThingWithFixity Source # | |
Defined in Mikan.Syntax.Fixity Methods fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b # (<$) :: a -> ThingWithFixity b -> ThingWithFixity a # | |
| Foldable ThingWithFixity Source # | |
Defined in Mikan.Syntax.Fixity Methods fold :: Monoid m => ThingWithFixity m -> m # foldMap :: Monoid m => (a -> m) -> ThingWithFixity a -> m # foldMap' :: Monoid m => (a -> m) -> ThingWithFixity a -> m # foldr :: (a -> b -> b) -> b -> ThingWithFixity a -> b # foldr' :: (a -> b -> b) -> b -> ThingWithFixity a -> b # foldl :: (b -> a -> b) -> b -> ThingWithFixity a -> b # foldl' :: (b -> a -> b) -> b -> ThingWithFixity a -> b # foldr1 :: (a -> a -> a) -> ThingWithFixity a -> a # foldl1 :: (a -> a -> a) -> ThingWithFixity a -> a # toList :: ThingWithFixity a -> [a] # null :: ThingWithFixity a -> Bool # length :: ThingWithFixity a -> Int # elem :: Eq a => a -> ThingWithFixity a -> Bool # maximum :: Ord a => ThingWithFixity a -> a # minimum :: Ord a => ThingWithFixity a -> a # sum :: Num a => ThingWithFixity a -> a # product :: Num a => ThingWithFixity a -> a # | |
| Traversable ThingWithFixity Source # | |
Defined in Mikan.Syntax.Fixity Methods traverse :: Applicative f => (a -> f b) -> ThingWithFixity a -> f (ThingWithFixity b) # sequenceA :: Applicative f => ThingWithFixity (f a) -> f (ThingWithFixity a) # mapM :: Monad m => (a -> m b) -> ThingWithFixity a -> m (ThingWithFixity b) # sequence :: Monad m => ThingWithFixity (m a) -> m (ThingWithFixity a) # | |
| LensFixity (ThingWithFixity a) Source # | |
Defined in Mikan.Syntax.Fixity Methods lensFixity :: Lens' (ThingWithFixity a) Fixity Source # | |
| LensFixity' (ThingWithFixity a) Source # | |
Defined in Mikan.Syntax.Fixity Methods lensFixity' :: Lens' (ThingWithFixity a) Fixity' Source # | |
| Pretty (ThingWithFixity Name) Source # | |
Defined in Mikan.Syntax.Concrete.Pretty Methods pretty :: ThingWithFixity Name -> Doc Source # prettyPrec :: Int -> ThingWithFixity Name -> Doc Source # prettyList :: [ThingWithFixity Name] -> Doc Source # | |
| KillRange x => KillRange (ThingWithFixity x) Source # | |
Defined in Mikan.Syntax.Fixity Methods killRange :: KillRangeT (ThingWithFixity x) Source # | |
| Show x => Show (ThingWithFixity x) Source # | |
Defined in Mikan.Syntax.Fixity Methods showsPrec :: Int -> ThingWithFixity x -> ShowS # show :: ThingWithFixity x -> String # showList :: [ThingWithFixity x] -> ShowS # | |
type HoleContent = HoleContent' () Name Pattern Expr Source #
data HoleContent' qn nm p e Source #
Extended content of an interaction hole.
Constructors
| HoleContentExpr e | e |
| HoleContentRewrite [RewriteEqn' qn nm p e] | (rewrite | invert) e0 | ... | en |
Instances
| ToAbstract HoleContent Source # | Content of interaction hole. | ||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract Associated Types
Methods toAbstract :: HoleContent -> ScopeM (AbsOfCon HoleContent) Source # | |||||
| Functor (HoleContent' qn nm p) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fmap :: (a -> b) -> HoleContent' qn nm p a -> HoleContent' qn nm p b # (<$) :: a -> HoleContent' qn nm p b -> HoleContent' qn nm p a # | |||||
| Foldable (HoleContent' qn nm p) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods fold :: Monoid m => HoleContent' qn nm p m -> m # foldMap :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m # foldMap' :: Monoid m => (a -> m) -> HoleContent' qn nm p a -> m # foldr :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b # foldr' :: (a -> b -> b) -> b -> HoleContent' qn nm p a -> b # foldl :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b # foldl' :: (b -> a -> b) -> b -> HoleContent' qn nm p a -> b # foldr1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a # foldl1 :: (a -> a -> a) -> HoleContent' qn nm p a -> a # toList :: HoleContent' qn nm p a -> [a] # null :: HoleContent' qn nm p a -> Bool # length :: HoleContent' qn nm p a -> Int # elem :: Eq a => a -> HoleContent' qn nm p a -> Bool # maximum :: Ord a => HoleContent' qn nm p a -> a # minimum :: Ord a => HoleContent' qn nm p a -> a # sum :: Num a => HoleContent' qn nm p a -> a # product :: Num a => HoleContent' qn nm p a -> a # | |||||
| Traversable (HoleContent' qn nm p) Source # | |||||
Defined in Mikan.Syntax.Concrete Methods traverse :: Applicative f => (a -> f b) -> HoleContent' qn nm p a -> f (HoleContent' qn nm p b) # sequenceA :: Applicative f => HoleContent' qn nm p (f a) -> f (HoleContent' qn nm p a) # mapM :: Monad m => (a -> m b) -> HoleContent' qn nm p a -> m (HoleContent' qn nm p b) # sequence :: Monad m => HoleContent' qn nm p (m a) -> m (HoleContent' qn nm p a) # | |||||
| type AbsOfCon HoleContent Source # | |||||
Defined in Mikan.Syntax.Translation.ConcreteToAbstract | |||||
spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration]) Source #
Splits off allowed (= import) declarations before the first non-allowed declaration. After successful parsing, the first non-allowed declaration should be a module declaration.