X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=9f0cff9ad305696fc1f3ba6d5e33e4d8c009ee3a;hb=33a02e0b639217093eb63f30169aaa6ac8c78907;hp=160e2ff081c24418d2182649e6a6266cc8a59821;hpb=fc414b7e91d15ce6cccd9a4e8b558c2ab71b4b60;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 160e2ff08..9f0cff9ad 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -415,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
@@ -444,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 
@@ -581,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