tstp2agda- Proof-term reconstruction from TSTP to Agda

Safe HaskellNone





type Tactic = AgdaSignature -> Maybe (IO ())

A Tactic is a function that tries to give a corresponding implementation to a Metis-generated proof step:

Given some Metis-generated Formulae

fof(a1, axiom, (a)).

fof(normalize_0_2, plain, (a), inference(canonicalize, [], [a1])).

tstp2agda will generate the following signature for the function fun-normalize-0-2 that given a1 return normalize_0_2 (Actually their corresponding formula)

fun-normalize-0-2 : {a : Set} → a → a

A Tactic is function that given a signature in the form of AgdaSignature will determine the corresponding "implementation"

fun-normalize-0-2 : { a : Set} → a → a
fun-normalize-0-2 = id


resolveTactic :: AgdaSignature -> [Tactic] -> IO ()

resolveTactic τ χ tries to find and implementation for τ using every tactic in χ and in case of failure prints the default implementation.

resolveTacticGen :: AgdaSignature -> IO ()

Similar to resolveTactic but using all the build-in tactics.


identity :: Tactic

In Metis some applications of the inference rule canonicalize result in trivial [a ↦ a] behavior that is captured in Agda with the identity function.