From 173747336f7ae8213c827327c5a0ae1b385acf6f Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Thu, 28 May 2015 16:56:05 -0700 Subject: [PATCH] prove(_print) and sat(_print) now require 'ProofScript SatResult' argument This avoids a run-time type error, instead catching the error in the saw-script typechecker. Fixes #10. This is a temporary stop-gap measure: Eventually the proof commands will change so that we can allow additional types of proof scripts. (See issue #9.) --- src/SAWScript/Interpreter.hs | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index 9ff2bd9429..6578eb75f2 100644 --- a/src/SAWScript/Interpreter.hs +++ b/src/SAWScript/Interpreter.hs @@ -555,19 +555,19 @@ primitives = Map.fromList (pureVal (writeCore :: FilePath -> TypedTerm SAWCtx -> IO ())) [ "Write out a representation of a term in SAWCore external format." ] - , prim "prove" "{b} ProofScript b -> Term -> TopLevel ProofResult" + , prim "prove" "ProofScript SatResult -> Term -> TopLevel ProofResult" (scVal provePrim) [ "TODO" ] - , prim "prove_print" "{b} ProofScript b -> Term -> TopLevel Theorem" + , prim "prove_print" "ProofScript SatResult -> Term -> TopLevel Theorem" (scVal provePrintPrim) [ "TODO" ] - , prim "sat" "{b} ProofScript b -> Term -> TopLevel SatResult" + , prim "sat" "ProofScript SatResult -> Term -> TopLevel SatResult" (scVal satPrim) [ "TODO" ] - , prim "sat_print" "{b} ProofScript b -> Term -> TopLevel ()" + , prim "sat_print" "ProofScript SatResult -> Term -> TopLevel ()" (scVal satPrintPrim) [ "TODO" ]