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/
30 let is_main_pos = function
32 | `MainHypothesis _ -> true
35 let main_pos (pos: position): main_position =
37 | `MainConclusion depth -> `MainConclusion depth
38 | `MainHypothesis depth -> `MainHypothesis depth
41 let next_pos = function
42 | `MainConclusion _ -> `InConclusion
43 | `MainHypothesis _ -> `InHypothesis
46 let string_of_uri = UriManager.string_of_uri
48 module OrderedMetadata =
50 type t = MetadataTypes.metadata
51 let compare m1 m2 = (* ignore universes in Cic.Type sort *)
53 | `Sort (Cic.Type _, pos1), `Sort (Cic.Type _, pos2) ->
54 Pervasives.compare pos1 pos2
55 | _ -> Pervasives.compare m1 m2
58 module MetadataSet = Set.Make (OrderedMetadata)
59 module StringSet = Set.Make (String)
61 module S = MetadataSet
63 let unopt = function Some x -> x | None -> assert false
65 let incr_depth = function
66 | `MainConclusion (Some depth) -> `MainConclusion (Some (depth + 1))
67 | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1))
70 let compute_term pos term =
71 let rec aux (pos: position) set = function
74 if is_main_pos pos then
75 S.add (`Rel (main_pos pos)) set
78 | Cic.Meta (_, local_context) ->
83 | Some term -> aux (next_pos pos) set term)
87 if is_main_pos pos then
88 S.add (`Sort (sort, main_pos pos)) set
91 | Cic.Implicit _ -> assert false
92 | Cic.Cast (term, ty) ->
93 (* TODO consider also ty? *)
95 | Cic.Prod (_, source, target) ->
97 | `MainConclusion _ ->
98 let set = aux (`MainHypothesis (Some 0)) set source in
99 aux (incr_depth pos) set target
100 | `MainHypothesis _ ->
101 let set = aux `InHypothesis set source in
102 aux (incr_depth pos) set target
106 let set = aux pos set source in
108 | Cic.Lambda (_, source, target) ->
109 (*assert (not (is_main_pos pos));*)
110 let set = aux (next_pos pos) set source in
111 aux (next_pos pos) set target
112 | Cic.LetIn (_, term, target) ->
113 if is_main_pos pos then
114 aux pos set (CicSubstitution.subst term target)
116 let set = aux pos set term in
118 | Cic.Appl [] -> assert false
119 | Cic.Appl (hd :: tl) ->
120 let set = aux pos set hd in
122 (fun set term -> aux (next_pos pos) set term)
124 | Cic.Const (uri, subst) ->
125 let set = S.add (`Obj (string_of_uri uri, pos)) set in
127 (fun set (_, term) -> aux (next_pos pos) set term)
129 | Cic.MutInd (uri, typeno, subst) ->
130 let uri = UriManager.string_of_uriref (uri, [typeno]) in
131 let set = S.add (`Obj (uri, pos)) set in
132 List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
134 | Cic.MutConstruct (uri, typeno, consno, subst) ->
135 let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
136 let set = S.add (`Obj (uri, pos)) set in
137 List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
139 | Cic.MutCase (uri, _, outtype, term, pats) ->
140 let pos = next_pos pos in
141 let set = aux pos set term in
142 let set = aux pos set outtype in
143 List.fold_left (fun set term -> aux pos set term) set pats
144 | Cic.Fix (_, funs) ->
145 let pos = next_pos pos in
147 (fun set (_, _, ty, body) ->
148 let set = aux pos set ty in
151 | Cic.CoFix (_, funs) ->
152 let pos = next_pos pos in
154 (fun set (_, ty, body) ->
155 let set = aux pos set ty in
164 let compare = Pervasives.compare
167 module IntSet = Set.Make (OrderedInt)
169 let compute_metas term =
170 let rec aux in_hyp ((concl_metas, hyp_metas) as acc) cic =
175 | Cic.Meta (no, local_context) ->
178 (concl_metas, IntSet.add no hyp_metas)
180 (IntSet.add no concl_metas, hyp_metas)
186 | Some term -> aux in_hyp set term)
189 | Cic.Implicit _ -> assert false
190 | Cic.Cast (term, ty) ->
191 (* TODO consider also ty? *)
193 | Cic.Prod (_, source, target) ->
195 let acc = aux in_hyp acc source in
196 aux in_hyp acc target
198 let acc = aux true acc source in
199 aux in_hyp acc target
200 | Cic.Lambda (_, source, target) ->
201 let acc = aux in_hyp acc source in
202 aux in_hyp acc target
203 | Cic.LetIn (_, term, target) ->
204 aux in_hyp acc (CicSubstitution.subst term target)
205 | Cic.Appl [] -> assert false
206 | Cic.Appl (hd :: tl) ->
207 let acc = aux in_hyp acc hd in
208 List.fold_left (fun acc term -> aux in_hyp acc term) acc tl
209 | Cic.Const (_, subst)
210 | Cic.MutInd (_, _, subst)
211 | Cic.MutConstruct (_, _, _, subst) ->
212 List.fold_left (fun acc (_, term) -> aux in_hyp acc term) acc subst
213 | Cic.MutCase (uri, _, outtype, term, pats) ->
214 let acc = aux in_hyp acc term in
215 let acc = aux in_hyp acc outtype in
216 List.fold_left (fun acc term -> aux in_hyp acc term) acc pats
217 | Cic.Fix (_, funs) ->
219 (fun acc (_, _, ty, body) ->
220 let acc = aux in_hyp acc ty in
223 | Cic.CoFix (_, funs) ->
225 (fun acc (_, ty, body) ->
226 let acc = aux in_hyp acc ty in
230 aux false (IntSet.empty, IntSet.empty) term
232 (** type of inductiveType *)
233 let compute_type pos uri typeno (name, _, ty, constructors) =
234 let consno = ref 0 in
236 (UriManager.string_of_uriref (uri, [typeno]), name,
237 S.elements (compute_term pos ty))
239 let constructors_metadata =
243 let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
244 (uri, name, S.elements
245 (compute_term pos term)))
248 type_metadata :: constructors_metadata
250 let compute_ind pos ~uri ~types =
254 (fun ty -> incr idx; compute_type pos uri !idx ty) types)
256 let compute (pos:position) ~body ~ty =
257 let type_metadata = compute_term pos ty in
261 | Some body -> compute_term `InBody body
265 (fun metadata uris ->
267 | `Obj (uri, _) -> StringSet.add uri uris
269 type_metadata StringSet.empty
275 | `Obj (uri, _) when StringSet.mem uri uris -> false
280 let compute_term start_pos term = S.elements (compute_term start_pos term)
282 let rec compute_var pos uri =
283 let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
285 | Cic.Variable (_, body, ty, params, _) ->
286 let metadata_of_vars =
288 (List.map (compute_var (next_pos pos)) params) in
290 | `MainHypothesis (Some 0) ->
291 let pos = `MainHypothesis(Some (List.length params)) in
292 (compute pos ~body ~ty)@metadata_of_vars
294 (compute pos ~body ~ty)@metadata_of_vars
298 let compute_obj uri =
299 let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
301 | Cic.Variable (_, body, ty, params, _)
302 | Cic.Constant (_, body, ty, params, _) ->
303 let pos = `MainConclusion(Some (List.length params)) in
304 let metadata = compute pos ~body ~ty
306 let metadata_of_vars =
308 (List.map (compute_var (`MainHypothesis (Some 0))) params)
310 [UriManager.string_of_uri uri,
311 UriManager.name_of_uri uri,metadata @ metadata_of_vars]
312 | Cic.InductiveDefinition (types, params, _, _) ->
313 let pos = `MainConclusion(Some (List.length params)) in
314 let metadata_of_vars =
316 (List.map (compute_var (`MainHypothesis (Some 0))) params) in
317 let metadata = compute_ind pos ~uri ~types in
318 List.map (fun (uri,name,md) -> (uri,name,md@metadata_of_vars)) metadata
319 | Cic.CurrentProof _ -> assert false
322 let compute ~body ~ty = compute (`MainConclusion (Some 0)) ~body ~ty