]> matita.cs.unibo.it Git - helm.git/blob - helm/ocaml/metadata/metadataExtractor.ml
added cast rendering (used in check window by gTopLevel/matita)
[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 StringSet = Set.Make (String)
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 depth) -> `MainConclusion (Some (depth + 1))
67   | `MainHypothesis (Some depth) -> `MainHypothesis (Some (depth + 1))
68   | _ -> assert false
69
70 let compute_term pos term =
71   let rec aux (pos: position) set = function
72     | Cic.Rel _ ->
73         if is_main_pos pos then
74           S.add (`Rel (main_pos pos)) set
75         else
76           set
77     | Cic.Var _ -> set
78     | Cic.Meta (_, local_context) ->
79         List.fold_left
80           (fun set context ->
81             match context with
82             | None -> set
83             | Some term -> aux pos set term)
84           set
85           local_context
86     | Cic.Sort sort ->
87         if is_main_pos pos then
88           S.add (`Sort (sort, main_pos pos)) set
89         else
90           set
91     | Cic.Implicit _ -> assert false
92     | Cic.Cast (term, ty) ->
93         (* TODO consider also ty? *)
94         aux pos set term
95     | Cic.Prod (_, source, target) ->
96         (match pos with
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
103         | `InConclusion
104         | `InHypothesis
105         | `InBody ->
106             let set = aux pos set source in
107             aux pos set target)
108     | Cic.Lambda (_, source, target) ->
109         assert (not (is_main_pos pos));
110         let set = aux pos set source in
111         aux pos set target
112     | Cic.LetIn (_, term, target) ->
113         if is_main_pos pos then
114           aux pos set (CicSubstitution.subst term target)
115         else
116           let set = aux pos set term in
117           aux pos set target
118     | Cic.Appl [] -> assert false
119     | Cic.Appl (hd :: tl) ->
120         let set = aux pos set hd in
121         List.fold_left
122           (fun set term -> aux (next_pos pos) set term)
123           set tl
124     | Cic.Const (uri, subst) ->
125         let set = S.add (`Obj (string_of_uri uri, pos)) set in
126         List.fold_left
127           (fun set (_, term) -> aux (next_pos pos) set term)
128           set subst
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)
133           set subst
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)
138           set subst
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
146         List.fold_left
147           (fun set (_, _, ty, body) ->
148             let set = aux pos set ty in
149             aux pos set body)
150           set funs
151     | Cic.CoFix (_, funs) ->
152         let pos = next_pos pos in
153         List.fold_left
154           (fun set (_, ty, body) ->
155             let set = aux pos set ty in
156             aux pos set body)
157           set funs
158   in
159   aux pos S.empty term
160
161 let compute_type uri typeno (name, _, ty, constructors) =
162   let consno = ref 0 in
163   let type_metadata =
164     (UriManager.string_of_uriref (uri, [typeno]), name,
165     S.elements (compute_term (`MainConclusion (Some 0)) ty))
166   in
167   let constructors_metadata =
168     List.map
169       (fun (name, term) ->
170         incr consno;
171         let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
172         (uri, name, S.elements (compute_term (`MainConclusion (Some 0)) term)))
173       constructors
174   in
175   type_metadata :: constructors_metadata
176
177 let compute_ind ~uri ~types =
178   let idx = ref ~-1 in
179   List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types)
180
181 let compute ~body ~ty =
182   let type_metadata = compute_term (`MainConclusion (Some 0)) ty in
183   let body_metadata =
184     match body with
185     | None -> S.empty
186     | Some body -> compute_term `InBody body
187   in
188   let uris =
189     S.fold
190       (fun metadata uris ->
191         match metadata with
192         | `Obj (uri, _) -> StringSet.add uri uris
193         | _ -> uris)
194       type_metadata StringSet.empty
195   in
196   S.elements 
197     (S.union
198       (S.filter
199         (function
200           | `Obj (uri, _) when StringSet.mem uri uris -> false
201           | _ -> true)
202         body_metadata)
203       type_metadata)
204
205 let compute_term start_pos term = S.elements (compute_term start_pos term)
206