From 7a651a85d575ff0294f76f78d7771b96e50c5012 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 3 Feb 2010 15:41:02 +0000 Subject: [PATCH] Bug fixed: projection redexes obtained reducing other projection redexes were not reduced. --- .../components/ng_kernel/nCicUntrusted.ml | 22 ++++++++++--------- 1 file changed, 12 insertions(+), 10 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicUntrusted.ml b/helm/software/components/ng_kernel/nCicUntrusted.ml index 1d8f6c49e..524a00cd3 100644 --- a/helm/software/components/ng_kernel/nCicUntrusted.ml +++ b/helm/software/components/ng_kernel/nCicUntrusted.ml @@ -175,21 +175,23 @@ let rec fire_projection_redex on_args = function in if pragma <> `Projection || List.length args <= rno then conclude () else - (match List.nth args rno with + (match List.nth l (rno+1) with | C.Appl (C.Const(Ref.Ref(_,Ref.Con _))::_) -> let _, _, _, _, fbody = List.nth ifl fno in (* fbody is closed! *) - let t = C.Appl (fbody::args) in + let t = C.Appl (fbody::List.tl l) in (match NCicReduction.head_beta_reduce ~delta:max_int t with - | C.Match (_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat])-> + | C.Match (_,_, C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno))) + ::kargs),[pat])-> let _,kargs = HExtlib.split_nth leftno kargs in - fire_projection_redex false - (NCicReduction.head_beta_reduce - ~delta:max_int (C.Appl (pat :: kargs))) - | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno)))::kargs),[pat]) :: args) -> + fire_projection_redex false + (NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs))) + | C.Appl(C.Match(_,_,C.Appl(C.Const(Ref.Ref(_,Ref.Con (_,_,leftno))) + ::kargs),[pat]) :: args) -> let _,kargs = HExtlib.split_nth leftno kargs in - fire_projection_redex false - (NCicReduction.head_beta_reduce - ~delta:max_int (C.Appl (pat :: kargs @ args))) + fire_projection_redex false + (NCicReduction.head_beta_reduce + ~delta:max_int (C.Appl (pat :: kargs @ args))) | _ -> conclude ()) | _ -> conclude ()) | t when on_args -> NCicUtils.map (fun _ x -> x) true fire_projection_redex t -- 2.39.2