new signature of auto_tac, with a new optional argument "full", to invoke the

new paramodulation

diff --git a/helm/ocaml/cic_notation/grafiteAst.ml b/helm/ocaml/cic_notation/grafiteAst.ml
index da5c85411317faa108cc7891947d6870ca2fb909..53cbc353fa49aa676003df9ced084cd221a7fd53 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteAst.ml
+++ b/helm/ocaml/cic_notation/grafiteAst.ml
@@ -47,8 +47,8 @@ type ('term, 'lazy_term, 'reduction, 'ident) tactic =
   | Absurd of loc * 'term
   | Apply of loc * 'term
   | Assumption of loc
-  | Auto of loc * int option * int option * string option
-      (* depth, width, paramodulation *)
+  | Auto of loc * int option * int option * string option * string option 
+      (* depth, width, paramodulation, full *) (* ALB *)
   | Change of loc * ('term, 'lazy_term, 'ident) pattern * 'lazy_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 5caba868b1e220b2392f337f17e56317baaa2d2f..c3a4b7f01ef998e30c5debd31d5ee34a032725bb 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -112,8 +112,9 @@ EXTEND
     | IDENT "auto";
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
       width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
-      paramodulation = OPT [ IDENT "paramodulation" ] ->  (* ALB *)
-          GrafiteAst.Auto (loc,depth,width,paramodulation)
+      paramodulation = OPT [ IDENT "paramodulation" ];
+      full = OPT [ IDENT "full" ] ->  (* ALB *)
+          GrafiteAst.Auto (loc,depth,width,paramodulation,full)
     | IDENT "clear"; id = IDENT ->
         GrafiteAst.Clear (loc,id)
     | IDENT "clearbody"; id = IDENT ->

diff --git a/helm/ocaml/tactics/.depend b/helm/ocaml/tactics/.depend
index d28ff337d3a17aa5d71ef17f3401c83a9f589f02..1ef89807d6d96a58db886f8fdfc39572a4d9fb81 100644 (file)
--- a/helm/ocaml/tactics/.depend
+++ b/helm/ocaml/tactics/.depend
@@ -18,10 +18,12 @@ statefulProofEngine.cmi: proofEngineTypes.cmi
 tactics.cmi: proofEngineTypes.cmi 
 proofEngineTypes.cmo: proofEngineTypes.cmi 
 proofEngineTypes.cmx: proofEngineTypes.cmi 
-proofEngineReduction.cmo: proofEngineHelpers.cmi proofEngineReduction.cmi 
-proofEngineReduction.cmx: proofEngineHelpers.cmx proofEngineReduction.cmi 
 proofEngineHelpers.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi 
 proofEngineHelpers.cmx: proofEngineTypes.cmx proofEngineHelpers.cmi 
+proofEngineReduction.cmo: proofEngineTypes.cmi proofEngineHelpers.cmi \
+    proofEngineReduction.cmi 
+proofEngineReduction.cmx: proofEngineTypes.cmx proofEngineHelpers.cmx \
+    proofEngineReduction.cmi 
 tacticals.cmo: proofEngineTypes.cmi tacticals.cmi 
 tacticals.cmx: proofEngineTypes.cmx tacticals.cmi 
 reductionTactics.cmo: proofEngineTypes.cmi proofEngineReduction.cmi \

diff --git a/helm/ocaml/tactics/autoTactic.ml b/helm/ocaml/tactics/autoTactic.ml
index a0835a9b89db982e12e2a483cda54c72afa29068..9b716637a9ed8c0c1c4ba2736034595365b461b3 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.ml
+++ b/helm/ocaml/tactics/autoTactic.ml
@@ -305,13 +305,15 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
 *)
 
 let paramodulation_tactic = ref
-  (fun dbd status -> raise (ProofEngineTypes.Fail "Not Ready yet..."));;
+  (fun dbd ?full ?depth ?width status ->
+     raise (ProofEngineTypes.Fail "Not Ready yet..."));;
 
 let term_is_equality = ref
   (fun term -> debug_print (lazy "term_is_equality E` DUMMY!!!!"); false);;
 
 
-let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd:HMysql.dbd) () =
+let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation
+    ?full ~(dbd:HMysql.dbd) () =
   let auto_tac dbd (proof, goal) =
     let normal_auto () = 
       let universe = MetadataQuery.signature_of_goal ~dbd (proof, goal) in
