Commit 8e35f674 authored by Heiko Becker's avatar Heiko Becker

Sort out some bugs in Certificate generation and parser in Coq

parent 0091072c
......@@ -20,6 +20,7 @@ Inductive Token:Type :=
| DMUL
| DDIV
| DFRAC
| DCAST
| DFAIL: ascii -> Token.
Open Scope string_scope.
......@@ -93,7 +94,9 @@ match fuel with
| "Let" => DLET :: lex input'' fuel'
| "PRE" => DPRE :: lex input'' fuel'
| "ABS" => DABS :: lex input'' fuel'
| "GAMMA" => DGAMMA :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| "Cast" => DCAST :: lex input'' fuel'
| "MTYPE" => let ts := lex input'' fuel' in
(match ts with
|DCONST 32 :: ts' => DTYPE M32 :: ts'
......@@ -122,11 +125,17 @@ match fuel with
|_ => []
end.
Fixpoint str_join s1 s2 :=
match s1 with
| String c s1' => String c (str_join s1' s2)
| "" => s2
end.
Fixpoint str_of_num (n:nat) (m:nat):=
match m with
|S m' =>
if n <? 10 then String (ascii_of_nat (n + 48)) ""
else String (ascii_of_nat ((n mod 10) + 48)) (str_of_num (n / 10) m')
else str_join (str_of_num (n/10) m') (String (ascii_of_nat ((n mod 10) + 48)) "")
|_ => ""
end .
......@@ -137,7 +146,6 @@ match m with
| _ => "" (* FIXME *)
end.
(*
Definition pp_token (token:Token) :=
match token with
| DLET => "Let"
......@@ -146,34 +154,32 @@ Definition pp_token (token:Token) :=
| DABS => "ABS"
| DCOND => "?"
| DVAR => "Var"
| DCONST num => str_of_num num num
| DCONST num => str_of_num (N.to_nat num) (N.to_nat num)
| DGAMMA => "Gamma"
| DTYPE m => str_join "MTYPE " (type_to_string m)
| DNEG => "~"
| DPLUS => "+"
| DSUB => "-"
| DMUL => "*"
| DDIV => "/"
| DFRAC => "#"
| DCAST => "Cast"
| DFAIL s => ""
end .
Fixpoint str_join s1 s2 :=
match s1 with
| String c s1' => String c (str_join s1' s2)
| "" => s2
end.
(* Pretty Printer for Tokens *)
Fixpoint pp (tokList:list Token) :=
match tokList with
| token :: tokRest => str_join (pp_token token) (pp tokRest)
| token :: tokRest => str_join (pp_token token) ( str_join " " (pp tokRest))
| [] => ""
end.
*)
(** Prefix form parser for expressions **)
Fixpoint parseExp (tokList:list Token) (fuel:nat):option (exp Q * list Token) :=
match fuel with
|S fuel' =>
match tokList with
| DTYPE t :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
| DCONST n :: DFRAC :: DCONST m :: DTYPE t :: tokRest =>
match m with
|N0 => None
|Npos p => Some (Const t (Z.of_N n # p), tokRest)
......@@ -221,6 +227,12 @@ Fixpoint parseExp (tokList:list Token) (fuel:nat):option (exp Q * list Token) :=
end
| None => None
end
| DCAST :: DTYPE m :: tokRest =>
match parseExp tokRest fuel' with
|Some (e1, tokRest') =>
Some (Downcast m e1, tokRest')
|_ => None
end
| _ => None
end
|_ => None
......@@ -237,7 +249,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
|S fuel' =>
match input with
(* We already have a valid let binding *)
| DVAR :: DTYPE m :: DCONST n :: expLetRest =>
| DVAR ::DCONST n :: DTYPE m :: expLetRest =>
(* so we parse an expression *)
match parseExp expLetRest fuel with
| Some (e, letRest) =>
......@@ -534,4 +546,12 @@ Definition runChecker (input:string) :=
| _ => "failure no num of functions"
end.
(* Definition res := Eval compute in runChecker "1 1 Ret + 1657#5 Var 1 PRE ? Var 1 ~100#1 100#1 ABS ? + 1657#5 Var 1 1157#5 2157#5 7771411516990528329#81129638414606681695789005144064 ? 1657#5 1657#5 1657#5 1657#45035996273704960 ? Var 1 ~100#1 100#1 25#2251799813685248". *)
\ No newline at end of file
(* Eval compute in "100 1 *)
Eval compute in parseExp (lex "Cast MTYPE 32 * ~9143#5 MTYPE 64 Var 0" 100) 100.
Eval compute in parseExp (lex "+ Var 6 * ~5143#5 MTYPE 64 Var 1" 100)100.
GAMMA Var 0 MTYPE 64 Var 1 MTYPE 64 Var 6 MTYPE 32 Var 2 MTYPE 32 Var 3 MTYPE 64
PRE ? Var 0 0#1 1#1 ? Var 1 ~1#2 1#2 ? Var 2 0#1 1#2 ? Var 3 0#1 1#2
ABS ? Var 6 ~9143#5 0#1 6681254772392645084970685889310303821814064616580023#61299821634635554334333881086012367344749564887344087040 ? Cast MTYPE 32 * ~9143#5 Var 0 ~9143#5 0#1 6681254772392645084970685889310303821814064616580023#61299821634635554334333881086012367344749564887344087040 ? * ~9143#5 Var 0 ~9143#5 0#1 2225304852074246919292264980387210167#3653754093327257295509212081790707549139831357440 ? ~9143#5 ~9143#5 ~9143#5 9143#45035996273704960 ? Var 0 0#1 1#1 1#9007199254740992 ? + + + Var 6 * ~5143#5 Var 1 * ~2008#1 Var 2 * ~104#1 Var 3 ~33989#10 5143#10 7562996188354616957999453839786539197309920400907048039773818377804552534410042513635368200206033847#44794894843556084211148845611368885562432909944692990697999782019275837423603218907617549865432142315520 ? + + Var 6 * ~5143#5 Var 1 * ~2008#1 Var 2 ~33469#10 5143#10 839661248383557755304484875533645064922397376094449615419192672646813101333139170231#4973232364097866421553822481468208401004561507973477174404639768931594970125333755330560 ? + Var 6 * ~5143#5 Var 1 ~23429#10 5143#10 60179393244828582529861129846732930624201324211232549387089435698103#552139707743245102994780468982162036196088717773630924413001937903943680 ? Var 6 ~9143#5 0#1 6681254772392645084970685889310303821814064616580023#61299821634635554334333881086012367344749564887344087040 ? * ~5143#5 Var 1 ~5143#10 5143#10 1251749191098966630856405861766534167#7307508186654514591018424163581415098279662714880 ? ~5143#5 ~5143#5 ~5143#5 5143#45035996273704960 ? Var 1 ~1#2 1#2 1#18014398509481984 ? * ~2008#1 Var 2 ~1004#1 0#1 20363539317926376808075051095032059#340282366920938463463374607431768211456 ? ~2008#1 ~2008#1 ~2008#1 251#1125899906842624 ? Var 2 0#1 1#2 1#33554432 ? * ~104#1 Var 3 ~52#1 0#1 3164055898169660937416542135517197#182687704666362864775460604089535377456991567872 ? ~104#1 ~104#1 ~104#1 13#1125899906842624 ? Var 3 0#1 1#2 1#18014398509481984"
......@@ -144,6 +144,16 @@ object CertificatePhase extends DaisyPhase {
}
}
private def precisionToBinaryString(p: Precision): String =
{
p match {
case Float32 => "32"
case Float64 => "64"
// case DoubleDouble => "M128"
// case QuadDouble => "M256"
case _ => reporter.fatalError ("In precisionToString, unknown precision.")
}
}
private def ocamlVariable(vname:Identifier, id:Int, reporter:Reporter) :(String, String) =
{
val theExpr = s"let ExpVar$vname${vname.globalId} = Var $id.\n"
......@@ -241,7 +251,6 @@ object CertificatePhase extends DaisyPhase {
s"UMin${nameOp}")
private def getValues(e: Expr, precisions: Map[Identifier, Precision], constPrecision: Precision, prv: String): (String, String) = {
reporter.info(s"$e\n\n")
//if the expression has already been defined before
if (expressionNames.contains(e)){
("", expressionNames(e))
......@@ -271,7 +280,8 @@ object CertificatePhase extends DaisyPhase {
else if (prv == "hol4")
hol4Constant (x, nextConstantId(), constPrecision)
else {
val text = r.toFractionString.replace("/","#").replace("(","").replace(")","").replace("-","~")
val fracText = r.toFractionString.replace("/","#").replace("(","").replace(")","").replace("-","~")
val text = s"$fracText MTYPE ${precisionToBinaryString(constPrecision)} "
(text, text)
}
expressionNames += (e -> name)
......@@ -368,9 +378,12 @@ object CertificatePhase extends DaisyPhase {
if (prv == "coq") {
val (dDef, dName) = coqDowncast(expName, tpe_prec)
(expDef + dDef, dName)
} else {
} else if (prv == "hol4") {
val (dDef, dName) = hol4Downcast(expName, tpe_prec)
(expDef + dDef, dName)
} else {
val text = s"Cast MTYPE ${precisionToBinaryString(tpe_prec)} $expName"
(text,text)
}
expressionNames += (e -> name)
(definition, name)
......@@ -396,7 +409,9 @@ object CertificatePhase extends DaisyPhase {
}else if (prv == "hol4"){
hol4Variable (x)
} else {
(s"Var ${varId.toString}", s"Var ${varId.toString}")
val text = s"Var ${varId.toString}"
val textWithType = s"$text MTYPE ${precisionToBinaryString(precisions(x))}"
(textWithType, text)
}
expressionNames += (Variable(x) -> varName)
//now recursively compute the command
......@@ -466,11 +481,49 @@ object CertificatePhase extends DaisyPhase {
(theFunction, s"thePrecondition_${fName}")
}
private def hol4Precondition (ranges: Map[Identifier, (Rational, Rational)], fName: String): (String, String) =
{
var theFunction = s"val thePrecondition_${fName}_def = Define ` \n thePrecondition${fName} (n:num):interval = \n"
for ((id, intv) <- ranges) {
val ivHolLight = hol4Interval(intv)
theFunction += "if n = " + identifierNums(id) + " then " + ivHolLight + " else "
}
theFunction += "(0,1)`;"
(theFunction, s"thePrecondition${fName}")
}
private def binaryPrecondition (ranges:Map [Identifier, (Rational, Rational)],fName:String) :(String, String) =
{
var theFunction = " PRE "
for ((id,intv) <- ranges) {
val ivBin = binaryInterval(intv)
theFunction += s"? Var ${identifierNums(id)} $ivBin "
}
(theFunction, "")
}
private def getPrecondFunction(pre: Expr, fName: String, prv: String): (String, String) =
{
val (ranges, errors) = daisy.analysis.SpecsProcessingPhase.extractPreCondition(pre)
if (! errors.isEmpty){
reporter.fatalError("Errors on inputs are currently unsupported")
}
if (prv == "coq"){
coqPrecondition(ranges, fName)
}else if (prv == "hol4"){
hol4Precondition(ranges,fName)
} else {
binaryPrecondition(ranges,fName)
}
}
private def getDefVars(fnc: FunDef, precMap: Map[Identifier, Precision], prv: String): (String, String) = {
if (prv == "coq")
coqDefVars(fnc, precMap)
else if(prv == "hol4")
hol4DefVars(fnc, precMap)
else if (prv=="binary")
binaryDefVars(fnc,precMap)
else
reporter.fatalError("Unknown theorem prover in getDefVars call)")
}
......@@ -498,41 +551,18 @@ object CertificatePhase extends DaisyPhase {
(theFunction, s"defVars_$fName")
}
private def hol4Precondition (ranges: Map[Identifier, (Rational, Rational)], fName: String): (String, String) =
private def binaryDefVars (fnc: FunDef, precMap: Map[Identifier, Precision]): (String, String) =
{
var theFunction = s"val thePrecondition_${fName}_def = Define ` \n thePrecondition${fName} (n:num):interval = \n"
for ((id, intv) <- ranges) {
val ivHolLight = hol4Interval(intv)
theFunction += "if n = " + identifierNums(id) + " then " + ivHolLight + " else "
}
theFunction += "(0,1)`;"
(theFunction, s"thePrecondition${fName}")
}
private def binaryPrecondition (ranges:Map [Identifier, (Rational, Rational)],fName:String) :(String, String) =
{
var theFunction = " PRE "
for ((id,intv) <- ranges) {
val ivBin = binaryInterval(intv)
theFunction += s"? Var ${identifierNums(id)} $ivBin "
val fName = fnc.id.toString
var theFunction = "GAMMA "
for (variable <- allVariablesOf(fnc.body.get)) {
//DVAR :: DCONST n :: MTYPE m
theFunction += s"Var ${identifierNums(variable)} MTYPE ${precisionToBinaryString(precMap(variable))} "
}
(theFunction, "")
theFunction += "\n"
(theFunction, s"")
}
private def getPrecondFunction(pre: Expr, fName: String, prv: String): (String, String) =
{
val (ranges, errors) = daisy.analysis.SpecsProcessingPhase.extractPreCondition(pre)
if (! errors.isEmpty){
reporter.fatalError("Errors on inputs are currently unsupported")
}
if (prv == "coq"){
coqPrecondition(ranges, fName)
}else if (prv == "hol4"){
hol4Precondition(ranges,fName)
} else {
binaryPrecondition(ranges,fName)
}
}
private def conditional (condition: String, thenC: String, elseC: String): String =
"if " + condition + "\n" +
......@@ -723,6 +753,9 @@ object CertificatePhase extends DaisyPhase {
case x @ UMinus(e) =>
binaryAbsEnv (e, errorMap, rangeMap, reporter)
case x @ Downcast(e, t) =>
binaryAbsEnv (e, errorMap, rangeMap, reporter)
case x @ _ =>
reporter.fatalError(s"Unsupported operation $e while generating absenv")
}
......
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