Copyright	(c) C. Maeder and Uni Bremen 2005-2006
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	portable
Safe Haskell	None

Isabelle.IsaParse

Description

parse the outer syntax of an Isabelle theory file. The syntax is taken from http://isabelle.in.tum.de/dist/Isabelle/doc/isar-ref.pdf for Isabelle2005 and is adjusted for Isabelle2011-1.

Synopsis

Documentation

parses a complete isabelle theory file, but skips i.e. proofs

The axioms, goals, constants and data types of a theory

Constructors

Body
Fields axiomsF :: Map Token (SimpValue Token) goalsF :: Map Token (SimpValue [Token]) constsF :: Map Token Token datatypesF :: Map Token ([Token], [[Token]])

Instances details

Show Body Source #
Instance details Defined in Isabelle.IsaParse Methods showsPrec :: Int -> Body -> ShowS show :: Body -> String showList :: [Body] -> ShowS

the theory part before and including the begin keyword with a context

Constructors

TheoryHead
Fields theoryname :: Token imports :: [Token] uses :: [Token] context :: Maybe Token

Instances details

Eq TheoryHead Source #
Instance details Defined in Isabelle.IsaParse Methods (==) :: TheoryHead -> TheoryHead -> Bool (/=) :: TheoryHead -> TheoryHead -> Bool

Constructors

SimpValue
Fields hasSimp :: Bool simpValue :: a

Instances details

Eq a => Eq (SimpValue a) Source #
Instance details Defined in Isabelle.IsaParse Methods (==) :: SimpValue a -> SimpValue a -> Bool (/=) :: SimpValue a -> SimpValue a -> Bool
Show a => Show (SimpValue a) Source #
Instance details Defined in Isabelle.IsaParse Methods showsPrec :: Int -> SimpValue a -> ShowS show :: SimpValue a -> String showList :: [SimpValue a] -> ShowS
Pretty a => Pretty (SimpValue a) Source #
Instance details Defined in Isabelle.IsaParse Methods pretty :: SimpValue a -> Doc Source # pretties :: [SimpValue a] -> Doc Source #

Check that constants and data type are unchanged and that no axioms was added and no theorem deleted.