{- |
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 :: Parser String
latin = ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a]
single ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
letter Parser String -> String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "latin"

{- | this is a slash and an ident in angle brackets
(not just some greek letters spelled out). -}
greek :: Parser String
greek :: Parser String
greek = String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "\\<" Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++>
         Parser String -> Parser String
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string "^") -- isup
         Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> Parser String
ident Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string ">" Parser String -> String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "greek"

isaLetter :: Parser String
isaLetter :: Parser String
isaLetter = Parser String
latin Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
greek

quasiletter :: Parser String
quasiletter :: Parser String
quasiletter = ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a]
single (ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit ParsecT String () Identity Char
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '\'' ParsecT String () Identity Char
-> ParsecT String () Identity Char
-> ParsecT String () Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '_' ) Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
isaLetter
              Parser String -> String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "quasiletter"

restident :: Parser String
restident :: Parser String
restident = ParsecT String () Identity [String] -> Parser String
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (Parser String -> ParsecT String () Identity [String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many Parser String
quasiletter)

ident :: Parser String
ident :: Parser String
ident = Parser String
isaLetter Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> Parser String
restident

longident :: Parser String
longident :: Parser String
longident = Parser String
ident Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> ParsecT String () Identity [String] -> Parser String
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (Parser String -> ParsecT String () Identity [String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (Parser String -> ParsecT String () Identity [String])
-> Parser String -> ParsecT String () Identity [String]
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.' ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> Parser String
ident)

symident :: Parser String
symident :: Parser String
symident = ParsecT String () Identity Char -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
oneOf "!#$%&*+-/<=>?@^_|~" ParsecT String () Identity Char
-> String -> ParsecT String () Identity Char
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "sym") Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
greek

strContent :: Char -> Parser String
strContent :: Char -> Parser String
strContent c :: Char
c = ParsecT String () Identity [String] -> Parser String
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (ParsecT String () Identity [String] -> Parser String)
-> ParsecT String () Identity [String] -> Parser String
forall a b. (a -> b) -> a -> b
$ Parser String -> ParsecT String () Identity [String]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a]
single (String -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m Char
noneOf (String -> ParsecT String () Identity Char)
-> String -> ParsecT String () Identity Char
forall a b. (a -> b) -> a -> b
$ Char
c Char -> String -> String
forall a. a -> [a] -> [a]
: "\\")
                                 Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '\\' ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a]
single ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
anyChar)

genString :: Char -> Parser String
genString :: Char -> Parser String
genString c :: Char
c = Parser String -> ParsecT String () Identity Char -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m a -> m [a]
enclosedBy (Char -> Parser String
strContent Char
c) (ParsecT String () Identity Char -> Parser String)
-> ParsecT String () Identity Char -> Parser String
forall a b. (a -> b) -> a -> b
$ Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char Char
c

isaString :: Parser String
isaString :: Parser String
isaString = Char -> Parser String
genString '"'

altString :: Parser String
altString :: Parser String
altString = Char -> Parser String
genString '`'

verbatim :: Parser String
verbatim :: Parser String
verbatim = String -> String -> Parser String
forall st. String -> String -> CharParser st String
plainBlock "{*" "*}"

nestComment :: Parser String
nestComment :: Parser String
nestComment = String -> String -> Parser String
forall st. String -> String -> CharParser st String
nestedComment "(*" "*)"

nat :: Parser String
nat :: Parser String
nat = ParsecT String () Identity Char -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
digit Parser String -> String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "nat"

name :: Parser String
name :: Parser String
name = Parser String
ident Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
symident Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
isaString Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
nat

nameref :: Parser String -- sort
nameref :: Parser String
nameref = Parser String
longident Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
symident Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
isaString Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
nat

isaText :: Parser String
isaText :: Parser String
isaText = Parser String
nameref Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
verbatim

typefree :: Parser String
typefree :: Parser String
typefree = Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '\'' ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> Parser String
ident

indexsuffix :: Parser String
indexsuffix :: Parser String
indexsuffix = Parser String -> Parser String
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.' ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> Parser String
nat)

typevar :: Parser String
typevar :: Parser String
typevar = String -> Parser String
forall st. String -> CharParser st String
tryString "?'" Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> Parser String
ident Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> Parser String -> Parser String
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.' ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> Parser String
nat)

typeP :: Parser Token
typeP :: Parser Token
typeP = Parser String -> Parser Token
lexP Parser String
typefree Parser Token -> Parser Token -> Parser Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String -> Parser Token
lexP Parser String
typevar Parser Token -> Parser Token -> Parser Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Token
namerefP

var :: Parser String
var :: Parser String
var = Parser String -> Parser String
forall tok st a. GenParser tok st a -> GenParser tok st a
try (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '?' ParsecT String () Identity Char -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> Parser String
isaLetter) Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> Parser String
restident Parser String -> Parser String -> Parser String
forall (m :: * -> *) a. Monad m => m [a] -> m [a] -> m [a]
<++> Parser String
indexsuffix

term :: Parser String -- prop
term :: Parser String
term = Parser String
var Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
nameref

isaSkip :: Parser ()
isaSkip :: Parser ()
isaSkip = Parser String -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany (ParsecT String () Identity Char -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String () Identity Char
forall s (m :: * -> *) u. Stream s m Char => ParsecT s u m Char
space Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
nestComment Parser String -> String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> String -> ParsecT s u m a
<?> "")

lexP :: Parser String -> Parser Token
lexP :: Parser String -> Parser Token
lexP = (Pos -> String -> Token)
-> ParsecT String () Identity Pos -> Parser String -> Parser Token
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\ p :: Pos
p s :: String
s -> String -> Range -> Token
Token String
s ([Pos] -> Range
Range [Pos
p])) ParsecT String () Identity Pos
forall tok st. GenParser tok st Pos
getPos (Parser String -> Parser Token)
-> (Parser String -> Parser String)
-> Parser String
-> Parser Token
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Parser String -> Parser () -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
isaSkip)

lexS :: String -> Parser String
lexS :: String -> Parser String
lexS = (Parser String -> Parser () -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
isaSkip) (Parser String -> Parser String)
-> (String -> Parser String) -> String -> Parser String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Parser String
forall st. String -> CharParser st String
tryString

headerP :: Parser Token
headerP :: Parser Token
headerP = String -> Parser String
lexS String
headerS Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser Token
lexP Parser String
isaText

nameP :: Parser Token
nameP :: Parser Token
nameP = Parser String -> Parser Token
lexP (Parser String -> Parser Token) -> Parser String -> Parser Token
forall a b. (a -> b) -> a -> b
$ [String] -> Parser String -> Parser String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
isaKeywords Parser String
name

namerefP :: Parser Token
namerefP :: Parser Token
namerefP = Parser String -> Parser Token
lexP (Parser String -> Parser Token) -> Parser String -> Parser Token
forall a b. (a -> b) -> a -> b
$ [String] -> Parser String -> Parser String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
isaKeywords Parser String
nameref

parname :: Parser Token
parname :: Parser Token
parname = String -> Parser String
lexS "(" Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser Token
lexP Parser String
name Parser Token -> Parser String -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< String -> Parser String
lexS ")"

