Suppression de Abst

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

8 files changed, 30 insertions, 80 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b01b3e283a..54869505ee 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -79,7 +79,7 @@ let make_case_ml isrec pred c ci lf =
   if isrec then 
     DOPN(XTRA("REC"),Array.append [|pred;c|] lf)
   else 
-    mkMutCaseA ci pred c lf
+    mkMutCase (ci, pred, c, lf)
 
 (* if arity of mispec is (p_bar:P_bar)(a_bar:A_bar)s where p_bar are the
  * K parameters. Then then build_notdep builds the predicate
@@ -598,7 +598,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 = mkMutCaseA caseinfo predpred (Rel 1) brs in
+      let predbody = mkMutCase (caseinfo, predpred, Rel 1, brs) in
       let pred = lam_it (lift (List.length sign) typn) sign in
       failwith "TODO4-2"; (true,pred)
 
@@ -833,7 +833,7 @@ and match_current pb (n,tm) =
 	    find_predicate pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt in
 	  let ci = make_case_info mis None tags in
-	  { uj_val = mkMutCaseA ci (*eta_reduce_if_rel*) pred current brvals;
+	  { uj_val = mkMutCase (ci, (*eta_reduce_if_rel*)pred,current,brvals);
 	    uj_type = make_typed typ s }
 
 and compile_further pb firstnext rest =
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 596310512a..a6d06f3f95 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -30,11 +30,30 @@ open Rawterm
 
 type used_idents = identifier list
 
+exception Occur
+
+let occur_rel p env id = 
+  try lookup_name_of_rel p env = Name id
+  with Not_found -> false (* Unbound indice : may happen in debug *)
+
+let occur_id env id0 c =
+  let rec occur n c = match kind_of_term c with
+    | IsVar id when  id=id0 -> raise Occur
+    | IsConst (sp, _) when basename sp = id0 -> raise Occur
+    | IsMutInd (ind_sp, _)
+	when basename (path_of_inductive_path ind_sp) = id0 -> raise Occur
+    | IsMutConstruct (cstr_sp, _) 
+	when basename (path_of_constructor_path cstr_sp) = id0 -> raise Occur
+    | IsRel p when p>n & occur_rel (p-n) env id0 -> raise Occur
+    | _ -> iter_constr_with_binders succ occur n c
+  in 
+  try occur 1 c; false
+  with Occur -> true
+(*
 let occur_id env_names id0 c =
   let rec occur n = function
     | VAR id             -> id=id0
     | DOPN (Const sp,cl) -> (basename sp = id0) or (array_exists (occur n) cl)
-    | DOPN (Abst sp,cl)  -> (basename sp = id0) or (array_exists (occur n) cl)
     | DOPN (MutInd ind_sp, cl) as t -> 
   	(basename (path_of_inductive_path ind_sp) = id0)
 	or (array_exists (occur n) cl)
@@ -56,7 +75,7 @@ let occur_id env_names id0 c =
     | DOP0 _             -> false
   in 
   occur 1 c
-
+*)
 let next_name_not_occuring name l env_names t =
   let rec next id =
     if List.mem id l or occur_id env_names id t then next (lift_ident id)
@@ -83,7 +102,6 @@ let global_vars_and_consts t =
     match op with
     | OpVar id -> id::acc'
     | OpConst sp -> (basename sp)::acc'
-    | OpAbst sp  -> (basename sp)::acc'
     | OpMutInd ind_sp -> (basename (path_of_inductive_path ind_sp))::acc'
     | OpMutConstruct csp -> (basename (path_of_constructor_path csp))::acc'
     | _ -> acc'
@@ -247,15 +265,6 @@ let computable p k =
   in 
   striprec (k,p)
 
-(*
-let ids_of_var cl =
-  List.map
-    (function 
-       | RRef (_,RVar id) -> id
-       | _-> anomaly "ids_of_var")
-    (Array.to_list cl)
-*)
-
 let lookup_name_as_renamed ctxt t s =
   let rec lookup avoid env_names n c = match kind_of_term c with
     | IsProd (name,t,c') ->
@@ -278,12 +287,10 @@ let lookup_index_as_renamed t n =
     | _ -> None
   in lookup n 1 t
 
-exception StillDLAM
-
 let rec detype avoid env t =
   match collapse_appl t with
     (* Not well-formed constructions *)
-    | DLAM _ | DLAMV _ -> raise StillDLAM
+    | DLAM _ | DLAMV _ -> error "Cannot detype"
     (* Well-formed constructions *)
     | regular_constr -> 
     (match kind_of_term regular_constr with
@@ -312,8 +319,6 @@ let rec detype avoid env t =
 	RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl))
     | IsEvar (ev,cl) ->
 	RRef(dummy_loc,REVar(ev,Array.map (detype avoid env) cl))
-    | IsAbst (sp,cl) -> 
-	anomaly "bdize: Abst should no longer occur in constr"
     | IsMutInd (ind_sp,cl) ->
 	RRef (dummy_loc,RInd (ind_sp,Array.map (detype avoid env) cl))
     | IsMutConstruct (cstr_sp,cl) ->
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index e961cfe917..8c8dd417d1 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -12,8 +12,6 @@ open Rawterm
 (* [detype avoid env c] turns [c], typed in [env], into a rawconstr. *)
 (* De Bruijn indexes are turned to bound names, avoiding names in [avoid] *)
 
-exception StillDLAM
-
 val detype : identifier list -> names_context -> constr -> rawconstr
 
 (* look for the index of a named var or a nondep var as it is renamed *)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e4e2e48c59..f9a3fe69b0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -210,32 +210,6 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	in 
 	ise_try isevars [f3; f4]
 
-    | IsAbst (_,_), IsAbst (_,_) ->
-	let f1 () =
-          (term1=term2) &
- 	  (List.length(l1) = List.length(l2)) &
- 	  (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
-	and f2 () =
-          if evaluable_abst env term2 then 
-	    evar_eqappr_x env isevars pbty
-              appr1 (evar_apprec env isevars l2 (abst_value env term2))
-	  else 
-	    evaluable_abst env term1
-            & evar_eqappr_x env isevars pbty
-              (evar_apprec env isevars l1 (abst_value env term1)) appr2
-	in 
-	ise_try isevars [f1; f2]
-
-    | IsAbst (_,_), _ ->  
-        (evaluable_abst env term1)
-	& evar_eqappr_x env isevars pbty
-          (evar_apprec env isevars l1 (abst_value env term1)) appr2
-	  
-    | _, IsAbst (_,_)  -> 
-        (evaluable_abst env term2)
-	& evar_eqappr_x env isevars pbty
- 	  appr1 (evar_apprec env isevars l2 (abst_value env term2))
-
     | IsRel n, IsRel m ->
 	n=m
 	  & (List.length(l1) = List.length(l2))
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 09dd230654..295e081a34 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -96,7 +96,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)),
-            mkMutCaseA ci (lift (nar+2) p) (Rel 1) branches))
+            mkMutCase (ci, lift (nar+2) p, Rel 1, branches)))
         (lift_context 1 lnames) 
     in
     if noccurn 1 deffix then 
