{-# OPTIONS_GHC -Wunused-imports #-}
{-# OPTIONS_GHC -Wunused-matches #-}
{-# OPTIONS_GHC -Wunused-binds #-}

{-# LANGUAGE CPP #-}

-- | Attributes: concrete syntax for ArgInfo.

module Mikan.Syntax.Concrete.Attribute where

import Prelude hiding (null)

#if !MIN_VERSION_base(4,20,0)
import Data.List (foldl')
#endif

import Data.Map (Map)
import Data.Map qualified as Map

import Mikan.Syntax.Common
import Mikan.Syntax.Concrete (Expr(..))
import Mikan.Syntax.Concrete.Pretty () --instance only
import Mikan.Syntax.Common.Pretty (prettyShow)
import Mikan.Syntax.Position

import Mikan.Utils.Impossible

-- | An attribute is a modifier for a function argument.
--
-- Currently only tactic attributes are supported, so the functions
-- below look a bit silly.

data Attribute
  = TacticAttribute (Ranged Expr)
  deriving (Int -> Attribute -> ShowS
[Attribute] -> ShowS
Attribute -> String
(Int -> Attribute -> ShowS)
-> (Attribute -> String)
-> ([Attribute] -> ShowS)
-> Show Attribute
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Attribute -> ShowS
showsPrec :: Int -> Attribute -> ShowS
$cshow :: Attribute -> String
show :: Attribute -> String
$cshowList :: [Attribute] -> ShowS
showList :: [Attribute] -> ShowS
Show)

instance HasRange Attribute where
  getRange :: Attribute -> Range
getRange = \case
    TacticAttribute Ranged Expr
e    -> Ranged Expr -> Range
forall a. HasRange a => a -> Range
getRange Ranged Expr
e

instance SetRange Attribute where
  setRange :: Range -> Attribute -> Attribute
setRange Range
_ = \case
    TacticAttribute Ranged Expr
e    -> Ranged Expr -> Attribute
TacticAttribute Ranged Expr
e  -- -- $ setRange r e -- SetRange Expr not yet implemented

instance KillRange Attribute where
  killRange :: Attribute -> Attribute
killRange = \case
    TacticAttribute Ranged Expr
e    -> Ranged Expr -> Attribute
TacticAttribute    (Ranged Expr -> Attribute) -> Ranged Expr -> Attribute
forall a b. (a -> b) -> a -> b
$ KillRangeT (Ranged Expr)
forall a. KillRange a => KillRangeT a
killRange Ranged Expr
e

-- | Parsed attribute.

data Attr = Attr
  { Attr -> Range
attrRange :: Range       -- ^ Range includes the @.
  , Attr -> String
attrName  :: String      -- ^ Concrete, user written attribute for error reporting, not including the "@".
  , Attr -> Attribute
theAttr   :: Attribute   -- ^ Parsed attribute.
  } deriving (Int -> Attr -> ShowS
[Attr] -> ShowS
Attr -> String
(Int -> Attr -> ShowS)
-> (Attr -> String) -> ([Attr] -> ShowS) -> Show Attr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Attr -> ShowS
showsPrec :: Int -> Attr -> ShowS
$cshow :: Attr -> String
show :: Attr -> String
$cshowList :: [Attr] -> ShowS
showList :: [Attr] -> ShowS
Show)

instance HasRange Attr where
  getRange :: Attr -> Range
getRange = Attr -> Range
attrRange

instance SetRange Attr where
  setRange :: Range -> Attr -> Attr
setRange Range
r (Attr Range
_ String
x Attribute
a) = Range -> String -> Attribute -> Attr
Attr Range
r String
x Attribute
a

instance KillRange Attr where
  killRange :: Attr -> Attr
killRange (Attr Range
_ String
x Attribute
a) = Range -> String -> Attribute -> Attr
Attr Range
forall a. Range' a
noRange String
x (Attribute -> Attribute
forall a. KillRange a => KillRangeT a
killRange Attribute
a)

-- | Information about attributes (attribute, range, printed
-- representation).
--
-- This information is returned by the parser. Code that calls the
-- parser should, if appropriate, complain if support for the given
-- attributes has not been enabled. This can be taken care of by
-- 'Agda.Syntax.Translation.ConcreteToAbstract.checkAttributes', which
-- should not be called until after pragma options have been set.

type Attributes = [Attr]

-- | Concrete syntax for all attributes.

attributesMap :: Map String Attribute
attributesMap :: Map String Attribute
attributesMap = (Attribute -> Attribute -> Attribute)
-> [(String, Attribute)] -> Map String Attribute
forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
Map.fromListWith Attribute -> Attribute -> Attribute
forall a. HasCallStack => a
__IMPOSSIBLE__ []

-- | Parsing a string into an attribute.

stringToAttribute :: String -> Maybe Attribute
stringToAttribute :: String -> Maybe Attribute
stringToAttribute = (String -> Map String Attribute -> Maybe Attribute
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` Map String Attribute
attributesMap)

-- | Parsing an expression into an attribute.

exprToAttribute :: Range -> Expr -> Maybe Attribute
exprToAttribute :: Range -> Expr -> Maybe Attribute
exprToAttribute Range
r = \case
  Paren Range
_ (Tactic Range
_ Expr
t) -> Attribute -> Maybe Attribute
forall a. a -> Maybe a
Just (Attribute -> Maybe Attribute) -> Attribute -> Maybe Attribute
forall a b. (a -> b) -> a -> b
$ Ranged Expr -> Attribute
TacticAttribute (Ranged Expr -> Attribute) -> Ranged Expr -> Attribute
forall a b. (a -> b) -> a -> b
$ Range -> Expr -> Ranged Expr
forall a. Range -> a -> Ranged a
Ranged Range
r Expr
t
  Expr
e -> Range -> Maybe Attribute -> Maybe Attribute
forall a. SetRange a => Range -> a -> a
setRange Range
r (Maybe Attribute -> Maybe Attribute)
-> Maybe Attribute -> Maybe Attribute
forall a b. (a -> b) -> a -> b
$ String -> Maybe Attribute
stringToAttribute (String -> Maybe Attribute) -> String -> Maybe Attribute
forall a b. (a -> b) -> a -> b
$ Expr -> String
forall a. Pretty a => a -> String
prettyShow Expr
e