Agda.Syntax.Concrete

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.

Expressions

data Expr

Concrete expressions. Should represent exactly what the user wrote.

Constructors

Ident QName

ex: x

Lit Literal

ex: 1 or "foo"

QuestionMark Range (Maybe Nat)

ex: ? or {! ... !}

Underscore Range (Maybe String)

ex: _ or _A_5

RawApp Range [Expr]

before parsing operators

App Range Expr (NamedArg Expr)

ex: e e, e {e}, or e {x = e}

OpApp Range QName (Set Name) [NamedArg (MaybePlaceholder (OpApp Expr))]

ex: e + e The QName is possibly ambiguous, but it must correspond to one of the names in the set.

WithApp Range Expr [Expr]

ex: e | e1 | .. | en

HiddenArg Range (Named_ Expr)

ex: {e} or {x=e}

InstanceArg Range (Named_ Expr)

ex: {{e}} or {{x=e}}

Lam Range [LamBinding] Expr

ex: \x {y} -> e or \(x:A){y:B} -> e

AbsurdLam Range Hiding

ex: \ ()

ExtendedLam Range [(LHS, RHS, WhereClause, Bool)]

ex: \ { p11 .. p1a -> e1 ; .. ; pn1 .. pnz -> en }

Fun Range Expr Expr

ex: e -> e or .e -> e (NYI: {e} -> e)

Pi Telescope Expr

ex: (xs:e) -> e or {xs:e} -> e

Set Range

ex: Set

Prop Range

ex: Prop

SetN Range Integer

ex: Set0, Set1, ..

Rec Range RecordAssignments

ex: record {x = a; y = b}, or record { x = a; M1; M2 }

RecUpdate Range Expr [FieldAssignment]

ex: record e {x = a; y = b}

Let Range [Declaration] Expr

ex: let Ds in e

Paren Range Expr

ex: (e)

Absurd Range

ex: () or {}, only in patterns

As Range Name Expr

ex: x@p, only in patterns

Dot Range Expr

ex: .p, only in patterns

ETel Telescope

only used for printing telescopes

QuoteGoal Range Name Expr

ex: quoteGoal x in e

QuoteContext Range

ex: quoteContext

Quote Range

ex: quote, should be applied to a name

QuoteTerm Range

ex: quoteTerm, should be applied to a term

Tactic Range Expr [Expr]

tactic solve | subgoal1 | .. | subgoalN

Unquote Range

ex: unquote, should be applied to a term of type Term

DontCare Expr

to print irrelevant things

Equal Range Expr Expr

ex: a = b, used internally in the parser

Instances

NFData Expr

Ranges are not forced.

Methods

rnf :: Expr -> ()

KillRange RHS

Methods

killRange :: KillRangeT RHS

KillRange TypedBinding

Methods

killRange :: KillRangeT TypedBinding

KillRange TypedBindings

Methods

killRange :: KillRangeT TypedBindings

KillRange LamBinding

Methods

killRange :: KillRangeT LamBinding

KillRange Expr

Methods

killRange :: KillRangeT Expr

SetRange TypedBindings

Methods

setRange :: Range -> TypedBindings -> TypedBindings

HasRange RHS

Methods

getRange :: RHS -> Range

HasRange TypedBinding

Methods

getRange :: TypedBinding -> Range

HasRange TypedBindings

Methods

getRange :: TypedBindings -> Range

HasRange LamBinding

Methods

getRange :: LamBinding -> Range

HasRange Expr

Methods

getRange :: Expr -> Range

LensRelevance TypedBindings

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings

LensHiding TypedBindings

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

ExprLike TypedBindings

Methods

mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings

traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBindings -> m TypedBindings

foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m

ExprLike LamBinding

Methods

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

ExprLike Expr

Methods

mapExpr :: (Expr -> Expr) -> Expr -> Expr

traverseExpr :: Monad m => (Expr -> m Expr) -> Expr -> m Expr

foldExpr :: Monoid m => (Expr -> m) -> Expr -> m

ExprLike FieldAssignment

Methods

mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment

traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment

foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m

IsExpr Expr

Methods

exprView :: Expr -> ExprView Expr

unExprView :: ExprView Expr -> Expr

ToConcrete InteractionId Expr

Methods

toConcrete :: InteractionId -> AbsToCon Expr

bindToConcrete :: InteractionId -> (Expr -> AbsToCon b) -> AbsToCon b

ToConcrete TypedBinding TypedBinding

Methods

toConcrete :: TypedBinding -> AbsToCon TypedBinding

bindToConcrete :: TypedBinding -> (TypedBinding -> AbsToCon b) -> AbsToCon b

ToConcrete Expr Expr

Methods

toConcrete :: Expr -> AbsToCon Expr

bindToConcrete :: Expr -> (Expr -> AbsToCon b) -> AbsToCon b

