abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-------------------------------------------------------------------------------

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- the Generic Model Parser Abstract Syntax

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder-- Copyright 2007, Lutz Schroeder and Georgel Calin

75a6279dbae159d018ef812185416cf6df386c10Till Mossakowski-------------------------------------------------------------------------------

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maedermodule GMPParser where

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maederimport Text.ParserCombinators.Parsec

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport Lexer

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder--import ModalLogic

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maederimport GMPAS

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-------------------------------------------------------------------------------

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder-- Parser for polymorphic (Formula a) Type

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder-------------------------------------------------------------------------------

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederpar5er :: Parser a -> Parser (Formula a) -- main parser

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederpar5er pa = do f <- prim pa; option (f) (inf pa f)

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder <?> "GMPParser.par5er"

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maeder

0df692ce8b9293499b2e1768458613a63e7b5cd0Christian Maederjunc :: Parser Junctor -- junctor parser

da245da15da78363c896e44ea97a14ab1f83eb50Christian Maederjunc = do try(string "/\\"); whiteSpace; return And

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder <|> do try(string "\\/"); whiteSpace; return Or

e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder <|> do try(string "->"); whiteSpace; return If

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder <|> do try(string "<->"); whiteSpace; return Iff

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder <|> do try(string "<-"); whiteSpace; return Fi

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder <?> "GMPParser.junc"

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maeder

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maederinf :: Parser a -> (Formula a)-> Parser (Formula a) -- infix parser

3c5cc698b0c061209ff83eb8de027daef5ae922aChristian Maederinf pa f1 =

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder do iot <- junc; f2 <-par5er pa; return $ Junctor f1 iot f2

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder <?> "GMPParser.inf"

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederprim :: Parser a -> Parser (Formula a) -- primitive parser

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maederprim pa =

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder do try(string "F")

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder ;whiteSpace

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder ;return F

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder <|> do try(string "T")

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;whiteSpace

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;return T

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder <|> do try(string "~")

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;whiteSpace

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;f <- par5er pa

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder ;return $ Neg f

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder <|> do try(char '(')

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;whiteSpace

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;f <- par5er pa

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;whiteSpace

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;char ')'

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;whiteSpace

0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder ;return f

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder <|> do try(char '[')

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;whiteSpace

c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder ;i <- pa

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ;whiteSpace

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder ;char ']'

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder ;whiteSpace

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;f <-par5er pa

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder ;return $ Mapp (Mop i Square) f

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder <|> do try(char '<')

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder ;whiteSpace

48c4688439e0aade4faeebf25ca8b16d661e47afChristian Maeder ;i <- pa

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ;whiteSpace

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder ;char '>'

c4e912fc181d72c8d0e0e38d0351278182f0d0b5Christian Maeder ;whiteSpace

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder ;f <- par5er pa

d703a61b7fa9f85d92ac8f768d7c290b7c0a41c5Christian Maeder ;return $ Neg (Mapp (Mop i Square) (Neg f)) -- Mapp (Mop i Angle) f

abd8dd44106c507dd2cb64359b63d7d56fa0a9c8Christian Maeder <?> "GMPParser.prim"

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder-------------------------------------------------------------------------------

024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder-------------------------------------------------------------------------------

2dfc7b04f2db681992ca04175f2beb0f127c9844Christian Maeder