X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fcic_proof_checking%2FcicReduction.ml;h=f4880e426de66ffd74b78808eea763cb4b761a71;hb=7e30c63fcf9f9fe1780ba7aa4d95fd0d8658548b;hp=bd8d07b8dd9a516bac801de533b1329864acc58b;hpb=bbdb53860d667dfba1aab3a6f195d0fcd4a9e818;p=helm.git

diff --git a/helm/software/components/cic_proof_checking/cicReduction.ml b/helm/software/components/cic_proof_checking/cicReduction.ml
index bd8d07b8d..f4880e426 100644
--- 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 =
@@ -792,7 +790,7 @@ let (===) x y =
 let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
  let heuristic = ref true in
  let rec aux test_equality_only context t1 t2 ugraph =
-  let aux2 test_equality_only t1 t2 ugraph =
+  let rec aux2 test_equality_only t1 t2 ugraph =
 
    (* this trivial euristic cuts down the total time of about five times ;-) *)
    (* this because most of the time t1 and t2 are "sintactically" the same   *)
@@ -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 *)
@@ -1008,7 +1010,8 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
              fl1 fl2 (true,ugraph)
             else
               false,ugraph
-        | (C.Cast _, _) | (_, C.Cast _)
+        | C.Cast (bo,_),t -> aux2 test_equality_only bo t ugraph
+        | t,C.Cast (bo,_) -> aux2 test_equality_only t bo ugraph
         | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
         | (_,_) -> false,ugraph
     end
@@ -1117,7 +1120,7 @@ let normalize ?delta ?subst ctx term =
   
   
 (* performs an head beta/cast reduction *)
-let rec head_beta_reduce =
+let rec head_beta_reduce ?(delta=false) =
  function
     (Cic.Appl (Cic.Lambda (_,_,t)::he'::tl')) ->
       let he'' = CicSubstitution.subst he' t in
@@ -1129,8 +1132,33 @@ let rec head_beta_reduce =
             Cic.Appl l -> Cic.Appl (l@tl')
           | _ -> Cic.Appl (he''::tl')
         in
-         head_beta_reduce he'''
-  | Cic.Cast (te,_) -> head_beta_reduce te
+         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
 
 (*