PVS printer in progress

fixed Coq printer on mutually recursive functions

drivers/pvs-common.gen

@@ -7,6 +7,7 @@ time "why3cpulimit time : %s s"
 transformation "inline_trivial"
 
 transformation "eliminate_builtin"
+transformation "eliminate_mutual_recursion"
 transformation "eliminate_non_struct_recursion"
 
 transformation "compile_match"
@@ -14,12 +15,16 @@ transformation "compile_match"
 transformation "simplify_formula"
 
 theory BuiltIn
-
   syntax type   int   "int"
   syntax type   real  "real"
   syntax predicate  (=)   "(%1 = %2)"
 end
 
+theory Tuple0
+  syntax type     tuple0 "tuple0"
+  syntax function Tuple0 "Tuple0"
+end
+
 theory bool.Bool
 
   syntax type bool   "bool"

share/provers-detection-data.conf.in

@@ -261,6 +261,6 @@ exec = "pvs"
 version_switch = "-version"
 version_regexp = "PVS Version \\([^ \n]+\\)"
 version_ok = "5.0"
-command = "@LOCALBIN@why3-cpulimit 0 %m -s %e -l %f"
+command = "@LOCALBIN@why3-cpulimit 0 %m -s proveit %f"
 driver = "drivers/pvs.drv"
 editor = "pvs %f"

src/printer/coq.ml

@@ -162,8 +162,10 @@ let unambig_fs fs =
 
 let lparen_l fmt () = fprintf fmt "@ ("
 let lparen_r fmt () = fprintf fmt "(@,"
-let print_paren_l fmt x = print_list_delim lparen_l rparen comma fmt x
-let print_paren_r fmt x = print_list_delim lparen_r rparen comma fmt x
+let print_paren_l fmt x =
+  print_list_delim ~start:lparen_l ~stop:rparen ~sep:comma fmt x
+let print_paren_r fmt x =
+  print_list_delim ~start:lparen_r ~stop:rparen ~sep:comma fmt x
 
 let arrow fmt () = fprintf fmt "@ -> "
 let print_arrow_list fmt x = print_list arrow fmt x
@@ -590,7 +592,7 @@ let print_recursive_decl info tm fmt (ls,ld) =
   begin match ld with
     | Some ld ->
         let vl,e = open_ls_defn ld in
-        fprintf fmt "%a%a%a {struct %a}: %a :=@ %a.@]@\n"
+        fprintf fmt "%a%a%a {struct %a}: %a :=@ %a@]"
           print_ls ls
           print_ne_params all_ty_params
           (print_space_list (print_vsty info)) vl
@@ -604,15 +606,13 @@ let print_recursive_decl info tm fmt (ls,ld) =
 
 let print_recursive_decl info fmt dl =
   let tm = check_termination dl in
-  let d, dl = match dl with d :: dl -> d, dl | [] -> assert false in
   fprintf fmt "Set Implicit Arguments.@\n";
-  fprintf fmt "@[<hov 2>Fixpoint ";
-  print_recursive_decl info tm fmt d; forget_tvs ();
-  List.iter
-    (fun d ->
-       fprintf fmt "@[<hov 2>with ";
-       print_recursive_decl info tm fmt d; forget_tvs ())
-    dl;
+  print_list_delim
+    ~start:(fun fmt () -> fprintf fmt "@[<hov 2>Fixpoint ")
+    ~stop:(fun fmt () -> fprintf fmt ".@\n")
+    ~sep:(fun fmt () -> fprintf fmt "@\n@[<hov 2>with ")
+    (fun fmt d -> print_recursive_decl info tm fmt d; forget_tvs ())
+    fmt dl;
   fprintf fmt "Unset Implicit Arguments.@\n@\n"
 
 let print_ind info fmt (pr,f) =

src/util/pp.ml

@@ -43,7 +43,7 @@ let print_list_or_default default sep print fmt = function
 let print_list_par sep pr fmt l =
   print_list sep (fun fmt x -> fprintf fmt "(%a)" pr x) fmt l
 
-let print_list_delim start stop sep pr fmt = function
+let print_list_delim ~start ~stop ~sep pr fmt = function
   | [] -> ()
   | l -> fprintf fmt "%a%a%a" start () (print_list sep pr) l stop ()
 

src/util/pp.mli

@@ -34,9 +34,9 @@ val print_list_par :
   (Format.formatter -> unit -> 'a) ->
   (Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
 val print_list_delim :
-  (Format.formatter -> unit -> unit) ->
-  (Format.formatter -> unit -> unit) ->
-  (Format.formatter -> unit -> unit) ->
+  start:(Format.formatter -> unit -> unit) ->
+  stop:(Format.formatter -> unit -> unit) ->
+  sep:(Format.formatter -> unit -> unit) ->
   (Format.formatter -> 'b -> unit) -> Format.formatter -> 'b list -> unit
 
 val print_pair_delim :

tests/test-jcf.why

 
-theory TestConstant
+theory TestPVS
 
-  constant a : int
-  constant b : int
-  constant c : int
+  use import int.Int
 
-  function f : int
-  function g : int
+(***
+  function f int : int
 
-  predicate p
+  axiom f_def: forall x: int. f(x) = x+1
 
-  goal G: a=0 && p
-end
+  goal G: forall x: int. f(x) > x
 
-theory TestCoq
-  use import list.List
-  use import list.Append
+  type t = A int (int, int) | B () | C
 
-  lemma append_nil: forall l: list 'a. Nil ++ l = l
-end
+  function g (x:int) : t = A x (x+1, x+2)
 
-theory Bijection
-  use export int.Int
-  function n : int
-  function f int : int
-  axiom dom_f : forall i: int. 0 <= i < n -> 0 <= f i < n
-  function g int : int
-  axiom gf : forall i: int. 0 <= i < n -> g (f i) = i
-end
+  goal G1: match g 1 with
+             | A x ((y,z) as p) -> y=1+1 /\ p = (2,3)
+             | B (() as p) -> p=()
+             | C -> false end
+***)
 
-theory Test1
-  function id (i: int) : int = i
-  clone import Bijection with function f = id, lemma dom_f
-  goal G: n > 4 -> g (id 4) = 4
-end
+  type elt
+  type tree = Null | Node tree elt tree
+
+  predicate contains (t: tree) (x: elt) = match t with
+    | Null       -> false
+    | Node l y r -> contains l x || x = y || contains r x
+  end
+
+  (* the size of a tree, to prove termination *)
+  function size (t: tree) : int = match t with
+    | Null       -> 0
+    | Node l _ r -> size2 l + size2 r + 1
+  end
+  with size2 (t: tree) : int = match t with
+    | Null       -> 0
+    | Node l _ r -> size l + size r + 1
+  end
+
+  function size3 (t: tree) : int = match t with
+    | Null       -> 0
+    | Node l _ r -> size2 l + size2 r + 1
+  end
+
+  type u = t
+  with t = A | B u
+
+(*
+  inductive even int =
+    | even0: even 0
+    | evens: forall n: int. even n -> even (n+2)
+*)
 
-theory Order
-  type t
-  predicate (<=) t t
+  lemma size_nonneg: forall t: tree. size t >= 0
 
-  axiom le_refl : forall x : t. x <= x
-  axiom le_asym : forall x y : t. x <= y -> y <= x -> x = y
-  axiom le_trans: forall x y z : t. x <= y -> y <= z -> x <= z
 end
 
 (*