X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=9355dfc10d20f1c1e4dca37c4754c1bbbacf68ca;hb=71590f4a0cb620a5e98fee3e8d65670271234532;hp=a3e774d1d84e46f7345392f81780cc212d229732;hpb=1db44a3e28f767afea3b87f21aaeb81c586b1733;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index a3e774d1d..9355dfc10 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
@@ -500,8 +544,8 @@ let get_metadata t =
 let debug_metadata = function
    | None                 -> ()
    | Some (outer, inners) -> 
-      let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n uri in
-      Printf.eprintf "\n%s: %s\n" "fwd" outer;
+      let f (n, uri) = Printf.eprintf "%s: %i %s\n" "fwd" n (UriManager.string_of_uri uri) in
+      Printf.eprintf "\n%s: %s\n" "fwd" (UriManager.string_of_uri outer);
       List.iter f inners; prerr_newline ()
 
 let fwd_simpl ~dbd t =
@@ -525,8 +569,9 @@ let fwd_simpl ~dbd t =
    let compare (_, x) (_, y) = compare x y in
    let filter n (uri, rank) =
       if rank > 0 then Some (UriManager.uri_of_string uri) else None
-   in   
-   match get_metadata t with
+   in
+   let metadata = get_metadata t in debug_metadata metadata;
+   match metadata with
       | None                 -> []
       | Some (outer, inners) ->
          let select = "source, h_inner, h_index" in
@@ -536,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
+         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