tactique Gappa : mise en place

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

5 files changed, 373 insertions, 12 deletions

diff --git a/contrib/dp/Gappa.v b/contrib/dp/Gappa.v
new file mode 100644
index 000000000..2259cb269
--- /dev/null
+++ b/contrib/dp/Gappa.v
@@ -0,0 +1,122 @@
+Require Export ZArith.
+Require Export Reals.
+
+Inductive float :=
+  | Fzero : float
+  | Float (b : positive) (s : bool) (m : positive) (e : Z) : float.
+
+Fixpoint P2R (p : positive) :=
+  match p with
+  | xH => 1%R
+  | xO xH => 2%R
+  | xO t => (2 * P2R t)%R
+  | xI xH => 3%R
+  | xI t => (1 + 2 * P2R t)%R
+  end.
+
+Definition Z2R n :=
+  match n with
+  | Zpos p => P2R p
+  | Zneg p => Ropp (P2R p)
+  | Z0 => R0
+  end.
+
+Lemma IZR_Z2R :
+  forall x, IZR x = Z2R x.
+Admitted.
+
+Ltac get_float t :=
+  let get_mantissa t :=
+    let rec aux t :=
+      match t with
+      | 1%R => xH
+      | 2%R => constr:(xO xH)
+      | 3%R => constr:(xI xH)
+      | (2 * ?v)%R =>
+        let w := aux v in constr:(xO w)
+      | (1 + 2 * ?v)%R =>
+        let w := aux v in constr:(xI w)
+      end in
+    aux t in
+  let get_float_rational s n d :=
+    let rec aux t :=
+      match t with
+      | 2%R => xH
+      | (2 * ?v)%R =>
+        let w := aux v in
+        eval vm_compute in (Psucc w)
+      end in
+    let e := aux d in
+    let m := get_mantissa n in
+    eval vm_compute in (Float 2 s m (Zneg e)) in
+  let get_float_integer s t :=
+    let rec aux m e :=
+      match m with
+      | xO ?v =>
+        let u := eval vm_compute in (Zsucc e) in
+        aux v u
+      | _ => constr:(m, e)
+      end in
+    let m := get_mantissa t in
+    let v := aux m Z0 in
+    match v with
+    | (?m, ?e) => eval vm_compute in (Float 2 s m e)
+    end in
+  match t with
+  | 0%R => Fzero
+  | (-?n * /?d)%R => get_float_rational true n d
+  | (?n * /?d)%R => get_float_rational false n d
+  | (-?n / ?d)%R => get_float_rational true n d
+  | (?n / ?d)%R => get_float_rational false n d
+  | (-?n)%R => get_float_integer true n
+  | ?n => get_float_integer false n
+  | _ => false
+  end.
+
+Definition FtoR radix (s : bool) m e :=
+  let sm := if s then Zneg m else Zpos m in
+  match e with
+  | Zpos p => Z2R (sm * Zpower_pos (Zpos radix) p)
+  | Z0 => Z2R sm
+  | Zneg p => (Z2R sm / Z2R (Zpower_pos (Zpos radix) p))%R
+  end.
+
+Definition F2R f :=
+  match f with
+  | Fzero => R0
+  | Float b s m e => FtoR b s m e
+  end.
+
+Ltac get_term t :=
+  match get_float t with
+  | false =>
+    match t with
+    | (?a + ?b)%R =>
+      let a' := get_term a in
+      let b' := get_term b in
+      constr:(Rplus a' b')
+    | ?e => e
+    end
+  | ?f =>constr:(F2R f)
+  end.
+
+Ltac gappar :=
+  intros ; subst ;
+  repeat
+  match goal with
+  | H: (?a <= ?e <= ?b)%R |- _ =>
+    let a' := get_float a in
+    let b' := get_float b in
+    let e' := get_term e in
+    change (F2R a' <= e' <= F2R b')%R in H
+  | |- (?a <= ?e <= ?b)%R =>
+    let a' := get_float a in
+    let b' := get_float b in
+    let e' := get_term e in
+    change (F2R a' <= e' <= F2R b')%R
+  end.
+
+Ltac gappa2 :=
+  gappar;
+  gappa.
+
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 22fefa65d..b24ba55fb 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -37,6 +37,7 @@ let set_timeout n = timeout := n
 let logic_dir = ["Coq";"Logic";"Decidable"]
 let coq_modules =
   init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
+    @ [["Coq"; "ZArith"; "BinInt"]]
     @ [["Coq"; "omega"; "OmegaLemmas"]]
 
 let constant = gen_constant_in_modules "dp" coq_modules
diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml
new file mode 100644
index 000000000..65ec7124f
--- /dev/null
+++ b/contrib/dp/dp_gappa.ml
@@ -0,0 +1,226 @@
+
+open Format
+open Util
+open Pp
+open Term
+open Tacmach
+open Tactics
+open Tacticals
+open Names
+open Nameops
+open Termops
+open Coqlib
+open Hipattern
+open Libnames
+open Declarations
+
+(* 1. gappa syntax trees and output *)
+
+module Constant = struct
+
+  type t = { mantissa : int; base : int; exp : int }
+
+  let create (b, m, e) =
+    if b <> 2 && b <> 10 then invalid_arg "Constant.create";
+    { 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"
+
+  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
+    | _ -> assert false
+
+end
+
+type binop = Bminus | Bplus | Bmult | Bdiv
+
+type unop = Usqrt | Uabs | Uopp
+
+type term =
+  | Tconst of Constant.t
+  | Tvar of string
+  | Tbinop of binop * term * term
+  | Tunop of unop * term
+
+type pred =
+  | Pin of term * Constant.t * Constant.t
+
+let rec print_term fmt = function
+  | Tconst c -> Constant.print fmt c
+  | Tvar s -> pp_print_string fmt s
+  | Tbinop (op, t1, t2) -> 
+      let op = match op with 
+	| Bplus -> "+" | Bminus -> "-" | Bmult -> "*" | Bdiv -> "/"
+      in
+      fprintf fmt "(%a %s %a)" print_term t1 op print_term t2
+  | Tunop (Uabs, t) ->
+      fprintf fmt "|%a|" print_term t
+  | Tunop (Uopp | Usqrt as op, t) ->
+      let s = match op with 
+	| Uopp -> "-" | Usqrt -> "sqrt" | _ -> assert false 
+      in
+      fprintf fmt "(%s(%a))" s print_term t
+
+let print_pred fmt = function
+  | Pin (t, c1, c2) -> 
+      fprintf fmt "%a in [%a, %a]" 
+	print_term t Constant.print c1 Constant.print c2
+
+let call_gappa hl p =
+  let f = "test.gappa" in
+  let c = open_out f 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 out = Sys.command (sprintf "gappa < %s" f) in
+  msgnl (str ("gappa exit code is " ^ string_of_int out))
+
+(* 2. coq -> gappa translation *)
+
+exception NotGappa
+
+let logic_dir = ["Coq";"Logic";"Decidable"]
+let coq_modules =
+  init_modules @ [logic_dir] @ arith_modules @ zarith_base_modules
+    @ [["Coq"; "ZArith"; "BinInt"];
+       ["Coq"; "Reals"; "Rdefinitions"]; 
+       ["Coq"; "Reals"; "Raxioms";];
+       ["Coq"; "Reals"; "Rbasic_fun";];
+       ["Coq"; "Reals"; "R_sqrt";];
+       ["Coq"; "Reals"; "Rfunctions";];
+       ["Coq"; "dp"; "Gappa";];
+    ]
+
+let constant = gen_constant_in_modules "gappa" coq_modules
+
+let coq_Rle = lazy (constant "Rle")
+let coq_Rplus = lazy (constant "Rplus")
+let coq_Rminus = lazy (constant "Rminus")
+let coq_Rmult = lazy (constant "Rmult")
+let coq_Rdiv = lazy (constant "Rdiv")
+let coq_powerRZ = lazy (constant "powerRZ")
+let coq_R1 = lazy (constant "R1")
+let coq_Ropp = lazy (constant "Ropp")
+let coq_Rabs = lazy (constant "Rabs")
+let coq_sqrt = lazy (constant "sqrt")
+
+let coq_F2R = lazy (constant "F2R")
+let coq_Fzero = lazy (constant "Fzero")
+let coq_Float = lazy (constant "Float")
+
+let coq_true = lazy (constant "true")
+let coq_false = lazy (constant "false")
+
+let coq_Z0 = lazy (constant "Z0")
+let coq_Zpos = lazy (constant "Zpos")
+let coq_Zneg = lazy (constant "Zneg")
+let coq_xH = lazy (constant "xH")
+let coq_xI = lazy (constant "xI")
+let coq_xO = lazy (constant "xO")
+let coq_IZR = lazy (constant "IZR")
+
+(* translates a closed Coq term p:positive into a FOL term of type int *)
+let rec tr_positive p = match kind_of_term p with
+  | Term.Construct _ when p = Lazy.force coq_xH ->
+      1
+  | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
+      2 * (tr_positive a) + 1
+  | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
+      2 * (tr_positive a)
+  | Term.Cast (p, _, _) ->
+      tr_positive p
+  | _ ->
+      raise NotGappa
+
+(* 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
+  | _ -> 
+      raise NotGappa
+
+let decomp c = 
+  let c, args = decompose_app c in
+  kind_of_term c, args
+
+let tr_bool c = match decompose_app c with
+  | c, [] when c = Lazy.force coq_true -> true
+  | c, [] when c = Lazy.force coq_false -> false
+  | _ -> raise NotGappa
+
+let tr_float c = match decompose_app c with
+  | c, [] when c = Lazy.force coq_Fzero ->
+      (2,0,0)
+  | c, [b; s; m; e] when c = Lazy.force coq_Float ->
+      let m = tr_positive m in
+      let m' = if tr_bool s then - m else m in
+      (tr_positive b, m', tr_arith_constant e)
+  | _ ->
+      raise NotGappa
+
+let rec tr_term c0 = 
+  let c, args = decompose_app c0 in
+  match kind_of_term c, args with
+    | Var id, [] ->
+	Tvar (string_of_id id)
+    | _, [a] when c = Lazy.force coq_F2R ->
+	Tconst (Constant.create (tr_float a))
+    | _, [a;b] when c = Lazy.force coq_Rplus ->
+	Tbinop (Bplus, tr_term a, tr_term b)
+    | _, [a;b] when c = Lazy.force coq_Rminus ->
+	Tbinop (Bminus, tr_term a, tr_term b)
+    | _, [a;b] when c = Lazy.force coq_Rmult ->
+	Tbinop (Bmult, tr_term a, tr_term b)
+    | _, [a;b] when c = Lazy.force coq_Rdiv ->
+	Tbinop (Bmult, tr_term a, tr_term b)
+    | _, [a] when c = Lazy.force coq_sqrt ->
+	Tunop (Usqrt, tr_term a)
+    | _, [a] when c = Lazy.force coq_Rabs ->
+	Tunop (Uabs, tr_term a)
+    | _, [a] when c = Lazy.force coq_Ropp ->
+	Tunop (Uopp, tr_term a)
+    | _ -> 
+	msgnl (str "tr_term: " ++ Printer.pr_constr c0); raise NotGappa
+
+let tr_rle c = 
+  let c, args = decompose_app c in
+  match kind_of_term c, args with
+   | _, [a;b] when c = Lazy.force coq_Rle -> tr_term a, tr_term b
+   | _ -> raise NotGappa
+
+let tr_pred c =
+  let c, args = decompose_app c in
+  match kind_of_term c, args with
+    | _, [a;b] when c = build_coq_and () ->
+	begin match tr_rle a, tr_rle b with
+	  | (Tconst c1, t1), (t2, Tconst c2) when t1 = t2 -> Pin (t1,c1,c2)
+	  | _ -> raise NotGappa
+	end
+    | _ -> raise NotGappa
+
+let tr_hyps =
+  List.fold_left 
+    (fun acc (_,h) -> try tr_pred h :: acc with NotGappa -> acc) []
+
+let gappa gl =
+  try
+    let c = tr_pred (pf_concl gl) in
+    call_gappa (tr_hyps (pf_hyps_types gl)) c;
+    Tacticals.tclIDTAC gl
+  with NotGappa ->
+    error "not a gappa goal"
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index 9f5fe5be9..f7c5135bd 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -40,6 +40,10 @@ TACTIC EXTEND Gwhy
   [ "gwhy" ] -> [ gwhy ]
 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/tests.v b/contrib/dp/tests.v
index 0284623c4..61de5d81c 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -5,21 +5,29 @@ Require Import Classical.
 Dp_debug.
 Dp_timeout 3.
 
+(* Coq lists *)
 
-Inductive expr: Set := Some: expr -> expr -> expr | None: expr. 
-Parameter depth: expr -> expr -> nat. 
+Require Export List.
+Parameter nlist: list nat -> Prop.
 
-Fixpoint length (t: expr) : nat :=
-  match t with
-  | None => 0
-  | Some t1 t2 => depth t t1
-  end.
+ Goal forall l,  nlist l -> True.
+ intros. 
+ simplify.
 
-Goal forall e, length e = 0. 
-intros. 
-gwhy.
-ergo.
-Qed.
+(* user lists *)
+
+Inductive list (A:Set) : Set :=
+| nil : list A
+| cons: forall a:A, list A -> list A.
+
+Fixpoint app (A:Set) (l m:list A) {struct l} : list A :=
+match l with
+| nil => m
+| cons a l1 => cons A a (app A l1 m)
+end.
+
+Lemma entail: (nil Z) = app Z (nil Z) (nil Z) -> True. 
+intros; ergo. 
 
 
 (* polymorphism *)