1 (* Copyright (C) 2005, 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/
30 let nonvar uri = not (UriManager.uri_is_var uri)
32 (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
33 * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
34 let sqlpat_of_shellglob =
35 let star_RE, qmark_RE, percent_RE, uscore_RE =
36 Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_"
39 Pcre.replace ~rex:star_RE ~templ:"%"
40 (Pcre.replace ~rex:qmark_RE ~templ:"_"
41 (Pcre.replace ~rex:percent_RE ~templ:"\\%"
42 (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
45 let locate ~(dbd:HMysql.dbd) ?(vars = false) pat =
46 let sql_pat = sqlpat_of_shellglob pat in
48 sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
49 "SELECT source FROM %s WHERE value LIKE \"%s\"")
50 (MetadataTypes.name_tbl ()) sql_pat
51 MetadataTypes.library_name_tbl sql_pat
53 let result = HMysql.exec dbd query in
56 (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
58 let match_term ~(dbd:HMysql.dbd) ty =
59 (* debug_print (lazy (CicPp.ppterm ty)); *)
60 let metadata = MetadataExtractor.compute ~body:None ~ty in
62 MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty)
65 if CicUtil.is_meta_closed ty then
66 Some (MetadataConstraints.Eq constants_no), None
69 let (hyp_constants, concl_constants) =
70 (* collect different constants in hypotheses and conclusions *)
72 (fun ((hyp, concl) as acc) metadata ->
73 match (metadata: MetadataTypes.metadata) with
74 | `Sort _ | `Rel _ -> acc
75 | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
76 when not (List.mem uri concl) -> (hyp, uri :: concl)
77 | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
78 when not (List.mem uri hyp) -> (uri :: hyp, concl)
83 List.length hyp_constants - List.length concl_constants
85 let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
87 if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
88 Some (MetadataConstraints.Eq diff_no)
89 else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
90 Some (MetadataConstraints.Gt (diff_no - 1))
91 else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
92 Some (MetadataConstraints.Lt (diff_no + 1))
98 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
99 MetadataConstraints.at_least ~dbd ?full_card ?diff constraints
101 let fill_with_dummy_constants t =
102 let rec aux i types =
104 Cic.Lambda (n,s,t) ->
106 UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in
107 (aux (i+1) (s::types)
108 (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
111 let t,types = aux 0 [] t in
114 let instance ~dbd t =
115 let t',types = fill_with_dummy_constants t in
116 let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
120 (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))))
122 let no_concl = MetadataDb.count_distinct `Conclusion metadata in
123 let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
124 let no_full = MetadataDb.count_distinct `Statement metadata in
125 let is_dummy = function
126 | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy"
129 let rec look_for_dummy_main = function
131 | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_
132 when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") ->
133 let s = UriManager.string_of_uri s in
134 let len = String.length s in
135 let dummy_index = int_of_string (String.sub s 11 (len-15)) in
136 let dummy_type = List.nth types dummy_index in
138 | _::l -> look_for_dummy_main l
140 match (look_for_dummy_main metadata) with
142 (* debug_print (lazy "Caso None"); *)
143 (* no dummy in main position *)
144 let metadata = List.filter is_dummy metadata in
145 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
146 let concl_card = Some (MetadataConstraints.Eq no_concl) in
147 let full_card = Some (MetadataConstraints.Eq no_full) in
148 let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
149 MetadataConstraints.at_least ~dbd ?concl_card ?full_card ?diff
151 | Some (depth, dummy_type) ->
153 (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *)
154 (* a dummy in main position *)
155 let metadata_for_dummy_type =
156 MetadataExtractor.compute ~body:None ~ty:dummy_type in
157 (* Let us skip this for the moment
158 let main_of_dummy_type =
159 look_for_dummy_main metadata_for_dummy_type in *)
160 let metadata = List.filter is_dummy metadata in
161 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
162 let metadata_for_dummy_type =
163 List.filter is_dummy metadata_for_dummy_type in
164 let metadata_for_dummy_type, depth' =
165 (* depth' = the depth of the A -> A -> Prop *)
166 List.fold_left (fun (acc,dep) c ->
168 | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
169 (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
170 | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
171 (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
172 | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) ->
173 (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
174 | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type
176 let constraints_for_dummy_type =
177 List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
178 (* start with the dummy constant in main conlusion *)
179 let from = ["refObj as table0"] in
181 [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
182 sprintf "table0.h_depth >= %d" depth] in
185 (MetadataConstraints.add_constraint ~start:2)
186 (2,from,where) constraints in
187 let concl_card = Some (MetadataConstraints.Eq no_concl) in
188 let full_card = Some (MetadataConstraints.Eq no_full) in
189 let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
191 MetadataConstraints.add_all_constr
192 (n,from,where) concl_card full_card diff in
193 (* join with the constraints over the type of the constant *)
195 (sprintf "table0.h_occurrence = table%d.source" n)::where in
197 sprintf "table0.h_depth - table%d.h_depth = %d"
198 n (depth - depth')::where
202 (MetadataConstraints.add_constraint ~start:n)
203 (n,from,where) constraints_for_dummy_type in
204 MetadataConstraints.exec ~dbd (m,from,where)
208 [`Rel [`MainConclusion None];
209 `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]);
210 `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
211 `Obj (uri,[`InHypothesis]);
214 MetadataConstraints.at_least ~rating:`Hits ~dbd constraints