tactique gappa

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10810 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 106 insertions, 53 deletions

diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml
index 053622712..70439a970 100644
--- a/contrib/dp/dp_gappa.ml
+++ b/contrib/dp/dp_gappa.ml
@@ -15,26 +15,26 @@ open Libnames
 open Declarations
 open Evarutil
 
+let debug = ref false
+
 (* 1. gappa syntax trees and output *)
 
 module Constant = struct
 
-  type t = { mantissa : int; base : int; exp : int }
+  open Bigint
+
+  type t = { mantissa : bigint; base : int; exp : bigint }
 
   let create (b, m, e) =
     { mantissa = m; base = b; exp = e }
 
   let of_int x = 
-    { mantissa = x; base = 1; exp = 0 }
-
-  let mult x y =
-    if x.base = 1 then { y with mantissa = x.mantissa * y.mantissa }
-    else invalid_arg "Constant.mult"
+    { mantissa = x; base = 1; exp = zero }
 
   let print fmt x = match x.base with
-    | 1 -> fprintf fmt "%d" x.mantissa
-    | 2 -> fprintf fmt "%db%d" x.mantissa x.exp
-    | 10 -> fprintf fmt "%de%d" x.mantissa x.exp
+    | 1 -> fprintf fmt "%s" (to_string x.mantissa)
+    | 2 -> fprintf fmt "%sb%s" (to_string x.mantissa) (to_string x.exp)
+    | 10 -> fprintf fmt "%se%s" (to_string x.mantissa) (to_string x.exp)
     | _ -> assert false
 
 end
@@ -78,6 +78,9 @@ let print_pred fmt = function
       fprintf fmt "%a in [%a, %a]" 
 	print_term t Constant.print c1 Constant.print c2
 
+let temp_file f = if !debug then f else Filename.temp_file f ".v"
+let remove_file f = if not !debug then try Sys.remove f with _ -> ()
+
 let read_gappa_proof f =
   let buf = Buffer.create 1024 in
   Buffer.add_char buf '(';
@@ -97,6 +100,8 @@ let read_gappa_proof f =
     done;
     assert false
   with Exit ->
+    close_in cin;
+    remove_file f;
     Buffer.add_char buf ')';
     Buffer.contents buf
 
@@ -132,34 +137,38 @@ let patch_gappa_proof fin fout =
     fprintf fmt "Definition proof := Eval cbv delta [%s] in %s.@." !defs !last;
     close_out cout
     
-
 let call_gappa hl p =
-  let gappa_in = "test.gappa" in
+  let gappa_in = temp_file "gappa_input" in
   let c = open_out gappa_in in
   let fmt = formatter_of_out_channel c in
   fprintf fmt "@[{ "; 
   List.iter (fun h -> fprintf fmt "%a ->@ " print_pred h) hl;
   fprintf fmt "%a }@]@." print_pred p;
   close_out c;
-  let gappa_out = "gappa.v" in
-  let cmd = sprintf "gappa -Bcoq < %s > %s" gappa_in gappa_out in
+  let gappa_out = temp_file "gappa_output" in
+  let cmd = sprintf "gappa -Bcoq < %s > %s 2> /dev/null" gappa_in gappa_out in
   let out = Sys.command cmd in
   if out <> 0 then raise GappaFailed;
-  let gappa_out2 = "gappa2.v" in
+  remove_file gappa_in;
+  let gappa_out2 = temp_file "gappa2" in
   patch_gappa_proof gappa_out gappa_out2;
-  let lambda = "test.lambda" in
+  remove_file gappa_out;
   let cmd = sprintf "%s/coqc %s" Coq_config.bindir gappa_out2 in
   let out = Sys.command cmd in
   if out <> 0 then raise GappaProofFailed;
-  let gappa_out3 = "gappa3.v" in
+  let gappa_out3 = temp_file "gappa3" in
   let c = open_out gappa_out3 in
-  let gappa2 = Filename.chop_suffix gappa_out2 ".v" in
+  let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in
   Printf.fprintf c 
-    "Require %s. Set Printing Depth 9999999. Print %s.proof." gappa2 gappa2;
+    "Require \"%s\". Set Printing Depth 9999999. Print %s.proof." 
+    (Filename.chop_suffix gappa_out2 ".v") gappa2;
   close_out c;
+  let lambda = temp_file "gappa_lambda" in
   let cmd = sprintf "%s/coqc %s > %s" Coq_config.bindir gappa_out3 lambda in
   let out = Sys.command cmd in
   if out <> 0 then raise GappaProofFailed;
