helm/ocaml/tactics/metadataQuery.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 module Constr = MetadataConstraints
  29
  30 let locate ~(dbh:Dbi.connection) name =
  31   let query =
  32     dbh#prepare (sprintf "SELECT value FROM %s WHERE source = \"%s\""
  33       MetadataTypes.name_tbl name)
  34   in
  35   query#execute [];
  36   List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
  37
  38 let match_term ~(dbh:Dbi.connection) ty =
  39   let metadata = MetadataExtractor.compute ~body:None ~ty in
  40   Constr.at_least ~dbh metadata
  41
  42 let nonvar (_, s) =
  43   let len = String.length s in
  44   let suffix = String.sub s (len-4) 4 in
  45   not (suffix  = ".var")
  46
  47 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
  48
  49 let signature_of_hypothesis context =
  50   List.fold_left
  51     (fun set hyp ->
  52       match hyp with
  53       | None -> set
  54       | Some (_, Cic.Decl t)
  55       | Some (_, Cic.Def (t, _)) ->
  56           Constr.StringSet.union set (Constr.constants_of t))
  57     Constr.StringSet.empty context
  58
  59 let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
  60   let (_, metasenv, _, _) = proof in
  61   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
  62   let (uris, (main, sig_constants)) =
  63     match signature with
  64     | Some signature -> (Constr.sigmatch ~dbh signature, signature)
  65     | None -> (Constr.cmatch' ~dbh ty, Constr.signature_of ty)
  66   in
  67   let uris = List.filter nonvar uris in
  68 (*
  69   let concl_constants =
  70     match main with
  71     | None -> sig_constants
  72     | Some (main, types) ->
  73         List.fold_right Constr.StringSet.add sig_constants (main :: types)
  74   in
  75 *)
  76   let types_constants =
  77     match main with
  78     | None -> Constr.StringSet.empty
  79     | Some (main, types) ->
  80         List.fold_right Constr.StringSet.add (main :: types)
  81           Constr.StringSet.empty
  82   in
  83   let hyp_constants =
  84     Constr.StringSet.diff (signature_of_hypothesis context) types_constants
  85   in
  86   let other_constants = Constr.StringSet.union sig_constants hyp_constants in
  87   let uris =
  88     if (List.length uris < 2 ** (Constr.StringSet.cardinal other_constants))
  89     then begin
  90       prerr_endline
  91         "MetadataQuery: large signature, falling back to old method";
  92       List.filter (Filter_auto.filter_new_constants ~dbh all_constants main)
  93         uris
  94     end else
  95       Filter_auto.filter_uris ~dbh all_constants uris main
  96   in
  97   List.map
  98     (fun uri ->
  99       (uri,
 100        ProofEngineTypes.apply_tactic
 101         (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
 102         status))
 103