a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{- |

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederModule : $Header$

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettDescription : AParser for first-order logic with dependent types (DFOL)

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederCopyright : (c) Kristina Sojakova, Jacobs University 2009

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : k.sojakova@ijacobs-university.de

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederStability : experimental

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachPortability : portable

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach-}

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblettmodule DFOL.Parse_AS_DFOL

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett (

78718c37b1a50086a27e0f031db4cf82bea934aeChristian Maeder basicSpec -- parser for DFOL specifications

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , symbItems -- parser for symbol lists

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach , symbMapItems -- parser for symbol map lists

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach )

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach where

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport qualified Common.Lexer as Lexer

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederimport Common.Token (casl_structured_reserved_words)

5cc369fbceee1b13bd0f06e43620c46541d1d4f8Christian Maederimport qualified Common.Keywords as Keywords

dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maederimport qualified Common.AnnoState as AnnoState

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachimport DFOL.AS_DFOL

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maederimport Text.ParserCombinators.Parsec

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- keywords which cannot appear as identifiers in a signature

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettreserved :: [String]

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbachreserved = [Keywords.trueS,

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Keywords.falseS,

70a691ea12f53381209a3709cdd325df5fc0a0c8Christian Maeder Keywords.notS,

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Keywords.forallS,

792df0347edab377785d98c63e2be8e2ce0a8bdeChristian Maeder Keywords.existsS,

0ea916d1e6aea10fd7b84f802fb5148a79d8c20aAndy Gimblett "Univ",

04ceed96d1528b939f2e592d0656290d81d1c045Andy Gimblett "Sort",

d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett "Form",

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly "Pi"] ++ casl_structured_reserved_words

9f93b2a8b552789cd939d599504d39732672dc84Christian Maeder

1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblett-- parser for basic spec

3b48e17c1da54ee669e70b626d9fbc32ce495b2cChristian MaederbasicSpec :: AnnoState.AParser st BASIC_SPEC

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillybasicSpec = fmap Basic_spec (AnnoState.trailingAnnosParser basicItemP)

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|>

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder (Lexer.oBraceT >> Lexer.cBraceT >> return (Basic_spec []))

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- parser for basic items

842ae753ab848a8508c4832ab64296b929167a97Christian MaederbasicItemP :: AnnoState.AParser st BASIC_ITEM

c4b2418421546a337f83332fe0db04742dcd735dAndy GimblettbasicItemP = do AnnoState.dotT

bcd914850de931848b86d7728192a149f9c0108bChristian Maeder f <- formulaP

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder return $ Axiom_item f

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <|>

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder do ns <- namesP

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder AnnoState.asKey "::"

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder t <- typeP

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return $ Decl_item (ns, t)

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- parser for all types

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaedertypeP :: AnnoState.AParser st TYPE

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian MaedertypeP = do AnnoState.asKey "Pi"

a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder vs <- varsP

a78bb62cd6f0beb2dab862db865357fc9d3c25feChristian Maeder t <- typeP

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder return $ Pi vs t

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder <|>

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder do t <- type1P

7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder (do AnnoState.asKey Keywords.funS

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder (ts, _) <- type1P `Lexer.separatedBy`

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder AnnoState.asKey Keywords.funS

bcd914850de931848b86d7728192a149f9c0108bChristian Maeder let xs = t:ts

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder return $ Func (init xs) (last xs)

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder <|>

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder return t)

bcd914850de931848b86d7728192a149f9c0108bChristian Maeder

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- parser for basic types and types enclosed in parentheses

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maedertype1P :: AnnoState.AParser st TYPE

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maedertype1P = do AnnoState.asKey "Sort"

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder return Sort

8db2221917c1bc569614f3481bcdb3b988facaedChristian Maeder <|>

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder do AnnoState.asKey "Form"

12b2ae689353ecbaad720a9af9f9be01c1a3fe2dChristian Maeder return Form

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett <|>

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett do AnnoState.asKey "Univ"

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett Lexer.oParenT

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett t <- termP

2f35e5f6757968746dbab385be21fcae52378a3fLiam O'Reilly Lexer.cParenT

fbc0c2baf563fe5b664f0152674a8d3acecca58cAndy Gimblett return $ Univ t

31f039ffdb33d78cb31d24b71d3155b11a323975Andy Gimblett <|>

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett do t <- termP

e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett return $ Univ t

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett <|>

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder do Lexer.oParenT

f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder t <- typeP

f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maeder Lexer.cParenT

90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett return t

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- parser for terms

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedertermP :: AnnoState.AParser st TERM

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimbletttermP = do f <- nameP

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (do Lexer.oParenT

4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder (as, _) <- termP `Lexer.separatedBy` AnnoState.anComma

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder Lexer.cParenT

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder return $ Appl (Identifier f) as

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder <|>

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder do return $ Identifier f)

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder-- parsers for names

842ae753ab848a8508c4832ab64296b929167a97Christian MaedernameP :: AnnoState.AParser st NAME

842ae753ab848a8508c4832ab64296b929167a97Christian MaedernameP = Lexer.pToken $ Lexer.reserved reserved Lexer.scanAnyWords

842ae753ab848a8508c4832ab64296b929167a97Christian Maeder

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy GimblettnamesP :: AnnoState.AParser st [NAME]

bb83db66bd9b3b4ce67be66419daf29886175276Andy GimblettnamesP = fmap fst $ nameP `Lexer.separatedBy` AnnoState.anComma

a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett-- parser for variable declarations

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedervarP :: AnnoState.AParser st ([NAME], TYPE)

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaedervarP = do ns <- namesP

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder AnnoState.asKey Keywords.colonS

dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder t <- typeP

dfc58f5ec6492d1a9b9babd9cdcdbb15baa6e657Christian Maeder return (ns, t)

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyvarsP :: AnnoState.AParser st [([NAME], TYPE)]

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyvarsP = do (vs, _) <- varP `Lexer.separatedBy` AnnoState.asKey ";"

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly AnnoState.dotT

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly return vs

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- parser for all formulas

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederformulaP :: AnnoState.AParser st FORMULA

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederformulaP = forallP

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett <|>

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett existsP

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett <|>

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett formula1P

4314e26a12954cb1c9be4dea10aa8103edac5bbbChristian Maeder

e54c5af823b9775dd2c058185ea5bdf7593950faAndy Gimblett{- parser for equivalences, implications, conjunctions, disjunctions,

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly negations, equalities, atomic formulas, and formulas in parentheses -}

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettformula1P :: AnnoState.AParser st FORMULA

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettformula1P = do f <- formula2P

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (-- equivalences

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly do AnnoState.asKey Keywords.equivS

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly g <- formula2P

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ Equivalence f g

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <|>

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- implications

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder do AnnoState.asKey Keywords.implS

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly g <- formula2P

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ Implication f g

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|>

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- all other cases

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return f)

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder{- parser for conjunctions, disjunctions, negations, equalities,

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly atomic formulas, and formulas in parentheses -}

f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maederformula2P :: AnnoState.AParser st FORMULA

f4a5178450076ee54f3a9adb4f91e241aea3ba75Christian Maederformula2P = do f <- formula3P

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (-- conjunctions

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett do AnnoState.asKey Keywords.lAnd

d297a45fc73aa6c4a1f9d073c3170611415f324bAndy Gimblett (fs, _) <- formula3P `Lexer.separatedBy`

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder AnnoState.asKey Keywords.lAnd

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return $ Conjunction (f:fs)

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <|>

0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder -- disjunctions

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder do AnnoState.asKey Keywords.lOr

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly (fs, _) <- formula3P `Lexer.separatedBy`

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly AnnoState.asKey Keywords.lOr

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ Disjunction (f:fs)

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|>

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly -- all other cases

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return f)

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly{- parser for negations, equalities, atomic formulas,

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly and formulas in parentheses -}

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyformula3P :: AnnoState.AParser st FORMULA

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reillyformula3P = parenFormulaP

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|>

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly negP

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|>

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly formula4P

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|>

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly trueP

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|>

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly falseP

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- parser for equalities and predicate formulas

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederformula4P :: AnnoState.AParser st FORMULA

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maederformula4P = do x <- termP

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder (-- equalities

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder do AnnoState.asKey "=="

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder y <- termP

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ Equality x y

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly <|>

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly -- predicates

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return (Pred x))

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- parser for formulas enclosed in parentheses

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyparenFormulaP :: AnnoState.AParser st FORMULA

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyparenFormulaP = do Lexer.oParenT

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly f <- formulaP

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly Lexer.cParenT

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return f

bb83db66bd9b3b4ce67be66419daf29886175276Andy Gimblett

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- parser for forall formulas

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederforallP :: AnnoState.AParser st FORMULA

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian MaederforallP = do AnnoState.asKey Keywords.forallS

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder vs <- varsP

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder f <- formulaP

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return $ Forall vs f

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- parser for exists formulas

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyexistsP :: AnnoState.AParser st FORMULA

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillyexistsP = do AnnoState.asKey Keywords.existsS

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly vs <- varsP

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly f <- formulaP

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly return $ Exists vs f

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly-- parser for negations

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillynegP :: AnnoState.AParser st FORMULA

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillynegP = do AnnoState.asKey Keywords.negS <|> AnnoState.asKey Keywords.notS

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly f <- formula3P

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return $ Negation f

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- parser for true

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedertrueP :: AnnoState.AParser st FORMULA

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedertrueP = do AnnoState.asKey Keywords.trueS

0b8146e4f675518993a34eb2255ad7ddd7bf82a4Christian Maeder return T

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'Reilly

ad872d5e07383c8fec42bddf02a13d1fbcac52b2Christian Maeder-- parser for false

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'ReillyfalseP :: AnnoState.AParser st FORMULA

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaederfalseP = do AnnoState.asKey Keywords.falseS

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return F

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder

7e7d791d2f643ffd82843b78e424b6f9f68c24eeChristian Maeder-- parser for symbol items

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedersymbItems :: AnnoState.AParser st SYMB_ITEMS

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedersymbItems = fmap Symb_items namesP

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- parser for symbol map items

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian MaedersymbMapItems :: AnnoState.AParser st SYMB_MAP_ITEMS

bcd914850de931848b86d7728192a149f9c0108bChristian MaedersymbMapItems = do (xs, _) <- symbOrMap `Lexer.separatedBy` AnnoState.anComma

05cc55892e6c93bdd7b9c3f100ab1bb65fe6a21eLiam O'Reilly return $ Symb_map_items xs

d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder-- parser for symbols or symbol maps

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillysymbOrMap :: AnnoState.AParser st SYMB_OR_MAP

9aeda2b3ae8ce0b018955521e4ca835a8ba8a27bLiam O'ReillysymbOrMap = do s <- nameP

fd4ad12563262ebe380d810df8f7755cfab5fb42Liam O'Reilly (do AnnoState.asKey Keywords.mapsTo

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder t <- nameP

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return $ Symb_map s t

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder <|>

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder return (Symb s))

7f24d24e63854a9a2539c2dac55198f746ad57dbChristian Maeder