+  remove_file gappa_out2; remove_file gappa_out3;
+  remove_file (gappa_out2 ^ "o"); remove_file (gappa_out3 ^ "o");
   read_gappa_proof lambda
 
 (* 2. coq -> gappa translation *)
@@ -203,6 +212,7 @@ let coq_sqrt = lazy (constant "sqrt")
 let coq_convert = lazy (constant "convert")
 let coq_reUnknown = lazy (constant "reUnknown")
 let coq_reFloat2 = lazy (constant "reFloat2")
+let coq_reFloat10 = lazy (constant "reFloat10")
 let coq_reInteger = lazy (constant "reInteger")
 let coq_reBinary = lazy (constant "reBinary")
 let coq_reUnary = lazy (constant "reUnary")
@@ -249,17 +259,34 @@ let rec tr_positive p = match kind_of_term p with
 
 (* translates a closed Coq term t:Z into a term of type int *)
 let rec tr_arith_constant t = match kind_of_term t with
-  | Term.Construct _ when t = Lazy.force coq_Z0 ->
-      0
-  | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos ->
-      tr_positive a
-  | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
-      - (tr_positive a)
-  | Term.Cast (t, _, _) ->
-      tr_arith_constant t
-  | _ -> 
+  | Term.Construct _ when t = Lazy.force coq_Z0 -> 0
+  | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_positive a
+  | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> - (tr_positive a)
+  | Term.Cast (t, _, _) -> tr_arith_constant t
+  | _ -> raise NotGappa
+
+(* translates a closed Coq term p:positive into a FOL term of type bigint *)
+let rec tr_bigpositive p = match kind_of_term p with
+  | Term.Construct _ when p = Lazy.force coq_xH -> 
+      Bigint.one
+  | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
+      Bigint.add_1 (Bigint.mult_2 (tr_bigpositive a))
+  | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
+      (Bigint.mult_2 (tr_bigpositive a))
+  | Term.Cast (p, _, _) ->
+      tr_bigpositive p
+  | _ ->
       raise NotGappa
 
+(* translates a closed Coq term t:Z into a term of type bigint *)
+let rec tr_arith_bigconstant t = match kind_of_term t with
+  | Term.Construct _ when t = Lazy.force coq_Z0 -> Bigint.zero
+  | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos -> tr_bigpositive a
+  | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg -> 
+      Bigint.neg (tr_bigpositive a)
+  | Term.Cast (t, _, _) -> tr_arith_bigconstant t
+  | _ -> raise NotGappa
+
 let decomp c = 
   let c, args = decompose_app c in
   kind_of_term c, args
@@ -270,7 +297,7 @@ let tr_bool c = match decompose_app c with
   | _ -> raise NotGappa
 
 let tr_float b m e =
-  (b, tr_arith_constant m, tr_arith_constant e)
+  (b, tr_arith_bigconstant m, tr_arith_bigconstant e)
 
 let tr_binop c = match decompose_app c with
   | c, [] when c = Lazy.force coq_boAdd -> Bplus
@@ -317,8 +344,10 @@ let rec tr_term c0 =
 	Tvar (tr_var a)
     | _, [a; b] when c = Lazy.force coq_reFloat2 ->
 	Tconst (Constant.create (tr_float 2 a b))
+    | _, [a; b] when c = Lazy.force coq_reFloat10 ->
+	Tconst (Constant.create (tr_float 10 a b))
     | _, [a] when c = Lazy.force coq_reInteger ->
-	Tconst (Constant.create (1, tr_arith_constant a, 0))
+	Tconst (Constant.create (1, tr_arith_bigconstant a, Bigint.zero))
     | _, [op;a;b] when c = Lazy.force coq_reBinary ->
 	Tbinop (tr_binop op, tr_term a, tr_term b)
     | _, [op;a] when c = Lazy.force coq_reUnary ->
@@ -383,33 +412,31 @@ let var_name = function
 
 let build_proof_term c0 =
   let bl,c = decompose_lam c0 in
-  let c = 
-    List.fold_right 
-      (fun (x,t) pf -> 
-	mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |]))
-      bl c0
-  in
-  mkApp 
-    (Lazy.force coq_subset, 
-    [| mk_new_meta (); mk_new_meta (); 
-       mkApp (Lazy.force coq_makepairF, [| mk_new_meta(); mk_new_meta() |]);
-       c; mk_new_meta () |])
+  List.fold_right 
+    (fun (x,t) pf -> 
+      mkApp (pf, [| if is_R t then var_name x else mk_new_meta () |]))
+    bl c0
 
 let gappa_internal gl =
   try
     let c = tr_pred (pf_concl gl) in
     let s = call_gappa (tr_hyps (pf_hyps_types gl)) c in
