module Agda.Syntax.Notation where
import Control.Applicative
import Control.Monad
import Control.Monad.Error (throwError)
import Data.List
import Data.Maybe
import Data.Typeable (Typeable)
import Agda.Syntax.Common
#include "../undefined.h"
import Agda.Utils.Impossible
data HoleName = LambdaHole RawName RawName
| ExprHole RawName
holeName (LambdaHole _ n) = n
holeName (ExprHole n) = n
type Notation = [GenPart]
data GenPart = BindHole Int
| NormalHole (NamedArg () Int)
| IdPart RawName
deriving (Typeable, Show, Eq)
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 (BindHole _) = True
isBindingHole _ = False
isLambdaHole (LambdaHole _ _) = True
isLambdaHole _ = False
mkNotation :: [NamedArg c HoleName] -> [RawName] -> Either String Notation
mkNotation _ [] = throwError "empty notation is disallowed"
mkNotation holes ids = do
unless (uniqueNames holes) $ throwError "syntax must use unique argument names"
let xs = 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
holeMap = concat $ zipWith mkHole [0..] holes
where mkHole i h =
case namedArg h of
ExprHole x -> [(x, normalHole)]
LambdaHole x y -> [(x, BindHole i), (y, normalHole)]
where normalHole = NormalHole $ setArgColors [] $ fmap (i <$) h
uniqueNames hs = nub xs == xs
where xs = concatMap (names . namedArg) hs
names (ExprHole x) = [x]
names (LambdaHole x y) = [x, y]
isExprLinear xs = sort [ namedArg x | NormalHole x <- xs] == [ i | (i, h) <- zip [0..] holes ]
isLambdaLinear xs = sort [ x | BindHole x <- xs] == [ i | (i, h) <- zip [0..] holes, isLambdaHole (namedArg h) ]
isAlternating :: [GenPart] -> Bool
isAlternating [] = __IMPOSSIBLE__
isAlternating [x] = True
isAlternating (x:y:xs) = isAHole x /= isAHole y && isAlternating (y:xs)
defaultNotation = []
noNotation = []