module Agda.Syntax.Notation where
import Control.Applicative
import Control.Monad
import Data.List
import Data.Maybe
import Data.Typeable (Typeable)
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Utils.Except ( MonadError(throwError) )
import Agda.Utils.List
import Agda.Utils.Impossible
#include "undefined.h"
data HoleName
= LambdaHole { _bindHoleName :: RawName
, holeName :: RawName }
| ExprHole { holeName :: RawName }
isLambdaHole :: HoleName -> Bool
isLambdaHole (LambdaHole _ _) = True
isLambdaHole _ = False
type Notation = [GenPart]
data GenPart
= BindHole Int
| NormalHole (NamedArg () Int)
| IdPart RawName
deriving (Typeable, Show, Eq, Ord)
instance KillRange GenPart where
killRange p = case p of
IdPart x -> IdPart x
BindHole i -> BindHole i
NormalHole x -> NormalHole $ killRange x
stringParts :: Notation -> [RawName]
stringParts gs = [ x | IdPart x <- gs ]
holeTarget :: GenPart -> Maybe Int
holeTarget (BindHole n) = Just n
holeTarget (NormalHole n) = Just $ namedArg n
holeTarget IdPart{} = Nothing
isAHole :: GenPart -> Bool
isAHole = isJust . holeTarget
isBindingHole :: GenPart -> Bool
isBindingHole (BindHole _) = True
isBindingHole _ = False
data NotationKind
= InfixNotation
| PrefixNotation
| PostfixNotation
| NonfixNotation
| NoNotation
deriving (Eq, Show)
notationKind :: Notation -> NotationKind
notationKind [] = NoNotation
notationKind syn =
case (isAHole $ head syn, isAHole $ last syn) of
(True , True ) -> InfixNotation
(True , False) -> PostfixNotation
(False, True ) -> PrefixNotation
(False, False) -> NonfixNotation
mkNotation :: [NamedArg c HoleName] -> [RawName] -> Either String Notation
mkNotation _ [] = throwError "empty notation is disallowed"
mkNotation holes ids = do
unless uniqueHoleNames $ throwError "syntax must use unique argument names"
let xs :: Notation = map mkPart ids
unless (isAlternating xs) $ throwError "syntax must alternate holes and non-holes"
unless (isExprLinear xs) $ throwError "syntax must use holes exactly once"
unless (isLambdaLinear xs) $ throwError "syntax must use binding holes exactly once"
return xs
where
mkPart ident = fromMaybe (IdPart ident) $ lookup ident holeMap
holeNumbers = [0 .. length holes 1]
numberedHoles = zip holeNumbers holes
holeMap = do
(i, h) <- numberedHoles
let normalHole = NormalHole $ setArgColors [] $ fmap (i <$) h
case namedArg h of
ExprHole y -> [(y, normalHole)]
LambdaHole x y -> [(x, BindHole i), (y, normalHole)]
uniqueHoleNames = distinct $ map fst holeMap
isExprLinear xs = sort [ namedArg x | NormalHole x <- xs] == holeNumbers
isLambdaLinear xs = sort [ x | BindHole x <- xs] == [ i | (i, h) <- numberedHoles, isLambdaHole (namedArg h) ]
isAlternating :: [GenPart] -> Bool
isAlternating [] = __IMPOSSIBLE__
isAlternating [x] = True
isAlternating (x:y:xs) = isAHole x /= isAHole y && isAlternating (y:xs)
defaultNotation, noNotation :: Notation
defaultNotation = []
noNotation = []