{-# LANGUAGE DeriveDataTypeable  #-}

{-| 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.DeepSeq
import Control.Monad

import qualified Data.List as List
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set

import Data.Data (Data)

import qualified Agda.Syntax.Abstract.Name as A
import Agda.Syntax.Common
import Agda.Syntax.Concrete.Name
import Agda.Syntax.Position

import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.Functor ((<&>))
import Agda.Utils.Lens
import Agda.Utils.List
import Agda.Utils.Null

import Agda.Utils.Impossible

-- | Data type constructed in the Happy parser; converted to 'GenPart'
--   before it leaves the Happy code.
data HoleName
  = LambdaHole { HoleName -> RString
_bindHoleName :: RString
               , HoleName -> RString
holeName      :: RString }
    -- ^ @\ x -> y@; 1st argument is the bound name (unused for now).
  | ExprHole   { holeName      :: RString }
    -- ^ Simple named hole with hiding.

-- | Is the hole a binder?
isLambdaHole :: HoleName -> Bool
isLambdaHole :: HoleName -> Bool
isLambdaHole (LambdaHole RString
_ RString
_) = Bool
True
isLambdaHole HoleName
_ = Bool
False

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

-- | Target argument position of a part (Nothing if it is not a hole).
holeTarget :: GenPart -> Maybe Int
holeTarget :: GenPart -> Maybe Int
holeTarget (BindHole Range
_   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
n
holeTarget (WildHole     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
n
holeTarget (NormalHole 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

-- | Is the part a hole? WildHoles don't count since they don't correspond to
--   anything the user writes.
isAHole :: GenPart -> Bool
isAHole :: GenPart -> Bool
isAHole BindHole{}   = Bool
True
isAHole NormalHole{} = Bool
True
isAHole WildHole{}   = Bool
False
isAHole IdPart{}     = Bool
False

-- | Is the part a normal hole?
isNormalHole :: GenPart -> Bool
isNormalHole :: GenPart -> Bool
isNormalHole NormalHole{} = Bool
True
isNormalHole BindHole{}   = Bool
False
isNormalHole WildHole{}   = Bool
False
isNormalHole IdPart{}     = Bool
False

-- | Is the part a binder?
isBindingHole :: GenPart -> Bool
isBindingHole :: GenPart -> Bool
isBindingHole BindHole{} = Bool
True
isBindingHole WildHole{} = Bool
True
isBindingHole GenPart
_          = 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
(NotationKind -> NotationKind -> Bool)
-> (NotationKind -> NotationKind -> Bool) -> Eq NotationKind
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 -> String
(Int -> NotationKind -> ShowS)
-> (NotationKind -> String)
-> ([NotationKind] -> ShowS)
-> Show NotationKind
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NotationKind] -> ShowS
$cshowList :: [NotationKind] -> ShowS
show :: NotationKind -> String
$cshow :: NotationKind -> String
showsPrec :: Int -> NotationKind -> ShowS
$cshowsPrec :: Int -> NotationKind -> ShowS
Show)

-- | Classify a notation by presence of leading and/or trailing
-- /normal/ holes.
notationKind :: Notation -> NotationKind
notationKind :: Notation -> NotationKind
notationKind []  = NotationKind
NoNotation
notationKind Notation
syn =
  case (GenPart -> Bool
isNormalHole (GenPart -> Bool) -> GenPart -> Bool
forall a b. (a -> b) -> a -> b
$ Notation -> GenPart
forall a. [a] -> a
head Notation
syn, GenPart -> Bool
isNormalHole (GenPart -> Bool) -> GenPart -> Bool
forall a b. (a -> b) -> a -> b
$ Notation -> GenPart
forall a. [a] -> a
last 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.
--
--   Example:
--   @
--      ids   = ["for", "x", "∈", "xs", "return", "e"]
--      holes = [ LambdaHole "x" "e",  ExprHole "xs" ]
--   @
--   creates the notation
--   @
--      [ IdPart "for"    , BindHole 0
--      , IdPart "∈"      , NormalHole 1
--      , IdPart "return" , NormalHole 0
--      ]
--   @
mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
mkNotation :: [NamedArg HoleName] -> [RString] -> Either String Notation
mkNotation [NamedArg HoleName]
_ [] = String -> Either String Notation
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"empty notation is disallowed"
mkNotation [NamedArg HoleName]
holes [RString]
ids = do
  Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless Bool
uniqueHoleNames     (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"syntax must use unique argument names"
  let Notation
xs :: Notation = (RString -> GenPart) -> [RString] -> Notation
forall a b. (a -> b) -> [a] -> [b]
map RString -> GenPart
mkPart [RString]
ids
  Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isAlternating Notation
xs)  (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError (String -> Either String ()) -> String -> Either String ()
forall a b. (a -> b) -> a -> b
$ [String] -> String
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat
     [ String
"syntax must alternate holes ("
     , String
prettyHoles
     , String
") and non-holes ("
     , Notation -> String
prettyNonHoles Notation
xs
     , String
")"
     ]
  Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isExprLinear Notation
xs)   (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"syntax must use holes exactly once"
  Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Notation -> Bool
isLambdaLinear Notation
xs) (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"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
  Bool -> Either String () -> Either String ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when   (Notation -> Bool
isSingleHole Notation
xs)   (Either String () -> Either String ())
-> Either String () -> Either String ()
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall e (m :: * -> *) a. MonadError e m => e -> m a
throwError String
"syntax cannot be a single hole"
  Notation -> Either String Notation
forall (m :: * -> *) a. Monad m => a -> m a
return (Notation -> Either String Notation)
-> Notation -> Either String Notation
forall a b. (a -> b) -> a -> b
$ Notation -> Notation
insertWildHoles Notation
xs
    where
      holeNames :: [RString]
      holeNames :: [RString]
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 -> [RString]) -> [RString]
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 :: String
prettyHoles = [String] -> String
List.unwords ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$ (RString -> String) -> [RString] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
rawNameToString ShowS -> (RString -> String) -> RString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RString -> String
forall a. Ranged a -> a
rangedThing) [RString]
holeNames

      nonHoleNames :: Notation -> [RString]
      nonHoleNames :: Notation -> [RString]
nonHoleNames Notation
xs = ((GenPart -> Maybe RString) -> Notation -> [RString])
-> Notation -> (GenPart -> Maybe RString) -> [RString]
forall a b c. (a -> b -> c) -> b -> a -> c
flip (GenPart -> Maybe RString) -> Notation -> [RString]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Notation
xs ((GenPart -> Maybe RString) -> [RString])
-> (GenPart -> Maybe RString) -> [RString]
forall a b. (a -> b) -> a -> b
$ \case
        WildHole{}   -> RString -> Maybe RString
forall a. a -> Maybe a
Just (RString -> Maybe RString) -> RString -> Maybe RString
forall a b. (a -> b) -> a -> b
$ String -> RString
forall a. a -> Ranged a
unranged String
"_"
        IdPart RString
x     -> RString -> Maybe RString
forall a. a -> Maybe a
Just RString
x
        BindHole{}   -> Maybe RString
forall a. Maybe a
Nothing
        NormalHole{} -> Maybe RString
forall a. Maybe a
Nothing

      prettyNonHoles :: Notation -> String
      prettyNonHoles :: Notation -> String
prettyNonHoles = [String] -> String
List.unwords ([String] -> String)
-> (Notation -> [String]) -> Notation -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RString -> String) -> [RString] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (ShowS
rawNameToString ShowS -> (RString -> String) -> RString -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RString -> String
forall a. Ranged a -> a
rangedThing) ([RString] -> [String])
-> (Notation -> [RString]) -> Notation -> [String]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Notation -> [RString]
nonHoleNames

      mkPart :: RString -> GenPart
mkPart RString
ident = GenPart -> (GenPart -> GenPart) -> Maybe GenPart -> GenPart
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (RString -> GenPart
IdPart RString
ident) (GenPart -> RString -> GenPart
forall t u. (SetRange t, HasRange u) => t -> u -> t
`withRangeOf` RString
ident) (Maybe GenPart -> GenPart) -> Maybe GenPart -> GenPart
forall a b. (a -> b) -> a -> b
$ RString -> [(RString, GenPart)] -> Maybe GenPart
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup RString
ident [(RString, GenPart)]
holeMap

      holeNumbers :: [Int]
holeNumbers   = [Int
0 .. [NamedArg HoleName] -> 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

      -- The WildHoles 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.
      insertWildHoles :: [GenPart] -> [GenPart]
      insertWildHoles :: Notation -> Notation
insertWildHoles Notation
xs = (Ranged Int -> Notation -> Notation)
-> Notation -> [Ranged Int] -> Notation
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)
            | 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
== Ranged Int
w = Range -> NamedArg (Ranged Int) -> GenPart
NormalHole Range
r NamedArg (Ranged Int)
h GenPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Ranged Int -> GenPart
WildHole Ranged Int
w GenPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Notation
hs
          ins Ranged Int
w (GenPart
h : Notation
hs) = GenPart
h GenPart -> Notation -> Notation
forall a. a -> [a] -> [a]
: Ranged Int -> Notation -> Notation
insBefore Ranged Int
w Notation
hs
          ins Ranged Int
_ [] = Notation
forall a. HasCallStack => a
__IMPOSSIBLE__

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

      -- Create a map (association list) from hole names to holes.
      -- A @LambdaHole@ contributes two entries:
      -- both names are mapped to the same number,
      -- but distinguished by BindHole vs. NormalHole.
      holeMap :: [(RString, GenPart)]
      holeMap :: [(RString, GenPart)]
holeMap = do
        (Int
i, NamedArg HoleName
h) <- [(Int, NamedArg HoleName)]
numberedHoles    -- v This range is filled in by mkPart
        let ri :: t -> Ranged Int
ri t
x = Range -> Int -> Ranged Int
forall a. Range -> a -> Ranged a
Ranged (t -> Range
forall t. HasRange t => t -> Range
getRange t
x) Int
i
            normalHole :: t -> GenPart
normalHole t
y = Range -> NamedArg (Ranged Int) -> GenPart
NormalHole Range
forall a. Range' a
noRange (NamedArg (Ranged Int) -> GenPart)
-> NamedArg (Ranged Int) -> GenPart
forall a b. (a -> b) -> a -> b
$ (Named NamedName HoleName -> Named NamedName (Ranged Int))
-> NamedArg HoleName -> NamedArg (Ranged Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (t -> Ranged Int
forall t. HasRange t => t -> Ranged Int
ri t
y Ranged Int
-> Named NamedName HoleName -> Named NamedName (Ranged Int)
forall (f :: * -> *) a b. Functor f => a -> f b -> f a
<$) NamedArg HoleName
h
        case NamedArg HoleName -> HoleName
forall a. NamedArg a -> a
namedArg NamedArg HoleName
h of
          ExprHole RString
y       -> [(RString
y, RString -> GenPart
forall t. HasRange t => t -> GenPart
normalHole RString
y)]
          LambdaHole RString
x RString
y
            | String
"_" <- RString -> String
forall a. Ranged a -> a
rangedThing RString
x -> [(RString
x, Ranged Int -> GenPart
WildHole (RString -> Ranged Int
forall t. HasRange t => t -> Ranged Int
ri RString
x)),         (RString
y, RString -> GenPart
forall t. HasRange t => t -> GenPart
normalHole RString
y)]
            | Bool
otherwise            -> [(RString
x, Range -> Ranged Int -> GenPart
BindHole Range
forall a. Range' a
noRange (RString -> Ranged Int
forall t. HasRange t => t -> Ranged Int
ri RString
x)), (RString
y, RString -> GenPart
forall t. HasRange t => t -> GenPart
normalHole RString
y)]
                                                 -- Filled in by mkPart

      -- Check whether all hole names are distinct.
      -- The hole names are the keys of the @holeMap@.
      uniqueHoleNames :: Bool
uniqueHoleNames = [RString] -> Bool
forall a. Eq a => [a] -> Bool
distinct [ RString
x | (RString
x, GenPart
_) <- [(RString, GenPart)]
holeMap, RString -> String
forall a. Ranged a -> a
rangedThing RString
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"_" ]

      isExprLinear :: Notation -> Bool
isExprLinear   Notation
xs = [Int] -> [Int]
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 ] [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
== [Int]
holeNumbers
      isLambdaLinear :: Notation -> Bool
isLambdaLinear Notation
xs = [Int] -> [Int]
forall a. Ord a => [a] -> [a]
List.sort [ Ranged Int -> Int
forall a. Ranged a -> a
rangedThing Ranged Int
x | BindHole Range
_ Ranged Int
x <- Notation
xs ] [Int] -> [Int] -> Bool
forall a. Eq a => a -> a -> Bool
==
                          [ Int
i | (Int
i, NamedArg HoleName
h) <- [(Int, NamedArg HoleName)]
numberedHoles,
                                LambdaHole RString
x RString
_ <- [NamedArg HoleName -> HoleName
forall a. NamedArg a -> a
namedArg NamedArg HoleName
h], RString -> String
forall a. Ranged a -> a
rangedThing RString
x String -> String -> Bool
forall a. Eq a => a -> a -> Bool
/= String
"_" ]

      isAlternating :: [GenPart] -> Bool
      isAlternating :: Notation -> Bool
isAlternating []       = Bool
forall a. HasCallStack => a
__IMPOSSIBLE__
      isAlternating [GenPart
x]      = Bool
True
      isAlternating (GenPart
x:GenPart
y:Notation
xs) = GenPart -> Bool
isAHole GenPart
x Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
/= GenPart -> Bool
isAHole GenPart
y Bool -> Bool -> Bool
&& Notation -> Bool
isAlternating (GenPart
yGenPart -> Notation -> Notation
forall a. a -> [a] -> [a]
:Notation
xs)

      isSingleHole :: [GenPart] -> Bool
      isSingleHole :: Notation -> Bool
isSingleHole = \case
        [ IdPart{} ] -> Bool
False
        [ GenPart
_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 -> String
(Int -> NewNotation -> ShowS)
-> (NewNotation -> String)
-> ([NewNotation] -> ShowS)
-> Show NewNotation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NewNotation] -> ShowS
$cshowList :: [NewNotation] -> ShowS
show :: NewNotation -> String
$cshow :: NewNotation -> String
showsPrec :: Int -> NewNotation -> ShowS
$cshowsPrec :: Int -> NewNotation -> ShowS
Show

instance LensFixity NewNotation where
  lensFixity :: (Fixity -> f Fixity) -> NewNotation -> f NewNotation
lensFixity Fixity -> f Fixity
f NewNotation
nota = Fixity -> f Fixity
f (NewNotation -> Fixity
notaFixity NewNotation
nota) f Fixity -> (Fixity -> NewNotation) -> f NewNotation
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 :: QName -> Set Name -> Fixity -> Notation -> Bool -> NewNotation
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

-- | Replace 'noFixity' by 'defaultFixity'.
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 :: 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
_) =
  ((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) [Range -> NameInScope -> [NamePart] -> Name
Name Range
forall a. Range' a
noRange NameInScope
InScope [String -> NamePart
Id (String -> NamePart) -> String -> NamePart
forall a b. (a -> b) -> a -> b
$ RString -> String
forall a. Ranged a -> a
rangedThing RString
x] | IdPart RString
x <- Notation
parts ]
  where
    -- The qualification of @q@.
    modules :: [Name]
modules     = [Name] -> [Name]
forall a. [a] -> [a]
init (QName -> [Name]
qnameParts QName
q)
    -- Putting the qualification onto @x@.
    reQualify :: Name -> QName
reQualify Name
x = (Name -> QName -> QName) -> QName -> [Name] -> QName
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 'NormalHole's, 'Id's become 'IdParts'.
--   If 'Name' has no 'Hole's, it returns 'noNotation'.
syntaxOf :: Name -> Notation
syntaxOf :: Name -> Notation
syntaxOf (NoName Range
_ NameId
_)    = Notation
noNotation
syntaxOf (Name Range
_ NameInScope
_ [NamePart
_])  = Notation
noNotation
syntaxOf (Name Range
_ NameInScope
_ [NamePart]
xs)   = Int -> [NamePart] -> Notation
mkSyn Int
0 [NamePart]
xs
  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) -> GenPart
NormalHole 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) GenPart -> 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 String
x : [NamePart]
xs) = RString -> GenPart
IdPart (String -> RString
forall a. a -> Ranged a
unranged String
x) GenPart -> Notation -> Notation
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 :: [NewNotation] -> [NewNotation]
mergeNotations :: [NewNotation] -> [NewNotation]
mergeNotations =
  ([NewNotation] -> NewNotation) -> [[NewNotation]] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map [NewNotation] -> NewNotation
