*** empty log message ***

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

6 files changed, 187 insertions, 106 deletions

diff --git a/contrib/dp/.cvsignore b/contrib/dp/.cvsignore
new file mode 100644
index 000000000..27102315a
--- /dev/null
+++ b/contrib/dp/.cvsignore
@@ -0,0 +1,2 @@
+test.why
+test_why*
diff --git a/contrib/dp/TODO b/contrib/dp/TODO
new file mode 100644
index 000000000..387cacdf3
--- /dev/null
+++ b/contrib/dp/TODO
@@ -0,0 +1,28 @@
+
+TODO
+----
+
+- axiomes pour les prédicats récursifs comme
+
+  Fixpoint even (n:nat) : Prop :=
+  match n with 
+  O => True
+  | S O => False
+  | S (S p) => even p
+  end.
+
+  ou encore In sur les listes du module Coq List.
+
+- discriminate
+
+- inversion (Set et Prop)
+
+
+BUGS
+----
+
+- value = Some : forall A:Set, A -> option A
+
+  -> eta_expanse échoue sur assert false (ligne 147)
+
+
diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index a9d450f75..6f6a5a803 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -231,19 +231,35 @@ let term_abstractions = Hashtbl.create 97
 let new_abstraction = 
   let r = ref 0 in fun () -> incr r; "abstraction_" ^ string_of_int !r
 
