{- |

Module : ./Isabelle/IsaParse.hs

Description : parser for an Isabelle theory

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

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.

-}

module Isabelle.IsaParse

( parseTheory

, Body (..)

, TheoryHead (..)

, SimpValue (..)

, warnSimpAttr

, compatibleBodies)

where

import Isabelle.IsaConsts

import Common.DocUtils

import Common.Id

import Common.Lexer

import Common.Parsec

import Common.Result

import Text.ParserCombinators.Parsec

import Control.Monad

import Data.List

import qualified Data.Map as Map

-- | should be only ascii letters

latin :: Parser String

latin = single letter <?> "latin"

{- | this is a slash and an ident in angle brackets

(not just some greek letters spelled out). -}

greek :: Parser String

greek = string "\\<" <++>

optionL (string "^") -- isup

<++> ident <++> string ">" <?> "greek"

isaLetter :: Parser String

isaLetter = latin <|> greek

quasiletter :: Parser String

quasiletter = single (digit <|> char '\'' <|> char '_' ) <|> isaLetter

<?> "quasiletter"

restident :: Parser String

restident = flat (many quasiletter)

ident :: Parser String

ident = isaLetter <++> restident

longident :: Parser String

longident = ident <++> flat (many $ char '.' <:> ident)

symident :: Parser String

symident = many1 (oneOf "!#$%&*+-/<=>?@^_|~" <?> "sym") <|> greek

strContent :: Char -> Parser String

strContent c = flat $ many (single (noneOf $ c : "\\")

<|> char '\\' <:> single anyChar)

genString :: Char -> Parser String

genString c = enclosedBy (strContent c) $ char c

isaString :: Parser String

isaString = genString '"'

altString :: Parser String

altString = genString '`'

verbatim :: Parser String

verbatim = plainBlock "{*" "*}"

nestComment :: Parser String

nestComment = nestedComment "(*" "*)"

nat :: Parser String

nat = many1 digit <?> "nat"

name :: Parser String

name = ident <|> symident <|> isaString <|> nat

nameref :: Parser String -- sort

nameref = longident <|> symident <|> isaString <|> nat

isaText :: Parser String

isaText = nameref <|> verbatim

typefree :: Parser String

typefree = char '\'' <:> ident

indexsuffix :: Parser String

indexsuffix = optionL (char '.' <:> nat)

typevar :: Parser String

typevar = tryString "?'" <++> ident <++> optionL (char '.' <:> nat)

typeP :: Parser Token

typeP = lexP typefree <|> lexP typevar <|> namerefP

var :: Parser String

var = try (char '?' <:> isaLetter) <++> restident <++> indexsuffix

term :: Parser String -- prop

term = var <|> nameref

isaSkip :: Parser ()

isaSkip = skipMany (many1 space <|> nestComment <?> "")

lexP :: Parser String -> Parser Token

lexP = liftM2 (\ p s -> Token s (Range [p])) getPos . (<< isaSkip)

lexS :: String -> Parser String

lexS = (<< isaSkip) . tryString

headerP :: Parser Token

headerP = lexS headerS >> lexP isaText

nameP :: Parser Token

nameP = lexP $ reserved isaKeywords name

namerefP :: Parser Token

namerefP = lexP $ reserved isaKeywords nameref

parname :: Parser Token

parname = lexS "(" >> lexP name << lexS ")"

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

data TheoryHead = TheoryHead

{ theoryname :: Token

, imports :: [Token]

, uses :: [Token]

, context :: Maybe Token

} deriving Eq

theoryHead :: Parser TheoryHead

theoryHead = do

isaSkip

optionMaybe headerP

lexS theoryS

th <- nameP

is <- lexS importsS >> many1 nameP

us <- optionL (lexS usesS >> many1 (nameP <|> parname))

lexS beginS

us2 <- optionL (lexS mlFileS >> many1 nameP)

oc <- optionMaybe nameP

return $ TheoryHead th is (us ++ us2) oc

commalist :: Parser a -> Parser [a]

commalist = flip sepBy1 (lexS ",")

parensP :: Parser a -> Parser a

parensP p = do

lexS "("

a <- p

lexS ")"

return a

bracketsP :: Parser a -> Parser a

bracketsP p = do

lexS "["

a <- p

lexS "]"

return a

bracesP :: Parser a -> Parser a

bracesP p = do

lexS "{"

a <- p

lexS "}"

return a

recordP :: Parser a -> Parser a

recordP p = do

lexS "(|"

a <- p

lexS "|)"

return a

locale :: Parser Token

locale = parensP $ lexS "in" >> nameP

markupP :: Parser Token

markupP = choice (map lexS markups) >> optional locale >> lexP isaText

infixP :: Parser ()

infixP = choice (map lexS ["infixl", "infixr", "infix"])

>> optional (lexP isaString) << lexP nat

mixfixSuffix :: Parser ()

mixfixSuffix = lexP isaString

>> optionL (bracketsP $ commalist $ lexP nat)

>> optional (lexP nat)

structureL :: Parser ()

structureL = forget $ lexS structureS

