added homepage URL, now we have one

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

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