1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
26 (*****************************************************************************)
30 (* Enrico Tassi <tassi@cs.unibo.it> *)
33 (* This module implements some useful function regarding univers graphs *)
35 (*****************************************************************************)
38 module H = UriManager.UriHashtbl
39 let eq = UriManager.eq
41 (* uri is the uri of the actual object that must be 'skipped' *)
42 let universes_of_obj uri t =
43 (* don't the same work twice *)
44 let visited_objs = H.create 31 in
45 let visited u = H.replace visited_objs u true in
46 let is_not_visited u = not (H.mem visited_objs u) in
49 let results = ref [] in
50 let add_result l = results := l :: !results in
52 let rec aux = function
53 | C.Const (u,exp_named_subst)
54 | C.Var (u,exp_named_subst) when is_not_visited u ->
57 List.iter (fun (_,t) -> aux t) exp_named_subst
58 | C.Const (u,exp_named_subst)
59 | C.Var (u,exp_named_subst) ->
60 List.iter (fun (_,t) -> aux t) exp_named_subst
61 | C.MutInd (u,_,exp_named_subst) when is_not_visited u ->
63 (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
64 | C.InductiveDefinition (l,_,_,_) ->
68 List.iter (fun (_,t) -> aux t) l')
71 List.iter (fun (_,t) -> aux t) exp_named_subst
72 | C.MutInd (_,_,exp_named_subst) ->
73 List.iter (fun (_,t) -> aux t) exp_named_subst
74 | C.MutConstruct (u,_,_,exp_named_subst) when is_not_visited u ->
76 (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
77 | C.InductiveDefinition (l,_,_,_) ->
81 List.iter (fun (_,t) -> aux t) l')
84 List.iter (fun (_,t) -> aux t) exp_named_subst
85 | C.MutConstruct (_,_,_,exp_named_subst) ->
86 List.iter (fun (_,t) -> aux t) exp_named_subst
88 List.iter (fun t -> match t with Some t' -> aux t' | _ -> ()) l1
89 | C.Sort ( C.Type i) -> add_result [i]
93 | C.Cast (v,t) -> aux v; aux t
96 | C.LetIn (b,s,t) -> aux s; aux t
97 | C.Appl li -> List.iter (fun t -> aux t) li
98 | C.MutCase (uri,n1,ty,te,patterns) ->
99 aux ty; aux te; (List.iter (fun t -> aux t) patterns)
100 | C.Fix (no, funs) -> List.iter (fun (_,_,b,c) -> aux b; aux c) funs
101 | C.CoFix (no,funs) -> List.iter (fun (_,b,c) -> aux b; aux c) funs
104 if is_not_visited u then
106 CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph u in
108 and aux_obj = function
109 | C.Constant (_,Some te,ty,v,_)
110 | C.Variable (_,Some te,ty,v,_) ->
114 | C.Constant (_,None, ty, v,_)
115 | C.Variable (_,None, ty, v,_) ->
118 | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
119 | C.InductiveDefinition (l,v,_,_) ->
123 List.iter (fun (_,t) -> aux t) l')
128 List.flatten !results
130 let rec list_uniq = function
133 | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl)
134 | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
137 list_uniq (List.fast_sort CicUniv.compare l)
139 let clean_and_fill uri obj ugraph =
140 let list_of_universes = universes_of_obj uri obj in
141 let list_of_universes = list_uniq list_of_universes in
142 let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
143 let ugraph, list_of_universes =
144 CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri
146 ugraph, list_of_universes