Hets - the Heterogeneous Tool Set

Copyright(c) C. Maeder and Uni Bremen 2005-2006
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerChristian.Maeder@dfki.de
Stabilityprovisional
Portabilityportable
Safe HaskellNone

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

parseTheory :: Parser (TheoryHead, Body)

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

data Body

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

data TheoryHead

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

data SimpValue a

Constructors

SimpValue 

Fields

hasSimp :: Bool
 
simpValue :: a
 

Instances

Eq a => Eq (SimpValue a) 
Show a => Show (SimpValue a) 
Pretty a => Pretty (SimpValue a) 

warnSimpAttr :: Body -> [Diagnosis]

compatibleBodies :: Body -> Body -> [Diagnosis]

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