Add prove_extcore command (#1656)

* Add a "prove_prop" command

For proving terms that have already been translated into proposition types

* Whoops, fix Interpreter.hs to reflect a name change

* Refactor prove_print and prove_prop

* Rename prove_prop to prove_extcore

src/SAWScript/Builtins.hs

@@ -924,13 +924,13 @@ provePrim script t = do
     _ -> return ()
   return res
 
-provePrintPrim ::
+proveHelper ::
   ProofScript () ->
   TypedTerm ->
+  (Term -> TopLevel Prop) ->
   TopLevel Theorem
-provePrintPrim script t = do
-  sc <- getSharedContext
-  prop <- io $ predicateToProp sc Universal (ttTerm t)
+proveHelper script t f = do
+  prop <- f $ ttTerm t
   let goal = ProofGoal 0 "prove" "prove" prop
   opts <- rwPPOpts <$> getTopLevelRW
   res <- SV.runProofScript script goal Nothing "prove_print_prim"
@@ -944,6 +944,22 @@ provePrintPrim script t = do
     InvalidProof _stats _cex pst -> failProof pst
     UnfinishedProof pst -> failProof pst
 
+provePrintPrim ::
+  ProofScript () ->
+  TypedTerm ->
+  TopLevel Theorem
+provePrintPrim script t = do
+  sc <- getSharedContext
+  proveHelper script t $ io . predicateToProp sc Universal
+
+provePropPrim ::
+  ProofScript () ->
+  TypedTerm ->
+  TopLevel Theorem
+provePropPrim script t = do
+  sc <- getSharedContext
+  proveHelper script t $ io . termToProp sc
+
 satPrim ::
   ProofScript () ->
   TypedTerm ->

src/SAWScript/Interpreter.hs

@@ -1313,6 +1313,15 @@ primitives = Map.fromList
     , "if unsuccessful."
     ]
 
+  , prim "prove_extcore"         "ProofScript () -> Term -> TopLevel Theorem"
+    (pureVal provePropPrim)
+    Current
+    [ "Use the given proof script to attempt to prove that a term representing"
+    , "a proposition is valid. For example, this is useful for proving a goal"
+    , "obtained with 'offline_extcore'. Returns a Theorem if successful, and"
+    , "aborts if unsuccessful."
+    ]
+
   , prim "sat"                 "ProofScript () -> Term -> TopLevel SatResult"
     (pureVal satPrim)
     Current