X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FproofEngineReduction.ml;h=d5dbf9f35b51760559b50e78328dcaf9daa06595;hb=4ccc7ef7fe3d43fb0f882768d2818a54e24c8857;hp=016a7ba994fbe54593e68ac96647981ce0505b4e;hpb=d8e0b34863a7359fb54fdbf9d747d7b624713130;p=helm.git

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 016a7ba99..d5dbf9f35 100644
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/components/tactics/proofEngineReduction.ml
@@ -86,7 +86,7 @@ let replace ~equality ~what ~with_what ~where =
      | C.Cast (te,ty) -> C.Cast (aux te, aux ty)
      | 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.LetIn (n,s,ty,t) -> C.LetIn (n, aux s, aux ty, aux t)
      | C.Appl l ->
         (* Invariant enforced: no application of an application *)
         (match List.map aux l with
@@ -139,7 +139,7 @@ let replace_lifting ~equality ~context ~what ~with_what ~where =
     find_image_aux (what,with_what)
   in
   let add_ctx ctx n s = (Some (n, Cic.Decl s))::ctx in
-  let add_ctx1 ctx n s = (Some (n, Cic.Def (s,None)))::ctx in
+  let add_ctx1 ctx n s ty = (Some (n, Cic.Def (s,ty)))::ctx in
   let rec substaux k ctx what t =
    try
     S.lift (k-1) (find_image ctx what t)
@@ -169,9 +169,9 @@ let replace_lifting ~equality ~context ~what ~with_what ~where =
     | C.Lambda (n,s,t) ->
        C.Lambda
         (n, substaux k ctx what s, substaux (k + 1) (add_ctx ctx n s) (List.map (S.lift 1) what) t)
-    | C.LetIn (n,s,t) ->
+    | C.LetIn (n,s,ty,t) ->
        C.LetIn
-        (n, substaux k ctx what s, substaux (k + 1) (add_ctx1 ctx n s) (List.map (S.lift 1) what) t)
+        (n, substaux k ctx what s, substaux k ctx what ty, substaux (k + 1) (add_ctx1 ctx n s ty) (List.map (S.lift 1) what) t)
     | C.Appl (he::tl) ->
        (* Invariant: no Appl applied to another Appl *)
        let tl' = List.map (substaux k ctx what) tl in
@@ -268,8 +268,8 @@ let replace_lifting_csc nnn ~equality ~what ~with_what ~where =
         C.Prod (n, substaux k s, substaux (k + 1) t)
      | C.Lambda (n,s,t) ->
         C.Lambda (n, substaux k s, substaux (k + 1) t)
-     | C.LetIn (n,s,t) ->
-        C.LetIn (n, substaux k s, substaux (k + 1) t)
+     | C.LetIn (n,s,ty,t) ->
+        C.LetIn (n, substaux k s, substaux k ty, substaux (k + 1) t)
      | C.Appl (he::tl) ->
         (* Invariant: no Appl applied to another Appl *)
         let tl' = List.map (substaux k) tl in
@@ -358,8 +358,8 @@ let replace_with_rel_1_from ~equality ~what =
         C.Prod (n, subst_term k v, subst_term (succ k) t)
      | C.Lambda (n, v, t) ->
         C.Lambda (n, subst_term k v, subst_term (succ k) t)
-     | C.LetIn (n, v, t) ->
-        C.LetIn (n, subst_term k v, subst_term (succ k) t)
+     | C.LetIn (n, v, ty, t) ->
+        C.LetIn (n, subst_term k v, subst_term k ty, subst_term (succ k) t)
      | C.Fix (i, fixes) ->
         let fixesno = List.length fixes in
         let fixes = List.map (subst_fix fixesno k) fixes in
@@ -379,216 +379,6 @@ let replace_with_rel_1_from ~equality ~what =
 in
 subst_term
    
-
-
-
-(* Takes a well-typed term and fully reduces it. *)
-(*CSC: It does not perform reduction in a Case *)
-let reduce context =
- let rec reduceaux context l =
-   function
-      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,exp_named_subst) ->
-       let exp_named_subst' =
-        reduceaux_exp_named_subst context l exp_named_subst
-       in
-       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-	 match o with
-           C.Constant _ -> raise ReferenceToConstant
-         | C.CurrentProof _ -> raise ReferenceToCurrentProof
-         | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_,_,_) ->
-            let t' = C.Var (uri,exp_named_subst') in
-             if l = [] then t' else C.Appl (t'::l)
-         | C.Variable (_,Some body,_,_,_) ->
-            (reduceaux context l
-              (CicSubstitution.subst_vars exp_named_subst' 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) ->
-       C.Cast (reduceaux context l te, reduceaux context l ty)
-    | C.Prod (name,s,t) ->
-       assert (l = []) ;
-       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 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 context l (S.subst (reduceaux context [] s) t)
-    | C.Appl (he::tl) ->
-       let tl' = List.map (reduceaux context []) tl in
-        reduceaux context (tl'@l) he
-    | C.Appl [] -> raise (Impossible 1)
-    | C.Const (uri,exp_named_subst) ->
-       let exp_named_subst' =
-        reduceaux_exp_named_subst context l exp_named_subst
-       in
-        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
-	  match o with
-            C.Constant (_,Some body,_,_,_) ->
-             (reduceaux context l
-               (CicSubstitution.subst_vars exp_named_subst' body))
-          | C.Constant (_,None,_,_,_) ->
-             let t' = C.Const (uri,exp_named_subst') in
-              if l = [] then t' else C.Appl (t'::l)
-          | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,body,_,_,_) ->
-             (reduceaux context l
-               (CicSubstitution.subst_vars exp_named_subst' body))
-          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-        )
-    | C.MutInd (uri,i,exp_named_subst) ->
-       let exp_named_subst' =
-        reduceaux_exp_named_subst context l exp_named_subst
-       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) ->
-       let exp_named_subst' =
-        reduceaux_exp_named_subst context l exp_named_subst
-       in
-        let t' = C.MutConstruct (uri,i,j,exp_named_subst') in
-         if l = [] then t' else C.Appl (t'::l)
-    | C.MutCase (mutind,i,outtype,term,pl) ->
-       let decofix =
-        function
-           C.CoFix (i,fl) ->
-             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 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 context []) tl in
-                reduceaux context tl' body'
-         | t -> t
-       in
-        (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) =
-	       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
-		 match o with
-                     C.InductiveDefinition (tl,_,r,_) ->
-                       let (_,_,arity,_) = List.nth tl i in
-			 (arity,r)
-		   | _ -> raise WrongUriToInductiveDefinition
-             in
-              let ts =
-               let rec eat_first =
-                function
-                   (0,l) -> l
-                 | (n,he::tl) when n > 0 -> eat_first (n - 1, tl)
-                 | _ -> raise (Impossible 5)
-               in
-                eat_first (r,tl)
-              in
-               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 context [] outtype in
-           let term' = reduceaux context [] term in
-           let pl' = List.map (reduceaux context []) pl in
-            let res =
-             C.MutCase (mutind,i,outtype',term',pl')
-            in
-             if l = [] then res else C.Appl (res::l)
-       )
-    | C.Fix (i,fl) ->
-       let tys,_ =
-        List.fold_left
-          (fun (types,len) (n,_,ty,_) ->
-             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-              len+1)
-         ) ([],0) fl 
-       in
-        let t' () =
-         let fl' =
-          List.map
-           (function (n,recindex,ty,bo) ->
-             (n,recindex,reduceaux context [] ty, reduceaux (tys@context) [] bo)
-           ) fl
-         in
-          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.fold_left
-          (fun (types,len) (n,ty,_) ->
-             (Some (C.Name n,(C.Decl (CicSubstitution.lift len ty)))::types,
-              len+1)
-         ) ([],0) 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)
- and reduceaux_exp_named_subst context l =
-  List.map (function uri,t -> uri,reduceaux context [] t)
- in
-  reduceaux context []
-;;
-
-
 let unfold ?what context where =
  let contextlen = List.length context in
  let first_is_the_expandable_head_of_second context' t1 t2 =
