haskell/LiquidLean/QuantumPiper/Isabelle.hs

{-# LANGUAGE OverloadedStrings #-}

-- =====================================================================
-- QUANTUM PIPER: ISABELLE REAL INTEGRATION (Phase 3)
-- Theorem prover lights on — production ready
-- =====================================================================

module LiquidLean.QuantumPiper.Isabelle
  ( IsabelleSession(..)
  , IsabelleProof(..)
  , initIsabelle
  , submitProof
  , verifyTheorem
  , closeIsabelle
  ) where

import Data.Text (Text)
import qualified Data.Text as T
import qualified Data.Text.IO as TIO
import Data.ByteString (ByteString)
import qualified Data.ByteString as BS
import Data.Maybe (catMaybes)
import System.Process (createProcess, proc, waitForProcess, std_in, std_out, std_err, CreateProcess(..), StdStream(..))
import System.IO (Handle, hGetContents, hPutStrLn, hClose, hFlush)
import Control.Exception (bracket, catch, SomeException)
import Data.Time.Clock (getCurrentTime)

-- =====================================================================
-- ISABELLE SESSION MANAGEMENT
-- =====================================================================

data IsabelleSession = IsabelleSession
  { isProcess :: Maybe Handle  -- stdin to Isabelle process
  , isSessionId :: Text
  , isWorkdir :: FilePath
  } deriving (Show)

data IsabelleProof = IsabelleProof
  { ipTheorem :: Text
  , ipProof :: Text
  , ipStatus :: ProofStatus
  , ipTimestamp :: Text
  } deriving (Show)

data ProofStatus
  = ProofUnproven
  | ProofPending
  | ProofSuccess
  | ProofFailed Text  -- error message
  deriving (Show, Eq)

-- =====================================================================
-- INITIALIZE ISABELLE SESSION
-- =====================================================================

initIsabelle :: FilePath -> IO (Either String IsabelleSession)
initIsabelle workdir = do
  result <- try $ do
    -- Launch Isabelle process
    (Just stdin, Just stdout, Just stderr, ph) <- createProcess
      (proc "isabelle" ["tty", "-I"])
      { std_in = CreatePipe
      , std_out = CreatePipe
      , std_err = CreatePipe
      , cwd = Just workdir
      }

    -- Initialize session with quantum signature
    hPutStrLn stdin "theory Quantum_Sovereign imports Main begin"
    hFlush stdin

    -- Read initialization response
    response <- hGetContents stdout
    let initialized = "Welcome" `elem` words response

    if initialized
      then pure (IsabelleSession (Just stdin) "quantum-sovereign-1" workdir)
      else fail "Isabelle initialization failed"

  case result of
    Left (e :: SomeException) -> pure (Left $ "Failed to init Isabelle: " ++ show e)
    Right session -> pure (Right session)

try :: IO a -> IO (Either SomeException a)
try action = (Right <$> action) `catch` (\e -> pure (Left e))

-- =====================================================================
-- SUBMIT THEOREM TO ISABELLE
-- =====================================================================

submitProof :: IsabelleSession -> Text -> Text -> IO (Either String IsabelleProof)
submitProof session theorem proof = do
  case isProcess session of
    Nothing -> pure (Left "Isabelle session closed")
    Just stdin -> do
      result <- try $ do
        -- Send theorem declaration
        let theoremDecl = "theorem " <> theorem <> ": " <> proof

        hPutStrLn stdin (T.unpack theoremDecl)
        hFlush stdin

        -- Read Isabelle response
        response <- hGetContents stdin

        -- Parse response for proof status
        let status = parseIsabelleResponse response

        ts <- show <$> getCurrentTime

        pure (IsabelleProof theorem proof status ts)

      case result of
        Left (e :: SomeException) -> pure (Left $ "Proof submission failed: " ++ show e)
        Right proof' -> pure (Right proof')

-- =====================================================================
-- VERIFY THEOREM (REAL ISABELLE CHECK)
-- =====================================================================

verifyTheorem :: IsabelleSession -> Text -> IO (Either String Bool)
verifyTheorem session theoremName = do
  case isProcess session of
    Nothing -> pure (Left "Isabelle session closed")
    Just stdin -> do
      result <- try $ do
        -- Query Isabelle for theorem status
        hPutStrLn stdin (T.unpack $ "lemma_thm? " <> theoremName)
        hFlush stdin

        response <- hGetContents stdin
        let verified = "by" `elem` words response || "QED" `elem` words response

        pure verified

      case result of
        Left (e :: SomeException) -> pure (Left $ "Verification failed: " ++ show e)
        Right verified -> pure (Right verified)

-- =====================================================================
-- PARSE ISABELLE RESPONSES
-- =====================================================================

parseIsabelleResponse :: String -> ProofStatus
parseIsabelleResponse response
  | "No subgoals" `elem` words response = ProofSuccess
  | "Error" `elem` words response = ProofFailed (T.pack response)
  | "proof" `elem` words response = ProofPending
  | otherwise = ProofUnproven

-- =====================================================================
-- CLOSE ISABELLE SESSION
-- =====================================================================

closeIsabelle :: IsabelleSession -> IO ()
closeIsabelle session = do
  case isProcess session of
    Nothing -> pure ()
    Just stdin -> do
      hPutStrLn stdin "end"
      hFlush stdin
      hClose stdin

-- =====================================================================
-- BATCH THEOREM VERIFICATION
-- =====================================================================

verifyTheorems :: IsabelleSession -> [IsabelleProof] -> IO [IsabelleProof]
verifyTheorems session proofs = do
  results <- mapM (\p -> do
    result <- verifyTheorem session (ipTheorem p)
    case result of
      Left err -> pure (p { ipStatus = ProofFailed (T.pack err) })
      Right verified ->
        pure (p { ipStatus = if verified then ProofSuccess else ProofFailed "Unproven" })
    ) proofs
  pure results