more PVS realizations

bin/why3-call-pvs

 #!/bin/bash
 
-export PVS_LIBRARY_PATH=$1/pvs
+if test -z "$PVS_LIBRARY_PATH"; then
+    export PVS_LIBRARY_PATH=$1/pvs
+else
+    export PVS_LIBRARY_PATH=$1/pvs:$PVS_LIBRARY_PATH
+fi
 exec pvs $2
 
 

bin/why3-check-pvs

 #!/bin/bash
 
-export PVS_LIBRARY_PATH=$1/pvs
+if test -z "$PVS_LIBRARY_PATH"; then
+    export PVS_LIBRARY_PATH=$1/pvs
+else
+    export PVS_LIBRARY_PATH=$1/pvs:$PVS_LIBRARY_PATH
+fi
 cd `dirname $2`
 exec proveit -q `basename $2`
 

configure.in

@@ -453,8 +453,6 @@ fi
 
 # PVS
 
-enable_pvs_fp_libs=no
-
 if test "$enable_pvs_libs" = no; then
     enable_pvs_support=no
     AC_MSG_WARN(PVS support disabled)
@@ -488,6 +486,19 @@ if test "$enable_pvs_support" = no; then
    enable_pvs_libs=no
 fi
 
+if test "$enable_pvs_libs" = yes; then
+   AC_MSG_CHECKING([for NASA libraries])
+   enable_pvs_nasa_libs=no
+   reason_pvs_nasa_libs="(not in PVS_LIBRARY_PATH)"
+   for dir in ${PVS_LIBRARY_PATH//:/ }; do
+       if test -f $dir/nasalib-version; then
+          enable_pvs_nasa_libs=yes
+          reason_pvs_nasa_libs=""
+       fi
+   done
+   AC_MSG_RESULT($enable_pvs_nasa_libs)
+fi
+
 # hypothesis_selection
 
 if test "$enable_hypothesis_selection" = yes; then
@@ -573,7 +584,7 @@ AC_SUBST(COQLIB)
 AC_SUBST(COQVERSION)
 
 AC_SUBST(enable_pvs_libs)
-AC_SUBST(enable_pvs_fp_libs)
+AC_SUBST(enable_pvs_nasa_libs)
 AC_SUBST(PVS)
 AC_SUBST(PVSVERSION)
 
@@ -631,7 +642,7 @@ if test "$enable_pvs_support" = "yes" ; then
    echo "    Lib                 : $PVSLIB"
    echo "    Realization support : $enable_pvs_libs $reason_pvs_libs"
    if test "$enable_pvs_libs" = "yes" ; then
-      echo "        FP arithmetic   : $enable_pvs_fp_libs $reason_pvs_fp_libs"
+      echo "        NASA libraries  : $enable_pvs_nasa_libs $reason_pvs_nasa_libs"
    fi
 fi
 echo "hypothesis selection    : $enable_hypothesis_selection"

lib/pvs/int/Abs.pvs

@@ -2,6 +2,8 @@ Abs: THEORY
  BEGIN
   IMPORTING Int
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   

lib/pvs/int/ComputerDivision.prf

+(ComputerDivision
+ (div_mod 0
+  (div_mod-1 nil 3551625251 ("" (grind) nil nil)
+   ((boolean nonempty-type-decl nil booleans nil)
+    (bool nonempty-type-eq-decl nil booleans nil)
+    (NOT const-decl "[bool -> bool]" booleans nil)
+    (number nonempty-type-decl nil numbers nil)
+    (number_field_pred const-decl "[number -> boolean]" number_fields
+     nil)
+    (number_field nonempty-type-from-decl nil number_fields nil)
+    (real_pred const-decl "[number_field -> boolean]" reals nil)
+    (real nonempty-type-from-decl nil reals nil)
+    (rational_pred const-decl "[real -> boolean]" rationals nil)
+    (rational nonempty-type-from-decl nil rationals nil)
+    (integer_pred const-decl "[rational -> boolean]" integers nil)
+    (int nonempty-type-eq-decl nil integers nil)
+    (real_lt_is_strict_total_order name-judgement
+     "(strict_total_order?[real])" real_props nil)
+    (/= const-decl "boolean" notequal nil)
+    (sgn const-decl "int" real_defs nil)
+    (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs
+         nil)
+    (div const-decl "integer" div "ints/")
+    (rem const-decl "{k | abs(k) < abs(j)}" rem "ints/")
+    (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}"
+     real_defs nil)
+    (minus_int_is_int application-judgement "int" integers nil)
+    (minus_odd_is_odd application-judgement "odd_int" integers nil)
+    (mult_divides1 application-judgement "(divides(n))" divides nil)
+    (mult_divides2 application-judgement "(divides(m))" divides nil))
+   shostak))
+ (div_bound 0
+  (div_bound-1 nil 3551625260
+   ("" (grind) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)
+   nil shostak))
+ (mod_bound 0
+  (mod_bound-1 nil 3551625904 ("" (default-strategy)) nil shostak))
+ (div_sign_pos 0
+  (div_sign_pos-1 nil 3551625906 ("" (default-strategy)) nil shostak))
+ (div_sign_neg 0
+  (div_sign_neg-1 nil 3551625906 ("" (default-strategy)) nil shostak))
+ (mod_sign_pos 0
+  (mod_sign_pos-1 nil 3551625906 ("" (default-strategy)) nil shostak))
+ (mod_sign_neg 0
+  (mod_sign_neg-1 nil 3551625907 ("" (default-strategy)) nil shostak))
+ (rounds_toward_zero 0
+  (rounds_toward_zero-1 nil 3551625313
+   ("" (grind)
+    (("1" (postpone) nil nil) ("2" (postpone) nil nil)
+     ("3" (postpone) nil nil) ("4" (postpone) nil nil)
+     ("5" (postpone) nil nil) ("6" (postpone) nil nil)
+     ("7" (postpone) nil nil) ("8" (postpone) nil nil))
+    nil)
+   nil shostak))
+ (div_1 0 (div_1-1 nil 3551625908 ("" (default-strategy)) nil shostak))
+ (mod_1 0 (mod_1-1 nil 3551625908 ("" (default-strategy)) nil shostak))
+ (div_inf 0
+  (div_inf-1 nil 3551625909 ("" (default-strategy)) nil shostak))
+ (mod_inf 0
+  (mod_inf-1 nil 3551625909 ("" (default-strategy)) nil shostak))
+ (div_mult 0
+  (div_mult-1 nil 3551625910 ("" (default-strategy)) nil shostak))
+ (mod_mult 0
+  (mod_mult-1 nil 3551625910 ("" (default-strategy)) nil shostak)))
+

