ExternalProver.agda

{-# OPTIONS --rewriting #-}

module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.String renaming (primStringEquality to _==_)
open import Agda.Builtin.List

data ⊥ : Set where

postulate
  primExec : String → List String → String

postulate
  Problem : Set
  ⟦_⟧ : Problem → Set
  formatP : Problem → String

prover : Problem → Bool
prover p = primExec "z3" (formatP p ∷ []) == "OK"

postulate
  sound : ∀ p → prover p ≡ true → ⟦ p ⟧

Proof : ∀ p → Set
Proof p with prover p
... | true  = ⟦ p ⟧
... | false = ⊤

prove : ∀ p → Proof p
prove p with prover p | sound p
... | true  | s = s refl
... | false | _ = _

{-# BUILTIN REWRITE _≡_ #-}

postulate
  hard-problem : Problem
  eval-format : formatP hard-problem ≡ "hard-problem"
  eval-exec : primExec "z3" ("hard-problem" ∷ []) ≡ "OK"
  
{-# REWRITE eval-format #-}
{-# REWRITE eval-exec #-}

test : ⟦ hard-problem ⟧
test = prove hard-problem

check : test ≡ sound hard-problem refl
check = refl

What it might look like with a TC version of primExec:

{-# OPTIONS --rewriting #-}

module _ where

open import Agda.Builtin.Bool
open import Agda.Builtin.Equality
open import Agda.Builtin.Unit
open import Agda.Builtin.String renaming (primStringEquality to _==_)
open import Agda.Builtin.List
open import Agda.Builtin.Reflection renaming (bindTC to _>>=_)

data ⊥ : Set where

primExec : String → List String → TC String
primExec "z3" ("hard-problem" ∷ []) = returnTC "OK"
primExec _ _ = returnTC "NO"

postulate
  Problem : Set
  ⟦_⟧ : Problem → Set
  formatP : Problem → String

private
  data Witness (p : Problem) : Set where
    proved-by : String → Witness p
  
postulate
  sound : ∀ p → Witness p → ⟦ p ⟧

pattern vArg x = arg (arg-info visible relevant) x

macro
  prove : Problem → Term → TC ⊤
  prove p hole = do
    "OK" ← primExec "z3" (formatP p ∷ [])
      where _ → typeError (strErr "Not provable" ∷ [])
    `p ← quoteTC p
    unify hole (def (quote sound) ( vArg `p
                                  ∷ vArg (con (quote proved-by) (vArg (lit (string "z3")) ∷ []))
                                  ∷ []))
    
{-# BUILTIN REWRITE _≡_ #-}

postulate
  hard-problem : Problem
  eval-format : formatP hard-problem ≡ "hard-problem"
  
{-# REWRITE eval-format #-}

test : ⟦ hard-problem ⟧
test = prove hard-problem

check : test ≡ sound hard-problem (proved-by "z3")
check = refl