-- | the theory part before and including the begin keyword with a context
data TheoryHead = TheoryHead
   { TheoryHead -> Token
theoryname :: Token
   , TheoryHead -> [Token]
imports :: [Token]
   , TheoryHead -> [Token]
uses :: [Token]
   , TheoryHead -> Maybe Token
context :: Maybe Token
   } deriving TheoryHead -> TheoryHead -> Bool
(TheoryHead -> TheoryHead -> Bool)
-> (TheoryHead -> TheoryHead -> Bool) -> Eq TheoryHead
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: TheoryHead -> TheoryHead -> Bool
$c/= :: TheoryHead -> TheoryHead -> Bool
== :: TheoryHead -> TheoryHead -> Bool
$c== :: TheoryHead -> TheoryHead -> Bool
Eq

theoryHead :: Parser TheoryHead
theoryHead :: Parser TheoryHead
theoryHead = do
    Parser ()
isaSkip
    Parser Token -> ParsecT String () Identity (Maybe Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe Parser Token
headerP
    String -> Parser String
lexS String
theoryS
    Token
th <- Parser Token
nameP
    [Token]
is <- String -> Parser String
lexS String
importsS Parser String
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> ParsecT String () Identity [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 Parser Token
nameP
    [Token]
us <- ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (String -> Parser String
lexS String
usesS Parser String
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> ParsecT String () Identity [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser Token
nameP Parser Token -> Parser Token -> Parser Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Token
parname))
    String -> Parser String
lexS String
beginS
    [Token]
us2 <- ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (String -> Parser String
lexS String
mlFileS Parser String
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> ParsecT String () Identity [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 Parser Token
nameP)
    Maybe Token
oc <- Parser Token -> ParsecT String () Identity (Maybe Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe Parser Token
nameP
    TheoryHead -> Parser TheoryHead
forall (m :: * -> *) a. Monad m => a -> m a
return (TheoryHead -> Parser TheoryHead)
-> TheoryHead -> Parser TheoryHead
forall a b. (a -> b) -> a -> b
$ Token -> [Token] -> [Token] -> Maybe Token -> TheoryHead
TheoryHead Token
th [Token]
is ([Token]
us [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
us2) Maybe Token
oc

commalist :: Parser a -> Parser [a]
commalist :: Parser a -> Parser [a]
commalist = (Parser a -> Parser String -> Parser [a])
-> Parser String -> Parser a -> Parser [a]
forall a b c. (a -> b -> c) -> b -> a -> c
flip Parser a -> Parser String -> Parser [a]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 (String -> Parser String
lexS ",")

parensP :: Parser a -> Parser a
parensP :: Parser a -> Parser a
parensP p :: Parser a
p = do
    String -> Parser String
lexS "("
    a
a <- Parser a
p
    String -> Parser String
lexS ")"
    a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

bracketsP :: Parser a -> Parser a
bracketsP :: Parser a -> Parser a
bracketsP p :: Parser a
p = do
    String -> Parser String
lexS "["
    a
a <- Parser a
p
    String -> Parser String
lexS "]"
    a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

bracesP :: Parser a -> Parser a
bracesP :: Parser a -> Parser a
bracesP p :: Parser a
p = do
    String -> Parser String
lexS "{"
    a
a <- Parser a
p
    String -> Parser String
lexS "}"
    a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

recordP :: Parser a -> Parser a
recordP :: Parser a -> Parser a
recordP p :: Parser a
p = do
    String -> Parser String
lexS "(|"
    a
a <- Parser a
p
    String -> Parser String
lexS "|)"
    a -> Parser a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a

locale :: Parser Token
locale :: Parser Token
locale = Parser Token -> Parser Token
forall a. Parser a -> Parser a
parensP (Parser Token -> Parser Token) -> Parser Token -> Parser Token
forall a b. (a -> b) -> a -> b
$ String -> Parser String
lexS "in" Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token
nameP

markupP :: Parser Token
markupP :: Parser Token
markupP = [Parser String] -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> Parser String) -> [String] -> [Parser String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Parser String
lexS [String]
markups) Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser Token
locale Parser () -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser Token
lexP Parser String
isaText

infixP :: Parser ()
infixP :: Parser ()
infixP = [Parser String] -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> Parser String) -> [String] -> [Parser String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Parser String
lexS ["infixl", "infixr", "infix"])
         Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (Parser String -> Parser Token
lexP Parser String
isaString) Parser () -> Parser Token -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser String -> Parser Token
lexP Parser String
nat

mixfixSuffix :: Parser ()
mixfixSuffix :: Parser ()
mixfixSuffix = Parser String -> Parser Token
lexP Parser String
isaString
    Parser Token
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall a. Parser a -> Parser a
bracketsP (ParsecT String () Identity [Token]
 -> ParsecT String () Identity [Token])
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall a b. (a -> b) -> a -> b
$ Parser Token -> ParsecT String () Identity [Token]
forall a. Parser a -> Parser [a]
commalist (Parser Token -> ParsecT String () Identity [Token])
-> Parser Token -> ParsecT String () Identity [Token]
forall a b. (a -> b) -> a -> b
$ Parser String -> Parser Token
lexP Parser String
nat)
           ParsecT String () Identity [Token] -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (Parser String -> Parser Token
lexP Parser String
nat)

structureL :: Parser ()
structureL :: Parser ()
structureL = Parser String -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (Parser String -> Parser ()) -> Parser String -> Parser ()
forall a b. (a -> b) -> a -> b
$ String -> Parser String
lexS String
structureS

genMixfix :: Bool -> Parser ()
genMixfix :: Bool -> Parser ()
genMixfix b :: Bool
b = Parser () -> Parser ()
forall a. Parser a -> Parser a
parensP (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$
    (if Bool
b then Parser () -> Parser ()
forall a. a -> a
id else (Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser ()
structureL)) (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$
        Parser ()
infixP Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser ()
mixfixSuffix Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser String
lexS "binder" Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
mixfixSuffix)

mixfix :: Parser ()
mixfix :: Parser ()
mixfix = Bool -> Parser ()
genMixfix Bool
False

-- ignores float that may start with "-"
atom :: Parser String
atom :: Parser String
atom = Parser String
var Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
typefree Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
typevar Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String
nameref
        -- nameref covers nat and symident keywords

arg :: Parser [Token]
arg :: ParsecT String () Identity [Token]
arg = (Token -> [Token])
-> Parser Token -> ParsecT String () Identity [Token]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: []) (Parser String -> Parser Token
lexP Parser String
atom) ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall a. Parser a -> Parser a
parensP ParsecT String () Identity [Token]
args ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall a. Parser a -> Parser a
bracketsP ParsecT String () Identity [Token]
args

args :: Parser [Token]
args :: ParsecT String () Identity [Token]
args = ParsecT String () Identity [[Token]]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat (ParsecT String () Identity [[Token]]
 -> ParsecT String () Identity [Token])
-> ParsecT String () Identity [[Token]]
-> ParsecT String () Identity [Token]
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity [Token]
-> ParsecT String () Identity [[Token]]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many ParsecT String () Identity [Token]
arg

-- | look for the simp attribute
attributes :: Parser [Bool]
attributes :: Parser [Bool]
attributes = Parser [Bool] -> Parser [Bool]
forall a. Parser a -> Parser a
bracketsP (Parser [Bool] -> Parser [Bool])
-> (Parser Bool -> Parser [Bool]) -> Parser Bool -> Parser [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser [Bool] -> Parser [Bool]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (Parser [Bool] -> Parser [Bool])
-> (Parser Bool -> Parser [Bool]) -> Parser Bool -> Parser [Bool]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser Bool -> Parser [Bool]
forall a. Parser a -> Parser [a]
commalist (Parser Bool -> Parser [Bool]) -> Parser Bool -> Parser [Bool]
forall a b. (a -> b) -> a -> b
$
             (Token -> [Token] -> Bool)
-> Parser Token
-> ParsecT String () Identity [Token]
-> Parser Bool
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 (\ n :: Token
n l :: [Token]
l -> [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
l Bool -> Bool -> Bool
&& Token -> String
forall a. Show a => a -> String
show Token
n String -> String -> Bool
forall a. Eq a => a -> a -> Bool
== String
simpS) Parser Token
namerefP ParsecT String () Identity [Token]
args

lessOrEq :: Parser String
lessOrEq :: Parser String
lessOrEq = String -> Parser String
lexS "<" Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> Parser String
lexS "\\<subseteq>"

classdecl :: Parser [Token]
classdecl :: ParsecT String () Identity [Token]
classdecl = do
    Token
n <- Parser Token
nameP
    Parser String
lessOrEq
    [Token]
ns <- Parser Token -> ParsecT String () Identity [Token]
forall a. Parser a -> Parser [a]
commalist Parser Token
namerefP
    [Token] -> ParsecT String () Identity [Token]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Token] -> ParsecT String () Identity [Token])
-> [Token] -> ParsecT String () Identity [Token]
forall a b. (a -> b) -> a -> b
$ Token
n Token -> [Token] -> [Token]
forall a. a -> [a] -> [a]
: [Token]
ns

classes :: Parser [[Token]]
classes :: ParsecT String () Identity [[Token]]
classes = String -> Parser String
lexS String
classesS Parser String
-> ParsecT String () Identity [[Token]]
-> ParsecT String () Identity [[Token]]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity [Token]
-> ParsecT String () Identity [[Token]]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ParsecT String () Identity [Token]
classdecl

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

typespec :: Parser Typespec
typespec :: Parser Typespec
typespec = Bool -> Parser Typespec
typespecSort Bool
False

typespecSort :: Bool -> Parser Typespec
typespecSort :: Bool -> Parser Typespec
typespecSort b :: Bool
b = (Token -> Typespec) -> Parser Token -> Parser Typespec
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([(Token, Maybe Token)] -> Token -> Typespec
Typespec []) Parser Token
namerefP
  Parser Typespec -> Parser Typespec -> Parser Typespec
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([(Token, Maybe Token)] -> Token -> Typespec)
-> ParsecT String () Identity [(Token, Maybe Token)]
-> Parser Token
-> Parser Typespec
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 [(Token, Maybe Token)] -> Token -> Typespec
Typespec
      (ParsecT String () Identity [(Token, Maybe Token)]
-> ParsecT String () Identity [(Token, Maybe Token)]
forall a. Parser a -> Parser a
parensP (Parser (Token, Maybe Token)
-> ParsecT String () Identity [(Token, Maybe Token)]
forall a. Parser a -> Parser [a]
commalist Parser (Token, Maybe Token)
typefreeP) ParsecT String () Identity [(Token, Maybe Token)]
-> ParsecT String () Identity [(Token, Maybe Token)]
-> ParsecT String () Identity [(Token, Maybe Token)]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ((Token, Maybe Token) -> [(Token, Maybe Token)])
-> Parser (Token, Maybe Token)
-> ParsecT String () Identity [(Token, Maybe Token)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Token, Maybe Token)
-> [(Token, Maybe Token)] -> [(Token, Maybe Token)]
forall a. a -> [a] -> [a]
: []) Parser (Token, Maybe Token)
typefreeP)
      Parser Token
namerefP
    where typefreeP :: Parser (Token, Maybe Token)
typefreeP = Parser Token
-> ParsecT String () Identity (Maybe Token)
-> Parser (Token, Maybe Token)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (Parser String -> Parser Token
lexP Parser String
typefree)
              (ParsecT String () Identity (Maybe Token)
 -> Parser (Token, Maybe Token))
-> ParsecT String () Identity (Maybe Token)
-> Parser (Token, Maybe Token)
forall a b. (a -> b) -> a -> b
$ if Bool
b then Parser Token -> ParsecT String () Identity (Maybe Token)
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m (Maybe a)
optionMaybe (Parser Token -> ParsecT String () Identity (Maybe Token))
-> Parser Token -> ParsecT String () Identity (Maybe Token)
forall a b. (a -> b) -> a -> b
$ String -> Parser String
lexS "::" Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token
namerefP
                else Maybe Token -> ParsecT String () Identity (Maybe Token)
forall (m :: * -> *) a. Monad m => a -> m a
return Maybe Token
forall a. Maybe a
Nothing

optinfix :: Parser ()
optinfix :: Parser ()
optinfix = Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ Parser () -> Parser ()
forall a. Parser a -> Parser a
parensP Parser ()
infixP

types :: Parser [Typespec]
types :: Parser [Typespec]
types = String -> Parser String
lexS String
typesS Parser String -> Parser [Typespec] -> Parser [Typespec]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Typespec -> Parser [Typespec]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser Typespec
typespec Parser Typespec -> Parser () -> Parser Typespec
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< (String -> Parser String
lexS "=" Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token
typeP Parser Token -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser ()
optinfix))

typedecl :: Parser [Typespec]
typedecl :: Parser [Typespec]
typedecl = String -> Parser String
lexS String
typedeclS Parser String -> Parser [Typespec] -> Parser [Typespec]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Typespec -> Parser [Typespec]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser Typespec
typespec Parser Typespec -> Parser () -> Parser Typespec
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
optinfix)

arity :: Parser ([Token], Token)
arity :: Parser ([Token], Token)
arity = (Token -> ([Token], Token))
-> Parser Token -> Parser ([Token], Token)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\ n :: Token
n -> ([], Token
n)) Parser Token
namerefP
  Parser ([Token], Token)
-> Parser ([Token], Token) -> Parser ([Token], Token)
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [Token]
-> Parser Token -> Parser ([Token], Token)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair (ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall a. Parser a -> Parser a
parensP (ParsecT String () Identity [Token]
 -> ParsecT String () Identity [Token])
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall a b. (a -> b) -> a -> b
$ Parser Token -> ParsecT String () Identity [Token]
forall a. Parser a -> Parser [a]
commalist Parser Token
namerefP) Parser Token
namerefP

data Const = Const Token Token

typeSuffix :: Parser Token
typeSuffix :: Parser Token
typeSuffix = String -> Parser String
lexS "::" Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token
typeP

consts :: Parser [Const]
consts :: Parser [Const]
consts = String -> Parser String
lexS String
constsS Parser String -> Parser [Const] -> Parser [Const]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity Const -> Parser [Const]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 ((Token -> Token -> Const)
-> Parser Token -> Parser Token -> ParsecT String () Identity Const
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Token -> Token -> Const
Const Parser Token
nameP (Parser Token
typeSuffix
                                          Parser Token -> Parser () -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser ()
mixfix))

vars :: Parser ()
vars :: Parser ()
vars = Parser Token -> ParsecT String () Identity [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 Parser Token
nameP ParsecT String () Identity [Token] -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser Token
typeSuffix

andL :: Parser String
andL :: Parser String
andL = String -> Parser String
lexS String
andS

structs :: Parser ()
structs :: Parser ()
structs = Parser () -> Parser ()
forall a. Parser a -> Parser a
parensP (Parser () -> Parser ()) -> Parser () -> Parser ()
forall a b. (a -> b) -> a -> b
$ Parser ()
structureL Parser () -> ParsecT String () Identity [()] -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser () -> Parser String -> ParsecT String () Identity [()]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 Parser ()
vars Parser String
andL

constdecl :: Parser [Const]
constdecl :: Parser [Const]
constdecl = do
    Token
n <- Parser Token
nameP
    do Token
t <- Parser Token
typeSuffix Parser Token -> Parser () -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser ()
mixfix
       [Const] -> Parser [Const]
forall (m :: * -> *) a. Monad m => a -> m a
return [Token -> Token -> Const
Const Token
n Token
t]
     Parser [Const] -> Parser [Const] -> Parser [Const]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (String -> Parser String
lexS "where" Parser String -> Parser [Const] -> Parser [Const]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Const] -> Parser [Const]
forall (m :: * -> *) a. Monad m => a -> m a
return [])
  Parser [Const] -> Parser [Const] -> Parser [Const]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Parser ()
mixfix Parser () -> Parser [Const] -> Parser [Const]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [Const] -> Parser [Const]
forall (m :: * -> *) a. Monad m => a -> m a
return [])

constdef :: Parser ()
constdef :: Parser ()
constdef = ParsecT String () Identity SenDecl -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional ParsecT String () Identity SenDecl
thmdecl Parser () -> Parser Token -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser Token
prop

constdefs :: Parser [[Const]]
constdefs :: Parser [[Const]]
constdefs = String -> Parser String
lexS String
constdefsS Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser ()
structs Parser () -> Parser [[Const]] -> Parser [[Const]]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
            Parser [Const] -> Parser [[Const]]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser [Const] -> Parser [Const]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL Parser [Const]
constdecl Parser [Const] -> Parser () -> Parser [Const]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
constdef)

-- | the sentence name plus simp attribute (if True)
data SenDecl = SenDecl Token Bool

emptySen :: SenDecl
emptySen :: SenDecl
emptySen = Token -> Bool -> SenDecl
SenDecl (String -> Token
mkSimpleId "") Bool
False

optAttributes :: Parser Bool
optAttributes :: Parser Bool
optAttributes = ([Bool] -> Bool) -> Parser [Bool] -> Parser Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
or (Parser [Bool] -> Parser Bool) -> Parser [Bool] -> Parser Bool
forall a b. (a -> b) -> a -> b
$ Parser [Bool] -> Parser [Bool]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL Parser [Bool]
attributes

axmdecl :: Parser SenDecl
axmdecl :: ParsecT String () Identity SenDecl
axmdecl = (Token -> Bool -> SenDecl)
-> Parser Token
-> Parser Bool
-> ParsecT String () Identity SenDecl
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Token -> Bool -> SenDecl
SenDecl Parser Token
nameP Parser Bool
optAttributes ParsecT String () Identity SenDecl
-> Parser String -> ParsecT String () Identity SenDecl
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< String -> Parser String
lexS ":"

prop :: Parser Token
prop :: Parser Token
prop = Parser String -> Parser Token
lexP (Parser String -> Parser Token) -> Parser String -> Parser Token
forall a b. (a -> b) -> a -> b
$ [String] -> Parser String -> Parser String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
isaKeywords Parser String
term

data Axiom = Axiom SenDecl Token

axiomP :: Parser Axiom
axiomP :: Parser Axiom
axiomP = (SenDecl -> Token -> Axiom)
-> ParsecT String () Identity SenDecl
-> Parser Token
-> Parser Axiom
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 SenDecl -> Token -> Axiom
Axiom ParsecT String () Identity SenDecl
axmdecl Parser Token
prop

axiomsP :: Parser [Axiom]
axiomsP :: Parser [Axiom]
axiomsP = Parser Axiom -> Parser [Axiom]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 Parser Axiom
axiomP

defs :: Parser [Axiom]
defs :: Parser [Axiom]
defs = String -> Parser String
lexS String
defsS Parser String -> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser String
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL (Parser String -> Parser String
forall a. Parser a -> Parser a
parensP (Parser String -> Parser String) -> Parser String -> Parser String
forall a b. (a -> b) -> a -> b
$ String -> Parser String
lexS "overloaded") Parser String -> Parser [Axiom] -> Parser [Axiom]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>>
       Parser [Axiom]
axiomsP

axioms :: Parser [Axiom]
axioms :: Parser [Axiom]
axioms = String -> Parser String
lexS String
axiomsS Parser String -> Parser [Axiom] -> Parser [Axiom]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Axiom]
axiomsP

newAxioms :: Parser [Axiom]
newAxioms :: Parser [Axiom]
newAxioms = String -> Parser String
lexS String
axiomatizationS Parser String -> Parser String -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> String -> Parser String
lexS String
whereS
   Parser String -> Parser [Axiom] -> Parser [Axiom]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Axiom -> Parser String -> Parser [Axiom]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy Parser Axiom
axiomP (String -> Parser String
lexS String
andS)

thmbind :: Parser SenDecl
thmbind :: ParsecT String () Identity SenDecl
thmbind = (Token -> Bool -> SenDecl)
-> Parser Token
-> Parser Bool
-> ParsecT String () Identity SenDecl
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 Token -> Bool -> SenDecl
SenDecl Parser Token
nameP Parser Bool
optAttributes
          ParsecT String () Identity SenDecl
-> ParsecT String () Identity SenDecl
-> ParsecT String () Identity SenDecl
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Parser [Bool]
attributes Parser [Bool]
-> ParsecT String () Identity SenDecl
-> ParsecT String () Identity SenDecl
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> SenDecl -> ParsecT String () Identity SenDecl
forall (m :: * -> *) a. Monad m => a -> m a
return SenDecl
emptySen)

selection :: Parser [()]
selection :: ParsecT String () Identity [()]
selection = ParsecT String () Identity [()] -> ParsecT String () Identity [()]
forall a. Parser a -> Parser a
parensP (ParsecT String () Identity [()]
 -> ParsecT String () Identity [()])
-> (Parser () -> ParsecT String () Identity [()])
-> Parser ()
-> ParsecT String () Identity [()]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser () -> ParsecT String () Identity [()]
forall a. Parser a -> Parser [a]
commalist (Parser () -> ParsecT String () Identity [()])
-> Parser () -> ParsecT String () Identity [()]
forall a b. (a -> b) -> a -> b
$
  Parser Token
natP Parser Token -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (String -> Parser String
lexS "-" Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser Token
natP)
  where natP :: Parser Token
natP = Parser String -> Parser Token
lexP Parser String
nat

thmref :: Parser Token
thmref :: Parser Token
thmref = ((Parser Token
namerefP Parser Token -> Parser () -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String () Identity [()] -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional ParsecT String () Identity [()]
selection) Parser Token -> Parser Token -> Parser Token
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser String -> Parser Token
lexP Parser String
altString)
          Parser Token -> Parser [Bool] -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser [Bool] -> Parser [Bool]
forall tok st a. GenParser tok st [a] -> GenParser tok st [a]
optionL Parser [Bool]
attributes

thmrefs :: Parser [Token]
thmrefs :: ParsecT String () Identity [Token]
thmrefs = ParsecT String () Identity [[Token]]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a. Monad m => m [[a]] -> m [a]
flat
  (ParsecT String () Identity [[Token]]
 -> ParsecT String () Identity [Token])
-> ParsecT String () Identity [[Token]]
-> ParsecT String () Identity [Token]
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity [Token]
-> ParsecT String () Identity [[Token]]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser Token -> ParsecT String () Identity [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a]
single Parser Token
thmref ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Bool] -> [Token])
-> Parser [Bool] -> ParsecT String () Identity [Token]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Token] -> [Bool] -> [Token]
forall a b. a -> b -> a
const []) (Parser [Bool] -> Parser [Bool]
forall a. Parser a -> Parser a
bracketsP Parser [Bool]
attributes))

thmdef :: Parser SenDecl
thmdef :: ParsecT String () Identity SenDecl
thmdef = ParsecT String () Identity SenDecl
-> ParsecT String () Identity SenDecl
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String () Identity SenDecl
 -> ParsecT String () Identity SenDecl)
-> ParsecT String () Identity SenDecl
-> ParsecT String () Identity SenDecl
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity SenDecl
thmbind ParsecT String () Identity SenDecl
-> Parser String -> ParsecT String () Identity SenDecl
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< String -> Parser String
lexS "="

thmdecl :: Parser SenDecl
thmdecl :: ParsecT String () Identity SenDecl
thmdecl = ParsecT String () Identity SenDecl
-> ParsecT String () Identity SenDecl
forall tok st a. GenParser tok st a -> GenParser tok st a
try (ParsecT String () Identity SenDecl
 -> ParsecT String () Identity SenDecl)
-> ParsecT String () Identity SenDecl
-> ParsecT String () Identity SenDecl
forall a b. (a -> b) -> a -> b
$ ParsecT String () Identity SenDecl
thmbind ParsecT String () Identity SenDecl
-> Parser String -> ParsecT String () Identity SenDecl
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< String -> Parser String
lexS ":"

theorems :: Parser [[Token]]
theorems :: ParsecT String () Identity [[Token]]
theorems = (String -> Parser String
lexS String
theoremsS Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> Parser String
lexS String
lemmasS)
    Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser Token
locale
    Parser ()
-> ParsecT String () Identity [[Token]]
-> ParsecT String () Identity [[Token]]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity [Token]
-> Parser String -> ParsecT String () Identity [[Token]]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 (ParsecT String () Identity SenDecl -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional ParsecT String () Identity SenDecl
thmdef Parser ()
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity [Token]
thmrefs) Parser String
andL

proppat :: Parser [Token]
proppat :: ParsecT String () Identity [Token]
proppat = ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall a. Parser a -> Parser a
parensP (ParsecT String () Identity [Token]
 -> ParsecT String () Identity [Token])
-> (Parser Token -> ParsecT String () Identity [Token])
-> Parser Token
-> ParsecT String () Identity [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Parser Token -> ParsecT String () Identity [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser Token -> ParsecT String () Identity [Token])
-> Parser Token -> ParsecT String () Identity [Token]
forall a b. (a -> b) -> a -> b
$ String -> Parser String
lexS "is" Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser Token
lexP Parser String
term

data Goal = Goal SenDecl [Token]

props :: Parser Goal
props :: Parser Goal
props = (SenDecl -> [Token] -> Goal)
-> ParsecT String () Identity SenDecl
-> ParsecT String () Identity [Token]
-> Parser Goal
forall (m :: * -> *) a1 a2 r.
Monad m =>
(a1 -> a2 -> r) -> m a1 -> m a2 -> m r
liftM2 SenDecl -> [Token] -> Goal
Goal (SenDecl
-> ParsecT String () Identity SenDecl
-> ParsecT String () Identity SenDecl
forall s (m :: * -> *) t a u.
Stream s m t =>
a -> ParsecT s u m a -> ParsecT s u m a
option SenDecl
emptySen ParsecT String () Identity SenDecl
thmdecl)
        (ParsecT String () Identity [Token] -> Parser Goal)
-> ParsecT String () Identity [Token] -> Parser Goal
forall a b. (a -> b) -> a -> b
$ Parser Token -> ParsecT String () Identity [Token]
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Parser Token
prop Parser Token -> Parser () -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< ParsecT String () Identity [Token] -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional ParsecT String () Identity [Token]
proppat)

goal :: Parser [Goal]
goal :: Parser [Goal]
goal = Parser Goal -> Parser String -> Parser [Goal]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 Parser Goal
props Parser String
andL

lemma :: Parser [Goal]
lemma :: Parser [Goal]
lemma = [Parser String] -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> Parser String) -> [String] -> [Parser String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Parser String
lexS [String
lemmaS, String
theoremS, String
corollaryS])
    Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser Token
locale Parser () -> Parser [Goal] -> Parser [Goal]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser [Goal]
goal -- longgoal ignored

instanceP :: Parser Token
instanceP :: Parser Token
instanceP =
    String -> Parser String
lexS String
instanceS Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token
namerefP Parser Token -> Parser String -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<<
    ((String -> Parser String
lexS "::" Parser String -> Parser ([Token], Token) -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ([Token], Token)
arity) Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> (Parser String
lessOrEq Parser String -> Parser Token -> Parser String
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser Token
namerefP))

axclass :: Parser [Token]
axclass :: ParsecT String () Identity [Token]
axclass = String -> Parser String
lexS String
axclassS Parser String
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ParsecT String () Identity [Token]
classdecl ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser Token -> ParsecT String () Identity [Token]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String () Identity SenDecl
axmdecl ParsecT String () Identity SenDecl -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Token
prop)

mltext :: Parser Token
mltext :: Parser Token
mltext = String -> Parser String
lexS String
mlS Parser String -> Parser Token -> Parser Token
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser String -> Parser Token
lexP Parser String
isaText

cons :: Parser [Token]
cons :: ParsecT String () Identity [Token]
cons = Parser Token
nameP Parser Token
-> ParsecT String () Identity [Token]
-> ParsecT String () Identity [Token]
forall (m :: * -> *) a. Monad m => m a -> m [a] -> m [a]
<:> Parser Token -> ParsecT String () Identity [Token]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many Parser Token
typeP ParsecT String () Identity [Token]
-> Parser () -> ParsecT String () Identity [Token]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser () -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional Parser ()
mixfix

data Dtspec = Dtspec Typespec [[Token]]

dtspec :: Parser Dtspec
dtspec :: Parser Dtspec
dtspec = do
    Parser Token -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
optional (Parser Token -> Parser ()) -> Parser Token -> Parser ()
forall a b. (a -> b) -> a -> b
$ Parser Token -> Parser Token
forall tok st a. GenParser tok st a -> GenParser tok st a
try Parser Token
parname
    Typespec