genMixfix :: Bool -> Parser ()

genMixfix b = parensP $

(if b then id else (<|> structureL)) $

infixP <|> mixfixSuffix <|> (lexS "binder" >> mixfixSuffix)

mixfix :: Parser ()

mixfix = genMixfix False

-- ignores float that may start with "-"

atom :: Parser String

atom = var <|> typefree <|> typevar <|> nameref

-- nameref covers nat and symident keywords

arg :: Parser [Token]

arg = fmap (: []) (lexP atom) <|> parensP args <|> bracketsP args

args :: Parser [Token]

args = flat $ many arg

-- | look for the simp attribute

attributes :: Parser [Bool]

attributes = bracketsP . optionL . commalist $

liftM2 (\ n l -> null l && show n == simpS) namerefP args

lessOrEq :: Parser String

lessOrEq = lexS "<" <|> lexS "\\<subseteq>"

classdecl :: Parser [Token]

classdecl = do

n <- nameP

lessOrEq

ns <- commalist namerefP

return $ n : ns

classes :: Parser [[Token]]

classes = lexS classesS >> many1 classdecl

data Typespec = Typespec [(Token, Maybe Token)] Token

typespec :: Parser Typespec

typespec = typespecSort False

typespecSort :: Bool -> Parser Typespec

typespecSort b = fmap (Typespec []) namerefP

<|> liftM2 Typespec

(parensP (commalist typefreeP) <|> fmap (: []) typefreeP)

namerefP

where typefreeP = pair (lexP typefree)

$ if b then optionMaybe $ lexS "::" >> namerefP

else return Nothing

optinfix :: Parser ()

optinfix = optional $ parensP infixP

types :: Parser [Typespec]

types = lexS typesS >> many1 (typespec << (lexS "=" >> typeP >> optinfix))

typedecl :: Parser [Typespec]

typedecl = lexS typedeclS >> many1 (typespec << optinfix)

arity :: Parser ([Token], Token)

arity = fmap (\ n -> ([], n)) namerefP

<|> pair (parensP $ commalist namerefP) namerefP

data Const = Const Token Token

typeSuffix :: Parser Token

typeSuffix = lexS "::" >> typeP

consts :: Parser [Const]

consts = lexS constsS >> many1 (liftM2 Const nameP (typeSuffix

<< optional mixfix))

vars :: Parser ()

vars = many1 nameP >> optional typeSuffix

andL :: Parser String

andL = lexS andS

structs :: Parser ()

structs = parensP $ structureL << sepBy1 vars andL

constdecl :: Parser [Const]

constdecl = do

n <- nameP

do t <- typeSuffix << optional mixfix

return [Const n t]

<|> (lexS "where" >> return [])

<|> (mixfix >> return [])

constdef :: Parser ()

constdef = optional thmdecl << prop

constdefs :: Parser [[Const]]

constdefs = lexS constdefsS >> optional structs >>

many1 (optionL constdecl << constdef)

-- | the sentence name plus simp attribute (if True)

data SenDecl = SenDecl Token Bool

emptySen :: SenDecl

emptySen = SenDecl (mkSimpleId "") False

optAttributes :: Parser Bool

optAttributes = fmap or $ optionL attributes

axmdecl :: Parser SenDecl

axmdecl = liftM2 SenDecl nameP optAttributes << lexS ":"

prop :: Parser Token

prop = lexP $ reserved isaKeywords term

data Axiom = Axiom SenDecl Token

axiomP :: Parser Axiom

axiomP = liftM2 Axiom axmdecl prop

axiomsP :: Parser [Axiom]

axiomsP = many1 axiomP

defs :: Parser [Axiom]

defs = lexS defsS >> optionL (parensP $ lexS "overloaded") >>

axiomsP

axioms :: Parser [Axiom]

axioms = lexS axiomsS >> axiomsP

newAxioms :: Parser [Axiom]

newAxioms = lexS axiomatizationS >> lexS whereS

>> sepBy axiomP (lexS andS)

thmbind :: Parser SenDecl

thmbind = liftM2 SenDecl nameP optAttributes

<|> (attributes >> return emptySen)

selection :: Parser [()]

selection = parensP . commalist $

natP >> optional (lexS "-" >> optional natP)

where natP = lexP nat

thmref :: Parser Token

thmref = ((namerefP << optional selection) <|> lexP altString)

<< optionL attributes

thmrefs :: Parser [Token]

thmrefs = flat

$ many1 (single thmref <|> fmap (const []) (bracketsP attributes))

thmdef :: Parser SenDecl

thmdef = try $ thmbind << lexS "="

thmdecl :: Parser SenDecl

thmdecl = try $ thmbind << lexS ":"

theorems :: Parser [[Token]]

theorems = (lexS theoremsS <|> lexS lemmasS)

>> optional locale

>> sepBy1 (optional thmdef >> thmrefs) andL

proppat :: Parser [Token]

proppat = parensP . many1 $ lexS "is" >> lexP term

data Goal = Goal SenDecl [Token]

props :: Parser Goal

