the decompose tactic is now working

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 160e2ff081c24418d2182649e6a6266cc8a59821..9355dfc10d20f1c1e4dca37c4754c1bbbacf68ca 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -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