Abstraction de constr

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

7 files changed, 75 insertions, 108 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0745081760..ac778ded80 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -132,8 +132,7 @@ let mssg_this_case_cannot_occur () =
 
 (* Utils *)
 
-let ctxt_of_ids ids =
-  Array.of_list (List.map (function id -> VAR id) ids)
+let ctxt_of_ids ids = Array.of_list (List.map mkVar ids)
 let constructor_of_rawconstructor (cstr_sp,ids) = (cstr_sp,ctxt_of_ids ids)
 let inductive_of_rawconstructor c =
   inductive_of_constructor (constructor_of_rawconstructor c)
@@ -589,7 +588,7 @@ let infer_predicate env isevars typs cstrs (IndFamily (mis,_) as indf) =
       let predpred = lam_it (mkSort s) sign in
       let caseinfo = make_default_case_info mis in
       let brs = array_map2 abstract_conclusion typs cstrs in
-      let predbody = mkMutCase (caseinfo, predpred, Rel 1, brs) in
+      let predbody = mkMutCase (caseinfo, predpred, mkRel 1, brs) in
       let pred = lam_it (lift (List.length sign) typn) sign in
       failwith "TODO4-2"; (true,pred)
 
@@ -631,11 +630,11 @@ let rec weaken_predicate n pred =
 		    anomaly "weaken_predicate: only product can be weakened"
     | PrProd ((dep,_,IsInd (_,IndType(indf,realargs))),pred) ->
 	(* To make it more uniform, we apply realargs but they not occur! *)
-	let copt = if dep then Some (Rel n) else None in
+	let copt = if dep then Some (mkRel n) else None in
 	PrLetIn ((realargs,copt), weaken_predicate (n-1)
 		   (lift_predicate (List.length realargs) pred))
     | PrProd ((dep,_,NotInd t),pred) ->
-	let copt = if dep then Some (Rel n) else None in
+	let copt = if dep then Some (mkRel n) else None in
 	PrLetIn (([],copt), weaken_predicate (n-1) pred)
 
 let rec extract_predicate = function
@@ -770,7 +769,7 @@ let build_branch pb defaults current eqns const_info =
        (List.map (lift const_info.cs_nargs) const_info.cs_params)
        @(rel_list 0 const_info.cs_nargs)) in
 
-  (* We replace [(Rel 1)] by its expansion [ci] *)
+  (* We replace [(mkRel 1)] by its expansion [ci] *)
   let updated_old_tomatch =
     lift_subst_tomatch const_info.cs_nargs (1,ci) pb.tomatch in
   { pb with
@@ -830,13 +829,13 @@ and match_current pb (n,tm) =
 and compile_further pb firstnext rest =
   (* We pop as much as possible tomatch not dependent one of the other *)
   let nexts,future = pop_next_tomatchs [firstnext] rest in
-  (* the next pattern to match is at the end of [nexts], it has ref (Rel n)
+  (* the next pattern to match is at the end of [nexts], it has ref (mkRel n)
      where n is the length of nexts *)
   let sign = List.map (fun ((na,t),_) -> (na,type_of_tomatch_type t)) nexts in
   let currents =
     list_map_i
       (fun i ((na,t),(_,rhsdep)) ->
-	 Pushed (insert_lifted ((Rel i, lift_tomatch_type i t), rhsdep)))
+	 Pushed (insert_lifted ((mkRel i, lift_tomatch_type i t), rhsdep)))
       1 nexts in
   let pb' = { pb with
 		env = push_rels sign pb.env;
diff --git a/pretyping/class.ml b/pretyping/class.ml
index ee759ad96d..21935be3c7 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -31,8 +31,8 @@ let stre_max (stre1,stre2) =
 let stre_max4 stre1 stre2 stre3 stre4 =
   stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4)))
 
-let id_of_varid = function
-  | VAR id -> id
+let id_of_varid c = match kind_of_term c with
+  | IsVar id -> id
   | _ -> anomaly "class__id_of_varid"
 
 let stre_of_VAR c = variable_strength (destVar c)
