Abstraction de constr

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

2 files changed, 23 insertions, 28 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 33fb0f284a..0393f54237 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -247,16 +247,6 @@ let global_operator kind id =
   let sp = Nametab.sp_of_id kind id in
   global_sp_operator (Global.env()) sp id
 
-(*
-let construct_sp_reference env sp id =
-  let (oper,hyps) = global_sp_operator env sp id in
-  let hyps' = Global.var_context () in
-  if not (hyps_inclusion env Evd.empty hyps hyps') then
-    error_reference_variables CCI env id;
-  let ids = ids_of_sign hyps in
-  DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
-*)
-
 let occur_decl env (id,c,t) hyps =
   try
     let (c',t') = Sign.lookup_id id hyps in
@@ -296,7 +286,12 @@ let construct_sp_reference env sp id =
   let hyps0 = Global.var_context () in
   let env0 = Environ.reset_context env in
   let args = List.map mkVar (ids_of_var_context hyps) in
-  let body = DOPN(oper,Array.of_list args) in
+  let body = match oper with
+    | Const sp -> mkConst (sp,Array.of_list args)
+    | MutConstruct sp -> mkMutConstruct (sp,Array.of_list args)
+    | MutInd sp -> mkMutInd (sp,Array.of_list args)
+    | _ -> assert false
+  in
   find_common_hyps_then_abstract body env0 hyps0 hyps
 
 let construct_reference env kind id =
@@ -304,7 +299,7 @@ let construct_reference env kind id =
     let sp = Nametab.sp_of_id kind id in
     construct_sp_reference env sp id
   with Not_found -> 
-    VAR (let _ = Environ.lookup_var id env in id)
+    mkVar (let _ = Environ.lookup_var id env in id)
 
 let global_sp_reference sp id = 
   construct_sp_reference (Global.env()) sp id
@@ -322,7 +317,7 @@ let global_reference_imps kind id =
     | _ -> assert false
 (*
 let global env id =
-  try let _ = lookup_glob id (Environ.context env) in VAR id
+  try let _ = lookup_glob id (Environ.context env) in mkVar id
   with Not_found -> global_reference CCI id
 *)
 let is_global id =
@@ -362,7 +357,7 @@ let declare_eliminations sp i =
   if not (list_subset ids (ids_of_var_context (Global.var_context ()))) then
     error ("Declarations of elimination scheme outside the section "^
     "of the inductive definition is not implemented");
-  let ctxt = Array.of_list (List.map (fun id -> VAR id) ids) in
+  let ctxt = Array.of_list (List.map mkVar ids) in
   let mispec = Global.lookup_mind_specif ((sp,i),ctxt) in 
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
diff --git a/library/indrec.ml b/library/indrec.ml
index 59e11cbff8..b39f834f4e 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -57,14 +57,14 @@ let mis_make_case_com depopt env sigma mispec kind =
        	(lambda_create env'
            (build_dependent_inductive ind,
             mkMutCase (ci,
-		       Rel (nbprod+nbargsprod),
-		       Rel 1,
+		       mkRel (nbprod+nbargsprod),
+		       mkRel 1,
 		       rel_vect nbargsprod k)))
        	lnamesar
     else
       let cs = lift_constructor (k+1) constrs.(k) in
       mkLambda_string "f"
-	(build_branch_type env' dep (Rel (k+1)) cs)
+	(build_branch_type env' dep (mkRel (k+1)) cs)
 	(add_branch (k+1))
   in
   let indf = make_ind_family (mispec,rel_list 0 nparams) in
@@ -100,7 +100,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
 	    let (_,realargs) = list_chop nparams largs in 
 	    let base = applist (lift i pk,realargs) in       
             if depK then 
-	      mkAppL (base, [|appvect (Rel (i+1),rel_vect 0 i)|])
+	      mkAppL (base, [|appvect (mkRel (i+1),rel_vect 0 i)|])
             else 
 	      base
       	| _ -> assert false 
@@ -124,13 +124,13 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
           (match optionpos with 
 	     | None -> 
 		 make_prod env (n,t,process_constr (i+1) c_0 rest 
-				  (mkAppL (lift 1 co, [|Rel 1|])))
+				  (mkAppL (lift 1 co, [|mkRel 1|])))
              | Some(dep',p) -> 
 		 let nP = lift (i+1+decP) p in
 		 let t_0 = process_pos dep' nP (lift 1 t) in 
 		 make_prod_dep (dep or dep') env
                    (n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest
-				       (mkAppL (lift 2 co, [|Rel 2|])))))
+				       (mkAppL (lift 2 co, [|mkRel 2|])))))
       | IsMutInd ((_,tyi),_) -> 
       	  let nP = match depPvect.(tyi) with 
 	    | Some(_,p) -> lift (i+decP) p
