dp: traitement des definitions

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

3 files changed, 106 insertions, 45 deletions

diff --git a/contrib/dp/dp.ml b/contrib/dp/dp.ml
index 1076a48ba..961dd1c4c 100644
--- a/contrib/dp/dp.ml
+++ b/contrib/dp/dp.ml
@@ -13,6 +13,7 @@ open Termops
 open Coqlib
 open Hipattern
 open Libnames
+open Declarations
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
 let coq_modules =
@@ -66,6 +67,21 @@ let rename_global r =
     in
     loop (Nametab.id_of_global r)
 
+let foralls =
+  List.fold_right (fun (x,t) p -> Forall (rename_global (VarRef x), t, p))
+
+(* 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 *)
+let coq_rename_vars env vars =
+  let avoid = ref (ids_of_named_context (Environ.named_context env)) in
+  List.fold_right
+    (fun (na,t) (newvars, newenv) -> 
+       let id = next_name_away na !avoid in
+       avoid := id :: !avoid;
+       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"
@@ -110,23 +126,23 @@ let lookup t r =  match Hashtbl.find t r with
   | Gnot_fo -> raise NotFO
   | Gfo d -> d
 
-let rec tr_global_type gl id ty =
+let rec tr_global_type env id ty =
   if is_Prop ty then
     DeclPred (id, [])
   else if is_Set ty then
     DeclType id
   else 
-    let s = pf_type_of gl ty in
+    let s = Typing.type_of env Evd.empty ty in
     if is_Prop s then
-      Assert (id, tr_formula gl ty)
+      Assert (id, tr_formula env ty)
     else
-      let l,t = tr_type (pf_env gl) ty in 
+      let l,t = tr_type env ty in 
       if is_Set s then DeclVar (id, l, t)
       else if t = "BOOLEAN" then
 	DeclPred(id, l)
       else raise NotFO
 
-and tr_global gl = function
+and tr_global env r = match r with
   | Libnames.VarRef id ->
       lookup locals id
   | r ->
@@ -136,28 +152,78 @@ and tr_global gl = function
 	try
 	  let ty = Global.type_of_global r in
 	  let id = rename_global r in
-	  let d = tr_global_type gl id ty in
+	  let d = tr_global_type env id ty in
 	  Hashtbl.add globals 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;
 	  raise NotFO
 
+and axiomatize_body env r id d = match r with
+  | Libnames.VarRef ident -> 
+      assert false
+  | Libnames.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
+		  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)) 
+	      | 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 vars = List.rev vars in
+		  let fol_var x = Tvar (rename_global (VarRef x)) in
+		  let fol_vars = List.map fol_var vars in
+		  let vars = List.combine vars l in
+		  let p = match d with
+		    | DeclVar _ ->
+			Fatom (Eq (App (id, fol_vars), tr_term env t))
+		    | DeclPred _ ->
+			let value = tr_formula env t in
+			And (Imp (Fatom (Pred (id, fol_vars)), value),
+			     Imp (value, Fatom (Pred (id, fol_vars))))
+		    | _ ->
+			assert false
+		  in
+		  id, foralls vars p
+	      | _ ->
+		  raise NotFO (* TODO *)
+	    in
+	    let ax = Assert (id, ax) in
+	    globals_stack := ax :: !globals_stack
+	| None -> 
+	    () (* Coq axiom *)
+      end
+  | _ -> ()
+
+
 
 (* assumption: t:T:Set *)
-and tr_term gl t =
+and tr_term 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 gl a, tr_term gl b)
+	Plus (tr_term env a, tr_term env b)
     | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zminus -> 
-	Moins (tr_term gl a, tr_term gl b)
+	Moins (tr_term env a, tr_term env b)
     | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zmult -> 
-	Mult (tr_term gl a, tr_term gl b)
+	Mult (tr_term env a, tr_term env b)
     | Term.App (f, [|a;b|]) when f = Lazy.force coq_Zdiv -> 
