From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 2 Oct 2009 17:54:16 +0000 (+0000)
Subject: projections redex (proj (mk_foo ...)) where mk_foo
X-Git-Tag: make_still_working~3396
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=56d3455abc6bcffd9d0e2af3ed370bf0751057a0;p=helm.git

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
---

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, _ ->