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/
28 let nonvar uri = not (UriManager.uri_is_var uri)
30 (** maps a shell like pattern (which uses '*' and '?') to a sql pattern for
31 * the "like" operator (which uses '%' and '_'). Does not support escaping. *)
32 let sqlpat_of_shellglob =
33 let star_RE, qmark_RE, percent_RE, uscore_RE =
34 Pcre.regexp "\\*", Pcre.regexp "\\?", Pcre.regexp "%", Pcre.regexp "_"
37 Pcre.replace ~rex:star_RE ~templ:"%"
38 (Pcre.replace ~rex:qmark_RE ~templ:"_"
39 (Pcre.replace ~rex:percent_RE ~templ:"\\%"
40 (Pcre.replace ~rex:uscore_RE ~templ:"\\_"
43 let locate ~(dbd:HMysql.dbd) ?(vars = false) pat =
44 let sql_pat = sqlpat_of_shellglob pat in
46 sprintf ("SELECT source FROM %s WHERE value LIKE \"%s\" UNION "^^
47 "SELECT source FROM %s WHERE value LIKE \"%s\"")
48 (MetadataTypes.name_tbl ()) sql_pat
49 MetadataTypes.library_name_tbl sql_pat
51 let result = HMysql.exec dbd query in
54 (fun cols -> match cols.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false))
56 let match_term ~(dbd:HMysql.dbd) ty =
57 (* debug_print (lazy (CicPp.ppterm ty)); *)
58 let metadata = MetadataExtractor.compute ~body:None ~ty in
60 MetadataConstraints.UriManagerSet.cardinal (MetadataConstraints.constants_of ty)
63 if CicUtil.is_meta_closed ty then
64 Some (MetadataConstraints.Eq constants_no), None
67 let (hyp_constants, concl_constants) =
68 (* collect different constants in hypotheses and conclusions *)
70 (fun ((hyp, concl) as acc) metadata ->
71 match (metadata: MetadataTypes.metadata) with
72 | `Sort _ | `Rel _ -> acc
73 | `Obj (uri, `InConclusion) | `Obj (uri, `MainConclusion _)
74 when not (List.mem uri concl) -> (hyp, uri :: concl)
75 | `Obj (uri, `InHypothesis) | `Obj (uri, `MainHypothesis _)
76 when not (List.mem uri hyp) -> (uri :: hyp, concl)
81 List.length hyp_constants - List.length concl_constants
83 let (concl_metas, hyp_metas) = MetadataExtractor.compute_metas ty in
85 if MetadataExtractor.IntSet.equal concl_metas hyp_metas then
86 Some (MetadataConstraints.Eq diff_no)
87 else if MetadataExtractor.IntSet.subset concl_metas hyp_metas then
88 Some (MetadataConstraints.Gt (diff_no - 1))
89 else if MetadataExtractor.IntSet.subset hyp_metas concl_metas then
90 Some (MetadataConstraints.Lt (diff_no + 1))
96 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
97 MetadataConstraints.at_least ~dbd ?full_card ?diff constraints
99 let fill_with_dummy_constants t =
100 let rec aux i types =
102 Cic.Lambda (n,s,t) ->
104 UriManager.uri_of_string ("cic:/dummy_"^(string_of_int i)^".con") in
105 (aux (i+1) (s::types)
106 (CicSubstitution.subst (Cic.Const(dummy_uri,[])) t))
109 let t,types = aux 0 [] t in
112 let instance ~dbd t =
113 let t',types = fill_with_dummy_constants t in
114 let metadata = MetadataExtractor.compute ~body:None ~ty:t' in
118 (lazy (MetadataPp.pp_constr (MetadataTypes.constr_of_metadata x))))
120 let no_concl = MetadataDb.count_distinct `Conclusion metadata in
121 let no_hyp = MetadataDb.count_distinct `Hypothesis metadata in
122 let no_full = MetadataDb.count_distinct `Statement metadata in
123 let is_dummy = function
124 | `Obj(s, _) -> (String.sub (UriManager.string_of_uri s) 0 10) <> "cic:/dummy"
127 let rec look_for_dummy_main = function
129 | `Obj(s,`MainConclusion (Some (MetadataTypes.Eq d)))::_
130 when (String.sub (UriManager.string_of_uri s) 0 10 = "cic:/dummy") ->
131 let s = UriManager.string_of_uri s in
132 let len = String.length s in
133 let dummy_index = int_of_string (String.sub s 11 (len-15)) in
134 let dummy_type = List.nth types dummy_index in
136 | _::l -> look_for_dummy_main l
138 match (look_for_dummy_main metadata) with
140 (* debug_print (lazy "Caso None"); *)
141 (* no dummy in main position *)
142 let metadata = List.filter is_dummy metadata in
143 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
144 let concl_card = Some (MetadataConstraints.Eq no_concl) in
145 let full_card = Some (MetadataConstraints.Eq no_full) in
146 let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
147 MetadataConstraints.at_least ~dbd ?concl_card ?full_card ?diff
149 | Some (depth, dummy_type) ->
151 (lazy (sprintf "Caso Some %d %s" depth (CicPp.ppterm dummy_type))); *)
152 (* a dummy in main position *)
153 let metadata_for_dummy_type =
154 MetadataExtractor.compute ~body:None ~ty:dummy_type in
155 (* Let us skip this for the moment
156 let main_of_dummy_type =
157 look_for_dummy_main metadata_for_dummy_type in *)
158 let metadata = List.filter is_dummy metadata in
159 let constraints = List.map MetadataTypes.constr_of_metadata metadata in
160 let metadata_for_dummy_type =
161 List.filter is_dummy metadata_for_dummy_type in
162 let metadata_for_dummy_type, depth' =
163 (* depth' = the depth of the A -> A -> Prop *)
164 List.fold_left (fun (acc,dep) c ->
166 | `Sort (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
167 (`Sort (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
168 | `Obj (s,`MainConclusion (Some (MetadataTypes.Eq i))) ->
169 (`Obj (s,`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
170 | `Rel (`MainConclusion (Some (MetadataTypes.Eq i))) ->
171 (`Rel (`MainConclusion (Some (MetadataTypes.Ge i))))::acc, i
172 | _ -> (c::acc,dep)) ([],0) metadata_for_dummy_type
174 let constraints_for_dummy_type =
175 List.map MetadataTypes.constr_of_metadata metadata_for_dummy_type in
176 (* start with the dummy constant in main conlusion *)
177 let from = ["refObj as table0"] in
179 [sprintf "table0.h_position = \"%s\"" MetadataTypes.mainconcl_pos;
180 sprintf "table0.h_depth >= %d" depth] in
183 (MetadataConstraints.add_constraint ~start:2)
184 (2,from,where) constraints in
185 let concl_card = Some (MetadataConstraints.Eq no_concl) in
186 let full_card = Some (MetadataConstraints.Eq no_full) in
187 let diff = Some (MetadataConstraints.Eq (no_hyp - no_concl)) in
189 MetadataConstraints.add_all_constr
190 (n,from,where) concl_card full_card diff in
191 (* join with the constraints over the type of the constant *)
193 (sprintf "table0.h_occurrence = table%d.source" n)::where in
195 sprintf "table0.h_depth - table%d.h_depth = %d"
196 n (depth - depth')::where
200 (MetadataConstraints.add_constraint ~start:n)
201 (n,from,where) constraints_for_dummy_type in
202 MetadataConstraints.exec ~dbd (m,from,where)
206 [`Rel [`MainConclusion None];
207 `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]);
208 `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
209 `Obj (uri,[`InHypothesis]);
212 MetadataConstraints.at_least ~rating:`Hits ~dbd constraints