-	Div (tr_term gl a, tr_term gl b)
+	Div (tr_term env a, tr_term env b)
     | Term.Construct _ when t = Lazy.force coq_Z0 ->
 	Cst 0
     | Term.App (f, [|a|]) when f = Lazy.force coq_Zpos ->
@@ -168,52 +234,54 @@ and tr_term gl t =
 	let f, cl = decompose_app t in
 	begin try
 	  let r = Libnames.reference_of_constr f in
-	  match tr_global gl r with
-	    | DeclVar (s, _, _) -> Fol.App (s, List.map (tr_term gl) cl)
+	  match tr_global env r with
+	    | DeclVar (s, _, _) -> Fol.App (s, List.map (tr_term env) cl)
 	    | _ -> raise NotFO
 	with Not_found ->
 	  raise NotFO
 	end
 
 (* assumption: f is of type Prop *)
-and tr_formula gl f =
+and tr_formula env f =
   let c, args = decompose_app f in
   match kind_of_term c, args with
     | Var id, [] -> 
-	Fvar (rename_global (VarRef id))
+	Fatom (Pred (rename_global (VarRef id), []))
     | _, [t;a;b] when c = build_coq_eq () -> 
-	(* TODO: verifier type t *)
-	Fatom (Eq (tr_term gl a, tr_term gl b))
+	(*let ty = pf_type_of gl t in
+	if is_Set ty then*)
+	  Fatom (Eq (tr_term env a, tr_term env b))
+	(*else raise NotFO*)
     | _, [a;b] when c = Lazy.force coq_Zle ->
-	Fatom (Le (tr_term gl a, tr_term gl b))
+	Fatom (Le (tr_term env a, tr_term env b))
     | _, [a;b] when c = Lazy.force coq_Zlt ->
-	Fatom (Lt (tr_term gl a, tr_term gl b))
+	Fatom (Lt (tr_term env a, tr_term env b))
     | _, [a;b] when c = Lazy.force coq_Zge ->
-	Fatom (Ge (tr_term gl a, tr_term gl b))
+	Fatom (Ge (tr_term env a, tr_term env b))
     | _, [a;b] when c = Lazy.force coq_Zgt ->
-	Fatom (Gt (tr_term gl a, tr_term gl b))
+	Fatom (Gt (tr_term env a, tr_term env b))
     | _, [] when c = build_coq_False () ->
 	False
     | _, [] when c = build_coq_True () ->
 	True
     | _, [a] when c = build_coq_not () ->
-	Not (tr_formula gl a)
+	Not (tr_formula env a)
     | _, [a;b] when c = build_coq_and () ->
-	And (tr_formula gl a, tr_formula gl b)
+	And (tr_formula env a, tr_formula env b)
     | _, [a;b] when c = build_coq_or () ->
-	Or (tr_formula gl a, tr_formula gl b)
+	Or (tr_formula env a, tr_formula env b)
     | Prod (_, a, b), _ ->
 	if is_imp_term f then
-	  Imp (tr_formula gl a, tr_formula gl b)
+	  Imp (tr_formula env a, tr_formula env b)
 	else
 	  assert false (* TODO Forall *)	  
     | _, [a] when c = build_coq_ex () ->
-	assert false (* TODO Exists (tr_formula gl a) *)
+	assert false (* TODO Exists (tr_formula env a) *)
     | _ ->
 	begin try
 	  let r = Libnames.reference_of_constr c in
-	  match tr_global gl r with
-	    | DeclPred (s, _) -> Fatom (Pred (s, List.map (tr_term gl) args))
+	  match tr_global env r with
+	    | DeclPred (s, _) -> Fatom (Pred (s, List.map (tr_term env) args))
 	    | _ -> raise NotFO
 	with Not_found ->
 	  raise NotFO
@@ -225,7 +293,7 @@ let tr_goal gl =
   let tr_one_hyp (id, ty) = 
     try
       let s = rename_global (VarRef id) in
