beginning of the tactics lapply and fwd

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 962aad8e7cac5e93999ccba089737116340ebc7d..1e7bbe690cc3ca52033d577965cd60e60fc1bbef 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -444,4 +444,69 @@ let instance ~dbd t =
             (n,from,where) constraints_for_dummy_type in
         Constr.exec ~dbd (m,from,where)
 
+(* fwd_simpl ****************************************************************)
 
+let rec map_filter f n = function
+   | []       -> []
+   | hd :: tl -> 
+      match f n hd with
+         | None    -> map_filter f (succ n) tl
+        | Some hd -> hd :: map_filter f (succ n) tl
+
+let get_uri t =
+   let aux = function
+      | Cic.Appl (hd :: tl) -> Some (CicUtil.uri_of_term hd, tl)
+      | hd                  -> Some (CicUtil.uri_of_term hd, []) 
+   in
+   try aux t with
+      | Invalid_argument "uri_of_term" -> None
+
+let get_metadata t =
+   let f n t =
+      match get_uri t with
+         | None          -> None 
+        | Some (uri, _) -> Some (n, uri)
+   in
+   match get_uri t with
+      | None             -> None
+      | Some (uri, args) -> Some (uri, map_filter f 1 args) 
+
+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;
+      List.iter f inners; prerr_newline ()
+
+let fwd_simpl ~dbd t =
+   let map inners row = 
+      match row.(0), row.(1), row.(2) with  
+         | Some source, Some inner, Some index -> 
+           source, List.mem (int_of_string index, inner) inners
+        | _                                   -> "", false
+   in
+   let rec rank ranks (source, ok) = 
+      match ranks, ok with
+         | [], false                               -> [source, 0]
+        | [], true                                -> [source, 1]
+        | (uri, i) :: tl, false when uri = source -> (uri, 0) :: tl
+        | (uri, 0) :: tl, true when uri = source  -> (uri, 0) :: tl
+        | (uri, i) :: tl, true when uri = source  -> (uri, succ i) :: tl
+        | hd :: tl, _ -> hd :: rank tl (source, ok)
+   in
+   let compare (_, x) (_, y) = compare x y in
+   let filter n (uri, rank) =
+      if rank > 0 then Some uri else None
+   in   
+   match get_metadata t with
+      | None                 -> []
+      | Some (outer, inners) ->
+         let select = "source, h_inner, h_index" in
+        let from = "genLemma" in
+        let where = Printf.sprintf "h_outer = \"%s\"" (Mysql.escape 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 ranked = List.fold_left rank [] lemmas in
+        let ordered = List.rev (List.fast_sort compare ranked) in
+        map_filter filter 0 ordered