{-# OPTIONS_GHC -Wunused-imports #-}
module Agda.Syntax.Notation where
import Prelude hiding (null)
import Control.Arrow ( (&&&) )
import Control.DeepSeq
import Control.Monad
import Control.Monad.Except
import qualified Data.List as List
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.Common.Pretty
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Concrete.Pretty()
import Agda.Syntax.Position
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.List1 ( List1, pattern (:|) )
import qualified Agda.Utils.List1 as List1
import Agda.Utils.Null
import Agda.Utils.Singleton
import Agda.Utils.Impossible
data HoleName
= LambdaHole { HoleName -> List1 (Ranged [Char])
_bindHoleNames :: List1 RString
, HoleName -> Ranged [Char]
holeName :: RString
}
| ExprHole { holeName :: RString }
isLambdaHole :: HoleName -> Bool
isLambdaHole :: HoleName -> Bool
isLambdaHole (LambdaHole List1 (Ranged [Char])
_ Ranged [Char]
_) = Bool
True
isLambdaHole HoleName
_ = Bool
False
stringParts :: Notation -> [String]
stringParts :: Notation -> [[Char]]
stringParts Notation
gs = [ Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing Ranged [Char]
x | IdPart Ranged [Char]
x <- Notation
gs ]
holeTarget :: NotationPart -> Maybe Int
holeTarget :: NotationPart -> Maybe Int
holeTarget (VarPart Range
_ Ranged BoundVariablePosition
n) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ BoundVariablePosition -> Int
holeNumber (BoundVariablePosition -> Int) -> BoundVariablePosition -> Int
forall a b. (a -> b) -> a -> b
$ Ranged BoundVariablePosition -> BoundVariablePosition
forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
n
holeTarget (WildPart Ranged BoundVariablePosition
n) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ BoundVariablePosition -> Int
holeNumber (BoundVariablePosition -> Int) -> BoundVariablePosition -> Int
forall a b. (a -> b) -> a -> b
$ Ranged BoundVariablePosition -> BoundVariablePosition
forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
n
holeTarget (HolePart Range
_ NamedArg (Ranged Int)
n) = Int -> Maybe Int
forall a. a -> Maybe a
Just (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Ranged Int -> Int
forall a. Ranged a -> a
rangedThing (Ranged Int -> Int) -> Ranged Int -> Int
forall a b. (a -> b) -> a -> b
$ NamedArg (Ranged Int) -> Ranged Int
forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
n
holeTarget IdPart{} = Maybe Int
forall a. Maybe a
Nothing
isAHole :: NotationPart -> Bool
isAHole :: NotationPart -> Bool
isAHole HolePart{} = Bool
True
isAHole VarPart{} = Bool
False
isAHole WildPart{} = Bool
False
isAHole IdPart{} = Bool
False
isBinder :: NotationPart -> Bool
isBinder :: NotationPart -> Bool
isBinder HolePart{} = Bool
False
isBinder VarPart{} = Bool
True
isBinder WildPart{} = Bool
True
isBinder IdPart{} = Bool
False
data NotationKind
= InfixNotation
| PrefixNotation
| PostfixNotation
| NonfixNotation
| NoNotation
deriving (NotationKind -> NotationKind -> Bool
(NotationKind -> NotationKind -> Bool)
-> (NotationKind -> NotationKind -> Bool) -> Eq NotationKind
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NotationKind -> NotationKind -> Bool
== :: NotationKind -> NotationKind -> Bool
$c/= :: NotationKind -> NotationKind -> Bool
/= :: NotationKind -> NotationKind -> Bool
Eq, Int -> NotationKind -> ShowS
[NotationKind] -> ShowS
NotationKind -> [Char]
(Int -> NotationKind -> ShowS)
-> (NotationKind -> [Char])
-> ([NotationKind] -> ShowS)
-> Show NotationKind
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotationKind -> ShowS
showsPrec :: Int -> NotationKind -> ShowS
$cshow :: NotationKind -> [Char]
show :: NotationKind -> [Char]
$cshowList :: [NotationKind] -> ShowS
showList :: [NotationKind] -> ShowS
Show, (forall x. NotationKind -> Rep NotationKind x)
-> (forall x. Rep NotationKind x -> NotationKind)
-> Generic NotationKind
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
$cfrom :: forall x. NotationKind -> Rep NotationKind x
from :: forall x. NotationKind -> Rep NotationKind x
$cto :: forall x. Rep NotationKind x -> NotationKind
to :: forall x. Rep NotationKind x -> NotationKind
Generic)
notationKind :: Notation -> NotationKind
notationKind :: Notation -> NotationKind
notationKind [] = NotationKind
NoNotation
notationKind (NotationPart
h:Notation
syn) =
case (NotationPart -> Bool
isAHole NotationPart
h, NotationPart -> Bool
isAHole (NotationPart -> Bool) -> NotationPart -> Bool
forall a b. (a -> b) -> a -> b
$ NotationPart -> Notation -> NotationPart
forall a. a -> [a] -> a
last1 NotationPart
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] -> [Ranged [Char]] -> Either [Char] Notation
mkNotation [NamedArg HoleName]
_ [] = [Char] -> Either [Char] Notation
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"empty notation is disallowed"
mkNotation [NamedArg HoleName]
holes [Ranged [Char]]
ids = do
Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
uniqueHoleNames (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use unique argument names"
let Notation
xs :: Notation = (Ranged [Char] -> NotationPart) -> [Ranged [Char]] -> Notation
forall a b. (a -> b) -> [a] -> [b]
map Ranged [Char] -> NotationPart
mkPart [Ranged [Char]]
ids
Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
noAdjacentHoles Notation
xs) (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError ([Char] -> Either [Char] ()) -> [Char] -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [[Char]] -> [Char]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
[ [Char]
"syntax must not contain adjacent holes ("
, [Char]
prettyHoles
, [Char]
")"
]
Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isExprLinear Notation
xs) (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use holes exactly once"
Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isLambdaLinear Notation
xs) (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax must use binding holes exactly once"
Bool -> Either [Char] () -> Either [Char] ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Notation -> Bool
isSingleHole Notation
xs) (Either [Char] () -> Either [Char] ())
-> Either [Char] () -> Either [Char] ()
forall a b. (a -> b) -> a -> b
$ [Char] -> Either [Char] ()
forall a. [Char] -> Either [Char] a
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError [Char]
"syntax cannot be a single hole"
Notation -> Either [Char] Notation
forall a. a -> Either [Char] a
forall (m :: * -> *) a. Monad m => a -> m a
return (Notation -> Either [Char] Notation)
-> Notation -> Either [Char] Notation
forall a b. (a -> b) -> a -> b
$ Notation -> Notation
insertWildParts Notation
xs
where
holeNames :: [RString]
holeNames :: [Ranged [Char]]
holeNames = (NamedArg HoleName -> HoleName)
-> [NamedArg HoleName] -> [HoleName]
forall a b. (a -> b) -> [a] -> [b]
map NamedArg HoleName -> HoleName
forall a. NamedArg a -> a
namedArg [NamedArg HoleName]
holes [HoleName] -> (HoleName -> [Ranged [Char]]) -> [Ranged [Char]]
forall a b. [a] -> (a -> [b]) -> [b]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
LambdaHole List1 (Ranged [Char])
_ Ranged [Char]
y -> [Ranged [Char]
y]
ExprHole Ranged [Char]
y -> [Ranged [Char]
y]
prettyHoles :: String
prettyHoles :: [Char]
prettyHoles = [[Char]] -> [Char]
List.unwords ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ (Ranged [Char] -> [Char]) -> [Ranged [Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
rawNameToString ShowS -> (Ranged [Char] -> [Char]) -> Ranged [Char] -> [Char]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing) [Ranged [Char]]
holeNames
mkPart :: Ranged [Char] -> NotationPart
mkPart Ranged [Char]
ident = NotationPart
-> (NotationPart -> NotationPart)
-> Maybe NotationPart
-> NotationPart
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ranged [Char] -> NotationPart
IdPart Ranged [Char]
ident) (NotationPart -> Ranged [Char] -> NotationPart
forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` Ranged [Char]
ident) (Maybe NotationPart -> NotationPart)
-> Maybe NotationPart -> NotationPart
forall a b. (a -> b) -> a -> b
$ Ranged [Char]
-> [(Ranged [Char], NotationPart)] -> Maybe NotationPart
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ranged [Char]
ident [(Ranged [Char], NotationPart)]
holeMap
holeNumbers :: [Int]
holeNumbers = [Int
0 .. [NamedArg HoleName] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [NamedArg HoleName]
holes Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1]
numberedHoles :: [(Int, NamedArg HoleName)]
numberedHoles :: [(Int, NamedArg HoleName)]
numberedHoles = [Int] -> [NamedArg HoleName] -> [(Int, NamedArg HoleName)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int]
holeNumbers [NamedArg HoleName]
holes
insertWildParts :: [NotationPart] -> [NotationPart]
insertWildParts :: Notation -> Notation
insertWildParts Notation
xs = (Ranged BoundVariablePosition -> Notation -> Notation)
-> Notation -> [Ranged BoundVariablePosition] -> Notation
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Ranged BoundVariablePosition -> Notation -> Notation
ins Notation
xs [Ranged BoundVariablePosition]
wilds
where
wilds :: [Ranged BoundVariablePosition]
wilds = [ Ranged BoundVariablePosition
i | (Ranged [Char]
_, WildPart Ranged BoundVariablePosition
i) <- [(Ranged [Char], NotationPart)]
holeMap ]
ins :: Ranged BoundVariablePosition -> Notation -> Notation
ins Ranged BoundVariablePosition
w (HolePart Range
r NamedArg (Ranged Int)
h : Notation
hs)
| NamedArg (Ranged Int) -> Ranged Int
forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
h Ranged Int -> Ranged Int -> Bool
forall a. Eq a => a -> a -> Bool
== (BoundVariablePosition -> Int)
-> Ranged BoundVariablePosition -> Ranged Int
forall a b. (a -> b) -> Ranged a -> Ranged b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BoundVariablePosition -> Int
holeNumber Ranged BoundVariablePosition
w =
Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
r NamedArg (Ranged Int)
h NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> NotationPart
WildPart Ranged BoundVariablePosition
w NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Notation
hs
ins Ranged BoundVariablePosition
w (NotationPart
h : Notation
hs) = NotationPart
h NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w Notation
hs
ins Ranged BoundVariablePosition
_ [] = Notation
forall a. HasCallStack => a
__IMPOSSIBLE__
insBefore :: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w (HolePart Range
r NamedArg (Ranged Int)
h : Notation
hs)
| NamedArg (Ranged Int) -> Ranged Int
forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
h Ranged Int -> Ranged Int -> Bool
forall a. Eq a => a -> a -> Bool
== (BoundVariablePosition -> Int)
-> Ranged BoundVariablePosition -> Ranged Int
forall a b. (a -> b) -> Ranged a -> Ranged b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap BoundVariablePosition -> Int
holeNumber Ranged BoundVariablePosition
w =
Ranged BoundVariablePosition -> NotationPart
WildPart Ranged BoundVariablePosition
w NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
r NamedArg (Ranged Int)
h NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Notation
hs
insBefore Ranged BoundVariablePosition
w (NotationPart
h : Notation
hs) = NotationPart
h NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w Notation
hs
insBefore Ranged BoundVariablePosition
_ [] = Notation
forall a. HasCallStack => a
__IMPOSSIBLE__
holeMap :: [(RString, NotationPart)]
holeMap :: [(Ranged [Char], NotationPart)]
holeMap = do
(i, h) <- [(Int, NamedArg HoleName)]
numberedHoles
let ri Ranged [Char]
x = Range -> Int -> Ranged Int
forall a. Range -> a -> Ranged a
Ranged (Ranged [Char] -> Range
forall a. HasRange a => a -> Range
getRange Ranged [Char]
x) Int
i
rp Ranged [Char]
x Int
n = Range -> BoundVariablePosition -> Ranged BoundVariablePosition
forall a. Range -> a -> Ranged a
Ranged (Ranged [Char] -> Range
forall a. HasRange a => a -> Range
getRange Ranged [Char]
x) (BoundVariablePosition -> Ranged BoundVariablePosition)
-> BoundVariablePosition -> Ranged BoundVariablePosition
forall a b. (a -> b) -> a -> b
$
BoundVariablePosition
{ holeNumber :: Int
holeNumber = Int
i
, varNumber :: Int
varNumber = Int
n
}
hole Ranged [Char]
y = Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
forall a. Range' a
noRange (NamedArg (Ranged Int) -> NotationPart)
-> NamedArg (Ranged Int) -> NotationPart
forall a b. (a -> b) -> a -> b
$ (Named NamedName HoleName -> Named_ (Ranged Int))
-> NamedArg HoleName -> NamedArg (Ranged Int)
forall a b. (a -> b) -> Arg a -> Arg b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Ranged [Char] -> Ranged Int
ri Ranged [Char]
y Ranged Int -> Named NamedName HoleName -> Named_ (Ranged Int)
forall a b. a -> Named NamedName b -> Named NamedName a
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) NamedArg HoleName
h
case namedArg h of
ExprHole Ranged [Char]
y -> [(Ranged [Char]
y, Ranged [Char] -> NotationPart
hole Ranged [Char]
y)]
LambdaHole List1 (Ranged [Char])
xs Ranged [Char]
y -> [(Ranged [Char]
y, Ranged [Char] -> NotationPart
hole Ranged [Char]
y)] [(Ranged [Char], NotationPart)]
-> [(Ranged [Char], NotationPart)]
-> [(Ranged [Char], NotationPart)]
forall a. [a] -> [a] -> [a]
++
(Int -> Ranged [Char] -> (Ranged [Char], NotationPart))
-> [Int] -> [Ranged [Char]] -> [(Ranged [Char], NotationPart)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
(\ Int
n Ranged [Char]
x -> case Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing Ranged [Char]
x of
[Char]
"_" -> (Ranged [Char]
x, Ranged BoundVariablePosition -> NotationPart
WildPart (Ranged [Char] -> Int -> Ranged BoundVariablePosition
rp Ranged [Char]
x Int
n))
[Char]
_ -> (Ranged [Char]
x, Range -> Ranged BoundVariablePosition -> NotationPart
VarPart Range
forall a. Range' a
noRange (Ranged [Char] -> Int -> Ranged BoundVariablePosition
rp Ranged [Char]
x Int
n)))
[Int
0..]
(List1 (Ranged [Char]) -> [Item (List1 (Ranged [Char]))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Ranged [Char])
xs)
uniqueHoleNames :: Bool
uniqueHoleNames = [Ranged [Char]] -> Bool
forall a. Eq a => [a] -> Bool
distinct [ Ranged [Char]
x | (Ranged [Char]
x, NotationPart
_) <- [(Ranged [Char], NotationPart)]
holeMap, Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing Ranged [Char]
x [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
"_" ]
isExprLinear :: Notation -> Bool
isExprLinear Notation
xs =
[Int] -> [Int]
forall a. Ord a => [a] -> [a]
List.sort [ Int
i | NotationPart
x <- Notation
xs, NotationPart -> Bool
isAHole NotationPart
x, let Just Int
i = NotationPart -> Maybe Int
holeTarget NotationPart
x ]
[Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
==
[Int]
holeNumbers
isLambdaLinear :: Notation -> Bool
isLambdaLinear Notation
xs =
[BoundVariablePosition] -> [BoundVariablePosition]
forall a. Ord a => [a] -> [a]
List.sort [ Ranged BoundVariablePosition -> BoundVariablePosition
forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
x | VarPart Range
_ Ranged BoundVariablePosition
x <- Notation
xs ]
[BoundVariablePosition] -> [BoundVariablePosition] -> Bool
forall a. Eq a => a -> a -> Bool
==
[ BoundVariablePosition { holeNumber :: Int
holeNumber = Int
i, varNumber :: Int
varNumber = Int
v }
| (Int
i, NamedArg HoleName
h) <- [(Int, NamedArg HoleName)]
numberedHoles
, LambdaHole List1 (Ranged [Char])
vs Ranged [Char]
_ <- [NamedArg HoleName -> HoleName
forall a. NamedArg a -> a
namedArg NamedArg HoleName
h]
, (Int
v, [Char]
x) <- [Int] -> [[Char]] -> [(Int, [Char])]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] ([[Char]] -> [(Int, [Char])]) -> [[Char]] -> [(Int, [Char])]
forall a b. (a -> b) -> a -> b
$ (Ranged [Char] -> [Char]) -> [Ranged [Char]] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing ([Ranged [Char]] -> [[Char]]) -> [Ranged [Char]] -> [[Char]]
forall a b. (a -> b) -> a -> b
$ List1 (Ranged [Char]) -> [Item (List1 (Ranged [Char]))]
forall l. IsList l => l -> [Item l]
List1.toList List1 (Ranged [Char])
vs
, [Char]
x [Char] -> [Char] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Char]
"_"
]
noAdjacentHoles :: [NotationPart] -> Bool
noAdjacentHoles :: Notation -> Bool
noAdjacentHoles =
Notation -> Bool
noAdj (Notation -> Bool) -> (Notation -> Notation) -> Notation -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
(NotationPart -> Bool) -> Notation -> Notation
forall a. (a -> Bool) -> [a] -> [a]
filter (\NotationPart
h -> case NotationPart
h of
HolePart{} -> Bool
True
IdPart{} -> Bool
True
NotationPart
_ -> Bool
False)
where
noAdj :: Notation -> Bool
noAdj [] = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
noAdj [NotationPart
x] = Bool
True
noAdj (NotationPart
x:NotationPart
y:Notation
xs) =
Bool -> Bool
not (NotationPart -> Bool
isAHole NotationPart
x Bool -> Bool -> Bool
&& NotationPart -> Bool
isAHole NotationPart
y) Bool -> Bool -> Bool
&&
Notation -> Bool
noAdj (NotationPart
yNotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
:Notation
xs)
isSingleHole :: [NotationPart] -> Bool
isSingleHole :: Notation -> Bool
isSingleHole = \case
[ IdPart{} ] -> Bool
False
[ NotationPart
_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]
(Int -> NewNotation -> ShowS)
-> (NewNotation -> [Char])
-> ([NewNotation] -> ShowS)
-> Show NewNotation
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NewNotation -> ShowS
showsPrec :: Int -> NewNotation -> ShowS
$cshow :: NewNotation -> [Char]
show :: NewNotation -> [Char]
$cshowList :: [NewNotation] -> ShowS
showList :: [NewNotation] -> ShowS
Show, (forall x. NewNotation -> Rep NewNotation x)
-> (forall x. Rep NewNotation x -> NewNotation)
-> Generic NewNotation
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
$cfrom :: forall x. NewNotation -> Rep NewNotation x
from :: forall x. NewNotation -> Rep NewNotation x
$cto :: forall x. Rep NewNotation x -> NewNotation
to :: forall x. Rep NewNotation x -> NewNotation
Generic)
instance LensFixity NewNotation where
lensFixity :: Lens' NewNotation Fixity
lensFixity Fixity -> f Fixity
f NewNotation
nota = Fixity -> f Fixity
f (NewNotation -> Fixity
notaFixity NewNotation
nota) f Fixity -> (Fixity -> NewNotation) -> f NewNotation
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \ Fixity
fx -> NewNotation
nota { notaFixity = 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 = Name -> Set Name
forall a. a -> Set a
Set.singleton Name
n
, notaFixity :: Fixity
notaFixity = Fixity
f
, notation :: Notation
notation = if Notation -> Bool
forall a. Null a => a -> Bool
null Notation
syn then Name -> Notation
syntaxOf (QName -> Name
unqualify QName
q) else Notation
syn
, notaIsOperator :: Bool
notaIsOperator = Notation -> Bool
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 Fixity -> Fixity -> Bool
forall a. Eq a => a -> a -> Bool
== Fixity
noFixity = NewNotation
n { notaFixity = defaultFixity }
| Bool
otherwise = NewNotation
n
notationNames :: NewNotation -> [QName]
notationNames :: NewNotation -> [QName]
notationNames (NewNotation QName
q Set Name
_ Fixity
_ Notation
parts Bool
_) =
((Name -> QName) -> Name -> QName)
-> [Name -> QName] -> [Name] -> [QName]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Name -> QName) -> Name -> QName
forall a b. (a -> b) -> a -> b
($) (Name -> QName
reQualify (Name -> QName) -> [Name -> QName] -> [Name -> QName]
forall a. a -> [a] -> [a]
: (Name -> QName) -> [Name -> QName]
forall a. a -> [a]
repeat Name -> QName
QName) [[Char] -> Name
simpleName ([Char] -> Name) -> [Char] -> Name
forall a b. (a -> b) -> a -> b
$ Ranged [Char] -> [Char]
forall a. Ranged a -> a
rangedThing Ranged [Char]
x | IdPart Ranged [Char]
x <- Notation
parts ]
where
modules :: [Name]
modules = NonEmpty Name -> [Name]
forall a. NonEmpty a -> [a]
List1.init (QName -> NonEmpty Name
qnameParts QName
q)
reQualify :: Name -> QName
reQualify Name
x = (Name -> QName -> QName) -> QName -> [Name] -> QName
forall a b. (a -> b -> b) -> b -> [a] -> b
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 ([NamePart] -> Notation) -> [NamePart] -> Notation
forall a b. (a -> b) -> a -> b
$ NameParts -> [Item NameParts]
forall l. IsList l => l -> [Item l]
List1.toList (NameParts -> [Item NameParts]) -> NameParts -> [Item NameParts]
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) -> NotationPart
HolePart Range
forall a. Range' a
noRange (Ranged Int -> NamedArg (Ranged Int)
forall a. a -> NamedArg a
defaultNamedArg (Ranged Int -> NamedArg (Ranged Int))
-> Ranged Int -> NamedArg (Ranged Int)
forall a b. (a -> b) -> a -> b
$ Int -> Ranged Int
forall a. a -> Ranged a
unranged Int
n) NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Int -> [NamePart] -> Notation
mkSyn (Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) [NamePart]
xs
mkSyn Int
n (Id [Char]
x : [NamePart]
xs) = Ranged [Char] -> NotationPart
IdPart ([Char] -> Ranged [Char]
forall a. a -> Ranged a
unranged [Char]
x) NotationPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Int -> [NamePart] -> Notation
mkSyn Int
n [NamePart]
xs
mergeNotations :: List1 NewNotation -> List1 NewNotation
mergeNotations :: NonEmpty NewNotation -> NonEmpty NewNotation
mergeNotations =
(NonEmpty NewNotation -> NewNotation)
-> List1 (NonEmpty NewNotation) -> NonEmpty NewNotation
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty NewNotation -> NewNotation
merge
(List1 (NonEmpty NewNotation) -> NonEmpty NewNotation)
-> (NonEmpty NewNotation -> List1 (NonEmpty NewNotation))
-> NonEmpty NewNotation
-> NonEmpty NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NonEmpty NewNotation -> List1 (NonEmpty NewNotation))
-> List1 (NonEmpty NewNotation) -> List1 (NonEmpty NewNotation)
forall a b. (a -> List1 b) -> List1 a -> List1 b
List1.concatMap1 NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
groupIfLevelsMatch
(List1 (NonEmpty NewNotation) -> List1 (NonEmpty NewNotation))
-> (NonEmpty NewNotation -> List1 (NonEmpty NewNotation))
-> NonEmpty NewNotation
-> List1 (NonEmpty NewNotation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NewNotation -> (Notation, Bool))
-> NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
forall b a. Ord b => (a -> b) -> List1 a -> List1 (List1 a)
List1.groupOn1 (NewNotation -> Notation
notation (NewNotation -> Notation)
-> (NewNotation -> Bool) -> NewNotation -> (Notation, Bool)
forall b c c'. (b -> c) -> (b -> c') -> b -> (c, c')
forall (a :: * -> * -> *) b c c'.
Arrow a =>
a b c -> a b c' -> a b (c, c')
&&& NewNotation -> Bool
notaIsOperator)
where
groupIfLevelsMatch :: List1 NewNotation -> List1 (List1 NewNotation)
groupIfLevelsMatch :: NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
groupIfLevelsMatch NonEmpty NewNotation
ns =
if [FixityLevel] -> Bool
forall a. Eq a => [a] -> Bool
allEqual ((Fixity -> FixityLevel) -> [Fixity] -> [FixityLevel]
forall a b. (a -> b) -> [a] -> [b]
map Fixity -> FixityLevel
fixityLevel [Fixity]
related)
then NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
forall el coll. Singleton el coll => el -> coll
singleton (NonEmpty NewNotation -> List1 (NonEmpty NewNotation))
-> NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
forall a b. (a -> b) -> a -> b
$ NonEmpty NewNotation -> NonEmpty NewNotation
sameAssoc (NonEmpty NewNotation -> NonEmpty NewNotation)
-> NonEmpty NewNotation -> NonEmpty NewNotation
forall a b. (a -> b) -> a -> b
$ NonEmpty NewNotation -> NonEmpty NewNotation
sameLevel NonEmpty NewNotation
ns
else (NewNotation -> NonEmpty NewNotation)
-> NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NewNotation -> NonEmpty NewNotation
forall el coll. Singleton el coll => el -> coll
singleton NonEmpty NewNotation
ns
where
related :: [Fixity]
related = (NewNotation -> Maybe Fixity) -> NonEmpty NewNotation -> [Fixity]
forall a b. (a -> Maybe b) -> List1 a -> [b]
List1.mapMaybe (Fixity -> Maybe Fixity
maybeRelated (Fixity -> Maybe Fixity)
-> (NewNotation -> Fixity) -> NewNotation -> Maybe Fixity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Fixity
notaFixity) NonEmpty NewNotation
ns
where
maybeRelated :: Fixity -> Maybe Fixity
maybeRelated Fixity
f =
case Fixity -> FixityLevel
fixityLevel Fixity
f of
FixityLevel
Unrelated -> Maybe Fixity
forall a. Maybe a
Nothing
Related {} -> Fixity -> Maybe Fixity
forall a. a -> Maybe a
Just Fixity
f
sameLevel :: NonEmpty NewNotation -> NonEmpty NewNotation
sameLevel = (NewNotation -> NewNotation)
-> NonEmpty NewNotation -> NonEmpty NewNotation
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Lens' NewNotation FixityLevel -> LensSet NewNotation FixityLevel
forall o i. Lens' o i -> LensSet o i
set ((Fixity -> f Fixity) -> NewNotation -> f NewNotation
Lens' NewNotation Fixity
_notaFixity ((Fixity -> f Fixity) -> NewNotation -> f NewNotation)
-> ((FixityLevel -> f FixityLevel) -> Fixity -> f Fixity)
-> (FixityLevel -> f FixityLevel)
-> NewNotation
-> f NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FixityLevel -> f FixityLevel) -> Fixity -> f Fixity
Lens' Fixity FixityLevel
_fixityLevel) FixityLevel
level)
where
level :: FixityLevel
level = case [Fixity]
related of
Fixity
f : [Fixity]
_ -> Fixity -> FixityLevel
fixityLevel Fixity
f
[] -> FixityLevel
Unrelated
sameAssoc :: NonEmpty NewNotation -> NonEmpty NewNotation
sameAssoc = (NewNotation -> NewNotation)
-> NonEmpty NewNotation -> NonEmpty NewNotation
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Lens' NewNotation Associativity
-> LensSet NewNotation Associativity
forall o i. Lens' o i -> LensSet o i
set ((Fixity -> f Fixity) -> NewNotation -> f NewNotation
Lens' NewNotation Fixity
_notaFixity ((Fixity -> f Fixity) -> NewNotation -> f NewNotation)
-> ((Associativity -> f Associativity) -> Fixity -> f Fixity)
-> (Associativity -> f Associativity)
-> NewNotation
-> f NewNotation
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Associativity -> f Associativity) -> Fixity -> f Fixity
Lens' Fixity Associativity
_fixityAssoc) Associativity
assoc)
where
assoc :: Associativity
assoc = case [Fixity]
related of
Fixity
f : [Fixity]
_ | [Associativity] -> Bool
forall a. Eq a => [a] -> Bool
allEqual ((Fixity -> Associativity) -> [Fixity] -> [Associativity]
forall a b. (a -> b) -> [a] -> [b]
map Fixity -> Associativity
fixityAssoc [Fixity]
related) -> Fixity -> Associativity
fixityAssoc Fixity
f
[Fixity]
_ -> Associativity
NonAssoc
merge :: List1 NewNotation -> NewNotation
merge :: NonEmpty NewNotation -> NewNotation
merge (NewNotation
n :| [NewNotation]
ns) = NewNotation
n { notaNames = Set.unions $ map notaNames $ n:ns }
isLambdaNotation :: NewNotation -> Bool
isLambdaNotation :: NewNotation -> Bool
isLambdaNotation NewNotation
n = (NotationPart -> Bool) -> Notation -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any NotationPart -> Bool
isBinder (NewNotation -> Notation
notation NewNotation
n)
where
isBinder :: NotationPart -> Bool
isBinder VarPart{} = Bool
True
isBinder WildPart{} = Bool
True
isBinder IdPart{} = Bool
False
isBinder HolePart{} = Bool
False
_notaFixity :: Lens' NewNotation Fixity
_notaFixity :: Lens' NewNotation Fixity
_notaFixity Fixity -> f Fixity
f NewNotation
r = Fixity -> f Fixity
f (NewNotation -> Fixity
notaFixity NewNotation
r) f Fixity -> (Fixity -> NewNotation) -> f NewNotation
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> \Fixity
x -> NewNotation
r { notaFixity = 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]
(Int -> NotationSection -> ShowS)
-> (NotationSection -> [Char])
-> ([NotationSection] -> ShowS)
-> Show NotationSection
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NotationSection -> ShowS
showsPrec :: Int -> NotationSection -> ShowS
$cshow :: NotationSection -> [Char]
show :: NotationSection -> [Char]
$cshowList :: [NotationSection] -> ShowS
showList :: [NotationSection] -> ShowS
Show, (forall x. NotationSection -> Rep NotationSection x)
-> (forall x. Rep NotationSection x -> NotationSection)
-> Generic NotationSection
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
$cfrom :: forall x. NotationSection -> Rep NotationSection x
from :: forall x. NotationSection -> Rep NotationSection x
$cto :: forall x. Rep NotationSection x -> NotationSection
to :: forall x. Rep NotationSection x -> NotationSection
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 = FixityLevel -> Maybe FixityLevel
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 = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep [ if Bool
isOp then Doc
forall a. Null a => a
empty else Doc
"syntax" , Fixity -> Doc
forall a. Pretty a => a -> Doc
pretty Fixity
fx , QName -> Doc
forall a. Pretty a => a -> Doc
pretty QName
x ]
pn :: Doc
pn = if Bool
isOp then Doc
forall a. Null a => a
empty else Notation -> Doc
forall a. Pretty a => a -> Doc
pretty Notation
nota
instance Pretty NotationKind where pretty :: NotationKind -> Doc
pretty = NotationKind -> Doc
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 = [Doc] -> Doc
forall (t :: * -> *). Foldable t => t Doc -> Doc
fsep
[ Doc
"section"
, NotationKind -> Doc
forall a. Pretty a => a -> Doc
pretty NotationKind
kind
, Doc -> (FixityLevel -> Doc) -> Maybe FixityLevel -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
forall a. Null a => a
empty FixityLevel -> Doc
forall a. Pretty a => a -> Doc
pretty Maybe FixityLevel
mlevel
, NewNotation -> Doc
forall a. Pretty a => a -> Doc
pretty NewNotation
nota
]
| Bool
otherwise = NewNotation -> Doc
forall a. Pretty a => a -> Doc
pretty NewNotation
nota
instance NFData NotationKind
instance NFData NewNotation
instance NFData NotationSection