]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/metadata/metadataExtractor.ml
aded prifiler factory
[helm.git] / helm / ocaml / metadata / metadataExtractor.ml
1 (* Copyright (C) 2004, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://helm.cs.unibo.it/
24  *)
25
26 open Printf
27
28 open MetadataTypes
29
30 let is_main_pos = function
31   | `MainConclusion _
32   | `MainHypothesis _ -> true
33   | _ -> false
34
35 let main_pos (pos: position): main_position =
36   match pos with
37   | `MainConclusion depth -> `MainConclusion depth
38   | `MainHypothesis depth -> `MainHypothesis depth
39   | _ -> assert false
40
41 let next_pos = function
42   | `MainConclusion _ -> `InConclusion
43   | `MainHypothesis _ -> `InHypothesis
44   | pos -> pos
45
46 let string_of_uri = UriManager.string_of_uri
47
48 module OrderedMetadata =
49   struct
50     type t = MetadataTypes.metadata
51     let compare m1 m2 = (* ignore universes in Cic.Type sort *)
52       match (m1, m2) with
53       | `Sort (Cic.Type _, pos1), `Sort (Cic.Type _, pos2) ->
54           Pervasives.compare pos1 pos2
55       | _ -> Pervasives.compare m1 m2
56   end
57
58 module MetadataSet = Set.Make (OrderedMetadata)
59 module UriManagerSet = UriManager.UriSet
60
61 module S = MetadataSet
62
63 let unopt = function Some x -> x | None -> assert false
64
65 let incr_depth = function
66   | `MainConclusion (Some (Eq depth)) -> `MainConclusion (Some (Eq (depth + 1)))
67   | `MainHypothesis (Some (Eq depth)) -> `MainHypothesis (Some (Eq (depth + 1)))
68   | _ -> assert false
69
70 let var_has_body uri =
71   match CicEnvironment.get_obj CicUniv.empty_ugraph uri with
72   | Cic.Variable (_, Some body, _, _, _), _ -> true
73   | _ -> false
74
75 let string_of_uriref s =
76  UriManager.uri_of_string (UriManager.string_of_uriref s)
77
78 let compute_term pos term =
79   let rec aux (pos: position) set = function
80     | Cic.Var (uri, subst) when var_has_body uri ->
81         (* handles variables with body as constants *)
82         aux pos set (Cic.Const (uri, subst))
83     | Cic.Rel _
84     | Cic.Var _ ->
85         if is_main_pos pos then
86           S.add (`Rel (main_pos pos)) set
87         else
88           set
89     | Cic.Meta (_, local_context) ->
90         List.fold_left
91           (fun set context ->
92             match context with
93             | None -> set
94             | Some term -> aux (next_pos pos) set term)
95           set
96           local_context
97     | Cic.Sort sort ->
98         if is_main_pos pos then
99           S.add (`Sort (sort, main_pos pos)) set
100         else
101           set
102     | Cic.Implicit _ -> assert false
103     | Cic.Cast (term, ty) ->
104         (* TODO consider also ty? *)
105         aux pos set term
106     | Cic.Prod (_, source, target) ->
107         (match pos with
108         | `MainConclusion _ ->
109             let set = aux (`MainHypothesis (Some (Eq 0))) set source in
110             aux (incr_depth pos) set target
111         | `MainHypothesis _ ->
112             let set = aux `InHypothesis set source in
113             aux (incr_depth pos) set target
114         | `InConclusion
115         | `InHypothesis
116         | `InBody ->
117             let set = aux pos set source in
118             aux pos set target)
119     | Cic.Lambda (_, source, target) ->
120         (*assert (not (is_main_pos pos));*)
121         let set = aux (next_pos pos) set source in
122         aux (next_pos pos) set target
123     | Cic.LetIn (_, term, target) ->
124         if is_main_pos pos then
125           aux pos set (CicSubstitution.subst term target)
126         else
127           let set = aux pos set term in
128           aux pos set target
129     | Cic.Appl [] -> assert false
130     | Cic.Appl (hd :: tl) ->
131         let set = aux pos set hd in
132         List.fold_left
133           (fun set term -> aux (next_pos pos) set term)
134           set tl
135     | Cic.Const (uri, subst) ->
136         let set = S.add (`Obj (uri, pos)) set in
137         List.fold_left
138           (fun set (_, term) -> aux (next_pos pos) set term)
139           set subst
140     | Cic.MutInd (uri, typeno, subst) ->
141         let uri = string_of_uriref (uri, [typeno]) in
142         let set = S.add (`Obj (uri, pos)) set in
143         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
144           set subst
145     | Cic.MutConstruct (uri, typeno, consno, subst) ->
146         let uri = string_of_uriref (uri, [typeno; consno]) in
147         let set = S.add (`Obj (uri, pos)) set in
148         List.fold_left (fun set (_, term) -> aux (next_pos pos) set term)
149           set subst
150     | Cic.MutCase (uri, _, outtype, term, pats) ->
151         let pos = next_pos pos in
152         let set = aux pos set term in
153         let set = aux pos set outtype in
154         List.fold_left (fun set term -> aux pos set term) set pats
155     | Cic.Fix (_, funs) ->
156         let pos = next_pos pos in
157         List.fold_left
158           (fun set (_, _, ty, body) ->
159             let set = aux pos set ty in
160             aux pos set body)
161           set funs
162     | Cic.CoFix (_, funs) ->
163         let pos = next_pos pos in
164         List.fold_left
165           (fun set (_, ty, body) ->
166             let set = aux pos set ty in
167             aux pos set body)
168           set funs
169   in
170   aux pos S.empty term
171
172 module OrderedInt =
173 struct
174   type t = int
175   let compare = Pervasives.compare
176 end
177
178 module IntSet = Set.Make (OrderedInt)
179
180 let compute_metas term =
181   let rec aux in_hyp ((concl_metas, hyp_metas) as acc) cic =
182     match cic with
183     | Cic.Rel _
184     | Cic.Sort _
185     | Cic.Var _ -> acc
186     | Cic.Meta (no, local_context) ->
187         let acc =
188           if in_hyp then
189             (concl_metas, IntSet.add no hyp_metas)
190           else
191             (IntSet.add no concl_metas, hyp_metas)
192         in
193         List.fold_left
194           (fun set context ->
195             match context with
196             | None -> set
197             | Some term -> aux in_hyp set term)
198           acc
199           local_context
200     | Cic.Implicit _ -> assert false
201     | Cic.Cast (term, ty) ->
202         (* TODO consider also ty? *)
203         aux in_hyp acc term
204     | Cic.Prod (_, source, target) ->
205         if in_hyp then
206           let acc = aux in_hyp acc source in
207           aux in_hyp acc target
208         else
209           let acc = aux true acc source in
210           aux in_hyp acc target
211     | Cic.Lambda (_, source, target) ->
212         let acc = aux in_hyp acc source in
213         aux in_hyp acc target
214     | Cic.LetIn (_, term, target) ->
215         aux in_hyp acc (CicSubstitution.subst term target)
216     | Cic.Appl [] -> assert false
217     | Cic.Appl (hd :: tl) ->
218         let acc = aux in_hyp acc hd in
219         List.fold_left (fun acc term -> aux in_hyp acc term) acc tl
220     | Cic.Const (_, subst)
221     | Cic.MutInd (_, _, subst)
222     | Cic.MutConstruct (_, _, _, subst) ->
223         List.fold_left (fun acc (_, term) -> aux in_hyp acc term) acc subst
224     | Cic.MutCase (uri, _, outtype, term, pats) ->
225         let acc = aux in_hyp acc term in
226         let acc = aux in_hyp acc outtype in
227         List.fold_left (fun acc term -> aux in_hyp acc term) acc pats
228     | Cic.Fix (_, funs) ->
229         List.fold_left
230           (fun acc (_, _, ty, body) ->
231             let acc = aux in_hyp acc ty in
232             aux in_hyp acc body)
233           acc funs
234     | Cic.CoFix (_, funs) ->
235         List.fold_left
236           (fun acc (_, ty, body) ->
237             let acc = aux in_hyp acc ty in
238             aux in_hyp acc body)
239           acc funs
240   in
241   aux false (IntSet.empty, IntSet.empty) term
242
243   (** type of inductiveType *)
244 let compute_type pos uri typeno (name, _, ty, constructors) =
245   let consno = ref 0 in
246   let type_metadata =
247     (string_of_uriref (uri, [typeno]), name, (compute_term pos ty))
248   in
249   let constructors_metadata =
250     List.map
251       (fun (name, term) ->
252         incr consno;
253         let uri = string_of_uriref (uri, [typeno; !consno]) in
254         (uri, name, (compute_term pos term)))
255       constructors
256   in
257   type_metadata :: constructors_metadata
258
259 let compute_ind pos ~uri ~types =
260   let idx = ref ~-1 in
261   List.map (fun ty -> incr idx; compute_type pos uri !idx ty) types
262
263 let compute (pos:position) ~body ~ty = 
264   let type_metadata = compute_term pos ty in
265   let body_metadata =
266     match body with
267     | None -> S.empty
268     | Some body -> compute_term `InBody body
269   in
270   let uris =
271     S.fold
272       (fun metadata uris ->
273         match metadata with
274         | `Obj (uri, _) -> UriManagerSet.add uri uris
275         | _ -> uris)
276       type_metadata UriManagerSet.empty
277   in
278   S.union
279     (S.filter
280       (function
281         | `Obj (uri, _) when UriManagerSet.mem uri uris -> false
282         | _ -> true)
283       body_metadata)
284     type_metadata
285
286 let depth_offset params =
287   let non p x = not (p x) in
288   List.length (List.filter (non var_has_body) params)
289
290 let rec compute_var pos uri =
291   let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
292   match o with
293     | Cic.Variable (_, Some _, _, _, _) -> S.empty
294     | Cic.Variable (_, None, ty, params, _) ->
295         let var_metadata = 
296           List.fold_left
297             (fun metadata uri ->
298               S.union metadata (compute_var (next_pos pos) uri))
299             S.empty
300             params
301         in
302         (match pos with
303            | `MainHypothesis (Some (Eq 0)) -> 
304                let pos = `MainHypothesis (Some (Eq (depth_offset params))) in
305                let ty_metadata = compute_term pos ty in
306                S.union ty_metadata var_metadata
307            | `InHypothesis ->
308                let ty_metadata = compute_term pos ty in
309                S.union ty_metadata var_metadata
310            | _ -> assert false)
311     | _ -> assert false 
312
313 let compute_obj uri =
314   let o, _ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
315   match o with
316   | Cic.Variable (_, body, ty, params, _)
317   | Cic.Constant (_, body, ty, params, _) -> 
318       let pos = `MainConclusion (Some (Eq (depth_offset params))) in
319       let metadata = compute pos ~body ~ty in
320       let var_metadata = 
321         List.fold_left
322           (fun metadata uri ->
323             S.union metadata (compute_var (`MainHypothesis (Some (Eq 0))) uri))
324           S.empty
325           params
326       in
327       [ uri, 
328         UriManager.name_of_uri uri,
329         S.union metadata var_metadata ]
330   | Cic.InductiveDefinition (types, params, _, _) ->
331       let pos = `MainConclusion(Some (Eq (depth_offset params))) in
332       let metadata = compute_ind pos ~uri ~types in
333       let var_metadata = 
334         List.fold_left
335           (fun metadata uri ->
336             S.union metadata (compute_var (`MainHypothesis (Some (Eq 0))) uri))
337           S.empty params
338       in
339       List.fold_left
340         (fun acc m -> 
341           (List.map (fun (uri,name,md) -> (uri,name,S.union md var_metadata)) m)
342           @ acc)
343         [] metadata
344   | Cic.CurrentProof _ -> assert false    
345
346 let compute_obj uri = 
347   List.map (fun (u, n, md) -> (u, n, S.elements md)) (compute_obj uri)
348   
349 let compute ~body ~ty =
350   S.elements (compute (`MainConclusion (Some (Eq 0))) ~body ~ty)
351