ToConcrete NamedMeta Expr

Methods

toConcrete :: NamedMeta -> AbsToCon Expr

bindToConcrete :: NamedMeta -> (Expr -> AbsToCon b) -> AbsToCon b

ToAbstract RHS AbstractRHS

Methods

toAbstract :: RHS -> ScopeM AbstractRHS

ToAbstract TypedBinding TypedBinding

Methods

toAbstract :: TypedBinding -> ScopeM TypedBinding

ToAbstract TypedBindings TypedBindings

Methods

toAbstract :: TypedBindings -> ScopeM TypedBindings

ToAbstract LamBinding LamBinding

Methods

toAbstract :: LamBinding -> ScopeM LamBinding

ToAbstract Expr Expr

Methods

toAbstract :: Expr -> ScopeM Expr

ToConcrete TypedBindings [TypedBindings]

Methods

toConcrete :: TypedBindings -> AbsToCon [TypedBindings]

bindToConcrete :: TypedBindings -> ([TypedBindings] -> AbsToCon b) -> AbsToCon b

ToConcrete LamBinding [LamBinding]

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding]

bindToConcrete :: LamBinding -> ([LamBinding] -> AbsToCon b) -> AbsToCon b

ToAbstract LHSCore (LHSCore' Expr)

Methods

toAbstract :: LHSCore -> ScopeM (LHSCore' Expr)

ToAbstract Pattern (Pattern' Expr)

Methods

toAbstract :: Pattern -> ScopeM (Pattern' Expr)

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Methods

toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration])

bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b

ToAbstract (Pattern' Expr) (Pattern' Expr)

Methods

toAbstract :: Pattern' Expr -> ScopeM (Pattern' Expr)

ToAbstract (LHSCore' Expr) (LHSCore' Expr)

Methods

toAbstract :: LHSCore' Expr -> ScopeM (LHSCore' Expr)

data OpApp e

Constructors

SyntaxBindingLambda Range [LamBinding] e

An abstraction inside a special syntax declaration (see Issue 358 why we introduce this).

Ordinary e

Instances

Functor OpApp

Methods

fmap :: (a -> b) -> OpApp a -> OpApp b

(<$) :: a -> OpApp b -> OpApp a

Foldable OpApp

Methods

fold :: Monoid m => OpApp m -> 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

toList :: OpApp a -> [a]

null :: OpApp a -> Bool

length :: OpApp a -> Int

elem :: Eq a => a -> OpApp a -> Bool

maximum :: Ord a => OpApp a -> a

minimum :: Ord a => OpApp a -> a

sum :: Num a => OpApp a -> a

product :: Num a => OpApp a -> a

Traversable OpApp

Methods

traverse :: Applicative f => (a -> f b) -> OpApp a -> f (OpApp b)

sequenceA :: Applicative f => OpApp (f a) -> f (OpApp a)

mapM :: Monad m => (a -> m b) -> OpApp a -> m (OpApp b)

sequence :: Monad m => OpApp (m a) -> m (OpApp a)

NFData a => NFData (OpApp a)

Ranges are not forced.

Methods

rnf :: OpApp a -> ()

KillRange e => KillRange (OpApp e)

Methods

killRange :: KillRangeT (OpApp e)

HasRange e => HasRange (OpApp e)

Methods

getRange :: OpApp e -> Range

ExprLike a => ExprLike (OpApp a)

Methods

mapExpr :: (Expr -> Expr) -> OpApp a -> OpApp a

traverseExpr :: Monad m => (Expr -> m Expr) -> OpApp a -> m (OpApp a)

foldExpr :: Monoid m => (Expr -> m) -> OpApp a -> m

fromOrdinary :: e -> OpApp e -> e

module Agda.Syntax.Concrete.Name

appView :: Expr -> AppView

data AppView

The Expr is not an application.

Constructors

AppView Expr [NamedArg Expr]

Bindings

type LamBinding = LamBinding' TypedBindings

A lambda binding is either domain free or typed.

data LamBinding' a

Constructors

DomainFree ArgInfo BoundName

. x or {x} or .x or .{x} or {.x}

DomainFull a

. (xs : e) or {xs : e}

Instances

Functor LamBinding'

Methods

fmap :: (a -> b) -> LamBinding' a -> LamBinding' b

(<$) :: a -> LamBinding' b -> LamBinding' a

Foldable LamBinding'

Methods

fold :: Monoid m => LamBinding' m -> 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'

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)

KillRange LamBinding

Methods

killRange :: KillRangeT LamBinding

HasRange LamBinding

Methods

getRange :: LamBinding -> Range

LensHiding LamBinding

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

ExprLike LamBinding

Methods

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

ToAbstract LamBinding LamBinding

Methods

toAbstract :: LamBinding -> ScopeM LamBinding

ToConcrete LamBinding [LamBinding]

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding]

bindToConcrete :: LamBinding -> ([LamBinding] -> AbsToCon b) -> AbsToCon b

NFData a => NFData (LamBinding' a)

Methods

rnf :: LamBinding' a -> ()

type TypedBindings = TypedBindings' TypedBinding

A sequence of typed bindings with hiding information. Appears in dependent function spaces, typed lambdas, and telescopes.

If the individual binding contains hiding information as well, the Hiding in TypedBindings must be the unit NotHidden.

data TypedBindings' a

Constructors

TypedBindings Range (Arg a)

. (xs : e) or {xs : e} or something like (x {y} _ : e).

Instances

Functor TypedBindings'

Methods

fmap :: (a -> b) -> TypedBindings' a -> TypedBindings' b

(<$) :: a -> TypedBindings' b -> TypedBindings' a

Foldable TypedBindings'

Methods

fold :: Monoid m => TypedBindings' m -> m

foldMap :: Monoid m => (a -> m) -> TypedBindings' a -> m

foldr :: (a -> b -> b) -> b -> TypedBindings' a -> b

foldr' :: (a -> b -> b) -> b -> TypedBindings' a -> b

foldl :: (b -> a -> b) -> b -> TypedBindings' a -> b

foldl' :: (b -> a -> b) -> b -> TypedBindings' a -> b

foldr1 :: (a -> a -> a) -> TypedBindings' a -> a

foldl1 :: (a -> a -> a) -> TypedBindings' a -> a

toList :: TypedBindings' a -> [a]

null :: TypedBindings' a -> Bool

length :: TypedBindings' a -> Int

elem :: Eq a => a -> TypedBindings' a -> Bool

maximum :: Ord a => TypedBindings' a -> a

minimum :: Ord a => TypedBindings' a -> a

sum :: Num a => TypedBindings' a -> a

product :: Num a => TypedBindings' a -> a

Traversable TypedBindings'

Methods

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

sequenceA :: Applicative f => TypedBindings' (f a) -> f (TypedBindings' a)

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

sequence :: Monad m => TypedBindings' (m a) -> m (TypedBindings' a)

KillRange TypedBindings

Methods

killRange :: KillRangeT TypedBindings

KillRange LamBinding

Methods

killRange :: KillRangeT LamBinding

SetRange TypedBindings

Methods

setRange :: Range -> TypedBindings -> TypedBindings

HasRange TypedBindings

Methods

getRange :: TypedBindings -> Range

HasRange LamBinding

Methods

getRange :: LamBinding -> Range

LensRelevance TypedBindings

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings

LensHiding TypedBindings

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

ExprLike TypedBindings

Methods

mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings

traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBindings -> m TypedBindings

foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m

ExprLike LamBinding

Methods

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

ToAbstract TypedBindings TypedBindings

Methods

toAbstract :: TypedBindings -> ScopeM TypedBindings

ToAbstract LamBinding LamBinding

Methods

toAbstract :: LamBinding -> ScopeM LamBinding

ToConcrete TypedBindings [TypedBindings]

Methods

toConcrete :: TypedBindings -> AbsToCon [TypedBindings]

bindToConcrete :: TypedBindings -> ([TypedBindings] -> AbsToCon b) -> AbsToCon b

ToConcrete LamBinding [LamBinding]

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding]

bindToConcrete :: LamBinding -> ([LamBinding] -> AbsToCon b) -> AbsToCon b

NFData a => NFData (TypedBindings' a)

Ranges are not forced.

Methods

rnf :: TypedBindings' a -> ()

type TypedBinding = TypedBinding' Expr

A typed binding.

data TypedBinding' e

Constructors

TBind Range [WithHiding BoundName] e

Binding (x1 ... xn : A).

TLet Range [Declaration]

Let binding (let Ds) or (open M args).

Instances

Functor TypedBinding'

Methods

fmap :: (a -> b) -> TypedBinding' a -> TypedBinding' b

(<$) :: a -> TypedBinding' b -> TypedBinding' a

Foldable TypedBinding'

Methods

fold :: Monoid m => TypedBinding' m -> 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'

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)

KillRange TypedBinding

Methods

killRange :: KillRangeT TypedBinding

KillRange TypedBindings

Methods

killRange :: KillRangeT TypedBindings

KillRange LamBinding

Methods

killRange :: KillRangeT LamBinding

SetRange TypedBindings

Methods

setRange :: Range -> TypedBindings -> TypedBindings

HasRange TypedBinding

Methods

getRange :: TypedBinding -> Range

HasRange TypedBindings

Methods

getRange :: TypedBindings -> Range

HasRange LamBinding

Methods

getRange :: LamBinding -> Range

LensRelevance TypedBindings

Methods

getRelevance :: TypedBindings -> Relevance

setRelevance :: Relevance -> TypedBindings -> TypedBindings

