module Agda.Syntax.Notation where
import Prelude hiding (null)
import Control.DeepSeq
import Control.Monad
import Control.Monad.Except
import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import GHC.Generics (Generic)
import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Concrete.Pretty()
import Agda.Syntax.Position
import Agda.Utils.Lens
import Agda.Utils.List
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Pretty
import Agda.Utils.Impossible
data HoleName
= LambdaHole { HoleName -> RString
_bindHoleName :: RString
, HoleName -> RString
holeName :: RString }
| ExprHole { holeName :: RString }
isLambdaHole :: HoleName -> Bool
isLambdaHole :: HoleName -> Bool
isLambdaHole (LambdaHole RString
_ RString
_) = Bool
True
isLambdaHole HoleName
_ = Bool
False
stringParts :: Notation -> [String]
stringParts :: Notation -> [[Char]]
stringParts Notation
gs = [ forall a. Ranged a -> a
rangedThing RString
x | IdPart RString
x <- Notation
gs ]
holeTarget :: GenPart -> Maybe Int
holeTarget :: GenPart -> Maybe Int
holeTarget (BindHole Range
_ Ranged Int
n) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Ranged a -> a
rangedThing Ranged Int
n
holeTarget (WildHole Ranged Int
n) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Ranged a -> a
rangedThing Ranged Int
n
holeTarget (NormalHole Range
_ NamedArg (Ranged Int)
n) = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall a. Ranged a -> a
rangedThing forall a b. (a -> b) -> a -> b
$ forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
n
holeTarget IdPart{} = forall a. Maybe a
Nothing
isAHole :: GenPart -> Bool
isAHole :: GenPart -> Bool
isAHole BindHole{} = Bool
True
isAHole NormalHole{} = Bool
True
isAHole WildHole{} = Bool
False
isAHole IdPart{} = Bool
False
isNormalHole :: GenPart -> Bool
isNormalHole :: GenPart -> Bool
isNormalHole NormalHole{} = Bool
True
isNormalHole BindHole{} = Bool
False
isNormalHole WildHole{} = Bool
False
isNormalHole IdPart{} = Bool
False
isBindingHole :: GenPart -> Bool
isBindingHole :: GenPart -> Bool
isBindingHole BindHole{} = Bool
True
isBindingHole WildHole{} = Bool
True
isBindingHole GenPart
_ = Bool
False
data NotationKind
= InfixNotation
| PrefixNotation
| PostfixNotation
| NonfixNotation
| NoNotation
deriving (NotationKind -> NotationKind -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: NotationKind -> NotationKind -> Bool
$c/= :: NotationKind -> NotationKind -> Bool
== :: NotationKind -> NotationKind -> Bool
$c== :: NotationKind -> NotationKind -> Bool
Eq, Int -> NotationKind -> ShowS
[NotationKind] -> ShowS
NotationKind -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [NotationKind] -> ShowS
$cshowList :: [NotationKind] -> ShowS
show :: NotationKind -> [Char]
$cshow :: NotationKind -> [Char]
showsPrec :: Int -> NotationKind -> ShowS
$cshowsPrec :: Int -> NotationKind -> ShowS
Show, forall x. Rep NotationKind x -> NotationKind
forall x. NotationKind -> Rep NotationKind x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NotationKind x -> NotationKind
$cfrom :: forall x. NotationKind -> Rep NotationKind x
Generic)
notationKind :: Notation -> NotationKind
notationKind :: Notation -> NotationKind
notationKind [] = NotationKind
NoNotation
notationKind (GenPart
h:Notation
syn) =
case (GenPart -> Bool
isNormalHole GenPart
h, GenPart -> Bool
isNormalHole forall a b. (a -> b) -> a -> b
$ forall a. a -> [a] -> a
last1 GenPart
h Notation
syn) of
(Bool
True , Bool
True ) -> NotationKind
InfixNotation
(Bool
True , Bool
False) -> NotationKind
PostfixNotation
(Bool
False, Bool
True ) -> NotationKind
PrefixNotation
(Bool
False, Bool
False) -> NotationKind
NonfixNotation
mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
mkNotation :: [NamedArg HoleName] -> [RString] -> Either [Char] Notation
mkNotation [NamedArg HoleName]
_ [] = forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"empty notation is disallowed"
mkNotation [NamedArg HoleName]
holes [RString]
ids = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
uniqueHoleNames forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use unique argument names"
let Notation
xs :: Notation = forall a b. (a -> b) -> [a] -> [b]
map RString -> GenPart
mkPart [RString]
ids
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
noAdjacentHoles Notation
xs) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError forall a b. (a -> b) -> a -> b
$ forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char]
"syntax must not contain adjacent holes ("
, [Char]
prettyHoles
, [Char]
")"
]
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isExprLinear Notation
xs) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use holes exactly once"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isLambdaLinear Notation
xs) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use binding holes exactly once"
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Notation -> Bool
isSingleHole Notation
xs) forall a b. (a -> b) -> a -> b
$ forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax cannot be a single hole"
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Notation -> Notation
insertWildHoles Notation
xs
where
holeNames :: [RString]
holeNames :: [RString]
holeNames = forall a b. (a -> b) -> [a] -> [b]
map forall a. NamedArg a -> a
namedArg [NamedArg HoleName]
holes forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LambdaHole RString
x RString
y -> [RString
x, RString
y]
ExprHole RString
y -> [RString
y]
prettyHoles :: String
prettyHoles :: [Char]
prettyHoles = [[Char]] -> [Char]
List.unwords forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map (ShowS
rawNameToString forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. Ranged a -> a
rangedThing) [RString]
holeNames
mkPart :: RString -> GenPart
mkPart RString
ident = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (RString -> GenPart
IdPart RString
ident) (forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` RString
ident) forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup RString
ident [(RString, GenPart)]
holeMap
holeNumbers :: [Int]
holeNumbers = [Int
0 .. forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg HoleName]
holes forall a. Num a => a -> a -> a
- Int
1]
numberedHoles :: [(Int, NamedArg HoleName)]
numberedHoles :: [(Int, NamedArg HoleName)]
numberedHoles = forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
holeNumbers [NamedArg HoleName]
holes
insertWildHoles :: [GenPart] -> [GenPart]
insertWildHoles :: Notation -> Notation
insertWildHoles Notation
xs = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ranged Int -> Notation -> Notation
ins Notation
xs [Ranged Int]
wilds
where
wilds :: [Ranged Int]
wilds = [ Ranged Int
i | (RString
_, WildHole Ranged Int
i) <- [(RString, GenPart)]
holeMap ]
ins :: Ranged Int -> Notation -> Notation
ins Ranged Int
w (NormalHole Range
r NamedArg (Ranged Int)
h : Notation
hs)
| forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
h forall a. Eq a => a -> a -> Bool
== Ranged Int
w = Range -> NamedArg (Ranged Int) -> GenPart
NormalHole Range
r NamedArg (Ranged Int)
h forall a. a -> [a] -> [a]
: Ranged Int -> GenPart
WildHole Ranged Int
w forall a. a -> [a] -> [a]
: Notation
hs
ins Ranged Int
w (GenPart
h : Notation
hs) = GenPart
h forall a. a -> [a] -> [a]
: Ranged Int -> Notation -> Notation
insBefore Ranged Int
w Notation
hs
ins Ranged Int
_ [] = forall a. HasCallStack => a
__IMPOSSIBLE__
insBefore :: Ranged Int -> Notation -> Notation
insBefore Ranged Int
w (NormalHole Range
r NamedArg (Ranged Int)
h : Notation
hs)
| forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
h forall a. Eq a => a -> a -> Bool
== Ranged Int
w = Ranged Int -> GenPart
WildHole Ranged Int
w forall a. a -> [a] -> [a]
: Range -> NamedArg (Ranged Int) -> GenPart
NormalHole Range
r NamedArg (Ranged Int)
h forall a. a -> [a] -> [a]
: Notation
hs
insBefore Ranged Int
w (GenPart
h : Notation
hs) = GenPart
h forall a. a -> [a] -> [a]
: Ranged Int -> Notation -> Notation
insBefore Ranged Int
w Notation
hs
insBefore Ranged Int
_ [] = forall a. HasCallStack => a
__IMPOSSIBLE__
holeMap :: [(RString, GenPart)]
holeMap :: [(RString, GenPart)]
holeMap = do
(Int
i, NamedArg HoleName
h) <- [(Int, NamedArg HoleName)]
numberedHoles
let ri :: RString -> Ranged Int
ri RString
x = forall a. Range -> a -> Ranged a
Ranged (forall a. HasRange a => a -> Range
getRange RString
x) Int
i
normalHole :: RString -> GenPart
normalHole RString
y = Range -> NamedArg (Ranged Int) -> GenPart
NormalHole forall a. Range' a
noRange forall a b. (a -> b) -> a -> b
$ forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (RString -> Ranged Int
ri RString
y forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) NamedArg HoleName
h
case forall a. NamedArg a -> a
namedArg NamedArg HoleName
h of
ExprHole RString
y -> [(RString
y, RString -> GenPart
normalHole RString
y)]
LambdaHole RString
x RString
y
| [Char]
"_" <- forall a. Ranged a -> a
rangedThing RString
x -> [(RString
x, Ranged Int -> GenPart
WildHole (RString -> Ranged Int
ri RString
x)), (RString
y, RString -> GenPart
normalHole RString
y)]
| Bool
otherwise -> [(RString
x, Range -> Ranged Int -> GenPart
BindHole forall a. Range' a
noRange (RString -> Ranged Int
ri RString
x)), (RString
y, RString -> GenPart
normalHole RString
y)]
uniqueHoleNames :: Bool
uniqueHoleNames = forall a. Eq a => [a] -> Bool
distinct [ RString
x | (RString
x, GenPart
_) <- [(RString, GenPart)]
holeMap, forall a. Ranged a -> a
rangedThing RString
x forall a. Eq a => a -> a -> Bool
/= [Char]
"_" ]
isExprLinear :: Notation -> Bool
isExprLinear Notation
xs = forall a. Ord a => [a] -> [a]
List.sort [ Int
i | GenPart
x <- Notation
xs, GenPart -> Bool
isNormalHole GenPart
x, let Just Int
i = GenPart -> Maybe Int
holeTarget GenPart
x ] forall a. Eq a => a -> a -> Bool
== [Int]
holeNumbers
isLambdaLinear :: Notation -> Bool
isLambdaLinear Notation
xs = forall a. Ord a => [a] -> [a]
List.sort [ forall a. Ranged a -> a
rangedThing Ranged Int
x | BindHole Range
_ Ranged Int
x <- Notation
xs ] forall a. Eq a => a -> a -> Bool
==
[ Int
i | (Int
i, NamedArg HoleName
h) <- [(Int, NamedArg HoleName)]
numberedHoles,
LambdaHole RString
x RString
_ <- [forall a. NamedArg a -> a
namedArg NamedArg HoleName
h], forall a. Ranged a -> a
rangedThing RString
x forall a. Eq a => a -> a -> Bool
/= [Char]
"_" ]
noAdjacentHoles :: [GenPart] -> Bool
noAdjacentHoles :: Notation -> Bool
noAdjacentHoles [] = forall a. HasCallStack => a
__IMPOSSIBLE__
noAdjacentHoles [GenPart
x] = Bool
True
noAdjacentHoles (GenPart
x:GenPart
y:Notation
xs) =
Bool -> Bool
not (GenPart -> Bool
isAHole GenPart
x Bool -> Bool -> Bool
&& GenPart -> Bool
isAHole GenPart
y) Bool -> Bool -> Bool
&& Notation -> Bool
noAdjacentHoles (GenPart
yforall a. a -> [a] -> [a]
:Notation
xs)
isSingleHole :: [GenPart] -> Bool
isSingleHole :: Notation -> Bool
isSingleHole = \case
[ IdPart{} ] -> Bool
False
[ GenPart
_hole ] -> Bool
True
Notation
_ -> Bool
False
data NewNotation = NewNotation
{ NewNotation -> QName
notaName :: QName
, NewNotation -> Set Name
notaNames :: Set A.Name
, NewNotation -> Fixity
notaFixity :: Fixity
, NewNotation -> Notation
notation :: Notation
, NewNotation -> Bool
notaIsOperator :: Bool
} deriving (Int -> NewNotation -> ShowS
[NewNotation] -> ShowS
NewNotation -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [NewNotation] -> ShowS
$cshowList :: [NewNotation] -> ShowS
show :: NewNotation -> [Char]
$cshow :: NewNotation -> [Char]
showsPrec :: Int -> NewNotation -> ShowS
$cshowsPrec :: Int -> NewNotation -> ShowS
Show, forall x. Rep NewNotation x -> NewNotation
forall x. NewNotation -> Rep NewNotation x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NewNotation x -> NewNotation
$cfrom :: forall x. NewNotation -> Rep NewNotation x
Generic)
instance LensFixity NewNotation where
lensFixity :: Lens' Fixity NewNotation
lensFixity Fixity -> f Fixity
f NewNotation
nota = Fixity -> f Fixity
f (NewNotation -> Fixity
notaFixity NewNotation
nota) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \ Fixity
fx -> NewNotation
nota { notaFixity :: Fixity
notaFixity = Fixity
fx }
namesToNotation :: QName -> A.Name -> NewNotation
namesToNotation :: QName -> Name -> NewNotation
namesToNotation QName
q Name
n = NewNotation
{ notaName :: QName
notaName = QName
q
, notaNames :: Set Name
notaNames = forall a. a -> Set a
Set.singleton Name
n
, notaFixity :: Fixity
notaFixity = Fixity
f
, notation :: Notation
notation = if forall a. Null a => a -> Bool
null Notation
syn then Name -> Notation
syntaxOf (QName -> Name
unqualify QName
q) else Notation
syn
, notaIsOperator :: Bool
notaIsOperator = forall a. Null a => a -> Bool
null Notation
syn
}
where Fixity' Fixity
f Notation
syn Range
_ = Name -> Fixity'
A.nameFixity Name
n
useDefaultFixity :: NewNotation -> NewNotation
useDefaultFixity :: NewNotation -> NewNotation
useDefaultFixity NewNotation
n
| NewNotation -> Fixity
notaFixity NewNotation
n forall a. Eq a => a -> a -> Bool
== Fixity
noFixity = NewNotation
n { notaFixity :: Fixity
notaFixity = Fixity
defaultFixity }
| Bool
otherwise = NewNotation
n
notationNames :: NewNotation -> [QName]
notationNames :: NewNotation -> [QName]
notationNames (NewNotation QName
q Set Name
_ Fixity
_ Notation
parts Bool
_) =
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith forall a b. (a -> b) -> a -> b
($) (Name -> QName
reQualify forall a. a -> [a] -> [a]
: forall a. a -> [a]
repeat Name -> QName
QName) [[Char] -> Name
simpleName forall a b. (a -> b) -> a -> b
$ forall a. Ranged a -> a
rangedThing RString
x | IdPart RString
x <- Notation
parts ]
where
modules :: [Name]
modules = forall a. NonEmpty a -> [a]
List1.init (QName -> List1 Name
qnameParts QName
q)
reQualify :: Name -> QName
reQualify Name
x = forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
List.foldr Name -> QName -> QName
Qual (Name -> QName
QName Name
x) [Name]
modules
syntaxOf :: Name -> Notation
syntaxOf :: Name -> Notation
syntaxOf Name
y
| Name -> Bool
isOperator Name
y = Int -> [NamePart] -> Notation
mkSyn Int
0 forall a b. (a -> b) -> a -> b
$ forall a. NonEmpty a -> [a]
List1.toList forall a b. (a -> b) -> a -> b
$ Name -> NameParts
nameNameParts Name
y
| Bool
otherwise = Notation
noNotation
where
mkSyn :: Int -> [NamePart] -> Notation
mkSyn :: Int -> [NamePart] -> Notation
mkSyn Int
n [] = []
mkSyn Int
n (NamePart
Hole : [NamePart]
xs) = Range -> NamedArg (Ranged Int) -> GenPart
NormalHole forall a. Range' a
noRange (forall a. a -> NamedArg a
defaultNamedArg forall a b. (a -> b) -> a -> b
$ forall a. a -> Ranged a
unranged Int
n) forall a. a -> [a] -> [a]
: Int -> [NamePart] -> Notation
mkSyn (Int
1 forall a. Num a => a -> a -> a
+ Int
n) [NamePart]
xs
mkSyn Int
n (Id [Char]
x : [NamePart]
xs) = RString -> GenPart
IdPart (forall a. a -> Ranged a
unranged [Char]
x) forall a. a -> [a] -> [a]
: Int -> [NamePart] -> Notation
mkSyn Int
n [NamePart]
xs
mergeNotations :: [NewNotation] -> [NewNotation]
mergeNotations :: [NewNotation] -> [NewNotation]
mergeNotations =
forall a b. (a -> b) -> [a] -> [b]
map [NewNotation] -> NewNotation
merge forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [NewNotation] -> [[NewNotation]]
groupIfLevelsMatch forall b c a. (b -> c) -> (a -> b) -> a -> c
.
forall b a. Ord b => (a -> b) -> [a] -> [[a]]
groupOn (\NewNotation
n -> ( NewNotation -> Notation
notation NewNotation
n
, NewNotation -> Bool
notaIsOperator NewNotation
n
))
where
groupIfLevelsMatch :: [NewNotation] -> [[NewNotation]]
groupIfLevelsMatch :: [NewNotation] -> [[NewNotation]]
groupIfLevelsMatch [] = forall a. HasCallStack => a
__IMPOSSIBLE__
groupIfLevelsMatch ns :: [NewNotation]
ns@(NewNotation
n : [NewNotation]
_) =
if forall a. Eq a => [a] -> Bool
allEqual (forall a b. (a -> b) -> [a] -> [b]
map Fixity -> FixityLevel
fixityLevel [Fixity]
related)
then [[NewNotation] -> [NewNotation]
sameAssoc ([NewNotation] -> [NewNotation]
sameLevel [NewNotation]
ns)]
else forall a b. (a -> b) -> [a] -> [b]
map (forall a. a -> [a] -> [a]
: []) [NewNotation]
ns
where
related :: [Fixity]
related = forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((\Fixity
f -> case Fixity -> FixityLevel
fixityLevel Fixity
f of
FixityLevel
Unrelated -> forall a. Maybe a
Nothing
Related {} -> forall a. a -> Maybe a
Just Fixity
f)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Fixity
notaFixity) [NewNotation]
ns
sameLevel :: [NewNotation] -> [NewNotation]
sameLevel = forall a b. (a -> b) -> [a] -> [b]
map (forall i o. Lens' i o -> LensSet i o
set (Lens' Fixity NewNotation
_notaFixity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' FixityLevel Fixity
_fixityLevel) FixityLevel
level)
where
level :: FixityLevel
level = case [Fixity]
related of
Fixity
f : [Fixity]
_ -> Fixity -> FixityLevel
fixityLevel Fixity
f
[] -> FixityLevel
Unrelated
sameAssoc :: [NewNotation] -> [NewNotation]
sameAssoc = forall a b. (a -> b) -> [a] -> [b]
map (forall i o. Lens' i o -> LensSet i o
set (Lens' Fixity NewNotation
_notaFixity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Associativity Fixity
_fixityAssoc) Associativity
assoc)
where
assoc :: Associativity
assoc = case [Fixity]
related of
Fixity
f : [Fixity]
_ | forall a. Eq a => [a] -> Bool
allEqual (forall a b. (a -> b) -> [a] -> [b]
map Fixity -> Associativity
fixityAssoc [Fixity]
related) -> Fixity -> Associativity
fixityAssoc Fixity
f
[Fixity]
_ -> Associativity
NonAssoc
merge :: [NewNotation] -> NewNotation
merge :: [NewNotation] -> NewNotation
merge [] = forall a. HasCallStack => a
__IMPOSSIBLE__
merge ns :: [NewNotation]
ns@(NewNotation
n : [NewNotation]
_) = NewNotation
n { notaNames :: Set Name
notaNames = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> Set Name
notaNames [NewNotation]
ns }
_notaFixity :: Lens' Fixity NewNotation
_notaFixity :: Lens' Fixity NewNotation
_notaFixity Fixity -> f Fixity
f NewNotation
r = Fixity -> f Fixity
f (NewNotation -> Fixity
notaFixity NewNotation
r) forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
<&> \Fixity
x -> NewNotation
r { notaFixity :: Fixity
notaFixity = Fixity
x }
data NotationSection = NotationSection
{ NotationSection -> NewNotation
sectNotation :: NewNotation
, NotationSection -> NotationKind
sectKind :: NotationKind
, NotationSection -> Maybe FixityLevel
sectLevel :: Maybe FixityLevel
, NotationSection -> Bool
sectIsSection :: Bool
}
deriving (Int -> NotationSection -> ShowS
[NotationSection] -> ShowS
NotationSection -> [Char]
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [NotationSection] -> ShowS
$cshowList :: [NotationSection] -> ShowS
show :: NotationSection -> [Char]
$cshow :: NotationSection -> [Char]
showsPrec :: Int -> NotationSection -> ShowS
$cshowsPrec :: Int -> NotationSection -> ShowS
Show, forall x. Rep NotationSection x -> NotationSection
forall x. NotationSection -> Rep NotationSection x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cto :: forall x. Rep NotationSection x -> NotationSection
$cfrom :: forall x. NotationSection -> Rep NotationSection x
Generic)
noSection :: NewNotation -> NotationSection
noSection :: NewNotation -> NotationSection
noSection NewNotation
n = NotationSection
{ sectNotation :: NewNotation
sectNotation = NewNotation
n
, sectKind :: NotationKind
sectKind = Notation -> NotationKind
notationKind (NewNotation -> Notation
notation NewNotation
n)
, sectLevel :: Maybe FixityLevel
sectLevel = forall a. a -> Maybe a
Just (Fixity -> FixityLevel
fixityLevel (NewNotation -> Fixity
notaFixity NewNotation
n))
, sectIsSection :: Bool
sectIsSection = Bool
False
}
instance Pretty NewNotation where
pretty :: NewNotation -> Doc
pretty (NewNotation QName
x Set Name
_xs Fixity
fx Notation
nota Bool
isOp) = Doc -> Doc -> Doc -> Doc
hsepWith Doc
"=" Doc
px Doc
pn
where
px :: Doc
px = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep [ if Bool
isOp then forall a. Null a => a
empty else Doc
"syntax" , forall a. Pretty a => a -> Doc
pretty Fixity
fx , forall a. Pretty a => a -> Doc
pretty QName
x ]
pn :: Doc
pn = if Bool
isOp then forall a. Null a => a
empty else forall a. Pretty a => a -> Doc
pretty Notation
nota
instance Pretty NotationKind where pretty :: NotationKind -> Doc
pretty = forall a. Show a => a -> Doc
pshow
instance Pretty NotationSection where
pretty :: NotationSection -> Doc
pretty (NotationSection NewNotation
nota NotationKind
kind Maybe FixityLevel
mlevel Bool
isSection)
| Bool
isSection = forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep
[ Doc
"section"
, forall a. Pretty a => a -> Doc
pretty NotationKind
kind
, forall b a. b -> (a -> b) -> Maybe a -> b
maybe forall a. Null a => a
empty forall a. Pretty a => a -> Doc
pretty Maybe FixityLevel
mlevel
, forall a. Pretty a => a -> Doc
pretty NewNotation
nota
]
| Bool
otherwise = forall a. Pretty a => a -> Doc
pretty NewNotation
nota
instance NFData NotationKind
instance NFData NewNotation
instance NFData NotationSection