{-# OPTIONS_GHC -Wunused-imports #-}

{-| As a concrete name, a notation is a non-empty list of alternating 'IdPart's and holes.
    In contrast to concrete names, holes can be binders.

    Example:
    @
       syntax fmap (λ x → e) xs = for x ∈ xs return e
    @

    The declared notation for @fmap@ is @for_∈_return_@ where the first hole is a binder.
-}

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 type constructed in the Happy parser; converted to
-- 'NotationPart' before it leaves the Happy code.
data HoleName
  = LambdaHole { HoleName -> List1 (Ranged [Char])
_bindHoleNames :: List1 RString
               , HoleName -> Ranged [Char]
holeName       :: RString
               }
    -- ^ @λ x₁ … xₙ → y@: The first argument contains the bound names.
  | ExprHole   { holeName      :: RString }
    -- ^ Simple named hole with hiding.

-- | Is the hole a binder?
isLambdaHole :: HoleName -> Bool
isLambdaHole :: HoleName -> Bool
isLambdaHole (LambdaHole List1 (Ranged [Char])
_ Ranged [Char]
_) = Bool
True
isLambdaHole HoleName
_ = Bool
False

-- | Get a flat list of identifier parts of a notation.
stringParts :: Notation -> [String]
stringParts :: Notation -> [[Char]]
stringParts Notation
gs = [ forall a. Ranged a -> a
rangedThing Ranged [Char]
x | IdPart Ranged [Char]
x <- Notation
gs ]

-- | Target argument position of a part (Nothing if it is not a hole).
holeTarget :: NotationPart -> Maybe Int
holeTarget :: NotationPart -> Maybe Int
holeTarget (VarPart Range
_ Ranged BoundVariablePosition
n)  = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ BoundVariablePosition -> Int
holeNumber forall a b. (a -> b) -> a -> b
$ forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
n
holeTarget (WildPart Ranged BoundVariablePosition
n)   = forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ BoundVariablePosition -> Int
holeNumber forall a b. (a -> b) -> a -> b
$ forall a. Ranged a -> a
rangedThing Ranged BoundVariablePosition
n
holeTarget (HolePart 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

-- | Is the part a hole?
isAHole :: NotationPart -> Bool
isAHole :: NotationPart -> Bool
isAHole HolePart{} = Bool
True
isAHole VarPart{}  = Bool
False
isAHole WildPart{} = Bool
False
isAHole IdPart{}   = Bool
False

-- | Is the part a binder?
isBinder :: NotationPart -> Bool
isBinder :: NotationPart -> Bool
isBinder HolePart{} = Bool
False
isBinder VarPart{}  = Bool
True
isBinder WildPart{} = Bool
True
isBinder IdPart{}   = Bool
False

-- | Classification of notations.

data NotationKind
  = InfixNotation   -- ^ Ex: @_bla_blub_@.
  | PrefixNotation  -- ^ Ex: @_bla_blub@.
  | PostfixNotation -- ^ Ex: @bla_blub_@.
  | NonfixNotation  -- ^ Ex: @bla_blub@.
  | 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)

-- | Classify a notation by presence of leading and/or trailing
-- /normal/ holes.
notationKind :: Notation -> NotationKind
notationKind :: Notation -> NotationKind
notationKind []  = NotationKind
NoNotation
notationKind (NotationPart
h:Notation
syn) =
  case (NotationPart -> Bool
isAHole NotationPart
h, NotationPart -> Bool
isAHole forall a b. (a -> b) -> a -> b
$ 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

-- | From notation with names to notation with indices.
--
--   An example (with some parts of the code omitted):
--   The lists
--   @["for", "x", "∈", "xs", "return", "e"]@
--   and
--   @['LambdaHole' ("x" :| []) "e", 'ExprHole' "xs"]@
--   are mapped to the following notation:
--   @
--      [ 'IdPart' "for"    , 'VarPart' ('BoundVariablePosition' 0 0)
--      , 'IdPart' "∈"      , 'HolePart' 1
--      , 'IdPart' "return" , 'HolePart' 0
--      ]
--   @
mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
mkNotation :: [NamedArg HoleName] -> [Ranged [Char]] -> 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 [Ranged [Char]]
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 Ranged [Char] -> NotationPart
mkPart [Ranged [Char]]
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"
  -- Andreas, 2018-10-18, issue #3285:
  -- syntax that is just a single hole is ill-formed and crashes the operator parser
  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
insertWildParts Notation
xs
    where
      holeNames :: [RString]
      holeNames :: [Ranged [Char]]
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 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 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) [Ranged [Char]]
holeNames

      mkPart :: Ranged [Char] -> NotationPart
mkPart Ranged [Char]
ident = forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Ranged [Char] -> NotationPart
IdPart Ranged [Char]
ident) (forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` Ranged [Char]
ident) forall a b. (a -> b) -> a -> b
$ forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup Ranged [Char]
ident [(Ranged [Char], NotationPart)]
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

      -- The WildParts don't correspond to anything in the right-hand side so
      -- we add them next to their corresponding body. Slightly subtle: due to
      -- the way the operator parsing works they can't be added first or last.
      insertWildParts :: [NotationPart] -> [NotationPart]
      insertWildParts :: Notation -> Notation
insertWildParts Notation
xs = 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)
            | forall a. NamedArg a -> a
namedArg NamedArg (Ranged Int)
h forall a. Eq a => a -> a -> Bool
== 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 forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> NotationPart
WildPart Ranged BoundVariablePosition
w forall a. a -> [a] -> [a]
: Notation
hs
          ins Ranged BoundVariablePosition
w (NotationPart
h : Notation
hs) = NotationPart
h forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w Notation
hs
          ins Ranged BoundVariablePosition
_ [] = forall a. HasCallStack => a
__IMPOSSIBLE__

          insBefore :: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w (HolePart 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
== 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 forall a. a -> [a] -> [a]
: Range -> NamedArg (Ranged Int) -> NotationPart
HolePart Range
r NamedArg (Ranged Int)
h forall a. a -> [a] -> [a]
: Notation
hs
          insBefore Ranged BoundVariablePosition
w (NotationPart
h : Notation
hs) = NotationPart
h forall a. a -> [a] -> [a]
: Ranged BoundVariablePosition -> Notation -> Notation
insBefore Ranged BoundVariablePosition
w Notation
hs
          insBefore Ranged BoundVariablePosition
_ [] = forall a. HasCallStack => a
__IMPOSSIBLE__

      -- A map (association list) from hole names to notation parts. A
      -- @LambdaHole@ contributes one or more entries, one @HolePart@
      -- and zero or more @VarPart@s or @WildParts@, all mapped to the
      -- same number.
      holeMap :: [(RString, NotationPart)]
      holeMap :: [(Ranged [Char], NotationPart)]
holeMap = do
        (Int
i, NamedArg HoleName
h) <- [(Int, NamedArg HoleName)]
numberedHoles
        let ri :: Ranged [Char] -> Ranged Int
ri Ranged [Char]
x   = forall a. Range -> a -> Ranged a
Ranged (forall a. HasRange a => a -> Range
getRange Ranged [Char]
x) Int
i
            rp :: Ranged [Char] -> Int -> Ranged BoundVariablePosition
rp Ranged [Char]
x Int
n = forall a. Range -> a -> Ranged a
Ranged (forall a. HasRange a => a -> Range
getRange Ranged [Char]
x) forall a b. (a -> b) -> a -> b
$
                     BoundVariablePosition
                       { holeNumber :: Int
holeNumber = Int
i
                       , varNumber :: Int
varNumber  = Int
n
                       }
            hole :: Ranged [Char] -> NotationPart
hole Ranged [Char]
y = Range -> NamedArg (Ranged Int) -> NotationPart
HolePart 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 (Ranged [Char] -> Ranged Int
ri Ranged [Char]
y forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) NamedArg HoleName
h
                              -- This range is filled in by mkPart.
        case forall a. NamedArg a -> a
namedArg NamedArg HoleName
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)] forall a. [a] -> [a] -> [a]
++
            forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith
              (\ Int
n Ranged [Char]
x -> case 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 forall a. Range' a
noRange (Ranged [Char] -> Int -> Ranged BoundVariablePosition
rp Ranged [Char]
x Int
n)))
                                   -- Filled in by mkPart.
              [Int
0..]
              (forall l. IsList l => l -> [Item l]
List1.toList List1 (Ranged [Char])
xs)

      -- Check whether all hole names are distinct.
      -- The hole names are the keys of the @holeMap@.
      uniqueHoleNames :: Bool
uniqueHoleNames = forall a. Eq a => [a] -> Bool
distinct [ Ranged [Char]
x | (Ranged [Char]
x, NotationPart
_) <- [(Ranged [Char], NotationPart)]
holeMap, forall a. Ranged a -> a
rangedThing Ranged [Char]
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 | NotationPart
x <- Notation
xs, NotationPart -> Bool
isAHole NotationPart
x, let Just Int
i = NotationPart -> Maybe Int
holeTarget NotationPart
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 BoundVariablePosition
x | VarPart Range
_ Ranged BoundVariablePosition
x <- Notation
xs ]
          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]
_ <- [forall a. NamedArg a -> a
namedArg NamedArg HoleName
h]
        , (Int
v, [Char]
x) <- forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..] forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Ranged a -> a
rangedThing forall a b. (a -> b) -> a -> b
$ forall l. IsList l => l -> [Item l]
List1.toList List1 (Ranged [Char])
vs
        , [Char]
x forall a. Eq a => a -> a -> Bool
/= [Char]
"_"
        ]

      noAdjacentHoles :: [NotationPart] -> Bool
      noAdjacentHoles :: Notation -> Bool
noAdjacentHoles =
        Notation -> Bool
noAdj forall b c a. (b -> c) -> (a -> b) -> a -> c
.
        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 []       = 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
yforall a. a -> [a] -> [a]
:Notation
xs)

      isSingleHole :: [NotationPart] -> Bool
      isSingleHole :: Notation -> Bool
isSingleHole = \case
        [ IdPart{} ] -> Bool
False
        [ NotationPart
_hole ]    -> Bool
True
        Notation
_            -> Bool
False

-- | All the notation information related to a name.
data NewNotation = NewNotation
  { NewNotation -> QName
notaName  :: QName
  , NewNotation -> Set Name
notaNames :: Set A.Name
    -- ^ The names the syntax and/or fixity belong to.
    --
    -- Invariant: The set is non-empty. Every name in the list matches
    -- 'notaName'.
  , NewNotation -> Fixity
notaFixity :: Fixity
    -- ^ Associativity and precedence (fixity) of the names.
  , NewNotation -> Notation
notation :: Notation
    -- ^ Syntax associated with the names.
  , NewNotation -> Bool
notaIsOperator :: Bool
    -- ^ True if the notation comes from an operator (rather than a
    -- syntax declaration).
  } 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' NewNotation Fixity
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 }

-- | If an operator has no specific notation, then it is computed from
-- its name.
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

-- | Replace 'noFixity' by 'defaultFixity'.
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

-- | Return the 'IdPart's of a notation, the first part qualified,
--   the other parts unqualified.
--   This allows for qualified use of operators, e.g.,
--   @M.for x ∈ xs return e@, or @x ℕ.+ y@.
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 Ranged [Char]
x | IdPart Ranged [Char]
x <- Notation
parts ]
  where
    -- The qualification of @q@.
    modules :: [Name]
modules     = forall a. NonEmpty a -> [a]
List1.init (QName -> List1 Name
qnameParts QName
q)
    -- Putting the qualification onto @x@.
    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

-- | Create a 'Notation' (without binders) from a concrete 'Name'.
--   Does the obvious thing:
--   'Hole's become 'HolePart's, 'Id's become 'IdParts'.
--   If 'Name' has no 'Hole's, it returns 'noNotation'.
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 l. IsList l => l -> [Item l]
List1.toList forall a b. (a -> b) -> a -> b
$ Name -> NameParts
nameNameParts Name
y
  | Bool
otherwise    = Notation
noNotation
  where
    -- Turn a concrete name into a Notation,
    -- numbering the holes from left to right.
    -- Result will have no 'BindingHole's.
    mkSyn :: Int -> [NamePart] -> Notation
    mkSyn :: Int -> [NamePart] -> Notation
mkSyn Int
n []          = []
    mkSyn Int
n (NamePart
Hole : [NamePart]
xs) = Range -> NamedArg (Ranged Int) -> NotationPart
HolePart 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) = Ranged [Char] -> NotationPart
IdPart (forall a. a -> Ranged a
unranged [Char]
x) forall a. a -> [a] -> [a]
: Int -> [NamePart] -> Notation
mkSyn Int
n [NamePart]
xs

-- | Merges 'NewNotation's that have the same precedence level and
-- notation, with two exceptions:
--
-- * Operators and notations coming from syntax declarations are kept
--   separate.
--
-- * If /all/ instances of a given 'NewNotation' have the same
--   precedence level or are \"unrelated\", then they are merged. They
--   get the given precedence level, if any, and otherwise they become
--   unrelated (but related to each other).
--
-- If 'NewNotation's that are merged have distinct associativities,
-- then they get 'NonAssoc' as their associativity.
--
-- Precondition: No 'A.Name' may occur in more than one list element.
-- Every 'NewNotation' must have the same 'notaName'.
--
-- Postcondition: No 'A.Name' occurs in more than one list element.
mergeNotations :: List1 NewNotation -> List1 NewNotation
mergeNotations :: NonEmpty NewNotation -> NonEmpty NewNotation
mergeNotations =
  forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap NonEmpty NewNotation -> NewNotation
merge
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> List1 b) -> List1 a -> List1 b
List1.concatMap1 NonEmpty NewNotation -> List1 (NonEmpty NewNotation)
groupIfLevelsMatch
  forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall b a. Ord b => (a -> b) -> List1 a -> List1 (List1 a)
List1.groupOn1 (NewNotation -> Notation
notation 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 forall a. Eq a => [a] -> Bool
allEqual (forall a b. (a -> b) -> [a] -> [b]
map Fixity -> FixityLevel
fixityLevel [Fixity]
related)
    then forall el coll. Singleton el coll => el -> coll
singleton forall a b. (a -> b) -> a -> b
$ NonEmpty NewNotation -> NonEmpty NewNotation
sameAssoc forall a b. (a -> b) -> a -> b
$ NonEmpty NewNotation -> NonEmpty NewNotation
sameLevel NonEmpty NewNotation
ns
    else forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall el coll. Singleton el coll => el -> coll
singleton NonEmpty NewNotation
ns
    where
    -- Fixities of operators whose precedence level is not Unrelated.
    related :: [Fixity]
related = forall a b. (a -> Maybe b) -> List1 a -> [b]
List1.mapMaybe (Fixity -> Maybe Fixity
maybeRelated 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  -> forall a. Maybe a
Nothing
            Related {} -> forall a. a -> Maybe a
Just Fixity
f

    -- Precondition: All related operators have the same precedence
    -- level.
    --
    -- Gives all unrelated operators the same level.
    sameLevel :: NonEmpty NewNotation -> NonEmpty NewNotation
sameLevel = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall o i. Lens' o i -> LensSet o i
set (Lens' NewNotation Fixity
_notaFixity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Fixity FixityLevel
_fixityLevel) FixityLevel
level)
      where
      level :: FixityLevel
level = case [Fixity]
related of
        Fixity
f : [Fixity]
_ -> Fixity -> FixityLevel
fixityLevel Fixity
f
        []    -> FixityLevel
Unrelated

    -- If all related operators have the same associativity, then the
    -- unrelated operators get the same associativity, and otherwise
    -- all operators get the associativity NonAssoc.
    sameAssoc :: NonEmpty NewNotation -> NonEmpty NewNotation
sameAssoc = forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (forall o i. Lens' o i -> LensSet o i
set (Lens' NewNotation Fixity
_notaFixity forall b c a. (b -> c) -> (a -> b) -> a -> c
. Lens' Fixity Associativity
_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 :: List1 NewNotation -> NewNotation
  merge :: NonEmpty NewNotation -> NewNotation
merge (NewNotation
n :| [NewNotation]
ns) = 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 forall a b. (a -> b) -> a -> b
$ NewNotation
nforall a. a -> [a] -> [a]
:[NewNotation]
ns }

-- | Check if a notation contains any lambdas (in which case it cannot be used in a pattern).
isLambdaNotation :: NewNotation -> Bool
isLambdaNotation :: NewNotation -> Bool
isLambdaNotation NewNotation
n = 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

-- | Lens for 'Fixity' in 'NewNotation'.

_notaFixity :: Lens' NewNotation Fixity
_notaFixity :: Lens' NewNotation Fixity
_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 }

-- * Sections

-- | Sections, as well as non-sectioned operators.

data NotationSection = NotationSection
  { NotationSection -> NewNotation
sectNotation  :: NewNotation
  , NotationSection -> NotationKind
sectKind      :: NotationKind
    -- ^ For non-sectioned operators this should match the notation's
    -- 'notationKind'.
  , NotationSection -> Maybe FixityLevel
sectLevel     :: Maybe FixityLevel
    -- ^ Effective precedence level. 'Nothing' for closed notations.
  , NotationSection -> Bool
sectIsSection :: Bool
    -- ^ 'False' for non-sectioned operators.
  }
  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)

-- | Converts a notation to a (non-)section.

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
  }


-- * Pretty printing

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

-- NFData instances

instance NFData NotationKind
instance NFData NewNotation
instance NFData NotationSection