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