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
66 let intersect uris siguris =
67 let set1 = List.fold_right Constr.StringSet.add uris Constr.StringSet.empty in
69 List.fold_right Constr.StringSet.add siguris Constr.StringSet.empty
71 let inter = Constr.StringSet.inter set1 set2 in
72 List.filter (fun s -> Constr.StringSet.mem s inter) uris
74 let filter_uris_forward ~dbh (main, constants) uris =
78 | Some (main, types) -> main :: types
81 List.fold_right Constr.StringSet.add main_uris constants
83 List.filter (Constr.at_most ~dbh ~where:`Statement full_signature) uris
85 let filter_uris_backward ~dbh signature uris =
87 List.map snd (MetadataConstraints.sigmatch ~dbh ~where:`Statement signature)
89 intersect uris siguris
91 let compare_goal_list proof goal1 goal2 =
92 let _,metasenv,_,_ = proof in
93 let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
94 let (_, ey2, ty2) = CicUtil.lookup_meta goal2 metasenv in
95 let ty_sort1 = CicTypeChecker.type_of_aux' metasenv ey1 ty1 in
96 let ty_sort2 = CicTypeChecker.type_of_aux' metasenv ey2 ty2 in
98 if CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1 then 0
102 if CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2 then 0
107 let hint ~(dbh:Dbi.connection) ?signature ((proof, goal) as status) =
108 let (_, metasenv, _, _) = proof in
109 let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
110 let (uris, (main, sig_constants)) =
112 | Some signature -> (Constr.sigmatch ~dbh signature, signature)
113 | None -> (Constr.cmatch' ~dbh ty, Constr.signature_of ty)
115 let uris = List.filter nonvar (List.map snd uris) in
116 let types_constants =
118 | None -> Constr.StringSet.empty
119 | Some (main, types) ->
120 List.fold_right Constr.StringSet.add (main :: types)
121 Constr.StringSet.empty
124 Constr.StringSet.diff (signature_of_hypothesis context) types_constants
126 let other_constants = Constr.StringSet.union sig_constants hyp_constants in
128 let pow = 2 ** (Constr.StringSet.cardinal other_constants) in
129 if ((List.length uris < pow) or (pow <= 0))
131 prerr_endline "MetadataQuery: large sig, falling back to old method";
132 filter_uris_forward ~dbh (main, other_constants) uris
134 filter_uris_backward ~dbh (main, other_constants) uris
136 let rec aux = function
141 let (proof, goal_list) =
142 ProofEngineTypes.apply_tactic
143 (PrimitiveTactics.apply_tac ~term:(CicUtil.term_of_uri uri))
147 List.stable_sort (compare_goal_list proof) goal_list
149 Some (uri, (proof, goal_list))
150 with ProofEngineTypes.Fail _ -> None
155 prerr_endline ("HO APPLICATO " ^ uri);
159 (fun (_, (_, goals1)) (_, (_, goals2)) ->
160 Pervasives.compare (List.length goals1) (List.length goals2))
165 [`Rel [`MainConclusion None];
166 `Sort (Cic.Prop,[`MainHypothesis (Some 1)]);
167 `Obj (uri,[`MainHypothesis (Some 0)]);
168 `Obj (uri,[`InHypothesis]);
171 MetadataConstraints.at_least ~dbh constraints