{-# OPTIONS -fglasgow-exts #-}

module LISS.Parser where

import LISS.Syntax

import UU.Parsing
import UU.Parsing.CharParser
import UU.Scanner hiding (pSpec)

import Data.Either
import System.Console.GetOpt
import System.Environment
import Data.Maybe (fromMaybe)


-- Parsing Utilities
paren x = pKey "(" *> x <* pKey ")"


-- Parsing
pIdentifier :: Parser Token String
pIdentifier = pVarid

pLiss :: Parser Token Liss
pLiss = Liss <$ pKey "program" <*> pIdentifier <*> pBody

pBody :: Parser Token Body
pBody = Body <$ pOCurly
                 <* pKey "declarations" <*> pDeclarations
                 <* pKey "statements" <*> pStatements <*
               pCCurly

pStatements = foldr1 SequenceS <$> (pList1Sep_ng (pKey ";") pStatement) <* pKey ";"

flatten = foldr (++) []

pDeclarations :: Parser Token Declarations
pDeclarations = flatten <$> (pListSep_ng (pKey ";") (pVarDec <|> pSubprogDec)) <* pKey ";"

pVarDec :: Parser Token [Declaration]
pVarDec = sem <$> (pListSep (pKey ",") pVar) <* pKey "->" <*> pType
 where
   sem l ty = map (\x -> VarDec $ Arg x ty) l

pSubprogDec :: Parser Token [Declaration]
pSubprogDec = (\a _ b c d (e,f) -> [SubprogDec a b c d e f]) <$>
     pSpecs <*> pKey "subProgram" <*> pIdentifier
   <* pOParen <*> pArgs <* pCParen
   <* pKey "->" <*> pType <*> pFBody

pSpecs :: Parser Token [Spec]
pSpecs = pListSep_ng (pKey ";") pSpec <* opt (pKey ";") []

pSpec :: Parser Token Spec
pSpec =
   Pre <$ pKey "pre" <*> pPredicate
 <|>
   Post <$ pKey "post" <*> pPredicate

pPredicate, pPredicateF :: Parser Token Predicate
pPredicateF =
   PBoolConst <$> pBool
 <|>
   PBoolVar <$> pVar
 <|>
   (\a b c -> f b a c) <$> pTerm <*> pOps ["==","!=","<",">","<=",">="] <*> pTerm
 <|>
   pParens pPredicate
 <|>
   PNegation <$ pKey "!" <*> pPredicate
 <|>
   PEmptySeq <$ pKey "emptySeq" <*> pSeqExp
 <|>
   PElemSet <$ pKey "elemSet" <*> pIntExp <*> pSetExp
 <|>
   PBoolFunction <$> pFName <* pOParen <*> pListSep (pKey ",") pVar <* pCParen
 <|>
   PIfThenElse
     <$ pKey "if" <* pOParen <*> pTerm <* pCParen
       <* pKey "then" <* pOCurly <*> pPredicate <* pCCurly
         <* pKey "else" <* pOCurly <*> pPredicate <* pCCurly
 <|>
   Forall <$ pKey "forall" <*> paren (pList1Sep (pKey ",") pArg) <* pKey ":" <*> pPredicate
 <|>
   Exists <$ pKey "exists" <*> paren (pList1Sep (pKey ",") pArg) <* pKey ":" <*> pPredicate
--  <|>
--    POld <$ pKey "old" <*> paren pPredicate
 <|>
   ValidIndex <$ pKey "valid_index" <* pKey "(" <*> pIdentifier <* pKey "," <*> pIntExp <* pKey ")"
 where
   f "==" = PEqual
   f "!=" = PDiff
   f "<"  = PLesser
   f ">"  = PGreater
   f ">=" = PGreatEq
   f "<=" = PLessEq

pPredicate = pChainl (f <$> pOps ["=>","<=>"])
            (pChainl (PDisj <$ pKey "||")
              (pChainl (PConj <$ pKey "&&") pPredicateF))
 where
   f "<=>" = PEquiv
   f "=>" = PImp

pTerm, pTermF :: Parser Token Term
pTermF =
   TIntConst <$> pInt
 <|>
   TIntVar <$> pVar
 <|>
   pParens pTerm
 <|>
   TArrayAccess <$> pVar <* pKey "[" <*> pTerm <* pKey "]"
 <|>
   THead <$ pKey "head" <*> pSeqExp
 <|>
   TIntFun <$> pFName <* pOParen <*> pListSep_ng (pKey ",") pVar <* pCParen
 <|>
   TOld <$ pKey "old" <*> paren pVar
--  <|>
--    TOldPos <$ pKey "old" <* pKey "(" <*> pVar <* pKey "[" <*> pTerm <* pKey "]" <* pKey ")"
 <|>
   Result <$ pKey "result"

pTerm =
   TNegative <$ pKey "-" <*> pTerm
 <|>
   pChainl (f <$> pOps ["+","-"])
     (pChainl (f <$> pOps ["*", "/"])
       (pChainl (f <$> pKey "%") pTermF))
 where
   f "+" = TSum
   f "-" = TSub
   f "*" = TMult
   f "/" = TDiv
   f "%" = TRem

pArgs = pListSep (pKey ",") pArg

pArg = Arg <$> pIdentifier <* pKey "->" <*> pType

pFBody = (\a b c -> (Body a b, c))
              <$ pOCurly
                   <* pKey "declarations" <*> pDeclarations
                   <* pKey "statements" <*> (opt pStatements Skip) <*> pReturnStat <*
                 pCCurly

pReturnStat =
   ReturnInt <$ pKey "return" <*> pIntExp <* pKey ";"
 <|>
   ReturnBool <$ pKey "return" <*> pBoolExp <* pKey ";"
 <|>
   ReturnSet <$ pKey "return" <*> pSetExp <* pKey ";"
 <|>
   ReturnSeq <$ pKey "return" <*> pSeqExp <* pKey ";"
 <|>
   ReturnArray <$ pKey "return" <*> pArrayExp <* pKey ";"

pVar :: Parser Token Var
pVar = pIdentifier

pType :: Parser Token Type
pType = const Integer <$> pKey "Integer"
 <|> const Boolean <$> pKey "Boolean"
 <|> const Sequence <$> pKey "Sequence"
 <|> const Set <$> pKey "Set"
 <|> Array <$ pKey "Array" <* pKey "[" <*> pInt <* pKey "]"

pStatement :: Parser Token Statement
pStatement =
{-      IntAssign <$> pVar <* pKey ":=" <*> pIntExp

 <|> SetAssign <$> pVar <* pKey ":=" <*> pSetExp

 <|> SeqAssign <$> pVar <* pKey ":=" <*> pSeqExp

 <|> BoolAssign <$> pVar <* pKey ":=" <*> pBoolExp
 -}
     (pVar <* pKey ":=") <**>
       (IntAssign <$$> pIntExp <* pCost 1
      <|> SetAssign <$$> pSetExp <* pCost 2
      <|> SeqAssign <$$> pSeqExp <* pCost 3
      <|> BoolAssign <$$> pBoolExp <* pCost 4) <* pCost 5

 <|> (ArrayPosAssign <$> pVar <* pKey "["  <*> pIntExp <* pKey "]" <* pKey ":=" <*> pIntExp) <* pCost 6

 <|> (IfThenElse
   <$ pKey "if" <* pOParen
     <*> pBoolExp <* pCParen
   <* pKey "then" <* pOCurly
     <*> pStatements <* pCCurly
   <*> opt ((\_ _ x _ -> x) <$> pKey "else" <*> pOCurly <*> pStatements <*> pCCurly) Skip) <* pCost 7

 <|> ((\a b c d -> While (a,b) c d) <$
       pKey "invariant" <*> pAssertion <* pKey ";" <*> opt (Just <$ pKey "variant" <*> pWfArg <* pKey ";") Nothing <*
         pKey "while" <* pOParen <*> pBoolExp <* pCParen <* pOCurly <*> pStatements <* pCCurly) <* pCost 8

 <|> (For <$
       pKey "for" <* pOParen
         <*> pVar <* pKey "in" <*> pIntExp <* pKey "to" <*> pIntExp <* pCParen
         <*> opt (pKey "step" *> pInt) 1
         <*> opt (id <$ pKey "satisfying" <* pOParen *> pBoolExp <* pCParen) (BoolConst True)
         <* pOCurly <*> pStatements <* pCCurly) <* pCost 9

 <|> (ForEach <$
       pKey "foreach" <* pOParen
         <*> pVar <* pKey "inSeq" <*> pSeqExp <* pCParen
         <*> opt (id <$ pKey "satisfying" <* pOParen *> pBoolExp <* pCParen) (BoolConst True)
         <* pOCurly <*> pStatements <* pCCurly) <* pCost 10

 <|> (Read <$ pKey "read" <*> pVar) <* pCost 11

 <|> (Write <$ pKey "write" <*> pIntExp) <* pCost 12

 <|> (WriteString <$ pKey "write" <*> pString) <* pCost 13

 <|> (Skip <$ pKey "skip") <* pCost 14

pAssertion :: Parser Token Assertion
pAssertion = pPredicate

pWfArg :: Parser Token WfArg
pWfArg = pTerm

pOps = pAny pKey

pInt :: Parser Token Int
pInt = (\x -> (read x :: Int)) <$> pInteger

pIntFactor :: Parser Token IntExp
pIntFactor =
   (IntConst <$> pInt) <* pCost 1
 <|>
   (IntVarExp <$> pVar) <* pCost 2
 <|>
   (Head <$ pKey "head" <*> pSeqExp) <* pCost 3
 <|>
   (pParens pIntExp) <* pCost 4
 <|>
   ((\a _ c _ -> ArrayAccess a c) <$> pIdentifier <*> pKey "[" <*> pIntExp <*> pKey "]") <* pCost 5
 <|>
   (IntFunction <$> pFName <* pOParen <*> pListSep_ng (pKey ",") pVar <* pCParen) <* pCost 6

pIntExp = Negative <$ pKey "-" <*> pIntExp
     <|> pChainl (semIntExp <$> pOps ["+","-"])
           (pChainl (semIntExp <$> pOps ["*", "/"])
             (pChainl (semIntExp <$> pKey "%") pIntFactor))
     <|> pIntFactor

semIntExp "+" = Sum
semIntExp "-" = Sub
semIntExp "*" = Mult
semIntExp "/" = Div
semIntExp "%" = Rem

pBool :: Parser Token Bool
pBool = (\x -> (read x :: Bool)) <$> (pKey "True" <|> pKey "False")

pBoolFactor :: Parser Token BoolExp
pBoolFactor =
           BoolConst <$> pBool
         <|>
           BoolVarExp <$> pVar
         <|>
           (\a b c -> semBoolIExp b a c) <$>
             pIntExp <*> pOps ["==","!=","<",">","<=",">="] <*> pIntExp
         <|>
           EmptySeq <$ pKey "emptySeq" <*> pSeqExp
         <|>
           ElemSet <$ pKey "elemSet" <*> pIntExp <*> pSetExp
         <|>
           pParens pBoolExp
         <|>
           Negation <$ pKey "!" <*> pBoolExp
         <|>
           BoolFunction <$> pFName <* pOParen <*> pListSep (pKey ",") pVar <* pCParen

pBoolExp :: Parser Token BoolExp
pBoolExp = pChainl (semBoolExp <$> pOps ["=>","<=>"])
            (pChainl (semBoolExp <$> pKey "||")
              (pChainl (semBoolExp <$> pKey "&&") pBoolFactor))


semBoolIExp "==" = Equal
semBoolIExp "!=" = Diff
semBoolIExp "<"  = Lesser
semBoolIExp ">"  = Greater
semBoolIExp ">=" = GreatEq
semBoolIExp "<=" = LessEq

semBoolExp "&&" = Conj
semBoolExp "||" = Disj
semBoolExp "<=>" = Equiv
semBoolExp "=>" = Imp

pSetExp =
   SetVarExp <$> pVar
 <|>
   SetConst <$ pKey "{" <*> pVar <* pKey "|" <*> pBoolExp <* pKey "}"
 <|>
   SetNull <$ pKey "{" <* pKey "}"
 <|>
   Union <$ pKey "union" <*> pSetExp <*> pSetExp
 <|>
   Intersect <$ pKey "intersect" <*> pSetExp <*> pSetExp
--  <|>
--    Add <$ pKey "add" <*> pIntExp <*> pSetExp
 <|>
   SetFunction <$> pFName <* pOParen <*> pListSep (pKey ",") pVar <* pCParen
 <|>
   pParens pSetExp


pSeqExp =
   SeqVarExp <$> pVar
 <|>
   SeqConst <$ pKey "[" <*> pList1Sep (pKey ",") pIntExp <* pKey "]"
 <|>
   SeqNull <$ pKey "[" <* pKey "]"
 <|>
   Tail <$ pKey "tail" <*> pSeqExp
 <|>
   Cons <$ pKey "cons" <*> pIntExp <*> pSeqExp
 <|>
   SeqFunction <$> pFName <* pOParen <*> pListSep (pKey ",") pVar <* pCParen
 <|>
   pParens pSeqExp


pArrayExp =
   ArrayVarExp <$> pVar
 <|>
   ArrayFunction <$> pFName <* pOParen <*> pListSep (pKey ",") pVar <* pCParen

pFName = pIdentifier

slScan name   = scanFile keywordsText keywordsOps specialChars opChars name

keywordsText  =  [ "program", "declarations", "statements", "subProgram",
                  "Integer", "Boolean", "Sequence", "Set", "Array",
                  "if", "then", "else", "True", "False",
                  "union", "intersect", "add", "while", "skip",
                  "emptySeq", "elemSeq", "elemSet", "head", "tail", "cons",
                  "for", "in", "inSeq", "satisfying", "to", "step", "foreach",
                  "subProgram", "return", "write", "read",
                  "pre", "post", "forall", "exists", "old", "base_addr",
                  "at", "valid_index", "valid_range", "block_length",
                  "result", "null", "fresh", "variant", "invariant"
                ]
keywordsOps   =  [ "=", "->", ":=", ":",
                  "&&", "||", "!", "=>", "<=>",
                  "==", "!=","<", ">","<=",">=",
                  "+","-","*", "/", "%"
                ]
specialChars  = "|();,[]{}.\""
opChars       = "!#$%&*+/<=>?@\\^|-:%"

compile name = do
 tokens <- slScan name
 res <- parseIO pLiss tokens
 putStrLn "Evaluates to:"
 putStrLn (show res)
 putStrLn "----------------------------------------------------"

parseFromFile = do
 putStr "Enter file to parse: "
 name <- getLine
 compile name

parseFromInput = do
 putStr "Enter text to parse: "
 text <- getLine
 let scanned = scan keywordsText keywordsOps specialChars opChars noPos text
 res <- parseIO pLiss scanned
 putStrLn "Evaluates to:"
 putStrLn (show res)
 putStrLn "----------------------------------------------------"

test s = do
 let scanned = scan keywordsText keywordsOps specialChars opChars noPos s
 res <- parseIO pLiss scanned
 putStrLn $ show res

mainParser = do
 a <- getArgs
 let h:_ = a
 compile h
