Changeset 12725
- Timestamp:
- 26.10.2009 15:58:48 (4 weeks ago)
- Location:
- trunk
- Files:
-
- 12 modified
-
CASL/Formula.hs (modified) (1 diff)
-
CASL/Parse_AS_Basic.hs (modified) (3 diffs)
-
Common/AnnoState.hs (modified) (7 diffs)
-
Common/Lexer.hs (modified) (8 diffs)
-
HasCASL/ParseItem.hs (modified) (7 diffs)
-
HasCASL/ParseTerm.hs (modified) (9 diffs)
-
Isabelle/IsaParse.hs (modified) (14 diffs)
-
Propositional/Parse_AS_Basic.hs (modified) (3 diffs)
-
SoftFOL/DFGParser.hs (modified) (21 diffs)
-
SoftFOL/ParseTPTP.hs (modified) (4 diffs)
-
Syntax/Parse_AS_Architecture.hs (modified) (18 diffs)
-
Syntax/Parse_AS_Structured.hs (modified) (9 diffs)
Legend:
- Unmodified
- Added
- Removed
-
trunk/CASL/Formula.hs
r12184 r12725 80 80 restTerms :: AParsable f => [String] -> AParser st [TERM f] 81 81 restTerms k = (tryItemEnd startKeyword >> return []) 82 <|> bind (:) (restTerm k) (restTerms k)82 <|> restTerm k <:> restTerms k 83 83 <|> return [] 84 84 -
trunk/CASL/Parse_AS_Basic.hs
r10313 r12725 26 26 import Common.Keywords 27 27 import Common.Lexer 28 import Common.AS_Annotation 29 28 30 import CASL.AS_Basic_CASL 29 import Common.AS_Annotation30 import Text.ParserCombinators.Parsec31 31 import CASL.Formula 32 32 import CASL.SortItem 33 33 import CASL.OpItem 34 35 import Text.ParserCombinators.Parsec 36 37 import Control.Monad 34 38 35 39 -- * signature items … … 117 121 118 122 aFormula :: AParsable f => [String] -> AParser st (Annoted (FORMULA f)) 119 aFormula ks = bind appendAnno (annoParser $ formula ks) lineAnnos123 aFormula = allAnnoParser . formula 120 124 121 125 -- * basic spec … … 123 127 basicSpec :: (AParsable f, AParsable s, AParsable b) => 124 128 [String] -> AParser st (BASIC_SPEC b s f) 125 basicSpec ks = fmap Basic_spec $ annosParser $ basicItems ks129 basicSpec = fmap Basic_spec . annosParser . basicItems -
trunk/Common/AnnoState.hs
r11694 r12725 26 26 import Common.AS_Annotation 27 27 import Common.AnnoParser 28 28 29 import Text.ParserCombinators.Parsec 29 import Data.List(delete) 30 31 import Data.List 32 import Control.Monad 30 33 31 34 -- | parsers that can collect annotations via side effects 32 type AParser st a = GenParser Char (AnnoState st) a35 type AParser st = GenParser Char (AnnoState st) 33 36 34 37 class AParsable a where … … 99 102 -- | optional semicolon followed by annotations on consecutive lines 100 103 optSemi :: AParser st ([Token], [Annotation]) 101 optSemi = do (a1, s) <- try $ bind (,)annos semiT104 optSemi = do (a1, s) <- try $ pair annos semiT 102 105 a2 <- lineAnnos 103 106 return ([s], a1 ++ a2) … … 111 114 (single (oneOf "\"([{") <|> placeS <|> scanAnySigns 112 115 <|> many (scanLPD <|> char '_' <?> "") <?> "") 113 if null c || c `elem` l then return () elsepzero116 unless (null c || elem c l) pzero 114 117 115 118 -- | keywords that indicate a new item for 'tryItemEnd'. … … 120 123 -- | parse preceding annotations and the following item 121 124 annoParser :: AParser st a -> AParser st (Annoted a) 122 annoParser = bind addLeftAnno annos 125 annoParser = liftM2 addLeftAnno annos 126 127 allAnnoParser :: AParser st a -> AParser st (Annoted a) 128 allAnnoParser p = liftM2 appendAnno (annoParser p) lineAnnos 123 129 124 130 {- | parse preceding and consecutive trailing annotations of an item in … … 127 133 trailingAnnosParser :: AParser st a -> AParser st [Annoted a] 128 134 trailingAnnosParser p = do 129 l <- many1 $ bind appendAnno (annoParser p) lineAnnos135 l <- many1 $ allAnnoParser p 130 136 a <- annos -- append remaining annos to last item 131 137 return $ init l ++ [appendAnno (last l) a] … … 135 141 annosParser parser = 136 142 do a <- annos 137 l <- many1 $ bind (,)parser annos143 l <- many1 $ pair parser annos 138 144 let ps = map fst l 139 145 as = map snd l … … 147 153 itemList ks kw ip constr = 148 154 do p <- pluralKeyword kw 149 auxItemList (ks ++startKeyword) [p] (ip ks) constr155 auxItemList (ks ++ startKeyword) [p] (ip ks) constr 150 156 151 157 -- | generalized version of 'itemList' -
trunk/Common/Lexer.hs
r11206 r12725 18 18 import Text.ParserCombinators.Parsec 19 19 import qualified Text.ParserCombinators.Parsec.Pos as Pos 20 21 import Control.Monad 20 22 import Data.Char (digitToInt, isDigit, ord) 21 23 import Data.List (isPrefixOf) … … 42 44 caslLetters ch = let c = ord ch in 43 45 if c <= 122 && c >= 65 then c >= 97 || c <= 90 44 else c >= 192 && c <= 255 && not (elem c [215, 247])46 else c >= 192 && c <= 255 && notElem c [215, 247] 45 47 46 48 -- ['A'..'Z'] ++ ['a'..'z'] ++ … … 61 63 -- * Monad and Functor extensions 62 64 63 bind :: (Monad m) => (a -> b -> c) -> m a -> m b -> m c64 bind f p q = do { x <- p; y <- q; return (f x y) }65 66 65 infixl << 67 66 68 (<<) :: (Monad m)=> m a -> m b -> m a69 (<<) = bindconst67 (<<) :: Monad m => m a -> m b -> m a 68 (<<) = liftM2 const 70 69 71 70 infixr 5 <:> 72 71 73 (<:>) :: (Monad m)=> m a -> m [a] -> m [a]74 (<:>) = bind(:)72 (<:>) :: Monad m => m a -> m [a] -> m [a] 73 (<:>) = liftM2 (:) 75 74 76 75 infixr 5 <++> 77 76 78 (<++>) :: (Monad m) => m [a] -> m [a] -> m [a] 79 (<++>) = bind (++) 77 (<++>) :: Monad m => m [a] -> m [a] -> m [a] 78 (<++>) = liftM2 (++) 79 80 pair :: Monad m => m a -> m b -> m (a, b) 81 pair = liftM2 (,) 80 82 81 83 -- Functor extension … … 83 85 single = fmap return 84 86 85 flat :: (Functor f)=> f [[a]] -> f [a]87 flat :: Functor f => f [[a]] -> f [a] 86 88 flat = fmap concat 87 89 … … 273 275 skip 274 276 q <- getPosition 275 if Pos.sourceLine q <= Pos.sourceLine p + 1 276 then return () 277 else notFollowedBy (char '%') >> return ()) 277 unless (Pos.sourceLine q <= Pos.sourceLine p + 1) 278 $ notFollowedBy (char '%') >> return ()) 278 279 <|> return () 279 280 … … 281 282 282 283 keyWord :: CharParser st a -> CharParser st a 283 keyWord p = try(p<< notFollowedBy (scanLPD <|> singleUnderline))284 keyWord = try . (<< notFollowedBy (scanLPD <|> singleUnderline)) 284 285 285 286 keySign :: CharParser st a -> CharParser st a 286 keySign p = try(p<< notFollowedBy (oneOf signChars))287 keySign = try . (<< notFollowedBy (oneOf signChars)) 287 288 288 289 reserved :: [String] -> CharParser st String -> CharParser st String … … 293 294 294 295 pToken :: CharParser st String -> CharParser st Token 295 pToken parser = 296 bind (\ p s -> Token s $ Range [p]) getPos (parser << skipSmart) 296 pToken = liftM2 (\ p s -> Token s $ Range [p]) getPos . (<< skipSmart) 297 297 298 298 pluralKeyword :: String -> CharParser st Token … … 355 355 notFollowedWith :: GenParser tok st a -> GenParser tok st b 356 356 -> GenParser tok st a 357 notFollowedWith p1 p2 = try $ do 358 pp <- (try (p1 >> p2) >> return pzero) <|> return p1 359 pp 357 notFollowedWith p1 p2 = 358 try $ join $ (try (p1 >> p2) >> return pzero) <|> return p1 360 359 -- see http://www.mail-archive.com/haskell@haskell.org/msg14388.html 361 360 -- by Andrew Pimlott -
trunk/HasCASL/ParseItem.hs
r11877 r12725 28 28 import HasCASL.ParseTerm 29 29 30 import Control.Monad 31 30 32 -- * adapted item list parser (using 'itemAux') 31 33 … … 38 40 hasCaslItemAux :: [Token] -> AParser st b -> ([Annoted b] -> Range -> a) 39 41 -> AParser st a 40 hasCaslItemAux ps = auxItemList hasCaslStartKeywords ps42 hasCaslItemAux = auxItemList hasCaslStartKeywords 41 43 42 44 -- * parsing type items … … 118 120 119 121 typeItemList :: [Token] -> Instance -> AParser st SigItems 120 typeItemList ps k = hasCaslItemAux ps typeItem $ TypeItems k122 typeItemList ps = hasCaslItemAux ps typeItem . TypeItems 121 123 122 124 typeItems :: AParser st SigItems … … 184 186 c <- asKey defnS 185 187 a <- annos 186 let aAlternative = bind (\ i an -> Annoted i nullRange [] an)188 let aAlternative = liftM2 (\ i -> Annoted i nullRange []) 187 189 alternative annos 188 190 (Annoted v _ _ b : as, ps) <- aAlternative `separatedBy` barT … … 214 216 classDecl = do 215 217 (is, cs) <- classId `separatedBy` anComma 216 (ps, k) <- option ([], universe) $ bind(,) (single lessT) kind218 (ps, k) <- option ([], universe) $ liftM2 (,) (single lessT) kind 217 219 return $ ClassDecl is k $ catRange $ cs ++ ps 218 220 … … 227 229 228 230 classItemList :: [Token] -> Instance -> AParser st BasicItem 229 classItemList ps k = hasCaslItemAux ps classItem $ ClassItems k231 classItemList ps = hasCaslItemAux ps classItem . ClassItems 230 232 231 233 classItems :: AParser st BasicItem … … 395 397 dotFormulae = do 396 398 d <- dotT 397 let aFormula = bind appendAnno (annoParser term) lineAnnos 398 (fs, ds) <- aFormula `separatedBy` dotT 399 (fs, ds) <- allAnnoParser term `separatedBy` dotT 399 400 let ps = catRange $ d : ds 400 401 lst = last fs -
trunk/HasCASL/ParseTerm.hs
r10656 r12725 22 22 import HasCASL.As 23 23 import HasCASL.AsUtils 24 24 25 import Text.ParserCombinators.Parsec 26 27 import Control.Monad 28 25 29 import Data.List ((\\)) 26 30 import qualified Data.Set as Set 31 27 32 28 33 -- * key sign tokens … … 45 50 -- | parser for square brackets 46 51 mkBrackets :: AParser st a -> ([a] -> Range -> b) -> AParser st b 47 mkBrackets p c = bracketParser p oBracketT cBracketT anComma c52 mkBrackets p = bracketParser p oBracketT cBracketT anComma 48 53 49 54 -- | parser for braces 50 55 mkBraces :: AParser st a -> ([a] -> Range -> b) -> AParser st b 51 mkBraces p c = bracketParser p oBraceT cBraceT anComma c56 mkBraces p = bracketParser p oBraceT cBraceT anComma 52 57 53 58 -- * kinds … … 63 68 -- | do 'parseSimpleKind' and check for an optional 'Variance' 64 69 parseExtKind :: AParser st (Variance, Kind) 65 parseExtKind = bind (,)variance parseSimpleKind70 parseExtKind = pair variance parseSimpleKind 66 71 67 72 -- | parse a (right associative) function kind for a given argument kind … … 96 101 -- a (simple) type variable with a 'Variance' 97 102 extVar :: AParser st Id -> AParser st (Id, Variance) 98 extVar vp = bind (,)vp variance103 extVar vp = pair vp variance 99 104 100 105 -- several 'extVar' with a 'Kind' … … 333 338 -- | attach the 'Type' to every 'Var' 334 339 makeVarDecls :: [Id] -> [Token] -> Type -> Range -> [VarDecl] 335 makeVarDecls vs ps t q = zipWith ( \ v p -> VarDecl v t Comma $ tokPos p)340 makeVarDecls vs ps t q = zipWith ( \ v -> VarDecl v t Comma . tokPos) 336 341 (init vs) ps ++ [VarDecl (last vs) t Other q] 337 342 … … 347 352 let other = fmap (map GenTypeVarDecl) (typeKind True vs ps) 348 353 if allIsNonVar vs then fmap (map GenVarDecl) 349 (varDeclType (map ( \ (i, _) -> i)vs) ps) <|> other354 (varDeclType (map fst vs) ps) <|> other 350 355 else other 351 356 … … 414 419 lamPattern :: AParser st [Term] 415 420 lamPattern = 416 (lookAhead lamDot >> return []) <|> bind (:) (typedPattern [])lamPattern421 (lookAhead lamDot >> return []) <|> typedPattern [] <:> lamPattern 417 422 418 423 -- * terms … … 497 502 -- | 'opS' or 'functS' 498 503 opBrand :: AParser st (Token, OpBrand) 499 opBrand = bind (,)(asKey opS) (return Op)500 <|> bind (,)(asKey functS) (return Fun)504 opBrand = pair (asKey opS) (return Op) 505 <|> pair (asKey functS) (return Fun) 501 506 502 507 parsePolyId :: AParser st PolyId … … 573 578 -- | a 'Universal', 'Unique' or 'Existential' 'QuantifiedTerm' 574 579 exQuant :: AParser st (Token, Quantifier) 575 exQuant = choice $ map (\ (v, s) -> bind (,)(asKey s) $ return v)580 exQuant = choice $ map (\ (v, s) -> pair (asKey s) $ return v) 576 581 [ (Universal, forallS) 577 582 , (Unique, existsS ++ exMark) -
trunk/Isabelle/IsaParse.hs
r10689 r12725 21 21 , compatibleBodies) where 22 22 23 import Isabelle.IsaConsts 24 25 import Common.DocUtils 26 import Common.Id 27 import Common.Lexer 28 import Common.Result 29 30 import Text.ParserCombinators.Parsec 31 32 import Control.Monad 33 23 34 import Data.List 24 import Common.Lexer25 import Text.ParserCombinators.Parsec26 35 import qualified Data.Map as Map 27 import Isabelle.IsaConsts28 import Common.Id29 import Common.Result30 import Common.DocUtils31 36 32 37 latin :: Parser String … … 102 107 103 108 lexP :: Parser String -> Parser Token 104 lexP pa = bind (\ p s -> Token s (Range [p])) getPos $ pa << isaSkip109 lexP = liftM2 (\ p s -> Token s (Range [p])) getPos . (<< isaSkip) 105 110 106 111 lexS :: String -> Parser String … … 140 145 141 146 commalist :: Parser a -> Parser [a] 142 commalist p = fmap fst $ p `separatedBy` lexS ","147 commalist = fmap fst . flip separatedBy (lexS ",") 143 148 144 149 parensP :: Parser a -> Parser a … … 206 211 attributes :: Parser [Bool] 207 212 attributes = bracketsP . commalist $ 208 bind(\ n l -> null l && show n == simpS) namerefP args213 liftM2 (\ n l -> null l && show n == simpS) namerefP args 209 214 210 215 lessOrEq :: Parser String … … 251 256 252 257 consts :: Parser [Const] 253 consts = lexS constsS >> many1 ( bindConst nameP (typeSuffix258 consts = lexS constsS >> many1 (liftM2 Const nameP (typeSuffix 254 259 << option () mixfix)) 255 260 … … 288 293 289 294 axmdecl :: Parser SenDecl 290 axmdecl = (bind SenDecl nameP optAttributes)<< lexS ":"295 axmdecl = liftM2 SenDecl nameP optAttributes << lexS ":" 291 296 292 297 prop :: Parser Token … … 296 301 297 302 axiomsP :: Parser [Axiom] 298 axiomsP = many1 ( bindAxiom axmdecl prop)303 axiomsP = many1 (liftM2 Axiom axmdecl prop) 299 304 300 305 defs :: Parser [Axiom] … … 306 311 307 312 thmbind :: Parser SenDecl 308 thmbind = (bind SenDecl nameP optAttributes)313 thmbind = liftM2 SenDecl nameP optAttributes 309 314 <|> (attributes >> return emptySen) 310 315 … … 337 342 338 343 props :: Parser Goal 339 props = bind Goal (option (emptySen)thmdecl)344 props = liftM2 Goal (option emptySen thmdecl) 340 345 $ many1 (prop << option () proppat) 341 346 … … 358 363 359 364 cons :: Parser [Token] 360 cons = bind (:) nameP (many typeP)<< option () mixfix365 cons = nameP <:> many typeP << option () mixfix 361 366 362 367 data Dtspec = Dtspec Typespec [[Token]] … … 436 441 addAxiom :: Axiom -> Map.Map Token (SimpValue Token) 437 442 -> Map.Map Token (SimpValue Token) 438 addAxiom (Axiom (SenDecl n b) a) m = Map.insert n (SimpValue b a) m443 addAxiom (Axiom (SenDecl n b) a) = Map.insert n (SimpValue b a) 439 444 440 445 addGoal :: Goal -> Map.Map Token (SimpValue [Token]) 441 446 -> Map.Map Token (SimpValue [Token]) 442 addGoal (Goal (SenDecl n b) a) m = Map.insert n (SimpValue b a) m447 addGoal (Goal (SenDecl n b) a) = Map.insert n (SimpValue b a) 443 448 444 449 addConst :: Const -> Map.Map Token Token -> Map.Map Token Token 445 addConst (Const n a) m = Map.insert n a m450 addConst (Const n a) = Map.insert n a 446 451 447 452 addDatatype :: Dtspec -> Map.Map Token ([Token], [[Token]]) 448 453 -> Map.Map Token ([Token], [[Token]]) 449 addDatatype (Dtspec (Typespec n ps) a) m = Map.insert n (ps, a) m454 addDatatype (Dtspec (Typespec n ps) a) = Map.insert n (ps, a) 450 455 451 456 emptyBody :: Body … … 467 472 -- | parses a complete isabelle theory file, but skips i.e. proofs 468 473 parseTheory :: Parser (TheoryHead, Body) 469 parseTheory = bind (,)474 parseTheory = pair 470 475 theoryHead (fmap (foldr concatBodyElems emptyBody) theoryBody) 471 476 << lexS endS << eof … … 481 486 482 487 warnSimpAttr :: Body -> [Diagnosis] 483 warnSimpAttr b=488 warnSimpAttr = 484 489 map ( \ a -> Diag Warning 485 490 ("use 'declare " ++ tokStr a 486 491 ++ " [simp]' for proper Isabelle proof details") $ tokPos a) 487 $ Map.keys . Map.filter hasSimp $ axiomsF b492 . Map.keys . Map.filter hasSimp . axiomsF 488 493 489 494 diffMap :: (Ord a, Pretty a, GetRange a, Eq b, Show b) … … 505 510 LT -> True 506 511 kd = if b then kd12 else kd21 507 in map ( \ k ->mkDiag Error508 (msg ++ " entry illegally " ++509 if b then "added" else "deleted") k ) kd512 in map (mkDiag Error 513 $ msg ++ " entry illegally " ++ 514 if b then "added" else "deleted") kd -
trunk/Propositional/Parse_AS_Basic.hs
r11682 r12725 30 30 import Common.Keywords as Keywords 31 31 import Common.Lexer as Lexer 32 32 33 import Propositional.AS_BASIC_Propositional as AS_BASIC 33 import qualified Common.AS_Annotation as AS_Anno34 34 import Text.ParserCombinators.Parsec 35 36 import Control.Monad 35 37 36 38 propKeywords :: [String] … … 62 64 (_, an) <- AnnoState.optSemi 63 65 let _ = Id.catRange (d:ds) 64 ns = init fs ++ [A S_Anno.appendAnno (last fs) an]66 ns = init fs ++ [Annotation.appendAnno (last fs) an] 65 67 return $ AS_BASIC.Axiom_items ns 66 68 … … 164 166 165 167 -- | Toplevel parser for formulae 166 aFormula :: AnnoState.AParser st (AS_Anno.Annoted AS_BASIC.FORMULA) 167 aFormula = Lexer.bind AS_Anno.appendAnno (AnnoState.annoParser impFormula) 168 AnnoState.lineAnnos 168 aFormula :: AnnoState.AParser st (Annotation.Annoted AS_BASIC.FORMULA) 169 aFormula = AnnoState.allAnnoParser impFormula 169 170 170 171 -- | parsing a prop symbol -
trunk/SoftFOL/DFGParser.hs
r10322 r12725 22 22 import qualified Data.Map as Map 23 23 import Data.Char (isSpace) 24 import Data.Maybe 25 import Control.Monad 24 26 25 27 -- * lexical matter … … 43 45 44 46 identifierT :: Parser Token 45 identifierT = bind(\ p s -> Token s (Range [p])) getPos identifierS47 identifierT = liftM2 (\ p s -> Token s (Range [p])) getPos identifierS 46 48 47 49 arityT :: Parser Int … … 81 83 squaresDot p = symbolT "[" >> p << symbolT "]." 82 84 83 text :: Parser [Char]85 text :: Parser String 84 86 text = fmap (reverse . dropWhile isSpace . reverse) $ 85 symbolT "{*" >> (manyTill anyChar $symbolT "*}")86 87 list _of :: [Char]-> Parser String88 list _of sort = symbolT $ "list_of_" ++ sort89 90 list _of_dot :: [Char]-> Parser String91 list _of_dot sort = list_of (sort++ ".")92 93 end _of_list :: Parser String94 end _of_list = symbolT "end_of_list."87 symbolT "{*" >> manyTill anyChar (symbolT "*}") 88 89 listOf :: String -> Parser String 90 listOf = symbolT . ("list_of_" ++) 91 92 listOfDot :: String -> Parser String 93 listOfDot = listOf . (++ ".") 94 95 endOfList :: Parser String 96 endOfList = symbolT "end_of_list." 95 97 96 98 mapTokensToData :: [(String, a)] -> Parser a … … 113 115 symbolT "begin_problem" 114 116 i <- parensDot identifierS 115 dl <- description _list116 lp <- logical _part117 s <- setting _list117 dl <- descriptionList 118 lp <- logicalPartP 119 s <- settingList 118 120 symbolT "end_problem." 119 121 many anyChar … … 130 132 at least a 'name', the name of the 'author', the 'status' (see also 131 133 'SPLogState' below), and a (verbose) description. -} 132 description _list :: Parser SPDescription133 description _list = do134 list _of_dot "descriptions"134 descriptionList :: Parser SPDescription 135 descriptionList = do 136 listOfDot "descriptions" 135 137 keywordT "name" 136 138 n <- parensDot text … … 146 148 de <- parensDot text 147 149 da <- maybeParser (keywordT "date" >> parensDot text) 148 end _of_list150 endOfList 149 151 return SPDescription 150 152 { name = n … … 163 165 been implemented yet. 164 166 -} 165 logical _part:: Parser SPLogicalPart166 logical _part= do167 sl <- maybeParser symbol _list168 dl <- maybeParser declaration _list169 fs <- many formula _list170 cl <- many clause _list171 pl <- many proof _list167 logicalPartP :: Parser SPLogicalPart 168 logicalPartP = do 169 sl <- maybeParser symbolListP 170 dl <- maybeParser declarationListP 171 fs <- many formulaList 172 cl <- many clauseList 173 pl <- many proofList 172 174 return SPLogicalPart 173 175 { symbolList = sl … … 182 184 SPASS Symbol List 183 185 -} 184 symbol _list:: Parser SPSymbolList185 symbol _list= do186 list _of_dot "symbols"186 symbolListP :: Parser SPSymbolList 187 symbolListP = do 188 listOfDot "symbols" 187 189 fs <- option [] (signSymFor "functions") 188 190 ps <- option [] (signSymFor "predicates") 189 191 ss <- option [] sortSymFor 190 end _of_list192 endOfList 191 193 return emptySymbolList 192 194 { functions = fs … … 209 211 return SPSignSym {sym = s, arity = a} 210 212 211 func _list :: Parser [SPIdentifier]212 func _list = squaresDot $ commaSep identifierT213 functList :: Parser [SPIdentifier] 214 functList = squaresDot $ commaSep identifierT 213 215 214 216 -- *** Formula List … … 217 219 SPASS Formula List 218 220 -} 219 formula _list :: Parser SPFormulaList220 formula _list = do221 list _of "formulae"221 formulaList :: Parser SPFormulaList 222 formulaList = do 223 listOf "formulae" 222 224 ot <- parensDot $ mapTokensToData 223 225 [ ("axioms", SPOriginAxioms) 224 226 , ("conjectures", SPOriginConjectures)] 225 227 fs <- many (formula (case ot of {SPOriginAxioms -> True; _ -> False})) 226 end _of_list228 endOfList 227 229 return SPFormulaList { originType = ot, formulae = fs } 228 230 229 clause _list :: Parser SPClauseList230 clause _list = do231 list _of "clauses"231 clauseList :: Parser SPClauseList 232 clauseList = do 233 listOf "clauses" 232 234 (ot, ct) <- parensDot $ do 233 235 ot <- mapTokensToData … … 240 242 SPOriginAxioms -> True 241 243 _ -> False 242 end _of_list244 endOfList 243 245 return SPClauseList 244 246 { coriginType = ot … … 254 256 clauseFork :: SPClauseType -> Parser NSPClause 255 257 clauseFork ct = do 256 termWsList1@(TWL ls b) <- term _ws_list258 termWsList1@(TWL ls b) <- termWsList 257 259 do symbolT "||" 258 termWsList2 <- term _ws_list260 termWsList2 <- termWsList 259 261 symbolT "->" 260 termWsList3 <- term _ws_list262 termWsList3 <- termWsList 261 263 return (BriefClause termWsList1 termWsList2 termWsList3) 262 264 <|> case ls of … … 274 276 return $ SimpleClause b 275 277 276 term _ws_list :: Parser TermWsList277 term _ws_list = do278 termWsList :: Parser TermWsList 279 termWsList = do 278 280 twl <- many term 279 281 p <- maybeParser (symbolT "+") 280 return (TWL twl (maybe False (const True) p))282 return $ TWL twl $ isJust p 281 283 282 284 formula :: Bool -> Parser (Named SoftFOL.Sign.SPTerm) … … 286 288 return (makeNamed fname sen) { isAxiom = bool }) 287 289 288 declaration _list:: Parser [SPDeclaration]289 declaration _list= do290 list _of_dot "declarations"290 declarationListP :: Parser [SPDeclaration] 291 declarationListP = do 292 listOfDot "declarations" 291 293 decl <- many declaration 292 end _of_list294 endOfList 293 295 return decl 294 296 … … 299 301 maybeFreely <- option False (keywordT "freely" >> return True) 300 302 keywordT "generated by" 301 funList <- func _list303 funList <- functList 302 304 return SPGenDecl 303 305 { sortSym = sortName … … 317 319 pn <- identifierT 318 320 comma 319 sl <- commaSep $identifierT321 sl <- commaSep identifierT 320 322 return (pn, sl) 321 323 return SPPredDecl { predSym = pn, sortSyms = sl } … … 329 331 330 332 -- | SPASS Proof List 331 proof _list :: Parser SPProofList332 proof _list = do333 list _of "proof"333 proofList :: Parser SPProofList 334 proofList = do 335 listOf "proof" 334 336 pa <- maybeParser $ parensDot $ do 335 337 pt <- maybeParser getproofType 336 ass ocList <- option Map.empty (comma >> assoc_list)337 return (pt, ass ocList)338 steps <- many proof _step339 end _of_list338 assList <- option Map.empty (comma >> assocList) 339 return (pt, assList) 340 steps <- many proofStep 341 endOfList 340 342 return $ case pa of 341 343 Nothing -> SPProofList … … 351 353 getproofType = identifierT 352 354 353 assoc_list :: Parser SPAssocList 354 assoc_list = fmap Map.fromList $ squares ( commaSep $ takeTroop ) 355 where takeTroop = do 356 key <- getKey 357 symbolT ":" 358 val <- getValue 359 return (key, val) 355 assocList :: Parser SPAssocList 356 assocList = fmap Map.fromList $ squares $ commaSep 357 $ pair getKey $ symbolT ":" >> getValue 360 358 361 359 getKey :: Parser SPKey … … 365 363 getValue = fmap PValTerm term 366 364 367 proof _step :: Parser SPProofStep368 proof _step = do365 proofStep :: Parser SPProofStep 366 proofStep = do 369 367 keywordT "step" 370 368 (ref, res, rule, pl, mal) <- parensDot takeStep … … 383 381 comma 384 382 pl <- getParentList 385 mal <- option Map.empty (comma >> assoc _list)383 mal <- option Map.empty (comma >> assocList) 386 384 return (ref, res, rule, pl, mal) 387 385 … … 409 407 Nothing -> r 410 408 _ -> r 411 getParentList = squares (commaSep $ getParent)409 getParentList = squares $ commaSep getParent 412 410 getParent = fmap PParTerm term 413 411 414 412 -- SPASS Settings. 415 setting _list :: Parser [SPSetting]416 setting _list = many setting413 settingList :: Parser [SPSetting] 414 settingList = many setting 417 415 418 416 setting :: Parser SPSetting 419 417 setting = do 420 list _of_dot "general_settings"421 entriesList <- many setting _entry422 end _of_list418 listOfDot "general_settings" 419 entriesList <- many settingEntry 420 endOfList 423 421 return SPGeneralSettings {entries = entriesList} 424 422 <|> do 425 list _of "settings"423 listOf "settings" 426 424 slabel <- parensDot getLabel 427 425 symbolT "{*" 428 426 t <- many clauseFormulaRelation 429 427 symbolT "*}" 430 end _of_list428 endOfList 431 429 return SPSettings {settingName = slabel, settingBody = t} 432 430 433 setting _entry :: Parser SPHypothesis434 setting _entry = do431 settingEntry :: Parser SPHypothesis 432 settingEntry = do 435 433 keywordT "hypothesis" 436 434 slabels <- squaresDot (commaSep identifierT) -
trunk/SoftFOL/ParseTPTP.hs
r11854 r12725 17 17 import Text.ParserCombinators.Parsec 18 18 import SoftFOL.Sign 19 import SoftFOL.PrintTPTP 20 21 import qualified Common.Doc as Doc 19 22 import Common.Id 20 import Common.Lexer ((<<), bind, getPos) 23 import Common.Lexer ((<<), getPos) 24 25 import Control.Monad 21 26 import Data.Char (ord, toLower, isAlphaNum) 22 import qualified Common.Doc as Doc 23 import SoftFOL.PrintTPTP 27 24 28 25 29 data TPTP = … … 105 109 106 110 blank :: Parser p -> Parser () 107 blank p = p >> skipMany1 whiteSpace111 blank = (>> skipMany1 whiteSpace) 108 112 109 113 szsOutput :: Parser () … … 145 149 146 150 lexeme :: Parser a -> Parser a 147 lexeme p = p << skipAll151 lexeme = (<< skipAll) 148 152 149 153 key :: Parser a -> Parser () 150 key p = p >> skipAll154 key = (>> skipAll) 151 155 152 156 comma :: Parser () … … 292 296 293 297 pToken :: Parser String -> Parser Token 294 pToken parser = 295 bind (\ p s -> Token s (Range [p])) getPos (parser << skipAll) 298 pToken = liftM2 (\ p s -> Token s (Range [p])) getPos . (<< skipAll) 296 299 297 300 form :: Parser SPTerm -
trunk/Syntax/Parse_AS_Architecture.hs
r10299 r12725 20 20 21 21 import Logic.Grothendieck(LogicGraph) 22 22 23 import Syntax.AS_Structured 23 24 import Syntax.AS_Architecture 24 25 import Syntax.Parse_AS_Structured 25 (annoParser2, groupSpec, parseMapping, translation_list) 26 (annoParser2, groupSpec, parseMapping, translationList) 27 26 28 import Common.AS_Annotation 27 29 import Common.AnnoState 30 import Common.Id 28 31 import Common.Keywords 29 32 import Common.Lexer 30 33 import Common.Token 34 31 35 import Text.ParserCombinators.Parsec 32 import Common.Id33 36 34 37 ------------------------------------------------------------------------ … … 37 40 -- | Parse annotated architectural specification 38 41 annotedArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC) 39 annotedArchSpec l = annoParser2 (archSpec l)42 annotedArchSpec = annoParser2 . archSpec 40 43 41 44 -- | Parse architectural specification … … 44 47 -- @ 45 48 archSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC) 46 archSpec l = 47 do asp <- basicArchSpec l 48 return asp 49 <|> 50 do asp <- groupArchSpec l 51 return asp 49 archSpec l = basicArchSpec l <|> groupArchSpec l 52 50 53 51 -- | Parse group architectural specification … … 56 54 -- @ 57 55 groupArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC) 58 groupArchSpec l = 59 do kOpBr <- oBraceT 60 asp <- annoParser $ archSpec l 61 kClBr <- cBraceT 62 return (replaceAnnoted 63 (Group_arch_spec (item asp) $ toRange kOpBr [] kClBr) asp) 64 <|> 65 do name <- simpleId 66 return (emptyAnno $ Arch_spec_name name) 56 groupArchSpec l = do 57 kOpBr <- oBraceT 58 asp <- annoParser $ archSpec l 59 kClBr <- cBraceT 60 return $ replaceAnnoted 61 (Group_arch_spec (item asp) $ toRange kOpBr [] kClBr) asp 62 <|> fmap (emptyAnno . Arch_spec_name) simpleId 67 63 68 64 -- | Parse basic architectural specification … … 72 68 -- @ 73 69 basicArchSpec :: LogicGraph -> AParser st (Annoted ARCH_SPEC) 74 basicArchSpec l = 75 dokUnit <- pluralKeyword unitS76 77 78 79 80 81 $ tokPos kUnit `appRange` ps `appRange` catRange (kResult:m)70 basicArchSpec l = do 71 kUnit <- pluralKeyword unitS 72 (declDefn, ps) <- auxItemList [resultS] [] (unitDeclDefn l) (,) 73 kResult <- asKey resultS 74 expr <- annoParser2 $ unitExpr l 75 (m, an) <- optSemi 76 return $ emptyAnno $ Basic_arch_spec declDefn (appendAnno expr an) 77 $ tokPos kUnit `appRange` ps `appRange` catRange (kResult : m) 82 78 83 79 -- | Parse unit declaration or definition … … 90 86 do c <- colonT -- unit declaration 91 87 decl <- refSpec l 92 (gs, ps) <- option ([], []) $ 93 dokGiven <- asKey givenS94 95 return (guts, kGiven:qs)96 return (Unit_decl name decl gs $ catRange (c:ps))88 (gs, ps) <- option ([], []) $ do 89 kGiven <- asKey givenS 90 (guts, qs) <- groupUnitTerm l `separatedBy` anComma 91 return (guts, kGiven : qs) 92 return $ Unit_decl name decl gs $ catRange $ c : ps 97 93 <|> -- unit definition 98 94 unitDefn' l name … … 103 99 -- @ 104 100 unitRef :: LogicGraph -> AParser st UNIT_REF 105 unitRef l = 106 doname <- simpleId107 108 109 101 unitRef l = do 102 name <- simpleId 103 sep1 <- asKey toS 104 usp <- refSpec l 105 return $ Unit_ref name usp $ tokPos sep1 110 106 111 107 -- | Parse unit specification … … 120 116 do kClosed <- asKey closedS 121 117 uSpec <- unitSpec l 122 return (Closed_unit_spec uSpec $ tokPos kClosed)118 return $ Closed_unit_spec uSpec $ tokPos kClosed 123 119 <|> -- unit type 124 120 {- NOTE: this can also be a spec name. If this is the case, this unit spec 125 121 will be converted on the static analysis stage. 126 122 See Static.AnalysisArchitecture.ana_UNIT_SPEC. -} 127 do gps@(gs :gss, _) <- annoParser (groupSpec l) `separatedBy` crossT123 do gps@(gs : gss, _) <- annoParser (groupSpec l) `separatedBy` crossT 128 124 let rest = unitRestType l gps 129 if null gss then do125 if null gss then 130 126 option ( {- case item gs of 131 127 Spec_inst sn [] _ -> Spec_name sn -- annotations are lost … … 142 138 refSpec :: LogicGraph -> AParser st REF_SPEC 143 139 refSpec l = do 144 (rs, ps) <- basicRefSpec l `separatedBy` (asKey thenS) 145 return $ if isSingle rs then head rs 146 else Compose_ref rs $ catRange ps 140 (rs, ps) <- basicRefSpec l `separatedBy` asKey thenS 141 return $ if isSingle rs then head rs else Compose_ref rs $ catRange ps 147 142 148 143 -- | Parse refinement specification … … 179 174 r <- asKey refinedS 180 175 (ms, ps) <- option ([], []) $ do 181 182 183 176 v <- asKey viaS -- not a keyword 177 (m, ts) <- parseMapping l 178 return (m, v : ts) 184 179 t <- asKey toS 185 180 rsp <- refSpec l … … 211 206 -- The SYMB-MAP-ITEMS-LIST is parsed using parseItemsMap. 212 207 fitArgUnit :: LogicGraph -> AParser st FIT_ARG_UNIT 213 fitArgUnit l = 214 doo <- oBracketT215 216 (fargs, qs) <- option ([], [])217 (dokFit <- asKey fitS218 219 return (smis, kFit:ps))220 221 208 fitArgUnit l = do 209 o <- oBracketT 210 ut <- unitTerm l 211 (fargs, qs) <- option ([], []) $ do 212 kFit <- asKey fitS 213 (smis, ps) <- parseMapping l 214 return (smis, kFit : ps) 215 c <- cBracketT 216 return $ Fit_arg_unit ut fargs $ toRange o qs c 222 217 223 218 -- | Parse unit term. … … 232 227 -- the operator precedence; see other 'unitTerm*' functions. 233 228 unitTerm :: LogicGraph -> AParser st (Annoted UNIT_TERM) 234 unitTerm l = unitTermAmalgamation l229 unitTerm = unitTermAmalgamation 235 230 236 231 -- | Parse unit amalgamation. … … 239 234 -- @ 240 235 unitTermAmalgamation :: LogicGraph -> AParser st (Annoted UNIT_TERM) 241 unitTermAmalgamation l = 242 do (uts, toks) <- annoParser2 (unitTermLocal l) `separatedBy` (asKey andS)243 return (case uts of244 245 _ -> emptyAnno (Amalgamation uts (catRange toks)))236 unitTermAmalgamation l = do 237 (uts, toks) <- annoParser2 (unitTermLocal l) `separatedBy` asKey andS 238 return $ case uts of 239 [ut] -> ut 240 _ -> emptyAnno $ Amalgamation uts $ catRange toks 246 241 247 242 -- | Parse local unit term … … 260 255 $ tokPos kLocal `appRange` ps `appRange` tokPos kWithin 261 256 <|> -- translation/reduction 262 do ut <- unitTermTransRed l 263 return ut 257 unitTermTransRed l 264 258 265 259 -- | Parse translation or reduction unit term … … 273 267 unitTermTransRed :: LogicGraph -> AParser st (Annoted UNIT_TERM) 274 268 unitTermTransRed l = groupUnitTerm l >>= 275 translation _list l Unit_translation Unit_reduction269 translationList l Unit_translation Unit_reduction 276 270 277 271 -- | Parse unit expression … … 281 275 -- @ 282 276 unitExpr :: LogicGraph -> AParser st (Annoted UNIT_EXPRESSION) 283 unitExpr l = 284 do (bindings, poss) <- option ([], nullRange)285 (dokLambda <- asKey lambdaS286 287 288 return (bindings, toRange kLambda poss kDot))289 290 return (emptyAnno $ Unit_expression bindings ut poss)277 unitExpr l = do 278 (bindings, poss) <- option ([], nullRange) $ do 279 kLambda <- asKey lambdaS 280 (bindings, poss) <- unitBinding l `separatedBy` anSemi 281 kDot <- dotT 282 return (bindings, toRange kLambda poss kDot) 283 ut <- unitTerm l 284 return $ emptyAnno $ Unit_expression bindings ut poss 291 285 292 286 -- | Parse unit binding … … 295 289 -- @ 296 290 unitBinding :: LogicGraph -> AParser st UNIT_BINDING 297 unitBinding l = 298 doname <- simpleId299 300 301 return (Unit_binding name usp $ tokPos kCol)291 unitBinding l = do 292 name <- simpleId 293 kCol <- colonT 294 usp <- unitSpec l 295 return $ Unit_binding name usp $ tokPos kCol 302 296 303 297 -- | Parse an unit definition … … 310 304 unitDefn' :: LogicGraph -> SIMPLE_ID -> AParser st UNIT_DECL_DEFN 311 305 unitDefn' l name = do 312 313 314 return (Unit_defn name (item expr) $ tokPos kEqu)306 kEqu <- equalT 307 expr <- annoParser2 $ unitExpr l 308 return $ Unit_defn name (item expr) $ tokPos kEqu -
trunk/Syntax/Parse_AS_Structured.hs
r11264 r12725 19 19 , logicName 20 20 , parseMapping 21 , translation _list21 , translationList 22 22 ) where 23 23 … … 32 32 , lookupComorphism) 33 33 import Syntax.AS_Structured 34 34 35 import Common.AS_Annotation 35 36 import Common.AnnoState … … 38 39 import Common.Token 39 40 import Common.Id 41 40 42 import Text.ParserCombinators.Parsec 43 41 44 import Data.List((\\)) 45 import Control.Monad 42 46 43 47 -- | parse annotations and then still call an annotation parser 44 48 annoParser2 :: AParser st (Annoted a) -> AParser st (Annoted a) 45 annoParser2 parser = bind (\ x (Annoted y pos l r) ->46 Annoted y pos (x ++ l) r) annos parser49 annoParser2 = 50 liftM2 (\ x (Annoted y pos l r) -> Annoted y pos (x ++ l) r) annos 47 51 48 52 ------------------------------------------------------------------------ … … 128 132 callSymParser :: Maybe (AParser st a) -> String -> String -> 129 133 AParser st ([a], [Token]) 130 callSymParser p name itemType = do 131 case p of 132 Nothing -> fail ("no symbol" ++itemType++ " parser for language " 133 ++ name) 134 Just pa -> pa `separatedBy` plainComma 134 callSymParser p name itemType = case p of 135 Nothing -> 136 fail $ "no symbol" ++ itemType ++ " parser for language " ++ name 137 Just pa -> separatedBy pa plainComma 135 138 136 139 parseItemsMap :: AnyLogic -> AParser st (G_symb_map_items_list, [Token]) … … 178 181 179 182 spec :: LogicGraph -> AParser st (Annoted SPEC) 180 spec l = do (sps,ps) <- annoParser2 (specA l) `separatedBy` (asKey thenS) 181 return $ case sps of 182 [sp] -> sp 183 _ -> emptyAnno (Extension sps $ catRange ps) 183 spec l = do 184 (sps,ps) <- annoParser2 (specA l) `separatedBy` asKey thenS 185 return $ case sps of 186 [sp] -> sp 187 _ -> emptyAnno (Extension sps $ catRange ps) 184 188 185 189 specA :: LogicGraph -> AParser st (Annoted SPEC) 186 specA l = do (sps,ps) <- annoParser2 (specB l) `separatedBy` (asKey andS) 187 return $ case sps of 188 [sp] -> sp 189 _ -> emptyAnno (Union sps $ catRange ps) 190 specA l = do 191 (sps,ps) <- annoParser2 (specB l) `separatedBy` asKey andS 192 return $ case sps of 193 [sp] -> sp 194 _ -> emptyAnno (Union sps $ catRange ps) 190 195 191 196 specB :: LogicGraph -> AParser st (Annoted SPEC) 192 specB l = do p1 <- asKey localS193 sp1 <- aSpec l194 p2 <- asKey withinS195 sp2 <- annoParser2 $ specB l196 return (emptyAnno $ Local_spec sp1 sp2197 198 197 specB l = do 198 p1 <- asKey localS 199 sp1 <- aSpec l 200 p2 <- asKey withinS 201 sp2 <- annoParser2 $ specB l 202 return (emptyAnno $ Local_spec sp1 sp2 $ tokPos p1 `appRange` tokPos p2) 203 <|> specC l 199 204 200 205 specC :: LogicGraph -> AParser st (Annoted SPEC) 201 206 specC lG = do 202 207 let spD = annoParser $ specD lG 203 rest = spD >>= translation _list lG Translation Reduction208 rest = spD >>= translationList lG Translation Reduction 204 209 l@(Logic lid) <- lookupCurrentLogic "specC" lG 205 210 -- if the current logic has an associated data_logic, … … 217 222 <|> rest 218 223 219 translation_list :: LogicGraph -> (Annoted b -> RENAMING -> b) 220 -> (Annoted b -> RESTRICTION -> b) -> Annoted b 221 -> AParser st (Annoted b) 222 translation_list l ftrans frestr sp = 224 translationList :: LogicGraph -> (Annoted b -> RENAMING -> b) 225 -> (Annoted b -> RESTRICTION -> b) -> Annoted b -> AParser st (Annoted b) 226 translationList l ftrans frestr sp = 223 227 do sp' <- translation l sp ftrans frestr 224 translation _list l ftrans frestr (emptyAnno sp')225 <|> return sp228 translationList l ftrans frestr (emptyAnno sp') 229 <|> return sp 226 230 227 231 -- | Parse renaming … … 265 269 266 270 groupSpecLookhead :: AParser st Token 267 groupSpecLookhead = oBraceT <|> ((simpleId << annos) 268 `followedWith` 269 (asKey withS <|> asKey hideS 270 <|> asKey revealS <|> asKey andS 271 <|> asKey thenS <|> cBraceT 272 <|> asKey fitS <|> asKey viewS 273 <|> asKey specS <|> asKey archS 274 <|> asKey unitS 275 <|> asKey withinS <|> asKey endS 276 <|> oBracketT <|> cBracketT 277 <|> (eof >> return (Token "" nullRange)))) 271 groupSpecLookhead = oBraceT <|> followedWith (simpleId << annos) 272 (asKey withS <|> asKey hideS <|> asKey revealS <|> asKey andS 273 <|> asKey thenS <|> cBraceT <|> asKey fitS <|> asKey viewS 274 <|> asKey specS <|> asKey archS <|> asKey unitS <|> asKey withinS 275 <|> asKey endS <|> oBracketT <|> cBracketT 276 <|> (eof >> return (Token "" nullRange))) 278 277 279 278 specD :: LogicGraph -> AParser st SPEC … … 293 292 specE l = logicSpec l 294 293 <|> (lookAhead groupSpecLookhead >> groupSpec l) 295 <|> do 296 nl <- lookupCurrentLogic "basic spec" l 297 basicSpec nl 294 <|> (lookupCurrentLogic "basic spec" l >>= basicSpec) 298 295 299 296 -- | call a logic specific parser if it exists 300 297 callParser :: Maybe (AParser st a) -> String -> String -> AParser st a 301 callParser p name itemType = do 302 case p of 303 Nothing -> fail ("no "++itemType++" parser for language " 304 ++ name) 305 Just pa -> pa 298 callParser p name itemType = case p of 299 Nothing -> fail $ "no "++ itemType ++ " parser for language " ++ name 300 Just pa -> pa 306 301 307 302 basicSpec :: AnyLogic -> AParser st SPEC … … 330 325 331 326 aSpec :: LogicGraph -> AParser st (Annoted SPEC) 332 aSpec l = annoParser2 (spec l)327 aSpec = annoParser2 . spec 333 328 334 329 groupSpec :: LogicGraph -> AParser st SPEC
