X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FmetadataQuery.ml;h=962aad8e7cac5e93999ccba089737116340ebc7d;hb=f541206af7fccf9de78b31d8f2aaf5f786f63d1f;hp=13a73b561b6e477b164c1f008e351b832e9bdb17;hpb=536faacc0486948d23c5fd02a693f0def64fb666;p=helm.git

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 13a73b561..962aad8e7 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -26,27 +26,84 @@
 open Printf
 
 module Constr = MetadataConstraints
+module PET = ProofEngineTypes 
 
-let locate ~(dbh:Dbi.connection) name =
-  let query =
-    dbh#prepare (sprintf "SELECT value FROM %s WHERE source = \"%s\""
-      MetadataTypes.name_tbl name)
-  in
-  query#execute [];
-  List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
+let debug_print = fun _ -> ()
 
-let match_term ~(dbh:Dbi.connection) ty =
-  let constraints =
-    List.map MetadataTypes.constr_of_metadata
-      (MetadataExtractor.compute ~body:None ~ty)
+  (** 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
-  Constr.at_least ~dbh constraints
+  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) pat =
+  let sql_pat = sqlpat_of_shellglob pat in
+  let query =
+        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
+    (Mysql.map result
+      (fun cols -> match cols.(0) with Some s -> s | _ -> assert false))
+
+let match_term ~(dbd:Mysql.dbd) ty =
+(*   debug_print (CicPp.ppterm ty); *)
+  let metadata = MetadataExtractor.compute ~body:None ~ty in
+  let constants_no =
+    MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
+  in
+  let full_card, diff =
+    if CicUtil.is_meta_closed ty then
+      Some (MetadataConstraints.Eq constants_no), None
+    else
+      let diff_no =
+        let (hyp_constants, concl_constants) =
+          (* collect different constants in hypotheses and conclusions *)
+          List.fold_left
+            (fun ((hyp, concl) as acc) metadata ->
+               match (metadata: MetadataTypes.metadata) with
+               | `Sort _ | `Rel _ -> acc
+               | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
+                 when not (List.mem uri concl) -> (hyp, uri :: concl)
+               | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
+                 when not (List.mem uri hyp) -> (uri :: hyp, concl)
+               | `Obj _ -> acc)
+            ([], [])
+            metadata
+        in
+        List.length hyp_constants - List.length concl_constants
+      in
+      let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
+      let diff =
+        if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
+          Some (MetadataConstraints.Eq diff_no)
+        else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
+          Some (MetadataConstraints.Gt (diff_no - 1))
+        else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
+          Some (MetadataConstraints.Lt (diff_no + 1))
+        else
+          None
+      in
+      None, diff
+  in
+  let constraints = List.map MetadataTypes.constr_of_metadata metadata in
+    Constr.at_least ~dbd ?full_card ?diff constraints
+
 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
 
 let signature_of_hypothesis context =
@@ -59,12 +116,15 @@ let signature_of_hypothesis context =
           Constr.StringSet.union set (Constr.constants_of t))
     Constr.StringSet.empty context
 
-let intersect l1 l2 =
-  let set1 = List.fold_right Constr.StringSet.add l1 Constr.StringSet.empty in
-  let set2 = List.fold_right Constr.StringSet.add l2 Constr.StringSet.empty in
-  Constr.StringSet.elements (Constr.StringSet.inter set1 set2)
+let intersect uris siguris =
+  let set1 = List.fold_right Constr.StringSet.add uris Constr.StringSet.empty in
+  let set2 =
+    List.fold_right Constr.StringSet.add siguris Constr.StringSet.empty
+  in
+  let inter = Constr.StringSet.inter set1 set2 in
+  List.filter (fun s -> Constr.StringSet.mem s inter) uris
 
-let filter_uris_forward ~dbh (main, constants) uris =
+let filter_uris_forward ~dbd (main, constants) uris =
   let main_uris =
     match main with
     | None -> []
@@ -73,23 +133,53 @@ let filter_uris_forward ~dbh (main, constants) uris =
   let full_signature =
     List.fold_right Constr.StringSet.add main_uris constants
   in
-  List.filter (Constr.at_most ~dbh full_signature) uris
+  List.filter (Constr.at_most ~dbd ~where:`Statement full_signature) uris
 
-let filter_uris_backward ~dbh signature uris =
+let filter_uris_backward ~dbd ~facts signature uris =
   let siguris =
-    List.map snd (MetadataConstraints.sigmatch ~dbh ~where:`Statement signature)
+    List.map snd 
+      (MetadataConstraints.sigmatch ~dbd ~facts ~where:`Statement signature)
   in
-  intersect uris siguris
+    intersect uris siguris 
 
-let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
+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 CicUniv.empty_ugraph 
+  in
+  let ty_sort2,_ = 
+    CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph 
+  in
+  let prop1 =
+    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 =
+    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
+
+let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
   let (_, metasenv, _, _) = proof in
   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
   let (uris, (main, sig_constants)) =
     match signature with