@@ -333,18 +335,19 @@ let auto_tac ?(depth=default_depth) ?(width=default_width) ?paramodulation ~(dbd
          (proof,[])
       | _ -> assert false
     in
+    let full = match full with None -> false | Some _ -> true in
     let paramodulation_ok =
       match paramodulation with
       | None -> false
       | Some _ ->
           let _, metasenv, _, _ = proof in
           let _, _, meta_goal = CicUtil.lookup_meta goal metasenv in
-          !term_is_equality meta_goal
+          full || (!term_is_equality meta_goal)
     in
     if paramodulation_ok then (
       debug_print (lazy "USO PARAMODULATION...");
 (*       try *)
-        !paramodulation_tactic dbd (proof, goal)
+      !paramodulation_tactic dbd ~depth ~width ~full (proof, goal)
 (*       with ProofEngineTypes.Fail _ -> *)
 (*         normal_auto () *)
     ) else

diff --git a/helm/ocaml/tactics/autoTactic.mli b/helm/ocaml/tactics/autoTactic.mli
index e2f20f787f06c4b36ec70a98dca0d9e50824fd52..696c97007610b39a105fe6a74f338f3dc577fae9 100644 (file)
--- a/helm/ocaml/tactics/autoTactic.mli
+++ b/helm/ocaml/tactics/autoTactic.mli
@@ -25,12 +25,13 @@
  *)
 
 val auto_tac:
-  ?depth:int -> ?width:int -> ?paramodulation:string ->
+  ?depth:int -> ?width:int -> ?paramodulation:string -> ?full:string ->
   dbd:HMysql.dbd -> unit ->
   ProofEngineTypes.tactic
 
 val paramodulation_tactic:
-  (HMysql.dbd -> ProofEngineTypes.status ->
+  (HMysql.dbd -> ?full:bool -> ?depth:int -> ?width:int ->
+    ProofEngineTypes.status ->
      ProofEngineTypes.proof * ProofEngineTypes.goal list) ref
 
 val term_is_equality:

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index c266502cb16fa50378252228c2f3c7af2e9dea7c..6f6b2e00a68419b0e8ddfd179c6775e0e6c919cd 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -255,24 +255,46 @@ let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
   uris
 
 let equations_for_goal ~(dbd:HMysql.dbd) ((proof, goal) as status) =
+  let to_string set =
+    "{ " ^
+      (String.concat ", "
+         (Constr.UriManagerSet.fold
+            (fun u l -> (UriManager.string_of_uri u)::l) set []))
+    ^ " }"
+  in
  let (_, metasenv, _, _) = proof in
  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  let main, sig_constants = Constr.signature_of ty in
- match main with
-     None -> raise Goal_is_not_an_equation
-   | Some (m,l) ->
-       if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then
-        let set = signature_of_hypothesis context in
-        let set = Constr.UriManagerSet.union set sig_constants in
-        let set = close_with_types set metasenv context in
-         let set = close_with_constructors set metasenv context in
-         let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
-        let uris =
-          sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
-        let uris = List.filter nonvar (List.map snd uris) in
-        let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
-          uris
-       else raise Goal_is_not_an_equation
+(*  Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
+(*  match main with *)
+(*      None -> raise Goal_is_not_an_equation *)
+(*    | Some (m,l) -> *)
+ let m, l =
+   let eq_URI = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI in
+   match main with
+   | None -> eq_URI, []
+   | Some (m, l) when UriManager.eq m eq_URI -> m, l
+   | Some (m, l) -> eq_URI, []
+ in
+ Printf.printf "\nSome (m, l): %s, [%s]\n\n"
+   (UriManager.string_of_uri m)
+   (String.concat "; " (List.map UriManager.string_of_uri l));
+ (*        if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
+ let set = signature_of_hypothesis context in
+ (*          Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
+ let set = Constr.UriManagerSet.union set sig_constants in
+ let set = close_with_types set metasenv context in
+ (*          Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
+ let set = close_with_constructors set metasenv context in
+ (*          Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
+ let set = List.fold_right Constr.UriManagerSet.remove (m::l) set in
+ let uris =
+   sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
+ let uris = List.filter nonvar (List.map snd uris) in
+ let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+ uris
+   (*        ) *)
+   (*        else raise Goal_is_not_an_equation *)
 
 let experimental_hint 
   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =

diff --git a/helm/ocaml/tactics/tactics.mli b/helm/ocaml/tactics/tactics.mli
index 8ea9f641c08932c13e5f75a73bd9b6fb75f3045d..6d524093569a91663c8f57ec091286a756e31350 100644 (file)
--- a/helm/ocaml/tactics/tactics.mli
+++ b/helm/ocaml/tactics/tactics.mli
@@ -5,7 +5,8 @@ val assumption : ProofEngineTypes.tactic
 val auto :
   ?depth:int ->
   ?width:int ->
-  ?paramodulation:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic
+  ?paramodulation:string ->
+  ?full:string -> dbd:HMysql.dbd -> unit -> ProofEngineTypes.tactic
 val change :
   pattern:ProofEngineTypes.pattern ->
   ProofEngineTypes.lazy_term -> ProofEngineTypes.tactic