@@ -141,7 +141,7 @@ let constructor_at_head1 t =
 let uniform_cond nargs lt = 
   let rec aux = function
     | (0,[]) -> true
-    | (n,t::l) -> (strip_outer_cast t = Rel n) & (aux ((n-1),l))
+    | (n,t::l) -> (strip_outer_cast t = mkRel n) & (aux ((n-1),l))
     | _ -> false
   in 
   aux (nargs,lt)
@@ -216,10 +216,11 @@ let prods_of t =
 let build_id_coercion idf_opt ids =
   let env = Global.env () in
   let vs = construct_reference env CCI ids in 
-  let c = match (strip_outer_cast vs) with
-    | (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' ->
-	(try Instantiate.constant_value env c'
-         with _ -> errorlabstrm "build_id_coercion"
+  let c = match kind_of_term (strip_outer_cast vs) with
+    | IsConst cst -> 
+	(try Instantiate.constant_value env cst
+         with Instantiate.NotEvaluableConst _ ->
+	   errorlabstrm "build_id_coercion"
              [< 'sTR(string_of_id ids);
 		'sTR" must be a transparent constant" >])
     | _ -> 
@@ -234,7 +235,7 @@ let build_id_coercion idf_opt ids =
     it_mkLambda_or_LetIn
       (mkLambda (Name (id_of_string "x"),
 		 applistc vs (rel_list 0 llams),
-		 Rel 1))
+		 mkRel 1))
        lams
   in
   let typ_f =
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c298852f40..2892cddb43 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -144,7 +144,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
                let env1 = push_rel_decl (name,assu1) env in
                let h1 = 
 		 inh_conv_coerce_to_fail env isevars t1
-		   {uj_val = Rel 1; 
+		   {uj_val = mkRel 1; 
 		    uj_type = typed_app (fun _ -> u1) assu1 } in
                let h2 = inh_conv_coerce_to_fail env isevars u2  
 			 { uj_val = mkAppL (lift 1 v, [|h1.uj_val|]);
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 0801d8f2c3..dd3022764a 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -262,12 +262,7 @@ let lookup_index_as_renamed t n =
   in lookup n 1 t
 
 let rec detype avoid env t =
-  match collapse_appl t with
-    (* Not well-formed constructions *)
-    | DLAM _ | DLAMV _ -> error "Cannot detype"
-    (* Well-formed constructions *)
-    | regular_constr -> 
-    (match kind_of_term regular_constr with
+  match kind_of_term (collapse_appl t) with
     | IsRel n ->
       (try match lookup_name_of_rel n env with
 	 | Name id   -> RRef (dummy_loc, RVar id)
@@ -331,7 +326,7 @@ let rec detype avoid env t =
 	end
 	
     | IsFix (nvn,(cl,lfn,vt)) -> detype_fix (RFix nvn) avoid env cl lfn vt
-    | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCoFix n) avoid env cl lfn vt)
+    | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCoFix n) avoid env cl lfn vt
 
 and detype_fix fk avoid env cl lfn vt =
   let lfi = List.map (fun id -> next_name_away id avoid) lfn in
@@ -366,7 +361,7 @@ and detype_eqn avoid env constr_id construct_nargs branch =
 	| _ -> (* eta-expansion : n'arrivera plus lorsque tous les
                   termes seront construits à partir de la syntaxe Cases *)
             (* nommage de la nouvelle variable *)
-	    let new_b = applist (lift 1 b, [Rel 1]) in
+	    let new_b = applist (lift 1 b, [mkRel 1]) in
             let pat,new_avoid,new_env,new_ids =
 	      make_pat Anonymous avoid env new_b ids in
 	    buildrec new_ids (pat::patlist) new_avoid new_env (n-1) new_b
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 0a400a3a6d..d3b9c04f6f 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -14,7 +14,7 @@ open Recordops
 open Evarutil
 
 (* Pb: Mach cannot type evar in the general case (all Const must be applied
- * to VARs). But evars may be applied to Rels or other terms! This is the
+ * to Vars). But evars may be applied to Rels or other terms! This is the
  * difference between type_of_const and type_of_const2.
  *)
 
@@ -128,36 +128,37 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f1; f2]
 
-    | IsEvar (sp1,al1), IsConst (sp2,al2) ->
+    | IsEvar (sp1,al1), IsConst cst2 ->
 	let f1 () =
 	  (List.length l1 <= List.length l2) &
 	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
 	  solve_pb env isevars(pbty,term1,applist(term2,deb2))
           & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
 	and f4 () =
-          if evaluable_constant env term2 then
-            evar_eqappr_x env isevars pbty
-              appr1 (evar_apprec env isevars l2 (constant_value env term2))
-          else false
+	  match constant_opt_value env cst2 with
+	    | Some v2 ->
+		evar_eqappr_x env isevars pbty
+		  appr1 (evar_apprec env isevars l2 v2)
+	    | None -> false
 	in 
 	ise_try isevars [f1; f4]
 
-    | IsConst (sp1,al1), IsEvar (sp2,al2) ->
+    | IsConst cst1, IsEvar (sp2,al2) ->
 	let f1 () =
        	  (List.length l2 <= List.length l1) &
        	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
 	  solve_pb env isevars(pbty,applist(term1,deb1),term2)
           & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 	and f4 () =
-          if evaluable_constant env term1 then
-            evar_eqappr_x env isevars pbty
-              (evar_apprec env isevars l1 (constant_value env term1)) appr2
-          else 
-	    false
+	  match constant_opt_value env cst1 with
+	    | Some v1 ->
+		evar_eqappr_x env isevars pbty
+		  (evar_apprec env isevars l1 v1) appr2
+	    | None -> false
 	in 
 	ise_try isevars [f1; f4]
 
-    | IsConst (sp1,al1), IsConst (sp2,al2) ->
+    | IsConst (sp1,al1 as cst1), IsConst (sp2,al2 as cst2) ->
 	let f2 () =
           (sp1 = sp2)
 	  & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)  
