Commit 6acb343b authored by Heiko Becker's avatar Heiko Becker
Browse files

Fix certificate generation to generate actual theorems and to not ave HOL4 typechecker fail

parent f4c286a8
......@@ -49,7 +49,7 @@ object CertificatePhase extends DaisyPhase {
thePrecondition match {
case Some (pre) =>
//First write the imports
val prelude = getPrelude(prv)
val prelude = getPrelude(prv, "certificate_" + prg.id + "_" + fnc.id.toString)
//the definitions for the whole expression
val (theDefinitions, lastGenName) = getValues(theBody.get,reporter,prv)
//generate the precondition
......@@ -64,6 +64,8 @@ object CertificatePhase extends DaisyPhase {
val certificateText =
if (prv == "hol-light")
textWithoutFCall + "\n\n" + "let theRewrites = [thePrecondition;absenv;" + holLightExpList(theBody.get) + "];;" + "\n" + functionCall + "\nexit(0);;"
else if (prv == "hol4")
textWithoutFCall + "\n\n" + functionCall + "\n\n val _ = export_theory();"
else
textWithoutFCall + "\n\n" + functionCall
......@@ -85,11 +87,12 @@ object CertificatePhase extends DaisyPhase {
private val nextConstantId = { var i = 0; () => { i += 1; i} }
private val nextFreshVariable = { var i = 0; () => { i += 1; i} }
private def getPrelude(prover:String) :String=
private def getPrelude(prover:String, fname:String) :String=
if (prover == "coq")
"Require Import Daisy.CertificateChecker."
else if (prover == "hol4")
"open CertificateCheckerTheory;\nopen simpLib realTheory realLib RealArith;"
"open preamble abbrevsTheory CertificateCheckerTheory;\nopen simpLib realTheory realLib RealArith;\n\n" +
"val _ = new_theory \"" + fname +"\";\n\n"
else
"needs \"CertificateChecker.hl\";;\nneeds \"Infra/convs.hl\";;"
......@@ -339,7 +342,7 @@ object CertificatePhase extends DaisyPhase {
private def hol4Precondition (ranges:Map [Identifier, (Rational, Rational)]) :(String, String) =
{
var theFunction = "val thePrecondition_def = Define ` \n thePrecondition (n:num) = \n"
var theFunction = "val thePrecondition_def = Define ` \n thePrecondition (n:num):interval = \n"
for ((id,intv) <- ranges) {
val ivHolLight = hol4Interval(intv)
theFunction += "if n = " + identifierNums(id) + " then " + ivHolLight + " else "
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment