renommage du module Pcoq.Vernac en Pcoq.Vernac_ pour contourner un bug d'ocamldep

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

9 files changed, 152 insertions, 134 deletions

diff --git a/contrib/correctness/past.mli b/contrib/correctness/past.mli
index 5db3c87b6..7696c6698 100644
--- a/contrib/correctness/past.mli
+++ b/contrib/correctness/past.mli
@@ -87,11 +87,10 @@ type cc_binder = variable * cc_bind_type
 
 type cc_term =
   | CC_var of variable
-  | CC_letin of 
-      bool * cc_type * cc_binder list * (cc_term * Term.case_info) * cc_term
+  | CC_letin of bool * cc_type * cc_binder list * cc_term * cc_term
   | CC_lam of cc_binder list * cc_term
   | CC_app of cc_term * cc_term list
   | CC_tuple of bool * cc_type list * cc_term list
-  | CC_case of cc_type * (cc_term * Term.case_info) * cc_term list
+  | CC_case of cc_type * cc_term * cc_term list
   | CC_expr of Term.constr
   | CC_hole of cc_type
diff --git a/contrib/correctness/pcic.ml b/contrib/correctness/pcic.ml
index 49871b23a..170a56b28 100644
--- a/contrib/correctness/pcic.ml
+++ b/contrib/correctness/pcic.ml
@@ -13,6 +13,8 @@
 open Names
 open Term
 open Declarations
+open Sign
+open Rawterm
 
 open Pmisc
 open Past
@@ -87,86 +89,112 @@ let sig_n n =
 	    mind_entry_consnames = [ cname ];
 	    mind_entry_lc = [ lc ] } ] }
 	
-let tuple_name dep n =
+let pair = ConstructRef ((coq_constant ["Init"; "Datatypes"] "pair",0),1)
+let exist = ConstructRef ((coq_constant ["Init"; "Specif"] "exist",0),1)
+
+let tuple_ref dep n =
   if n = 2 & not dep then
-    "pair"
+    pair
   else
     let n = n - (if dep then 1 else 0) in
     if dep then
       if n = 1 then 
-	"exist" 
+	exist
       else begin
 	let name = Printf.sprintf "exist_%d" n in
-	if not (tuple_exists (id_of_string name)) then ignore (sig_n n);
-	name
+	let id = id_of_string name in
+	if not (tuple_exists id) then ignore (sig_n n);
+	Nametab.sp_of_id CCI id
       end
     else begin
       let name = Printf.sprintf "Build_tuple_%d" n in
-      if not (tuple_exists (id_of_string name)) then tuple_n n;
-      name
+      let id = id_of_string name in
+      if not (tuple_exists id) then tuple_n n;
+      Nametab.sp_of_id CCI id
     end
 
 (* Binders. *)
 
