made matita.runtime_base_dir overridable setting MATITA_RUNTIME_BASE_DIR env variable

[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 bd8d07b8dd9a516bac801de533b1329864acc58b..213aa2356bd1e3d9940efccdc4420f1e7dd05b2b 100644 (file)
--- a/components/cic_proof_checking/cicReduction.ml
+++ b/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 =
@@ -714,12 +712,12 @@ if List.mem uri params then debug_print (lazy "---- OK2") ;
                     let leng = List.length fl in
                     let new_env =
                      let counter = ref 0 in
-                     let rec build_env e =
-                      if !counter = leng then e
+                     let rec build_env e' =
+                      if !counter = leng then e'
                       else
                        (incr counter ;
                         build_env
-                         ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e))
+                         ((RS.to_env (k,e,ens,C.Fix (!counter -1, fl),[]))::e'))
                      in
                       build_env e
                     in
@@ -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 *)
@@ -971,8 +973,12 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.Fix (i1,fl1), C.Fix (i2,fl2)) ->
-            let tys =
-              List.map (function (n,_,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
+            let tys,_ =
+              List.fold_left
+                (fun (types,len) (n,_,ty,_) ->
+                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                    len+1)
+               ) ([],0) fl1
             in
             if i1 = i2 then
              List.fold_right2
@@ -990,9 +996,13 @@ prerr_endline ("%%%%%%: " ^ CicPp.ppterm term' ^ " <==> " ^ CicPp.ppterm t1);
             else
               false,ugraph
         | (C.CoFix (i1,fl1), C.CoFix (i2,fl2)) ->
-           let tys =
-            List.map (function (n,ty,_) -> Some (C.Name n,(C.Decl ty))) fl1
-           in
+            let tys,_ =
+              List.fold_left
+                (fun (types,len) (n,ty,_) ->
+                   (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
+                    len+1)
+               ) ([],0) fl1
+            in
             if i1 = i2 then
               List.fold_right2
               (fun (_,ty1,bo1) (_,ty2,bo2) (b,ugraph) ->
@@ -1008,7 +1018,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,21 +1128,49 @@ 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 =
+ 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 =