X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=0dc4ce4ee3e617a1b1cb6a98efa6dc68db8e922b;hb=6355ac16ff3996e16d9d9cfb08e4184bc7962f8b;hp=62c2adab57e2e9f34e04c7ca1fff6c50fa9d828b;hpb=5538a4548601ba1c1647ec9dc0fbbd875e5a93fd;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 62c2adab5..0dc4ce4ee 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -33,6 +33,7 @@
 (*                                                                            *)
 (******************************************************************************)
 
+(* $Id$ *)
 
 (* The code of this module is derived from the code of CicReduction *)
 
@@ -206,7 +207,7 @@ let replace_lifting ~equality ~what ~with_what ~where =
         List.map (function (uri,t) -> uri,substaux k what t) exp_named_subst
        in
         C.Var (uri,exp_named_subst')
-    | C.Meta (i, l) as t -> 
+    | C.Meta (i, l) -> 
        let l' =
         List.map
          (function
@@ -298,14 +299,14 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
     S.lift (k-1) (find_image t)
    with Not_found ->
     match t with
-       C.Rel n as t ->
+       C.Rel n ->
         if n < k then C.Rel n else C.Rel (n + nnn)
      | C.Var (uri,exp_named_subst) ->
         let exp_named_subst' =
          List.map (function (uri,t) -> uri,substaux k t) exp_named_subst
         in
          C.Var (uri,exp_named_subst')
-     | C.Meta (i, l) as t -> 
+     | C.Meta (i, l) -> 
         let l' =
          List.map
           (function
@@ -450,7 +451,7 @@ let reduce context =
        in
         let t' = C.MutInd (uri,i,exp_named_subst') in
          if l = [] then t' else C.Appl (t'::l)
-    | C.MutConstruct (uri,i,j,exp_named_subst) as t ->
+    | C.MutConstruct (uri,i,j,exp_named_subst) ->
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
@@ -459,10 +460,7 @@ let reduce context =
     | C.MutCase (mutind,i,outtype,term,pl) ->
        let decofix =
         function
-           C.CoFix (i,fl) as t ->
-            let tys =
-             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl
-            in
+           C.CoFix (i,fl) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -473,9 +471,6 @@ let reduce context =
               in
                reduceaux context [] body'
          | C.Appl (C.CoFix (i,fl) :: tl) ->
-            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
@@ -600,14 +595,6 @@ exception AlreadySimplified;;
 (*CSC: It does not perform simplification in a Case *)
 
 let simpl context =
- let mk_appl t l =
-   if l = [] then 
-     t 
-   else 
-     match t with
-     | Cic.Appl l' -> Cic.Appl (l'@l)
-     | _ -> Cic.Appl (t::l)
- in
  (* reduceaux is equal to the reduceaux locally defined inside *)
  (* reduce, but for the const case.                            *) 
  (**** Step 1 ****)
@@ -616,14 +603,8 @@ let simpl context =
   let module S = CicSubstitution in
    function
       C.Rel n as t ->
-       (try
-         match List.nth context (n-1) with
-            Some (_,C.Decl _) -> if l = [] then t else C.Appl (t::l)
-          | Some (_,C.Def (bo,_)) ->
-             try_delta_expansion context l t (S.lift n bo)
-	  | None -> raise RelToHiddenHypothesis
-        with
-         Failure _ -> assert false)
+       (* we never perform delta expansion automatically *)
+       if l = [] then t else C.Appl (t::l)
     | C.Var (uri,exp_named_subst) ->
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
@@ -644,7 +625,7 @@ let simpl context =
     | C.Sort _ as t -> t (* l should be empty *)
     | C.Implicit _ as t -> t
     | C.Cast (te,ty) ->
-       C.Cast (reduceaux context l te, reduceaux context l ty)
+       C.Cast (reduceaux context l te, reduceaux context [] ty)
     | C.Prod (name,s,t) ->
        assert (l = []) ;
        C.Prod (name,
@@ -697,9 +678,7 @@ let simpl context =
     | C.MutCase (mutind,i,outtype,term,pl) ->
        let decofix =
         function
-           C.CoFix (i,fl) as t ->
-            let tys =
-             List.map (function (name,ty,_) -> Some (C.Name name, C.Decl ty)) fl            in
+           C.CoFix (i,fl) ->
              let (_,_,body) = List.nth fl i in
               let body' =
                let counter = ref (List.length fl) in
@@ -710,18 +689,16 @@ let simpl context =
               in
                reduceaux context [] body'
          | C.Appl (C.CoFix (i,fl) :: tl) ->
-            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 context tl body'
+             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 context tl' body'
          | t -> t
        in
         (match decofix (CicReduction.whd context term) with
@@ -818,7 +795,7 @@ let simpl context =
     let res,constant_args =
      let rec aux rev_constant_args l =
       function
-         C.Lambda (name,s,t) as t' ->
+         C.Lambda (name,s,t) ->
           begin
            match l with
               [] -> raise WrongShape
@@ -829,11 +806,7 @@ let simpl context =
           end
        | C.LetIn (_,s,t) ->
           aux rev_constant_args l (S.subst s t)
-       | C.Fix (i,fl) as t ->
-          let tys =
-           List.map (function (name,_,ty,_) ->
-            Some (C.Name name, C.Decl ty)) fl
-          in
+       | C.Fix (i,fl) ->
            let (_,recindex,_,body) = List.nth fl i in
             let recparam =
              try