X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=4fc192a5b261f48be145c3e21cc7268c14a47055;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=f5c82a9fe7da0be3f2702d90c5733a99cc3c6f4d;hpb=6531c263da005e25ea2f58f9ee960acba7857ff6;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index f5c82a9fe..4fc192a5b 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -30,40 +30,56 @@ open ProofEngineTypes
 let reduction_tac ~reduction ~pattern (proof,goal) =
   let curi,metasenv,pbo,pty = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
-  let change subst where terms =
-   if terms = [] then where
+  let change subst where terms metasenv ugraph =
+   if terms = [] then where, metasenv, ugraph
    else
-    let terms, terms' = 
-      List.split (List.map (fun (context, t) -> t, reduction context t) terms)
-    in
-    let where' =
-     ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
-      ~where:where
-    in
-     CicMetaSubst.apply_subst subst where' in
+     let pairs, metasenv, ugraph =
+       List.fold_left
+        (fun (pairs, metasenv, ugraph) (context, t) ->
+          let reduction, metasenv, ugraph = reduction context metasenv ugraph in
+          ((t, reduction context t) :: pairs), metasenv, ugraph)
+        ([], metasenv, ugraph)
+        terms
+     in
+     let terms, terms' = List.split pairs in
+     let where' =
+       ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+        ~where:where
+     in
+     CicMetaSubst.apply_subst subst where', metasenv, ugraph
+  in
   let (subst,metasenv,ugraph,selected_context,selected_ty) =
-   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
-    ~conjecture ~pattern in
-  let ty' = change subst ty selected_ty in
-  let context' =
+    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+      ~conjecture ~pattern
+  in
+  let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
+  let context', metasenv, ugraph =
    List.fold_right2
