X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2FgTopLevel%2FproofEngineReduction.ml;h=7d4a799601dad71082943a92b5685480996b60da;hb=ee35bf33520d92753899985329cc4bfee141b808;hp=94e5b353de3534df42cba3016327de56abffdd6c;hpb=06e9498bf967323fe12d6383ec7b279a4546a06c;p=helm.git

diff --git a/helm/gTopLevel/proofEngineReduction.ml b/helm/gTopLevel/proofEngineReduction.ml
index 94e5b353d..7d4a79960 100644
--- a/helm/gTopLevel/proofEngineReduction.ml
+++ b/helm/gTopLevel/proofEngineReduction.ml
@@ -43,13 +43,14 @@ exception ReferenceToVariable;;
 exception ReferenceToCurrentProof;;
 exception ReferenceToInductiveDefinition;;
 exception WrongUriToInductiveDefinition;;
+exception RelToHiddenHypothesis;;
 
 (* "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
@@ -92,11 +93,16 @@ let replace ~what ~with_what ~where =
 (* Takes a well-typed term and fully reduces it. *)
 (*CSC: It does not perform reduction in a Case *)
 let reduce context =
- 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
@@ -104,32 +110,39 @@ let reduce context =
          | 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 ????? *)
@@ -139,30 +152,36 @@ let reduce context =
        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
@@ -187,66 +206,72 @@ let reduce context =
                 in
                  eat_first (num_to_eat,tl)
               in
-               reduceaux (ts@l) (List.nth pl (j-1))
+               reduceaux context (ts@l) (List.nth pl (j-1))
          | C.Abst _ | 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
-  reduceaux []
+  reduceaux context []
 ;;
 
 exception WrongShape;;
@@ -278,11 +303,16 @@ 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
@@ -290,25 +320,32 @@ let simpl context =
          | 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
@@ -330,28 +367,33 @@ let simpl context =
                     end
                  | C.LetIn (_,_,_) -> raise WhatShouldIDo (*CSC: ?????????? *)
                  | 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 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 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
@@ -363,14 +405,12 @@ let simpl context =
                  | _ -> C.Appl ((C.Const (uri,cookingsno))::constant_args)
                in
                 let reduced_term_to_fold = reduce context 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
+                 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 *)
@@ -382,7 +422,7 @@ 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 ????? *)
@@ -392,30 +432,34 @@ prerr_endline ("REDUCED TERM TO FOLD: " ^ CicPp.ppterm reduced_term_to_fold) ; f
        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
@@ -440,64 +484,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))
+               reduceaux context (ts@l) (List.nth pl (j-1))
          | C.Abst _ | 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 []
 ;;