X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=bb724fc758d2736c40a7c199b60898501fe4308a;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=52f07e4dc2411d8b8aa63a75fcb290c3ebefe044;hpb=9f6cd4bd4cf91930f8a49bc7a274ac5b08459956;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 52f07e4dc..bb724fc75 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -1,4 +1,4 @@
-(* Copyright (C) 2000, HELM Team.
+(* Copyright (C) 2002, HELM Team.
  * 
  * This file is part of HELM, an Hypertextual, Electronic
  * Library of Mathematics, developed at the Computer Science
@@ -43,13 +43,77 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 exception WrongUriToInductiveDefinition;;
+exception RelToHiddenHypothesis;;
+
+(* syntactic_equality up to cookingsno for uris *)
+(* (which is often syntactically irrilevant)    *)
+let syntactic_equality ~alpha_equivalence =
+ let module C = Cic in
+  let rec aux t t' =
+   if t = t' then true
+   else
+    match t,t' with
+       C.Rel _, C.Rel _
+     | C.Var _, C.Var _
+     | C.Meta _, C.Meta _
+     | C.Sort _, C.Sort _
+     | C.Implicit, C.Implicit -> false (* we already know that t != t' *)
+     | C.Cast (te,ty), C.Cast (te',ty') ->
+        aux te te' && aux ty ty'
+     | C.Prod (n,s,t), C.Prod (n',s',t') ->
+        (alpha_equivalence || n = n') && aux s s' && aux t t'
+     | C.Lambda (n,s,t), C.Lambda (n',s',t') ->
+        (alpha_equivalence || n = n') && aux s s' && aux t t'
+     | C.LetIn (n,s,t), C.LetIn(n',s',t') ->
+        (alpha_equivalence || n = n') && aux s s' && aux t t'
+     | C.Appl l, C.Appl l' ->
+        (try
+          List.fold_left2
+           (fun b t1 t2 -> b && aux 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'
+     | C.MutConstruct (uri,_,i,j), C.MutConstruct (uri',_,i',j') ->
+        UriManager.eq uri uri' && i = i' && j = j'
+     | C.MutCase (sp,_,i,outt,t,pl), C.MutCase (sp',_,i',outt',t',pl') ->
+        UriManager.eq sp sp' && i = i' &&
+         aux outt outt' && aux t t' &&
+          (try
+            List.fold_left2
+             (fun b t1 t2 -> b && aux t1 t2) true pl pl'
+           with
+            Invalid_argument _ -> false)
+     | C.Fix (i,fl), C.Fix (i',fl') ->
+        i = i' &&
+        (try
+          List.fold_left2
+           (fun b (name,i,ty,bo) (name',i',ty',bo') ->
+             b && (alpha_equivalence || name = name') && i = i' &&
+              aux ty ty' && aux bo bo') true fl fl'
+         with
+          Invalid_argument _ -> false)
+     | C.CoFix (i,fl), C.CoFix (i',fl') ->
+        i = i' &&
+        (try
+          List.fold_left2
+           (fun b (name,ty,bo) (name',ty',bo') ->
+             b && (alpha_equivalence || name = name') &&
+              aux ty ty' && aux bo bo') true fl fl'
+         with
+          Invalid_argument _ -> false)
+     | _,_ -> false
+ in
+  aux
+;;
 
 (* "textual" replacement of a subterm with another one *)
-let replace ~what ~with_what ~where =
+let replace ~equality ~what ~with_what ~where =
  let module C = Cic in
   let rec aux =
    function
-      t when t = what -> with_what
+      t when (equality t what) -> with_what
     | C.Rel _ as t -> t
     | C.Var _ as t  -> t
     | C.Meta _ as t -> t
@@ -59,9 +123,12 @@ let replace ~what ~with_what ~where =
     | C.Prod (n,s,t) -> C.Prod (n, aux s, aux t)
     | C.Lambda (n,s,t) -> C.Lambda (n, aux s, aux t)
     | C.LetIn (n,s,t) -> C.LetIn (n, aux s, aux t)
-    | C.Appl l -> C.Appl (List.map aux l)
+    | C.Appl l ->
+       (* Invariant enforced: no application of an application *)
+       (match List.map aux l with
+           (C.Appl l')::tl -> C.Appl (l'@tl)
+         | l' -> C.Appl l')
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -85,14 +152,84 @@ let replace ~what ~with_what ~where =
    aux where
 ;;
 
+(* replaces in a term a term with another one. *)
+(* Lifting are performed as usual.             *)
+let replace_lifting ~equality ~what ~with_what ~where =
+ let rec substaux k what =
+  let module C = Cic in
+  let module S = CicSubstitution in
+   function
+      t when (equality t what) -> S.lift (k-1) with_what
+    | C.Rel n as t -> t
+    | C.Var _ as t  -> t
+    | C.Meta (i, l) as t -> 
+       let l' =
+        List.map
+         (function
+             None -> None
+           | Some t -> Some (substaux k what t)
+         ) l
+       in
+        C.Meta(i,l')
+    | C.Sort _ as t -> t
+    | C.Implicit as t -> t
+    | C.Cast (te,ty) -> C.Cast (substaux k what te, substaux k what ty)
+    | C.Prod (n,s,t) ->
+       C.Prod (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+    | C.Lambda (n,s,t) ->
+       C.Lambda (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+    | C.LetIn (n,s,t) ->
+       C.LetIn (n, substaux k what s, substaux (k + 1) (S.lift 1 what) t)
+    | C.Appl (he::tl) ->
+       (* Invariant: no Appl applied to another Appl *)
+       let tl' = List.map (substaux k what) tl in
+        begin
+         match substaux k what he with
+            C.Appl l -> C.Appl (l@tl')
+          | _ as he' -> C.Appl (he'::tl')
+        end
+    | C.Appl _ -> assert false
+    | C.Const _ as t -> t
+    | C.MutInd _ as t -> t
+    | C.MutConstruct _ as t -> t
+    | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
+       C.MutCase (sp,cookingsno,i,substaux k what outt, substaux k what t,
+        List.map (substaux k what) pl)
+    | C.Fix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,i,ty,bo) ->
+           (name, i, substaux k what ty, substaux (k+len) (S.lift len what) bo))
+          fl
+       in
+        C.Fix (i, substitutedfl)
+    | C.CoFix (i,fl) ->
+       let len = List.length fl in
+       let substitutedfl =
+        List.map
+         (fun (name,ty,bo) ->
+           (name, substaux k what ty, substaux (k+len) (S.lift len what) bo))
+          fl
+       in
+        C.CoFix (i, substitutedfl)
+ in
+  substaux 1 what where
+;;
+
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
-let reduce =
- let rec reduceaux l =
+let reduce context =
+ let rec reduceaux context l =
   let module C = Cic in
   let module S = CicSubstitution in
    function
-      C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
+      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) -> reduceaux context l (S.lift n bo)
+	 | None -> raise RelToHiddenHypothesis
+       )
     | C.Var uri as t ->
        (match CicEnvironment.get_cooked_obj uri 0 with
            C.Definition _ -> raise ReferenceToDefinition
@@ -100,65 +237,77 @@ let reduce =
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
          | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
-         | C.Variable (_,Some body,_) -> reduceaux l body
+         | C.Variable (_,Some body,_) -> reduceaux context l body
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
     | C.Implicit as t -> t
-    | C.Cast (te,ty) -> reduceaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
+    | C.Cast (te,ty) ->
+       C.Cast (reduceaux context l te, reduceaux context l ty)
     | C.Prod (name,s,t) ->
        assert (l = []) ;
-       C.Prod (name, reduceaux [] s, reduceaux [] t)
+       C.Prod (name,
+        reduceaux context [] s,
+        reduceaux ((Some (name,C.Decl s))::context) [] t)
     | C.Lambda (name,s,t) ->
        (match l with
-           [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
-         | he::tl -> reduceaux tl (S.subst he t)
+           [] ->
+            C.Lambda (name,
+             reduceaux context [] s,
+             reduceaux ((Some (name,C.Decl s))::context) [] t)
+         | he::tl -> reduceaux context tl (S.subst he t)
            (* when name is Anonimous the substitution should be superfluous *)
        )
-    | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
+    | C.LetIn (n,s,t) ->
+       reduceaux context l (S.subst (reduceaux context [] s) t)
     | C.Appl (he::tl) ->
-       let tl' = List.map (reduceaux []) tl in
-        reduceaux (tl'@l) he
+       let tl' = List.map (reduceaux context []) tl in
+        reduceaux context (tl'@l) he
     | C.Appl [] -> raise (Impossible 1)
     | C.Const (uri,cookingsno) as t ->
        (match CicEnvironment.get_cooked_obj uri cookingsno with
-           C.Definition (_,body,_,_) -> reduceaux l body
+           C.Definition (_,body,_,_) -> reduceaux context l body
          | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
          | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_) -> reduceaux l body
+         | C.CurrentProof (_,_,body,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
        let decofix =
         function
            C.CoFix (i,fl) as t ->
-            let (_,_,body) = List.nth fl i in
-             let body' =
-              let counter = ref (List.length fl) in
-               List.fold_right
-                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                fl
-                body
-             in
-              reduceaux [] body'
+            let tys =
+             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+            in
+             let (_,_,body) = List.nth fl i in
+              let body' =
+               let counter = ref (List.length fl) in
+                List.fold_right
+                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+                 fl
+                 body
+              in
+               reduceaux (tys@context) [] body'
          | C.Appl (C.CoFix (i,fl) :: tl) ->
-            let (_,_,body) = List.nth fl i in
-             let body' =
-              let counter = ref (List.length fl) in
-               List.fold_right
-                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                fl
-                body
-             in
-              let tl' = List.map (reduceaux []) tl in
-               reduceaux tl body'
+            let tys =
+             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+            in
+             let (_,_,body) = List.nth fl i in
+              let body' =
+               let counter = ref (List.length fl) in
+                List.fold_right
+                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+                 fl
+                 body
+              in
+               let tl' = List.map (reduceaux context []) tl in
+                reduceaux (tys@context) tl' body'
          | t -> t
        in
-        (match decofix (reduceaux [] term) with
-            C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
+        (match decofix (reduceaux context [] term) with
+            C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
              let (arity, r, num_ingredients) =
               match CicEnvironment.get_obj mutind with
@@ -183,74 +332,76 @@ let reduce =
                 in
                  eat_first (num_to_eat,tl)
               in
-               reduceaux (ts@l) (List.nth pl (j-1))
-         | C.Abst _ | C.Cast _ | C.Implicit ->
+               reduceaux context (ts@l) (List.nth pl (j-1))
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
-           let outtype' = reduceaux [] outtype in
-           let term' = reduceaux [] term in
-           let pl' = List.map (reduceaux []) pl in
+           let outtype' = reduceaux context [] outtype in
+           let term' = reduceaux context [] term in
+           let pl' = List.map (reduceaux context []) pl in
             let res =
              C.MutCase (mutind,cookingsno,i,outtype',term',pl')
             in
              if l = [] then res else C.Appl (res::l)
        )
     | C.Fix (i,fl) ->
-       let t' () =
-        let fl' =
-         List.map
-          (function (n,recindex,ty,bo) ->
-            (n,recindex,reduceaux [] ty, reduceaux [] bo)
-          ) fl
-        in
-         C.Fix (i, fl')
+       let tys =
+        List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
        in
-        let (_,recindex,_,body) = List.nth fl i in
-         let recparam =
-          try
-           Some (List.nth l recindex)
-          with
-           _ -> None
+        let t' () =
+         let fl' =
+          List.map
+           (function (n,recindex,ty,bo) ->
+             (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+           ) fl
          in
-          (match recparam with
-              Some recparam ->
-               (match reduceaux [] recparam with
-                   C.MutConstruct _
-                 | C.Appl ((C.MutConstruct _)::_) ->
-                    let body' =
-                     let counter = ref (List.length fl) in
-                      List.fold_right
-                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
-                       fl
-                       body
-                    in
-                     (* Possible optimization: substituting whd recparam in l *)
-                     reduceaux l body'
-                 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
-               )
-            | None -> if l = [] then t' () else C.Appl ((t' ())::l)
-          )
-    | C.CoFix (i,fl) ->
-       let t' =
-        let fl' =
-         List.map
-          (function (n,ty,bo) ->
-            (n,reduceaux [] ty, reduceaux [] bo)
-          ) fl
+          C.Fix (i, fl')
         in
-         C.CoFix (i, fl')
+         let (_,recindex,_,body) = List.nth fl i in
+          let recparam =
+           try
+            Some (List.nth l recindex)
+           with
+            _ -> None
+          in
+           (match recparam with
+               Some recparam ->
+                (match reduceaux context [] recparam with
+                    C.MutConstruct _
+                  | C.Appl ((C.MutConstruct _)::_) ->
+                     let body' =
+                      let counter = ref (List.length fl) in
+                       List.fold_right
+                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+                        fl
+                        body
+                     in
+                      (* Possible optimization: substituting whd recparam in l*)
+                      reduceaux context l body'
+                  | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
+                )
+             | None -> if l = [] then t' () else C.Appl ((t' ())::l)
+           )
+    | C.CoFix (i,fl) ->
+       let tys =
+        List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
        in
-        if l = [] then t' else C.Appl (t'::l)
+        let t' =
+         let fl' =
+          List.map
+           (function (n,ty,bo) ->
+             (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+           ) fl
+         in
+          C.CoFix (i, fl')
+        in
+         if l = [] then t' else C.Appl (t'::l)
  in
-function t -> let res =
-prerr_endline ("<<<<<<<<<<<<<<<<" ^ CicPp.ppterm t) ; flush stderr ;
-  reduceaux []
-t in prerr_endline ("++++++++++++++++++" ^ CicPp.ppterm res) ; flush stderr ; res
+  reduceaux context []
 ;;
 
 exception WrongShape;;
 exception AlreadySimplified;;
-exception WhatShouldIDo;;
 
 (*CSC: I fear it is still weaker than Coq's one. For example, Coq is *)
 (*CSCS: able to simpl (foo (S n) (S n)) to (foo (S O) n) where       *)
@@ -273,15 +424,20 @@ exception WhatShouldIDo;;
 (*     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 =
+let simpl context =
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (*reduce, but for the const case.                             *) 
  (**** Step 1 ****)
- let rec reduceaux l =
+ let rec reduceaux context l =
   let module C = Cic in
   let module S = CicSubstitution in
    function
-      C.Rel _ as t -> if l = [] then t else C.Appl (t::l)
+      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) -> reduceaux context l (S.lift n bo)
+	 | None -> raise RelToHiddenHypothesis
+       )
     | C.Var uri as t ->
        (match CicEnvironment.get_cooked_obj uri 0 with
            C.Definition _ -> raise ReferenceToDefinition
@@ -289,25 +445,32 @@ let simpl =
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
          | C.Variable (_,None,_) -> if l = [] then t else C.Appl (t::l)
-         | C.Variable (_,Some body,_) -> reduceaux l body
+         | C.Variable (_,Some body,_) -> reduceaux context l body
        )
     | C.Meta _ as t -> if l = [] then t else C.Appl (t::l)
     | C.Sort _ as t -> t (* l should be empty *)
     | C.Implicit as t -> t
-    | C.Cast (te,ty) -> reduceaux l te  (*CSC E' GIUSTO BUTTARE IL CAST? *)
+    | C.Cast (te,ty) ->
+       C.Cast (reduceaux context l te, reduceaux context l ty)
     | C.Prod (name,s,t) ->
        assert (l = []) ;
-       C.Prod (name, reduceaux [] s, reduceaux [] t)
+       C.Prod (name,
+        reduceaux context [] s,
+        reduceaux ((Some (name,C.Decl s))::context) [] t)
     | C.Lambda (name,s,t) ->
        (match l with
-           [] -> C.Lambda (name, reduceaux [] s, reduceaux [] t)
-         | he::tl -> reduceaux tl (S.subst he t)
+           [] ->
+            C.Lambda (name,
+             reduceaux context [] s,
+             reduceaux ((Some (name,C.Decl s))::context) [] t)
+         | he::tl -> reduceaux context tl (S.subst he t)
            (* when name is Anonimous the substitution should be superfluous *)
        )
-    | C.LetIn (n,s,t) -> reduceaux l (S.subst (reduceaux [] s) t)
+    | C.LetIn (n,s,t) ->
+       reduceaux context l (S.subst (reduceaux context [] s) t)
     | C.Appl (he::tl) ->
-       let tl' = List.map (reduceaux []) tl in
-        reduceaux (tl'@l) he
+       let tl' = List.map (reduceaux context []) tl in
+        reduceaux context (tl'@l) he
     | C.Appl [] -> raise (Impossible 1)
     | C.Const (uri,cookingsno) as t ->
        (match CicEnvironment.get_cooked_obj uri cookingsno with
@@ -327,30 +490,36 @@ let simpl =
                          (* superfluous                                       *)
                          aux (he::rev_constant_args) tl (S.subst he t)
                     end
-                 | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
+                 | C.LetIn (_,s,t) ->
+                    aux rev_constant_args l (S.subst s t)
                  | C.Fix (i,fl) as t ->
-                    let (_,recindex,_,body) = List.nth fl i in
-                     let recparam =
-                      try
-                       List.nth l recindex
-                      with
-                       _ -> raise AlreadySimplified
-                     in
-                      (match CicReduction.whd recparam with
-                          C.MutConstruct _
-                        | C.Appl ((C.MutConstruct _)::_) ->
-                           let body' =
-                            let counter = ref (List.length fl) in
-                             List.fold_right
-                              (function _ ->
-                                decr counter ; S.subst (C.Fix (!counter,fl))
-                              ) fl body
-                           in
-                            (* Possible optimization: substituting whd *)
-                            (* recparam in l                           *)
-                            reduceaux l body', List.rev rev_constant_args
-                        | _ -> raise AlreadySimplified
-                      )
+                    let tys =
+                     List.map (function (name,_,ty,_) ->
+                      Some (C.Name name, C.Decl ty)) fl
+                    in
+                     let (_,recindex,_,body) = List.nth fl i in
+                      let recparam =
+                       try
+                        List.nth l recindex
+                       with
+                        _ -> raise AlreadySimplified
+                      in
+                       (match CicReduction.whd context recparam with
+                           C.MutConstruct _
+                         | C.Appl ((C.MutConstruct _)::_) ->
+                            let body' =
+                             let counter = ref (List.length fl) in
+                              List.fold_right
+                               (function _ ->
+                                 decr counter ; S.subst (C.Fix (!counter,fl))
+                               ) fl body
+                            in
+                             (* Possible optimization: substituting whd *)
+                             (* recparam in l                           *)
+                             reduceaux (tys@context) l body',
+                              List.rev rev_constant_args
+                         | _ -> raise AlreadySimplified
+                       )
                  | _ -> raise WrongShape
                in
                 aux [] l body
@@ -361,15 +530,13 @@ let simpl =
                    [] -> C.Const (uri,cookingsno)
                  | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
                in
-                let reduced_term_to_fold = reduce term_to_fold in
-prerr_endline ("TERM TO FOLD: " ^ CicPp.ppterm term_to_fold) ; flush stderr ;
-prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; flush stderr ;
-                 replace reduced_term_to_fold term_to_fold res
+                let reduced_term_to_fold = reduce context term_to_fold in
+                 replace (=) reduced_term_to_fold term_to_fold res
              with
                 WrongShape ->
                  (* The constant does not unfold to a Fix lambda-abstracted   *)
                  (* w.r.t. zero or more variables. We just perform reduction. *)
-                 reduceaux l body
+                 reduceaux context l body
               | AlreadySimplified ->
                  (* If we performed delta-reduction, we would find a Fix   *)
                  (* not applied to a constructor. So, we refuse to perform *)
@@ -381,40 +548,43 @@ prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; f
             end
          | C.Axiom _ -> if l = [] then t else C.Appl (t::l)
          | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_) -> reduceaux l body
+         | C.CurrentProof (_,_,body,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutCase (mutind,cookingsno,i,outtype,term,pl) ->
        let decofix =
         function
            C.CoFix (i,fl) as t ->
-            let (_,_,body) = List.nth fl i in
-             let body' =
-              let counter = ref (List.length fl) in
-               List.fold_right
-                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                fl
-                body
-             in
-              reduceaux [] body'
+            let tys =
+             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
+             let (_,_,body) = List.nth fl i in
+              let body' =
+               let counter = ref (List.length fl) in
+                List.fold_right
+                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+                 fl
+                 body
+              in
+               reduceaux (tys@context) [] body'
          | C.Appl (C.CoFix (i,fl) :: tl) ->
-            let (_,_,body) = List.nth fl i in
-             let body' =
-              let counter = ref (List.length fl) in
-               List.fold_right
-                (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
-                fl
-                body
-             in
-              let tl' = List.map (reduceaux []) tl in
-               reduceaux tl body'
+            let tys =
+             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
+             let (_,_,body) = List.nth fl i in
+              let body' =
+               let counter = ref (List.length fl) in
+                List.fold_right
+                 (fun _ -> decr counter ; S.subst (C.CoFix (!counter,fl)))
+                 fl
+                 body
+              in
+               let tl' = List.map (reduceaux context []) tl in
+                reduceaux (tys@context) tl body'
          | t -> t
        in
-        (match decofix (reduceaux [] term) with
-            C.MutConstruct (_,_,_,j) -> reduceaux l (List.nth pl (j-1))
+        (match decofix (reduceaux context [] term) with
+            C.MutConstruct (_,_,_,j) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,_,j) :: tl) ->
              let (arity, r, num_ingredients) =
               match CicEnvironment.get_obj mutind with
@@ -439,64 +609,70 @@ prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; f
                 in
                  eat_first (num_to_eat,tl)
               in
-               reduceaux (ts@l) (List.nth pl (j-1))
-         | C.Abst _ | C.Cast _ | C.Implicit ->
+               reduceaux context (ts@l) (List.nth pl (j-1))
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ ->
-           let outtype' = reduceaux [] outtype in
-           let term' = reduceaux [] term in
-           let pl' = List.map (reduceaux []) pl in
+           let outtype' = reduceaux context [] outtype in
+           let term' = reduceaux context [] term in
+           let pl' = List.map (reduceaux context []) pl in
             let res =
              C.MutCase (mutind,cookingsno,i,outtype',term',pl')
             in
              if l = [] then res else C.Appl (res::l)
        )
     | C.Fix (i,fl) ->
-       let t' () =
-        let fl' =
-         List.map
-          (function (n,recindex,ty,bo) ->
-            (n,recindex,reduceaux [] ty, reduceaux [] bo)
-          ) fl
-        in
-         C.Fix (i, fl')
+       let tys =
+        List.map (function (name,_,ty,_) -> Some (C.Name name, C.Decl ty)) fl
        in
-        let (_,recindex,_,body) = List.nth fl i in
-         let recparam =
-          try
-           Some (List.nth l recindex)
-          with
-           _ -> None
+        let t' () =
+         let fl' =
+          List.map
+           (function (n,recindex,ty,bo) ->
+             (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+           ) fl
          in
-          (match recparam with
-              Some recparam ->
-               (match reduceaux [] recparam with
-                   C.MutConstruct _
-                 | C.Appl ((C.MutConstruct _)::_) ->
-                    let body' =
-                     let counter = ref (List.length fl) in
-                      List.fold_right
-                       (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
-                       fl
-                       body
-                    in
-                     (* Possible optimization: substituting whd recparam in l *)
-                     reduceaux l body'
-                 | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
-               )
-            | None -> if l = [] then t' () else C.Appl ((t' ())::l)
-          )
-    | C.CoFix (i,fl) ->
-       let t' =
-        let fl' =
-         List.map
-          (function (n,ty,bo) ->
-            (n,reduceaux [] ty, reduceaux [] bo)
-          ) fl
+          C.Fix (i, fl')
         in
+         let (_,recindex,_,body) = List.nth fl i in
+          let recparam =
+           try
+            Some (List.nth l recindex)
+           with
+            _ -> None
+          in
+           (match recparam with
+               Some recparam ->
+                (match reduceaux context [] recparam with
+                    C.MutConstruct _
+                  | C.Appl ((C.MutConstruct _)::_) ->
+                     let body' =
+                      let counter = ref (List.length fl) in
+                       List.fold_right
+                        (fun _ -> decr counter ; S.subst (C.Fix (!counter,fl)))
+                        fl
+                        body
+                     in
+                      (* Possible optimization: substituting whd recparam in l*)
+                      reduceaux context l body'
+                  | _ -> if l = [] then t' () else C.Appl ((t' ())::l)
+                )
+             | None -> if l = [] then t' () else C.Appl ((t' ())::l)
+           )
+    | C.CoFix (i,fl) ->
+       let tys =
+        List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
+       in
+        let t' =
+         let fl' =
+          List.map
+           (function (n,ty,bo) ->
+             (n,reduceaux context [] ty, reduceaux (tys@context) [] bo)
+           ) fl
+         in
          C.CoFix (i, fl')
        in
-        if l = [] then t' else C.Appl (t'::l)
+         if l = [] then t' else C.Appl (t'::l)
  in
-  reduceaux []
+  reduceaux context []
 ;;