src/Main.hs

module Main where

import System.Environment (getArgs)
import System.Exit (exitFailure, exitSuccess)

import Language.AST
import Language.Parser (parseModule)
import Language.Elaborator (elaborate)
import IR.Boolean (Circuit(..), circuitBody)
import Proof.Produce (proveValidity)
import Proof.Certificate (ProofCertificate(..), ProofConclusion(..))
import Checker.Kernel (checkCertificate, CheckResult(..))

main :: IO ()
main = do
  args <- getArgs
  case args of
    [file] -> verifyFile file
    _ -> putStrLn "Usage: pure-validity <file.nf>" >> exitFailure

verifyFile :: FilePath -> IO ()
verifyFile path = do
  src <- readFile path
  let name = takeWhile (/= '.') $ reverse $ takeWhile (/= '/') $ reverse path
  case parseModule name src of
    Left err -> do
      putStrLn $ "PARSE ERROR: " ++ err
      exitFailure
    Right modul -> do
      case elaborate modul of
        Left err -> do
          putStrLn $ "ELABORATION ERROR: " ++ show err
          exitFailure
        Right circuits -> do
          putStrLn $ "Module: " ++ name
          putStrLn $ "Properties: " ++ show (length circuits)
          putStrLn ""
          results <- mapM verifyCircuit circuits
          let passed = length $ filter id results
              total = length results
          putStrLn ""
          putStrLn $ show passed ++ "/" ++ show total ++ " verified."
          if passed == total then exitSuccess else exitFailure

verifyCircuit :: Circuit -> IO Bool
verifyCircuit (Circuit name _ body) = do
  let cert = proveValidity name body
  case checkCertificate cert of
    Verified vname -> do
      putStrLn $ "  [OK] " ++ vname
      return True
    Rejected rname reason -> do
      putStrLn $ "  [FAIL] " ++ rname ++ " — " ++ reason
      return False