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

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

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index de3bf61f4dd6e5a8092cca6466476023e99cbb14..6e963a274d06befaf6e6e897009e88aad9a9473c 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicReduction.ml
+++ b/helm/software/components/cic_proof_checking/cicReduction.ml
@@ -664,14 +664,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
              (k', e', ens', C.MutConstruct (_,_,j,_), []) ->
               reduce (k, e, ens, (List.nth pl (j-1)), s)
            | (k', e', ens', C.MutConstruct (_,_,j,_), s') ->
-              let (arity, r) =
+              let r =
                 let o,_ = 
                   CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
                 in
                   match o with
-                      C.InductiveDefinition (s,ingredients,r,_) ->
-                        let (_,_,arity,_) = List.nth s i in
-                          (arity,r)
+                      C.InductiveDefinition (_,_,r,_) -> r
                     | _ -> raise WrongUriToInductiveDefinition
               in
                let ts =
@@ -858,10 +856,14 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             with  CicUtil.Subst_not_found _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) when test_equality_only ->
-            true,(CicUniv.add_eq t2 t1 ugraph)
+            (try
+              true,(CicUniv.add_eq t2 t1 ugraph)
+             with CicUniv.UniverseInconsistency _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort (C.Type t1), C.Sort (C.Type t2)) ->
-            true,(CicUniv.add_ge t2 t1 ugraph)
+            (try
+              true,(CicUniv.add_ge t2 t1 ugraph)
+             with CicUniv.UniverseInconsistency _ -> false,ugraph)
           (* TASSI: CONSTRAINTS *)
         | (C.Sort s1, C.Sort (C.Type _)) -> (not test_equality_only),ugraph
           (* TASSI: CONSTRAINTS *)
@@ -1118,21 +1120,50 @@ let normalize ?delta ?subst ctx term =
   
   
 (* performs an head beta/cast reduction *)
-let rec head_beta_reduce =
- 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
+         (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
-         head_beta_reduce he'''
-  | Cic.Cast (te,_) -> head_beta_reduce te
-  | t -> t
+         (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 =