From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Tue, 12 Jul 2005 14:54:18 +0000 (+0000)
Subject: Added a function equations_for_goal similar to signature_of_goal.
X-Git-Tag: pre_notation~28
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=fc414b7e91d15ce6cccd9a4e8b558c2ab71b4b60;p=helm.git

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 a01044e8c..160e2ff08 100644
--- 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 c4b844537..08ac016bf 100644
--- 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