content: -- |
  -- Copyright   : (c) 2010-2012 Simon Meier, Benedikt Schmidt
  --               contributing in 2019: Robert Künnemann, Johannes Wocker
  -- License     : GPL v3 (see LICENSE)
  --
  -- Portability : portable
  --
  -- Parsing Proofs
  
  module Theory.Text.Parser.Proof (
      startProofSkeleton
      , diffProofSkeleton
  )
  where
  
  import           Prelude                    hiding (id, (.))
  import qualified Data.Map                   as M
  -- import           Data.Monoid                hiding (Last)
  import           Control.Applicative        hiding (empty, many, optional)
  import           Control.Category
  import           Text.Parsec                hiding ((<|>))
  import           Theory
  import           Theory.Text.Parser.Token
  import Theory.Text.Parser.Fact
  import Theory.Text.Parser.Term
  import Theory.Text.Parser.Formula
  
  -- | Parse a node premise.
  nodePrem :: Parser NodePrem
  nodePrem = parens ((,) <$> nodevar
                         <*> (comma *> fmap (PremIdx . fromIntegral) natural))
  
  -- | Parse a node conclusion.
  nodeConc :: Parser NodeConc
  nodeConc = parens ((,) <$> nodevar
                         <*> (comma *> fmap (ConcIdx . fromIntegral) natural))
  
  -- | Parse a goal.
  goal :: Parser Goal
  goal = asum
      [ stSplitGoal    
      , premiseGoal
      , actionGoal
      , chainGoal     
      , disjSplitGoal
      , eqSplitGoal
      ]
    where
      actionGoal = do
          fa <- try (fact llit <* opAt)
          i  <- nodevar
          return $ ActionG i fa
  
      premiseGoal = do
          (fa, v) <- try ((,) <$> fact llit <*> opRequires)
          i  <- nodevar
          return $ PremiseG (i, v) fa
  
      chainGoal = ChainG <$> (try (nodeConc <* opChain)) <*> nodePrem
  
      disjSplitGoal = (DisjG . Disj) <$> sepBy1 guardedFormula (symbol "∥")
  
      stSplitGoal = do
        a <- try (termp <* opSubterm)
        b <- termp
        return $ SubtermG (a, b)
          where
            termp =  msetterm False (vlit msgvar)      
  
      eqSplitGoal = try $ do
          symbol_ "splitEqs"
          parens $ (SplitG . SplitId . fromIntegral) <$> natural
  
  
  -- | Parse a proof method.
  proofMethod :: Parser ProofMethod
  proofMethod = asum
    [ symbol "sorry"         *> pure (Sorry Nothing)
    , symbol "simplify"      *> pure Simplify
    , symbol "solve"         *> (SolveGoal <$> parens goal)
    , symbol "contradiction" *> pure (Finished (Contradictory Nothing))
    , symbol "induction"     *> pure Induction
    , symbol "INVALIDATED"   *> pure Invalidated 
    , symbol "UNFINISHABLE"  *> pure (Finished Unfinishable)
    ]
  
  -- | Start parsing a proof skeleton.
  -- | If the first step of the proof is a SOLVED, mark it as an inavalid proof step.
  -- | If that is not the case, call proofSkeleton
  startProofSkeleton :: Parser ProofSkeleton
  startProofSkeleton =
      solvedProof <|> otherProof
    where
      solvedProof = symbol "SOLVED" *> error "SOLVED without a proof was found."
      otherProof = proofSkeleton
  
  -- | Parse a proof skeleton.
  proofSkeleton :: Parser ProofSkeleton
  proofSkeleton =
      solvedProof <|> finalProof <|> interProof
    where
      solvedProof =
          symbol "SOLVED" *> pure (LNode (ProofStep (Finished Solved) ()) M.empty)
  
      finalProof = do
          method <- symbol "by" *> proofMethod
          return (LNode (ProofStep method ()) M.empty)
  
      interProof = do
          method <- proofMethod
          cases  <- (sepBy oneCase (symbol "next") <* symbol "qed") <|>
                    ((return . (,) "") <$> proofSkeleton          )
          return (LNode (ProofStep method ()) (M.fromList cases))
  
      oneCase = (,) <$> (symbol "case" *> identifier) <*> proofSkeleton
  
  -- | Parse a proof method.
  diffProofMethod :: Parser DiffProofMethod
  diffProofMethod = asum
    [ symbol "sorry"            *> pure (DiffSorry Nothing)
    , symbol "rule-equivalence" *> pure DiffRuleEquivalence
    , symbol "backward-search"  *> pure DiffBackwardSearch
    , symbol "step"             *> (DiffBackwardSearchStep <$> parens proofMethod)
    , symbol "ATTACK"           *> pure DiffAttack
    , symbol "UNFINISHABLEdiff" *> pure DiffUnfinishable
    ]
  
  -- | Parse a diff proof skeleton.
  diffProofSkeleton :: Parser DiffProofSkeleton
  diffProofSkeleton =
      solvedProof <|> finalProof <|> interProof
    where
      solvedProof =
          symbol "MIRRORED" *> pure (LNode (DiffProofStep DiffMirrored ()) M.empty)
  
      finalProof = do
          method <- symbol "by" *> diffProofMethod
          return (LNode (DiffProofStep method ()) M.empty)
  
      interProof = do
          method <- diffProofMethod
          cases  <- (sepBy oneCase (symbol "next") <* symbol "qed") <|>
                    ((return . (,) "") <$> diffProofSkeleton          )
          return (LNode (DiffProofStep method ()) (M.fromList cases))
  
      oneCase = (,) <$> (symbol "case" *> identifier) <*> diffProofSkeleton
  