{-# 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 :: RString
, holeName :: RString }
| ExprHole { holeName :: RString }
isLambdaHole :: HoleName -> Bool
isLambdaHole (LambdaHole _ _) = True
isLambdaHole _ = False
type Notation = [GenPart]
data GenPart
= BindHole Range (Ranged Int)
| NormalHole Range (NamedArg (Ranged Int))
| WildHole (Ranged Int)
| IdPart RString
deriving (Data, Show)
instance Eq GenPart where
BindHole _ i == BindHole _ j = i == j
NormalHole _ x == NormalHole _ y = x == y
WildHole i == WildHole j = i == j
IdPart x == IdPart y = x == y
_ == _ = False
instance Ord GenPart where
BindHole _ i `compare` BindHole _ j = i `compare` j
NormalHole _ x `compare` NormalHole _ y = x `compare` y
WildHole i `compare` WildHole j = i `compare` j
IdPart x `compare` IdPart y = x `compare` y
BindHole{} `compare` _ = LT
_ `compare` BindHole{} = GT
NormalHole{} `compare` _ = LT
_ `compare` NormalHole{} = GT
WildHole{} `compare` _ = LT
_ `compare` WildHole{} = GT
instance HasRange GenPart where
getRange p = case p of
IdPart x -> getRange x
BindHole r _ -> r
WildHole i -> getRange i
NormalHole r _ -> r
instance SetRange GenPart where
setRange r p = case p of
IdPart x -> IdPart x
BindHole _ i -> BindHole r i
WildHole i -> WildHole i
NormalHole _ i -> NormalHole r i
instance KillRange GenPart where
killRange p = case p of
IdPart x -> IdPart $ killRange x
BindHole _ i -> BindHole noRange $ killRange i
WildHole i -> WildHole $ killRange i
NormalHole _ x -> NormalHole noRange $ killRange x
instance NFData GenPart where
rnf (BindHole _ a) = rnf a
rnf (NormalHole _ a) = rnf a
rnf (WildHole a) = rnf a
rnf (IdPart a) = rnf a
stringParts :: Notation -> [String]
stringParts gs = [ rangedThing x | IdPart x <- gs ]
holeTarget :: GenPart -> Maybe Int
holeTarget (BindHole _ n) = Just $ rangedThing n
holeTarget (WildHole n) = Just $ rangedThing n
holeTarget (NormalHole _ n) = Just $ rangedThing $ 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] -> [RString] -> 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 $ concat
[ "syntax must alternate holes ("
, prettyHoles
, ") and non-holes ("
, prettyNonHoles xs
, ")"
]
unless (isExprLinear xs) $ throwError "syntax must use holes exactly once"
unless (isLambdaLinear xs) $ throwError "syntax must use binding holes exactly once"
when (isSingleHole xs) $ throwError "syntax cannot be a single hole"
return $ insertWildHoles xs
where
holeNames :: [RString]
holeNames = map namedArg holes >>= \case
LambdaHole x y -> [x, y]
ExprHole y -> [y]
prettyHoles :: String
prettyHoles = List.unwords $ map (rawNameToString . rangedThing) holeNames
nonHoleNames :: Notation -> [RString]
nonHoleNames xs = flip mapMaybe xs $ \case
WildHole{} -> Just $ unranged "_"
IdPart x -> Just x
BindHole{} -> Nothing
NormalHole{} -> Nothing
prettyNonHoles :: Notation -> String
prettyNonHoles = List.unwords . map (rawNameToString . rangedThing) . nonHoleNames
mkPart ident = maybe (IdPart ident) (`withRangeOf` ident) $ lookup ident holeMap
holeNumbers = [0 .. length holes - 1]
numberedHoles :: [(Int, NamedArg HoleName)]
numberedHoles = zip holeNumbers holes
insertWildHoles :: [GenPart] -> [GenPart]
insertWildHoles xs = foldr ins xs wilds
where
wilds = [ i | (_, WildHole i) <- holeMap ]
ins w (NormalHole r h : hs)
| namedArg h == w = NormalHole r h : WildHole w : hs
ins w (h : hs) = h : insBefore w hs
ins _ [] = __IMPOSSIBLE__
insBefore w (NormalHole r h : hs)
| namedArg h == w = WildHole w : NormalHole r h : hs
insBefore w (h : hs) = h : insBefore w hs
insBefore _ [] = __IMPOSSIBLE__
holeMap :: [(RString, GenPart)]
holeMap = do
(i, h) <- numberedHoles
let ri x = Ranged (getRange x) i
normalHole y = NormalHole noRange $ fmap (ri y <$) h
case namedArg h of
ExprHole y -> [(y, normalHole y)]
LambdaHole x y
| "_" <- rangedThing x -> [(x, WildHole (ri x)), (y, normalHole y)]
| otherwise -> [(x, BindHole noRange (ri x)), (y, normalHole y)]
uniqueHoleNames = distinct [ x | (x, _) <- holeMap, rangedThing x /= "_" ]
isExprLinear xs = List.sort [ i | x <- xs, isNormalHole x, let Just i = holeTarget x ] == holeNumbers
isLambdaLinear xs = List.sort [ rangedThing x | BindHole _ x <- xs ] ==
[ i | (i, h) <- numberedHoles,
LambdaHole x _ <- [namedArg h], rangedThing x /= "_" ]
isAlternating :: [GenPart] -> Bool
isAlternating [] = __IMPOSSIBLE__
isAlternating [x] = True
isAlternating (x:y:xs) = isAHole x /= isAHole y && isAlternating (y:xs)
isSingleHole :: [GenPart] -> Bool
isSingleHole = \case
[ IdPart{} ] -> False
[ _hole ] -> True
_ -> False
noNotation :: Notation
noNotation = []