Description : parser for an Isabelle theory
Copyright : (c) C. Maeder and Uni Bremen 2005-2006
Maintainer : Christian.Maeder@dfki.de
parse the outer syntax of an Isabelle theory file. The syntax is taken from
, compatibleBodies) where
latin = single letter <?> "latin"
greek = string "\\<" <++>
option "" (string "^") -- isup
<++> many1 letter <++> string ">" <?> "greek"
isaLetter :: Parser String
isaLetter = latin <|> greek
quasiletter :: Parser String
quasiletter = single (digit <|> prime <|> char '_' ) <|> isaLetter
restident :: Parser String
restident = flat (many quasiletter)
ident = isaLetter <++> restident
longident :: Parser String
longident = ident <++> flat (many $ char '.' <:> ident)
symident :: Parser String
symident = many1 (oneOf "!#$&*+-/:<=>?@^_|~" <?> "sym") <|> greek
isaString :: Parser String
isaString = enclosedBy (flat $ many (single (noneOf "\\\"")
<|> char '\\' <:> single anyChar))
verbatim :: Parser String
verbatim = plainBlock "{*" "*}"
nestComment :: Parser String
nestComment = nestedComment "(*" "*)"
nat = many1 digit <?> "nat"
name = ident <|> symident <|> isaString <|> nat
nameref :: Parser String -- sort
nameref = longident <|> symident <|> isaString <|> nat
isaText = nameref <|> verbatim
typefree :: Parser String
typefree = prime <:> ident
indexsuffix :: Parser String
indexsuffix = option "" (char '.' <:> nat)
typevar = try (string "?'") <++> ident <++> option "" (char '.' <:> nat)
typeP = lexP typefree <|> lexP typevar <|> namerefP
var = try (char '?' <:> isaLetter) <++> restident <++> indexsuffix
term :: Parser String -- prop
isaSkip = skipMany (many1 space <|> nestComment <?> "")
lexP :: Parser String -> Parser Token
lexP pa = bind (\ p s -> Token s (Range [p])) getPos $ pa << isaSkip
lexS :: String -> Parser String
lexS s = try (string s) << isaSkip
headerP = lexS headerS >> lexP isaText
nameP = lexP $ reserved isaKeywords name
namerefP = lexP $ reserved isaKeywords nameref
parname = lexS "(" >> lexP name << lexS ")"
-- | the theory part before and including the begin keyword with a context
data TheoryHead = TheoryHead
theoryHead :: Parser TheoryHead
option Nothing $ fmap Just headerP
is <- option [] (lexS importsS >> many nameP)
us <- option [] (lexS usesS >> many (nameP <|> parname))
oc <- option Nothing $ fmap Just nameP
return $ TheoryHead th is us oc
commalist :: Parser a -> Parser [a]
commalist p = fmap fst $ p `separatedBy` lexS ","
parensP :: Parser a -> Parser a
bracketsP :: Parser a -> Parser a
bracesP :: Parser a -> Parser a
recordP :: Parser a -> Parser a
locale = forget . parensP $ lexS "in" >> nameP
markupP = choice (map lexS markups) >> option () locale >> lexP isaText
infixP = forget $ choice (map lexS ["infix", "infixl", "infixr"])
>> option () (forget $ lexP isaString) >> lexP nat
mixfixSuffix :: Parser ()
mixfixSuffix = forget $ lexP isaString
>> option [] (bracketsP $ commalist $ lexP nat)
>> option () (forget $ lexP nat)
structureL = forget $ lexS structureS
genMixfix :: Bool -> Parser ()
(if b then id else (<|> structureL)) $
infixP <|> mixfixSuffix <|> (lexS "binder" >> mixfixSuffix)
atom = var <|> typefree <|> typevar <|> nameref
-- nameref covers nat and symident keywords
-- | look for the simp attribute
attributes :: Parser [Bool]
attributes = bracketsP . commalist $
bind (\ n l -> null l && show n == simpS) namerefP args
lessOrEq :: Parser String
lessOrEq = lexS "<" <|> lexS "\\<subseteq>"
classdecl :: Parser [Token]
classes = forget $ lexS classesS >> many1 classdecl
data Typespec = Typespec Token [Token]
typespec :: Parser Typespec
typespec = fmap (\ n -> Typespec n []) namerefP <|> do
ns <- parensP (commalist typefreeP) <|> fmap (:[]) typefreeP
where typefreeP = lexP typefree
optinfix = option () $ parensP infixP
types :: Parser [Typespec]
types = lexS typesS >> many1 (typespec << (lexS "=" >> typeP >> optinfix))
typedecl :: Parser [Typespec]
typedecl = lexS typedeclS >> many1 (typespec << optinfix)
arity = fmap (:[]) namerefP <|> do
ns <- parensP $ commalist namerefP
data Const = Const Token Token
typeSuffix :: Parser Token
typeSuffix = lexS "::" >> typeP
consts = lexS constsS >> many1 (bind Const nameP (typeSuffix
vars = many1 nameP >> option () (forget typeSuffix)
andL = forget $ lexS andS
structs = parensP $ structureL << separatedBy vars andL
constdecl :: Parser [Const]
do t <- typeSuffix << option () mixfix
<|> (lexS "where" >> return [])
<|> (mixfix >> return [])
constdef = option () (forget thmdecl) << prop
constdefs :: Parser [[Const]]
constdefs = lexS constdefsS >> option () structs >>
many1 (option [] constdecl << constdef)
-- | the sentence name plus simp attribute (if True)
data SenDecl = SenDecl Token Bool
emptySen = SenDecl (mkSimpleId "") False
optAttributes :: Parser Bool
optAttributes = fmap or $ option [] attributes
axmdecl :: Parser SenDecl
axmdecl = (bind SenDecl nameP optAttributes) << lexS ":"
prop = lexP $ reserved isaKeywords term
data Axiom = Axiom SenDecl Token
axiomsP :: Parser [Axiom]
axiomsP = many1 (bind Axiom axmdecl prop)
defs = lexS defsS >> option "" (parensP $ lexS "overloaded") >>
axioms = lexS axiomsS >> axiomsP
thmbind :: Parser SenDecl
thmbind = (bind SenDecl nameP optAttributes)
<|> (attributes >> return emptySen)
selection = forget . parensP . commalist $
natP >> option () (lexS "-" >> option () (forget natP))
thmref = namerefP << (option () selection >> option [] attributes)
thmrefs :: Parser [Token]
thmdef = try $ thmbind << lexS "="
thmdecl :: Parser SenDecl
thmdecl = try $ thmbind << lexS ":"
theorems = forget $ (lexS theoremsS <|> lexS lemmasS)
>> separatedBy (option () (forget thmdef) >> thmrefs) andL
proppat = forget . parensP . many1 $ lexP term
data Goal = Goal SenDecl [Token]
props = bind Goal (option (emptySen) thmdecl)
$ many1 (prop << option () proppat)
goal = fmap fst $ separatedBy props andL
lemma = choice (map lexS [lemmaS, theoremS, corollaryS])
>> option () locale >> goal -- longgoal ignored
instanceP :: Parser Token
lexS instanceS >> namerefP << (lexS "::" << arity <|> lessOrEq << namerefP)
axclass :: Parser [Token]
axclass = lexS axclassS >> classdecl << many (axmdecl >> prop)
mltext = lexS mlS >> lexP isaText
cons = bind (:) nameP (many typeP) << option () mixfix
data Dtspec = Dtspec Typespec [[Token]]
option () $ forget $ try parname
cs <- fmap fst $ separatedBy cons $ lexS "|"
datatype :: Parser [Dtspec]
datatype = lexS datatypeS >> fmap fst (separatedBy dtspec andL)
-- allow '.' sequences in unknown parts
anyP = atom <|> many1 (char '.')
-- allow "and", etc. in unknown parts
unknown = skipMany1 $ forget (lexP $ reserved usedTopKeys anyP)
<|> forget (bracketsP rec)
where rec = commalist $ unknown <|> forget (lexP anyP)
data BodyElem = Axioms [Axiom]
ignore :: Functor f => f a -> f BodyElem
ignore = fmap $ const Ignored
theoryBody :: Parser [BodyElem]
<|> fmap Datatype datatype
<|> fmap (Consts . concat) constdefs
<|> ignore (choice (map lexS ignoredKeys) >> skipMany unknown)
data SimpValue a = SimpValue { hasSimp :: Bool, simpValue :: a }
instance Show a => Show (SimpValue a) where
show (SimpValue _ a) = show a
instance Pretty a => Pretty (SimpValue a) where
pretty (SimpValue _ a) = pretty a
instance Eq a => Eq (SimpValue a) where
SimpValue _ a == SimpValue _ b = a == b
-- | The axioms, goals, constants and data types of a theory
{ axiomsF ::
Map.Map Token (SimpValue Token)
, goalsF ::
Map.Map Token (SimpValue [Token])
, datatypesF ::
Map.Map Token ([Token], [[Token]])
addAxiom :: Axiom ->
Map.Map Token (SimpValue Token)
addAxiom (Axiom (SenDecl n b) a) m =
Map.insert n (SimpValue b a) m
addGoal :: Goal ->
Map.Map Token (SimpValue [Token])
->
Map.Map Token (SimpValue [Token])
addGoal (Goal (SenDecl n b) a) m =
Map.insert n (SimpValue b a) m
addDatatype :: Dtspec ->
Map.Map Token ([Token], [[Token]])
->
Map.Map Token ([Token], [[Token]])
addDatatype (Dtspec (Typespec n ps) a) m =
Map.insert n (ps, a) m
concatBodyElems :: BodyElem -> Body -> Body
concatBodyElems x b = case x of
Axioms l -> b { axiomsF = foldr addAxiom (axiomsF b) l }
Goals l -> b { goalsF = foldr addGoal (goalsF b) l }
Consts l -> b { constsF = foldr addConst (constsF b) l }
Datatype l -> b { datatypesF = foldr addDatatype (datatypesF b) l }
-- | parses a complete isabelle theory file, but skips
i.e. proofs
parseTheory :: Parser (TheoryHead, Body)
theoryHead (fmap (foldr concatBodyElems emptyBody) theoryBody)
{- | Check that constants and data type are unchanged and that no axioms
was added and no theorem deleted. -}
compatibleBodies :: Body -> Body -> [Diagnosis]
diffMap "axiom" LT (axiomsF b2) (axiomsF b1)
++ diffMap "constant" EQ (constsF b2) (constsF b1)
++ diffMap "datatype" EQ (datatypesF b2) (datatypesF b1)
++ diffMap "goal" GT (goalsF b2) (goalsF b1)
warnSimpAttr :: Body -> [Diagnosis]
map ( \ a -> Diag Warning
("use 'declare " ++ tokStr a
++ " [simp]' for proper Isabelle proof details") $ tokPos a)
diffMap :: (Ord a, Pretty a, PosItem a, Eq b, Show b)
map ( \ (k, a) -> mkDiag Error
(msg ++ " entry " ++ show a ++ " was changed for: ") k)
kd = if b then kd12 else kd21
in map ( \ k -> mkDiag Error
(msg ++ " entry illegally " ++
if b then "added" else "deleted") k) kd