1 (* Copyright (C) 2004, HELM Team.
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.
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.
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.
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,
22 * For details, see the HELM World-Wide-Web page,
23 * http://helm.cs.unibo.it/
28 module Constr = MetadataConstraints
31 let len = String.length s in
32 let suffix = String.sub s (len-4) 4 in
35 let locate ~(dbh:Dbi.connection) ?(vars = false) name =
37 dbh#prepare (sprintf "SELECT source FROM %s WHERE value = \"%s\""
38 MetadataTypes.name_tbl name)
42 (List.map (function [`String s] -> s | _ -> assert false)
45 let match_term ~(dbh:Dbi.connection) ty =
46 let metadata = MetadataExtractor.compute ~body:None ~ty in
48 MetadataConstraints.StringSet.cardinal (MetadataConstraints.constants_of ty)
50 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
51 Constr.at_least ~dbh ~full_card:(MetadataConstraints.Eq constants_no)
54 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
56 let signature_of_hypothesis context =
61 | Some (_, Cic.Decl t)
62 | Some (_, Cic.Def (t, _)) ->
63 Constr.StringSet.union set (Constr.constants_of t))
64 Constr.StringSet.empty context
67 let set1 = List.fold_right Constr.StringSet.add l1 Constr.StringSet.empty in
68 let set2 = List.fold_right Constr.StringSet.add l2 Constr.StringSet.empty in
69 Constr.StringSet.elements (Constr.StringSet.inter set1 set2)
71 let filter_uris_forward ~dbh (main, constants) uris =
75 | Some (main, types) -> main :: types
78 List.fold_right Constr.StringSet.add main_uris constants
80 List.filter (Constr.at_most ~dbh ~where:`Statement full_signature) uris
82 let filter_uris_backward ~dbh signature uris =
84 List.map snd (MetadataConstraints.sigmatch ~dbh ~where:`Statement signature)
86 intersect uris siguris
88 let compare_goal_list proof goal1 goal2 =
89 let _,metasenv,_,_ = proof in
90 let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
91 let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
92 let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
93 let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
95 if CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
99 if CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
104 let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
105 let (_, metasenv, _, _) = proof in
106 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
107 let (uris, (main, sig_constants)) =
109 | Some signature -> (Constr.sigmatch ~dbh signature, signature)
110 | None -> (Constr.cmatch' ~dbh ty, Constr.signature_of ty)
112 let uris = List.filter nonvar (List.map snd uris) in
113 let types_constants =
115 | None -> Constr.StringSet.empty
116 | Some (main, types) ->
117 List.fold_right Constr.StringSet.add (main :: types)
118 Constr.StringSet.empty
121 Constr.StringSet.diff (signature_of_hypothesis context) types_constants
123 let other_constants = Constr.StringSet.union sig_constants hyp_constants in
125 let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
126 if ((List.length uris < pow) or (pow <= 0))
128 prerr_endline "MetadataQuery: large sig, falling back to old method";
129 filter_uris_forward ~dbh (main, other_constants) uris
131 filter_uris_backward ~dbh (main, other_constants) uris
133 prerr_endline "URIS";
134 List.iter prerr_endline uris;
135 let rec aux = function
140 let (proof, goal_list) =
141 ProofEngineTypes.apply_tactic
142 (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
146 List.stable_sort (compare_goal_list proof) goal_list
148 Some (uri, (proof, goal_list))
149 with ProofEngineTypes.Fail _ -> None
154 prerr_endline ("HO APPLICATO " ^ uri);
161 [`Rel [`MainConclusion None];
162 `Sort (Cic.Prop,[`MainHypothesis (Some 1)]);
163 `Obj (uri,[`MainHypothesis (Some 0)]);
164 `Obj (uri,[`InHypothesis]);
167 MetadataConstraints.at_least ~dbh constraints