-(* translates a Coq term p:positive into a FOL term of type int *)
-let rec fol_term_of_positive tv env p =
-  match kind_of_term p with
-    | Term.Construct _ when p = Lazy.force coq_xH ->
-	Cst 1
-    | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
-	Plus (Mult (Cst 2, (fol_term_of_positive tv env a)), Cst 1)
-    | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
-	Mult (Cst 2, (fol_term_of_positive tv env a))
-    | Var id ->
-	Fol.App (string_of_id id, [])
-    | _ ->
-	tr_term tv [] env p
+(* Arithmetic constants *)
+
+exception NotArithConstant
+
+(* 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 ->
+      Cst 1
+  | Term.App (f, [|a|]) when f = Lazy.force coq_xI ->
+      Plus (Mult (Cst 2, tr_positive a), Cst 1)
+  | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
+      Mult (Cst 2, tr_positive a)
+  | Term.Cast (p, _, _) ->
+      tr_positive p
+  | _ ->
+      raise NotArithConstant
+
+(* translates a closed Coq term t:Z into a FOL term of type int *)
+let rec tr_arith_constant t = match kind_of_term t with
+  | Term.Construct _ when t = Lazy.force coq_Z0 ->
+      Cst 0
+  | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos ->
+      tr_positive a
+  | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
+      Moins (Cst 0, tr_positive a)
+  | Term.Cast (t, _, _) ->
+      tr_arith_constant t
+  | _ -> 
+      raise NotArithConstant
 
 (* translate a Coq term t:Set into a FOL type expression;
    tv = list of type variables *)
@@ -272,54 +288,6 @@ and tr_type tv env t =
 	      raise NotFO
 	end
 
-(**** OLD TR_TYPE
-  else if is_Prop ty then [], Tid ("BOOLEAN", [])
-  else if is_Set ty then [], Tid ("TYPE", [])
-  else if is_imp_term ty then 
-    begin match match_with_imp_term ty with
-      | Some (t1, t2) -> begin match tr_type tv env t1, tr_type tv env t2 with
-	  | ([], t1'), (l2, t2') -> t1' :: l2, t2'
-	  | _ -> raise NotFO
-	end
-      | _ -> assert false
-    end
-  else
-    try let r = global_of_constr ty in
-    (try
-       begin match lookup_global r with
-	 | DeclType (id,0) -> [], Tid (id,[])
-	 | _ -> assert false (* assumption: t:Set *)
-       end
-     with Not_found ->
-       begin match r with
-	 | IndRef i ->
-	     let id = rename_global r in
-	     let d = DeclType (id,0) in
-	     add_global r (Gfo d);
-	     globals_stack := d :: !globals_stack;
-	     iter_all_constructors i
-	       (fun _ c ->
-		  let rc = global_of_constr c in
-		  try
-		    begin match tr_global env rc with
-		      | DeclFun (idc, [], _) -> ()
-		      | DeclFun (idc, al, _) -> injection idc al
-		      | _ -> assert false
-		    end
-		  with NotFO ->
-		    ());
-	     [], Tid (id,[])
-	 | _ -> 
-	     let id = rename_global r in
-	     let d = DeclType (id,0) in
-	     add_global r (Gfo d);
-	     globals_stack := d :: !globals_stack;
-	     [], Tid (id,[])
-	     (* TODO: constant type definition *)
-       end)
-    with Not_found -> raise NotFO
-***)
-
 and make_term_abstraction tv env c =
   let ty = Typing.type_of env Evd.empty c in
   let id = new_abstraction () in
@@ -404,6 +372,7 @@ and axiomatize_body env r id d = match r with
 		     let value = tr_term tv [] env b in
 		     [id, Fatom (Eq (Fol.App (id, []), value))]
 		 | DeclFun (id, _, l, _) | DeclPred (id, _, l) ->
+		     Format.eprintf "axiomatize_body %S@." id;
 		     let b = match kind_of_term b with
 		       (* a single recursive function *)
 		       | Fix (_, (_,_,[|b|])) -> 
@@ -528,27 +497,22 @@ and equations_for_case env id vars tv bv ci e br = match kind_of_term e with
   | _ ->
       raise NotFO
 
-
 (* assumption: t:T:Set *)
-and tr_term tv bv env t =
-  match kind_of_term t with
-    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> 
-	Plus (tr_term tv bv env a, tr_term tv bv env b)
-    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> 
-	Moins (tr_term tv bv env a, tr_term tv bv env b)
-    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> 
-	Mult (tr_term tv bv env a, tr_term tv bv env b)
-    | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> 
-	Div (tr_term tv bv env a, tr_term tv bv env b)
-    | Term.Construct _ when t = Lazy.force coq_Z0 ->
-	Cst 0
-    | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos ->
-	fol_term_of_positive tv env a
-    | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
-	Moins (Cst 0, (fol_term_of_positive tv env a))
-    | Term.Var id when List.mem id bv ->
-	App (string_of_id id, [])
-    | _ ->
+and tr_term tv bv env t = match kind_of_term t with
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> 
+      Plus (tr_term tv bv env a, tr_term tv bv env b)
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> 
+      Moins (tr_term tv bv env a, tr_term tv bv env b)
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> 
+      Mult (tr_term tv bv env a, tr_term tv bv env b)
+  | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> 
+      Div (tr_term tv bv env a, tr_term tv bv env b)
+  | Term.Var id when List.mem id bv ->
+      App (string_of_id id, [])
+  | _ ->
+      try
+	tr_arith_constant t
+      with NotArithConstant ->
 	let f, cl = decompose_app t in
 	begin try
 	  let r = global_of_constr f in
diff --git a/contrib/dp/dp_why.ml b/contrib/dp/dp_why.ml
index d6a5e145c..662a5a8be 100644
--- a/contrib/dp/dp_why.ml
+++ b/contrib/dp/dp_why.ml
@@ -12,16 +12,28 @@ let rec print_list sep print fmt = function
 let space fmt () = fprintf fmt "@ "
 let comma fmt () = fprintf fmt ",@ "
 
-let is_why_keyword s = false (* TODO *)
+let is_why_keyword = 
+  let h = Hashtbl.create 17 in
+  List.iter 
+    (fun s -> Hashtbl.add h s ())
+    ["absurd"; "and"; "array"; "as"; "assert"; "axiom"; "begin";
+     "bool"; "do"; "done"; "else"; "end"; "exception"; "exists";
+     "external"; "false"; "for"; "forall"; "fun"; "function"; "goal";
+     "if"; "in"; "int"; "invariant"; "label"; "let"; "logic"; "not";
+     "of"; "or"; "parameter"; "predicate"; "prop"; "raise"; "raises";
+     "reads"; "real"; "rec"; "ref"; "returns"; "then"; "true"; "try";
+     "type"; "unit"; "variant"; "void"; "while"; "with"; "writes" ]; 
+  Hashtbl.mem h
 
 let ident fmt s =
-  if is_why_keyword s then fprintf fmt "why__%s" s else fprintf fmt "%s" s
+  if is_why_keyword s then fprintf fmt "coq__%s" s else fprintf fmt "%s" s
 
 let rec print_typ fmt = function
-  | Tvar x -> fprintf fmt "'%s" x
-  | Tid (x, []) -> fprintf fmt "%s" x
-  | Tid (x, [t]) -> fprintf fmt "%a %s" print_typ t x
-  | Tid (x, tl) -> fprintf fmt "(%a) %s" (print_list comma print_typ) tl x
+  | Tvar x -> fprintf fmt "'%a" ident x
+  | Tid ("int", []) -> fprintf fmt "int"
+  | Tid (x, []) -> fprintf fmt "%a" ident x
+  | Tid (x, [t]) -> fprintf fmt "%a %a" print_typ t ident x
+  | Tid (x,tl) -> fprintf fmt "(%a) %a" (print_list comma print_typ) tl ident x
 
 let rec print_term fmt = function
   | Cst n -> 
@@ -79,40 +91,42 @@ let rec print_predicate fmt p =
 let print_query fmt (decls,concl) =
   let print_dtype = function
     | DeclType (id, 0) ->
-	fprintf fmt "@[type %s@]@\n@\n" id
+	fprintf fmt "@[type %a@]@\n@\n" ident id
     | DeclType (id, 1) ->
-	fprintf fmt "@[type 'a %s@]@\n@\n" id
+	fprintf fmt "@[type 'a %a@]@\n@\n" ident id
     | DeclType (id, n) ->
 	fprintf fmt "@[type (";
-	for i = 1 to n do fprintf fmt "'a%d" i done;
-	fprintf fmt ") %s@]@\n@\n" id
+	for i = 1 to n do 
+	  fprintf fmt "'a%d" i; if i < n then fprintf fmt ", "
+	done;
+	fprintf fmt ") %a@]@\n@\n" ident id
     | DeclFun _ | DeclPred _ | Axiom _ ->
 	()
   in
   let print_dvar_dpred = function
     | DeclFun (id, _, [], t) ->
-	fprintf fmt "@[logic %s : -> %a@]@\n@\n" id print_typ t
+	fprintf fmt "@[logic %a : -> %a@]@\n@\n" ident id print_typ t
     | DeclFun (id, _, l, t) ->
-	fprintf fmt "@[logic %s : %a -> %a@]@\n@\n" 
-	  id (print_list comma print_typ) l print_typ t
+	fprintf fmt "@[logic %a : %a -> %a@]@\n@\n" 
+	  ident id (print_list comma print_typ) l print_typ t
     | DeclPred (id, _, []) ->
-	fprintf fmt "@[logic %s : -> prop @]@\n@\n" id
+	fprintf fmt "@[logic %a : -> prop @]@\n@\n" ident id
     | DeclPred (id, _, l) -> 
-	fprintf fmt "@[logic %s : %a -> prop@]@\n@\n" 
-	  id (print_list comma print_typ) l
+	fprintf fmt "@[logic %a : %a -> prop@]@\n@\n" 
+	  ident id (print_list comma print_typ) l
     | DeclType _ | Axiom _ ->
 	()
   in
   let print_assert = function
     | Axiom (id, f)  -> 
-	fprintf fmt "@[<hov 2>axiom %s:@ %a@]@\n@\n" id print_predicate f
+	fprintf fmt "@[<hov 2>axiom %a:@ %a@]@\n@\n" ident id print_predicate f
     | DeclType _ | DeclFun _ | DeclPred _ ->
 	()
   in
   List.iter print_dtype decls;
   List.iter print_dvar_dpred decls;
   List.iter print_assert decls;
-  fprintf fmt "@[<hov 2>goal coq__goal: %a@]" print_predicate concl
+  fprintf fmt "@[<hov 2>goal coq___goal: %a@]" print_predicate concl
 
 let output_file f q =
   let c = open_out f in
diff --git a/contrib/dp/test2.v b/contrib/dp/test2.v
new file mode 100644
index 000000000..59f8807f9
--- /dev/null
+++ b/contrib/dp/test2.v
@@ -0,0 +1,73 @@
+Require Import ZArith.
+Require Import Classical.
+Require Import List.
+
+Open Scope list_scope.
+Open Scope Z_scope.
+
+Definition neg (z:Z) : Z := match z with
+  | Z0 => Z0
+  | Zpos p => Zneg p
+  | Zneg p => Zpos p
+  end.
+
+Goal forall z, neg (neg z) = z.
+  zenon.
+  Admitted.
+
+Open Scope nat_scope.
+Print plus.
+
+Goal forall x, x+0=x.
+  induction x; zenon.
+  (* simplify resoud le premier, pas le second *)
+  Admitted.
+
+Goal 1::2::3::nil = 1::2::(1+2)::nil.
+  zenon.
+  Admitted.
+
+Fixpoint even (n:nat) : Prop :=
+  match n with 
+  O => True
+  | S O => False
+  | S (S p) => even p
+  end.
+
+Goal even 4%nat.
+  zenon.
+  Admitted.
+
+Definition p (A B:Set) (a:A) (b:B) : list (A*B) := cons (a,b) nil.
+
+Definition head :=
+fun (A : Set) (l : list A) =>
+match l with
+| nil => None (A:=A)
+| x :: _ => Some x
+end.
+
+Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
+
+zenon.
+Admitted.
+
+(*
+BUG avec head prédéfini : manque eta-expansion sur A:Set
+
+Goal forall x, head _ (p _ _ 1 2) = Some x -> fst x = 1.
+
+Print value. 
+Print Some.
+ 
+zenon.
+*)
+
+Inductive IN (A:Set) : A -> list A -> Prop :=
+  | IN1 : forall x l, IN A x (x::l)
+  | IN2: forall x l, IN A x l -> forall y, IN A x (y::l).
+Implicit Arguments IN [A].
+
+Goal forall x, forall (l:list nat), IN x l -> IN x (1%nat::l).
+  zenon.
+Print In.
diff --git a/contrib/dp/tests.v b/contrib/dp/tests.v
index 10b6f0d83..222d08cc8 100644
--- a/contrib/dp/tests.v
+++ b/contrib/dp/tests.v
@@ -1,4 +1,3 @@
-Reset Initial.
 
 Require Import ZArith.
 Require Import Classical.
@@ -64,10 +63,11 @@ Goal (forall (x y : Z), x = y) -> 0 = 1.
 simplify.
 Qed.
 
+Goal forall (x: nat), (x + 0 = x)%nat.
 
-Goal forall (x y : Z), x + y = y + x.
-
-induction x ; simplify.
+induction x0.
+zenon.
+zenon.
 Qed.
 
 
@@ -98,7 +98,7 @@ simplify.
 Qed.
 
 
-(* Inductive types definitions - call to injection function *)
+(* Inductive types definitions - call to incontrib/dp/jection function *)
 
 Inductive even : Z -> Prop :=
 | even_0 : even 0
@@ -185,9 +185,9 @@ Qed.
 (* sorts issues *)
 
 Parameter foo : Set.         
-Parameter f : nat -> foo -> foo -> nat.
+Parameter ff : nat -> foo -> foo -> nat.
 Parameter g : foo -> foo.
-Goal (forall x:foo, f 0 x x = O) -> forall y, f 0 (g y) (g y) = O.
+Goal (forall x:foo, ff 0 x x = O) -> forall y, ff 0 (g y) (g y) = O.
 simplify.      
 Qed.