Gestion du forall et envoie d'axiome à la procédure

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

5 files changed, 182 insertions, 73 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 961dd1c4c..24744e768 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -6,6 +6,8 @@ open Util
 open Pp
 open Term
 open Tacmach
+open Tactics
+open Tacticals
 open Fol
 open Names
 open Nameops
@@ -70,6 +72,10 @@ let rename_global r =
 let foralls =
   List.fold_right (fun (x,t) p -> Forall (rename_global (VarRef x), t, p))
 
+let fresh_var = function
+  | Anonymous -> rename_global (VarRef (id_of_string "x"))
+  | Name x -> rename_global (VarRef x)
+
 (* coq_rename_vars env [(x1,t1);...;(xn,tn)] renames the xi outside of 
    env names, and returns the new variables together with the new 
    environment *)
@@ -82,23 +88,20 @@ let coq_rename_vars env vars =
        id :: newvars, Environ.push_named (id, None, t) newenv)
     vars ([],env)
 
-(* assumption: t:Set *)
-let rec tr_type env ty =
-  if ty = Lazy.force coq_Z then [], "INT"
-  else if is_Prop ty then [], "BOOLEAN"
-  else if is_Set ty then [], "TYPE"
-  else if is_imp_term ty then 
-    begin match match_with_imp_term ty with
-      | Some (t1, t2) -> begin match tr_type env t1, tr_type env t2 with
-	  | ([], t1'), (l2, t2') -> t1' :: l2, t2'
-	  | _ -> raise NotFO
-	end
-      | _ -> assert false
-    end
-  else match kind_of_term ty with
-    | Var id -> [], rename_global (VarRef id)
-    | Ind i -> [], rename_global (IndRef i)
-    | _ -> raise NotFO
+let rec eta_expanse t vars env i =
+  assert (i >= 0);
+  if i = 0 then
+    t, vars, env
+  else
+    match kind_of_term (Typing.type_of env Evd.empty t) with
+      | Prod (n, a, b) when not (dependent (mkRel 1) b) ->
+	  let avoid = ids_of_named_context (Environ.named_context env) in
+	  let id = next_name_away n avoid in
+	  let env' = Environ.push_named (id, None, a) env in
+	  let t' = mkApp (t, [| mkVar id |]) in
+	  eta_expanse t' (id :: vars) env' (pred i)
+      | _ -> 
+	  assert false
 
 (* assumption : p:Z *)
 let rec fol_term_of_positive p =
@@ -110,7 +113,7 @@ let rec fol_term_of_positive p =
     | Term.App (f, [|a|]) when f = Lazy.force coq_xO ->
 	Mult (Cst 2, (fol_term_of_positive a))
     | Var id ->
-	Tvar (rename_global (VarRef id))
+	Fol.App (rename_global (VarRef id), [])
     | _ -> 
 	assert false
 
@@ -118,15 +121,74 @@ let rec fol_term_of_positive p =
 
 type global = Gnot_fo | Gfo of Fol.hyp
 
-let globals = Hashtbl.create 97
+let globals = ref Refmap.empty
 let globals_stack = ref []
+
+(* synchronization *)
+let () =
+  Summary.declare_summary "Dp globals"
+    { Summary.freeze_function = (fun () -> !globals, !globals_stack);
+      Summary.unfreeze_function = 
+	(fun (g,s) -> globals := g; globals_stack := s);
+      Summary.init_function = (fun () -> ());
+      Summary.survive_module = false;
+      Summary.survive_section = false }
+
+let add_global r d = globals := Refmap.add r d !globals
+let mem_global r = Refmap.mem r !globals
+let lookup_global r = match Refmap.find r !globals with
+  | Gnot_fo -> raise NotFO
+  | Gfo d -> d
+
 let locals = Hashtbl.create 97
 
-let lookup t r =  match Hashtbl.find t r with
+let lookup_local r =  match Hashtbl.find locals r with
   | Gnot_fo -> raise NotFO
   | Gfo d -> d
 
