hets/GMP/GMPParser.hs

	GMPParser.hs revision 97aef8ef18cd9aa4bb30e95f4e8b49b0b82dea22
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder----------------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- the Generic Model Parser Abstract Syntax
3a6c7a7ff823616f56cd3d205fc44664a683effdChristian Maeder-- Copyright 2007, Lutz Schroeder and Georgel Calin
73dfcef93ee2ba07fedf4f3c74bace31853d1b9fChristian Maeder----------------------------------------------------------------
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu
2eeec5240b424984e3ee26296da1eeab6c6d739eChristian Maedermodule GMPParser where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport Text.ParserCombinators.Parsec
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Text.ParserCombinators.Parsec.Token as P
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskiimport Text.ParserCombinators.Parsec.Expr
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowskiimport Text.ParserCombinators.Parsec.Language
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport qualified Data.Set as Set
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederimport GMPAS
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder----------------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Modal Logic Class
85ebda7270c6883b503d3bde4757033c09c25644Christian Maeder----------------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederclass ModalLogic a where
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    parseIndex :: Parser a
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance ModalLogic () where        -- unit parsed Mindex
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz    parseIndex = return ()
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance ModalLogic Integer where   -- integer parsed Mindex
10b1417752a7cd79344892ad4dbb14831851c638Ewaryst Schulz    parseIndex = natural
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maederinstance ModalLogic Kars where
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder    parseIndex =  do l <- letter; Kars i <- parseIndex; return (Kars (l:i))
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder              <|> do return (Kars [])
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- to be changed so that it works on BitString ... :
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder{-parse i = do
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder    char '0'; BitString n <- parse(i+1); return(BitString(setBit n i)) ... or so-}
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maederinstance ModalLogic [Integer] where -- bit-string parsed Mindex
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder    parseIndex =  do try(char '0'); i <- parseIndex; return (0:i)
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder              <|> do try(char '1'); i <- parseIndex; return (1:i)
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder              <|> return []
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-----------------------------------------------------------
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder-- The Different Parsers for general Formula Type
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder-----------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederpar5er :: ModalLogic a => Parser (Formula a) -- main parser to parse the infix/primitive formulae
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederpar5er = do f <- prim; option (f) (inf f)
60bf7f52638962c93ec43da9aad8cafc9f09c318Christian Maeder      <?> "GMPParser.par5er"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederjunc :: Parser Junctor -- junctor parser
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maederjunc =  do try(string "/\\"); whiteSpace; return And
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski    <|> do try(string "\\/"); whiteSpace; return Or
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski    <|> do try(string "->");  whiteSpace; return If
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski    <|> do try(string "<->"); whiteSpace; return Iff
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski    <|> do try(string "<-");  whiteSpace; return Fi
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski    <?> "GMPParser.junc"
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskiinf :: ModalLogic a => (Formula a)-> Parser (Formula a)-- infix parser
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowskiinf f1 =
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski    do iot <- junc; f2 <-par5er; return $ Junctor f1 iot f2
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    <?> "GMPParser.inf"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederprim :: ModalLogic a => Parser (Formula a)  -- primitive parser
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederprim =
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder        do try(string "F"); whiteSpace; return F;
6abfd7000f15635fd29746bd841b4c36819e552bTill Mossakowski    <|> do try(string "T"); whiteSpace; return T;
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder    <|> do try(string "~"); whiteSpace; f <- par5er; return $ Neg f
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder    <|> do try(char '('); whiteSpace; f <- par5er; whiteSpace; char ')'; whiteSpace; return f
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    <|> do try(char '['); whiteSpace; i <- parseIndex; whiteSpace; char ']'; whiteSpace; f <-par5er; return $ Mapp (Mop i Square) f
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    <|> do try(char '<'); whiteSpace; i <- parseIndex; whiteSpace; char '>'; whiteSpace; f <-par5er; return $ Mapp (Mop i Angle) f
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    <?> "GMPParser.prim"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder----------------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- Run GMP parser & print
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder----------------------------------------------------------------
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederrunLex :: Show b => Parser b -> String -> IO ()
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian MaederrunLex p input = run (do
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder    whiteSpace
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder    ; x <- p
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder    ; eof
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder    ; return x
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder    ) input
1bc5dccbf0083a620ae1181c717fea75e4af5e5cChristian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederrun :: Show a => Parser a -> String -> IO ()
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maederrun p input
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder        = case (parse p "" input) of
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder                Left err -> do{ putStr "parse error at "
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder                                ; print err
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder                              }
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder                Right x -> print x
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder----------------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder-- The lexer
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder----------------------------------------------------------------
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconulexer            = P.makeTokenParser gmpDef
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconu
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconulexeme          = P.lexeme lexer
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconuparens          = P.parens lexer
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconubraces          = P.braces lexer
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela DiaconusemiSep         = P.semiSep lexer
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela DiaconusemiSep1        = P.semiSep1 lexer
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela DiaconucommaSep        = P.commaSep lexer
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela DiaconucommaSep1       = P.commaSep1 lexer
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till MossakowskiwhiteSpace      = P.whiteSpace lexer
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskisymbol          = P.symbol lexer
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskiidentifier      = P.identifier lexer
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskireserved        = P.reserved lexer
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowskinatural         = P.natural lexer
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till Mossakowski
0fe1b901cec27c06b8aad7548f56a7cab4dee6a4Till MossakowskigmpDef
b20cc520e698253354303b7bf3bc17f84240b213Klaus Luettich    = haskellStyle
04857331be117d4e2215d866c309a17bd9a7e15cLoredana Mihaela Diaconu    { identStart        = letter
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    , identLetter       = alphaNum <|> oneOf "_'" -- ???
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    , opStart           = opLetter gmpDef
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    , opLetter          = oneOf "\\-</~[]"
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    , reservedOpNames   = ["~","->","<-","<->","/\\","\\/","[]"]
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder    }
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder----------------------------------------------------------------
acabd9ab36e1870f6f02c513bcfbfd10ffd118e0Christian Maeder----------------------------------------------------------------
8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder