content: --
  -- Copyright 2016, NICTA
  --
  -- This software may be distributed and modified according to the terms of
  -- the GNU General Public License version 2. Note that NO WARRANTY is provided.
  -- See "LICENSE_GPLv2.txt" for details.
  --
  -- @TAG(NICTA_GPL)
  --
  
  {-# LANGUAGE FlexibleContexts, GADTs, LambdaCase #-}
  {-# OPTIONS_GHC -fno-warn-unused-do-bind #-}
  
  module Isabelle.Parser where
  --
  -- System imports
  --
  import Control.Applicative hiding (many)
  import Control.Monad.Identity 
  import Data.Char (isSpace)
  import Data.List
  import Data.Monoid
  import qualified Text.Parsec as P
  import Text.Parsec hiding ((<|>))
  import Text.Parsec.Expr
  -- import Debug.Trace
  
  -- friends
  import Isabelle.InnerAST
  import Isabelle.OuterAST
  import Isabelle.PrettyHelper
  
  type OperatorM a = Operator String () Identity a
  
  --------------------------------------------------------------------------------
  -- Introduction
  --------------------------------------------------------------------------------
  
  --
  -- The parser is also a scanner/lexer (i.e. the tokens are just characters). Each parser is a
  -- "lexeme parser" which means it parses what it expects and any trailing white space.
  -- 
  --
  
  type ParserM a = Parsec String () a
  
  --
  -- Important: Do not nest uses of the @many@ combinator. Why? The |many| combinator cannot be
  -- applied to parsers which accept the empty string. It will cause a run-time error if it is applied
  -- to an empty string. However, @many p@ where @p@ is a parser will accept the empty string. Thus,
  -- something like @many (many p)@ will not work.
  --
  
  --------------------------------------------------------------------------------
  -- Constants
  --------------------------------------------------------------------------------
  
  --
  -- |reservedWords| is a collection of names that cannot be identifiers
  -- (i.e. be parsed by |nameL|)
  --
  -- FIXME: This is just for the "theory" language. Need to think about
  -- what comes between "begin" and "end"
  -- FIXME: Model as a data structure and then feed this data structure into @reserved@ combinator.
  --
  -- FIXME: I'm concerned that there is no notion of globally reserved words. Some words are (perhaps)
  -- reserved only at certain levels within the parse e.g. top-level parser vs. theory parser
  -- vs. definition parser
  --
  -- FIXME: Don't duplicate the names here and elsewhere. Define as one constant in one place.
  --
  reservedWords :: [String]
  reservedWords = [
    "and", "apply", "apply_end", "assumes", "begin", "by", "chapter", "class", "consts",
    "datatype", "definition", "defs", "domintros", "done", "end", "fixes", "for", "fun",
    "function", "imports", "instance", "instantiation", "is", "keywords", "lemma", "lemmas",
    "no_translations", "open", "overloaded", "primrec", "record ", "section", "sequential", "sorry",
    "subsection", "subsubsection", "termination", "text", "theorems", "theory", "translations",
    "type_synonym", "typedecl", "unchecked", "uses", "where" ]
  
  ---------------------------------------------------------------
  -- Utility functions and combinators
  -------------------------------------------------------------
  
  lift :: Monad m => (a -> b) -> m a -> m b
  lift f m = m >>= return . f
  
  concatP :: Monoid m => ParserM [m] -> ParserM m
  concatP m = m >>= return . foldl mappend mempty
  
  manyP :: Monoid m => ParserM m -> ParserM m
  manyP = concatP . many
  
  manyP1 :: Monoid m => ParserM m -> ParserM m
  manyP1 = concatP . many1
  
  mb :: ParserM a -> ParserM (Maybe a)
  mb p = option Nothing (Just <$> p)
  
  --
  -- For the sake of correctness I've decided to throw the notion of efficiency out the window and
  -- define my own "alternative" combinator that applies "try" to the first argument. With this
  -- combinator, the problem where the first parser @p@ fails, but consumes some input in the process
  -- causing parser @q@ not to succeed does not occurr.
  --
  infixr 1 <||>
  p <||> q = try $ (try p P.<|> q)
  
  --
  -- FIXME: Note the use of "try". May remove later to improve performance
  --
  infixr 5 <++>
  (<++>) :: Monoid m => ParserM m -> ParserM m -> ParserM m
  p <++> q = try $ do { x <- p; y <- q; return (x `mappend` y)  }
  
  oneStringOf :: [String] -> ParserM String
  oneStringOf [] = error "Must be applied to at least one parser"
  oneStringOf ss = foldl1 (<||>) (map string ss)
  
  parensL :: ParserM a -> ParserM a
  parensL p = do { stringL "("; r <- p; stringL ")"; return r }
  
  quotedL :: ParserM a -> ParserM a
  quotedL p = do { stringL "\""; r <- p; stringL "\""; return r }
  
  --------------------------------------------------------------------------------
  -- Primitive parsers
  --------------------------------------------------------------------------------
  
  --
  -- NOTE: The perils of lexeme parsers
  --
  -- Most of the time Parsec is used as a "scanner-less" parser library.  This means that there is no
  -- separate lexical analysis phase. i.e. the input is not tokenized.
  --
  -- The common solution is to define everything as a lexeme parser, a parser that accepts a token
  -- /and/ its trailing white space (/zero/ or more characters of it)
  --
  -- However, you don't want this behaviour for identifiers or reserved words. It's common that a
  -- name/identifier could have a reserved word as its prefex. e.g. "and" is a reserved word by "andy"
  -- isn't.
  --
  
  --
  -- In this file we have the convention that parsers ending in a 'L' are "lexeme parsers". They
  -- consume trailing whitespace.
  -- See |lexeme|
  --
  -- Parsers ending in an 'S' are parsers that are NOT lexeme parsers.
  --
  
  --
  -- @lexeme@ takes a parser @p@ and turns it into a parser that parses what @p@ does plus any
  -- trailing white space (/zero/ or more characters)
  --
  lexeme :: ParserM a -> ParserM a
  lexeme p = do { s <- p; many (satisfy isSpace); return s }
  
  importsL :: ParserM TheoryImports
  importsL = do
    reserved "imports"
    ns <- many1 nameL
    return (TheoryImports ns)
    
  --
  -- |reserved' s| expects the reserved word |s| and nothing else.
  --
  -- FIXME: Need to check that string is actually a reserved word and not a word that is longer than
  -- it e.g. "androgenous" has prefix "and".
  --
  reserved :: String -> ParserM ()
  reserved = lexeme . reservedS
    where
      reservedS :: String -> ParserM ()
      reservedS s = do { try (sequence (map char s))
                       ; notFollowedBy quasiletterS
                       ; return () } <?> ("reserved word '" ++ s ++ "'")
  
  identS :: ParserM String
  identS = letterS <++> manyP quasiletterS
  
  identL :: ParserM String
  identL = lexeme identS
  
  antiquoteS :: ParserM String 
  antiquoteS = char '$' >> lookAhead anyChar >>= \case
                 '(' -> char '(' >> hsExprL 0 ""
                 _   -> identS 
  
  hsExprL :: Int -> String -> ParserM String
  hsExprL = (lexeme .) . hsExprS
  
  hsExprS :: Int -> String -> ParserM String
  hsExprS depth s = anyChar >>= \case
              '(' -> hsExprL (depth+1) ('(':s)
              ')' | depth == 0 -> return $ reverse s
                  | otherwise  -> hsExprL (depth-1) (')':s)
              c -> hsExprL depth (c:s)
  
  antiquoteL :: ParserM String 
  antiquoteL = lexeme antiquoteS 
  
  antiquoteNameS :: ParserM String 
  antiquoteNameS = ('$':) <$> antiquoteS
  
  letterS :: ParserM String
  letterS = latinS <||> greekS
  
  latinS :: ParserM String
  latinS = s $ oneOf "abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ"
    where s = lift (:[])
  
  greekS :: ParserM String
  greekS = oneStringOf ["\\<alpha>",  "\\<beta>", "\\<gamma>", "\\<delta>",
                             "\\epsilon>", "\\<zeta>", "\\<eta>",   "\\<theta>",
                             "\\<iota>", "\\<kappa>", "\\<mu>", "\\<nu>",
                             "\\<xi>", "\\<pi>", "\\<rho>", "\\<sigma>", "\\<tau>",
                             "\\<upsilon>", "\\<phi>", "\\<chi>", "\\<psi>",
                             "\\<omega>", "\\<Gamma>", "\\<Delta>", "\\<Theta>",
                             "\\<Lambda>", "\\<Xi>", "\\<Pi>", "\\<Sigma>",
                             "\\<Upsilon>", "\\<Phi>", "\\<Psi>", "\\<Omega>" ]
  
  
  quasiletterS :: ParserM String
  quasiletterS = ((letterS <||> digitS <||> charString '_') <||> charString '\'') <?> "quasi-letter"
  
  digitS :: ParserM String
  digitS =  s $ oneOf "0123456789"
    where s = lift (:[])
  
  natS :: ParserM String
  natS = manyP1 digitS
  
  natL :: ParserM String
  natL = lexeme natS
  
  --
  -- Parses an Isabelle name
  --
  nameS :: ParserM String
  nameS = (antiquoteNameS <||> identS <||> symidentS <||> natS <||> isabelleStringS) <?> "an Isabelle name"
    where
  
  isabelleStringS = charString '"' <++> many1 (satisfy (\c -> c /= '"')) <++> charString '"'
  
  symS :: ParserM Char
  symS   = oneOf $ "!#$%&*+-/<=>?@^_|~"
      
  symidentS :: ParserM String
  symidentS = manySyms <||> (string "\\<" <++> identS <++> string ">")
    where manySyms = many1 symS
  
  
  namerefS :: ParserM String
  namerefS = longIdentS <||> nameS 
  
  namerefL :: ParserM String
  namerefL = notReservedLexeme namerefS
  
  charString :: Char -> ParserM String
  charString = lift (:[]) . char 
  
  longIdentS :: ParserM String
  longIdentS = identS <++> manyP1 (charString '.' <++> identS)
  
  --
  -- Like @lexeme@ but also checks that the thing parsed is not a reserved word.
  --
  notReservedLexeme :: ParserM String -> ParserM String
  notReservedLexeme p = lexeme . try $
    do { s <- p
       ; if s `elem` reservedWords
                then unexpected ("'" ++ s ++ "' is a reserved word")
                else return s }
  
  
  nameL :: ParserM String
  nameL = notReservedLexeme nameS
  
  
  
  --------------------------------------------------------------------------------
  -- Theory language parser
  --------------------------------------------------------------------------------
  
  --
  -- The parser presented in this section is for Isabelle's theory language.
  -- Within the 'begin' and 'end' is Isabelle's SOMETHING language.
  --
  
  type L d = d Type Term
  
  --
  -- Parser for top-level
  --
  topLevelL :: ParserM (L Theory)
  topLevelL = do
    many (satisfy isSpace)
    reserved "theory"
    n <- nameL
    imports <- importsL
    reserved "begin"
    theoryDecls <- many theoryDeclL
    reserved "end"
    return $ Theory n imports theoryDecls
    
  
  theoryDeclL :: ParserM (TheoryDecl Type Term)
  theoryDeclL = (Definition <$> definitionL) <||>
                (Abbreviation <$> abbreviationL) <||>
                (LemmaDecl <$> lemmaL) <||> 
                (LemmasDecl <$> lemmasL) <||> 
                (TypeSynonym <$> typeSynL) <||>
                (TypeDeclDecl <$> typeDeclL) <||>
                (ConstsDecl <$> constsL) <||>
                (RecordDecl <$> recordL) <||>
                (DataTypeDecl <$> datatypeL)
  
  
  definitionL :: ParserM (L Def)
  definitionL = do
    reserved "definition"
    res <- alt1 <||> alt2
    return res
  
    where
      alt1 = do
        t <- quotedTermL
        return (Def Nothing t)
      alt2 = do
        sig <- sigL
        reserved "where"
        t     <- quotedTermL
        return $ Def (Just sig) t
  
  sigL :: ParserM (Sig Type)
  sigL = do
    name  <- nameL
    stringL "::"
    mbTyp <- mb (quotedL typeL)
    return (Sig name mbTyp)
  
  abbreviationL :: ParserM (L Abbrev)
  abbreviationL = do
    mbSig <- mb sigL
    t     <- quotedTermL
    return (Abbrev mbSig t)
  
  lemmaL :: ParserM (L Lemma)
  lemmaL = do 
     reserved "lemma"
     l <- justPropsL <||> withTheoremDeclL -- order is important here
     return l
    where
      justPropsL = do
        ts <- many1 quotedTermL
        pf <- proofL
        return $ Lemma False Nothing ts pf
      withTheoremDeclL = do
        d  <- thmDeclL
        ts <- many1 quotedTermL
        pf <- proofL
        return $ Lemma False (Just d) ts pf
  
  lemmasL :: ParserM (L Lemmas)
  lemmasL = do 
     reserved "lemmas"
     name <- thmDeclL
     stringL "="
     lems <- many1 thmDeclL
     return $ Lemmas name lems
  
  typeSynL :: ParserM (L TypeSyn)
  typeSynL = do
    reserved "type_synonym"
    tyvars <- tyParamsL
    name  <- nameL
    stringL "="
    mbTyp <- quotedL typeL
    return $ TypeSyn name mbTyp tyvars
  
  typeDeclL :: ParserM (L TypeDecl)
  typeDeclL = do
    reserved "typedecl"
    tyvars <- tyParamsL
    name  <- nameL
    return $ TypeDecl name tyvars
  
  constsL :: ParserM (L Consts)
  constsL = do
    reserved "consts"
    sig <- sigL -- FIXME sigL has a maybe types, consts must have types
    return $ Consts sig
  
  recFieldL :: ParserM (L RecField)
  recFieldL = do
    name  <- nameL
    stringL "::"
    typ <- quotedL typeL
    return $ RecField name typ
  
  recordL :: ParserM (L Record)
  recordL = do
    reserved "record"
    tyvars <- tyParamsL
    name  <- nameL
    stringL "="
    fields <- many1 recFieldL
    return $ Record name fields tyvars
  
  dtConsL :: ParserM (L DTCons)
  dtConsL = do
    conName <- nameL
    conTypes <- many1 (quotedL typeL)
    return $ DTCons conName conTypes
  
  datatypeL :: ParserM (L Datatype)
  datatypeL = do
    reserved "datatype"
    tyvars <- tyParamsL
    name  <- nameL
    stringL "="
    cons <- many1 dtConsL
    return $ Datatype name cons tyvars
  
  thmDeclL :: ParserM TheoremDecl
  thmDeclL = do { d <- nameAndAttrsL <||> justNameL <||> justAttrsL; stringL ":"; return d }
             -- order is important. @justNameL@ has to come after @nameAndAttrsL@
    where
      justNameL = try $ do
        nm <- namerefL
        return $ TheoremDecl (Just nm) []
      nameAndAttrsL = try $ do
        nm <- namerefL
        attrs <- attributesL
        return $ TheoremDecl (Just nm) attrs
      justAttrsL = try $ do
        attrs <- attributesL
        return $ TheoremDecl Nothing attrs
  
  attributesL :: ParserM [Attribute]
  attributesL = do
    stringL "["
    as <- sepBy1 attributeL (stringL ",")
    stringL "]"
    return as
  
  attributeL :: ParserM Attribute
  attributeL = do
    nm   <- namerefL
    args <- option [] $ many1 nameL
    return $ Attribute nm args
    
  proofL :: ParserM Proof
  proofL = Proof <$> many1 applyMethodL <*> proofEndL
  
  proofEndL :: ParserM ProofEnd
  proofEndL = proofDoneL <||> proofSorryL
    where
      proofDoneL  = reserved "done" >> return ProofDone
      proofSorryL = reserved "sorry" >> return ProofSorry
  
  applyMethodL :: ParserM Method
  applyMethodL = do
    reserved "apply"
    methodTopLevelL
  
  --
  -- For simplicity's sake we only allow method modifiers +,?, and [n] at the top-level of an "apply".
  -- That is, there are no nested occurrences. 
  --
  methodTopLevelL = noArgsMethodL <||> bracketedMethodL 
    where
      noArgsMethodL = do
        nm <- namerefL
        return $ Method nm []
      bracketedMethodL = do
        stringL "("
        m <- methodL
        stringL ")"
        mbMM <- mb methodModifierL
        return $ case mbMM of 
          Just mm -> MethodModified m mm
          Nothing -> m 
  
  
  
  methodL = buildExpressionParser table restL
    where
      table = sortExprParserTable . mkBinOpTable methodBinOpRec MethodCompound $ [ MethodSeq, MethodOr ]
      restL = parensL methodL <||> methodWithArgsL
  
  
  
  methodWithArgsL = do
        nm   <- namerefL
        args <- many argL
        return $ Method nm args
        where
          argS = do
            n <- identS -- FIXME: What about: thm[THEN something]
            mbColon <- option "" (string ":")
            return $ n ++ mbColon
          argL = lexeme argS
  
  quotedTermL :: ParserM Term
  quotedTermL = quotedL termL
  
  methodModifierL :: ParserM MethodModifier
  methodModifierL = 
    (stringL "?" >> return MMOptional) <||>
    (stringL "+" >> return MMOneOrMore) <||>
    goalRestrictionL
    where
      goalRestrictionL = do
        stringL "["
        i <- option Nothing (read <$> natL)
        stringL "]"
        return $ MMGoalRestriction i
  
  -----------------------------------------------------------------------
  
  stringL = lexeme . string
  
  -- Precedence of type annotation operator "::"
  -- (should less than application precedence)
  typeAnnotationPrec = 90
  
  sortExprParserTable :: [(Int, OperatorM t)] -> [[OperatorM t]]
  sortExprParserTable = map (map snd) . descendingSortByPrec . groupByPrec 
    where
      infixr 5 <:$:>
      (<:$:>) :: (b -> b -> r) -> (a -> b) -> (a -> a -> r)
      f <:$:> g = \x y -> f (g x) (g y)
      -- the @flip@ makes it a descending sort.
      descendingSortByPrec = sortBy  (flip (compare <:$:> fst . head))
      groupByPrec          = groupBy ((==) <:$:> fst)
  
  mkBinOpTable :: (b -> BinOpRec) -> (b -> t -> t -> t) -> [b] -> [(Int, OperatorM t)]
  mkBinOpTable f con binOps = map binOpParser binOps
    where
      binOpParser b = (binOpRecPrec rec, Infix (do { try (stringL (binOpRecSym rec))
                                                   ; return (con b) }) (binOpRecAssoc rec))
        where
          rec = f b 
  
  
  antiquoteTermL :: ParserM Term 
  antiquoteTermL =  AntiTerm <$> antiquoteL
  
  
  --
  -- Term parser
  --
  --
  -- We are using Parsec's @buildExpressionParser@ function to handle binary operators, unary operators
  -- and, surprisingly, quantified terms.
  --
  -- The trick I have pulled with quantified terms is to treat them as
  -- unary operators.  The quantifier plus the identifiers that follow
  -- it are considered as a unary operator. (.e.g. "\<exists>x y z." is
  -- considered to be a unary operator which is applied to a term.)
  -- 
  termL :: ParserM Term
  termL = buildExpressionParser table restL
    where
      table =  sortExprParserTable $
                appParser:typedTermParser:(mkBinOpTable termBinOpRec TermBinOp binOps ++ 
                                           map quantifierParser quantifiers ++
                                           map unOpParser termUnOps)
  
      -- Think of application as an infix operator which is the empty string!
      appParser  = (termAppPrec, Infix (do { return TermApp }) AssocLeft)
      typedTermParser = (typeAnnotationPrec, Postfix (do { stringL "::"; ty <- typeL
                                                         ; return (\t -> TermWithType t ty) }))
      quantifierParser q = (quantifierPrec q, Prefix (do { try (stringL (quantifierSym q))
                                                         ; is <- many1 innerIdentL
                                                         -- note that string "." must be followed by at least one space
                                                         ; string "." 
                                                         ; many1 (satisfy isSpace)
                                                         ; return (QuantifiedTerm q is) }))
      unOpParser u = (termUnOpPrec u, Prefix (do { try (stringL (termUnOpSym u))
                                             ; return (TermUnOp u) }))
  
  
      restL =  antiquoteTermL <||> parensTermL <||> constTermL <||> (TermIdent <$> innerIdentL)
      parensTermL = parensL termL
  
  innerIdentL :: ParserM Ident
  innerIdentL = (Id <$> identL) <||> wildcardL <||> parensL typedIdentL
  
  wildcardL :: ParserM Ident
  wildcardL = do { char '_'; return Wildcard }
  
  typedIdentL :: ParserM Ident
  typedIdentL = do 
    ident <- innerIdentL
    stringL "::"
    ty <- typeL
    return $ TypedIdent ident ty
  
  typedTermL :: ParserM Term
  typedTermL = do
    t  <- termL
    stringL "::"
    ty <- typeL 
    return (TermWithType t ty)
    
  constTermL :: ParserM Term
  constTermL = ConstTerm <$> (trueL <||> falseL)  -- TODO: only support very limited forms of constants / zilinc
    where
      trueL  = stringL "True" >> return TrueC
      falseL = stringL "False" >> return FalseC
  
  antiquoteTypeL :: ParserM Type 
  antiquoteTypeL = AntiType <$> antiquoteL
  
  --
  -- Type parser
  --
  typeL :: ParserM Type
  typeL = buildExpressionParser table restL
    where
      table = [Postfix (do { s <- identL; return (\t -> TyDatatype s [t])})] : 
                (map (map toInfixR) [ [(tyTupleSym, TyTuple)], [(tyArrowSym, TyArrow)] ])
      toInfixR (s,c) = Infix (do { try (stringL s); return c }) AssocRight
      restL = antiquoteTypeL <||> parensL typeL <||> tyPrimL <||> tyVarL <||>
              multiParamDatatypeL <||> (TyDatatype <$> namerefL <*> pure [])
  
  multiParamL :: ParserM a -> ParserM [a]
  multiParamL pparser = do
    stringL "("
    t <- pparser
    stringL ","
    ts <- sepBy1 pparser (try (stringL ","))
    stringL ")"
    return (t:ts)
  
  multiParamDatatypeL = do
    ts <- multiParamL typeL
    s <- identL
    return $ TyDatatype s ts
  
  tyVarL :: ParserM Type
  tyVarL = do
    char '\''
    v <- identL -- FIXME: Could be wrong
    return $ TyVar v
  
  stripTyVar = map (\t -> let (TyVar v) = t in v)
  
  tyParamsL :: ParserM [String]
  tyParamsL = do 
    xs <- (do { s <- tyVarL ; return [s] }) <||> multiParamL tyVarL <||> return []
    return (stripTyVar xs)
  
  tyPrimL = TyPrim <$> primTypeL
  
  
  primTypeL :: ParserM PrimType
  primTypeL = foldl1 (<||>) [p "int" IntT, p "bool" BoolT, p "nat" NatT]
    where
      p s c = stringL s >> return c
  