module Agda.Syntax.Notation where
import Control.Applicative
import Control.Monad (when)
import Control.Monad.Error (throwError)
import Data.List
import Data.Maybe
import Data.Generics (Typeable, Data)
import System.FilePath
import Test.QuickCheck
import Agda.Syntax.Common
import Agda.Syntax.Position
import Agda.Utils.FileName
import Agda.Utils.Pretty
#include "../undefined.h"
import Agda.Utils.Impossible
data HoleName = LambdaHole String String
| ExprHole String
holeName (LambdaHole _ n) = n
holeName (ExprHole n) = n
type Notation = [GenPart]
data GenPart = BindHole Int
| NormalHole Int
| IdPart String
deriving (Data, Typeable, Show, Eq)
holeTarget (BindHole n) = Just n
holeTarget (NormalHole n) = Just n
holeTarget (IdPart _) = Nothing
isAHole :: GenPart -> Bool
isAHole = isJust . holeTarget
isBindingHole (BindHole _) = True
isBindingHole _ = False
isLambdaHole (LambdaHole _ _) = True
isLambdaHole _ = False
mkNotation :: [HoleName] -> [String] -> Either String Notation
mkNotation _ [] = throwError "empty notation is disallowed"
mkNotation holes ids = do
xs <- mapM mkPart ids
when (not (isAlternating xs)) $ throwError "syntax must alternate holes and non-holes"
when (not (isExprLinear xs)) $ throwError "syntax must use holes exactly once"
when (not (isLambdaLinear xs)) $ throwError "syntax must use binding holes exactly once"
return xs
where mkPart ident =
case (findIndices (\x -> ident == holeName x) holes,
findIndices (\x -> case x of LambdaHole ident' _ -> ident == ident';_ -> False) holes) of
([],[x]) -> return $ BindHole x
([x], []) -> return $ NormalHole x
([], []) -> return $ IdPart ident
_ -> throwError "hole names must be unique"
isExprLinear xs = sort [ x | NormalHole x <- xs] == [ i | (i,h) <- zip [0..] holes ]
isLambdaLinear xs = sort [ x | BindHole x <- xs] == [ i | (i,h) <- zip [0..] holes, isLambdaHole h ]
isAlternating :: [GenPart] -> Bool
isAlternating [] = __IMPOSSIBLE__
isAlternating [x] = True
isAlternating (x:y:xs) = isAHole x /= isAHole y && isAlternating (y:xs)
defaultNotation = []
noNotation = []