-let trad_binding bl =
-  List.map (function
-		(id,CC_untyped_binder) -> (id,isevar)
-	      | (id,CC_typed_binder ty) -> (id,ty)) bl
-
-let lambda_of_bl bl c =
-  let b = trad_binding bl in n_lambda c (List.rev b)
+let trad_binder avoid nenv = function
+  | CC_untyped_binder -> RHole None
+  | CC_typed_binder ty -> Detyping.detype avoid nenv ty
+
+let rec push_vars avoid nenv = function
+  | [] -> ([],avoid,nenv)
+  | (id,b) :: bl -> 
+      let b' = trad_binder avoid nenv b in
+      let bl',avoid',nenv' = 
+	push_vars (id :: avoid) (add_name (Name id) nenv) bl 
+      in
+      ((id,b') :: bl', avoid', nenv')
+
+let rec raw_lambda bl v = match bl with
+  | [] -> 
+      v
+  | (id,ty) :: bl' -> 
+      RLambda (dummy_loc, Name id, ty, raw_lambda bl' v)
 
 (* The translation itself is quite easy.
-   letin are translated into Cases construtions *)
+   letin are translated into Cases constructions *)
 
-let constr_of_prog p =
-  let rec trad = function
-    | CC_var id -> mkVar id
+let rawconstr_of_prog p =
+  let rec trad avoid nenv = function
+    | CC_var id -> 
+	RVar (dummy_loc, id)
 
-    (* optimisation : let x = <constr> in e2  =>  e2[x<-constr] *)
-    | CC_letin (_,_,[id,_],(CC_expr c,_),e2) ->
+    (*i optimisation : let x = <constr> in e2  =>  e2[x<-constr] 
+    | CC_letin (_,_,[id,_],CC_expr c,e2) ->
 	real_subst_in_constr [id,c] (trad e2)
+    i*)
 
-    | CC_letin (_,_,([_] as b),(e1,_),e2) ->
-      	let c = trad e1 and c2 = trad e2 in
-	Term.applist (lambda_of_bl b c2, [c])
+    | CC_letin (_,_,([_] as b),e1,e2) ->
+	let (b',avoid',nenv') = push_vars avoid nenv b in
+      	let c1 = trad avoid nenv e1 
+	and c2 = trad avoid' nenv' e2 in
+	RApp (dummy_loc, raw_lambda b' c2, [c1])
 
-    | CC_letin (dep,ty,bl,(e,info),e1) ->
-	let c1 = trad e1
-	and c = trad e in
-	let l = [| lambda_of_bl bl c1 |] in
-	Term.mkMutCase (info, ty, c, l)
+    | CC_letin (dep,ty,bl,e1,e2) ->
+	let (bl',avoid',nenv') = push_vars avoid nenv bl in
+	let c1 = trad avoid nenv e1
+	and c2 = trad avoid' nenv' e2 in
+	ROldCase (dummy_loc, false, None, c1, [| raw_lambda bl' c2 |])
 
     | CC_lam (bl,e) ->
-	let c = trad e in lambda_of_bl bl c
+	let bl',avoid',nenv' = push_vars avoid nenv bl in
+	let c = trad avoid' nenv' e in 
+	raw_lambda bl' c
 
     | CC_app (f,args) ->
-	let c = trad f
-	and cargs = List.map trad args in
-	Term.applist (c,cargs)
+	let c = trad avoid nenv f
+	and cargs = List.map (trad avoid nenv) args in
+	RApp (dummy_loc, c, cargs)
 
-    | CC_tuple (_,_,[e]) -> trad e
+    | CC_tuple (_,_,[e]) -> 
+	trad avoid nenv e
 	
     | CC_tuple (false,_,[e1;e2]) ->
-	let c1 = trad e1 
-	and c2 = trad e2 in
-	Term.applist (constant "pair", [isevar;isevar;c1;c2])
+	let c1 = trad avoid nenv e1 
+	and c2 = trad avoid nenv e2 in
+	RApp (dummy_loc, RRef (dummy_loc,pair), [RHole None;RHole None;c1;c2])
 
     | CC_tuple (dep,tyl,l) ->
       	let n = List.length l in
-      	let cl = List.map trad l in
-      	let name = tuple_name dep n in
+      	let cl = List.map (trad avoid nenv) l in
+      	let tuple = tuple_ref dep n in
+	let tyl = List.map (Detyping.detype avoid nenv) tyl in
       	let args = tyl @ cl in
-	Term.applist (constant name,args)
+	RApp (dummy_loc, RRef (dummy_loc, tuple), args)
 
-    | CC_case (ty,(b,info),el) ->
-	let c = trad b in
-	let cl = List.map trad el in
-	mkMutCase (info, ty, c, Array.of_list cl)
+    | CC_case (_,b,el) ->
+	let c = trad avoid nenv b in
+	let cl = List.map (trad avoid nenv) el in
+	ROldCase (dummy_loc, false, None, c, Array.of_list cl)
 
-    | CC_expr c -> c
+    | CC_expr c -> 
+	Detyping.detype avoid nenv c
 
-    | CC_hole c -> make_hole c
+    | CC_hole c -> 
+	RCast (dummy_loc, RHole None, Detyping.detype avoid nenv c)
 
   in
-  trad p
+  trad [] empty_names_context p
diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli
index 21c3839d9..f0b629071 100644
--- a/contrib/correctness/pcic.mli
+++ b/contrib/correctness/pcic.mli
@@ -8,13 +8,13 @@
 
 (* Certification of Imperative Programs / Jean-Christophe Filliâtre *)
 
-(* $Id$ *)
+(*i $Id$ i*)
 
 open Past
-open Term
+open Rawterm
 
 
-(* transforms intermediate functional programs into CIC terms *)
+(* transforms intermediate functional programs into (raw) CIC terms *)
 
-val constr_of_prog : cc_term -> constr
+val rawconstr_of_prog : cc_term -> rawconstr
 
diff --git a/contrib/correctness/pmisc.ml b/contrib/correctness/pmisc.ml
index f25541961..77356e17c 100644
--- a/contrib/correctness/pmisc.ml
+++ b/contrib/correctness/pmisc.ml
@@ -17,6 +17,8 @@ open Term
 
 module SpSet = Set.Make(struct type t = section_path let compare = sp_ord end)
 
+let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
+
 (* debug *)
 
 let debug = ref false
@@ -159,22 +161,20 @@ let is_connective id =
 
 (* [conj i s] constructs the conjunction of two constr *)
 
-let conj i s =
-  Term.applist (constant "and", [i; s])
-
+let conj i s = Term.applist (constant "and", [i; s])
 
-(* [n_mkNamedProd v [xn,tn;...;x1,t1]] constructs the type (x1:t1)...(xn:tn)v
- *)
+(* [n_mkNamedProd v [xn,tn;...;x1,t1]] constructs the type 
+   [(x1:t1)...(xn:tn)v] *)
 
 let rec n_mkNamedProd v = function
-    [] -> v
-  | (id,ty)::rem -> n_mkNamedProd (Term.mkNamedProd id ty v) rem
+  | [] -> v
+  | (id,ty) :: rem -> n_mkNamedProd (Term.mkNamedProd id ty v) rem
 
 (* [n_lambda v [xn,tn;...;x1,t1]] constructs the type [x1:t1]...[xn:tn]v *)
 
 let rec n_lambda v = function
-    [] -> v
-  | (id,ty)::rem -> n_lambda (Term.mkNamedLambda id ty v) rem
+  | [] -> v
+  | (id,ty) :: rem -> n_lambda (Term.mkNamedLambda id ty v) rem
 
 (* [abstract env idl c] constructs [x1]...[xn]c where idl = [x1;...;xn] *)
 
diff --git a/contrib/correctness/pmisc.mli b/contrib/correctness/pmisc.mli
index f486d0d4e..96519ee9f 100644
--- a/contrib/correctness/pmisc.mli
+++ b/contrib/correctness/pmisc.mli
@@ -15,6 +15,8 @@ open Term
 
 module SpSet : Set.S with type elt = section_path
 
+val coq_constant : string list -> string -> section_path
+
 (* Some misc. functions *)
 
 val reraise_with_loc : Coqast.loc -> ('a -> 'b) -> 'a -> 'b
diff --git a/contrib/correctness/pmonad.ml b/contrib/correctness/pmonad.ml
index 30892ee4c..6dbf1e460 100644
--- a/contrib/correctness/pmonad.ml
+++ b/contrib/correctness/pmonad.ml
@@ -35,17 +35,17 @@ open Peffect
  *)
 
 let product_name = function
-    2 -> "prod"
+  | 2 -> "prod"
   | n -> Printf.sprintf "tuple_%d" n
 
 let dep_product_name = function
-    1 -> "sig"
+  | 1 -> "sig"
   | n -> Printf.sprintf "sig_%d" n
 
 let product ren env before lo = function
-    None -> (* non dependent case *)
+  | None -> (* non dependent case *)
       begin match lo with
-	  [_,v] -> v
+	| [_,v] -> v
 	| _ ->
 	    let s = product_name (List.length lo) in
       	    Term.applist (constant s, List.map snd lo)
@@ -88,8 +88,7 @@ let rec abstract_post ren env (e,q) =
 
 and prod ren env g = 
   List.map
-    (fun id -> 
-       (current_var ren id,trad_type_in_env ren env id)) 
+    (fun id -> (current_var ren id, trad_type_in_env ren env id)) 
     g
 
 and input ren env e  =
@@ -124,7 +123,7 @@ and trad_ml_type_v ren env = function
       let bl',ren',env' =
 	List.fold_left
 	  (fun (bl,ren,env) b -> match b with
-	       (id,BindType ((Ref _ | Array _) as v)) ->
+	     | (id,BindType ((Ref _ | Array _) as v)) ->
 		 let env' = add (id,v) env in
 		 let ren' = initial_renaming env' in
 		 (bl,ren',env')
@@ -145,7 +144,7 @@ and trad_ml_type_v ren env = function
       (apply_pre ren env (anonymous_pre false c)).p_value
 
 and trad_imp_type ren env = function
-    Ref v        -> trad_ml_type_v ren env v
+  | Ref v        -> trad_ml_type_v ren env v
   | Array (c,v)  -> Term.applist (constant "array", 
 				  [c; trad_ml_type_v ren env v])
   | _            -> invalid_arg "Monad.trad_imp_type"
@@ -166,10 +165,9 @@ let binding_of_alist ren env al =
 (* [make_abs bl t p] abstracts t w.r.t binding list bl., that is
  * [x1:t1]...[xn:tn]t. Returns t if the binding is empty. *)
 
-let make_abs bl t =
-  match bl with
-      [] -> t
-    | _  -> CC_lam (bl, t)
+let make_abs bl t = match bl with
+  | [] -> t
+  | _  -> CC_lam (bl, t)
 
 
 (* [result_tuple ren before env (res,v) (ef,q)] constructs the tuple 
@@ -180,21 +178,21 @@ let make_abs bl t =
  * if there is no yi and no post-condition, it is simplified in res itself.
  *)
 
-let make_tuple l q ren env before =
-  match l with
-      [e,_] when q = None -> e
-    | _ ->
-	let tl = List.map snd l in
-	let dep,h,th = match q with
-	    None -> false,[],[]
-	  | Some c ->
-	      let args = List.map (fun (e,_) -> constr_of_prog e) l in
-	      let c = apply_post ren env before c in
-		true,
-		[ CC_hole (Term.applist (c.a_value, args)) ], (* hole *)
-		[ c.a_value ]                     (* type of the hole *)
-	in 
-	  CC_tuple (dep, tl @ th, (List.map fst l) @ h)
+let make_tuple l q ren env before = match l with
+  | [e,_] when q = None -> 
+      e
+  | _ ->
+      let tl = List.map snd l in
+      let dep,h,th = match q with
+	| None -> false,[],[]
+	| Some c ->
+	    let args = List.map (fun (e,_) -> constr_of_prog e) l in
+	    let c = apply_post ren env before c in
+	    true,
+	    [ CC_hole (Term.applist (c.a_value, args)) ], (* hole *)
+	    [ c.a_value ]                     (* type of the hole *)
+      in 
+      CC_tuple (dep, tl @ th, (List.map fst l) @ h)
 
 let result_tuple ren before env (res,v) (ef,q) =
   let ids = get_writes ef in
@@ -202,7 +200,7 @@ let result_tuple ren before env (res,v) (ef,q) =
     (List.map (fun id -> 
 		 let id' = current_var ren id in
 		 CC_var id', trad_type_in_env ren env id) ids)
-    @[res,v]
+    @ [res,v]
   in
   let q = abstract_post ren env (ef,q) in
   make_tuple lo q ren env before,
@@ -266,25 +264,25 @@ let abs_pre ren env (t,ty) pl =
 
 let make_block ren env finish bl =
   let rec rec_block ren result = function
-      [] ->
+    | [] ->
 	finish ren result
-   | (Assert c) :: block ->
-       let t,ty = rec_block ren result block in
-       let c = apply_assert ren env c in
-       let p = { p_assert = true; p_name = c.a_name; p_value = c.a_value } in
-       let_in_pre ty p t, ty
-   | (Label s) :: block ->
-       let ren' = push_date ren s in
-       rec_block ren' result block
-   | (Statement (te,info)) :: block ->
-       let (_,tye),efe,pe,qe = info in
-       let w = get_writes efe in
-       let ren' = next ren w in
-       let id = result_id in
-       let tye = trad_ml_type_v ren env tye in
-       let t = rec_block ren' (Some (id,tye)) block in
-       make_let_in ren env te pe (current_vars ren' w,qe) (id,tye) t,
-       snd t
+    | (Assert c) :: block ->
+	let t,ty = rec_block ren result block in
+	let c = apply_assert ren env c in
+	let p = { p_assert = true; p_name = c.a_name; p_value = c.a_value } in
+	let_in_pre ty p t, ty
+    | (Label s) :: block ->
+	let ren' = push_date ren s in
+	rec_block ren' result block
+    | (Statement (te,info)) :: block ->
+	let (_,tye),efe,pe,qe = info in
+	let w = get_writes efe in
+	let ren' = next ren w in
+	let id = result_id in
+	let tye = trad_ml_type_v ren env tye in
+	let t = rec_block ren' (Some (id,tye)) block in
+	make_let_in ren env te pe (current_vars ren' w,qe) (id,tye) t,
+	snd t
   in
   let t,_ = rec_block ren None bl in
   t
@@ -333,11 +331,7 @@ let make_app env ren args ren' (tf,cf) ((bl,cb),s,capp) c =
   let ((_,tvf),ef,pf,qf) = cf in
   let (_,eapp,papp,qapp) = capp in
   let ((_,v),e,p,q) = c in
-
-  let bl = Util.map_succeed 
-	     (function b -> if is_ref_binder b then failwith "caught" else b) 
-	     bl
-  in
+  let bl = List.filter (fun b -> not (is_ref_binder b)) bl in
   let recur = is_recursive env tf in
   let before = current_date ren in
   let ren'' = next ren' (get_writes ef) in
diff --git a/contrib/correctness/pred.ml b/contrib/correctness/pred.ml
index 02c84cf00..d6f9e0e72 100644
--- a/contrib/correctness/pred.ml
+++ b/contrib/correctness/pred.ml
@@ -29,23 +29,23 @@ let is_eta_redex bl al =
       Invalid_argument("List.for_all2") -> false
 
 let rec red = function
-    CC_letin (dep, ty, bl, (e1,info), e2) ->
+    CC_letin (dep, ty, bl, e1, e2) ->
       begin match red e2 with
 	  CC_tuple (false,tl,al) ->
 	    if is_eta_redex bl al then
 	      red e1
 	    else
-	      CC_letin (dep, ty, bl, (red e1,info),
+	      CC_letin (dep, ty, bl, red e1,
 			CC_tuple (false,tl,List.map red al))
-	| e -> CC_letin (dep, ty, bl, (red e1,info), e)
+	| e -> CC_letin (dep, ty, bl, red e1, e)
       end
 
   | CC_lam (bl, e) ->
       CC_lam (bl, red e)
   | CC_app (e, al) ->
       CC_app (red e, List.map red al)
-  | CC_case (ty, (e1,info), el) ->
-      CC_case (ty, (red e1,info), List.map red el)
+  | CC_case (ty, e1, el) ->
+      CC_case (ty, red e1, List.map red el)
   | CC_tuple (dep, tl, al) ->
       CC_tuple (dep, tl, List.map red al)
   | e -> e
diff --git a/contrib/correctness/ptactic.ml b/contrib/correctness/ptactic.ml
index 5eb03d23e..d92d8524b 100644
--- a/contrib/correctness/ptactic.ml
+++ b/contrib/correctness/ptactic.ml
@@ -13,6 +13,7 @@
 open Pp
 open Names
 open Term
+open Pretyping
 open Pfedit
 open Vernacentries
 
@@ -61,18 +62,15 @@ let coqast_of_prog p =
   deb_mess 
     [< 'fNL; 'sTR"Pcic.constr_of_prog: Traduction cc_term -> constr..."; 
        'fNL >];
-  let c = Pcic.constr_of_prog cc in
-  deb_mess (Printer.prterm c);
+  let r = Pcic.rawconstr_of_prog cc in
+  deb_mess (Printer.pr_rawterm r);
 
   (* 6. résolution implicites *)
   deb_mess [< 'fNL; 'sTR"Résolution implicites (? => Meta(n))..."; 'fNL >];
-  let c = c in
-  (*i WAS
-    (ise_resolve false (Evd.mt_evd()) [] (gLOB(initial_sign())) c)._VAL in
-  i*)
-  deb_mess (Printer.prterm c);
+  let oc = understand_gen_tcc Evd.empty (Global.env()) [] [] None r in
+  deb_mess (Printer.prterm (snd oc));
 
-  p,c,ty,v
+  p,oc,ty,v
 
 (* [automatic : tactic]
  * 
@@ -97,8 +95,6 @@ open Tactics
 open Tacticals
 open Equality
 
-let coq_constant d s = make_path ("Coq" :: d) (id_of_string s) CCI
-
 let nat = IndRef (coq_constant ["Init";"Datatypes"] "nat", 0)
 let lt = ConstRef (coq_constant ["Init";"Peano"] "lt")
 let well_founded = ConstRef (coq_constant ["Init";"Wf"] "well_founded")
@@ -201,7 +197,7 @@ let (automatic : tactic) =
 
 let correctness s p opttac =
   Pmisc.reset_names();
-  let p,c,cty,v = coqast_of_prog p in
+  let p,oc,cty,v = coqast_of_prog p in
   let env = Global.env () in
   let sign = Global.named_context () in
   let sigma = Evd.empty in
@@ -211,10 +207,9 @@ let correctness s p opttac =
   Penv.new_edited id (v,p);
   if !debug then show_open_subgoals();
   deb_mess [< 'sTR"Pred.red_cci: Réduction..."; 'fNL >];
-  let c = Pred.red_cci c in
+  let oc = let (mm,c) = oc in (mm, Pred.red_cci c) in
   deb_mess [< 'sTR"APRES REDUCTION :"; 'fNL >];
-  deb_mess (Printer.prterm c);
-  let oc = [],c in (* TODO: quid des existentielles ici *)
+  deb_mess (Printer.prterm (snd oc));
   let tac = (tclTHEN (Refine.refine_tac oc) automatic) in
   let tac = match opttac with 
     | None -> tac
diff --git a/contrib/correctness/putil.ml b/contrib/correctness/putil.ml
index 2f86d355e..e227a4459 100644
--- a/contrib/correctness/putil.ml
+++ b/contrib/correctness/putil.ml
@@ -264,7 +264,7 @@ and pp_binder = function
 
 let rec pp_cc_term = function
     CC_var id -> pr_id id
-  | CC_letin (_,_,bl,(c,_),c1) ->
+  | CC_letin (_,_,bl,c,c1) ->
       hOV 0 [< hOV 2 [< 'sTR"let ";
 		  	prlist_with_sep (fun () -> [< 'sTR"," >])
 			  (fun (id,_) -> pr_id id) bl;
@@ -287,7 +287,7 @@ let rec pp_cc_term = function
 	       prlist_with_sep (fun () -> [< 'sTR","; 'cUT >])
 		 pp_cc_term cl;
 	       'sTR")" >]
-  | CC_case (_,(b,_),[e1;e2]) ->
+  | CC_case (_,b,[e1;e2]) ->
       hOV 0 [< 'sTR"if "; pp_cc_term b; 'sTR" then"; 'fNL;
 	       'sTR"  "; hOV 0 (pp_cc_term e1); 'fNL;
 	       'sTR"else"; 'fNL;