-      let d = tr_global_type gl s ty in
+      let d = tr_global_type (pf_env gl) s ty in
       Hashtbl.add locals id (Gfo d);
       d
     with NotFO ->
@@ -237,7 +305,7 @@ 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 gl (pf_concl gl) in
+  let c = tr_formula (pf_env gl) (pf_concl gl) in
   let hyps = List.rev_append !globals_stack hyps in
   hyps, c
 
diff --git a/contrib/dp/dp_simplify.ml b/contrib/dp/dp_simplify.ml
index 353bb7092..35c80e72a 100644
--- a/contrib/dp/dp_simplify.ml
+++ b/contrib/dp/dp_simplify.ml
@@ -26,8 +26,6 @@ let rec print_term fmt = function
       fprintf fmt "%s" id 
   | App (id, tl) ->
       fprintf fmt "@[(%s@ %a)@]" id print_terms tl
-  | Db _ ->
-      assert false (*TODO*)
 
 and print_terms fmt tl = 
   print_list space print_term fmt tl
@@ -39,8 +37,6 @@ let rec print_predicate fmt p =
       fprintf fmt "TRUE"
   | False ->
       fprintf fmt "FALSE"
-  | Fvar id -> 
-      fprintf fmt "%s" id
   | Fatom (Eq (a, b)) ->
       fprintf fmt "@[(EQ %a@ %a)@]" print_term a print_term b
   | Fatom (Le (a, b)) ->
@@ -61,17 +57,15 @@ let rec print_predicate fmt p =
       fprintf fmt "@[(OR@ %a@ %a)@]" pp a pp b
   | Not a ->
       fprintf fmt "@[(NOT@ %a)@]" pp a
+  | Forall (id, _, p) -> 
+      fprintf fmt "@[(FORALL (%s)@ %a)@]" id pp p
 (*
-  | Forall (_,id,n,_,p) -> 
-      let id' = next_away id (predicate_vars p) in
-      let p' = subst_in_predicate (subst_onev n id') p in
-      fprintf fmt "@[(FORALL (%a)@ %a)@]" Ident.print id' pp p'
   | Exists (id,n,t,p) -> 
       let id' = next_away id (predicate_vars p) in
       let p' = subst_in_predicate (subst_onev n id') p in
       fprintf fmt "@[(EXISTS (%a)@ %a)@]" Ident.print id' pp p'
 *)
-  | Exists _|Forall _ ->
+  | Exists _ ->
       assert false (*TODO*)
 
 let print_query fmt (decls,concl) =
@@ -90,6 +84,7 @@ let call q =
   let fmt = formatter_of_out_channel c in
   fprintf fmt "@[%a@]@." print_query q;
   close_out c;
+  ignore (Sys.command (sprintf "cat %s" f));
   let cmd = 
     sprintf "timeout 10 Simplify %s > out 2>&1 && grep -q -w Valid out" f
   in
diff --git a/contrib/dp/fol.mli b/contrib/dp/fol.mli
index cce593cf4..2cbe62284 100644
--- a/contrib/dp/fol.mli
+++ b/contrib/dp/fol.mli
@@ -8,13 +8,12 @@ type typ = string
 
 type term =   
   | Cst of int
-  | Db of int
   | Tvar of string
   | Plus of term * term
   | Moins of term * term
   | Mult of term * term
   | Div of term * term
-  | App of string * (term list)
+  | App of string * term list
 
 and atom =   
   | Eq of term * term
@@ -22,17 +21,16 @@ and atom =
   | Lt of term * term
   | Ge of term * term
   | Gt of term * term
-  | Pred of string * (term list)
+  | Pred of string * term list
 
 and form = 
   | Fatom of atom
-  | Fvar of string
   | Imp of form * form
   | And of form * form
   | Or of form * form
   | Not of form
-  | Forall of string * (typ list * typ) * form
-  | Exists of string * (typ list * typ) * form
+  | Forall of string * typ * form
+  | Exists of string * typ * form
   | True
   | False