module Language.Haskell.FreeTheorems.Variations.PolySeq.Parser.ParseTerm(parseTerm, parseTermWithFlag) where

import Language.Haskell.FreeTheorems.Variations.PolySeq.Syntax

import Control.Monad.Identity
import Data.List ( nub )

import Text.Parsec
import Text.Parsec.Expr
import Text.Parsec.String(Parser)
import Text.Parsec.Combinator
import Text.Parsec.Token as P
import Text.Parsec.Language(emptyDef)
import Text.ParserCombinators.Parsec.Prim(getParserState)
import Language.Haskell.FreeTheorems.Variations.PolySeq.Debug

-- | ParseCont keeps track of all currently available term and type variable during parsing a term
data ParseCont = ParseCont { pcTVar :: [String], pcVar :: [String] } deriving (Show, Eq)

emptyParseCont = ParseCont [] []

-- * debug functions, are set to a function defined in Debug, (un)comment the definitions as necessary for debug

--trace1 = trace_toShell
trace1 = trace_ignore
--traceM = traceM_toShell
traceM = traceM_ignore
--traceM1 = traceM_toShell
traceM1 = traceM_ignore
--traceState = do state <- getParserState;
--                traceM ("with the Parser state " ++ show (stateInput state) ++ "\n");
traceState = return ()

-- * auxiliar functions
insertTVarPC (ParseCont tv v) str =
    if elem str tv
    then ParseCont tv v
    else ParseCont (str:tv) (filter (\x->x /= str) v)

checkOrInsertTVarState (ParseCont tv v) str =
    if elem str tv
    then return ()
    else modifyState (str:)

-- checkTVarPC (ParseCont tv v) str =
--     if elem str tv
--     then return ()
--     else parserZero <?> "unbound type variable"

insertVarPC (ParseCont tv v) str =
    if elem str v
    then ParseCont tv v
    else ParseCont (filter (\x->x /= str) tv) (str:v)

checkVarPC (ParseCont tv v) str =
    if elem str v
    then return ()
    else parserZero <?> "unbound term variable"

myLanguage = 
    emptyDef
    { identStart      = letter
    , identLetter     = alphaNum <|> oneOf "'"
    , opStart         = oneOf ":\\-+="
    , opLetter        = oneOf ":\\->+=_"
    , reservedOpNames = [":","::","=","->","\\","/\\","_","+"]
    , reservedNames   = ["forall","Int", "Bool", "if", "then", "else", "True", "False", "case","of","let!","in","fix","let","seq","undefined"]
    , caseSensitive   = True
    }

lexer = P.makeTokenParser myLanguage

int      = P.integer    lexer
res      = P.reserved   lexer
resOp    = P.reservedOp lexer
whiteSpc = P.whiteSpace lexer
lexe     = P.lexeme     lexer
par      = P.parens     lexer
brack    = P.brackets   lexer
symb     = P.symbol     lexer
ident    = P.identifier lexer
brace    = P.braces     lexer
nat      = P.natural    lexer


type MyState = [String]


termParser :: ParseCont -> ParsecT String MyState Identity Term
termParser pc = do
  whiteSpc
  x <- (term1 pc)
  eof
  return x