@@ -150,7 +150,7 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
 	| IsProd (n,t,c) -> lambda_name env (n,t,prec (i+1) c)
      	| IsMutInd _ -> 
             let (_,realargs) = list_chop nparams largs
-            and arg = appvect (Rel (i+1),rel_vect 0 i) in 
+            and arg = appvect (mkRel (i+1),rel_vect 0 i) in 
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
     in
@@ -170,14 +170,14 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
            | None -> 
 	       lambda_name env
 		 (n,incast_type t,process_constr (i+1)
-		    (whd_beta (applist (lift 1 f, [(Rel 1)])))
+		    (whd_beta (applist (lift 1 f, [(mkRel 1)])))
 		    (cprest,rest))
            | Some(_,f_0) -> 
 	       let nF = lift (i+1+decF) f_0 in
 	       let arg = process_pos nF (lift 1 (body_of_type t)) in 
                lambda_name env
 		 (n,incast_type t,process_constr (i+1)
-		    (whd_beta (applist (lift 1 f, [(Rel 1); arg])))
+		    (whd_beta (applist (lift 1 f, [(mkRel 1); arg])))
 		    (cprest,rest)))
     | (n,Some c,t)::cprest, rest -> failwith "TODO"
     | [],[] -> f
@@ -199,7 +199,7 @@ let mis_make_indrec env sigma listdepkind mispec =
       assign k = function 
 	| [] -> ()
         | (mispeci,dep,_)::rest -> 
-            (Array.set depPvec (mis_index mispeci) (Some(dep,Rel k));
+            (Array.set depPvec (mis_index mispeci) (Some(dep,mkRel k));
              assign (k-1) rest)
     in 
     assign nrec listdepkind  
@@ -230,7 +230,7 @@ let mis_make_indrec env sigma listdepkind mispec =
 		(make_rec_branch_arg env sigma (nparams,depPvec,nar+1))
                 vecfi constrs recargsvec.(tyi) in
 	    let j = (match depPvec.(tyi) with 
-		       | Some (_,Rel j) -> j 
+		       | Some (_,c) when isRel c -> destRel c 
 		       | _ -> assert false) in
 	    let indf = make_ind_family
 			 (mispeci,rel_list (nrec+nbconstruct) nparams) in
@@ -240,7 +240,7 @@ let mis_make_indrec env sigma listdepkind mispec =
 		   (build_dependent_inductive
 		      (lift_inductive_family nrec indf),
 		    mkMutCase (make_default_case_info mispeci,
-			       Rel (dect+j+1), Rel 1, branches)))
+			       mkRel (dect+j+1), mkRel 1, branches)))
 		(lift_context nrec lnames)
 	    in
 	    let typtyi = 
@@ -248,9 +248,9 @@ let mis_make_indrec env sigma listdepkind mispec =
 		(prod_create env
 		   (build_dependent_inductive indf,
 		    (if dep then 
-		       appvect (Rel (nbconstruct+nar+j+1), rel_vect 0 (nar+1)) 
+		       appvect (mkRel (nbconstruct+nar+j+1), rel_vect 0 (nar+1)) 
 		     else 
-		       appvect (Rel (nbconstruct+nar+j+1), rel_vect 1 nar))))
+		       appvect (mkRel (nbconstruct+nar+j+1), rel_vect 1 nar))))
           	lnames
 	    in 
 	    mrec (i+nctyi) (nar::ln) (typtyi::ltyp) (deftyi::ldef) rest