lib/pvs/int/ComputerDivision.pvs

@@ -3,14 +3,24 @@ ComputerDivision: THEORY
   IMPORTING Int
   IMPORTING Abs
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   
+  IMPORTING ints@div, ints@rem
+  
+  div_total(x: int): int
+  
   % Why3 div
-  div(x:int, x1:int): int
+  div(x:int,
+    x1:int): MACRO int =  IF x1 /= 0 THEN div(x, x1) ELSE div_total(x) ENDIF
+  
+  mod_total(x: int): int
   
   % Why3 mod
-  mod(x:int, x1:int): int
+  mod(x:int,
+    x1:int): MACRO int =  IF x1 /= 0 THEN rem(x, x1) ELSE mod_total(x) ENDIF
   
   % Why3 div_mod
   div_mod: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,

lib/pvs/int/EuclideanDivision.prf

+(EuclideanDivision
+ (div_mod 0
+  (div_mod-1 nil 3551625869 ("" (default-strategy))
+   ((mult_divides2 application-judgement "(divides(m))" divides nil)
+    (mult_divides1 application-judgement "(divides(n))" divides nil)
+    (minus_odd_is_odd application-judgement "odd_int" integers nil)
+    (mod const-decl "{k | abs(k) < abs(j)}" tmod "ints/")
+    (tdiv const-decl "integer" tdiv "ints/")
+    (/= const-decl "boolean" notequal nil)
+    (int_plus_int_is_int application-judgement "int" integers nil)
+    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
+    (int_minus_int_is_int application-judgement "int" integers nil)
+    (int nonempty-type-eq-decl nil integers nil)
+    (integer_pred const-decl "[rational -> boolean]" integers nil)
+    (rational nonempty-type-from-decl nil rationals nil)
+    (rational_pred const-decl "[real -> boolean]" rationals nil)
+    (real nonempty-type-from-decl nil reals nil)
+    (real_pred const-decl "[number_field -> boolean]" reals nil)
+    (number_field nonempty-type-from-decl nil number_fields nil)
+    (number_field_pred const-decl "[number -> boolean]" number_fields
+     nil)
+    (number nonempty-type-decl nil numbers nil)
+    (NOT const-decl "[bool -> bool]" booleans nil)
+    (bool nonempty-type-eq-decl nil booleans nil)
+    (boolean nonempty-type-decl nil booleans nil))
+   shostak))
+ (div_bound 0
+  (div_bound-1 nil 3551625870 ("" (default-strategy)) nil shostak))
+ (mod_bound 0
+  (mod_bound-1 nil 3551625870
+   ("" (default-strategy)
+    (("1" (postpone) nil nil) ("2" (postpone) nil nil)
+     ("3" (postpone) nil nil))
+    nil)
+   nil shostak))
+ (mod_1 0
+  (mod_1-1 nil 3551625870 ("" (default-strategy))
+   ((minus_odd_is_odd application-judgement "odd_int" integers nil)
+    (mod const-decl "{k | abs(k) < abs(j)}" tmod "ints/")
+    (tdiv const-decl "integer" tdiv "ints/")
+    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
+    (int_minus_int_is_int application-judgement "int" integers nil)
+    (int nonempty-type-eq-decl nil integers nil)
+    (integer_pred const-decl "[rational -> boolean]" integers nil)
+    (rational nonempty-type-from-decl nil rationals nil)
+    (rational_pred const-decl "[real -> boolean]" rationals nil)
+    (real nonempty-type-from-decl nil reals nil)
+    (real_pred const-decl "[number_field -> boolean]" reals nil)
+    (number_field nonempty-type-from-decl nil number_fields nil)
+    (number_field_pred const-decl "[number -> boolean]" number_fields
+     nil)
+    (number nonempty-type-decl nil numbers nil)
+    (NOT const-decl "[bool -> bool]" booleans nil)
+    (bool nonempty-type-eq-decl nil booleans nil)
+    (boolean nonempty-type-decl nil booleans nil))
+   shostak))
+ (div_1 0
+  (div_1-1 nil 3551625870 ("" (default-strategy))
+   ((tdiv const-decl "integer" tdiv "ints/")
+    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
+    (int nonempty-type-eq-decl nil integers nil)
+    (integer_pred const-decl "[rational -> boolean]" integers nil)
+    (rational nonempty-type-from-decl nil rationals nil)
+    (rational_pred const-decl "[real -> boolean]" rationals nil)
+    (real nonempty-type-from-decl nil reals nil)
+    (real_pred const-decl "[number_field -> boolean]" reals nil)
+    (number_field nonempty-type-from-decl nil number_fields nil)
+    (number_field_pred const-decl "[number -> boolean]" number_fields
+     nil)
+    (number nonempty-type-decl nil numbers nil)
+    (NOT const-decl "[bool -> bool]" booleans nil)
+    (bool nonempty-type-eq-decl nil booleans nil)
+    (boolean nonempty-type-decl nil booleans nil))
+   shostak))
+ (div_inf 0
+  (div_inf-1 nil 3551625870 ("" (default-strategy)) nil shostak))
+ (div_inf_neg 0
+  (div_inf_neg-1 nil 3551625870 ("" (default-strategy)) nil shostak))
+ (mod_0 0
+  (mod_0-1 nil 3551625871 ("" (default-strategy))
+   ((mod const-decl "{k | abs(k) < abs(j)}" tmod "ints/")
+    (tdiv const-decl "integer" tdiv "ints/")
+    (/= const-decl "boolean" notequal nil)
+    (mult_divides2 application-judgement "(divides(m))" divides nil)
+    (mult_divides1 application-judgement "(divides(n))" divides nil)
+    (minus_odd_is_odd application-judgement "odd_int" integers nil)
+    (rat_div_nzrat_is_rat application-judgement "rat" rationals nil)
+    (int nonempty-type-eq-decl nil integers nil)
+    (integer_pred const-decl "[rational -> boolean]" integers nil)
+    (rational nonempty-type-from-decl nil rationals nil)
+    (rational_pred const-decl "[real -> boolean]" rationals nil)
+    (real nonempty-type-from-decl nil reals nil)
+    (real_pred const-decl "[number_field -> boolean]" reals nil)
+    (number_field nonempty-type-from-decl nil number_fields nil)
+    (number_field_pred const-decl "[number -> boolean]" number_fields
+     nil)
+    (number nonempty-type-decl nil numbers nil)
+    (NOT const-decl "[bool -> bool]" booleans nil)
+    (bool nonempty-type-eq-decl nil booleans nil)
+    (boolean nonempty-type-decl nil booleans nil))
+   shostak))
+ (div_1_left 0
+  (div_1_left-1 nil 3551625871 ("" (default-strategy)) nil shostak))
+ (div_minus1_left 0
+  (div_minus1_left-1 nil 3551625871 ("" (default-strategy)) nil
+   shostak))
+ (mod_1_left 0
+  (mod_1_left-1 nil 3551625871 ("" (default-strategy)) nil shostak))
+ (mod_minus1_left 0
+  (mod_minus1_left-1 nil 3551625871 ("" (default-strategy)) nil
+   shostak)))
+

