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