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
data ParseCont = ParseCont { pcTVar :: [String], pcVar :: [String] } deriving (Show, Eq)
emptyParseCont = ParseCont [] []
trace1 = trace_ignore
traceM = traceM_ignore
traceM1 = traceM_ignore
traceState = return ()
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:)
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"
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"