{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
module Agda.Syntax.Notation where
import Control.DeepSeq
import Control.Monad
import qualified Data.List as List
import Data.Maybe
import Data.Data (Data)
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)
| WildHole !Int
| IdPart RawName
deriving (Data, Show, Eq, Ord)
instance KillRange GenPart where
killRange p = case p of
IdPart x -> IdPart x
BindHole i -> BindHole i
WildHole i -> WildHole i
NormalHole x -> NormalHole $ killRange x
instance NFData GenPart where
rnf (BindHole _) = ()
rnf (NormalHole a) = rnf a
rnf (WildHole _) = ()
rnf (IdPart a) = rnf a
stringParts :: Notation -> [RawName]
stringParts gs = [ x | IdPart x <- gs ]
holeTarget :: GenPart -> Maybe Int
holeTarget (BindHole n) = Just n
holeTarget (WildHole n) = Just n
holeTarget (NormalHole n) = Just $ namedArg n
holeTarget IdPart{} = Nothing
isAHole :: GenPart -> Bool
isAHole BindHole{} = True
isAHole NormalHole{} = True
isAHole WildHole{} = False
isAHole IdPart{} = False
isNormalHole :: GenPart -> Bool
isNormalHole NormalHole{} = True
isNormalHole BindHole{} = False
isNormalHole WildHole{} = False
isNormalHole IdPart{} = False
isBindingHole :: GenPart -> Bool
isBindingHole (BindHole _) = True
isBindingHole (WildHole _) = True
isBindingHole _ = False
data NotationKind
= InfixNotation
| PrefixNotation
| PostfixNotation
| NonfixNotation
| NoNotation
deriving (Eq, Show)
notationKind :: Notation -> NotationKind
notationKind [] = NoNotation
notationKind syn =
case (isNormalHole $ head syn, isNormalHole $ last syn) of
(True , True ) -> InfixNotation
(True , False) -> PostfixNotation
(False, True ) -> PrefixNotation
(False, False) -> NonfixNotation
mkNotation :: [NamedArg 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 $ insertWildHoles xs
where
mkPart ident = fromMaybe (IdPart ident) $ lookup ident holeMap
holeNumbers = [0 .. length holes - 1]
numberedHoles = zip holeNumbers holes
insertWildHoles xs = foldr ins xs wilds
where
wilds = [ i | (_, WildHole i) <- holeMap ]
ins w (NormalHole h : hs)
| namedArg h == w = NormalHole h : WildHole w : hs
ins w (h : hs) = h : insBefore w hs
ins _ [] = __IMPOSSIBLE__
insBefore w (NormalHole h : hs)
| namedArg h == w = WildHole w : NormalHole h : hs
insBefore w (h : hs) = h : insBefore w hs
insBefore _ [] = __IMPOSSIBLE__
holeMap = do
(i, h) <- numberedHoles
let normalHole = NormalHole $ fmap (i <$) h
case namedArg h of
ExprHole y -> [(y, normalHole)]
LambdaHole "_" y -> [("_", WildHole i), (y, normalHole)]
LambdaHole x y -> [(x, BindHole i), (y, normalHole)]
uniqueHoleNames = distinct [ x | (x, _) <- holeMap, x /= "_" ]
isExprLinear xs = List.sort [ i | x <- xs, isNormalHole x, let Just i = holeTarget x ] == holeNumbers
isLambdaLinear xs = List.sort [ x | BindHole x <- xs ] ==
[ i | (i, h) <- numberedHoles,
LambdaHole x _ <- [namedArg h], x /= "_" ]
isAlternating :: [GenPart] -> Bool
isAlternating [] = __IMPOSSIBLE__
isAlternating [x] = True
isAlternating (x:y:xs) = isAHole x /= isAHole y && isAlternating (y:xs)
noNotation :: Notation
noNotation = []