From d774aa49f50598f725ded815b87949110a6acdcf Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 29 Jun 2005 15:17:19 +0000
Subject: [PATCH] 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.
---
helm/ocaml/tactics/proofEngineReduction.ml | 19 +++++++++++--------
1 file changed, 11 insertions(+), 8 deletions(-)
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
--
2.39.5