PVS driver/printer: support for types 'real' and 'map'

drivers/pvs-common.gen

@@ -29,6 +29,21 @@ theory Tuple0
   syntax function Tuple0 "Tuple0"
 end
 
+theory map.Map
+  syntax type  map "[%1 -> %2]"
+
+  syntax function get "%1(%2)"
+  syntax function set "(%1 WITH [(%2) |-> %3])"
+
+  remove prop Select_eq
+  remove prop Select_neq
+
+  (*
+  syntax function const "(LAMBDA (x:%t0): %1)"
+  remove prop Const
+  *)
+end
+
 theory bool.Bool
 
   syntax type bool   "bool"
@@ -40,7 +55,7 @@ theory bool.Bool
   syntax function orb   "(%1 OR %2)"
   syntax function xorb  "(%1 XOR %2)"
   syntax function notb  "(NOT %1)"
-  syntax function implb  "(%1 => %2)"
+  syntax function implb "(%1 => %2)"
 
 end
 
@@ -107,6 +122,7 @@ theory int.EuclideanDivision
 
 end
 
+(***
 theory int.ComputerDivision
 
   syntax function div "(ZOdiv %1 %2)"
@@ -128,23 +144,24 @@ theory int.ComputerDivision
   remove prop Mod_mult
 
 end
+***)
 
 theory real.Real
 
-  syntax function zero "0%R"
-  syntax function one  "1%R"
+  syntax function zero "0"
+  syntax function one  "1"
 
-  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 function (+)  "(%1 + %2)"
+  syntax function (-)  "(%1 - %2)"
+  syntax function (-_) "(-%1)"
+  syntax function (*)  "(%1 * %2)"
+  syntax function (/)  "(%1 / %2)"
+  syntax function inv  "(1 / %1)"
 
-  syntax predicate (<=) "(%1 <= %2)%R"
-  syntax predicate (<)  "(%1 <  %2)%R"
-  syntax predicate (>=) "(%1 >= %2)%R"
-  syntax predicate (>)  "(%1 >  %2)%R"
+  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
@@ -171,22 +188,22 @@ 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 function (+.)  "(%1 + %2)"
+  syntax function (-.)  "(%1 - %2)"
+  syntax function (-._) "(-%1)"
+  syntax function ( *.) "(%1 * %2)"
+  syntax function (/.)  "(%1 / %2)"
 
-  syntax predicate (<=.) "(%1 <= %2)%R"
-  syntax predicate (<.)  "(%1 <  %2)%R"
-  syntax predicate (>=.) "(%1 >= %2)%R"
-  syntax predicate (>.)  "(%1 >  %2)%R"
+  syntax predicate (<=.) "(%1 <= %2)"
+  syntax predicate (<.)  "(%1 <  %2)"
+  syntax predicate (>=.) "(%1 >= %2)"
+  syntax predicate (>.)  "(%1 >  %2)"
 
 end
 
 theory real.Abs
 
-  syntax function abs "(Rabs %1)"
+  syntax function abs "abs(%1)"
 
   remove prop Abs_le
   remove prop Abs_pos
@@ -195,7 +212,7 @@ end
 
 theory real.FromInt
 
-  syntax function from_int "(IZR %1)"
+  syntax function from_int "(%1 :: real)"
 
   remove prop Zero
   remove prop One
@@ -208,62 +225,34 @@ 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
+  syntax function sqrt "SQRT(%1)"
 
 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
+  syntax function exp "EXP(%1)"
+  syntax function log "LOG(%1)"
 
 end
 
-
 theory real.Power
 
-  prelude "Require Import Rpower."
+  syntax function pow "(%1 ^ %2)"
+
+  remove prop Pow_x_zero
+  remove prop Pow_x_one
+  remove prop Pow_one_y
 
-  (* 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 cos "COS(%1)"
+  syntax function sin "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
+  syntax function tan "TAN(%1)"
 
 end

src/printer/pvs.ml

@@ -53,9 +53,8 @@ QUESTIONS FOR THE PVS TEAM
 
 TODO
 ----
-  * drivers
-    - maps
-    - reals
+  * driver
+    - maps: const
 
 *)
 
@@ -282,7 +281,7 @@ and print_tnode opl opr info fmt t = match t.t_node with
           Print_number.hex_real_support = Print_number.Number_unsupported;
           Print_number.frac_real_support = Print_number.Number_custom
             (Print_number.PrintFracReal
-               ("%s%%R", "(%s * %s)%%R", "(%s / %s)%%R"));
+               ("%s", "(%s * %s)", "(%s / %s)"));
           Print_number.def_real_support = Print_number.Number_unsupported;
         }
       in
@@ -808,7 +807,7 @@ let print_task _env pr thpr realize ?old fmt task =
         | _ -> used
       in
       Mid.iter
-        (fun id th -> fprintf fmt "Require %a.%s.@\n"
+        (fun id th -> fprintf fmt "IMPORTING %a.%s.@\n"
           print_path th.Theory.th_path id.id_string)
         used;
       let symbols = Task.used_symbols used in

tests/test-jcf.why

 
 theory TestPVS
 
+  use import bool.Bool
   use import int.Int
-  use import list.List
-  use import list.Append
+  use import map.Map
 
-  type elt
-  type tree = Null | Node tree elt tree
+  function m: map int bool
 
-  predicate contains (t: tree) (x: elt) = match t with
-    | Null       -> false
-    | Node l y r -> contains l x || x = y || contains r x
-  end
+  axiom a: get m 0 = True
+  axiom b: get m 1 = False
 
-  function elements (t: tree): list elt = match t with
-    | Null       -> Nil
-    | Node l x r -> elements l ++ (Cons x (elements r))
-  end
+  goal G: get (const False) 42 = False
 
-  goal G: forall t: tree. elements t = Nil <-> t = Null
+  use import real.Real
+  use import real.Power
+
+  goal G1: pow 2. 4. = 16.
 
 end