Added a function equations_for_goal similar to signature_of_goal.

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index a01044e8cf15ecc5f8434bec7faa26be5b0d52fe..160e2ff081c24418d2182649e6a6266cc8a59821 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -28,6 +28,8 @@ open Printf
 module Constr = MetadataConstraints
 module PET = ProofEngineTypes 
 
+exception Goal_is_not_an_equation
+
 let debug_print = fun _ -> ()
 
   (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
@@ -195,6 +197,28 @@ let close_with_types s metasenv context =
       Constr.UriManagerSet.union bag (Constr.constants_of ty)) 
     s s
 
+let close_with_constructors s metasenv context =
+  Constr.UriManagerSet.fold 
+    (fun e bag -> 
+      let t = CicUtil.term_of_uri e in
+      match t with
+         Cic.MutInd (uri,_,_)  
+       | Cic.MutConstruct (uri,_,_,_) ->  
+           (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
+                Cic.InductiveDefinition(tl,_,_,_) ->
+                  snd
+                    (List.fold_left
+                       (fun (i,s) (_,_,_,cl) ->
+                          let _,s =
+                            List.fold_left 
+                              (fun (j,s) _ -> 
+                                 let curi = UriManager.uri_of_uriref uri i (Some j) in
+                                   j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
+                            (i+1,s)) (0,bag) tl)
+              | _ -> assert false)
+       | _ -> bag)
+    s s
+
 let apply_tac_verbose =
  let profiler = CicUtil.profile "apply_tac_verbose" in
   fun ~term status -> profiler (PrimitiveTactics.apply_tac_verbose ~term) status
@@ -225,6 +249,26 @@ let signature_of_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   uris
 
+let equations_for_goal ~(dbd:Mysql.dbd) ((proof, goal) as status) =
+ 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
+
 let experimental_hint 
   ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in

diff --git a/helm/ocaml/tactics/metadataQuery.mli b/helm/ocaml/tactics/metadataQuery.mli
index c4b84453737206bb86263c91417496d39e338408..08ac016bf34e4cb175b1349d23b0858013d991fb 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.mli
+++ b/helm/ocaml/tactics/metadataQuery.mli
@@ -31,6 +31,9 @@
 val signature_of_goal:
   dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list
 
+val equations_for_goal:
+  dbd:Mysql.dbd -> ProofEngineTypes.status -> UriManager.uri list
+
 val locate:
   dbd:Mysql.dbd ->
   ?vars:bool -> string -> UriManager.uri list