elim tactic: it needs two arguments, a term as well as a pattern

[helm.git] / components / cic_proof_checking / cicReduction.ml

diff --git a/components/cic_proof_checking/cicReduction.ml b/components/cic_proof_checking/cicReduction.ml
index f4880e426de66ffd74b78808eea763cb4b761a71..6e963a274d06befaf6e6e897009e88aad9a9473c 100644 (file)
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/components/cic_proof_checking/cicReduction.ml
@@ -1120,46 +1120,50 @@ let normalize ?delta ?subst ctx term =
   
   
 (* performs an head beta/cast reduction *)
-let rec head_beta_reduce ?(delta=false) =
- function
-    (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
-      let he'' = CicSubstitution.subst he' t in
-       if tl' = [] then
-        he''
-       else
-        let he''' =
-         match he'' with
-            Cic.Appl l -> Cic.Appl (l@tl')
-          | _ -> Cic.Appl (he''::tl')
+let rec head_beta_reduce ?(delta=false) ?(upto=(-1)) t =
+ HLog.warn (Printf.sprintf "inside head_beta_reduce %i %s" upto (CicPp.ppterm t));
+ match upto with
+    0 -> t
+  | n ->
+    match t with
+       (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
+         let he'' = CicSubstitution.subst he' t in
+          if tl' = [] then
+           he''
+          else
+           let he''' =
+            match he'' with
+               Cic.Appl l -> Cic.Appl (l@tl')
+             | _ -> Cic.Appl (he''::tl')
+           in
+            head_beta_reduce ~delta ~upto:(upto - 1) he'''
+     | Cic.Cast (te,_) -> head_beta_reduce ~delta ~upto te
+     | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
+        let bo =
+         match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+            Cic.Constant (_,bo,_,_,_) -> bo
+          | Cic.Variable _ -> raise ReferenceToVariable
+          | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+          | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
         in
-         head_beta_reduce ~delta he'''
-  | Cic.Cast (te,_) -> head_beta_reduce ~delta te
-  | Cic.Appl (Cic.Const (uri,ens)::tl) as t when delta=true ->
-     let bo =
-      match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
-         Cic.Constant (_,bo,_,_,_) -> bo
-       | Cic.Variable _ -> raise ReferenceToVariable
-       | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
-       | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-     in
-      (match bo with
-          None -> t
-        | Some bo ->
-           head_beta_reduce
-            ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
-  | Cic.Const (uri,ens) as t when delta=true ->
-     let bo =
-      match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
-         Cic.Constant (_,bo,_,_,_) -> bo
-       | Cic.Variable _ -> raise ReferenceToVariable
-       | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
-       | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-     in
-      (match bo with
-          None -> t
-        | Some bo ->
-           head_beta_reduce ~delta (CicSubstitution.subst_vars ens bo))
-  | t -> t
+         (match bo with
+             None -> t
+           | Some bo ->
+              head_beta_reduce ~upto
+               ~delta (Cic.Appl ((CicSubstitution.subst_vars ens bo)::tl)))
+     | Cic.Const (uri,ens) as t when delta=true ->
+        let bo =
+         match fst (CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri) with
+            Cic.Constant (_,bo,_,_,_) -> bo
+          | Cic.Variable _ -> raise ReferenceToVariable
+          | Cic.CurrentProof (_,_,bo,_,_,_) -> Some bo
+          | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
+        in
+         (match bo with
+             None -> t
+           | Some bo ->
+              head_beta_reduce ~delta ~upto (CicSubstitution.subst_vars ens bo))
+     | t -> t
 
 (*
 let are_convertible ?subst ?metasenv context t1 t2 ugraph =