{-# LANGUAGE DeriveDataTypeable     #-}
{-# LANGUAGE FlexibleInstances      #-}

module Language.Nano.Types (
  -- * Configuration Options
    Config (..)

  -- * Some Operators on Pred
  , pAnd
  , pOr

  -- * Nano Definition
  , IsNano (..)
  , checkTopStmt

  -- * Located Values
  , Located (..) 
  , IsLocated (..)

  -- * Accessing Spec Annotations
  , getSpec
  , getRequires
  , getEnsures
  , getAssume
  , getAssert
  , getInvariant
  , isSpecification
  , returnSymbol
  , returnId
  , symbolId
  , mkId

  -- * Error message
  , convertError

  -- * Deconstructing Id
  , idName
  , idLoc 
 
  -- * Manipulating SourceSpan
  , dummySpan
  , srcSpanFile
  , srcSpanStartLine
  , srcSpanEndLine
  , srcSpanStartCol
  , srcSpanEndCol

  -- * Hardwired Operators
  , HwOp (..)
  ) where

import           Control.Applicative          ((<$>))
-- import qualified Data.HashMap.Strict as M
import           Data.Hashable
import           Data.Typeable                      (Typeable)
import           Data.Generics                      (Data)   
import           Data.Generics.Aliases
import           Data.Generics.Schemes
import           Data.Monoid                        (Monoid (..))
import           Data.Maybe                         (catMaybes)
import           Language.ECMAScript3.Syntax 
import           Language.ECMAScript3.Syntax.Annotations
import           Language.ECMAScript3.PrettyPrint   (PP (..))
import           Language.ECMAScript3.Parser        (SourceSpan (..))

import qualified Language.Fixpoint.Types as F

import           Language.Fixpoint.PrettyPrint
import           Language.Fixpoint.Misc
import           Language.Nano.Errors
import           Text.PrettyPrint.HughesPJ
import           Text.Parsec                        
import           Text.Parsec.Pos                    (initialPos)
import           Text.Printf                        (printf)

---------------------------------------------------------------------
-- | Command Line Configuration Options
---------------------------------------------------------------------

data Config 
  = Esc    { files   :: [FilePath]     -- ^ source files to check
           , incdirs :: [FilePath]     -- ^ path to directory for include specs
           } 
  | TC     { files   :: [FilePath]     -- ^ source files to check
           , incdirs :: [FilePath]     -- ^ path to directory for include specs
           }
  | Liquid { files   :: [FilePath]     -- ^ source files to check
           , incdirs :: [FilePath]     -- ^ path to directory for include specs
           }
  deriving (Data, Typeable, Show, Eq)

---------------------------------------------------------------------
-- | Hardwired Operations ------------------------------------------- 
---------------------------------------------------------------------

data HwOp = BracketRead deriving (Eq, Ord, Show)

instance PP HwOp where 
  pp BracketRead = text "BracketRead" 

---------------------------------------------------------------------
-- | Tracking Source Code Locations --------------------------------- 
---------------------------------------------------------------------


data Located a 
  = Loc { loc :: !SourceSpan
        , val :: a
        }
 
instance Functor Located where 
  fmap f (Loc l x) = Loc l (f x)

-- | `IsLocated` is a predicate for values which we have a SourceSpan

class IsLocated a where 
  srcPos :: a -> SourceSpan

instance IsLocated SourceSpan where 
  srcPos x = x 

instance IsLocated (Located a) where 
  srcPos = loc

-- instance (IsLocated a, HasAnnotation t) => IsLocated (t a) where 
--   srcPos = srcPos . getAnnotation

instance IsLocated a => IsLocated (Id a) where 
  srcPos (Id x _) = srcPos x


instance HasAnnotation Id where 
  getAnnotation (Id x _) = x


instance Eq a => Eq (Located a) where 
  x == y = val x == val y

---------------------------------------------------------------------
-- | Wrappers around `Language.ECMAScript3.Syntax` ------------------
---------------------------------------------------------------------

-- | `IsNano` is a predicate that describes the **syntactic subset** 
--   of ECMAScript3 that comprises `Nano`.

class IsNano a where 
  isNano :: a -> Bool


instance IsNano InfixOp where
  isNano OpLT   = True -- ^ @<@
  isNano OpLEq  = True -- ^ @<=@
  isNano OpGT   = True -- ^ @>@
  isNano OpGEq  = True -- ^ @>=@
  isNano OpEq   = True -- ^ @==@
  isNano OpNEq  = True -- ^ @!=@
  
  isNano OpLAnd = True -- ^ @&&@
  isNano OpLOr  = True -- ^ @||@

  isNano OpSub  = True -- ^ @-@
  isNano OpAdd  = True -- ^ @+@
  isNano OpMul  = True -- ^ @*@
  isNano OpDiv  = True -- ^ @/@
  isNano OpMod  = True -- ^ @%@
  isNano _      = False

instance IsNano (LValue a) where 
  isNano (LVar _ _) = True
  isNano _          = False

instance IsNano (VarDecl a) where
  isNano (VarDecl _ _ (Just e)) = isNano e
  isNano (VarDecl _ _ Nothing)  = True

instance IsNano (Expression a) where 
  isNano (BoolLit _ _)         = True
  isNano (IntLit _ _)          = True
  isNano (VarRef _ _)          = True
  isNano (BracketRef _ e1 e2)  = isNano e1 && isNano e2 
  isNano (InfixExpr _ o e1 e2) = isNano o  && isNano e1 && isNano e2
  isNano (PrefixExpr _ o e)    = isNano o  && isNano e
  isNano (CallExpr _ e es)     = all isNano (e:es)
  isNano e                     = errortext (text "Not Nano Expression!" <+> pp e) 
  -- isNano _                     = False

instance IsNano AssignOp where
  isNano OpAssign = True
  isNano x        = errortext (text "Not Nano AssignOp!" <+> pp x) 
  -- isNano _        = False

instance IsNano PrefixOp where
  isNano PrefixLNot  = True
  isNano PrefixMinus = True 
  isNano e           = errortext (text "Not Nano PrefixOp!" <+> pp e) 
  -- isNano _           = False

instance IsNano (Statement a) where
  isNano (EmptyStmt _)          = True                   -- ^ skip
  isNano (ExprStmt _ e)         = isNanoExprStatement e  -- ^ x = e
  isNano (BlockStmt _ ss)       = isNano ss              -- ^ sequence
  isNano (IfSingleStmt _ b s)   = isNano b && isNano s   
  isNano (IfStmt _ b s1 s2)     = isNano b && isNano s1 && isNano s2
  isNano (WhileStmt _ b s)      = isNano b && isNano s
  isNano (VarDeclStmt _ ds)     = all isNano ds 
  isNano (ReturnStmt _ e)       = isNano e 
  isNano (FunctionStmt _ _ _ b) = isNano b
  isNano e                      = errortext (text "Not Nano Statement!" <+> pp e) 

instance IsNano a => IsNano (Maybe a) where 
  isNano (Just x) = isNano x
  isNano Nothing  = True

instance IsNano [(Statement a)] where 
  isNano = all isNano 


-- | Holds for `Expression` that is a valid side-effecting `Statement` 

isNanoExprStatement :: Expression a -> Bool
isNanoExprStatement (AssignExpr _ o lv e) = isNano o && isNano lv && isNano e 
isNanoExprStatement (CallExpr _ e es)     = all isNano (e:es)
isNanoExprStatement e                     = errortext (text "Not Nano ExprStmt!" <+> pp e) 
-- isNanoExprStatement _                     = False



-- | Trivial Syntax Checking 

checkTopStmt :: Statement SourceSpan -> Statement SourceSpan 
checkTopStmt f@(FunctionStmt _ _ _ b) 
  | checkBody b = f
checkTopStmt s  = errorstar $ errorInvalidTopStmt s

checkBody :: [Statement SourceSpan] -> Bool
checkBody stmts = all isNano stmts && null (getWhiles stmts) 
    
getWhiles :: [Statement SourceSpan] -> [Statement SourceSpan]
getWhiles stmts = everything (++) ([] `mkQ` fromWhile) stmts
  where 
    fromWhile s@(WhileStmt {}) = [s]
    fromWhile _                = [] 





-----------------------------------------------------------------------------------
-- | Helpers for extracting specifications from @ECMAScript3@ @Statement@ 
-----------------------------------------------------------------------------------

-- Ideally, a la JML, we'd modify the parser to take in annotations for 
-- 
--   * assert(p)
--   * assume(p)
--   * invariant(p) 
--
-- For now, we hack them with function calls.

mkId = Id (initialPos "") 

returnName :: String
returnName = "$result"

symbolId :: (IsLocated l, F.Symbolic x) => l -> x -> Id l
symbolId l x = Id l $ F.symbolString $ F.symbol x

returnId   :: a -> Id a
returnId x = Id x returnName 

returnSymbol :: F.Symbol
returnSymbol = F.stringSymbol returnName



isSpecification :: Statement a -> Bool
isSpecification s  = not $ null $ catMaybes $ ($ s) <$> specs 
  where 
    specs          = [getAssert, getAssume, getInv, getRequires, getEnsures]

getInvariant :: Statement a -> F.Pred 

getInvariant = getSpec getInv . flattenStmt

flattenStmt (BlockStmt _ ss) = concatMap flattenStmt ss
flattenStmt s                = [s]


getAssume    :: Statement a -> Maybe F.Pred 
getAssume    = getStatementPred "assume"

getAssert    :: Statement a -> Maybe F.Pred 
getAssert    = getStatementPred "assert"

getRequires  = getStatementPred "requires"
getEnsures   = getStatementPred "ensures"
getInv       = getStatementPred "invariant"

getStatementPred :: String -> Statement a -> Maybe F.Pred 
getStatementPred name (ExprStmt _ (CallExpr _ (VarRef _ (Id _ f)) [p]))
  | name == f 
  = Just $ F.prop p
getStatementPred _ _ 
  = Nothing 

getSpec   :: (Statement a -> Maybe F.Pred) -> [Statement a] -> F.Pred 
getSpec g = mconcat . catMaybes . map g

------------------------------------------------------------------
-- | Converting `ECMAScript3` values into `Fixpoint` values, 
--   i.e. *language* level entities into *logic* level entities.
------------------------------------------------------------------

instance F.Symbolic   (Id a) where
  symbol (Id _ x)   = F.symbol x 

instance F.Symbolic (LValue a) where
  symbol (LVar _ x) = F.symbol x
  symbol lv         = convertError "F.Symbol" lv

instance F.Expression (Id a) where
  expr = F.eVar

instance F.Expression (LValue a) where
  expr = F.eVar

instance F.Expression (Expression a) where
  expr (IntLit _ i)                 = F.expr i
  expr (VarRef _ x)                 = F.expr x
  expr (InfixExpr _ o e1 e2)        = F.EBin (bop o) (F.expr e1) (F.expr e2)
  expr (PrefixExpr _ PrefixMinus e) = F.EBin F.Minus (F.expr (0 :: Int)) (F.expr e)  
  expr e                            = convertError "F.Expr" e

instance F.Predicate  (Expression a) where 
  prop (BoolLit _ True)            = F.PTrue
  prop (BoolLit _ False)           = F.PFalse
  prop (PrefixExpr _ PrefixLNot e) = F.PNot (F.prop e)
  prop e@(InfixExpr _ _ _ _ )      = eProp e
  prop e                           = convertError "F.Pred" e  

convertError tgt e  = errortext $ msg <+> pp e
  where 
    msg             = text $ "Cannot convert to: " ++ tgt


------------------------------------------------------------------
eProp :: Expression a -> F.Pred
------------------------------------------------------------------

eProp (InfixExpr _ OpLT   e1 e2) = F.PAtom F.Lt (F.expr e1) (F.expr e2) 
eProp (InfixExpr _ OpLEq  e1 e2) = F.PAtom F.Le (F.expr e1) (F.expr e2) 
eProp (InfixExpr _ OpGT   e1 e2) = F.PAtom F.Gt (F.expr e1) (F.expr e2)  
eProp (InfixExpr _ OpGEq  e1 e2) = F.PAtom F.Ge (F.expr e1) (F.expr e2)  
eProp (InfixExpr _ OpEq   e1 e2) = F.PAtom F.Eq (F.expr e1) (F.expr e2) 
eProp (InfixExpr _ OpNEq  e1 e2) = F.PAtom F.Ne (F.expr e1) (F.expr e2) 
eProp (InfixExpr _ OpLAnd e1 e2) = pAnd (F.prop e1) (F.prop e2) 
eProp (InfixExpr _ OpLOr  e1 e2) = pOr  (F.prop e1) (F.prop e2)
eProp e                          = convertError "InfixExpr -> F.Prop" e

------------------------------------------------------------------
bop       :: InfixOp -> F.Bop
------------------------------------------------------------------

bop OpSub = F.Minus 
bop OpAdd = F.Plus
bop OpMul = F.Times
bop OpDiv = F.Div
bop OpMod = F.Mod
bop o     = convertError "F.Bop" o

------------------------------------------------------------------
pAnd p q  = F.pAnd [p, q] 
pOr  p q  = F.pOr  [p, q]

------------------------------------------------------------------
-- SourcePos Instances -------------------------------------------
------------------------------------------------------------------

instance Hashable SourcePos where 
  hashWithSalt i   = hashWithSalt i . sourcePosElts

instance Hashable SourceSpan where 
  hashWithSalt i z = hashWithSalt i (sp_begin z, sp_end z)

instance Hashable a => Hashable (Id a) where 
  hashWithSalt i x = hashWithSalt i (idLoc x, idName x)

idName (Id _ x) = x
idLoc  (Id l _) = l

-- instance PP SourcePos where 
--   pp = ppSourcePos 
-- 
-- instance F.Fixpoint SourcePos where
--   toFix = pp 

instance PP SourceSpan where 
  pp    = ppSourceSpan

instance F.Fixpoint SourceSpan where
  toFix = pp 


instance (Ord a, F.Fixpoint a) => PP (F.FixResult a) where
  pp = F.resultDoc
 
sourcePosElts s = (src, line, col)
  where 
    src         = sourceName   s 
    line        = sourceLine   s
    col         = sourceColumn s 

ppSourcePos src = parens 
                $ text ("file: " ++ f) <> comma <+> int l <> comma <+> int c
  where 
    (f,l,c)     = sourcePosElts src 

ppSourceSpan z  = parens 
                $ text (printf "file %s: (%d, %d) - (%d, %d)" f l c l' c')  
  where 
    (f,l ,c )   = sourcePosElts $ sp_begin z
    (_,l',c')   = sourcePosElts $ sp_end   z

instance PP F.Pred where 
  pp = pprint

instance PP F.Symbol where 
  pp = pprint

instance PP (Id a) where
  pp (Id _ x) = text x

instance PP a => PP (Located a) where
  pp x = pp (val x) <+> text "at:" <+> pp (loc x)
--------------------------------------------------------------------------------

dummySpan :: SourceSpan
dummySpan = Span l l 
  where l = initialPos ""

srcSpanStartLine = snd3 . sourcePosElts . sp_begin 
srcSpanEndLine   = snd3 . sourcePosElts . sp_end
srcSpanStartCol  = thd3 . sourcePosElts . sp_begin 
srcSpanEndCol    = thd3 . sourcePosElts . sp_end
srcSpanFile      = fst3 . sourcePosElts . sp_begin

