suppression champs inutiles dans constantes et inductifs; verification definitions inductives

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

1 files changed, 18 insertions, 301 deletions

diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index c2309f8eda..7e81089453 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -1165,265 +1165,6 @@ let compute_consteval env c =
   in
   try Some (srec 0 [] c) with Elimconst -> None
 
-let is_elim env c =
-  let (sp, cl) = destConst c in
-  if evaluable_const env c && defined_const env c && (not (is_existential c))
-  then
-    let cb = lookup_constant sp env in 
-    begin match cb.const_eval with
-      | Some _ -> ()
-      | None -> 
-	  (match cb.const_body with
-	     | Some {contents = Cooked b} ->
-		 cb.const_eval <- Some (compute_consteval env b)
-	     | Some {contents = Recipe _} ->
-		 anomalylabstrm "Reduction.is_elim"
-		   [< 'sTR"Found an uncooked transparent constant," ; 'sPC ;
-		      'sTR"which is supposed to be impossible" >]
-	     | _ -> assert false)
-    end;
-    match (cb.const_eval) with
-      | Some (Some x) -> x
-      | Some None -> raise Elimconst
-      | _ -> assert false
-  else 
-    raise Elimconst
-
-(* takes the fn first elements of the list and gives them back lifted by ln 
-   and in reverse order *)
-
-let rev_firstn_liftn fn ln = 
-  let rec rfprec p res l = 
-    if p = 0 then 
-      res 
-    else
-      match l with
-        | [] -> invalid_arg "Reduction.rev_firstn_liftn"
-        | a::rest -> rfprec (p-1) ((lift ln a)::res) rest
-  in 
-  rfprec fn [] 
-
-let make_elim_fun env f largs =
-  try 
-    let (lv,n,b) = is_elim env f 
-    and ll = List.length largs in
-    if ll < n then 
-      raise Redelimination 
-    else
-      if b then
-	let labs,_ = list_chop n largs in
-	let p = List.length lv in
-        let la' = 
-	  list_map_i 
-	    (fun q aq ->
-	       try (Rel (p+1-(list_index (n+1-q) (List.map fst lv)))) 
-	       with Failure _ -> aq) 
-	    1
-            (List.map (lift p) labs) 
-	in
-        list_fold_left_i 
-	  (fun i c (k,a) -> 
-             DOP2(Lambda,(substl (rev_firstn_liftn (n-k) (-i) la') a),
-		  DLAM(Name(id_of_string"x"),c))) 
-	  0 (applistc f la') lv
-      else 
-	f
-  with 
-    | Elimconst | Failure _ -> raise Redelimination
-
-let rec red_elim_const env k largs =
-  if not(evaluable_const env k) then raise Redelimination else
-    let f = make_elim_fun env k largs in
-    match whd_betadeltaeta_stack env (const_or_ex_value env k) largs with
-      | (DOPN(MutCase _,_) as mc,lrest) ->
-          let (ci,p,c,lf) = destCase mc in
-          (special_red_case env (construct_const env) p c ci lf, lrest)
-      | (DOPN(Fix _,_) as fix,lrest) -> 
-          let (b,(c,rest)) = 
-	    reduce_fix_use_function f (construct_const env) fix lrest
-          in 
-	  if b then (nf_beta env c, rest) else raise Redelimination
-      | _ -> assert false
-
-and construct_const env c stack = 
-  let rec hnfstack x stack =
-    match x with
-      | (DOPN(Const _,_)) as k  ->
-          (try
-             let (c',lrest) = red_elim_const env k stack in
-             hnfstack c' lrest
-           with 
-	     | Redelimination ->
-		 if evaluable_const env k then
-		   let cval = const_or_ex_value env k in
-		   (match cval with
-		      | DOPN (CoFix _,_) -> (k,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
-      | DOP2(Cast,c,_) -> hnfstack c stack
-      | DOPN(AppL,cl) -> hnfstack (array_hd cl) (array_app_tl cl stack)
-      | DOP2(Lambda,_,DLAM(_,c)) ->
-          (match stack with 
-             | [] -> assert false
-             | c'::rest -> stacklam hnfstack [c'] c rest)
-      | DOPN(MutCase _,_) as c_0 ->
-          let (ci,p,c,lf) = destCase c_0 in
-          hnfstack (special_red_case env (construct_const env) p c ci lf) stack
-      | DOPN(MutConstruct _,_) as c_0 -> c_0,stack
-      | DOPN(CoFix _,_) as c_0 -> c_0,stack
-      | DOPN(Fix (_) ,_) as fix -> 
-          let (reduced,(fix,stack')) = reduce_fix hnfstack fix stack in
-          if reduced then hnfstack fix stack' else raise Redelimination
-      | _ -> raise Redelimination
-  in 
-  hnfstack c stack
-
-(* Hnf reduction tactic: *)
-let hnf_constr env c = 
-  let rec redrec x largs =
-    match x with
-      | DOP2(Lambda,t,DLAM(n,c)) ->
-          (match largs with
-             | []      -> applist(x,largs)
-             | a::rest -> stacklam redrec [a] c rest)
-      | DOPN(AppL,cl)   -> redrec (array_hd cl) (array_app_tl cl largs)
-      | DOPN(Const _,_) ->
-          (try
-             let (c',lrest) = red_elim_const env x largs in
-             redrec c' lrest
-           with Redelimination ->
-             if evaluable_const env x then
-               let c = const_or_ex_value env x in
-               match c with 
-                 | DOPN(CoFix _,_) -> x
-                 | _ ->  redrec c largs
-             else 
-	       applist(x,largs))
-      | DOPN(Abst _,_) ->
-          if evaluable_abst env x then 
-	    redrec (abst_value env x) largs
-          else 
-	    applist(x,largs)
-      | DOP2(Cast,c,_) -> redrec c largs
-      | DOPN(MutCase _,_) ->
-          let (ci,p,c,lf) = destCase x in
-          (try
-             redrec (special_red_case env (whd_betadeltaiota_stack env)
-		       p c ci lf) largs
-           with Redelimination -> 
-	     applist(x,largs))
-      | (DOPN(Fix _,_)) ->
-          let (reduced,(fix,stack)) = 
-            reduce_fix (whd_betadeltaiota_stack env) x largs
-          in 
-	  if reduced then redrec fix stack else applist(x,largs)
-      | _ -> applist(x,largs)
-  in 
-  redrec c []
-
-
-(* Simpl reduction tactic: same as simplify, but also reduces elimination constants *)
-let whd_nf env c = 
-  let rec nf_app c stack =
-    match c with
-      | DOP2(Lambda,c1,DLAM(name,c2))    ->
-          (match stack with
-             | [] -> (c,[])
-             | a1::rest -> stacklam nf_app [a1] c2 rest)
-      | DOPN(AppL,cl)      -> nf_app (array_hd cl) (array_app_tl cl stack)
-      | DOP2(Cast,c,_) -> nf_app c stack
-      | DOPN(Const _,_) ->
-          (try
-             let (c',lrest) = red_elim_const env c stack in
-             nf_app c' lrest
-           with Redelimination -> 
-	     (c,stack))
-      | DOPN(MutCase _,_) ->
-          let (ci,p,d,lf) = destCase c in
-          (try
-             nf_app (special_red_case env nf_app p d ci lf) stack
-           with Redelimination -> 
-	     (c,stack))
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,rest)) = reduce_fix nf_app c stack in
-          if reduced then nf_app fix rest else (fix,stack)
-      | _ -> (c,stack)
-  in 
-  applist (nf_app c [])
-
-let nf env c = strong (whd_nf env) env c
-
-
-(* Generic reduction: reduction functions used in reduction tactics *)
-type red_expr =
-  | Red
-  | Hnf
-  | Simpl
-  | Cbv of flags
-  | Lazy of flags
-  | Unfold of (int list * section_path) list
-  | Fold of constr list
-  | Change of constr
-  | Pattern of (int list * constr * constr) list
-
-let reduction_of_redexp = function
-  | Red -> red_product
-  | Hnf -> hnf_constr
-  | Simpl -> nf
-  | Cbv f -> cbv_norm_flags f
-  | Lazy f -> clos_norm_flags f
-  | Unfold ubinds -> unfoldn ubinds
-  | Fold cl -> fold_commands cl
-  | Change t -> (fun _ _ -> t)
-  | Pattern lp -> pattern_occs lp
-
-(* Other reductions *)
-
-let one_step_reduce env = 
-  let rec redrec largs x =
-    match x with
-      | DOP2(Lambda,t,DLAM(n,c))  ->
-          (match largs with
-             | []      -> error "Not reducible 1"
-             | a::rest -> applistc (subst1 a c) rest)
-      | DOPN(AppL,cl) -> redrec (array_app_tl cl largs) (array_hd cl)
-      | DOPN(Const _,_) ->
-          (try
-             let (c',l) = red_elim_const env x largs in
-             applistc c' l
-           with Redelimination ->
-	     if evaluable_const env x then
-	       applistc (const_or_ex_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"
-      | DOPN(MutCase _,_) ->
-          let (ci,p,c,lf) = destCase x in
-          (try  
-	     applistc (special_red_case env 
-			 (whd_betadeltaiota_stack env) p c ci lf) largs 
-           with Redelimination -> 
-	     error "Not reducible 2")
-      | DOPN(Fix _,_) ->
-          let (reduced,(fix,stack)) = 
-	    reduce_fix (whd_betadeltaiota_stack env) x largs
-          in 
-	  if reduced then applistc fix stack else error "Not reducible 3"
-      | DOP2(Cast,c,_) -> redrec largs c
-      | _ -> error "Not reducible 3"
-  in 
-  redrec []
-
 (* One step of approximation *)
 
 let rec apprec env c stack =
@@ -1446,7 +1187,6 @@ let rec apprec env c stack =
 
 let hnf env c = apprec env c []
 
-
 (* A reduction function like whd_betaiota but which keeps casts
  * and does not reduce redexes containing meta-variables.
  * ASSUMES THAT APPLICATIONS ARE BINARY ONES.
@@ -1486,39 +1226,6 @@ let whd_programs_stack env =
 
 let whd_programs env x = applist (whd_programs_stack env x [])
 
-
-(* Used in several tactics, moved from tactics.ml *)
-(* -- Eduardo                                     *)
-
-(* 
- * put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name
- * return name, B and t' 
-*)
-
-let reduce_to_mind env t = 
-  let rec elimrec t l = 
-    match whd_castapp_stack t [] with
-      | (DOPN(MutInd _,_) as mind,_) -> (mind,t,prod_it t l)
-      | (DOPN(Const _,_),_) -> 
-          (try 
-	     let t' = nf_betaiota env (one_step_reduce env t) in
-             elimrec t' l
-           with UserError _ -> 
-	     errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product: it is a constant." >])
-      | (DOPN(MutCase _,_),_) ->
-          (try 
-	     let t' = nf_betaiota env (one_step_reduce env t) in
-             elimrec t' l
-           with UserError _ -> 
-	     errorlabstrm "tactics__reduce_to_mind"
-               [< 'sTR"Not an inductive product: it is a case analysis." >])
-      | (DOP2(Cast,c,_),[]) -> elimrec c l
-      | (DOP2(Prod,ty,DLAM(n,t')),[]) -> elimrec t' ((n,ty)::l)
-      | _ -> error "Not an inductive product"
-  in 
-  elimrec t []
-    
 let find_mrectype env c =
   let (t,l) = whd_betadeltaiota_stack env c [] in
   match t with
@@ -1563,24 +1270,24 @@ let check_mrectype_spec env c =
 
 exception IsType
 
-let info_arity env = 
+let is_arity env = 
   let rec srec c = 
     match whd_betadeltaiota env c with 
-      | DOP0(Sort(Prop(Null)))  -> false 
-      | DOP0(Sort(Prop(Pos)))  -> true 
+      | DOP0(Sort _) -> true
       | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
       | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
-      | _ -> raise IsType
+      | _ -> false
   in 
   srec 
-    
-let is_type_arity env = 
+ 
+let info_arity env = 
   let rec srec c = 
     match whd_betadeltaiota env c with 
-      | DOP0(Sort(Type(_)))  -> true
+      | DOP0(Sort(Prop Null)) -> false 
+      | DOP0(Sort(Prop Pos)) -> true 
       | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
       | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
-      | _ -> false
+      | _ -> raise IsType
   in 
   srec 
     
@@ -1590,6 +1297,16 @@ let is_logic_arity env c =
 let is_info_arity env c = 
   try (info_arity env c) with IsType -> true
    
+let is_type_arity env = 
+  let rec srec c = 
+    match whd_betadeltaiota env c with 
+      | DOP0(Sort(Type _)) -> true
+      | DOP2(Prod,_,DLAM(_,c')) -> srec c' 
+      | DOP2(Lambda,_,DLAM(_,c')) -> srec c' 
+      | _ -> false
+  in 
+  srec 
+    
 let is_info_cast_type env c = 
   match c with  
     | DOP2(Cast,c,t) ->