mapRelevance :: (Relevance -> Relevance) -> TypedBindings -> TypedBindings

LensHiding TypedBindings

Methods

getHiding :: TypedBindings -> Hiding

setHiding :: Hiding -> TypedBindings -> TypedBindings

mapHiding :: (Hiding -> Hiding) -> TypedBindings -> TypedBindings

LensHiding LamBinding

Methods

getHiding :: LamBinding -> Hiding

setHiding :: Hiding -> LamBinding -> LamBinding

mapHiding :: (Hiding -> Hiding) -> LamBinding -> LamBinding

ExprLike TypedBindings

Methods

mapExpr :: (Expr -> Expr) -> TypedBindings -> TypedBindings

traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBindings -> m TypedBindings

foldExpr :: Monoid m => (Expr -> m) -> TypedBindings -> m

ExprLike LamBinding

Methods

mapExpr :: (Expr -> Expr) -> LamBinding -> LamBinding

traverseExpr :: Monad m => (Expr -> m Expr) -> LamBinding -> m LamBinding

foldExpr :: Monoid m => (Expr -> m) -> LamBinding -> m

ToConcrete TypedBinding TypedBinding

Methods

toConcrete :: TypedBinding -> AbsToCon TypedBinding

bindToConcrete :: TypedBinding -> (TypedBinding -> AbsToCon b) -> AbsToCon b

ToAbstract TypedBinding TypedBinding

Methods

toAbstract :: TypedBinding -> ScopeM TypedBinding

ToAbstract TypedBindings TypedBindings

Methods

toAbstract :: TypedBindings -> ScopeM TypedBindings

ToAbstract LamBinding LamBinding

Methods

toAbstract :: LamBinding -> ScopeM LamBinding

ToConcrete TypedBindings [TypedBindings]

Methods

toConcrete :: TypedBindings -> AbsToCon [TypedBindings]

bindToConcrete :: TypedBindings -> ([TypedBindings] -> AbsToCon b) -> AbsToCon b

ToConcrete LamBinding [LamBinding]

Methods

toConcrete :: LamBinding -> AbsToCon [LamBinding]

bindToConcrete :: LamBinding -> ([LamBinding] -> AbsToCon b) -> AbsToCon b

NFData a => NFData (TypedBinding' a)

Ranges are not forced.

Methods

rnf :: TypedBinding' a -> ()

ExprLike a => ExprLike (TypedBinding' a)

Methods

mapExpr :: (Expr -> Expr) -> TypedBinding' a -> TypedBinding' a

traverseExpr :: Monad m => (Expr -> m Expr) -> TypedBinding' a -> m (TypedBinding' a)

foldExpr :: Monoid m => (Expr -> m) -> TypedBinding' a -> m

type RecordAssignment = Either FieldAssignment ModuleAssignment

type RecordAssignments = [RecordAssignment]

type FieldAssignment = FieldAssignment' Expr

data FieldAssignment' a

Constructors

FieldAssignment

Fields

• _nameFieldA :: Name
• _exprFieldA :: a

Instances

Functor FieldAssignment'

Methods

fmap :: (a -> b) -> FieldAssignment' a -> FieldAssignment' b

(<$) :: a -> FieldAssignment' b -> FieldAssignment' a

Foldable FieldAssignment'

Methods

fold :: Monoid m => FieldAssignment' m -> 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'

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)

ExprLike FieldAssignment

Methods

mapExpr :: (Expr -> Expr) -> FieldAssignment -> FieldAssignment

traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment -> m FieldAssignment

foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment -> m

SubstExpr Assign

Methods

substExpr :: [(Name, Expr)] -> Assign -> Assign