@@ -168,14 +169,16 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	      with Not_found -> check_conv_record appr2 appr1)
            with _ -> false)
 	and f4 () =
-          if evaluable_constant env term2 then
-            evar_eqappr_x env isevars pbty
-              appr1 (evar_apprec env isevars l2 (constant_value env term2))
-          else if evaluable_constant env term1 then
-            evar_eqappr_x env isevars pbty
-              (evar_apprec env isevars l1 (constant_value env term1)) appr2
-          else 
-	    false
+	  match constant_opt_value env cst2 with
+	    | Some v2 ->
+		evar_eqappr_x env isevars pbty
+		  appr1 (evar_apprec env isevars l2 v2)
+	    | None ->
+		match constant_opt_value env cst1 with
+		  | Some v1 ->
+		      evar_eqappr_x env isevars pbty
+			(evar_apprec env isevars l1 v1) appr2
+		  | None -> false
 	in 
 	ise_try isevars [f2; f3; f4]
 
@@ -191,25 +194,29 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	solve_pb env isevars(pbty,applist(term1,deb1),term2)
         & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
 
-    | IsConst (_,_), _ ->
+    | IsConst cst1, _ ->
 	let f3 () =
 	  (try conv_record env isevars (check_conv_record appr1 appr2)
            with _ -> false)
-	and f4 () = 
-	  evaluable_constant env term1 &
- 	  evar_eqappr_x env isevars pbty
-            (evar_apprec env isevars l1 (constant_value env term1)) appr2
+	and f4 () =
+	  match constant_opt_value env cst1 with
+	    | Some v1 ->
+ 		evar_eqappr_x env isevars pbty
+		  (evar_apprec env isevars l1 v1) appr2
+	    | None -> false
 	in 
 	ise_try isevars [f3; f4]
 	     
-    | _ , IsConst (_,_) -> 
+    | _ , IsConst cst2 -> 
 	let f3 () = 
 	  (try (conv_record env isevars (check_conv_record appr2 appr1))
            with _ -> false)
 	and f4 () =