-let rec tr_global_type env id ty =
+(* assumption: t:Set *)
+let rec tr_type env ty =
+  if ty = Lazy.force coq_Z then [], "INT"
+  else if is_Prop ty then [], "BOOLEAN"
+  else if is_Set ty then [], "TYPE"
+  else if is_imp_term ty then 
+    begin match match_with_imp_term ty with
+      | Some (t1, t2) -> begin match tr_type env t1, tr_type env t2 with
+	  | ([], t1'), (l2, t2') -> t1' :: l2, t2'
+	  | _ -> raise NotFO
+	end
+      | _ -> assert false
+    end
+  else let r = reference_of_constr ty in
+  try
+    begin match lookup_global r with
+      | DeclType id -> [], id
+      | _ -> assert false (* ty is a type for sure ? *)
+    end
+  with Not_found ->
+    let id = rename_global r in
+    let d = DeclType id in
+    add_global r (Gfo d);
+    globals_stack := d :: !globals_stack;
+    [], id
+    (*begin match r with
+      | IndRef i ->
+	  let _, oib = Global.lookup_inductive i in
+	  let construct_types = oib.mind_nf_lc in
+	  let rec axiomatize_all_constr l = 
+	    begin match l with
+	      | [] -> ()
+	      | r::l' -> 
+		  axiomatize_body env r (rename_global r)
+		    (tr_global_type r);
+		  axiomatize_all_constr l'
+	    end in
+	  axiomatize_all_constr (list_of_array construct_types);
+	  [], id
+      | _ -> assert false (* TODO constant type definition ? *)
+    end*)
+
+and tr_global_type env id ty =
   if is_Prop ty then
     DeclPred (id, [])
   else if is_Set ty then
@@ -134,7 +196,7 @@ let rec tr_global_type env id ty =
   else 
     let s = Typing.type_of env Evd.empty ty in
     if is_Prop s then
-      Assert (id, tr_formula env ty)
+      Assert (id, tr_formula [] env ty)
     else
       let l,t = tr_type env ty in 
       if is_Set s then DeclVar (id, l, t)
@@ -143,56 +205,57 @@ let rec tr_global_type env id ty =
       else raise NotFO
 
 and tr_global env r = match r with
-  | Libnames.VarRef id ->
-      lookup locals id
+  | VarRef id ->
+      lookup_local id
   | r ->
       try
-	lookup globals r
+	lookup_global r
       with Not_found ->
 	try
 	  let ty = Global.type_of_global r in
 	  let id = rename_global r in
 	  let d = tr_global_type env id ty in
-	  Hashtbl.add globals r (Gfo d);
+	  add_global r (Gfo d);
 	  globals_stack := d :: !globals_stack;
 	  begin try axiomatize_body env r id d with NotFO -> () end;
 	  d
 	with NotFO ->
-	  Hashtbl.add globals r Gnot_fo;
+	  add_global r Gnot_fo;
 	  raise NotFO
 
 and axiomatize_body env r id d = match r with
-  | Libnames.VarRef ident -> 
+  | VarRef ident -> 
       assert false
-  | Libnames.ConstRef c ->
+  | ConstRef c ->
       begin match (Global.lookup_constant c).const_body with
 	| Some b -> 
 	    let b = force b in
 	    let id, ax = match d with
 	      | DeclPred (id, []) ->
-		  let value = tr_formula env b in
+		  let value = tr_formula [] env b in
 		  id, And (Imp (Fatom (Pred (id, [])), value),
 			   Imp (value, Fatom (Pred (id, []))))
 	      | DeclVar (id, [], _) ->
-		  let value = tr_term env b in
-		  id, Fatom (Eq (Tvar id, value)) 
+		  let value = tr_term [] env b in
+		  id, Fatom (Eq (Fol.App (id, []), value)) 
 	      | DeclVar (id, l, _) | DeclPred (id, l) ->
 		  let vars,t = decompose_lam b in
 		  let n = List.length l in
 		  let k = List.length vars in
 		  assert (k <= n);
-		  if k < n then raise NotFO; (* TODO: eta-expanser *)
 		  let vars,env = coq_rename_vars env vars in
 		  let t = substl (List.map mkVar vars) t in
+		  let t,vars,env = eta_expanse t vars env (n-k) in
 		  let vars = List.rev vars in
-		  let fol_var x = Tvar (rename_global (VarRef x)) in
+		  let fol_var x = Fol.App (rename_global (VarRef x), []) in
 		  let fol_vars = List.map fol_var vars in
 		  let vars = List.combine vars l in
+		  let bv = List.map fst vars in
 		  let p = match d with
 		    | DeclVar _ ->
-			Fatom (Eq (App (id, fol_vars), tr_term env t))
+			Fatom (Eq (App (id, fol_vars), tr_term bv env t))
 		    | DeclPred _ ->
-			let value = tr_formula env t in
+			let value = tr_formula bv env t in
 			And (Imp (Fatom (Pred (id, fol_vars)), value),
 			     Imp (value, Fatom (Pred (id, fol_vars))))
 		    | _ ->
@@ -210,39 +273,40 @@ and axiomatize_body env r id d = match r with
   | _ -> ()
 
 
-
 (* assumption: t:T:Set *)
-and tr_term env t =
+and tr_term bv env t =
   match kind_of_term t with
