{- |
Module      :  ./TIP/Prover/Common.hs
Description :  useful functions for provers with TIP input
Copyright   :  (c) Tom Kranz 2022
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :
Stability   :  experimental
Portability :  non-portable (imports TIP.AbsTIP)

These functions should be of use for any prover interfacing via the TIP format.
-}
module TIP.Prover.Common where

import TIP.AbsTIP
import TIP.Utils
import Common.ProofTree
import Common.Utils
import Interfaces.GenericATPState
import Data.Maybe (fromMaybe,maybeToList)
import qualified Data.IntMap.Strict as IM
import Control.Monad (when)
import Control.Arrow ((***),second)

data TIPQuirks = TIPQuirk
  { TIPQuirks -> Bool
noAnnotations :: Bool
  , TIPQuirks -> Bool
noPluralDatatype :: Bool
  }
noTIPQuirks :: TIPQuirks
noTIPQuirks :: TIPQuirks
noTIPQuirks = Bool -> Bool -> TIPQuirks
TIPQuirk Bool
False Bool
False

mkTheoryFileName :: String -> Decl -> String
mkTheoryFileName :: String -> Decl -> String
mkTheoryFileName theoryName :: String
theoryName goal :: Decl
goal =
  String -> String
basename (String
theoryName String -> String -> String
forall a. [a] -> [a] -> [a]
++ '_' Char -> String -> String
forall a. a -> [a] -> [a]
: String -> Maybe String -> String
forall a. a -> Maybe a -> a
fromMaybe "" (Decl -> Maybe String
getFormulaName Decl
goal) String -> String -> String
forall a. [a] -> [a] -> [a]
++ ".smt2")

makeGoal :: Decl -> Decl
makeGoal :: Decl -> Decl
makeGoal (Formula _ gAttrs :: [Attr]
gAttrs gExpr :: Expr
gExpr) = Assertion -> [Attr] -> Expr -> Decl
Formula Assertion
Prove [Attr]
gAttrs Expr
gExpr
makeGoal (FormulaPar _ gAttrs :: [Attr]
gAttrs gPar :: Par
gPar gExpr :: Expr
gExpr) = Assertion -> [Attr] -> Par -> Expr -> Decl
FormulaPar Assertion
Prove [Attr]
gAttrs Par
gPar Expr
gExpr
makeGoal d :: Decl
d = Decl
d

generateProblem :: TIPQuirks -> Start -> Maybe Decl -> (Start, IM.IntMap Int)
generateProblem :: TIPQuirks -> Start -> Maybe Decl -> (Start, IntMap Int)
generateProblem quirks :: TIPQuirks
quirks (Start decls :: [Decl]
decls) mGoal :: Maybe Decl
mGoal =
  ([Decl] -> Start
Start [Decl]
generatedDecls, IntMap Int
blame) where
    goalAdded :: [Decl]
goalAdded = [Decl]
decls [Decl] -> [Decl] -> [Decl]
forall a. [a] -> [a] -> [a]
++ (Decl -> Decl) -> [Decl] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Decl
makeGoal (Maybe Decl -> [Decl]
forall a. Maybe a -> [a]
maybeToList Maybe Decl
mGoal)
    applyAnno :: Decl -> Decl
applyAnno = if TIPQuirks -> Bool
noAnnotations TIPQuirks
quirks then Decl -> Decl
stripAttrs else Decl -> Decl
forall a. a -> a
id
    annoApplied :: [Decl]
annoApplied = (Decl -> Decl) -> [Decl] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map Decl -> Decl
applyAnno [Decl]
goalAdded
    applyPlural :: Decl -> [Decl]
applyPlural = if TIPQuirks -> Bool
noPluralDatatype TIPQuirks
quirks then Decl -> [Decl]
singularizeDatas else (Decl -> [Decl] -> [Decl]
forall a. a -> [a] -> [a]
:[])
    pluralAppliedBlame :: [(Decl, Int)]
