- changed license to lgpl

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

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index bb5594a35693f50917f86516419df44858e373b0..0a1f1ee441e939f22e9364b1806c626db1ada685 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -28,15 +28,31 @@ open Printf
 module Constr = MetadataConstraints
 module PET = ProofEngineTypes 
 
+  (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
+  * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
+let sqlpat_of_shellglob =
+  let star_RE, qmark_RE, percent_RE, uscore_RE =
+    Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_"
+  in
+  fun shellglob ->
+    Pcre.replace ~rex:star_RE ~templ:"%"
+      (Pcre.replace ~rex:qmark_RE ~templ:"_"
+        (Pcre.replace ~rex:percent_RE ~templ:"\\%"
+          (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
+            shellglob)))
+
 let nonvar s =
   let len = String.length s in
   let suffix = String.sub s (len-4) 4 in
   not (suffix  = ".var")
 
-let locate ~(dbd:Mysql.dbd) ?(vars = false) name =
+let locate ~(dbd:Mysql.dbd) ?(vars = false) pat =
+  let sql_pat = sqlpat_of_shellglob pat in
   let query =
-    sprintf "SELECT source FROM %s WHERE value = \"%s\""
-      MetadataTypes.name_tbl name
+        sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
+                 "SELECT source FROM %s WHERE value LIKE \"%s\"")
+          (MetadataTypes.name_tbl ()) sql_pat
+           MetadataTypes.library_name_tbl sql_pat
   in
   let result = Mysql.exec dbd query in
   List.filter nonvar
@@ -94,15 +110,27 @@ let compare_goal_list proof goal1 goal2 =
   let _,metasenv,_,_ = proof in
   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
-  let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
-  let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
+  let ty_sort1,_ = 
+    CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph 
+  in
+  let ty_sort2,_ = 
+    CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph 
+  in
   let prop1 =
-    if CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
-    else 1
+    let b,_ = 
+      CicReduction.are_convertible 
+       ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph 
+    in
+      if b then 0
+      else 1
   in
   let prop2 =
-    if CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
-    else 1
+    let b,_ = 
+      CicReduction.are_convertible 
+       ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph 
+    in 
+      if b then 0
+      else 1
   in
   prop1 - prop2
 
@@ -126,7 +154,6 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-prerr_endline "HYP SIGNATURE";
 Constr.StringSet.iter prerr_endline hyp_constants;
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
@@ -144,7 +171,7 @@ Constr.StringSet.iter prerr_endline hyp_constants;
         (let status' =
             try
               let (proof, goal_list) =
-                prerr_endline ("STO APPLICANDO " ^ uri);
+(*                prerr_endline ("STO APPLICANDO " ^ uri); *)
                PET.apply_tactic
                   (PrimitiveTactics.apply_tac
                    ~term:(CicUtil.term_of_uri uri))
@@ -198,7 +225,6 @@ let experimental_hint
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
-prerr_endline "HYP SIGNATURE";
 Constr.StringSet.iter prerr_endline hyp_constants;
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
@@ -216,7 +242,7 @@ Constr.StringSet.iter prerr_endline hyp_constants;
         (let status' =
             try
               let (subst,(proof, goal_list)) =
-                  prerr_endline ("STO APPLICANDO" ^ uri);
+                  (* prerr_endline ("STO APPLICANDO" ^ uri); *)
                   PrimitiveTactics.apply_tac_verbose 
                    ~term:(CicUtil.term_of_uri uri)
                   status