module Agda.Syntax.Notation where
import Control.Applicative
import Control.Monad (when)
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 _ [] = fail "empty notation is disallowed"
mkNotation holes ids = do
xs <- mapM mkPart ids
when (not (isAlternating xs)) $ fail "syntax must alternate holes and non-holes"
when (not (isExprLinear xs)) $ fail "syntax must use holes exactly once"
when (not (isLambdaLinear xs)) $ fail "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
_ -> fail "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 = []