{-# LANGUAGE CPP, DeriveDataTypeable #-}


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.Typeable (Typeable)

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

{-| A name is a non-empty list of alternating 'Id's and 'Hole's. A normal name
    is represented by a singleton list, and operators are represented by a list
    with 'Hole's where the arguments should go. For instance: @[Hole,Id "+",Hole]@
    is infix addition.

    Equality and ordering on @Name@s are defined to ignore range so same names
    in different locations are equal.
-}

-- | Data type constructed in the Happy parser; converted to 'GenPart'
-- before it leaves the Happy code.
data HoleName = LambdaHole String String -- ^ (\x -> y) ; 1st argument is the bound name (unused for now)
              | ExprHole String          -- ^ simple named hole

-- | Target of a hole
holeName (LambdaHole _ n) = n
holeName (ExprHole n) = n

type Notation = [GenPart]

-- | Part of a Notation
data GenPart = BindHole Int  -- ^ Argument is the position of the hole (with binding) where the binding should occur.
             | NormalHole Int -- ^ Argument is where the expression should go
             | IdPart String
  deriving (Typeable, Show, Eq)

-- | Get a flat list of identifier parts of a notation.
stringParts :: Notation -> [String]
stringParts gs = [ x | IdPart x <- gs ]

-- | Target argument position of a part (Nothing if it is not a hole)
holeTarget (BindHole n) = Just n
holeTarget (NormalHole n) = Just n
holeTarget (IdPart _) = Nothing

-- | Is the part a hole?
isAHole :: GenPart -> Bool
isAHole = isJust . holeTarget

isBindingHole (BindHole _) = True
isBindingHole _ = False

isLambdaHole (LambdaHole _ _) = True
isLambdaHole _ = False


-- | From notation with names to notation with indices.
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)


-- | No notation by default
defaultNotation = []
noNotation = []