props = liftM2 Goal (option emptySen thmdecl)

$ many1 (prop << optional proppat)

goal :: Parser [Goal]

goal = sepBy1 props andL

lemma :: Parser [Goal]

lemma = choice (map lexS [lemmaS, theoremS, corollaryS])

>> optional locale >> goal -- longgoal ignored

instanceP :: Parser Token

instanceP =

lexS instanceS >> namerefP <<

((lexS "::" << arity) <|> (lessOrEq << namerefP))

axclass :: Parser [Token]

axclass = lexS axclassS >> classdecl << many (axmdecl >> prop)

mltext :: Parser Token

mltext = lexS mlS >> lexP isaText

cons :: Parser [Token]

cons = nameP <:> many typeP << optional mixfix

data Dtspec = Dtspec Typespec [[Token]]

dtspec :: Parser Dtspec

dtspec = do

optional $ try parname

t <- typespec

optinfix

lexS "="

cs <- sepBy1 cons $ lexS "|"

return $ Dtspec t cs

datatype :: Parser [Dtspec]

datatype = lexS datatypeS >> sepBy1 dtspec andL

-- allow '.' sequences or ":" in unknown parts

anyP :: Parser String

anyP = atom <|> many1 (char '.') <|> string ":"

-- allow "and", etc. in unknown parts

unknown :: Parser ()

unknown = skipMany1 $ (lexP (reserved usedTopKeys anyP) >> return [()])

<|> recordP cus

<|> parensP cus

<|> bracketsP cus

<|> bracesP cus

where cus = commalist (unknown <|> forget (lexP anyP))

data BodyElem = Axioms [Axiom]

| Goals [Goal]

| Consts [Const]

| Datatype [Dtspec]

| Ignored

discard :: Functor f => f a -> f BodyElem

discard = fmap $ const Ignored

theoryBody :: Parser [BodyElem]

theoryBody = many $

discard typedecl

<|> discard types

<|> fmap Datatype datatype

<|> fmap Consts consts

<|> fmap (Consts . concat) constdefs

<|> fmap Axioms defs

<|> discard classes

<|> discard markupP

<|> discard theorems

<|> fmap Axioms axioms

<|> fmap Axioms newAxioms

<|> discard instanceP

<|> fmap Goals lemma

<|> discard axclass

<|> discard mltext

<|> discard (choice (map lexS ignoredKeys) >> skipMany unknown)

<|> discard 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

data Body = Body

{ axiomsF :: Map.Map Token (SimpValue Token)

, goalsF :: Map.Map Token (SimpValue [Token])

, constsF :: Map.Map Token Token

, datatypesF :: Map.Map Token ([Token], [[Token]])

} deriving Show

addAxiom :: Axiom -> Map.Map Token (SimpValue Token)

-> Map.Map Token (SimpValue Token)

addAxiom (Axiom (SenDecl n b) a) = Map.insert n (SimpValue b a)

addGoal :: Goal -> Map.Map Token (SimpValue [Token])

-> Map.Map Token (SimpValue [Token])

addGoal (Goal (SenDecl n b) a) = Map.insert n (SimpValue b a)

addConst :: Const -> Map.Map Token Token -> Map.Map Token Token

addConst (Const n a) = Map.insert n a

addDatatype :: Dtspec -> Map.Map Token ([Token], [[Token]])

-> Map.Map Token ([Token], [[Token]])

addDatatype (Dtspec (Typespec ps n) a) = Map.insert n (map fst ps, a)

emptyBody :: Body

emptyBody = Body

{ axiomsF = Map.empty

, goalsF = Map.empty

, constsF = Map.empty

, datatypesF = Map.empty

}

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 }

Ignored -> b

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

parseTheory :: Parser (TheoryHead, Body)

parseTheory = pair

theoryHead (fmap (foldr concatBodyElems emptyBody) theoryBody)

<< lexS endS << eof

{- | Check that constants and data type are unchanged and that no axioms

was added and no theorem deleted. -}

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

compatibleBodies b1 b2 =

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]

warnSimpAttr =

map ( \ a -> Diag Warning

("use 'declare " ++ tokStr a

++ " [simp]' for proper Isabelle proof details") $ tokPos a)

. Map.keys . Map.filter hasSimp . axiomsF

diffMap :: (Ord a, Pretty a, GetRange a, Eq b, Show b)

=> String -> Ordering -> Map.Map a b -> Map.Map a b -> [Diagnosis]

diffMap msg o m1 m2 =

let k1 = Map.keys m1

k2 = Map.keys m2

kd21 = k2 \\ k1

kd12 = k1 \\ k2

in if k1 == k2 then

map ( \ (k, a) -> mkDiag Error

(msg ++ " entry " ++ show a ++ " was changed for: ") k)

$ Map.toList $

Map.differenceWith ( \ a b -> if a == b then Nothing else

Just a) m1 m2

else let b = case o of

EQ -> null kd21

GT -> False

LT -> True

kd = if b then kd12 else kd21

in map (mkDiag Error

$ msg ++ " entry illegally " ++

if b then "added" else "deleted") kd