Moved paramodulation inside tactics.

[helm.git] / helm / ocaml / grafite_engine / grafiteEngine.ml

diff --git a/helm/ocaml/grafite_engine/grafiteEngine.ml b/helm/ocaml/grafite_engine/grafiteEngine.ml
index c0a453c932e0eae3dee583458e3d07f76bc6d9d8..60b2b6a9dbe08935058edbd75244ec0854d7aa17 100644 (file)
--- a/helm/ocaml/grafite_engine/grafiteEngine.ml
+++ b/helm/ocaml/grafite_engine/grafiteEngine.ml
@@ -95,6 +95,8 @@ let tactic_of_ast ast =
   | GrafiteAst.Fold (_, reduction_kind, term, pattern) ->
       let reduction =
         match reduction_kind with
+        | `Demodulate -> 
+            GrafiteTypes.command_error "demodulation can't be folded"
         | `Normalize ->
             PET.const_lazy_reduction
               (CicReduction.normalize ~delta:false ~subst:[])
@@ -136,11 +138,12 @@ let tactic_of_ast ast =
       Tactics.letin term ~mk_fresh_name_callback:(namer_of [name])
   | GrafiteAst.Reduce (_, reduction_kind, pattern) ->
       (match reduction_kind with
-      | `Normalize -> Tactics.normalize ~pattern
-      | `Reduce -> Tactics.reduce ~pattern  
-      | `Simpl -> Tactics.simpl ~pattern 
-      | `Unfold what -> Tactics.unfold ~pattern what
-      | `Whd -> Tactics.whd ~pattern)
+        | `Demodulate -> Tactics.demodulate ~dbd:(LibraryDb.instance ()) ~pattern
+        | `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) ->
      Tactics.replace ~pattern ~with_what