From 56d3455abc6bcffd9d0e2af3ed370bf0751057a0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 2 Oct 2009 17:54:16 +0000 Subject: [PATCH] projections redex (proj (mk_foo ...)) where mk_foo is explicit (not the result of a reduction) are always fired. on the contrary, when the delta avoids the reduction of a projetion (since the arg reduces to mk_foo but for a smaller delta) we store in stack not the reduct but its original version (before reducing it to delta=0). This seems nice anyway, and a FIXME is left in the code --- .../components/ng_kernel/nCicReduction.ml | 29 ++++++++++++++----- 1 file changed, 22 insertions(+), 7 deletions(-) diff --git a/helm/software/components/ng_kernel/nCicReduction.ml b/helm/software/components/ng_kernel/nCicReduction.ml index a88a1aaf3..e1e5bc7cb 100644 --- a/helm/software/components/ng_kernel/nCicReduction.ml +++ b/helm/software/components/ng_kernel/nCicReduction.ml @@ -141,21 +141,36 @@ module Reduction(RS : Strategy) = struct (Ref.Decl|Ref.Ind _|Ref.Con _|Ref.CoFix _))), _) as config -> config, true | (_, _, (C.Const (Ref.Ref - (_,Ref.Fix (fixno,recindex,height)) as refer) as head),s) as config -> -(* if delta >= height then config else *) + (_,Ref.Fix (fixno,recindex,height)) as refer) as head),s) as config -> (match - try Some (RS.from_stack ~delta (List.nth s recindex)) + try + let recarg = RS.from_stack ~delta:max_int (List.nth s recindex) in + let fixes,(_,_,pragma),_ = + NCicEnvironment.get_checked_fixes_or_cofixes refer in + Some (recarg, fixes, pragma) with Failure _ -> None with | None -> config, true - | Some recparam -> - let fixes,_,_ = NCicEnvironment.get_checked_fixes_or_cofixes refer in + | Some((_,_,C.Const(Ref.Ref(_,Ref.Con _)),_::_ as c),fs,`Projection) -> + let new_s = + replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst + context) ~unwind c) + in + let _,_,_,_,body = List.nth fs fixno in + aux (0, [], body, new_s) + | Some (recparam, fixes, pragma) -> match reduce ~delta:0 ~subst context recparam with | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _ when delta >= height -> let new_s = - replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst - context) ~unwind c) + (* FIXME, we should push on the stack + * c for CBV and recparam for CBN *) + if pragma = `Projection then + replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst + context) ~unwind recparam) + else + replace recindex s (RS.compute_to_stack ~reduce:(reduce ~subst + context) ~unwind c) in (0, [], head, new_s), false | (_,_,C.Const (Ref.Ref (_,Ref.Con _)), _) as c, _ -> -- 2.39.2