e1f395fef7ea8b00a675a330e5461fad35158ca5Christian MaederDescription : parser for an Isabelle theory
a3a58bbe5827eb1db384c85600748b70bc3a2021Christian MaederCopyright : (c) C. Maeder and Uni Bremen 2005-2006
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian MaederStability : provisional
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian MaederPortability : portable
a3a58bbe5827eb1db384c85600748b70bc3a2021Christian Maederparse the outer syntax of an Isabelle theory file. The syntax is taken from
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf> for Isabelle2005
730246022666619b5a47caa1f4c624da3f557a41Christian Maederand is adjusted for Isabelle2011-1.
622752e655865004756e41d39f110209dca367d0Christian Maeder ( parseTheory
622752e655865004756e41d39f110209dca367d0Christian Maeder , TheoryHead (..)
622752e655865004756e41d39f110209dca367d0Christian Maeder , SimpValue (..)
e54f9b5c61c7aa2d64474baacb76358893c93400Christian Maeder , warnSimpAttr
622752e655865004756e41d39f110209dca367d0Christian Maeder , compatibleBodies)
97279257021fd703f25019ae8869d86f455d1ea1Christian Maederimport qualified Data.Map as Map
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder-- | should be only ascii letters
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederlatin :: Parser String
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian Maederlatin = single letter <?> "latin"
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder{- | this is a slash and an ident in angle brackets
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder(not just some greek letters spelled out). -}
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedergreek :: Parser String
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maedergreek = string "\\<" <++>
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder optionL (string "^") -- isup
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <++> ident <++> string ">" <?> "greek"
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederisaLetter :: Parser String
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian MaederisaLetter = latin <|> greek
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederquasiletter :: Parser String
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maederquasiletter = single (digit <|> char '\'' <|> char '_' ) <|> isaLetter
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian Maeder <?> "quasiletter"
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederrestident :: Parser String
523389bd7ac032ec052362e93b12c5f5a6c81755Christian Maederrestident = flat (many quasiletter)
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederident :: Parser String
523389bd7ac032ec052362e93b12c5f5a6c81755Christian Maederident = isaLetter <++> restident
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederlongident :: Parser String
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian Maederlongident = ident <++> flat (many $ char '.' <:> ident)
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedersymident :: Parser String
5bb28c9e64a7bb22b426915f6b5b31aa2117c46dChristian Maedersymident = many1 (oneOf "!#$%&*+-/<=>?@^_|~" <?> "sym") <|> greek
730246022666619b5a47caa1f4c624da3f557a41Christian MaederstrContent :: Char -> Parser String
730246022666619b5a47caa1f4c624da3f557a41Christian MaederstrContent c = flat $ many (single (noneOf $ c : "\\")
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> char '\\' <:> single anyChar)
730246022666619b5a47caa1f4c624da3f557a41Christian MaedergenString :: Char -> Parser String
730246022666619b5a47caa1f4c624da3f557a41Christian MaedergenString c = enclosedBy (strContent c) $ char c
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederisaString :: Parser String
730246022666619b5a47caa1f4c624da3f557a41Christian MaederisaString = genString '"'
730246022666619b5a47caa1f4c624da3f557a41Christian MaederaltString :: Parser String
622752e655865004756e41d39f110209dca367d0Christian MaederaltString = genString '`'
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederverbatim :: Parser String
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian Maederverbatim = plainBlock "{*" "*}"
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaedernestComment :: Parser String
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian MaedernestComment = nestedComment "(*" "*)"
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedernat :: Parser String
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian Maedernat = many1 digit <?> "nat"
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedername :: Parser String
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian Maedername = ident <|> symident <|> isaString <|> nat
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedernameref :: Parser String -- sort
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian Maedernameref = longident <|> symident <|> isaString <|> nat
0324082a1ada89024a542f5d8478743b12b1924fChristian MaederisaText :: Parser String
0324082a1ada89024a542f5d8478743b12b1924fChristian MaederisaText = nameref <|> verbatim
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedertypefree :: Parser String
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maedertypefree = char '\'' <:> ident
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederindexsuffix :: Parser String
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maederindexsuffix = optionL (char '.' <:> nat)
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedertypevar :: Parser String
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maedertypevar = tryString "?'" <++> ident <++> optionL (char '.' <:> nat)
968b9a080bd93830f9c86d924b6dffa8b67e9433Christian MaedertypeP :: Parser Token
968b9a080bd93830f9c86d924b6dffa8b67e9433Christian MaedertypeP = lexP typefree <|> lexP typevar <|> namerefP
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedervar :: Parser String
523389bd7ac032ec052362e93b12c5f5a6c81755Christian Maedervar = try (char '?' <:> isaLetter) <++> restident <++> indexsuffix
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederterm :: Parser String -- prop
523389bd7ac032ec052362e93b12c5f5a6c81755Christian Maederterm = var <|> nameref
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederisaSkip :: Parser ()
75cb1ef0ccc025d57d9a54a26144c21313ff9f11Christian MaederisaSkip = skipMany (many1 space <|> nestComment <?> "")
0324082a1ada89024a542f5d8478743b12b1924fChristian MaederlexP :: Parser String -> Parser Token
97279257021fd703f25019ae8869d86f455d1ea1Christian MaederlexP = liftM2 (\ p s -> Token s (Range [p])) getPos . (<< isaSkip)
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederlexS :: String -> Parser String
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian MaederlexS = (<< isaSkip) . tryString
0324082a1ada89024a542f5d8478743b12b1924fChristian MaederheaderP :: Parser Token
0324082a1ada89024a542f5d8478743b12b1924fChristian MaederheaderP = lexS headerS >> lexP isaText
0324082a1ada89024a542f5d8478743b12b1924fChristian MaedernameP :: Parser Token
0324082a1ada89024a542f5d8478743b12b1924fChristian MaedernameP = lexP $ reserved isaKeywords name
0324082a1ada89024a542f5d8478743b12b1924fChristian MaedernamerefP :: Parser Token
0324082a1ada89024a542f5d8478743b12b1924fChristian MaedernamerefP = lexP $ reserved isaKeywords nameref
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederparname :: Parser Token
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederparname = lexS "(" >> lexP name << lexS ")"
a3a58bbe5827eb1db384c85600748b70bc3a2021Christian Maeder-- | the theory part before and including the begin keyword with a context
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maederdata TheoryHead = TheoryHead
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder { theoryname :: Token
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder , imports :: [Token]
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder , uses :: [Token]
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder , context :: Maybe Token
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder } deriving Eq
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaedertheoryHead :: Parser TheoryHead
523389bd7ac032ec052362e93b12c5f5a6c81755Christian MaedertheoryHead = do
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder optionMaybe headerP
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder is <- lexS importsS >> many1 nameP
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder us <- optionL (lexS usesS >> many1 (nameP <|> parname))
0fc370b28679137dec18ed4263e7e774a9c952cdChristian Maeder us2 <- optionL (lexS mlFileS >> many1 nameP)
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder oc <- optionMaybe nameP
0fc370b28679137dec18ed4263e7e774a9c952cdChristian Maeder return $ TheoryHead th is (us ++ us2) oc
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedercommalist :: Parser a -> Parser [a]
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maedercommalist = flip sepBy1 (lexS ",")
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederparensP :: Parser a -> Parser a
c97ea41501cc68e04648fbed17812eee014a89a0Christian MaederparensP p = do
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederbracketsP :: Parser a -> Parser a
c97ea41501cc68e04648fbed17812eee014a89a0Christian MaederbracketsP p = do
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederbracesP :: Parser a -> Parser a
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederbracesP p = do
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederrecordP :: Parser a -> Parser a
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederrecordP p = do
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederlocale :: Parser Token
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederlocale = parensP $ lexS "in" >> nameP
0324082a1ada89024a542f5d8478743b12b1924fChristian MaedermarkupP :: Parser Token
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian MaedermarkupP = choice (map lexS markups) >> optional locale >> lexP isaText
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederinfixP :: Parser ()
a81140cdef15cb5de8256e310eae035f98a054bfChristian MaederinfixP = choice (map lexS ["infixl", "infixr", "infix"])
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder >> optional (lexP isaString) << lexP nat
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaedermixfixSuffix :: Parser ()
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian MaedermixfixSuffix = lexP isaString
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder >> optionL (bracketsP $ commalist $ lexP nat)
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder >> optional (lexP nat)
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederstructureL :: Parser ()
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaederstructureL = forget $ lexS structureS
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedergenMixfix :: Bool -> Parser ()
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedergenMixfix b = parensP $
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder (if b then id else (<|> structureL)) $
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder infixP <|> mixfixSuffix <|> (lexS "binder" >> mixfixSuffix)
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedermixfix :: Parser ()
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maedermixfix = genMixfix False
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder-- ignores float that may start with "-"
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederatom :: Parser String
c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederatom = var <|> typefree <|> typevar <|> nameref
968b9a080bd93830f9c86d924b6dffa8b67e9433Christian Maeder -- nameref covers nat and symident keywords
730246022666619b5a47caa1f4c624da3f557a41Christian Maederarg :: Parser [Token]
730246022666619b5a47caa1f4c624da3f557a41Christian Maederarg = fmap (: []) (lexP atom) <|> parensP args <|> bracketsP args
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederargs :: Parser [Token]
730246022666619b5a47caa1f4c624da3f557a41Christian Maederargs = flat $ many arg
e54f9b5c61c7aa2d64474baacb76358893c93400Christian Maeder-- | look for the simp attribute
e54f9b5c61c7aa2d64474baacb76358893c93400Christian Maederattributes :: Parser [Bool]
730246022666619b5a47caa1f4c624da3f557a41Christian Maederattributes = bracketsP . optionL . commalist $
97279257021fd703f25019ae8869d86f455d1ea1Christian Maeder liftM2 (\ n l -> null l && show n == simpS) namerefP args
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederlessOrEq :: Parser String
3bff863b10da55233c3a10c389929e62ee6d221aChristian MaederlessOrEq = lexS "<" <|> lexS "\\<subseteq>"
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederclassdecl :: Parser [Token]
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maederclassdecl = do
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder ns <- commalist namerefP
c99a85b523f19594835d41ff99b22952c3c2463aChristian Maeder return $ n : ns
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederclasses :: Parser [[Token]]
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederclasses = lexS classesS >> many1 classdecl
730246022666619b5a47caa1f4c624da3f557a41Christian Maederdata Typespec = Typespec [(Token, Maybe Token)] Token
0324082a1ada89024a542f5d8478743b12b1924fChristian Maedertypespec :: Parser Typespec
730246022666619b5a47caa1f4c624da3f557a41Christian Maedertypespec = typespecSort False
730246022666619b5a47caa1f4c624da3f557a41Christian MaedertypespecSort :: Bool -> Parser Typespec
730246022666619b5a47caa1f4c624da3f557a41Christian MaedertypespecSort b = fmap (Typespec []) namerefP
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> liftM2 Typespec
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder (parensP (commalist typefreeP) <|> fmap (: []) typefreeP)
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder where typefreeP = pair (lexP typefree)
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder $ if b then optionMaybe $ lexS "::" >> namerefP
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder else return Nothing
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederoptinfix :: Parser ()
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederoptinfix = optional $ parensP infixP
0324082a1ada89024a542f5d8478743b12b1924fChristian Maedertypes :: Parser [Typespec]
968b9a080bd93830f9c86d924b6dffa8b67e9433Christian Maedertypes = lexS typesS >> many1 (typespec << (lexS "=" >> typeP >> optinfix))
0324082a1ada89024a542f5d8478743b12b1924fChristian Maedertypedecl :: Parser [Typespec]
3bff863b10da55233c3a10c389929e62ee6d221aChristian Maedertypedecl = lexS typedeclS >> many1 (typespec << optinfix)
730246022666619b5a47caa1f4c624da3f557a41Christian Maederarity :: Parser ([Token], Token)
730246022666619b5a47caa1f4c624da3f557a41Christian Maederarity = fmap (\ n -> ([], n)) namerefP
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> pair (parensP $ commalist namerefP) namerefP
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederdata Const = Const Token Token
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedertypeSuffix :: Parser Token
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian MaedertypeSuffix = lexS "::" >> typeP
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederconsts :: Parser [Const]
97279257021fd703f25019ae8869d86f455d1ea1Christian Maederconsts = lexS constsS >> many1 (liftM2 Const nameP (typeSuffix
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder << optional mixfix))
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maedervars :: Parser ()
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maedervars = many1 nameP >> optional typeSuffix
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian MaederandL :: Parser String
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian MaederandL = lexS andS
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maederstructs :: Parser ()
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederstructs = parensP $ structureL << sepBy1 vars andL
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maederconstdecl :: Parser [Const]
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maederconstdecl = do
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder do t <- typeSuffix << optional mixfix
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder return [Const n t]
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder <|> (lexS "where" >> return [])
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder <|> (mixfix >> return [])
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maederconstdef :: Parser ()
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederconstdef = optional thmdecl << prop
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maederconstdefs :: Parser [[Const]]
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederconstdefs = lexS constdefsS >> optional structs >>
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maeder many1 (optionL constdecl << constdef)
e54f9b5c61c7aa2d64474baacb76358893c93400Christian Maeder-- | the sentence name plus simp attribute (if True)
e54f9b5c61c7aa2d64474baacb76358893c93400Christian Maederdata SenDecl = SenDecl Token Bool
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian MaederemptySen :: SenDecl
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian MaederemptySen = SenDecl (mkSimpleId "") False
e54f9b5c61c7aa2d64474baacb76358893c93400Christian MaederoptAttributes :: Parser Bool
e64aab3e57d843884cd489cc3aa130120a400b05Christian MaederoptAttributes = fmap or $ optionL attributes
e54f9b5c61c7aa2d64474baacb76358893c93400Christian Maederaxmdecl :: Parser SenDecl
97279257021fd703f25019ae8869d86f455d1ea1Christian Maederaxmdecl = liftM2 SenDecl nameP optAttributes << lexS ":"
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederprop :: Parser Token
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederprop = lexP $ reserved isaKeywords term
e54f9b5c61c7aa2d64474baacb76358893c93400Christian Maederdata Axiom = Axiom SenDecl Token
622752e655865004756e41d39f110209dca367d0Christian MaederaxiomP :: Parser Axiom
622752e655865004756e41d39f110209dca367d0Christian MaederaxiomP = liftM2 Axiom axmdecl prop
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederaxiomsP :: Parser [Axiom]
622752e655865004756e41d39f110209dca367d0Christian MaederaxiomsP = many1 axiomP
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederdefs :: Parser [Axiom]
e64aab3e57d843884cd489cc3aa130120a400b05Christian Maederdefs = lexS defsS >> optionL (parensP $ lexS "overloaded") >>
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederaxioms :: Parser [Axiom]
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maederaxioms = lexS axiomsS >> axiomsP
622752e655865004756e41d39f110209dca367d0Christian MaedernewAxioms :: Parser [Axiom]
622752e655865004756e41d39f110209dca367d0Christian MaedernewAxioms = lexS axiomatizationS >> lexS whereS
622752e655865004756e41d39f110209dca367d0Christian Maeder >> sepBy axiomP (lexS andS)
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maederthmbind :: Parser SenDecl
97279257021fd703f25019ae8869d86f455d1ea1Christian Maederthmbind = liftM2 SenDecl nameP optAttributes
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maeder <|> (attributes >> return emptySen)
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederselection :: Parser [()]
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederselection = parensP . commalist $
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder natP >> optional (lexS "-" >> optional natP)
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder where natP = lexP nat
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederthmref :: Parser Token
622752e655865004756e41d39f110209dca367d0Christian Maederthmref = ((namerefP << optional selection) <|> lexP altString)
622752e655865004756e41d39f110209dca367d0Christian Maeder << optionL attributes
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederthmrefs :: Parser [Token]
730246022666619b5a47caa1f4c624da3f557a41Christian Maederthmrefs = flat
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder $ many1 (single thmref <|> fmap (const []) (bracketsP attributes))
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maederthmdef :: Parser SenDecl
3bff863b10da55233c3a10c389929e62ee6d221aChristian Maederthmdef = try $ thmbind << lexS "="
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maederthmdecl :: Parser SenDecl
3bff863b10da55233c3a10c389929e62ee6d221aChristian Maederthmdecl = try $ thmbind << lexS ":"
1589ac7d9c2687aa8f0b347d54f2bee895a8a74eChristian Maedertheorems :: Parser [[Token]]
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maedertheorems = (lexS theoremsS <|> lexS lemmasS)
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder >> optional locale
1589ac7d9c2687aa8f0b347d54f2bee895a8a74eChristian Maeder >> sepBy1 (optional thmdef >> thmrefs) andL
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederproppat :: Parser [Token]
730246022666619b5a47caa1f4c624da3f557a41Christian Maederproppat = parensP . many1 $ lexS "is" >> lexP term
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maederdata Goal = Goal SenDecl [Token]
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederprops :: Parser Goal
97279257021fd703f25019ae8869d86f455d1ea1Christian Maederprops = liftM2 Goal (option emptySen thmdecl)
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder $ many1 (prop << optional proppat)
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maedergoal :: Parser [Goal]
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maedergoal = sepBy1 props andL
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederlemma :: Parser [Goal]
3bff863b10da55233c3a10c389929e62ee6d221aChristian Maederlemma = choice (map lexS [lemmaS, theoremS, corollaryS])
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder >> optional locale >> goal -- longgoal ignored
0324082a1ada89024a542f5d8478743b12b1924fChristian MaederinstanceP :: Parser Token
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder lexS instanceS >> namerefP <<
10b02b2343246df6773585636fe3ddbefa3b6a1bChristian Maeder ((lexS "::" << arity) <|> (lessOrEq << namerefP))
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederaxclass :: Parser [Token]
de494a81b3126f87e5910b08e9b485141e1f5432Christian Maederaxclass = lexS axclassS >> classdecl << many (axmdecl >> prop)
0324082a1ada89024a542f5d8478743b12b1924fChristian Maedermltext :: Parser Token
0324082a1ada89024a542f5d8478743b12b1924fChristian Maedermltext = lexS mlS >> lexP isaText
0324082a1ada89024a542f5d8478743b12b1924fChristian Maedercons :: Parser [Token]
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maedercons = nameP <:> many typeP << optional mixfix
0324082a1ada89024a542f5d8478743b12b1924fChristian Maederdata Dtspec = Dtspec Typespec [[Token]]
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maederdtspec :: Parser Dtspec
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder optional $ try parname
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maeder t <- typespec
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder cs <- sepBy1 cons $ lexS "|"
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maeder return $ Dtspec t cs
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maederdatatype :: Parser [Dtspec]
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederdatatype = lexS datatypeS >> sepBy1 dtspec andL
5bb28c9e64a7bb22b426915f6b5b31aa2117c46dChristian Maeder-- allow '.' sequences or ":" in unknown parts
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederanyP :: Parser String
5bb28c9e64a7bb22b426915f6b5b31aa2117c46dChristian MaederanyP = atom <|> many1 (char '.') <|> string ":"
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder-- allow "and", etc. in unknown parts
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian Maederunknown :: Parser ()
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maederunknown = skipMany1 $ (lexP (reserved usedTopKeys anyP) >> return [()])
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder <|> recordP cus
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder <|> parensP cus
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder <|> bracketsP cus
d7a1e8df7455f1b5209020125bced07f7a9c5ad7Christian Maeder <|> bracesP cus
a81140cdef15cb5de8256e310eae035f98a054bfChristian Maeder where cus = commalist (unknown <|> forget (lexP anyP))
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maederdata BodyElem = Axioms [Axiom]
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder | Goals [Goal]
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder | Consts [Const]
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maeder | Datatype [Dtspec]
730246022666619b5a47caa1f4c624da3f557a41Christian Maederdiscard :: Functor f => f a -> f BodyElem
730246022666619b5a47caa1f4c624da3f557a41Christian Maederdiscard = fmap $ const Ignored
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaedertheoryBody :: Parser [BodyElem]
c97ea41501cc68e04648fbed17812eee014a89a0Christian MaedertheoryBody = many $
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder discard typedecl
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard types
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maeder <|> fmap Datatype datatype
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder <|> fmap Consts consts
5ecc14b8ff557d4af3a324be29053ec49b3bb679Christian Maeder <|> fmap (Consts . concat) constdefs
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder <|> fmap Axioms defs
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard classes
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard markupP
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard theorems
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder <|> fmap Axioms axioms
622752e655865004756e41d39f110209dca367d0Christian Maeder <|> fmap Axioms newAxioms
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard instanceP
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder <|> fmap Goals lemma
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard axclass
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard mltext
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard (choice (map lexS ignoredKeys) >> skipMany unknown)
730246022666619b5a47caa1f4c624da3f557a41Christian Maeder <|> discard unknown
95cdc09f2c2bd899d1cf0cea31e0a280e8f9d677Christian Maederdata SimpValue a = SimpValue { hasSimp :: Bool, simpValue :: a }
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maederinstance Show a => Show (SimpValue a) where
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maeder show (SimpValue _ a) = show a
95cdc09f2c2bd899d1cf0cea31e0a280e8f9d677Christian Maederinstance Pretty a => Pretty (SimpValue a) where
95cdc09f2c2bd899d1cf0cea31e0a280e8f9d677Christian Maeder pretty (SimpValue _ a) = pretty a
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maederinstance Eq a => Eq (SimpValue a) where
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maeder SimpValue _ a == SimpValue _ b = a == b
a3a58bbe5827eb1db384c85600748b70bc3a2021Christian Maeder-- | The axioms, goals, constants and data types of a theory
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maederdata Body = Body
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maeder { axiomsF :: Map.Map Token (SimpValue Token)
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maeder , goalsF :: Map.Map Token (SimpValue [Token])
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder , constsF :: Map.Map Token Token
6ce37fd27ce5eba52af160ae626aa3bfeb54729eChristian Maeder , datatypesF :: Map.Map Token ([Token], [[Token]])
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder } deriving Show
e1f395fef7ea8b00a675a330e5461fad35158ca5Christian MaederaddAxiom :: Axiom -> Map.Map Token (SimpValue Token)
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maeder -> Map.Map Token (SimpValue Token)
97279257021fd703f25019ae8869d86f455d1ea1Christian MaederaddAxiom (Axiom (SenDecl n b) a) = Map.insert n (SimpValue b a)
e1f395fef7ea8b00a675a330e5461fad35158ca5Christian MaederaddGoal :: Goal -> Map.Map Token (SimpValue [Token])
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maeder -> Map.Map Token (SimpValue [Token])
97279257021fd703f25019ae8869d86f455d1ea1Christian MaederaddGoal (Goal (SenDecl n b) a) = Map.insert n (SimpValue b a)
0324082a1ada89024a542f5d8478743b12b1924fChristian MaederaddConst :: Const -> Map.Map Token Token -> Map.Map Token Token
97279257021fd703f25019ae8869d86f455d1ea1Christian MaederaddConst (Const n a) = Map.insert n a
6ce37fd27ce5eba52af160ae626aa3bfeb54729eChristian MaederaddDatatype :: Dtspec -> Map.Map Token ([Token], [[Token]])
6ce37fd27ce5eba52af160ae626aa3bfeb54729eChristian Maeder -> Map.Map Token ([Token], [[Token]])
730246022666619b5a47caa1f4c624da3f557a41Christian MaederaddDatatype (Dtspec (Typespec ps n) a) = Map.insert n (map fst ps, a)
c97ea41501cc68e04648fbed17812eee014a89a0Christian MaederemptyBody :: Body
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederemptyBody = Body
c97ea41501cc68e04648fbed17812eee014a89a0Christian MaederconcatBodyElems :: BodyElem -> Body -> Body
c97ea41501cc68e04648fbed17812eee014a89a0Christian MaederconcatBodyElems x b = case x of
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder Axioms l -> b { axiomsF = foldr addAxiom (axiomsF b) l }
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder Goals l -> b { goalsF = foldr addGoal (goalsF b) l }
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder Consts l -> b { constsF = foldr addConst (constsF b) l }
ac53ffcb7dda01eb1faca2c4ef726b06bf7076fbChristian Maeder Datatype l -> b { datatypesF = foldr addDatatype (datatypesF b) l }
a3a58bbe5827eb1db384c85600748b70bc3a2021Christian Maeder-- | parses a complete isabelle theory file, but skips i.e. proofs
7cc5ee99644001cad8aa1ffd20411bc67f10d3e1Christian MaederparseTheory :: Parser (TheoryHead, Body)
97279257021fd703f25019ae8869d86f455d1ea1Christian MaederparseTheory = pair
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder theoryHead (fmap (foldr concatBodyElems emptyBody) theoryBody)
c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder << lexS endS << eof
a3a58bbe5827eb1db384c85600748b70bc3a2021Christian Maeder{- | Check that constants and data type are unchanged and that no axioms
a3a58bbe5827eb1db384c85600748b70bc3a2021Christian Maederwas added and no theorem deleted. -}
c97ea41501cc68e04648fbed17812eee014a89a0Christian MaedercompatibleBodies :: Body -> Body -> [Diagnosis]
99c923311eab71a85f1dcc4785d349609c828da4Christian MaedercompatibleBodies b1 b2 =
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder diffMap "axiom" LT (axiomsF b2) (axiomsF b1)
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder ++ diffMap "constant" EQ (constsF b2) (constsF b1)
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder ++ diffMap "datatype" EQ (datatypesF b2) (datatypesF b1)
57336c6fb2fb0e01cb0bcf6e3703d96e2a18c22cChristian Maeder ++ diffMap "goal" GT (goalsF b2) (goalsF b1)
e54f9b5c61c7aa2d64474baacb76358893c93400Christian MaederwarnSimpAttr :: Body -> [Diagnosis]
97279257021fd703f25019ae8869d86f455d1ea1Christian MaederwarnSimpAttr =
e1f395fef7ea8b00a675a330e5461fad35158ca5Christian Maeder map ( \ a -> Diag Warning
e1f395fef7ea8b00a675a330e5461fad35158ca5Christian Maeder ("use 'declare " ++ tokStr a
51db8ddc5236cf8f39d87bf6139cbc9aad146828Christian Maeder ++ " [simp]' for proper Isabelle proof details") $ tokPos a)
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian MaederdiffMap :: (Ord a, Pretty a, GetRange a, Eq b, Show b)
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder => String -> Ordering -> Map.Map a b -> Map.Map a b -> [Diagnosis]
6ce37fd27ce5eba52af160ae626aa3bfeb54729eChristian MaederdiffMap msg o m1 m2 =
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder kd21 = k2 \\ k1
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder kd12 = k1 \\ k2
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder in if k1 == k2 then
6ce37fd27ce5eba52af160ae626aa3bfeb54729eChristian Maeder map ( \ (k, a) -> mkDiag Error
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder (msg ++ " entry " ++ show a ++ " was changed for: ") k)
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder Map.differenceWith ( \ a b -> if a == b then Nothing else
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder Just a) m1 m2
6ce37fd27ce5eba52af160ae626aa3bfeb54729eChristian Maeder else let b = case o of
0324082a1ada89024a542f5d8478743b12b1924fChristian Maeder EQ -> null kd21
6ce37fd27ce5eba52af160ae626aa3bfeb54729eChristian Maeder kd = if b then kd12 else kd21
97279257021fd703f25019ae8869d86f455d1ea1Christian Maeder in map (mkDiag Error
97279257021fd703f25019ae8869d86f455d1ea1Christian Maeder $ msg ++ " entry illegally " ++
97279257021fd703f25019ae8869d86f455d1ea1Christian Maeder if b then "added" else "deleted") kd