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 -> `MainConclusion
38 | `MainHypothesis -> `MainHypothesis
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 _, p1, d1), `Sort (Cic.Type _, p2, d2) ->
54 Pervasives.compare (p1, d2) (p2, d2)
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 | None -> assert false
67 | Some x -> Some (x + 1)
69 let compute_term pos term =
70 let rec aux (pos: position) pi_depth set = function
72 if is_main_pos pos then
73 S.add (`Rel (main_pos pos, unopt pi_depth)) set
77 | Cic.Meta (_, local_context) ->
82 | Some term -> aux pos pi_depth set term)
86 if is_main_pos pos then
87 S.add (`Sort (sort, main_pos pos, unopt pi_depth)) set
90 | Cic.Implicit _ -> assert false
91 | Cic.Cast (term, ty) ->
92 (* TODO consider also ty? *)
93 aux pos pi_depth set term
94 | Cic.Prod (_, source, target) ->
97 let set = aux `MainHypothesis (Some 0) set source in
98 aux pos (incr_depth pi_depth) set target
100 let set = aux `InHypothesis None set source in
101 aux pos (incr_depth pi_depth) set target
105 let set = aux pos None set source in
106 aux pos None set target)
107 | Cic.Lambda (_, source, target) ->
108 assert (not (is_main_pos pos));
109 let set = aux pos None set source in
110 aux pos None set target
111 | Cic.LetIn (_, term, target) ->
112 if is_main_pos pos then
113 aux pos pi_depth set (CicSubstitution.subst term target)
115 let set = aux pos None set term in
116 aux pos None set target
117 | Cic.Appl [] -> assert false
118 | Cic.Appl (hd :: tl) ->
119 let set = aux pos pi_depth set hd in
121 (fun set term -> aux (next_pos pos) None set term)
123 | Cic.Const (uri, subst) ->
124 let set = S.add (`Obj (string_of_uri uri, pos, pi_depth)) set in
126 (fun set (_, term) -> aux (next_pos pos) None set term)
128 | Cic.MutInd (uri, typeno, subst) ->
129 let uri = UriManager.string_of_uriref (uri, [typeno]) in
130 let set = S.add (`Obj (uri, pos, pi_depth)) set in
131 List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term)
133 | Cic.MutConstruct (uri, typeno, consno, subst) ->
134 let uri = UriManager.string_of_uriref (uri, [typeno; consno]) in
135 let set = S.add (`Obj (uri, pos, pi_depth)) set in
136 List.fold_left (fun set (_, term) -> aux (next_pos pos) None set term)
138 | Cic.MutCase (uri, _, outtype, term, pats) ->
139 let pos = next_pos pos in
140 let set = aux pos None set term in
141 let set = aux pos None set outtype in
142 List.fold_left (fun set term -> aux pos None set term) set pats
143 | Cic.Fix (_, funs) ->
144 let pos = next_pos pos in
146 (fun set (_, _, ty, body) ->
147 let set = aux pos None set ty in
148 aux pos None set body)
150 | Cic.CoFix (_, funs) ->
151 let pos = next_pos pos in
153 (fun set (_, ty, body) ->
154 let set = aux pos None set ty in
155 aux pos None set body)
158 aux pos (Some 0) S.empty term
160 let compute_type uri typeno (name, _, ty, constructors) =
161 let consno = ref 0 in
163 (UriManager.string_of_uriref (uri, [typeno]), name,
164 S.elements (compute_term `MainConclusion ty))
166 let constructors_metadata =
170 let uri = UriManager.string_of_uriref (uri, [typeno; !consno]) in
171 (uri, name, S.elements (compute_term `MainConclusion term)))
174 type_metadata :: constructors_metadata
176 let compute_ind ~uri ~types =
178 List.concat (List.map (fun ty -> incr idx; compute_type uri !idx ty) types)
180 let compute ~body ~ty =
181 let type_metadata = compute_term `MainConclusion ty in
185 | Some body -> compute_term `InBody body
189 (fun metadata uris ->
191 | `Obj (uri, _, _) -> StringSet.add uri uris
193 type_metadata StringSet.empty
199 | `Obj (uri, _, _) when StringSet.mem uri uris -> false
204 let compute_term start_pos term = S.elements (compute_term start_pos term)