Eq a => Eq (FieldAssignment' a)

Methods

(==) :: FieldAssignment' a -> FieldAssignment' a -> Bool

(/=) :: FieldAssignment' a -> FieldAssignment' a -> Bool

Show a => Show (FieldAssignment' a)

Methods

showsPrec :: Int -> FieldAssignment' a -> ShowS

show :: FieldAssignment' a -> String

showList :: [FieldAssignment' a] -> ShowS

NFData a => NFData (FieldAssignment' a)

Methods

rnf :: FieldAssignment' a -> ()

KillRange a => KillRange (FieldAssignment' a)

Methods

killRange :: KillRangeT (FieldAssignment' a)

HasRange a => HasRange (FieldAssignment' a)

Methods

getRange :: FieldAssignment' a -> Range

ExprLike a => ExprLike (FieldAssignment' a)

Methods

recurseExpr :: Applicative m => (Expr -> m Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a)

foldExpr :: Monoid m => (Expr -> m) -> FieldAssignment' a -> m

traverseExpr :: Monad m => (Expr -> m Expr) -> FieldAssignment' a -> m (FieldAssignment' a)

mapExpr :: (Expr -> Expr) -> FieldAssignment' a -> FieldAssignment' a

NamesIn a => NamesIn (FieldAssignment' a)

Methods

namesIn :: FieldAssignment' a -> Set QName

ExpandPatternSynonyms a => ExpandPatternSynonyms (FieldAssignment' a)

Methods

expandPatternSynonyms :: FieldAssignment' a -> TCM (FieldAssignment' a)

ToConcrete a c => ToConcrete (FieldAssignment' a) (FieldAssignment' c)

Methods

toConcrete :: FieldAssignment' a -> AbsToCon (FieldAssignment' c)

bindToConcrete :: FieldAssignment' a -> (FieldAssignment' c -> AbsToCon b) -> AbsToCon b

ToAbstract c a => ToAbstract (FieldAssignment' c) (FieldAssignment' a)

Methods

toAbstract :: FieldAssignment' c -> ScopeM (FieldAssignment' a)

nameFieldA :: Lens' Name (FieldAssignment' a)

exprFieldA :: Lens' a (FieldAssignment' a)

data ModuleAssignment

Constructors

ModuleAssignment

Fields

• _qnameModA :: QName
• _exprModA :: [Expr]
• _importDirModA :: ImportDirective

Instances

NFData ModuleAssignment

Methods

rnf :: ModuleAssignment -> ()

KillRange ModuleAssignment

Methods

killRange :: KillRangeT ModuleAssignment

HasRange ModuleAssignment

Methods

getRange :: ModuleAssignment -> Range

ExprLike ModuleAssignment

Methods

mapExpr :: (Expr -> Expr) -> ModuleAssignment -> ModuleAssignment

traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleAssignment -> m ModuleAssignment

foldExpr :: Monoid m => (Expr -> m) -> ModuleAssignment -> m

ToAbstract ModuleAssignment (ModuleName, [LetBinding])

Methods

toAbstract :: ModuleAssignment -> ScopeM (ModuleName, [LetBinding])

data BoundName

Constructors

BName

Fields

• boundName :: Name
• boundLabel :: Name

  for implicit function types the label matters and can't be alpha-renamed

• bnameFixity :: Fixity'

Instances

NFData BoundName

Methods

rnf :: BoundName -> ()

KillRange BoundName

Methods

killRange :: KillRangeT BoundName

HasRange BoundName

Methods

getRange :: BoundName -> Range

ToAbstract (NewName BoundName) Name

Methods

toAbstract :: NewName BoundName -> ScopeM Name

mkBoundName_ :: Name -> BoundName

mkBoundName :: Name -> Fixity' -> BoundName

type Telescope = [TypedBindings]

A telescope is a sequence of typed bindings. Bound variables are in scope in later types.

countTelVars :: Telescope -> Nat

Declarations

data Declaration

The representation type of a declaration. The comments indicate which type in the intended family the constructor targets.

Constructors

TypeSig ArgInfo Name Expr

Axioms and functions can be irrelevant. (Hiding should be NotHidden)

Field IsInstance Name (Arg Expr)

Record field, can be hidden and/or irrelevant.

FunClause LHS RHS WhereClause Bool

DataSig Range Induction Name [LamBinding] Expr

lone data signature in mutual block

Data Range Induction Name [LamBinding] (Maybe Expr) [TypeSignatureOrInstanceBlock]

RecordSig Range Name [LamBinding] Expr

lone record signature in mutual block

Record Range Name (Maybe (Ranged Induction)) (Maybe Bool) (Maybe (Name, IsInstance)) [LamBinding] (Maybe Expr) [Declaration]

The optional name is a name for the record constructor.

Infix Fixity [Name]

Syntax Name Notation

notation declaration for a name

PatternSyn Range Name [Arg Name] Pattern

Mutual Range [Declaration]

Abstract Range [Declaration]

Private Range [Declaration]

InstanceB Range [Declaration]

Macro Range [Declaration]

Postulate Range [TypeSignatureOrInstanceBlock]

Primitive Range [TypeSignature]

Open Range QName ImportDirective

Import Range QName (Maybe AsName) !OpenShortHand ImportDirective

ModuleMacro Range Name ModuleApplication !OpenShortHand ImportDirective

Module Range QName [TypedBindings] [Declaration]

UnquoteDecl Range [Name] Expr

UnquoteDef Range [Name] Expr

Pragma Pragma

Instances

NFData Declaration

Ranges are not forced.

Methods

rnf :: Declaration -> ()

KillRange Declaration

Methods

killRange :: KillRangeT Declaration

KillRange WhereClause

Methods

killRange :: KillRangeT WhereClause

HasRange Declaration

Methods

getRange :: Declaration -> Range

HasRange WhereClause

Methods

getRange :: WhereClause -> Range

ExprLike Declaration

Methods

mapExpr :: (Expr -> Expr) -> Declaration -> Declaration

traverseExpr :: Monad m => (Expr -> m Expr) -> Declaration -> m Declaration

foldExpr :: Monoid m => (Expr -> m) -> Declaration -> m

ToConcrete LetBinding [Declaration]

Methods

toConcrete :: LetBinding -> AbsToCon [Declaration]

bindToConcrete :: LetBinding -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToConcrete Declaration [Declaration]

Methods

toConcrete :: Declaration -> AbsToCon [Declaration]

bindToConcrete :: Declaration -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Methods

toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration])

bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b

ToConcrete (Constr Constructor) Declaration

Methods

toConcrete :: Constr Constructor -> AbsToCon Declaration

bindToConcrete :: Constr Constructor -> (Declaration -> AbsToCon b) -> AbsToCon b

ToAbstract (TopLevel [Declaration]) TopLevelInfo

Top-level declarations are always (import|open)* -- a bunch of possibly opened imports module ThisModule ... -- the top-level module of this file

Methods

toAbstract :: TopLevel [Declaration] -> ScopeM TopLevelInfo

ToConcrete a LHS => ToConcrete (Clause' a) [Declaration]

Methods

toConcrete :: Clause' a -> AbsToCon [Declaration]

bindToConcrete :: Clause' a -> ([Declaration] -> AbsToCon b) -> AbsToCon b

ToAbstract [Declaration] [Declaration]

Methods

toAbstract :: [Declaration] -> ScopeM [Declaration]

data ModuleApplication

Constructors

SectionApp Range [TypedBindings] Expr

tel. M args

RecordModuleIFS Range QName

M {{...}}

Instances

NFData ModuleApplication

Ranges are not forced.

Methods

rnf :: ModuleApplication -> ()

KillRange ModuleApplication

Methods

killRange :: KillRangeT ModuleApplication

HasRange ModuleApplication

Methods

getRange :: ModuleApplication -> Range

ExprLike ModuleApplication

Methods

mapExpr :: (Expr -> Expr) -> ModuleApplication -> ModuleApplication

traverseExpr :: Monad m => (Expr -> m Expr) -> ModuleApplication -> m ModuleApplication

foldExpr :: Monoid m => (Expr -> m) -> ModuleApplication -> m

ToConcrete ModuleApplication ModuleApplication

Methods

toConcrete :: ModuleApplication -> AbsToCon ModuleApplication

bindToConcrete :: ModuleApplication -> (ModuleApplication -> AbsToCon b) -> AbsToCon b

type TypeSignature = Declaration

Just type signatures.

type TypeSignatureOrInstanceBlock = Declaration

Just type signatures or instance blocks.

type ImportDirective = ImportDirective' Name Name

The things you are allowed to say when you shuffle names between name spaces (i.e. in import, namespace, or open declarations).

type Using = Using' Name Name

type ImportedName = ImportedName' Name Name

An imported name can be a module or a defined name.

type Renaming = Renaming' Name Name

data AsName

Constructors

AsName

Fields

• asName :: Name

  The "as" name.

• asRange :: Range

  The range of the "as" keyword. Retained for highlighting purposes.

Instances

Show AsName

Methods

showsPrec :: Int -> AsName -> ShowS

show :: AsName -> String

showList :: [AsName] -> ShowS

NFData AsName

Ranges are not forced.

Methods

rnf :: AsName -> ()

KillRange AsName

Methods

killRange :: KillRangeT AsName

HasRange AsName

Methods

getRange :: AsName -> Range

data OpenShortHand

Constructors

DoOpen

DontOpen

Instances

Eq OpenShortHand

Methods

(==) :: OpenShortHand -> OpenShortHand -> Bool

(/=) :: OpenShortHand -> OpenShortHand -> Bool

Show OpenShortHand

Methods

showsPrec :: Int -> OpenShortHand -> ShowS

show :: OpenShortHand -> String

showList :: [OpenShortHand] -> ShowS

type RewriteEqn = Expr

type WithExpr = Expr

data LHS

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, with-patterns, rewrite equations and with-expressions

Fields

• lhsOriginalPattern :: Pattern

  f ps

• lhsWithPattern :: [Pattern]

  | p (many)

• lhsRewriteEqn :: [RewriteEqn]

  rewrite e (many)

• lhsWithExpr :: [WithExpr]

  with e (many)

Ellipsis Range [Pattern] [RewriteEqn] [WithExpr]

new with-patterns, rewrite equations and with-expressions

Instances

NFData LHS

Ranges are not forced.

Methods

rnf :: LHS -> ()

KillRange LHS

Methods

killRange :: KillRangeT LHS

HasRange LHS

Methods

getRange :: LHS -> Range

ExprLike LHS

Methods

mapExpr :: (Expr -> Expr) -> LHS -> LHS

traverseExpr :: Monad m => (Expr -> m Expr) -> LHS -> m LHS

foldExpr :: Monoid m => (Expr -> m) -> LHS -> m

ToConcrete LHS LHS

Methods

toConcrete :: LHS -> AbsToCon LHS

bindToConcrete :: LHS -> (LHS -> AbsToCon b) -> AbsToCon b

ToConcrete SpineLHS LHS

Methods

toConcrete :: SpineLHS -> AbsToCon LHS

bindToConcrete :: SpineLHS -> (LHS -> AbsToCon b) -> AbsToCon b

data Pattern

Concrete patterns. No literals in patterns at the moment.

Constructors

IdentP QName

c or x

QuoteP Range

quote

AppP Pattern (NamedArg Pattern)

p p' or p {x = p'}

RawAppP Range [Pattern]

p1..pn before parsing operators

OpAppP Range QName (Set Name) [NamedArg Pattern]

eg: p => p' for operator _=>_ The QName is possibly ambiguous, but it must correspond to one of the names in the set.

HiddenP Range (Named_ Pattern)

{p} or {x = p}

InstanceP Range (Named_ Pattern)

{{p}} or {{x = p}}

ParenP Range Pattern

(p)

WildP Range

_

AbsurdP Range

()

AsP Range Name Pattern

x@p unused

DotP Range Expr

.e

LitP Literal

0, 1, etc.

RecP Range [FieldAssignment' Pattern]

record {x = p; y = q}

Instances

NFData Pattern

Ranges are not forced.

Methods

rnf :: Pattern -> ()

KillRange Pattern

Methods

killRange :: KillRangeT Pattern

SetRange Pattern

Methods

setRange :: Range -> Pattern -> Pattern

HasRange Pattern

Methods

getRange :: Pattern -> Range

IsExpr Pattern

Methods

exprView :: Pattern -> ExprView Pattern

unExprView :: ExprView Pattern -> Pattern

ToConcrete Pattern Pattern

Methods

toConcrete :: Pattern -> AbsToCon Pattern

bindToConcrete :: Pattern -> (Pattern -> AbsToCon b) -> AbsToCon b

ToConcrete LHSCore Pattern

Methods

toConcrete :: LHSCore -> AbsToCon Pattern

bindToConcrete :: LHSCore -> (Pattern -> AbsToCon b) -> AbsToCon b

ToAbstract Pattern (Pattern' Expr)

Methods

toAbstract :: Pattern -> ScopeM (Pattern' Expr)

data LHSCore

Processed (scope-checked) intermediate form of the core f ps of LHS. Corresponds to lhsOriginalPattern.

Constructors

LHSHead

Fields

• lhsDefName :: QName

  f

• lhsPats :: [NamedArg Pattern]

  ps

LHSProj

Fields

• lhsDestructor :: QName

  record projection identifier

• lhsPatsLeft :: [NamedArg Pattern]

  side patterns

• lhsFocus :: NamedArg LHSCore

  main branch

• lhsPatsRight :: [NamedArg Pattern]

  side patterns

Instances

HasRange LHSCore

Methods

getRange :: LHSCore -> Range

ToAbstract LHSCore (LHSCore' Expr)

Methods

toAbstract :: LHSCore -> ScopeM (LHSCore' Expr)

type RHS = RHS' Expr

data RHS' e

Constructors

AbsurdRHS

No right hand side because of absurd match.

RHS e

Instances

Functor RHS'

Methods

fmap :: (a -> b) -> RHS' a -> RHS' b

(<$) :: a -> RHS' b -> RHS' a

Foldable RHS'

Methods

fold :: Monoid m => RHS' m -> 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

toList :: RHS' a -> [a]

null :: RHS' a -> Bool

length :: RHS' a -> Int

elem :: Eq a => a -> RHS' a -> Bool

maximum :: Ord a => RHS' a -> a

minimum :: Ord a => RHS' a -> a

sum :: Num a => RHS' a -> a

product :: Num a => RHS' a -> a

Traversable RHS'

Methods

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

sequenceA :: Applicative f => RHS' (f a) -> f (RHS' a)

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

sequence :: Monad m => RHS' (m a) -> m (RHS' a)

KillRange RHS

Methods

killRange :: KillRangeT RHS

HasRange RHS

Methods

getRange :: RHS -> Range

ToAbstract RHS AbstractRHS

Methods

toAbstract :: RHS -> ScopeM AbstractRHS

ToConcrete RHS (RHS, [Expr], [Expr], [Declaration])

Methods

toConcrete :: RHS -> AbsToCon (RHS, [Expr], [Expr], [Declaration])

bindToConcrete :: RHS -> ((RHS, [Expr], [Expr], [Declaration]) -> AbsToCon b) -> AbsToCon b

NFData a => NFData (RHS' a)

Methods

rnf :: RHS' a -> ()

ExprLike a => ExprLike (RHS' a)

Methods

mapExpr :: (Expr -> Expr) -> RHS' a -> RHS' a

traverseExpr :: Monad m => (Expr -> m Expr) -> RHS' a -> m (RHS' a)

foldExpr :: Monoid m => (Expr -> m) -> RHS' a -> m

type WhereClause = WhereClause' [Declaration]

data WhereClause' decls

Constructors

NoWhere

No where clauses.

AnyWhere decls

Ordinary where.

SomeWhere Name decls

Named where: module M where.

Instances

Functor WhereClause'

Methods

fmap :: (a -> b) -> WhereClause' a -> WhereClause' b

(<$) :: a -> WhereClause' b -> WhereClause' a

Foldable WhereClause'

Methods

fold :: Monoid m => WhereClause' m -> 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'

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)

KillRange WhereClause

Methods

killRange :: KillRangeT WhereClause

HasRange WhereClause

Methods

getRange :: WhereClause -> Range

NFData a => NFData (WhereClause' a)

Methods

rnf :: WhereClause' a -> ()

Null (WhereClause' a)

A WhereClause is null when the where keyword is absent. An empty list of declarations does not count as null here.

Methods

empty :: WhereClause' a

null :: WhereClause' a -> Bool

ExprLike a => ExprLike (WhereClause' a)

Methods

mapExpr :: (Expr -> Expr) -> WhereClause' a -> WhereClause' a

traverseExpr :: Monad m => (Expr -> m Expr) -> WhereClause' a -> m (WhereClause' a)

foldExpr :: Monoid m => (Expr -> m) -> WhereClause' a -> m

data ExprWhere

An expression followed by a where clause. Currently only used to give better a better error message in interaction.

Constructors

ExprWhere Expr WhereClause

data Pragma

Constructors

OptionsPragma Range [String]

BuiltinPragma Range String Expr

RewritePragma Range QName

CompiledDataPragma Range QName String [String]

CompiledDeclareDataPragma Range QName String

CompiledTypePragma Range QName String

CompiledPragma Range QName String

CompiledExportPragma Range QName String

CompiledEpicPragma Range QName String

CompiledJSPragma Range QName String

CompiledUHCPragma Range QName String

CompiledDataUHCPragma Range QName String [String]

HaskellCodePragma Range String

NoSmashingPragma Range QName

StaticPragma Range QName

InlinePragma Range QName

ImportPragma Range String

Invariant: The string must be a valid Haskell module name.

ImportUHCPragma Range String

same as above, but for the UHC backend

ImpossiblePragma Range

TerminationCheckPragma Range (TerminationCheck Name)

CatchallPragma Range

DisplayPragma Range Pattern Expr

NoPositivityCheckPragma Range

Instances

NFData Pragma

Ranges are not forced.

Methods

rnf :: Pragma -> ()

KillRange Pragma

Methods

killRange :: KillRangeT Pragma

HasRange Pragma

Methods

getRange :: Pragma -> Range

ToConcrete RangeAndPragma Pragma

Methods

toConcrete :: RangeAndPragma -> AbsToCon Pragma

bindToConcrete :: RangeAndPragma -> (Pragma -> AbsToCon b) -> AbsToCon b

ToAbstract Pragma [Pragma]

Methods

toAbstract :: Pragma -> ScopeM [Pragma]

type Module = ([Pragma], [Declaration])

Modules: Top-level pragmas plus other top-level declarations.

data ThingWithFixity x

Decorating something with Fixity'.

Constructors

ThingWithFixity x Fixity'

Instances

Functor ThingWithFixity

Methods

fmap :: (a -> b) -> ThingWithFixity a -> ThingWithFixity b

(<$) :: a -> ThingWithFixity b -> ThingWithFixity a

Foldable ThingWithFixity

Methods

fold :: Monoid m => ThingWithFixity m -> 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

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)

Show x => Show (ThingWithFixity x)

Methods

showsPrec :: Int -> ThingWithFixity x -> ShowS

show :: ThingWithFixity x -> String

showList :: [ThingWithFixity x] -> ShowS

KillRange x => KillRange (ThingWithFixity x)

Methods

killRange :: KillRangeT (ThingWithFixity x)

topLevelModuleName :: Module -> TopLevelModuleName

Computes the top-level module name.

Precondition: The Module has to be well-formed. This means that there are only allowed declarations before the first module declaration, typically import declarations. See spanAllowedBeforeModule.

spanAllowedBeforeModule :: [Declaration] -> ([Declaration], [Declaration])

Splits off allowed (= import) declarations before the first non-allowed declaration. After successful parsing, the first non-allowed declaration should be a module declaration.

Pattern tools

patternNames :: Pattern -> [Name]

Get all the identifiers in a pattern in left-to-right order.

patternQNames :: Pattern -> [QName]

Get all the identifiers in a pattern in left-to-right order.

Lenses

mapLhsOriginalPattern :: (Pattern -> Pattern) -> LHS -> LHS