From b3ee75c483592e858017a17e55f782d0c28fae51 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 11 Oct 2002 17:57:37 +0000 Subject: [PATCH] Trivial bug in equality_replace fixed: an exception was raised in spite of returning false. --- helm/gTopLevel/proofEngineReduction.ml | 40 +++++++++++++++++--------- 1 file changed, 27 insertions(+), 13 deletions(-) diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml index 265e5f99c..442873cec 100644 --- a/helm/gTopLevel/proofEngineReduction.ml +++ b/helm/gTopLevel/proofEngineReduction.ml @@ -73,7 +73,11 @@ let rec syntactic_equality t t' = syntactic_equality s s' && syntactic_equality t t' | C.Appl l, C.Appl l' -> - List.fold_left2 (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' + (try + List.fold_left2 + (fun b t1 t2 -> b && syntactic_equality t1 t2) true l l' + with + Invalid_argument _ -> false) | C.Const (uri,_), C.Const (uri',_) -> UriManager.eq uri uri' | C.MutInd (uri,_,i), C.MutInd (uri',_,i') -> UriManager.eq uri uri' && i = i' @@ -83,22 +87,31 @@ let rec syntactic_equality t t' = UriManager.eq sp sp' && i = i' && syntactic_equality outt outt' && syntactic_equality t t' && - List.fold_left2 - (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' + (try + List.fold_left2 + (fun b t1 t2 -> b && syntactic_equality t1 t2) true pl pl' + with + Invalid_argument _ -> false) | C.Fix (i,fl), C.Fix (i',fl') -> i = i' && - List.fold_left2 - (fun b (name,i,ty,bo) (name',i',ty',bo') -> - b && name = name' && i = i' && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' + (try + List.fold_left2 + (fun b (name,i,ty,bo) (name',i',ty',bo') -> + b && name = name' && i = i' && + syntactic_equality ty ty' && + syntactic_equality bo bo') true fl fl' + with + Invalid_argument _ -> false) | C.CoFix (i,fl), C.CoFix (i',fl') -> i = i' && - List.fold_left2 - (fun b (name,ty,bo) (name',ty',bo') -> - b && name = name' && - syntactic_equality ty ty' && - syntactic_equality bo bo') true fl fl' + (try + List.fold_left2 + (fun b (name,ty,bo) (name',ty',bo') -> + b && name = name' && + syntactic_equality ty ty' && + syntactic_equality bo bo') true fl fl' + with + Invalid_argument _ -> false) | _,_ -> false ;; @@ -152,6 +165,7 @@ let replace_lifting ~equality ~what ~with_what ~where = let rec substaux k = let module C = Cic in function +(*CSC: Possibile bug: debbo liftare di k what? *) t when (equality t what) -> CicSubstitution.lift (k-1) with_what | C.Rel n as t -> t (*CSC: ??? BUG ? *) | C.Var _ as t -> t -- 2.39.2