lib/pvs/int/EuclideanDivision.pvs

@@ -3,14 +3,24 @@ EuclideanDivision: THEORY
   IMPORTING Int
   IMPORTING Abs
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   
+  IMPORTING ints@tdiv, ints@tmod
+  
+  div_total(x: int): int
+  
   % Why3 div
-  div(x:int, x1:int): int
+  div(x:int,
+    x1:int): MACRO int =  IF x1 /= 0 THEN tdiv(x, x1) ELSE div_total(x) ENDIF
+  
+  mod_total(x: int): int
   
   % Why3 mod
-  mod(x:int, x1:int): int
+  mod(x:int,
+    x1:int): MACRO int =  IF x1 /= 0 THEN mod(x, x1) ELSE mod_total(x) ENDIF    
   
   % Why3 div_mod
   div_mod: LEMMA FORALL (x:int, y:int): (NOT (y = 0)) => (x = ((y * div(x,

lib/pvs/int/Int.pvs

 Int: THEORY
  BEGIN
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   

lib/pvs/int/MinMax.pvs

@@ -2,6 +2,8 @@ MinMax: THEORY
  BEGIN
   IMPORTING Int
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   

lib/pvs/real/Abs.pvs

@@ -2,6 +2,8 @@ Abs: THEORY
  BEGIN
   IMPORTING Real
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   

lib/pvs/real/FromInt.pvs

@@ -3,6 +3,8 @@ FromInt: THEORY
   IMPORTING int@Int
   IMPORTING Real
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   
@@ -32,4 +34,4 @@ FromInt: THEORY
   
   
  END FromInt
- 
+ 
\ No newline at end of file

lib/pvs/real/MinMax.pvs

@@ -2,6 +2,8 @@ MinMax: THEORY
  BEGIN
   IMPORTING Real
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   

lib/pvs/real/Real.pvs

 Real: THEORY
  BEGIN
   
+  % do not edit above this line
+  
   % Why3 tuple0
   tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0
   

src/printer/pvs.ml

@@ -482,8 +482,7 @@ type chunk =
   | Edition of string * contents (* name contents *)
   | Other of contents            (* contents *)
 
-let re_ignored =
-  Str.regexp "\\([^ :]+: THEORY\\)\\|\\([^ :]+: LIBRARY\\)\\|IMPORTING\\| BEGIN"
+let re_blank = Str.regexp "[ ]*$"
 let re_why3 = Str.regexp "% Why3 \\([^ ]+\\)"
 
 (* Reads an old version of the file, as a list of chunks.
@@ -495,9 +494,13 @@ let read_old_script ch =
   let contents = ref [] in
   let rec read_line () =
     let s = input_line ch in
-    let s = clean_line s in
-    if Str.string_match re_ignored s 0 then read_line () else s
+    clean_line s
   in
+  (* skip first lines, until we find a blank line *)
+  begin try while true do
+    let s = read_line () in if Str.string_match re_blank s 0 then raise Exit
+  done with End_of_file | Exit -> () end;
+  (* then read chunks *)
   let rec read ?name () =
     let s = read_line () in
     if s = "" then begin
@@ -852,7 +855,8 @@ let print_task env pr thpr realize ?old fmt task =
        let lib = if path = thpath then "" else String.concat "." path ^ "@" in
        fprintf fmt "IMPORTING %s%s@\n" lib th.Theory.th_name.id_string)
     realized_theories;
-  fprintf fmt "@\n%% Why3 tuple0@\n";
+  fprintf fmt "@\n%% do not edit above this line@\n@\n";
+  fprintf fmt "%% Why3 tuple0@\n";
   fprintf fmt "tuple0: DATATYPE BEGIN Tuple0: Tuple0? END tuple0@\n@\n";
   print_decls ~old info fmt local_decls;
   output_remaining fmt !old;