-- |
-- Module      :  $Header$
-- Copyright   :  (c) 2013-2015 Galois, Inc.
-- License     :  BSD3
-- Maintainer  :  cryptol@galois.com
-- Stability   :  provisional
-- Portability :  portable

{-# LANGUAGE Safe, PatternGuards #-}
module Cryptol.Parser.ParserUtils where

import Cryptol.Parser.AST
import Cryptol.Parser.Lexer
import Cryptol.Parser.Position
import Cryptol.Prims.Syntax
import Cryptol.Parser.Utils (translateExprToNumT)
import Cryptol.Utils.PP
import Cryptol.Utils.Panic

import Data.Maybe(listToMaybe,fromMaybe)
import Data.Bits(testBit,setBit)
import Control.Monad(liftM,ap)

#if __GLASGOW_HASKELL__ < 710
import Control.Applicative ((<$>),Applicative(..))
import Data.Traversable (mapM)
import Prelude hiding (mapM)
#endif

parse :: Config -> ParseM a -> String -> Either ParseError a
parse cfg p cs    = case unP p cfg eofPos (S toks) of
                      Left err    -> Left err
                      Right (a,_) -> Right a
  where (toks,eofPos) = lexer cfg cs


{- The parser is parameterized by the pozition of the final token. -}
data ParseM a   = P { unP :: Config -> Position -> S -> Either ParseError (a,S) }


lexerP :: (Located Token -> ParseM a) -> ParseM a
lexerP k = P $ \cfg p (S ts) ->
  case ts of
    t : _ | Err e <- tokenType it ->
      Left $ HappyErrorMsg (srcRange t) $
         case e of
           UnterminatedComment -> "unterminated comment"
           UnterminatedString  -> "unterminated string"
           UnterminatedChar    -> "unterminated character"
           InvalidString       -> "invalid string literal: " ++ tokenText it
           InvalidChar         -> "invalid character literal: " ++ tokenText it
           LexicalError        -> "lexical error: " ++ tokenText it
      where it = thing t

    t : more -> unP (k t) cfg p (S more)
    []       -> Left (HappyError (cfgSource cfg) p Nothing)

data ParseError = HappyError FilePath Position (Maybe Token)
                | HappyErrorMsg Range String
                  deriving Show

newtype S = S [Located Token]

instance PP ParseError where
  ppPrec _ (HappyError _ _ tok) = case tok of
                                  Nothing -> text "end of input"
                                  Just t  -> pp t
  ppPrec _ (HappyErrorMsg _ x) = text x

ppError :: ParseError -> Doc
ppError (HappyError path pos (Just tok))
  | Err _ <- tokenType tok = text "Parse error at" <+>
                              text path <> char ':' <> pp pos <> comma <+>
                              pp tok
ppError e@(HappyError path pos _) =
                               text "Parse error at" <+>
                               text path <> char ':' <> pp pos <> comma <+>
                               text "unexpected" <+> pp e
ppError (HappyErrorMsg p x)  = text "Parse error at" <+> pp p $$ nest 2 (text x)

instance Monad ParseM where
  return a  = P (\_ _ s -> Right (a,s))
  fail s    = panic "[Parser] fail" [s]
  m >>= k   = P (\cfg p s1 -> case unP m cfg p s1 of
                            Left e       -> Left e
                            Right (a,s2) -> unP (k a) cfg p s2)

instance Functor ParseM where
  fmap = liftM

instance Applicative ParseM where
  pure  = return
  (<*>) = ap

happyError :: ParseM a
happyError = P $ \cfg p (S ls) ->
  Left $ case listToMaybe ls of
           Nothing -> HappyError (cfgSource cfg) p Nothing
           Just l  -> HappyError (cfgSource cfg) (from (srcRange l)) (Just (thing l))

errorMessage :: Range -> String -> ParseM a
errorMessage r x = P $ \_ _ _ -> Left (HappyErrorMsg r x)

customError :: String -> Located Token -> ParseM a
customError x t = P $ \_ _ _ -> Left (HappyErrorMsg (srcRange t) x)

mkModName :: {-reversed-} [LName] -> Located ModName
mkModName xs = Located { srcRange = rComb (srcRange f) (srcRange l)
                       , thing    = ModName [ x | Name x <- map thing ns ]
                       }
  where l : _       = xs
        ns@(f : _)  = reverse xs

mkQName :: {-reversed-} [LName] -> Located QName
mkQName [x] = fmap mkUnqual x
mkQName xs =
  Located { srcRange = rComb (srcRange f) (srcRange l)
          , thing    = mkQual (ModName [ x | Name x <- map thing ns ]) (thing l)
          }
  where l : ls      = xs
        ns@(f : _)  = reverse ls

-- Note that type variables are not resolved at this point: they are tcons.
mkSchema :: [TParam] -> [Prop] -> Type -> Schema
mkSchema xs ps t = Forall xs ps t Nothing

getName :: Located Token -> Name
getName l = case thing l of
              Token (Ident x) _ -> Name x
              _ -> panic "[Parser] getName" ["not an Ident:", show l]

getNum :: Located Token -> Integer
getNum l = case thing l of
             Token (Num x _ _) _ -> x
             Token (ChrLit x) _  -> fromIntegral (fromEnum x)
             _ -> panic "[Parser] getNum" ["not a number:", show l]

getStr :: Located Token -> String
getStr l = case thing l of
             Token (StrLit x) _ -> x
             _ -> panic "[Parser] getStr" ["not a string:", show l]

numLit :: TokenT -> Expr
numLit (Num x base digs)
  | base == 2   = ELit $ ECNum x (BinLit digs)
  | base == 8   = ELit $ ECNum x (OctLit digs)
  | base == 10  = ELit $ ECNum x DecLit
  | base == 16  = ELit $ ECNum x (HexLit digs)

numLit x = panic "[Parser] numLit" ["invalid numeric literal", show x]


mkTupleSel :: Range -> Integer -> ParseM (Located Selector)
mkTupleSel pos n
  | n < 0 = errorMessage pos
             (show n ++ " is not a valid tuple selector (they start from 0).")
  | toInteger asInt /= n  = errorMessage pos "Tuple selector is too large."
  | otherwise             = return $ Located pos $ TupleSel asInt Nothing
  where asInt = fromInteger n

fromStrLit :: Located Token -> ParseM (Located String)
fromStrLit loc = case tokenType (thing loc) of
  StrLit str -> return loc { thing = str }
  _          -> errorMessage (srcRange loc) "Expected a string literal"


validDemotedType :: Range -> Type -> ParseM Type
validDemotedType rng ty =
  case ty of
    TLocated t r -> validDemotedType r t
    TRecord {}   -> bad "Record types"
    TTuple {}    -> bad "Tuple types"
    TFun {}      -> bad "Function types"
    TSeq {}      -> bad "Sequence types"
    TBit         -> bad "Type bit"
    TNum {}      -> ok
    TChar {}     -> ok
    TInf         -> bad "Infinity type"
    TWild        -> bad "Wildcard types"
    TUser {}     -> ok
    TApp {}      -> ok

  where bad x = errorMessage rng (x ++ " cannot be demoted.")
        ok    = return $ at rng ty

mkEApp :: [Expr] -> Expr
mkEApp es@(eLast : _) = at (eFirst,eLast) $ foldl EApp f xs
  where
  eFirst : rest = reverse es
  f : xs        = cvtTypeParams eFirst rest

  {- Type applications are parsed as `ETypeVal (TRecord fs)` expressions.
     Here we associate them with their corresponding functions,
     converting them into `EAppT` constructs.  For example:

     [ f, x, `{ a = 2 }, y ]
     becomes
     [ f, x ` { a = 2 }, y ]
  -}
  cvtTypeParams e [] = [e]
  cvtTypeParams e (p : ps) =
    case toTypeParam p of
      Just fs -> cvtTypeParams (EAppT e fs) ps
      Nothing -> e : cvtTypeParams p ps

  toTypeParam e =
    case dropLoc e of
      ETypeVal t -> case dropLoc t of
                      TRecord fs -> Just (map mkTypeInst fs)
                      _          -> Nothing
      _          ->  Nothing

mkEApp es        = panic "[Parser] mkEApp" ["Unexpected:", show es]


op :: ECon -> Range -> Expr
op s r = at r (ECon s)

unOp :: Expr -> Expr -> Expr
unOp f x = at (f,x) $ EApp f x

binOp :: Expr -> Expr -> Expr -> Expr
binOp x f y = at (x,y) $ EApp (EApp f x) y

eFromTo :: Range -> Expr -> Maybe Expr -> Maybe Expr -> ParseM Expr
eFromTo r e1 e2 e3 = EFromTo <$> exprToNumT r e1
                             <*> mapM (exprToNumT r) e2
                             <*> mapM (exprToNumT r) e3
exprToNumT :: Range -> Expr -> ParseM Type
exprToNumT r expr =
  case translateExprToNumT expr of
    Just t -> return t
    Nothing -> bad
  where
  bad = errorMessage (fromMaybe r (getLoc expr)) $ unlines
        [ "The boundaries of .. sequences should be valid numeric types."
        , "The expression `" ++ show (pp expr) ++ "` is not."
        , ""
        , "If you were trying to specify the width of the elements,"
        , "you may add a type annotation outside the sequence. For example:"
        , "   [ 1 .. 10 ] : [_][16]"
        ]


-- | WARNING: This is a bit of a hack.
-- It is used to represent anonymous type applications.
anonRecord :: Maybe Range -> [Type] -> Type
anonRecord ~(Just r) ts = TRecord (map toField ts)
  where noName    = Located { srcRange = r, thing = Name "" }
        toField t = Named { name = noName, value = t }

exportDecl :: ExportType -> Decl -> TopDecl
exportDecl e d = Decl TopLevel { tlExport = e, tlValue = d }

exportNewtype :: ExportType -> Newtype -> TopDecl
exportNewtype e n = TDNewtype TopLevel { tlExport = e, tlValue = n }

changeExport :: ExportType -> [TopDecl] -> [TopDecl]
changeExport e = map $ \ td -> case td of
  Decl d      -> Decl      d { tlExport = e }
  TDNewtype n -> TDNewtype n { tlExport = e }
  Include _   -> td

mkTypeInst :: Named Type -> TypeInst
mkTypeInst x | thing (name x) == Name "" = PosInst (value x)
             | otherwise                 = NamedInst x


mkTParam :: Located Name -> Maybe Kind -> ParseM TParam
mkTParam Located { srcRange = rng, thing = n } k
  | Name "width" <- n = errorMessage rng "`width` is not a valid type parameter name."
  | otherwise = return (TParam n k (Just rng))

mkTySyn :: Located Name -> [TParam] -> Type -> ParseM Decl
mkTySyn n ps b
  | Name "width" <- thing n = errorMessage (srcRange n) "`width` is not a valid type synonym name."
  | otherwise = return $ DType $ TySyn (fmap mkUnqual n) ps b

polyTerm :: Range -> Integer -> Integer -> ParseM (Bool, Integer)
polyTerm rng k p
  | k == 0          = return (False, p)
  | k == 1          = return (True, p)
  | otherwise       = errorMessage rng "Invalid polynomial coefficient"

mkPoly :: Range -> [ (Bool,Integer) ] -> ParseM Expr
mkPoly rng terms = mk 0 (map fromInteger bits)
  where
  w    = case terms of
           [] -> 0
           _  -> 1 + maximum (map (fromInteger . snd) terms)
  bits = [ n | (True,n) <- terms ]

  mk res []         = return $ ELit $ ECNum res (PolyLit w)
  mk res (n : ns)
    | testBit res n = errorMessage rng
                       ("Polynomial contains multiple terms with exponent "
                                                                    ++ show n)
    | otherwise     = mk (setBit res n) ns


-- NOTE: The list of patterns is reversed!
mkProperty :: LName -> [Pattern] -> Expr -> Decl
mkProperty f ps e = DBind Bind { bName       = fmap mkUnqual f
                               , bParams     = reverse ps
                               , bDef        = ETyped e TBit
                               , bSignature  = Nothing
                               , bPragmas    = [PragmaProperty]
                               , bMono       = False
                               }

mkIf :: [(Expr, Expr)] -> Expr -> Expr
mkIf ifThens theElse = foldr addIfThen theElse ifThens
    where
    addIfThen (cond, doexpr) elseExpr = EIf cond doexpr elseExpr