New tactic unfold.

[helm.git] / helm / matita / matitaEngine.ml

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index 1d23ac063709e3fe57265c86f57a95ae56bcb1e4..da3a730fb7831212b17c5f6ab09b012fefe78e2a 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -97,6 +97,7 @@ let tactic_of_ast = function
        | `Normalize -> CicReduction.normalize ~delta:false ~subst:[]
        | `Reduce -> ProofEngineReduction.reduce
        | `Simpl -> ProofEngineReduction.simpl
+       | `Unfold what -> ProofEngineReduction.unfold ?what
        | `Whd -> CicReduction.whd ~delta:false ~subst:[]
      in
       Tactics.fold ~reduction ~term ~pattern
@@ -125,6 +126,7 @@ let tactic_of_ast = function
       | `Normalize -> Tactics.normalize ~pattern
       | `Reduce -> Tactics.reduce ~pattern  
       | `Simpl -> Tactics.simpl ~pattern 
+      | `Unfold what -> Tactics.unfold ~pattern ?what
       | `Whd -> Tactics.whd ~pattern)
   | GrafiteAst.Reflexivity _ -> Tactics.reflexivity
   | GrafiteAst.Replace (_, pattern, with_what) ->
@@ -171,6 +173,16 @@ let disambiguate_pattern status (wanted, hyp_paths, goal_path) =
         status, Some wanted
   in
    status, (wanted, hyp_paths ,goal_path)
+
+let disambiguate_reduction_kind status = function
+  | `Unfold (Some t) ->
+      let status, t = disambiguate_term status t in
+      status, `Unfold (Some t)
+  | `Normalize
+  | `Reduce
+  | `Simpl
+  | `Unfold None
+  | `Whd as kind -> status, kind
   
 let disambiguate_tactic status = function
   | GrafiteAst.Apply (loc, term) ->
@@ -233,10 +245,11 @@ let disambiguate_tactic status = function
       status, GrafiteAst.ElimType (loc, what, None, depth, idents)
   | GrafiteAst.Exists loc -> status, GrafiteAst.Exists loc 
   | GrafiteAst.Fail loc -> status,GrafiteAst.Fail loc
-  | GrafiteAst.Fold (loc,reduction_kind, term, pattern) ->
+  | GrafiteAst.Fold (loc,red_kind, term, pattern) ->
      let status, pattern = disambiguate_pattern status pattern in
      let status, term = disambiguate_term status term in
-     status, GrafiteAst.Fold (loc,reduction_kind, term, pattern)
+     let status, red_kind = disambiguate_reduction_kind status red_kind in
+     status, GrafiteAst.Fold (loc,red_kind, term, pattern)
   | GrafiteAst.FwdSimpl (loc, hyp, names) ->
      status, GrafiteAst.FwdSimpl (loc, hyp, names)  
   | GrafiteAst.Fourier loc -> status, GrafiteAst.Fourier loc
@@ -262,9 +275,10 @@ let disambiguate_tactic status = function
   | GrafiteAst.LetIn (loc, term, name) ->
       let status, term = disambiguate_term status term in
       status, GrafiteAst.LetIn (loc,term,name)
-  | GrafiteAst.Reduce (loc, reduction_kind, pattern) ->
+  | GrafiteAst.Reduce (loc, red_kind, pattern) ->
       let status, pattern = disambiguate_pattern status pattern in
-      status, GrafiteAst.Reduce(loc, reduction_kind, pattern)
+      let status, red_kind = disambiguate_reduction_kind status red_kind in
+      status, GrafiteAst.Reduce(loc, red_kind, pattern)
   | GrafiteAst.Reflexivity loc -> status, GrafiteAst.Reflexivity loc
   | GrafiteAst.Replace (loc, pattern, with_what) -> 
       let status, pattern = disambiguate_pattern status pattern in