-    msgnl (str s);
     let pf = constr_of_string gl s in
     let pf = build_proof_term pf in
-    Tacticals.tclTHEN (Tactics.refine pf) 
-      (Tacticals.tclORELSE Tactics.assumption Tactics.reflexivity)
-      gl
+    Tacticals.tclTHEN (Tacmach.refine_no_check pf) Tactics.assumption gl
   with 
     | NotGappa -> error "not a gappa goal"
     | GappaFailed -> error "gappa failed"
     | GappaProofFailed -> error "incorrect gappa proof term"
 
+let gappa_prepare =
+  let id = Ident (dummy_loc, id_of_string "gappa_prepare") in
+  lazy (Tacinterp.interp (Tacexpr.TacArg (Tacexpr.Reference id)))
+
+let gappa gl =
+  Coqlib.check_required_library ["Gappa"; "Gappa_tactic"];
+  Tacticals.tclTHEN (Lazy.force gappa_prepare) gappa_internal gl
+
 (*
 Local Variables: 
 compile-command: "make -C ../.. bin/coqc.opt bin/coqide.opt"
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 7acbce26d..1454ec0dd 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -40,10 +40,14 @@ TACTIC EXTEND Gwhy
   [ "gwhy" ] -> [ gwhy ]
 END
 
-TACTIC EXTEND Gappa
+TACTIC EXTEND Gappa_internal
   [ "gappa_internal" ] -> [ Dp_gappa.gappa_internal ]
 END
 
+TACTIC EXTEND Gappa
+  [ "gappa" ] -> [ Dp_gappa.gappa ]
+END
+
 (* should be part of basic tactics syntax *)
 TACTIC EXTEND admit
   [ "admit"    ] -> [ Tactics.admit_as_an_axiom ]
diff --git a/contrib/dp/test_gappa.v b/contrib/dp/test_gappa.v
index 6fa4e8c96..eb65a59d6 100644
--- a/contrib/dp/test_gappa.v
+++ b/contrib/dp/test_gappa.v
@@ -4,7 +4,34 @@ Require Export Reals.
 Open Scope Z_scope.
 Open Scope R_scope.
 
-Ltac gappa := gappa_prepare; gappa_internal.
+Lemma test_base10 : 
+  forall x y:R,
+  0 <= x <= 4 -> 
+  0 <= x * (24 * powerRZ 10 (-1)) <= 10.
+Proof.
+  gappa.
+Qed.
+
+(*
+@rnd = float< ieee_32, zr >;
+a = rnd(a_); b = rnd(b_);
+{ a in [3.2,3.3] /\ b in [1.4,1.9] ->
+  rnd(a - b) - (a - b) in [0,0] }
+*)
+
+Definition rnd := gappa_rounding (rounding_float roundZR 43 (120)).
+
+Lemma test_float3 :
+  forall a_ b_ a b : R,
+  a = rnd a_ ->
+  b = rnd b_ ->
+  52 / 16 <= a <= 53 / 16 ->
+  22 / 16 <= b <= 30 / 16 ->
+  0 <= rnd (a - b) - (a - b) <= 0.
+Proof.
+  unfold rnd.
+  gappa.
+Qed.
 
 Lemma test_float2 :
   forall x y:R,
@@ -13,18 +40,13 @@ Lemma test_float2 :
   0 <= gappa_rounding (rounding_float roundNE 53 (1074)) (x+y) <= 2. 
 Proof.
   gappa.
-
-
-  gappa_prepare.
-  refine (subset _ _ (makepairF _ _) (gappa2.proof x y _ _) _); auto.
 Qed.
 
-
 Lemma test_float1 :
   forall x y:R,
   0 <= gappa_rounding (rounding_fixed roundDN (0)) x -
            gappa_rounding (rounding_fixed roundDN (0)) y <= 0 ->
-  0 <= Rabs (x - y) <= 1.
+  Rabs (x - y) <= 1.
 Proof.
   gappa.
 Qed.
@@ -40,7 +62,7 @@ Qed.
 
 Lemma test2 : 
   forall x y:R,
-  0 <= x <= 3 -> 
+  3/4 <= x <= 3 -> 
   0 <= sqrt x <= 1775 * (powerRZ 2 (-10)).
 Proof.
   gappa.