X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=9f0cff9ad305696fc1f3ba6d5e33e4d8c009ee3a;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=a01044e8cf15ecc5f8434bec7faa26be5b0d52fe;hpb=ebaf3deffea9ac78a2b8b2a6c128cc24ad8459ef;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index a01044e8c..9f0cff9ad 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
@@ -371,7 +415,7 @@ let fill_with_dummy_constants t =
     function
 	Cic.Lambda (n,s,t) -> 
 	  let dummy_uri = 
-	    UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)) in
+	    UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in
 	    (aux (i+1) (s::types)
 	       (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
       | t -> t,types
@@ -400,7 +444,7 @@ let instance ~dbd t =
       when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") -> 
       let s = UriManager.string_of_uri s in
       let len = String.length s in
-            let dummy_index = int_of_string (String.sub s 11 (len-11)) in
+            let dummy_index = int_of_string (String.sub s 11 (len-15)) in
       let dummy_type = List.nth types dummy_index in
       Some (d,dummy_type)
     | _::l -> look_for_dummy_main l 
@@ -537,7 +581,23 @@ let fwd_simpl ~dbd t =
            (Mysql.escape (UriManager.string_of_uri outer)) in
          let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
 	 let result = Mysql.exec dbd query in
-         let lemmas = Mysql.map result ~f:(map inners) in
+         let lemmas = Mysql.map ~f:(map inners) result in
 	 let ranked = List.fold_left rank [] lemmas in
 	 let ordered = List.rev (List.fast_sort compare ranked) in
          map_filter filter 0 ordered
+
+(* get_decomposables ********************************************************)
+
+let decomposables ~dbd =
+   let map row = match row.(0) with
+      | None     -> None
+      | Some str ->
+         match CicUtil.term_of_uri (UriManager.uri_of_string str) with
+            | Cic.MutInd (uri, typeno, _) -> Some (uri, typeno)
+	    | _                           -> 
+	       raise (UriManager.IllFormedUri str)
+   in
+   let select, from = "source", "decomposables" in
+   let query = Printf.sprintf "SELECT %s FROM %s" select from in
+   let decomposables = Mysql.map ~f:map (Mysql.exec dbd query) in
+   map_filter (fun _ x -> x) 0 decomposables