From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Jun 2005 15:17:19 +0000 (+0000)
Subject: Incredible bug of simpl fixed: the stack (in the terminology used for the
X-Git-Tag: PRE_GETTER_STORAGE~113
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d774aa49f50598f725ded815b87949110a6acdcf;p=helm.git

Incredible bug of simpl fixed: the stack (in the terminology used for the
Krivine's machine) was processed in the wrong context. As a result List.nth
(to get a Rel in the context) used to raise Failure in several cases. The
Failure, however, was catched somewhere in the code of matita and the
failure of simpl was hidden in most of the cases.
---

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index af41d8ee8..8a6ef81a2 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -596,6 +596,7 @@ exception AlreadySimplified;;
 (*     change in every iteration, i.e. to the actual arguments for the       *)
 (*     lambda-abstractions that precede the Fix.                             *)
 (*CSC: It does not perform simplification in a Case *)
+
 let simpl context =
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
@@ -605,12 +606,14 @@ let simpl context =
   let module S = CicSubstitution in
    function
       C.Rel n as t ->
-       (match List.nth context (n-1) with
-           Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-         | Some (_,C.Def (bo,_)) ->
-            try_delta_expansion l t (S.lift n bo)
-	 | None -> raise RelToHiddenHypothesis
-       )
+       (try
+         match List.nth context (n-1) with
+            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
+          | Some (_,C.Def (bo,_)) ->
+             try_delta_expansion context l t (S.lift n bo)
+	  | None -> raise RelToHiddenHypothesis
+        with
+         Failure _ -> assert false)
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
@@ -659,7 +662,7 @@ let simpl context =
         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	  match o with
            C.Constant (_,Some body,_,_,_) ->
-            try_delta_expansion l
+            try_delta_expansion context l
              (C.Const (uri,exp_named_subst'))
              (CicSubstitution.subst_vars exp_named_subst' body)
          | C.Constant (_,None,_,_,_) ->
@@ -798,7 +801,7 @@ let simpl context =
  and reduceaux_exp_named_subst context l =
   List.map (function uri,t -> uri,reduceaux context [] t)
  (**** Step 2 ****)
- and try_delta_expansion l term body =
+ and try_delta_expansion context l term body =
   let module C = Cic in
   let module S = CicSubstitution in
    try