pluralAppliedBlame =
      ((Decl, Int) -> [(Decl, Int)]) -> [(Decl, Int)] -> [(Decl, Int)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((([Decl] -> [Int] -> [(Decl, Int)])
-> ([Decl], [Int]) -> [(Decl, Int)]
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Decl] -> [Int] -> [(Decl, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip)(([Decl], [Int]) -> [(Decl, Int)])
-> ((Decl, Int) -> ([Decl], [Int])) -> (Decl, Int) -> [(Decl, Int)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(Decl -> [Decl]
applyPlural (Decl -> [Decl])
-> (Int -> [Int]) -> (Decl, Int) -> ([Decl], [Int])
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** Int -> [Int]
forall a. a -> [a]
repeat)) ([Decl] -> [Int] -> [(Decl, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Decl]
annoApplied [1..])
    generatedDecls :: [Decl]
generatedDecls = ((Decl, Int) -> Decl) -> [(Decl, Int)] -> [Decl]
forall a b. (a -> b) -> [a] -> [b]
map (Decl, Int) -> Decl
forall a b. (a, b) -> a
fst [(Decl, Int)]
pluralAppliedBlame
    blame :: IntMap Int
blame = ((Int, (Decl, Int)) -> IntMap Int -> IntMap Int)
-> IntMap Int -> [(Int, (Decl, Int))] -> IntMap Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (((Int -> Int -> IntMap Int -> IntMap Int)
-> (Int, Int) -> IntMap Int -> IntMap Int
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Int -> Int -> IntMap Int -> IntMap Int
forall a. Int -> a -> IntMap a -> IntMap a
IM.insert)((Int, Int) -> IntMap Int -> IntMap Int)
-> ((Int, (Decl, Int)) -> (Int, Int))
-> (Int, (Decl, Int))
-> IntMap Int
-> IntMap Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
.(((Decl, Int) -> Int) -> (Int, (Decl, Int)) -> (Int, Int)
forall (a :: * -> * -> *) b c d.
Arrow a =>
a b c -> a (d, b) (d, c)
second (Decl, Int) -> Int
forall a b. (a, b) -> b
snd)) IntMap Int
forall a. IntMap a
IM.empty ([(Int, (Decl, Int))] -> IntMap Int)
-> [(Int, (Decl, Int))] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [(Decl, Int)] -> [(Int, (Decl, Int))]
forall a b. [a] -> [b] -> [(a, b)]
zip [1..] [(Decl, Int)]
pluralAppliedBlame

prepareProverInput :: Start
                   -> GenericConfig ProofTree
                   -> Bool
                   -> String
                   -> Decl
                   -> TIPQuirks
                   -> String
                   -> IO (String, IM.IntMap Int)
prepareProverInput :: Start
-> GenericConfig ProofTree
-> Bool
-> String
-> Decl
-> TIPQuirks
-> String
-> IO (String, IntMap Int)
prepareProverInput spec :: Start
spec _cfg :: GenericConfig ProofTree
_cfg saveFile :: Bool
saveFile theoryName :: String
theoryName goal :: Decl
goal quirks :: TIPQuirks
quirks _prover_name :: String
_prover_name = 
  do
    let (tipProblem :: Start
tipProblem, blame :: IntMap Int
blame) = TIPQuirks -> Start -> Maybe Decl -> (Start, IntMap Int)
generateProblem TIPQuirks
quirks Start
spec (Maybe Decl -> (Start, IntMap Int))
-> Maybe Decl -> (Start, IntMap Int)
forall a b. (a -> b) -> a -> b
$ Decl -> Maybe Decl
forall a. a -> Maybe a
Just Decl
goal
    let theoryFileName :: String
theoryFileName = String -> Decl -> String
mkTheoryFileName String
theoryName Decl
goal
    let tipProblemString :: String
tipProblemString = Start -> String
printTIP Start
tipProblem
    String
problemFileName <- String -> String -> IO String
getTempFile String
tipProblemString String
theoryFileName
    String -> String -> IO ()
saveProblemFileIfNeeded String
theoryFileName String
tipProblemString
    (String, IntMap Int) -> IO (String, IntMap Int)
forall (m :: * -> *) a. Monad m => a -> m a
return (String
problemFileName,IntMap Int
blame)
  where
    saveProblemFileIfNeeded :: String -> String -> IO ()
    saveProblemFileIfNeeded :: String -> String -> IO ()
saveProblemFileIfNeeded theoryFileName :: String
theoryFileName tipProblemString :: String
tipProblemString =
      Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
saveFile (IO () -> IO ()) -> IO () -> IO ()
forall a b. (a -> b) -> a -> b
$ String -> String -> IO ()
writeFile String
theoryFileName String
tipProblemString