-    | Var id -> 
-	Tvar (rename_global (VarRef id))
     | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zplus -> 
-	Plus (tr_term env a, tr_term env b)
+	Plus (tr_term bv env a, tr_term bv env b)
     | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> 
-	Moins (tr_term env a, tr_term env b)
+	Moins (tr_term bv env a, tr_term bv env b)
     | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> 
-	Mult (tr_term env a, tr_term env b)
+	Mult (tr_term bv env a, tr_term bv env b)
     | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> 
-	Div (tr_term env a, tr_term env b)
+	Div (tr_term bv env a, tr_term 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 a
     | Term.App (f, [|a|]) when f = Lazy.force coq_Zneg ->
 	Moins (Cst 0, (fol_term_of_positive a))
+    | Term.Var id when List.mem id bv ->
+	App (string_of_id id, [])
     | _ ->
 	let f, cl = decompose_app t in
 	begin try
-	  let r = Libnames.reference_of_constr f in
+	  let r = reference_of_constr f in
 	  match tr_global env r with
-	    | DeclVar (s, _, _) -> Fol.App (s, List.map (tr_term env) cl)
-	    | _ -> raise NotFO
+	    | DeclVar (s, _, _) -> 
+		Fol.App (s, List.map (tr_term bv env) cl)
+	    | _ -> 
+		raise NotFO
 	with Not_found ->
 	  raise NotFO
 	end
 
 (* assumption: f is of type Prop *)
-and tr_formula env f =
+and tr_formula bv env f =
   let c, args = decompose_app f in
   match kind_of_term c, args with
     | Var id, [] -> 
@@ -250,39 +314,49 @@ and tr_formula env f =
     | _, [t;a;b] when c = build_coq_eq () -> 
 	(*let ty = pf_type_of gl t in
 	if is_Set ty then*)
-	  Fatom (Eq (tr_term env a, tr_term env b))
+	  Fatom (Eq (tr_term bv env a, tr_term bv env b))
 	(*else raise NotFO*)
     | _, [a;b] when c = Lazy.force coq_Zle ->
-	Fatom (Le (tr_term env a, tr_term env b))
+	Fatom (Le (tr_term bv env a, tr_term bv env b))
     | _, [a;b] when c = Lazy.force coq_Zlt ->
-	Fatom (Lt (tr_term env a, tr_term env b))
+	Fatom (Lt (tr_term bv env a, tr_term bv env b))
     | _, [a;b] when c = Lazy.force coq_Zge ->
-	Fatom (Ge (tr_term env a, tr_term env b))
+	Fatom (Ge (tr_term bv env a, tr_term bv env b))
     | _, [a;b] when c = Lazy.force coq_Zgt ->
-	Fatom (Gt (tr_term env a, tr_term env b))
+	Fatom (Gt (tr_term bv env a, tr_term bv env b))
     | _, [] when c = build_coq_False () ->
 	False
     | _, [] when c = build_coq_True () ->
 	True
     | _, [a] when c = build_coq_not () ->
-	Not (tr_formula env a)
+	Not (tr_formula bv env a)
     | _, [a;b] when c = build_coq_and () ->
-	And (tr_formula env a, tr_formula env b)
+	And (tr_formula bv env a, tr_formula bv env b)
     | _, [a;b] when c = build_coq_or () ->
-	Or (tr_formula env a, tr_formula env b)
-    | Prod (_, a, b), _ ->
+	Or (tr_formula bv env a, tr_formula bv env b)
+    | Prod (n, a, b), _ ->
 	if is_imp_term f then
-	  Imp (tr_formula env a, tr_formula env b)
+	  Imp (tr_formula bv env a, tr_formula bv env b)
 	else
-	  assert false (* TODO Forall *)	  
+	  let vars,env = coq_rename_vars env [n,a] in
+	  let id = match vars with [x] -> x | _ -> assert false in
+	  let b = subst1 (mkVar id) b in
+	  let t = match tr_type env a with
+	    | [], t -> t
+	    | _ -> raise NotFO
+	  in
+	  let bv = id :: bv in
+	  Forall (string_of_id id, t, tr_formula bv env b)
     | _, [a] when c = build_coq_ex () ->
-	assert false (* TODO Exists (tr_formula env a) *)
+	assert false (* TODO Exists (tr_formula bv env a) *)
     | _ ->
 	begin try
-	  let r = Libnames.reference_of_constr c in
+	  let r = reference_of_constr c in
 	  match tr_global env r with
-	    | DeclPred (s, _) -> Fatom (Pred (s, List.map (tr_term env) args))
-	    | _ -> raise NotFO
+	    | DeclPred (s, _) -> 
+		Fatom (Pred (s, List.map (tr_term bv env) args))
+	    | _ -> 
+		raise NotFO
 	with Not_found ->
 	  raise NotFO
 	end
@@ -305,8 +379,8 @@ let tr_goal gl =
       (fun h acc -> try tr_one_hyp h :: acc with NotFO -> acc)
       (pf_hyps_types gl) []
   in
-  let c = tr_formula (pf_env gl) (pf_concl gl) in
-  let hyps = List.rev_append !globals_stack hyps in
+  let c = tr_formula [] (pf_env gl) (pf_concl gl) in
+  let hyps = List.rev_append !globals_stack (List.rev hyps) in
   hyps, c
 
 
@@ -332,6 +406,32 @@ let dp prover gl =
     error "Not a first order goal"
   
 
-let simplify = dp Simplify
+let simplify = tclTHEN intros (dp Simplify)
 let cvc_lite = dp CVCLite
 let harvey = dp Harvey
+
+let dp_hint l =
+  let env = Global.env () in
+  let one_hint (qid,r) = 
+    if not (mem_global r) then begin
+      let ty = Global.type_of_global r in
+      let s = Typing.type_of env Evd.empty ty in
+      if is_Prop s then
+	try
+	  let id = rename_global r in
+	  let d = Assert (id, tr_formula [] env ty) in
+	  add_global r (Gfo d);
+	  globals_stack := d :: !globals_stack
+	with NotFO ->
+	  add_global r Gnot_fo;
+	  msg_warning
+	    (pr_reference qid ++ 
+	     str " ignored (not a first order proposition)")
+	else begin
+	  add_global r Gnot_fo;
+	  msg_warning
+	    (pr_reference qid ++ str " ignored (not a proposition)")
+	end
+    end
+  in
+  List.iter one_hint (List.map (fun qid -> qid, Nametab.global qid) l)
diff --git a/contrib/dp/dp.mli b/contrib/dp/dp.mli
index 40a523089..c5517cac8 100644
--- a/contrib/dp/dp.mli
+++ b/contrib/dp/dp.mli
@@ -1,5 +1,11 @@
 
+open Libnames
 open Proof_type
 
 val simplify : tactic
+val cvc_lite : tactic
+val harvey : tactic
+
+val dp_hint : reference list -> unit
+
 
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index 35c80e72a..c330b9617 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -10,8 +10,6 @@ let rec print_list sep print fmt = function
 let space fmt () = fprintf fmt "@ "
 
 let rec print_term fmt = function
-  | Tvar id -> 
-      fprintf fmt "%s" id
   | Cst n -> 
       fprintf fmt "%d" n
   | Plus (a, b) ->
@@ -70,8 +68,12 @@ let rec print_predicate fmt p =
 
 let print_query fmt (decls,concl) =
   let print_decl = function
-    | DeclVar _ | DeclPred _ | DeclType _ -> 
-	()
+    | DeclVar (id, _, _) ->
+	fprintf fmt "@[;; %s: <var>@]@\n" id
+    | DeclPred (id, _) -> 
+	fprintf fmt "@[;; %s: <predicate>@]@\n" id
+    | DeclType id ->
+	fprintf fmt "@[;; %s: TYPE@]@\n" id
     | Assert (id, f)  -> 
 	fprintf fmt "@[(BG_PUSH ;; %s@\n %a)@]@\n" id print_predicate f
   in
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
index 2cbe62284..02c73e301 100644
--- a/contrib/dp/fol.mli
+++ b/contrib/dp/fol.mli
@@ -8,7 +8,6 @@ type typ = string
 
 type term =   
   | Cst of int
-  | Tvar of string
   | Plus of term * term
   | Moins of term * term
   | Mult of term * term
diff --git a/contrib/dp/g_dp.ml4 b/contrib/dp/g_dp.ml4
index b85775597..e6667a95b 100644
--- a/contrib/dp/g_dp.ml4
+++ b/contrib/dp/g_dp.ml4
@@ -16,7 +16,6 @@ TACTIC EXTEND Simplify
   [ "simplify" ] -> [ simplify ]
 END
 
-(*
 TACTIC EXTEND CVCLite
   [ "cvcl" ] -> [ cvc_lite ]
 END
@@ -24,9 +23,12 @@ END
 TACTIC EXTEND Harvey
   [ "harvey" ] -> [ harvey ]
 END
-*)
 
 (* should be part of basic tactics syntax *)
 TACTIC EXTEND admit
   [ "admit"    ] -> [ Tactics.admit_as_an_axiom ]
 END
+
+VERNAC COMMAND EXTEND Dp_hint 
+  [ "Dp" ne_global_list(l) ] -> [ dp_hint l ]
+END