X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=576721be3542c1b67a098c05f0fbbadede1e2f85;hb=38d3574438b4f764ad433915c9733cc73a684b39;hp=f4880e426de66ffd74b78808eea763cb4b761a71;hpb=37018b8195f0f376d9eb04a98cbda5550f7ac8ef;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index f4880e426..576721be3 100644
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -1120,46 +1120,49 @@ 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 =
+ 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 =