t <- Parser Typespec
typespec
    Parser ()
optinfix
    String -> Parser String
lexS "="
    [[Token]]
cs <- ParsecT String () Identity [Token]
-> Parser String -> ParsecT String () Identity [[Token]]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 ParsecT String () Identity [Token]
cons (Parser String -> ParsecT String () Identity [[Token]])
-> Parser String -> ParsecT String () Identity [[Token]]
forall a b. (a -> b) -> a -> b
$ String -> Parser String
lexS "|"
    Dtspec -> Parser Dtspec
forall (m :: * -> *) a. Monad m => a -> m a
return (Dtspec -> Parser Dtspec) -> Dtspec -> Parser Dtspec
forall a b. (a -> b) -> a -> b
$ Typespec -> [[Token]] -> Dtspec
Dtspec Typespec
t [[Token]]
cs

datatype :: Parser [Dtspec]
datatype :: Parser [Dtspec]
datatype = String -> Parser String
lexS String
datatypeS Parser String -> Parser [Dtspec] -> Parser [Dtspec]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser Dtspec -> Parser String -> Parser [Dtspec]
forall s (m :: * -> *) t u a sep.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m sep -> ParsecT s u m [a]
sepBy1 Parser Dtspec
dtspec Parser String
andL

-- allow '.' sequences or ":" in unknown parts
anyP :: Parser String
anyP :: Parser String
anyP = Parser String
atom Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity Char -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m [a]
many1 (Char -> ParsecT String () Identity Char
forall s (m :: * -> *) u.
Stream s m Char =>
Char -> ParsecT s u m Char
char '.') Parser String -> Parser String -> Parser String
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> String -> Parser String
forall s (m :: * -> *) u.
Stream s m Char =>
String -> ParsecT s u m String
string ":"

-- allow "and", etc. in unknown parts
unknown :: Parser ()
unknown :: Parser ()
unknown = ParsecT String () Identity [()] -> Parser ()
forall s (m :: * -> *) t u a.
Stream s m t =>
ParsecT s u m a -> ParsecT s u m ()
skipMany1 (ParsecT String () Identity [()] -> Parser ())
-> ParsecT String () Identity [()] -> Parser ()
forall a b. (a -> b) -> a -> b
$ (Parser String -> Parser Token
lexP ([String] -> Parser String -> Parser String
forall st. [String] -> CharParser st String -> CharParser st String
reserved [String]
usedTopKeys Parser String
anyP) Parser Token
-> ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> [()] -> ParsecT String () Identity [()]
forall (m :: * -> *) a. Monad m => a -> m a
return [()])
          ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [()] -> ParsecT String () Identity [()]
forall a. Parser a -> Parser a
recordP ParsecT String () Identity [()]
cus
          ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [()] -> ParsecT String () Identity [()]
forall a. Parser a -> Parser a
parensP ParsecT String () Identity [()]
cus
          ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [()] -> ParsecT String () Identity [()]
forall a. Parser a -> Parser a
bracketsP ParsecT String () Identity [()]
cus
          ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
-> ParsecT String () Identity [()]
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [()] -> ParsecT String () Identity [()]
forall a. Parser a -> Parser a
bracesP ParsecT String () Identity [()]
cus
          where cus :: ParsecT String () Identity [()]
cus = Parser () -> ParsecT String () Identity [()]
forall a. Parser a -> Parser [a]
commalist (Parser ()
unknown Parser () -> Parser () -> Parser ()
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Token -> Parser ()
forall (m :: * -> *) a. Monad m => m a -> m ()
forget (Parser String -> Parser Token
lexP Parser String
anyP))

data BodyElem = Axioms [Axiom]
              | Goals [Goal]
              | Consts [Const]
              | Datatype [Dtspec]
              | Ignored

discard :: Functor f => f a -> f BodyElem
discard :: f a -> f BodyElem
discard = (a -> BodyElem) -> f a -> f BodyElem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((a -> BodyElem) -> f a -> f BodyElem)
-> (a -> BodyElem) -> f a -> f BodyElem
forall a b. (a -> b) -> a -> b
$ BodyElem -> a -> BodyElem
forall a b. a -> b -> a
const BodyElem
Ignored

theoryBody :: Parser [BodyElem]
theoryBody :: Parser [BodyElem]
theoryBody = ParsecT String () Identity BodyElem -> Parser [BodyElem]
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m [a]
many (ParsecT String () Identity BodyElem -> Parser [BodyElem])
-> ParsecT String () Identity BodyElem -> Parser [BodyElem]
forall a b. (a -> b) -> a -> b
$
    Parser [Typespec] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard Parser [Typespec]
typedecl
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser [Typespec] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard Parser [Typespec]
types
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Dtspec] -> BodyElem)
-> Parser [Dtspec] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Dtspec] -> BodyElem
Datatype Parser [Dtspec]
datatype
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Const] -> BodyElem)
-> Parser [Const] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Const] -> BodyElem
Consts Parser [Const]
consts
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([[Const]] -> BodyElem)
-> Parser [[Const]] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ([Const] -> BodyElem
Consts ([Const] -> BodyElem)
-> ([[Const]] -> [Const]) -> [[Const]] -> BodyElem
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [[Const]] -> [Const]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat) Parser [[Const]]
constdefs
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Axiom] -> BodyElem)
-> Parser [Axiom] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Axiom] -> BodyElem
Axioms Parser [Axiom]
defs
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [[Token]]
-> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard ParsecT String () Identity [[Token]]
classes
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Token -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard Parser Token
markupP
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [[Token]]
-> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard ParsecT String () Identity [[Token]]
theorems
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Axiom] -> BodyElem)
-> Parser [Axiom] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Axiom] -> BodyElem
Axioms Parser [Axiom]
axioms
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Axiom] -> BodyElem)
-> Parser [Axiom] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Axiom] -> BodyElem
Axioms Parser [Axiom]
newAxioms
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Token -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard Parser Token
instanceP
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ([Goal] -> BodyElem)
-> Parser [Goal] -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap [Goal] -> BodyElem
Goals Parser [Goal]
lemma
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> ParsecT String () Identity [Token]
-> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard ParsecT String () Identity [Token]
axclass
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser Token -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard Parser Token
mltext
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser () -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard ([Parser String] -> Parser String
forall s (m :: * -> *) t u a.
Stream s m t =>
[ParsecT s u m a] -> ParsecT s u m a
choice ((String -> Parser String) -> [String] -> [Parser String]
forall a b. (a -> b) -> [a] -> [b]
map String -> Parser String
lexS [String]
ignoredKeys) Parser String -> Parser () -> Parser ()
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Parser () -> Parser ()
forall s u (m :: * -> *) a. ParsecT s u m a -> ParsecT s u m ()
skipMany Parser ()
unknown)
    ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
-> ParsecT String () Identity BodyElem
forall s u (m :: * -> *) a.
ParsecT s u m a -> ParsecT s u m a -> ParsecT s u m a
<|> Parser () -> ParsecT String () Identity BodyElem
forall (f :: * -> *) a. Functor f => f a -> f BodyElem
discard Parser ()
unknown