-          evaluable_constant env term2 &
- 	  evar_eqappr_x env isevars pbty
-            appr1 (evar_apprec env isevars l2 (constant_value env term2))
+	  match constant_opt_value env cst2 with
+	    | Some v2 ->
+ 		evar_eqappr_x env isevars pbty
+		  appr1 (evar_apprec env isevars l2 v2)
+	    | None -> false
 	in 
 	ise_try isevars [f3; f4]
 
@@ -287,12 +294,6 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	& (array_for_all2 (evar_conv_x env isevars CONV) bds1 bds2)
 	& (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
 
-    (***
-    | (DOP0(Implicit),[]),(DOP0(Implicit),[]) -> true
-    (* added to compare easily the specification of fixed points
-     * But b (optional env) is not updated! *)
-    ***)
-
     | (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _), _ -> false
     | _, (IsRel _ | IsVar _ | IsMeta _ | IsXtra _ | IsLambda _) -> false
 
@@ -320,8 +321,7 @@ and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) =
        xs1 xs)
     & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
     & (evar_conv_x env isevars CONV t 
-	 (if ks=[] then c 
-	  else  (DOPN(AppL,Array.of_list(c::(List.rev ks))))))
+	 (if ks=[] then c else applist (c,(List.rev ks))))
   then
     (*TR*) (if !compter then (nbstruc:=!nbstruc+1;
                               nbimplstruc:=!nbimplstruc+(List.length ks);true)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index c360df8695..8afaf83692 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -174,7 +174,7 @@ let has_ise sigma t =
   with Uninstantiated_evar _ -> true
 
 (* We try to instanciate the evar assuming the body won't depend
- * on arguments that are not Rels or VARs, or appearing several times.
+ * on arguments that are not Rels or Vars, or appearing several times.
  *)
 (* Note: error_not_clean should not be an error: it simply means that the
  * conversion test that lead to the faulty call to [real_clean] should return
@@ -182,12 +182,12 @@ let has_ise sigma t =
  *)
 
 let real_clean isevars sp args rhs =
-  let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in
+  let subst = List.map (fun (x,y) -> (y,mkVar x)) (filter_unique args) in
   let rec subs k t =
     match kind_of_term t with
       |IsRel i ->
  	 if i<=k then t
- 	 else (try List.assoc (Rel (i-k)) subst with Not_found -> t)
+ 	 else (try List.assoc (mkRel (i-k)) subst with Not_found -> t)
       | IsVar _ -> (try List.assoc t subst with Not_found -> t)
       | _ -> map_constr_with_binders (fun na k -> k+1) subs k t
   in
@@ -195,30 +195,6 @@ let real_clean isevars sp args rhs =
   (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
   body
 
-(*
-let real_clean isevars sp args rhs =
-  let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in
-  let rec subs k t =
-    match t with
-      Rel i ->
- 	if i<=k then t
- 	else (try List.assoc (Rel (i-k)) subst with Not_found -> t)
-    | VAR _ -> (try List.assoc t subst with Not_found -> t)
-    | DOP0 _ -> t
-    | DOP1(o,a) -> DOP1(o, subs k a)
-    | DOP2(o,a,b) -> DOP2(o, subs k a, subs k b)
-    | DOPN(o,v) -> restrict_hyps isevars (DOPN(o, Array.map (subs k) v))
-    | DLAM(n,a) -> DLAM(n, subs (k+1) a)
-    | DLAMV(n,v) -> DLAMV(n, Array.map (subs (k+1)) v)
-    | CLam (n,t,c)   -> CLam (n, typed_app (subs k) t, subs (k+1) c)  
-    | CPrd (n,t,c)   -> CPrd (n, typed_app (subs k) t, subs (k+1) c)
-    | CLet (n,b,t,c) -> CLet (n, subs k b, typed_app (subs k) t, subs (k+1) c)
-  in
-  let body = subs 0 rhs in
-  (* if not (closed0 body) then error_not_clean CCI empty_env sp body; *)
-  body
-*)
-
 let make_instance_with_rel env =
   let n = rel_context_length (rel_context env) in
   let vars = 
@@ -250,7 +226,7 @@ let new_isevar isevars env typ k =
   evar
 
 (* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
- * evar, i.e. tries to find the body ?sp for lhs=mkConst (sp,args)
+ * evar, i.e. tries to find the body ?sp for lhs=mkEvar (sp,args)
  * ?sp [ sp.hyps \ args ]  unifies to rhs
  * ?sp must be a closed term, not referring to itself.
  * Not so trivial because some terms of args may be terms that are not
@@ -266,11 +242,15 @@ let new_isevar isevars env typ k =
  * cannot be done, as in  [x:?1; y:nat; z:(le y y)] x=z
  * ?1 would be instantiated by (le y y) but y is not in the scope of ?1
  *)
+
+let keep_rels_and_vars c = match kind_of_term c with
+  | IsVar _ | IsRel _ -> c
+  | _ -> mkImplicit   (* Mettre mkMeta ?? *)
+
 let evar_define isevars lhs rhs =
   let (ev,argsv) = destEvar lhs in
   if occur_evar ev rhs then error_occur_check CCI empty_env ev rhs;
-  let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit)
-      (Array.to_list argsv) in 
+  let args = List.map keep_rels_and_vars (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
   (* the substitution to invert *)
   let worklist = make_subst evd.evar_env args in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5743d7d063..bb396f528a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -42,7 +42,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
       (mkAppliedInd indt) (mis_nconstr mispec);
   if mis_is_recursive_subset [tyi] mispec then
     let dep = find_case_dep_nparams env sigma (c,p) indf pt in 
-    let init_depFvec i = if i = tyi then Some(dep,Rel 1) else None in
+    let init_depFvec i = if i = tyi then Some(dep,mkRel 1) else None in
     let depFvec = Array.init (mis_ntypes mispec) init_depFvec in
     let constrs = get_constructors indf in
     (* build now the fixpoint *)
@@ -64,7 +64,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
 	(lambda_create env
 	   (applist (mI,List.append (List.map (lift (nar+1)) params)
                        (rel_list 0 nar)),
-            mkMutCase (ci, lift (nar+2) p, Rel 1, branches)))
+            mkMutCase (ci, lift (nar+2) p, mkRel 1, branches)))
         (lift_context 1 lnames) 
     in
     if noccurn 1 deffix then 