term1 :: ParseCont -> ParsecT String MyState Identity Term
term1 pc = do
    do{ traceM "Enter term1\n";
        traceState;
         do{ resOp "\\";
	     str <- ident;
	     resOp "::";
	     tau <- typ pc;
	     symb ".";
	     t   <- term1 (insertVarPC pc str);
	     return (Abs (TermVar str) tau t)
	   }
     <|> do{ resOp "/\\";
	     str <- ident;
	     symb ".";
	     traceM1 ("scanned /\\ " ++ str ++ ".\n");
	     t <- (term1 (insertTVarPC pc str));
	     return (TAbs (TypVar str) t)
	   }
     <|> do{ res "case";
	     t <- (term1 pc);
	     res "of";
	     symb "{";
	     (do{ symb "[";
		  symb "]";
		  resOp "->";
		  t1 <- (term1 pc);
		  resOp ";";
		  v1 <- ident;
		  resOp ":";
		  v2 <- ident;
		  resOp "->";
		  t2 <- term1 (insertVarPC (insertVarPC pc v1) v2);
		  symb "}";
		  return (LCase t t1 (TermVar v1) (TermVar v2) t2)
		}
	      <|> do{ res "True";
		      resOp "->";
		      t1 <- term1 pc;
		      resOp ";";
		      res "False";
		      resOp "->";
		      t2 <- term1 pc;
		      symb "}";
		      return (BCase t t1 t2)
		    }
	      <|> do{ res "False";
		      resOp "->";
		      t1 <- term1 pc;
		      resOp ";";
		      res "True";
		      resOp "->";
		      t2 <- term1 pc;
		      symb "}";
		      return (BCase t t2 t1)
		    })
	   }
    <|> ifParser pc
    <|> do{ res "let!";
	    v <- ident;
	    let pc' = insertVarPC pc v in
	    do{ resOp "=";
		t <- (term1 pc');
		res "in";
		t' <- (term1 pc');
		return (LSeq (TermVar v) t t')
	      }
	  }
    <|> do{ res "let";
	    v <- ident;
	    let pc' = insertVarPC pc v in
	    do{ resOp "=";
		t <- (term1 pc');
		res "in";
		t' <- (term1 pc');
		return (Let (TermVar v) t t')
	      }
	  }
    <|> term2 pc
      }

ifParser :: ParseCont -> ParsecT String MyState Identity Term
ifParser pc = do
  res "if"
  t <- term1 pc
  res "then"
  t1 <- term1 pc
  res "else"
  t2 <- term1 pc
  return (BCase t t1 t2)

term2 :: ParseCont -> ParsecT String MyState Identity Term
term2 pc =
    do{ traceM "Enter term2\n";
        traceState;
        l <- sepBy1 (term3 pc) (resOp ":");
        traceState;
        trace1 "returned from term2" 
        return (foldr1 (\x y -> Cons x y) l)
      }

term3 :: ParseCont -> ParsecT String MyState Identity Term
term3 pc = do{traceM "Enter term3\n";
	      traceState;
	      h <- (do{ i<-int; 
			return (I (fromInteger i))
		      } 
	            <|> term4 pc);
	      l <- (do{ resOp "+";
			sepBy (term4 pc) (resOp "+")
		      }
		    <|> return []);
	      trace1 "returned from term3" 
              return (foldl1 (\x y -> Add x y) (h:l))
	     }

term4 :: ParseCont -> ParsecT String MyState Identity Term
term4 pc =
    do{ traceM "Enter term4\n";
	traceState;
     do{ t <- (term6 pc);
	 traceM ("term4 scanned term6: " ++ show t ++ "\n");
         args <- many (term5 pc);
	 traceM ("term4 with args = " ++ show (length args) ++ "\n");
	 traceM ("where the arguments are " ++ show (map ($(Var (TermVar "fake"))) args) ++ "\n");
         let t' = ((foldl (.) id (reverse args))$t) in
	 do{ traceM ("term4 is " ++ show t' ++ "\n");
	     return t'
	   }
       }
      }

term5 pc =
    do{traceM "Enter term5\n";
       traceState;
       do{ t' <- term7 pc;
	traceM ("returned in term5 with " ++ show t' ++ "\n");
        state <- getParserState;
	traceM ("with the Parser state " ++ show (stateInput state) ++ "\n");
        return (\t -> App t t')
	 }
      }

term6 pc =
    do{ traceM "Enter term6\n";
	traceState;
	do{ res "fix";
	    t <- (term7 pc) <?> "the previous \"fix\" to be applied to an argument";
	    return (Fix t)
	  }
	<|> do{ res "seq";
		t <- (term7 pc) <?> "the previous \"seq\" to be applied to two arguments";
		t'<- (term7 pc) <?> "the previous \"seq\" to be applied to two arguments";
		return (Seq t t')
	      }
	<|> term7 pc
      }
	    

term7 pc =
    do{ traceM "Enter term7\n";
	traceState;
	t <- term8 pc;
	do{ resOp "_";
	    tau <- brace (typ pc);
	    return (TApp t tau)
	  }
	<|> return t
      }
    
term8 pc =
    do{ traceM "Enter term8\n";
	traceState;
	par (term1 pc)
     <|> do{ tl <- brack (sepBy (term1 pc) (symb ","));
	     trace1 "scanned [t1, ..., tn], trying : ...\n" resOp "_";
	     tau <- trace1 "scanned :, trying typ\n" (brace (typ pc));
	     return (foldr (\x y -> Cons x y) (Nil tau) tl)
	   } 
     <|> do{ i <- (lexe nat);
	     return (I (fromInteger i))
	   }
     <|> do{ str <- ident;
	     traceM ("term8: identified " ++ str ++ "\n");
	     checkVarPC pc str;
	     traceM ("term8: Variable, checkVarPC successful\n");
	     return (Var (TermVar str))
	   }
    <|> do{ res "True";
	    return T
	  }
    <|> do{ res "False";
	    return F;
	  }
    <|> do{ res "undefined";
	    resOp "_" <?> "undefined has to be instantiated to a type.";
	    tau <- brace (typ pc);
	    return (Fix (Abs (TermVar "x") tau (Var (TermVar "x"))))
	  } 
    <|> do{ res "fix";
	    parserZero <?> "the previous \"fix\" to be immediately applied to a term and not to be the argument to a function"
	  }
    <|> do{ res "seq";
	    parserZero <?> "the previous \"seq\" to be immediately applied to two terms and not to be the argument to a function"
	  }
      }

typ :: ParseCont -> ParsecT String MyState Identity Typ
typ pc = buildExpressionParser tableTyp (typ1 pc)

tableTyp = [ [op "->" (\x y -> TArrow Non x y) AssocRight] ]
 where op s f assoc = Infix (do{ resOp s; return f} <?> "operator") assoc

typ1 :: ParseCont -> ParsecT String MyState Identity Typ
typ1 pc = 
        do{
        traceM "Enter typ1\n";
	traceState;
        par (typ pc)
    <|> do{ symb "[";
	    tau <- (typ pc);
	    symb "]";
	    return (TList tau)
	  }
    <|> do{ str <- ident;
	    traceM ("identifier TypeVariable " ++ str);
	    checkOrInsertTVarState pc str;
	    traceM "checked TVar identifier.";
	    return (TVar (TypVar str))
	  }
    <|> do{ res "Int";
	    return TInt
	  }
    <|> do{ res "forall";
	    str <- ident;
	    resOp ".";
	    tau <- (typ (insertTVarPC pc str));
	    return (TAll Non (TypVar str) tau)
	  }
    <|> do{ res "Bool";
	    return TBool
	  }
      }

cTermParser = termParser emptyParseCont
testParser = termParser (ParseCont ["a","b"] ["f","g"])

addFreeTVar :: [String] -> Term -> Term
addFreeTVar [] t = t
addFreeTVar (x:xs) t = addFreeTVar xs (TAbs (TypVar x) t)

addTVarParser :: ParseCont -> ParsecT String MyState Identity Term 
addTVarParser pc = do
  res <- termParser pc
  tvars <- getState
  return (addFreeTVar (nub tvars) res)

parseTerm :: String -> Either ParseError Term
parseTerm = runP (addTVarParser emptyParseCont) [] "user input term"

-- the additional Bool is a flag to see if type abstraction is explicit (Bool = True)

addTVarParserWithFlag :: ParseCont -> ParsecT String MyState Identity (Term,Bool) 
addTVarParserWithFlag pc = do
  res <- termParser pc
  tvars <- getState
  return (if tvars == [] then (res, True) else (addFreeTVar (nub tvars) res, False))

parseTermWithFlag :: String -> Either ParseError (Term,Bool)
parseTermWithFlag = runP (addTVarParserWithFlag emptyParseCont) [] "user input term"