-    | Some signature -> (Constr.sigmatch ~dbh signature, signature)
-    | None -> (Constr.cmatch' ~dbh ty, Constr.signature_of ty)
+    | Some signature -> (Constr.sigmatch ~dbd ~facts signature, signature)
+    | None -> (Constr.cmatch' ~dbd ~facts ty, Constr.signature_of ty)
   in
   let uris = List.filter nonvar (List.map snd uris) in
+  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
   let types_constants =
     match main with
     | None -> Constr.StringSet.empty
@@ -100,20 +190,258 @@ let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
   let hyp_constants =
     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
   in
+(* Constr.StringSet.iter debug_print hyp_constants; *)
   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
   let uris = 
-    if (List.length uris < 2 ** (Constr.StringSet.cardinal other_constants))
+    let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
+    if ((List.length uris < pow) or (pow <= 0))
+    then begin
+(*       debug_print "MetadataQuery: large sig, falling back to old method"; *)
+      filter_uris_forward ~dbd (main, other_constants) uris
+    end else
+      filter_uris_backward ~dbd ~facts (main, other_constants) uris
+  in
+  let rec aux = function
+    | [] -> []
+    | uri :: tl ->
+        (let status' =
+            try
+              let (proof, goal_list) =
+(*                debug_print ("STO APPLICANDO " ^ uri); *)
+		PET.apply_tactic
+                  (PrimitiveTactics.apply_tac
+		    ~term:(CicUtil.term_of_uri uri))
+                  status
+              in
+              let goal_list =
+                List.stable_sort (compare_goal_list proof) goal_list
+              in
+              Some (uri, (proof, goal_list))
+            with ProofEngineTypes.Fail _ -> None
+          in
+          match status' with
+          | None -> aux tl
+          | Some status' ->
+              status' :: aux tl)
+  in
+  List.stable_sort
+    (fun (_, (_, goals1)) (_, (_, goals2)) ->
+      Pervasives.compare (List.length goals1) (List.length goals2))
+    (aux uris)
+
+(* experimental_hint is a version of hint for experimental 
+    purposes. It uses auto_tac_verbose instead of auto tac.
+    Auto_tac verbose also returns a substitution - for the moment 
+    as a function from cic to cic, to be changed into an association
+    list in the future -. This substitution is used to build a
+    hash table of the inspected goals with their associated proofs.
+    The cose is a cut and paste of the previous one: at the end 
+    of the experimentation we shall make a choice. *)
+
+let close_with_types s metasenv context =
+  Constr.StringSet.fold 
+    (fun e bag -> 
+      let t = CicUtil.term_of_uri e in
+      let ty, _ = 
+        CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph  
+      in
+      Constr.StringSet.union bag (Constr.constants_of ty)) 
+    s s
+
+let experimental_hint 
+  ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
+  let (_, metasenv, _, _) = proof in
+  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
+  let (uris, (main, sig_constants)) =
+    match signature with
+    | Some signature -> 
+	(Constr.sigmatch ~dbd ~facts signature, signature)
+    | None -> 
+	(Constr.cmatch' ~dbd ~facts ty, Constr.signature_of ty)
+  in 
+  let uris = List.filter nonvar (List.map snd uris) in
+  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
+  let types_constants =
+    match main with
+    | None -> Constr.StringSet.empty
+    | Some (main, types) ->
+        List.fold_right Constr.StringSet.add (main :: types)
+          Constr.StringSet.empty
+  in
+  let all_constants =
+    let hyp_and_sug =
+      Constr.StringSet.union
+        (signature_of_hypothesis context) 
+        sig_constants
+    in
+    let main = 
+      match main with
+      | None -> Constr.StringSet.empty
+      | Some (main,_) -> 
+          let ty, _ = 
+            CicTypeChecker.type_of_aux' 
+              metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
+          in
+          Constr.constants_of ty
+    in
+    Constr.StringSet.union main hyp_and_sug
+  in
+(* Constr.StringSet.iter debug_print hyp_constants; *)
+  let all_constants_closed = close_with_types all_constants metasenv context in
+  let other_constants = 
+    Constr.StringSet.diff all_constants_closed types_constants
+  in
+  debug_print "all_constants_closed";
+  Constr.StringSet.iter debug_print all_constants_closed;
+  debug_print "other_constants";
+  Constr.StringSet.iter debug_print other_constants;
+  let uris = 
+    let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
+    if ((List.length uris < pow) or (pow <= 0))
     then begin
-      prerr_endline "MetadataQuery: large sig, falling back to old method";
-      filter_uris_forward ~dbh (main, other_constants) uris
+      debug_print "MetadataQuery: large sig, falling back to old method";
+      filter_uris_forward ~dbd (main, other_constants) uris
     end else
-      filter_uris_backward ~dbh (main, other_constants) uris
-  in
-  List.map
-    (fun uri ->
-      (uri,
-       ProofEngineTypes.apply_tactic
-        (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
-        status))
-    uris
+      filter_uris_backward ~dbd ~facts (main, other_constants) uris
+  in 
+  let rec aux = function
+    | [] -> []
+    | uri :: tl ->
+        (let status' =
+            try
+              let (subst,(proof, goal_list)) =
+                  (* debug_print ("STO APPLICANDO" ^ uri); *)
+                  PrimitiveTactics.apply_tac_verbose 
+		    ~term:(CicUtil.term_of_uri uri)
+                  status
+              in
+              let goal_list =
+                List.stable_sort (compare_goal_list proof) goal_list
+              in
+              Some (uri, (subst,(proof, goal_list)))
+            with ProofEngineTypes.Fail _ -> None
+          in
+          match status' with
+          | None -> aux tl
+          | Some status' -> status' :: aux tl)
+  in
+  List.stable_sort
+    (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
+      Pervasives.compare (List.length goals1) (List.length goals2))
+    (aux uris)
+
+let elim ~dbd uri =
+  let constraints =
+    [`Rel [`MainConclusion None];
+     `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]);
+     `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
+     `Obj (uri,[`InHypothesis]);
+    ]
+  in
+  MetadataConstraints.at_least ~rating:`Hits ~dbd constraints
+
+
+let fill_with_dummy_constants t =
+  let rec aux i types =
+    function
+	Cic.Lambda (n,s,t) -> 
+	  let dummy_uri = 
+	    UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)) in
+	    (aux (i+1) (s::types)
+	       (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
+      | t -> t,types
+  in 
+  let t,types = aux 0 [] t in
+  t, List.rev types
+      
+let instance ~dbd t =
+  let t',types = fill_with_dummy_constants t in 
+  let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
+(*   List.iter 
+    (fun x -> 
+       debug_print 
+         (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))) 
+    metadata; *)
+  let no_concl = MetadataDb.count_distinct `Conclusion metadata in
+  let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
+  let no_full = MetadataDb.count_distinct `Statement metadata in
+  let is_dummy = function
+    | `Obj(s, _) -> (String.sub s 0 10) <> "cic:/dummy" 
+	  | _ -> true 
+  in
+  let rec look_for_dummy_main = function
+	  | [] -> None
+    | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_ 
+      when ((String.sub s 0 10) = "cic:/dummy") -> 
+      let len = String.length s in
+            let dummy_index = int_of_string (String.sub s 11 (len-11)) in
+      let dummy_type = List.nth types dummy_index in
+      Some (d,dummy_type)
+    | _::l -> look_for_dummy_main l 
+  in
+  match (look_for_dummy_main metadata) with
+    | None->
+(*         debug_print "Caso None"; *)
+        (* no dummy in main position *)
+        let metadata = List.filter is_dummy metadata in
+        let constraints = List.map MetadataTypes.constr_of_metadata metadata in
+        let concl_card = Some (MetadataConstraints.Eq no_concl) in
+        let full_card = Some (MetadataConstraints.Eq no_full) in
+        let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
+          Constr.at_least ~dbd ?concl_card ?full_card ?diff constraints
+    | Some (depth, dummy_type) ->
+(*         debug_print 
+          (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type)); *)
+        (* a dummy in main position *)
+        let metadata_for_dummy_type = 
+          MetadataExtractor.compute ~body:None ~ty:dummy_type in
+        (* Let us skip this for the moment 
+           let main_of_dummy_type = 
+           look_for_dummy_main metadata_for_dummy_type in *)
+        let metadata = List.filter is_dummy metadata in
+        let constraints = List.map MetadataTypes.constr_of_metadata metadata in
+        let metadata_for_dummy_type = 
+          List.filter is_dummy metadata_for_dummy_type in
+        let metadata_for_dummy_type, depth' = 
+          (* depth' = the depth of the A -> A -> Prop *)
+          List.fold_left (fun (acc,dep) c ->
+            match c with
+            | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> 
+                (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
+            | `Obj  (s,`MainConclusion (Some (MetadataTypes.Eq i))) -> 
+                (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
+            | `Rel  (`MainConclusion (Some (MetadataTypes.Eq i))) -> 
+                (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
+            | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type
+        in
+        let constraints_for_dummy_type =
+           List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
+        (* start with the dummy constant in main conlusion *)
+        let from = ["refObj as table0"] in
+        let where = 
+          [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
+                 sprintf "table0.h_depth >= %d" depth] in
+        let (n,from,where) =
+          List.fold_left 
+            (MetadataConstraints.add_constraint ~start:2)
+            (2,from,where) constraints in
+        let concl_card = Some (MetadataConstraints.Eq no_concl) in
+        let full_card = Some (MetadataConstraints.Eq no_full) in
+        let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
+        let (n,from,where) = 
+          MetadataConstraints.add_all_constr 
+            (n,from,where) concl_card full_card diff in
+              (* join with the constraints over the type of the constant *)
+        let where = 
+          (sprintf "table0.h_occurrence = table%d.source" n)::where in
+        let where = 
+          sprintf "table0.h_depth - table%d.h_depth = %d" 
+            n (depth - depth')::where
+        in
+        let (m,from,where) =
+          List.fold_left 
+            (MetadataConstraints.add_constraint ~start:n)
+            (n,from,where) constraints_for_dummy_type in
+        Constr.exec ~dbd (m,from,where)
+