data SimpValue a = SimpValue { SimpValue a -> Bool
hasSimp :: Bool, SimpValue a -> a
simpValue :: a }

instance Show a => Show (SimpValue a) where
    show :: SimpValue a -> String
show (SimpValue _ a :: a
a) = a -> String
forall a. Show a => a -> String
show a
a

instance Pretty a => Pretty (SimpValue a) where
    pretty :: SimpValue a -> Doc
pretty (SimpValue _ a :: a
a) = a -> Doc
forall a. Pretty a => a -> Doc
pretty a
a

instance Eq a => Eq (SimpValue a) where
    SimpValue _ a :: a
a == :: SimpValue a -> SimpValue a -> Bool
== SimpValue _ b :: a
b = a
a a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
b

-- | The axioms, goals, constants and data types of a theory
data Body = Body
    { Body -> Map Token (SimpValue Token)
axiomsF :: Map.Map Token (SimpValue Token)
    , Body -> Map Token (SimpValue [Token])
goalsF :: Map.Map Token (SimpValue [Token])
    , Body -> Map Token Token
constsF :: Map.Map Token Token
    , Body -> Map Token ([Token], [[Token]])
datatypesF :: Map.Map Token ([Token], [[Token]])
    } deriving Int -> Body -> String -> String
[Body] -> String -> String
Body -> String
(Int -> Body -> String -> String)
-> (Body -> String) -> ([Body] -> String -> String) -> Show Body
forall a.
(Int -> a -> String -> String)
-> (a -> String) -> ([a] -> String -> String) -> Show a
showList :: [Body] -> String -> String
$cshowList :: [Body] -> String -> String
show :: Body -> String
$cshow :: Body -> String
showsPrec :: Int -> Body -> String -> String
$cshowsPrec :: Int -> Body -> String -> String
Show

addAxiom :: Axiom -> Map.Map Token (SimpValue Token)
         -> Map.Map Token (SimpValue Token)
addAxiom :: Axiom -> Map Token (SimpValue Token) -> Map Token (SimpValue Token)
addAxiom (Axiom (SenDecl n :: Token
n b :: Bool
b) a :: Token
a) = Token
-> SimpValue Token
-> Map Token (SimpValue Token)
-> Map Token (SimpValue Token)
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
n (Bool -> Token -> SimpValue Token
forall a. Bool -> a -> SimpValue a
SimpValue Bool
b Token
a)

addGoal :: Goal -> Map.Map Token (SimpValue [Token])
        -> Map.Map Token (SimpValue [Token])
addGoal :: Goal
-> Map Token (SimpValue [Token]) -> Map Token (SimpValue [Token])
addGoal (Goal (SenDecl n :: Token
n b :: Bool
b) a :: [Token]
a) = Token
-> SimpValue [Token]
-> Map Token (SimpValue [Token])
-> Map Token (SimpValue [Token])
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
n (Bool -> [Token] -> SimpValue [Token]
forall a. Bool -> a -> SimpValue a
SimpValue Bool
b [Token]
a)

addConst :: Const -> Map.Map Token Token -> Map.Map Token Token
addConst :: Const -> Map Token Token -> Map Token Token
addConst (Const n :: Token
n a :: Token
a) = Token -> Token -> Map Token Token -> Map Token Token
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
n Token
a

addDatatype :: Dtspec -> Map.Map Token ([Token], [[Token]])
            -> Map.Map Token ([Token], [[Token]])
addDatatype :: Dtspec
-> Map Token ([Token], [[Token]]) -> Map Token ([Token], [[Token]])
addDatatype (Dtspec (Typespec ps :: [(Token, Maybe Token)]
ps n :: Token
n) a :: [[Token]]
a) = Token
-> ([Token], [[Token]])
-> Map Token ([Token], [[Token]])
-> Map Token ([Token], [[Token]])
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Token
n (((Token, Maybe Token) -> Token)
-> [(Token, Maybe Token)] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (Token, Maybe Token) -> Token
forall a b. (a, b) -> a
fst [(Token, Maybe Token)]
ps, [[Token]]
a)

emptyBody :: Body
emptyBody :: Body
emptyBody = Body :: Map Token (SimpValue Token)
-> Map Token (SimpValue [Token])
-> Map Token Token
-> Map Token ([Token], [[Token]])
-> Body
Body
    { axiomsF :: Map Token (SimpValue Token)
axiomsF = Map Token (SimpValue Token)
forall k a. Map k a
Map.empty
    , goalsF :: Map Token (SimpValue [Token])
goalsF = Map Token (SimpValue [Token])
forall k a. Map k a
Map.empty
    , constsF :: Map Token Token
constsF = Map Token Token
forall k a. Map k a
Map.empty
    , datatypesF :: Map Token ([Token], [[Token]])
datatypesF = Map Token ([Token], [[Token]])
forall k a. Map k a
Map.empty
    }

concatBodyElems :: BodyElem -> Body -> Body
concatBodyElems :: BodyElem -> Body -> Body
concatBodyElems x :: BodyElem
x b :: Body
b = case BodyElem
x of
    Axioms l :: [Axiom]
l -> Body
b { axiomsF :: Map Token (SimpValue Token)
axiomsF = (Axiom
 -> Map Token (SimpValue Token) -> Map Token (SimpValue Token))
-> Map Token (SimpValue Token)
-> [Axiom]
-> Map Token (SimpValue Token)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Axiom -> Map Token (SimpValue Token) -> Map Token (SimpValue Token)
addAxiom (Body -> Map Token (SimpValue Token)
axiomsF Body
b) [Axiom]
l }
    Goals l :: [Goal]
l -> Body
b { goalsF :: Map Token (SimpValue [Token])
goalsF = (Goal
 -> Map Token (SimpValue [Token]) -> Map Token (SimpValue [Token]))
-> Map Token (SimpValue [Token])
-> [Goal]
-> Map Token (SimpValue [Token])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Goal
-> Map Token (SimpValue [Token]) -> Map Token (SimpValue [Token])
addGoal (Body -> Map Token (SimpValue [Token])
goalsF Body
b) [Goal]
l }
    Consts l :: [Const]
l -> Body
b { constsF :: Map Token Token
constsF = (Const -> Map Token Token -> Map Token Token)
-> Map Token Token -> [Const] -> Map Token Token
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Const -> Map Token Token -> Map Token Token
addConst (Body -> Map Token Token
constsF Body
b) [Const]
l }
    Datatype l :: [Dtspec]
l -> Body
b { datatypesF :: Map Token ([Token], [[Token]])
datatypesF = (Dtspec
 -> Map Token ([Token], [[Token]])
 -> Map Token ([Token], [[Token]]))
-> Map Token ([Token], [[Token]])
-> [Dtspec]
-> Map Token ([Token], [[Token]])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Dtspec
-> Map Token ([Token], [[Token]]) -> Map Token ([Token], [[Token]])
addDatatype (Body -> Map Token ([Token], [[Token]])
datatypesF Body
b) [Dtspec]
l }
    Ignored -> Body
b

-- | parses a complete isabelle theory file, but skips i.e. proofs
parseTheory :: Parser (TheoryHead, Body)
parseTheory :: Parser (TheoryHead, Body)
parseTheory = Parser TheoryHead
-> ParsecT String () Identity Body -> Parser (TheoryHead, Body)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m (a, b)
pair
    Parser TheoryHead