@@ -91,14 +91,6 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
 
 (***********************************************************************)
 
-(*
-let ctxt_of_ids ids =
-  Array.map
-    (function
-       | RRef (_,RVar id) -> VAR id
-       | _ -> error "pretyping: arbitrary subst of ref not implemented")
-    ids
-*)
 let ctxt_of_ids cl = cl
 
 let mt_evd = Evd.empty
@@ -164,11 +156,11 @@ let pretype_id loc env lvar id =
   with Not_found ->
   try
     let (n,typ) = lookup_rel_id id (rel_context env) in
-    { uj_val  = Rel n; uj_type = typed_app (lift n) typ }
+    { uj_val  = mkRel n; uj_type = typed_app (lift n) typ }
   with Not_found ->
   try
     let typ = lookup_id_type id (var_context env) in
-    { uj_val  = VAR id; uj_type = typ }
+    { uj_val  = mkVar id; uj_type = typ }
   with Not_found ->
     error_var_not_found_loc loc CCI id
 
@@ -442,9 +434,9 @@ let j_apply f env sigma j =
     uj_type= typed_app (strong f env sigma) j.uj_type }
 
 let utj_apply f env sigma j =
-  let under_outer_cast f env sigma = function
-    | DOP2 (Cast,b,t) -> DOP2 (Cast,f env sigma b,f env sigma t)
-    | c -> f env sigma c in
+  let under_outer_cast f env sigma c = match kind_of_term c with
+    | IsCast (b,t) -> mkCast (f env sigma b,f env sigma t)
+    | _ -> f env sigma c in
   { utj_val = strong (under_outer_cast f) env sigma j.utj_val;
     utj_type = j.utj_type }