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 f15417fc8ecea57bbaacea005ab3fc804007f1ec..11fef69a1317558fe75ed27deedac7cfd4c48fa0 100644 (file)
--- 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 cceeaf10dfb4b717f82e59c6e1d3154221607255..056e595e7ed8b8fc5eaf3867a47a1072e53058f9 100644 (file)
--- 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 48fbc4aa2115d9800e702ba8a1515beb7bbbc93a..3f4d4226f96fe5f19f40cb75495cae1a7707a9a2 100644 (file)
--- 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 72609b11842ac4f89e715eabdeba7ff714e6b19b..85c5c54be30300beb690e0d20a7c946afe11925a 100644 (file)
--- 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 c91e92e3f03e6c181148b47ed381101e9cfad79e..d9061c1efac5e026c88924897a3a8a9194d39e50 100644 (file)
--- 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 ->