X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FreductionTactics.ml;h=f5c82a9fe7da0be3f2702d90c5733a99cc3c6f4d;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=d34678e52cf95e426c917df1205ec9dd27100b54;hpb=25ec5b95fe67bbdee888a8268b3772a394cd74a5;p=helm.git

diff --git a/helm/ocaml/tactics/reductionTactics.ml b/helm/ocaml/tactics/reductionTactics.ml
index d34678e52..f5c82a9fe 100644
--- a/helm/ocaml/tactics/reductionTactics.ml
+++ b/helm/ocaml/tactics/reductionTactics.ml
@@ -30,31 +30,35 @@ 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 where terms =
+  let change subst where terms =
    if terms = [] then where
    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
-  let (selected_context,selected_ty) =
-   ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
-  let ty' = change ty selected_ty in
+      ~where:where
+    in
+     CicMetaSubst.apply_subst subst where' 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' =
    List.fold_right2
     (fun entry selected_entry context' ->
       match entry,selected_entry with
          None,None -> None::context'
        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
-          let ty' = change ty selected_ty in
+          let ty' = change subst ty selected_ty in
            Some (name,Cic.Decl ty')::context'
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
-          let bo' = change bo selected_bo in
+          let bo' = change subst bo selected_bo in
           let ty' =
            match ty,selected_ty with
               None,None -> None
-            | Some ty,Some selected_ty -> Some (change ty selected_ty)
+            | Some ty,Some selected_ty -> Some (change subst ty selected_ty)
             | _,_ -> assert false
           in
            Some (name,Cic.Def (bo',ty'))::context'
@@ -69,16 +73,20 @@ let reduction_tac ~reduction ~pattern (proof,goal) =
   (curi,metasenv',pbo,pty), [metano]
 ;;
 
-let simpl_tac ~pattern = 
+let simpl_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.simpl ~pattern);;
 
-let reduce_tac ~pattern = 
+let reduce_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:ProofEngineReduction.reduce ~pattern);;
+
+let unfold_tac what ~pattern =
+ mk_tactic (reduction_tac ~reduction:(ProofEngineReduction.unfold ?what)
+  ~pattern);;
   
-let whd_tac ~pattern = 
+let whd_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:CicReduction.whd ~pattern);;
 
-let normalize_tac ~pattern = 
+let normalize_tac ~pattern =
  mk_tactic (reduction_tac ~reduction:CicReduction.normalize ~pattern);;
 
 exception NotConvertible
@@ -97,7 +105,7 @@ let change_tac ~pattern with_what  =
   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 context'_len where terms =
+  let change subst context'_len where terms =
    if terms = [] then where
    else
     let terms, terms' = 
@@ -134,11 +142,15 @@ let change_tac ~pattern with_what  =
           else
            raise NotConvertible) terms)
     in
-     ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
-      ~where:where in
-  let (selected_context,selected_ty) =
-   ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in
-  let ty' = change context_len ty selected_ty in
+     let where' =
+      ProofEngineReduction.replace ~equality:(==) ~what:terms ~with_what:terms'
+       ~where:where
+     in
+      CicMetaSubst.apply_subst subst where' 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' =
    List.fold_right2
     (fun entry selected_entry context' ->
@@ -146,15 +158,15 @@ let change_tac ~pattern with_what  =
      match entry,selected_entry with
          None,None -> None::context'
        | Some (name,Cic.Decl ty),Some (`Decl selected_ty) ->
-          let ty' = change context'_len ty selected_ty in
+          let ty' = change subst context'_len ty selected_ty in
            Some (name,Cic.Decl ty')::context'
        | Some (name,Cic.Def (bo,ty)),Some (`Def (selected_bo,selected_ty)) ->
-          let bo' = change context'_len bo selected_bo in
+          let bo' = change subst context'_len bo selected_bo in
           let ty' =
            match ty,selected_ty with
               None,None -> None
             | Some ty,Some selected_ty ->
-               Some (change context'_len ty selected_ty)
+               Some (change subst context'_len ty selected_ty)
             | _,_ -> assert false
           in
            Some (name,Cic.Def (bo',ty'))::context'