support for PVS (in progress)

Makefile.in

@@ -136,7 +136,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
 		introduction abstraction close_epsilon lift_epsilon \
 		eval_match instantiate_predicate smoke_detector
 
-LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq simplify gappa \
+LIB_PRINTER = alt_ergo why3printer smtv1 smtv2 coq pvs simplify gappa \
 	      cvc3 yices
 
 LIB_SESSION = xml termcode session session_tools session_scheduler

drivers/pvs-common.gen

+
+valid 0
+unknown "Error: \\(.*\\)$" "\\1"
+fail "Syntax error: \\(.*\\)$" "\\1"
+time "why3cpulimit time : %s s"
+
+transformation "inline_trivial"
+
+transformation "eliminate_builtin"
+transformation "eliminate_non_struct_recursion"
+
+transformation "compile_match"
+
+transformation "simplify_formula"
+
+theory BuiltIn
+
+  syntax type   int   "int"
+  syntax type   real  "real"
+  syntax predicate  (=)   "(%1 = %2)"
+end
+
+theory bool.Bool
+
+  syntax type bool   "bool"
+
+  syntax function True  "TRUE"
+  syntax function False "FALSE"
+
+  syntax function andb  "(%1 AND %2)"
+  syntax function orb   "(%1 OR %2)"
+  syntax function xorb  "(%1 XOR %2)"
+  syntax function notb  "(NOT %1)"
+  syntax function implb  "(%1 => %2)"
+
+end
+
+
+theory int.Int
+
+  syntax function zero "0"
+  syntax function one  "1"
+
+  syntax function (+)  "(%1 + %2)"
+  syntax function (-)  "(%1 - %2)"
+  syntax function (*)  "(%1 * %2)"
+  syntax function (-_) "(-%1)"
+
+  syntax predicate (<=) "(%1 <= %2)"
+  syntax predicate (<)  "(%1 <  %2)"
+  syntax predicate (>=) "(%1 >= %2)"
+  syntax predicate (>)  "(%1 >  %2)"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
+  remove prop ZeroLessOne
+
+end
+
+theory int.Abs
+
+  syntax function abs "abs(%1)"
+
+  remove prop Abs_pos
+
+end
+
+theory int.MinMax
+
+  syntax function min "min(%1, %2)"
+  syntax function max "max(%1, %2)"
+
+end
+
+theory int.EuclideanDivision
+
+  syntax function div "ndiv(%1, %2)"
+  syntax function mod "mod(%1, %2)"
+
+  remove prop Div_mod
+  remove prop Div_bound
+  remove prop Mod_bound
+  remove prop Mod_1
+  remove prop Div_1
+
+end
+
+theory int.ComputerDivision
+
+  syntax function div "(ZOdiv %1 %2)"
+  syntax function mod "(ZOmod %1 %2)"
+
+  remove prop Div_mod
+  remove prop Div_bound
+  remove prop Mod_bound
+  remove prop Div_sign_pos
+  remove prop Div_sign_neg
+  remove prop Mod_sign_pos
+  remove prop Mod_sign_neg
+  remove prop Rounds_toward_zero
+  remove prop Div_1
+  remove prop Mod_1
+  remove prop Div_inf
+  remove prop Mod_inf
+  remove prop Div_mult
+  remove prop Mod_mult
+
+end
+
+theory real.Real
+
+  syntax function zero "0%R"
+  syntax function one  "1%R"
+
+  syntax function (+)  "(%1 + %2)%R"
+  syntax function (-)  "(%1 - %2)%R"
+  syntax function (-_) "(-%1)%R"
+  syntax function (*)  "(%1 * %2)%R"
+  syntax function (/)  "(Rdiv %1 %2)%R"
+  syntax function inv  "(Rinv %1)"
+
+  syntax predicate (<=) "(%1 <= %2)%R"
+  syntax predicate (<)  "(%1 <  %2)%R"
+  syntax predicate (>=) "(%1 >= %2)%R"
+  syntax predicate (>)  "(%1 >  %2)%R"
+
+  remove prop CommutativeGroup.Comm.Comm
+  remove prop CommutativeGroup.Assoc.Assoc
+  remove prop CommutativeGroup.Unit_def
+  remove prop CommutativeGroup.Inv_def
+  remove prop Assoc.Assoc
+  remove prop Mul_distr
+  remove prop Comm.Comm
+  remove prop Unitary
+  remove prop Inverse
+  remove prop NonTrivialRing
+  remove prop CompatOrderAdd
+  remove prop CompatOrderMult
+  remove prop ZeroLessOne
+  remove prop Refl
+  remove prop Trans
+  remove prop Antisymm
+  remove prop Total
+  remove prop assoc_mul_div
+  remove prop assoc_div_mul
+  remove prop assoc_div_div
+
+end
+
+theory real.RealInfix
+
+  syntax function (+.)  "(%1 + %2)%R"
+  syntax function (-.)  "(%1 - %2)%R"
+  syntax function (-._) "(-%1)%R"
+  syntax function ( *.) "(%1 * %2)%R"
+  syntax function (/.)  "(%1 / %2)%R"
+
+  syntax predicate (<=.) "(%1 <= %2)%R"
+  syntax predicate (<.)  "(%1 <  %2)%R"
+  syntax predicate (>=.) "(%1 >= %2)%R"
+  syntax predicate (>.)  "(%1 >  %2)%R"
+
+end
+
+theory real.Abs
+
+  syntax function abs "(Rabs %1)"
+
+  remove prop Abs_le
+  remove prop Abs_pos
+
+end
+
+theory real.FromInt
+
+  syntax function from_int "(IZR %1)"
+
+  remove prop Zero
+  remove prop One
+  remove prop Add
+  remove prop Sub
+  remove prop Mul
+  remove prop Neg
+
+end
+
+theory real.Square
+
+  syntax function sqr  "(Rsqr %1)"
+  syntax function sqrt "(sqrt %1)"  (* and not Rsqrt *)
+
+  remove prop Sqrt_positive
+  remove prop Sqrt_square
+  remove prop Square_sqrt
+
+end
+
+
+theory real.ExpLog
+
+  prelude "Require Import Rtrigo_def."
+  prelude "Require Import Rpower."
+
+  syntax function exp "(exp %1)"
+  syntax function log "(ln %1)"
+
+  remove prop Exp_zero
+  remove prop Exp_sum
+  remove prop Log_one
+  remove prop Log_mul
+  remove prop Log_exp
+  remove prop Exp_log
+
+end
+
+
+theory real.Power
+
+  prelude "Require Import Rpower."
+
+  (* no power: R -> R -> R in Coq ? (only powerRZ: R -> Z -> R) *)
+end
+
+theory real.Trigonometry
+
+  prelude "Require Import Rtrigo."
+  prelude "Require Import AltSeries. (* for def of pi *)"
+
+  syntax function cos "(Rtrigo_def.cos %1)"
+  syntax function sin "(Rtrigo_def.sin %1)"
+
+  syntax function pi "PI"
+
+  syntax function tan "(Rtrigo.tan %1)"
+  (* syntax function atan "atan not defined in Coq ?" *)
+
+  remove prop Pythagorean_identity
+  remove prop Cos_le_one
+  remove prop Sin_le_one
+  remove prop Cos_0
+  remove prop Sin_0
+  remove prop Cos_pi
+  remove prop Sin_pi
+  remove prop Cos_pi2
+  remove prop Sin_pi2
+
+end

drivers/pvs.drv

+
+prelude "% This file is generated by Why3's PVS driver"
+prelude "% Beware! Only edit allowed sections below   "
+
+printer "pvs"
+filename "%f_%t_%g.pvs"
+
+import "pvs-common.gen"

share/provers-detection-data.conf.in

@@ -255,3 +255,12 @@ command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -R %l/coq Why3 -l %f"
 driver = "drivers/coq.drv"
 editor = "coqide -R %l/coq Why3 %f"
 
+[ITP pvs]
+name = "PVS"
+exec = "pvs"
+version_switch = "-version"
+version_regexp = "PVS Version \\([^ \n]+\\)"
+version_ok = "5.0"
+command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -l %f"
+driver = "drivers/pvs.drv"
+editor = "pvs %f"

src/transform/eliminate_algebraic.ml

@@ -384,6 +384,9 @@ let eliminate_algebraic_smt = Trans.compose compile_match
 let eliminate_algebraic = Trans.compose compile_match
   (Trans.fold_map comp (empty_state false) None)
 
+let () =
+  Trans.register_transform "compile_match" compile_match
+
 let () =
   Trans.register_transform "eliminate_algebraic_smt" eliminate_algebraic_smt