d53747c386354ff7db8629dfdf20f44a7c4d715dEugen KuksaDescription : Parser of common logic interchange format
cacbb5e3100fb85d23d1614cace3a8662801f2e6Eugen KuksaCopyright : (c) Karl Luc, DFKI Bremen 2010, Eugen Kuksa and Uni Bremen 2011
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
cacbb5e3100fb85d23d1614cace3a8662801f2e6Eugen KuksaMaintainer : eugenk@informatik.uni-bremen.de
b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian MaederStability : provisional
6d81916b9004f8d9b6032113c5987ab07da47015Karl LucPortability : portable
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen KuksaParser of common logic interchange format
6498fe9ab2cd00e3b52109c76faa2fac1849ddaaChristian Maeder-- Ref. Common Logic ISO/IEC IS 24707:2007(E)
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucimport qualified Common.AnnoState as AnnoState
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Lucimport qualified Common.AS_Annotation as Annotation
a18c1e9cec48e0a33df38b9bf6f5421af684f054Eugen Kuksaimport Common.Lexer as Lexer hiding (oParenT, cParenT, pToken, parens)
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksaimport Common.Keywords (colonS, mapsTo)
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulzeimport Common.GlobalAnnotations (PrefixMap)
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaimport Data.Either (lefts, rights)
b3138d7e20d2d6dd26a325b844a8b21b0ecbb602Eugen Kuksaimport qualified Data.Set as Set
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulzeimport qualified Data.Map as Map
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksaimport qualified CommonLogic.Tools as Tools
b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederimport Text.ParserCombinators.Parsec as Parsec
1ea7fb6b0f66210bc0d3cb995f1b655277b33884Eugen Kuksa-- | parser for getText
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulzecltext :: PrefixMap -> CharParser st TEXT_META
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulzecltext pm = many white >> (do
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa try $ oParenT >> clTextKey
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa (nt, prfxs) <- namedtext
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa return $ tm nt prfxs
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa (t, prfxs) <- text <?> "text"
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa return $ tm t prfxs
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa where tm :: TEXT -> [PrefixMapping] -> TEXT_META
eea1dfbc731d45f624bc3c14bada0617ebaa6eaaEugen Kuksa tm t prfxs = emptyTextMeta { AS.getText = t
c3cfa8f613684439642d59fd89c6bae83cdbf6f0Soeren D. Schulze , prefix_map = Map.toList pm ++ prfxs
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksanamedtext :: CharParser st (TEXT, [PrefixMapping])
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksanamedtext = do
8b7e9bd07700b2fef4312835be342250347ad849Eugen Kuksa n <- identifier <?> "name after \"cl-text\""
6498fe9ab2cd00e3b52109c76faa2fac1849ddaaChristian Maeder (t, prfxs) <- option (Text [] nullRange, []) text
0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa return (Named_text n t nullRange, prfxs)
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksatext :: CharParser st (TEXT, [PrefixMapping])
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa phrPrfxs <- many1 phrase
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa let (phr, prfxs) = unzip phrPrfxs
0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa return (Text (concat phr) nullRange, concat prfxs)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- remove the try
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederkeys set here to prevent try in more complex parser to get the right
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedererror message in ex. the following text -}
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksaphrase :: CharParser st ([PHRASE], [PrefixMapping])
64401a16f05d2b42fa52301ec3ce01569e2a8e19Eugen Kuksaphrase = many white >> (do
d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksa try (oParenT >> clModuleKey)
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa (m, prfxs) <- pModule
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa return ([Module m], prfxs)
d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksa try (oParenT >> clImportsKey)
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc i <- importation
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa return ([Importation i], [])
d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksa try (oParenT >> clCommentKey)
ae371d21b7a25f2ad233db70049f0b6f2edcf411Soeren D. Schulze c <- (quotedstring <|> enclosedname) <?> "comment after \"cl-comment\""
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa (t, prfxs) <- comment_txt <?> "text after \"cl-comment <comment>\""
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa return ([Comment_text (Comment c nullRange) t nullRange], prfxs)
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa try (oParenT >> clPrefixKey)
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksa pm <- prefix
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksa return ([], pm)
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa s <- sentence <?> "sentence"
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa return ([Sentence s], [])
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksaprefix :: CharParser st [PrefixMapping]
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksa string colonS
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksa return colonS
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksa string colonS
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksa return $ x ++ colonS
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksa i <- iriCurie
fe656923fef897857a32d6de89a3196571ca2427Eugen Kuksa return [(p, i)]
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksacomment_txt :: CharParser st (TEXT, [PrefixMapping])
0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksacomment_txt = try text <|> return (Text [] nullRange, [])
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc-- | parser for module
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen KuksapModule :: CharParser st (MODULE, [PrefixMapping])
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl LucpModule = do
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa t <- identifier <?> "module name after \"cl-module\""
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (exs, (txt, prfxs)) <- pModExcl <?> "text in module"
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa [] -> return (Mod t txt nullRange, prfxs)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> return (Mod_ex t exs txt nullRange, prfxs)
18741eef977546e24fce1fde1b8a8f817aedc6d0Christian Maeder-- | parser for
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen KuksapModExcl :: CharParser st ([NAME], (TEXT, [PrefixMapping]))
64401a16f05d2b42fa52301ec3ce01569e2a8e19Eugen KuksapModExcl = many white >> (do
d1e1be2881bf54b507313a6a2b4a254090cd92b7Eugen Kuksa try (oParenT >> clExcludesKey)
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa exs <- many identifier <?> "only names in module-exclusion list"
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa return (exs, tp)
123c74ceb5c4d3f364323a015ecef3eaf0ab67d5Eugen Kuksa return ([], tp)
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucimportation :: CharParser st IMPORTATION
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Lucimportation = do
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc -- clImportsKey
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa n <- identifier <?> "importation name after \"cl-imports\""
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc return $ Imp_name n
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc-- | parser for sentences
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksasentence :: CharParser st SENTENCE
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksasentence = parens (do
8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa ck <- try clCommentKey
ae371d21b7a25f2ad233db70049f0b6f2edcf411Soeren D. Schulze c <- (quotedstring <|> enclosedname) <?> "comment after \"cl-comment\""
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa s <- sentence <?> "sentence after \"cl-comment <comment>\""
8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa return $ Comment_sent (Comment c $ Range $ rangeSpan c) s
8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa $ Range $ joinRanges [rangeSpan ck, rangeSpan c, rangeSpan s]
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa t0 <- try rolesetTerm
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa nts <- many rolesetNT
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa return $ rolesetSentence t0 nts
8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksa return $ Atom_sent at $ Range $ rangeSpan at
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc c <- andKey
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc s <- many sentence -- joinRanges with s = []?
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze return $ Bool_sent (Junction Conjunction s)
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze $ Range $ joinRanges [rangeSpan c, rangeSpan s]
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc s <- many sentence
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze return $ Bool_sent (Junction Disjunction s)
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze $ Range $ joinRanges [rangeSpan c, rangeSpan s]
fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc c <- notKey
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa s <- sentence <?> "sentence after \"not\""
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc return $ Bool_sent (Negation s) $ Range $ joinRanges [rangeSpan c,
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc rangeSpan s]
cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa c <- try iffKey
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa s1 <- sentence <?> "sentence after \"iff\""
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa s2 <- sentence <?> "second sentence after \"iff\""
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze return $ Bool_sent (BinOp Biconditional s1 s2)
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze $ Range $ joinRanges [rangeSpan c, rangeSpan s1, rangeSpan s1]
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa s1 <- sentence <?> "sentence after \"if\""
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa s2 <- sentence <?> "second sentence after \"if\""
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze return $ Bool_sent (BinOp Implication s1 s2)
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze $ Range $ joinRanges [rangeSpan c, rangeSpan s1, rangeSpan s1]
fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc c <- forallKey
dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksa quantsent1 True c
fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc c <- existsKey
dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksa quantsent1 False c
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaquantsent1 :: Bool -> Token -> CharParser st SENTENCE
dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksaquantsent1 t c = do
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa g <- identifier <?> "predicate after quantifier"
dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksa quantsent2 t c $ Just g -- Quant_sent using syntactic sugar
dabf0263008e0b55440c4e3fa0b61261af8c28ceEugen Kuksa quantsent2 t c Nothing -- normal Quant_sent
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaquantsent2 :: Bool -> Token -> Maybe NAME -> CharParser st SENTENCE
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaquantsent2 t c mg = do
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa bl <- parens boundlist
fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc s <- sentence
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa return $ quantsent3 t mg (rights bl) (lefts bl) s
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa $ Range $ joinRanges [rangeSpan c, rangeSpan s]
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaquantsent3 :: Bool -> Maybe NAME -> [NAME_OR_SEQMARK]
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa -> [(NAME_OR_SEQMARK, TERM)] -> SENTENCE -> Range -> SENTENCE
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederquantsent3 t mg bs ((n, trm) : nts) s rn = -- Quant_sent using syntactic sugar
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa let functerm = case n of
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa Name nm -> Atom (Funct_term trm [Term_seq $ Name_term nm] nullRange) []
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa SeqMark sqm -> Atom (Funct_term trm [Seq_marks sqm] nullRange) []
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze then Quant_sent Universal [n] (quantsent3 t mg bs nts (
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze Bool_sent (BinOp Implication (Atom_sent functerm rn) s) rn
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze else Quant_sent Universal [n] (quantsent3 t mg bs nts (
d2d5606ab65ddf48599bd044416de07a205095f2Soeren D. Schulze Bool_sent (Junction Conjunction [Atom_sent functerm rn, s]) rn
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaquantsent3 t mg bs [] s rn =
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze let quantType = if t then Universal else Existential
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa in case mg of
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze Nothing -> Quant_sent quantType bs s rn -- normal Quant_sent
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa Just g -> -- Quant_sent using syntactic sugar
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa let functerm = Atom (Funct_term (Name_term g) (map (Term_seq . Name_term)
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze then Quant_sent Universal bs (Bool_sent (BinOp Implication
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze (Atom_sent functerm nullRange) s) rn) rn
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze Quant_sent Existential bs (Bool_sent (Junction Conjunction
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze [Atom_sent functerm nullRange, s]) rn) rn
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksaboundlist :: CharParser st [Either (NAME_OR_SEQMARK, TERM) NAME_OR_SEQMARK]
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksaboundlist = many (do
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa nos <- intNameOrSeqMark
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa return $ Right nos
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa <|> parens (do
ff41d94839a36ce86291af5d83abe2bd39cce1d0Eugen Kuksa nos <- intNameOrSeqMark
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return $ Left (nos, t)
b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederatom :: CharParser st ATOM
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa t1 <- term <?> "term after \"=\""
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa t2 <- term <?> "second term after \"=\""
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc return $ Equation t1 t2
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa t <- term <?> "term"
d53747c386354ff7db8629dfdf20f44a7c4d715dEugen Kuksa ts <- many termseq
fe1d1e27d7199f3ae7be6406d0ab01b29afbacb0Karl Luc return $ Atom t ts
b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maederterm :: CharParser st TERM
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc t <- identifier
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc return $ Name_term t
0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa <|> term_fun_cmt
8b42604fc9e948093bde658f32b8446e9c6a3576Eugen Kuksaterm_fun_cmt :: CharParser st TERM
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksaterm_fun_cmt = parens (do
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa ck <- try clCommentKey
ae371d21b7a25f2ad233db70049f0b6f2edcf411Soeren D. Schulze c <- (quotedstring <|> enclosedname) <?> "comment after \"cl-comment\""
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa t <- term <?> "term after \"cl-comment <comment>\""
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa return $ Comment_term t (Comment c $ Range $ rangeSpan c)
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa $ Range $ joinRanges [rangeSpan ck, rangeSpan c, rangeSpan t]
f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze c <- try thatKey
f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze return $ That_term s $ Range $ joinRanges [rangeSpan c, rangeSpan s]
f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze t <- liftM Name_term $ pToken quotedstring
f03aa0b723e5545fddf7019e287368b9e208ca69Soeren D. Schulze return $ Funct_term t [] $ Range $ rangeSpan t
089b97b94738ce3d75ceb1c6466b4ba916ca4a4fSoeren D. Schulze ts <- many termseq
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa return $ Funct_term t ts $ Range $ joinRanges [rangeSpan t, rangeSpan ts]
b062631d2f72f0b2b2b6140bc5b0fccb66d1802bChristian Maedertermseq :: CharParser st TERM_SEQ
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luctermseq = do
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa x <- seqmark
0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa return $ Seq_marks x
b696e806e85f1c07f2f5ea07f2b5babcd656e0d6Karl Luc return $ Term_seq t
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa <?> "term or sequence marker in term sequence"
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetTerm :: CharParser st TERM
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetTerm = do
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa clRolesetKey
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetNT :: CharParser st (NAME, TERM)
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetNT = parens $ do
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa n <- identifier
befbd45c1a4c171f2194b59016590b02bf4df750Eugen Kuksa t <- term <?> "term"
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetSentence :: TERM -> [(NAME, TERM)] -> SENTENCE
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetSentence t0 nts =
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa let x = rolesetFreeName t0 nts
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in Quant_sent Existential [Name x] (Bool_sent (Junction Conjunction $
0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa rolesetAddToTerm x t0 : map (rolesetMixTerm x) nts
ea570f40967ef8bc16b76c54f9b867a8036cc750Soeren D. Schulze ) nullRange) $ Range $ rangeSpan t0
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetFreeName :: TERM -> [(NAME, TERM)] -> NAME
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetFreeName trm nts =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (\ (n, t) -> Set.union (Tools.indvC_term t)
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa in fst $ Tools.freeName ("x", 0) usedNames
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetAddToTerm :: NAME -> TERM -> SENTENCE
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetAddToTerm x trm = Atom_sent (Atom trm [Term_seq $ Name_term x]) nullRange
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen KuksarolesetMixTerm :: NAME -> (NAME, TERM) -> SENTENCE
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederrolesetMixTerm x (n, t) =
d5c6ddb570942f686319dcaf6c4b513a033e00ceEugen Kuksa Atom_sent (Atom (Name_term n) [Term_seq $ Name_term x, Term_seq t]) nullRange
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaedersymbIdentifier :: CharParser st Token
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaedersymbIdentifier =
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaeder pToken (reserved (reservedelement ++ casl_reserved_words) scanClSymbol)
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaeder <?> "symbol"
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaederscanClSymbol :: CharParser st String
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaederscanClSymbol = quotedstring <|> enclosedname <|>
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaeder (satisfy (\ c -> clLetters c && notElem c "%{}[],;=")
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaeder <:> many clLetter <?> "words")
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaintNameOrSeqMark :: CharParser st NAME_OR_SEQMARK
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaintNameOrSeqMark = do
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa s <- seqmark -- fix seqmark parser for one
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa return $ SeqMark s
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaeder n <- symbIdentifier
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa return $ Name n
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa-- | Parse a list of comma separated symbols.
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbItems :: GenParser Char st SYMB_ITEMS
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbItems = do
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa (is, ps) <- symbs
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa return (Symb_items is $ catRange ps)
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa-- | parse a comma separated list of symbols
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksasymbs :: GenParser Char st ([NAME_OR_SEQMARK], [Token])
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa s <- intNameOrSeqMark
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do c <- commaT `followedWith` intNameOrSeqMark
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (is, ps) <- symbs
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (s : is, c : ps)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder <|> return ([s], [])
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa-- | parse a list of symbol mappings
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMapItems :: GenParser Char st SYMB_MAP_ITEMS
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMapItems = do
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa (is, ps) <- symbMaps
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa return (Symb_map_items is $ catRange ps)
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa-- | parse a comma separated list of symbol mappings
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMaps :: GenParser Char st ([SYMB_OR_MAP], [Token])
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMaps = do
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa s <- symbMap
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do c <- commaT `followedWith` intNameOrSeqMark
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (is, ps) <- symbMaps
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (s : is, c : ps)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder <|> return ([s], [])
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa-- | parsing one symbol or a mapping of one to a second symbol
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMap :: GenParser Char st SYMB_OR_MAP
7b2c06587c0e51d5f75e5fc856d164ee92f4ed78Eugen KuksasymbMap = symbMapS <|> symbMapN
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMapS :: GenParser Char st SYMB_OR_MAP
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMapS = do
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa s <- seqmark
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do f <- pToken $ toKey mapsTo
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (Symb_mapS s t $ tokPos f)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder <|> return (Symb $ SeqMark s)
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMapN :: GenParser Char st SYMB_OR_MAP
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksasymbMapN = do
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaeder s <- symbIdentifier
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder do f <- pToken $ toKey mapsTo
ba7f2ee11dafeea528830f6a5f9c98eac1f7eca5cmaeder t <- symbIdentifier
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return (Symb_mapN s t $ tokPos f)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder <|> return (Symb $ Name s)
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc-- | Toplevel parser for basic specs
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzebasicSpec :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzebasicSpec pm = parseAxItems pm
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze bi <- AnnoState.allAnnoParser $ parseBasicItems pm
0c4da1aef47757166486f7aa0b037ffa30b840cdEugen Kuksa return $ Basic_spec [bi]
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- function to parse different syntaxes
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederparsing: axiom items with dots, clif sentences, clif text
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederfirst getting only the sentences -}
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseBasicItems :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseBasicItems pm = try (parseSentences pm)
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze <|> parseClText pm
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc -- parseClText
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseSentences :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseSentences pm = do
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze xs <- many1 $ aFormula pm
823ce7a568b0f653ebe83af7ab6ac9ec70f2cf8eKarl Luc return $ Axiom_items xs
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseClText :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseClText pm = do
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze tx <- cltext pm
cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen Kuksa return $ Axiom_items (textToAn [tx])
cba0aeea95db26960d4d2e5a1dd571f17a5b7ae4Eugen KuksatextToAn :: [TEXT_META] -> [Annotation.Annoted TEXT_META]
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc-- | parser for Axiom_items
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseAxItems :: PrefixMap -> AnnoState.AParser st BASIC_SPEC
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseAxItems pm = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (fs, ds) <- AnnoState.allAnnoParser (parseAx pm) `Lexer.separatedBy`
07f731e693fe433a238b5cc0aab6c5c99c1da798Karl Luc let _ = Id.catRange (d : ds)
08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa ns = init fs ++ [Annotation.appendAnno (last fs) an]
08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa return $ Basic_spec ns
08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa-- | Toplevel parser for formulae
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseAx :: PrefixMap -> AnnoState.AParser st BASIC_ITEMS
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeparseAx pm = do
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. Schulze t <- many $ aFormula pm
08e520eb8e9947de926d733c48a13249c857f570Eugen Kuksa return $ Axiom_items t
c51d1f5ff88cce030fe543e271ca6b85625b70d8Karl Luc-- | Toplevel parser for formulae
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeaFormula :: PrefixMap -> AnnoState.AParser st (Annotation.Annoted TEXT_META)
feeab95fdf7ec92bcce607c104d9dc98e0e6ea90Soeren D. SchulzeaFormula pm = AnnoState.allAnnoParser (cltext pm)