@@ -119,7 +119,7 @@ let transform_rec loc env sigma (p,c,lf) (indt,pt) =
       applist (fix,realargs@[c])
   else
     let ci = make_default_case_info mispec in
-    mkMutCaseA ci p c lf
+    mkMutCase (ci, p, c, lf)
 
 (***********************************************************************)
 
@@ -217,8 +217,6 @@ let pretype_ref pretype loc isevars env lvar = function
     let cst = (sp,Array.map pretype ctxt) in
     make_judge (mkConst cst) (type_of_constant env !isevars cst)
 
-| RAbst sp -> failwith "Pretype: abst doit disparaître"
-
 | REVar (sp,ctxt) -> error " Not able to type terms with dependent subgoals"
 
 | RInd (ind_sp,ctxt) ->
@@ -401,7 +399,7 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
       else
 	let mis,_ = dest_ind_family indf in
 	let ci = make_default_case_info mis in
-	mkMutCaseA ci pj.uj_val cj.uj_val (Array.map (fun j-> j.uj_val) lfj)
+	mkMutCase (ci, pj.uj_val, cj.uj_val, Array.map (fun j-> j.uj_val) lfj)
     in
     let s = snd (splay_arity env !isevars evalPt) in
     {uj_val = v;
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index aa499fb630..bd1b88bea5 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -48,7 +48,6 @@ let rec type_of env cstr=
       (try body_of_type (snd (lookup_var id env))
        with Not_found ->
          anomaly ("type_of: variable "^(string_of_id id)^" unbound"))
-    | IsAbst _ -> error "No more Abst" (*type_of env (abst_value cstr)*)
     | IsConst c -> body_of_type (type_of_constant env sigma c)
     | IsEvar _ -> type_of_existential env sigma cstr
     | IsMutInd ind -> body_of_type (type_of_inductive env sigma ind)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 16eebbefb7..dde27dbae8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -91,7 +91,7 @@ let reduce_mind_case_use_function env f mia =
 	applist (mia.mlf.(i-1),real_cargs)
     | DOPN(CoFix _,_) as cofix ->
 	let cofix_def = contract_cofix_use_function f (destCoFix cofix) in
-	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
+	mkMutCase (mia.mci, mia.mP, applist(cofix_def,mia.mcargs), mia.mlf)
     | _ -> assert false
 	  
 let special_red_case env whfun p c ci lf  =
@@ -160,13 +160,6 @@ and construct_const env sigma c stack =
                   | _ -> hnfstack (cval, stack))
              else 
 	       raise Redelimination)
-(*
-      | (DOPN(Abst _,_) as a) ->
-          if evaluable_abst env a then 
-	    hnfstack (abst_value env a) stack
-          else 
-	    raise Redelimination
-*)
       | IsCast (c,_) -> hnfstack (c, stack)
       | IsAppL (f,cl) -> hnfstack (f, cl@stack)
       | IsLambda (_,_,c) ->
@@ -208,13 +201,6 @@ let hnf_constr env sigma c =
 		  | _ ->  redrec (c, largs))
              else 
 	       applist s)
-(*
-      | DOPN(Abst _,_) ->
-          if evaluable_abst env x then 
-	    redrec (abst_value env x) largs
-          else 
-	    applist s
-*)
       | IsCast (c,_) -> redrec (c, largs)
       | IsMutCase (ci,p,c,lf) ->
           (try
@@ -307,11 +293,7 @@ let one_step_reduce env sigma c =
              if evaluable_constant env x then
                applistc (constant_value env x) largs
              else error "Not reductible 1")
-(*
-      | DOPN(Abst _,_) ->
-          if evaluable_abst env x then applistc (abst_value env x) largs
-          else error "Not reducible 0"
-*)
+
       | IsMutCase (ci,p,c,lf) ->
           (try
 	     applistc 
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5dfcfdce3c..cbe8b36013 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -40,12 +40,6 @@ let rec execute mf env sigma cstr =
        with Not_found ->
          error ("execute: variable " ^ (string_of_id id) ^ " not defined"))
 	  
-    | IsAbst _ ->
-        if evaluable_abst env cstr then 
-	  execute mf env sigma (abst_value env cstr)
-        else 
-	  error "Cannot typecheck an unevaluable abstraction"
-	      
     | IsConst c ->
         make_judge cstr (type_of_constant env sigma c)