@@ -627,7 +417,7 @@ let unfold ?what context where =
       with
          Failure _ -> assert false)
   | Cic.Const (uri,exp_named_subst) as t ->
-     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+     let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
       (match o with
           Cic.Constant (_,Some body,_,_,_) ->
            CicReduction.head_beta_reduce
@@ -638,7 +428,7 @@ let unfold ?what context where =
         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
       )
   | Cic.Var (uri,exp_named_subst) as t ->
-     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+     let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
       (match o with
           Cic.Constant _ -> raise ReferenceToConstant
         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -722,7 +512,7 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 	  match o with
             C.Constant _ -> raise ReferenceToConstant
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -753,7 +543,7 @@ let simpl context =
          | he::tl -> reduceaux context tl (S.subst he t)
            (* when name is Anonimous the substitution should be superfluous *)
        )
-    | C.LetIn (n,s,t) ->
+    | C.LetIn (n,s,ty,t) ->
        reduceaux context l (S.subst (reduceaux context [] s) t)
     | C.Appl (he::tl) ->
        let tl' = List.map (reduceaux context []) tl in
@@ -763,7 +553,7 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
 	  match o with
            C.Constant (_,Some body,_,_,_) ->
             if List.exists is_active l then
@@ -822,7 +612,7 @@ let simpl context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-	       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
+	       let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph mutind in
 		 match o with
                      C.InductiveDefinition (tl,ingredients,r,_) ->
                        let (_,_,arity,_) = List.nth tl i in
@@ -936,7 +726,7 @@ let simpl context =
                (* be superfluous                                 *)
                aux (he::rev_constant_args) tl (S.subst he t)
           end
-       | C.LetIn (_,s,t) ->
+       | C.LetIn (_,s,_,t) ->
           aux rev_constant_args l (S.subst s t)
        | C.Fix (i,fl) ->
            let (_,recindex,_,body) = List.nth fl i in
@@ -1014,7 +804,7 @@ let simpl context =
                  (* when name is Anonimous the substitution should *)
                  (* be superfluous                                 *)
                  aux tl (S.subst he t))
-         | C.LetIn (_,s,t) -> aux l (S.subst s t)
+         | C.LetIn (_,s,_,t) -> aux l (S.subst s t)
          | Cic.Appl (Cic.Const (uri,_) :: args) as t when is_fix uri ->
              let recno =
                prerr_endline ("cerco : " ^ string_of_int (guess_recno uri)
@@ -1080,7 +870,7 @@ let simpl context =
                        prerr_endline (CicPp.ppterm t2 ^ "\n");
                        let subst1, _, _ = 
                          CicUnification.fo_unif metasenv ctx t1 t2
-                           CicUniv.empty_ugraph
+                           CicUniv.oblivion_ugraph
                        in
                        prerr_endline "UNIFICANO\n\n\n";
                        subst := subst1;