merge ([[NewNotation]] -> [NewNotation])
-> ([NewNotation] -> [[NewNotation]])
-> [NewNotation]
-> [NewNotation]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  ([NewNotation] -> [[NewNotation]])
-> [[NewNotation]] -> [[NewNotation]]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap [NewNotation] -> [[NewNotation]]
groupIfLevelsMatch ([[NewNotation]] -> [[NewNotation]])
-> ([NewNotation] -> [[NewNotation]])
-> [NewNotation]
-> [[NewNotation]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
  (NewNotation -> (Notation, Bool))
-> [NewNotation] -> [[NewNotation]]
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 []         = [[NewNotation]]
forall a. HasCallStack => a
__IMPOSSIBLE__
  groupIfLevelsMatch ns :: [NewNotation]
ns@(NewNotation
n : [NewNotation]
_) =
    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 [[NewNotation] -> [NewNotation]
sameAssoc ([NewNotation] -> [NewNotation]
sameLevel [NewNotation]
ns)]
    else (NewNotation -> [NewNotation]) -> [NewNotation] -> [[NewNotation]]
forall a b. (a -> b) -> [a] -> [b]
map (NewNotation -> [NewNotation] -> [NewNotation]
forall a. a -> [a] -> [a]
: []) [NewNotation]
ns
    where
    -- Fixities of operators whose precedence level is not Unrelated.
    related :: [Fixity]
related = (NewNotation -> Maybe Fixity) -> [NewNotation] -> [Fixity]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe ((\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)
                              (Fixity -> Maybe Fixity)
-> (NewNotation -> Fixity) -> NewNotation -> Maybe Fixity
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NewNotation -> Fixity
notaFixity) [NewNotation]
ns

    -- Precondition: All related operators have the same precedence
    -- level.
    --
    -- Gives all unrelated operators the same level.
    sameLevel :: [NewNotation] -> [NewNotation]
sameLevel = (NewNotation -> NewNotation) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (Lens' FixityLevel NewNotation -> LensSet FixityLevel NewNotation
forall i o. Lens' i o -> LensSet i o
set ((Fixity -> f Fixity) -> NewNotation -> f NewNotation
Lens' Fixity NewNotation
_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' FixityLevel Fixity
_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 :: [NewNotation] -> [NewNotation]
sameAssoc = (NewNotation -> NewNotation) -> [NewNotation] -> [NewNotation]
forall a b. (a -> b) -> [a] -> [b]
map (Lens' Associativity NewNotation
-> LensSet Associativity NewNotation
forall i o. Lens' i o -> LensSet i o
set ((Fixity -> f Fixity) -> NewNotation -> f NewNotation
Lens' Fixity NewNotation
_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' Associativity Fixity
_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 :: [NewNotation] -> NewNotation
  merge :: [NewNotation] -> NewNotation
merge []         = NewNotation
forall a. HasCallStack => a
__IMPOSSIBLE__
  merge ns :: [NewNotation]
ns@(NewNotation
n : [NewNotation]
_) = NewNotation
n { notaNames :: Set Name
notaNames = [Set Name] -> Set Name
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([Set Name] -> Set Name) -> [Set Name] -> Set Name
forall a b. (a -> b) -> a -> b
$ (NewNotation -> Set Name) -> [NewNotation] -> [Set Name]
forall a b. (a -> b) -> [a] -> [b]
map NewNotation -> Set Name
notaNames [NewNotation]
ns }

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

_notaFixity :: Lens' Fixity NewNotation
_notaFixity :: (Fixity -> f Fixity) -> NewNotation -> f NewNotation
_notaFixity Fixity -> f Fixity
f NewNotation
r = Fixity -> f Fixity
f (NewNotation -> Fixity
notaFixity NewNotation
r) f Fixity -> (Fixity -> NewNotation) -> f NewNotation
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 -> String
(Int -> NotationSection -> ShowS)
-> (NotationSection -> String)
-> ([NotationSection] -> ShowS)
-> Show NotationSection
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [NotationSection] -> ShowS
$cshowList :: [NotationSection] -> ShowS
show :: NotationSection -> String
$cshow :: NotationSection -> String
showsPrec :: Int -> NotationSection -> ShowS
$cshowsPrec :: Int -> NotationSection -> ShowS
Show

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

noSection :: NewNotation -> NotationSection
noSection :: NewNotation -> NotationSection
noSection NewNotation
n = NotationSection :: NewNotation
-> NotationKind -> Maybe FixityLevel -> Bool -> NotationSection
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
  }