From: Alberto Griggio <griggio@fbk.eu>
Date: Fri, 22 Jul 2005 17:29:00 +0000 (+0000)
Subject: added optional "paramodulation" parameter to auto to turn on paramodulation
X-Git-Tag: V_0_7_2~98
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d43002dfc61afac676ea14bc6a1418e5ec0e3e9c;p=helm.git

added optional "paramodulation" parameter to auto to turn on paramodulation
---

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index f15417fc8..11fef69a1 100644
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -38,7 +38,7 @@ type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
   | Assumption of loc
-  | Auto of loc * int option * int option (* depth, width *)
+  | Auto of loc * int option * int option * string option (* depth, width, paramodulation ALB *)
   | Change of loc * ('term,'ident) pattern * 'term
   | Clear of loc * 'ident
   | ClearBody of loc * 'ident
diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index cceeaf10d..056e595e7 100644
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -107,8 +107,9 @@ EXTEND
         GrafiteAst.Assumption loc
     | IDENT "auto";
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
-      width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ] -> 
-          GrafiteAst.Auto (loc,depth,width)
+      width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
+      paramodulation = OPT [ IDENT "paramodulation" ] ->  (* ALB *)
+          GrafiteAst.Auto (loc,depth,width,paramodulation)
     | IDENT "clear"; id = IDENT ->
         GrafiteAst.Clear (loc,id)
     | IDENT "clearbody"; id = IDENT ->
diff --git a/helm/ocaml/cic_transformations/tacticAst.ml b/helm/ocaml/cic_transformations/tacticAst.ml
index 48fbc4aa2..3f4d4226f 100644
--- a/helm/ocaml/cic_transformations/tacticAst.ml
+++ b/helm/ocaml/cic_transformations/tacticAst.ml
@@ -38,7 +38,7 @@ type ('term, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
   | Assumption of loc
-  | Auto of loc * int option * int option (* depth, width *)
+  | Auto of loc * int option * int option * string option (* depth, width, paramodulation ALB *)
   | Change of loc * ('term,'ident) pattern * 'term
   | Clear of loc * 'ident
   | ClearBody of loc * 'ident
diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index 72609b118..85c5c54be 100644
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -308,7 +308,7 @@ let term_is_equality = ref
   (fun term -> debug_print "term_is_equality E` DUMMY!!!!"; false);;
 
 
-let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () =
+let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:Mysql.dbd) () =
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
       let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
@@ -331,16 +331,19 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd) () =
       | _ -> assert false
     in
     let paramodulation_ok =
-      let _, metasenv, _, _ = proof in
-      let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-      !term_is_equality meta_goal
+      match paramodulation with
+      | None -> false
+      | Some _ ->
+          let _, metasenv, _, _ = proof in
+          let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
+          !term_is_equality meta_goal
     in
     if paramodulation_ok then (
       debug_print "USO PARAMODULATION...";
-      try
+(*       try *)
         !paramodulation_tactic dbd (proof, goal)
-      with e ->
-        normal_auto ()
+(*       with ProofEngineTypes.Fail _ -> *)
+(*         normal_auto () *)
     ) else
       normal_auto () 
   in
diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli
index c91e92e3f..d9061c1ef 100644
--- a/helm/ocaml/tactics/autoTactic.mli
+++ b/helm/ocaml/tactics/autoTactic.mli
@@ -25,8 +25,9 @@
  *)
 
 val auto_tac:
-  ?depth:int -> ?width:int -> dbd:Mysql.dbd -> unit ->
-    ProofEngineTypes.tactic
+  ?depth:int -> ?width:int -> ?paramodulation:string ->
+  dbd:Mysql.dbd -> unit ->
+  ProofEngineTypes.tactic
 
 val paramodulation_tactic:
   (Mysql.dbd -> ProofEngineTypes.status ->