-    (fun entry selected_entry context' ->
+    (fun entry selected_entry (context', metasenv, ugraph) ->
       match entry,selected_entry with
-         None,None -> None::context'
+         None,None -> None::context', metasenv, ugraph
        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
-          let ty' = change subst ty selected_ty in
-           Some (name,Cic.Decl ty')::context'
+          let ty', metasenv, ugraph =
+            change subst ty selected_ty metasenv ugraph
+          in
+          Some (name,Cic.Decl ty')::context', metasenv, ugraph
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
-          let bo' = change subst bo selected_bo in
-          let ty' =
+          let bo', metasenv, ugraph =
+            change subst bo selected_bo metasenv ugraph
+          in
+          let ty', metasenv, ugraph =
            match ty,selected_ty with
-              None,None -> None
-            | Some ty,Some selected_ty -> Some (change subst ty selected_ty)
+              None,None -> None, metasenv, ugraph
+            | Some ty,Some selected_ty ->
+                let ty', metasenv, ugraph =
+                  change subst ty selected_ty metasenv ugraph
+                in
+                Some ty', metasenv, ugraph
             | _,_ -> assert false
           in
-           Some (name,Cic.Def (bo',ty'))::context'
+           (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
        | _,_ -> assert false
-    ) context selected_context [] in
+    ) context selected_context ([], metasenv, ugraph) in
   let metasenv' = 
     List.map (function 
       | (n,_,_) when n = metano -> (metano,context',ty')
@@ -74,20 +90,31 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
 ;;
 
 let simpl_tac ~pattern =
- mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
+ mk_tactic (reduction_tac
+  ~reduction:(const_lazy_reduction ProofEngineReduction.simpl) ~pattern)
 
 let reduce_tac ~pattern =
- mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
+ mk_tactic (reduction_tac
+  ~reduction:(const_lazy_reduction ProofEngineReduction.reduce) ~pattern)
 
 let unfold_tac what ~pattern =
- mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
-  ~pattern);;
+  let reduction =
+    match what with
+    | None -> const_lazy_reduction (ProofEngineReduction.unfold ?what:None)
+    | Some lazy_term ->
+        (fun context metasenv ugraph ->
+          let what, metasenv, ugraph = lazy_term context metasenv ugraph in
+          ProofEngineReduction.unfold ~what, metasenv, ugraph)
+  in
+  mk_tactic (reduction_tac ~reduction ~pattern)
   
 let whd_tac ~pattern =
- mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
+ mk_tactic (reduction_tac
+  ~reduction:(const_lazy_reduction CicReduction.whd) ~pattern)
 
 let normalize_tac ~pattern =
- mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);;
+ mk_tactic (reduction_tac
+  ~reduction:(const_lazy_reduction CicReduction.normalize) ~pattern)
 
 exception NotConvertible
 
@@ -104,80 +131,73 @@ let change_tac ~pattern with_what  =
  let change_tac ~pattern ~with_what (proof, goal) =
   let curi,metasenv,pbo,pty = proof in
   let (metano,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in
-  let context_len = List.length context in
-  let change subst context'_len where terms =
-   if terms = [] then where
+  let change subst where terms metasenv ugraph =
+   if terms = [] then where, metasenv, ugraph
    else
-    let terms, terms' = 
-      List.split
-       (List.map
-        (fun (context_of_t, t) ->
-          let context_of_t_len = List.length context_of_t in
-          let with_what_in_context' =
-            if context_len > context'_len then
-             begin
-              let with_what,subst,metasenv' =
-               CicMetaSubst.delift_rels [] metasenv
-                (context_len - context'_len) with_what
-              in
-               assert (subst = []);
-               assert (metasenv = metasenv');
-               with_what
-             end
-            else
-             with_what in
-          let with_what_in_context_of_t =
-           if context_of_t_len > context'_len then
-            CicSubstitution.lift (context_of_t_len - context'_len)
-             with_what_in_context'
-           else
-            with_what in
+    let pairs, metasenv, ugraph =
+      List.fold_left
+        (fun (pairs, metasenv, ugraph) (context_of_t, t) ->
+          let with_what, metasenv, ugraph =
+            with_what context_of_t metasenv ugraph
+          in
           let _,u =
-           CicTypeChecker.type_of_aux' metasenv context_of_t with_what
-            CicUniv.empty_ugraph in
+            CicTypeChecker.type_of_aux' metasenv context_of_t with_what ugraph
+          in
           let b,_ =
-           CicReduction.are_convertible ~metasenv context_of_t t with_what u in
+           CicReduction.are_convertible ~metasenv context_of_t t with_what u
+          in
           if b then
-           t, with_what_in_context_of_t
+           ((t, with_what) :: pairs), metasenv, ugraph
           else
-           raise NotConvertible) terms)
+           raise NotConvertible)
+        ([], metasenv, ugraph)
+        terms
     in
+    let terms, terms' = List.split pairs in
      let where' =
       ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
        ~where:where
      in
-      CicMetaSubst.apply_subst subst where' in
+      CicMetaSubst.apply_subst subst where', metasenv, ugraph
+  in
   let (subst,metasenv,ugraph,selected_context,selected_ty) =
    ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph ~conjecture
     ~pattern in
-  let ty' = change subst context_len ty selected_ty in
-  let context' =
+  let ty', metasenv, ugraph = change subst ty selected_ty metasenv ugraph in
+  let context', metasenv, ugraph =
    List.fold_right2
-    (fun entry selected_entry context' ->
-     let context'_len = List.length context' in
+    (fun entry selected_entry (context', metasenv, ugraph) ->
      match entry,selected_entry with
-         None,None -> None::context'
+         None,None -> (None::context'), metasenv, ugraph
        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
-          let ty' = change subst context'_len ty selected_ty in
-           Some (name,Cic.Decl ty')::context'
+          let ty', metasenv, ugraph =
+            change subst ty selected_ty metasenv ugraph
+          in
+           (Some (name,Cic.Decl ty')::context'), metasenv, ugraph
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
-          let bo' = change subst context'_len bo selected_bo in
-          let ty' =
+          let bo', metasenv, ugraph =
+            change subst bo selected_bo metasenv ugraph
+          in
+          let ty', metasenv, ugraph =
            match ty,selected_ty with
-              None,None -> None
+              None,None -> None, metasenv, ugraph
             | Some ty,Some selected_ty ->
-               Some (change subst context'_len ty selected_ty)
+                let ty', metasenv, ugraph =
+                  change subst ty selected_ty metasenv ugraph
+                in
+                Some ty', metasenv, ugraph
             | _,_ -> assert false
           in
-           Some (name,Cic.Def (bo',ty'))::context'
+           (Some (name,Cic.Def (bo',ty'))::context'), metasenv, ugraph
        | _,_ -> assert false
-    ) context selected_context [] in
- let metasenv' = 
-   List.map (function 
-     | (n,_,_) when n = metano -> (metano,context',ty')
-     | _ as t -> t
-   ) metasenv
- in
+    ) context selected_context ([], metasenv, ugraph) in
+  let metasenv' = 
+    List.map
+      (function 
+        | (n,_,_) when n = metano -> (metano,context',ty')
+        | _ as t -> t)
+      metasenv
+  in
   (curi,metasenv',pbo,pty), [metano]
   in
     mk_tactic (change_tac ~pattern ~with_what)
@@ -185,12 +205,14 @@ let change_tac ~pattern with_what  =
 let fold_tac ~reduction ~term ~pattern =
  let fold_tac ~reduction ~term ~pattern:(wanted,hyps_pat,concl_pat) status =
   assert (wanted = None); (* this should be checked syntactically *)
-  let proof,goal = status in
-  let _,metasenv,_,_ = proof in
-  let _,context,_ = CicUtil.lookup_meta goal metasenv in
-  let reduced_term = reduction context term in
+  let reduced_term =
+    (fun context metasenv ugraph ->
+      let term, metasenv, ugraph = term context metasenv ugraph in
+      let reduction, metasenv, ugraph = reduction context metasenv ugraph in
+      reduction context term, metasenv, ugraph)
+  in
    apply_tactic
     (change_tac ~pattern:(Some reduced_term,hyps_pat,concl_pat) term) status
  in
   mk_tactic (fold_tac ~reduction ~term ~pattern)
-;;
+