theoryHead (([BodyElem] -> Body)
-> Parser [BodyElem] -> ParsecT String () Identity Body
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((BodyElem -> Body -> Body) -> Body -> [BodyElem] -> Body
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr BodyElem -> Body -> Body
concatBodyElems Body
emptyBody) Parser [BodyElem]
theoryBody)
    Parser (TheoryHead, Body)
-> Parser String -> Parser (TheoryHead, Body)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< String -> Parser String
lexS String
endS Parser (TheoryHead, Body) -> Parser () -> Parser (TheoryHead, Body)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m a
<< Parser ()
forall s (m :: * -> *) t u.
(Stream s m t, Show t) =>
ParsecT s u m ()
eof

{- | Check that constants and data type are unchanged and that no axioms
was added and no theorem deleted. -}
compatibleBodies :: Body -> Body -> [Diagnosis]
compatibleBodies :: Body -> Body -> [Diagnosis]
compatibleBodies b1 :: Body
b1 b2 :: Body
b2 =
    String
-> Ordering
-> Map Token (SimpValue Token)
-> Map Token (SimpValue Token)
-> [Diagnosis]
forall a b.
(Ord a, Pretty a, GetRange a, Eq b, Show b) =>
String -> Ordering -> Map a b -> Map a b -> [Diagnosis]
diffMap "axiom" Ordering
LT (Body -> Map Token (SimpValue Token)
axiomsF Body
b2) (Body -> Map Token (SimpValue Token)
axiomsF Body
b1)
    [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String
-> Ordering -> Map Token Token -> Map Token Token -> [Diagnosis]
forall a b.
(Ord a, Pretty a, GetRange a, Eq b, Show b) =>
String -> Ordering -> Map a b -> Map a b -> [Diagnosis]
diffMap "constant" Ordering
EQ (Body -> Map Token Token
constsF Body
b2) (Body -> Map Token Token
constsF Body
b1)
    [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String
-> Ordering
-> Map Token ([Token], [[Token]])
-> Map Token ([Token], [[Token]])
-> [Diagnosis]
forall a b.
(Ord a, Pretty a, GetRange a, Eq b, Show b) =>
String -> Ordering -> Map a b -> Map a b -> [Diagnosis]
diffMap "datatype" Ordering
EQ (Body -> Map Token ([Token], [[Token]])
datatypesF Body
b2) (Body -> Map Token ([Token], [[Token]])
datatypesF Body
b1)
    [Diagnosis] -> [Diagnosis] -> [Diagnosis]
forall a. [a] -> [a] -> [a]
++ String
-> Ordering
-> Map Token (SimpValue [Token])
-> Map Token (SimpValue [Token])
-> [Diagnosis]
forall a b.
(Ord a, Pretty a, GetRange a, Eq b, Show b) =>
String -> Ordering -> Map a b -> Map a b -> [Diagnosis]
diffMap "goal" Ordering
GT (Body -> Map Token (SimpValue [Token])
goalsF Body
b2) (Body -> Map Token (SimpValue [Token])
goalsF Body
b1)

warnSimpAttr :: Body -> [Diagnosis]
warnSimpAttr :: Body -> [Diagnosis]
warnSimpAttr =
    (Token -> Diagnosis) -> [Token] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ( \ a :: Token
a -> DiagKind -> String -> Range -> Diagnosis
Diag DiagKind
Warning
         ("use 'declare " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
tokStr Token
a
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ " [simp]' for proper Isabelle proof details") (Range -> Diagnosis) -> Range -> Diagnosis
forall a b. (a -> b) -> a -> b
$ Token -> Range
tokPos Token
a)
        ([Token] -> [Diagnosis])
-> (Body -> [Token]) -> Body -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map Token (SimpValue Token) -> [Token]
forall k a. Map k a -> [k]
Map.keys (Map Token (SimpValue Token) -> [Token])
-> (Body -> Map Token (SimpValue Token)) -> Body -> [Token]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimpValue Token -> Bool)
-> Map Token (SimpValue Token) -> Map Token (SimpValue Token)
forall a k. (a -> Bool) -> Map k a -> Map k a
Map.filter SimpValue Token -> Bool
forall a. SimpValue a -> Bool
hasSimp (Map Token (SimpValue Token) -> Map Token (SimpValue Token))
-> (Body -> Map Token (SimpValue Token))
-> Body
-> Map Token (SimpValue Token)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Body -> Map Token (SimpValue Token)
axiomsF

diffMap :: (Ord a, Pretty a, GetRange a, Eq b, Show b)
          => String -> Ordering -> Map.Map a b -> Map.Map a b -> [Diagnosis]
diffMap :: String -> Ordering -> Map a b -> Map a b -> [Diagnosis]
diffMap msg :: String
msg o :: Ordering
o m1 :: Map a b
m1 m2 :: Map a b
m2 =
    let k1 :: [a]
k1 = Map a b -> [a]
forall k a. Map k a -> [k]
Map.keys Map a b
m1
        k2 :: [a]
k2 = Map a b -> [a]
forall k a. Map k a -> [k]
Map.keys Map a b
m2
        kd21 :: [a]
kd21 = [a]
k2 [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
k1
        kd12 :: [a]
kd12 = [a]
k1 [a] -> [a] -> [a]
forall a. Eq a => [a] -> [a] -> [a]
\\ [a]
k2
    in if [a]
k1 [a] -> [a] -> Bool
forall a. Eq a => a -> a -> Bool
== [a]
k2 then
    ((a, b) -> Diagnosis) -> [(a, b)] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map ( \ (k :: a
k, a :: b
a) -> DiagKind -> String -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
          (String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ " entry " String -> String -> String
forall a. [a] -> [a] -> [a]
++ b -> String
forall a. Show a => a -> String
show b
a String -> String -> String
forall a. [a] -> [a] -> [a]
++ " was changed for: ") a
k)
    ([(a, b)] -> [Diagnosis]) -> [(a, b)] -> [Diagnosis]
forall a b. (a -> b) -> a -> b
$ Map a b -> [(a, b)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map a b -> [(a, b)]) -> Map a b -> [(a, b)]
forall a b. (a -> b) -> a -> b
$
    (b -> b -> Maybe b) -> Map a b -> Map a b -> Map a b
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith ( \ a :: b
a b :: b
b -> if b
a b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
b then Maybe b
forall a. Maybe a
Nothing else
                                      b -> Maybe b
forall a. a -> Maybe a
Just b
a) Map a b
m1 Map a b
m2
    else let b :: Bool
b = case Ordering
o of
                   EQ -> [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [a]
kd21
                   GT -> Bool
False
                   LT -> Bool
True
             kd :: [a]
kd = if Bool
b then [a]
kd12 else [a]
kd21
               in (a -> Diagnosis) -> [a] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (DiagKind -> String -> a -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error
                      (String -> a -> Diagnosis) -> String -> a -> Diagnosis
forall a b. (a -> b) -> a -> b
$ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ " entry illegally " String -> String -> String
forall a. [a] -> [a] -> [a]
++
                         if Bool
b then "added" else "deleted") [a]
kd