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) when is_not_visited u ->
56 C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
57 | C.Var (u,exp_named_subst) when is_not_visited u ->
60 C.Var (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
61 | C.Const (u,exp_named_subst) ->
62 C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
63 | C.Var (u,exp_named_subst) ->
64 C.Var (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
65 | C.MutInd (u,x,exp_named_subst) when is_not_visited u ->
68 C.MutInd (u,x,List.map (fun (x,t) -> x,aux t) exp_named_subst)
69 | C.MutInd (u,x,exp_named_subst) ->
70 C.MutInd (u,x, List.map (fun (x,t) -> x,aux t) exp_named_subst)
71 | C.MutConstruct (u,x,y,exp_named_subst) when is_not_visited u ->
74 C.MutConstruct (u,x,y,List.map (fun (x,t) -> x,aux t) exp_named_subst)
75 | C.MutConstruct (x,y,z,exp_named_subst) ->
76 C.MutConstruct (x,y,z,List.map (fun (x,t) -> x,aux t) exp_named_subst)
77 | C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1)
78 | C.Sort (C.Type i) -> add_result [i];
79 C.Sort (C.Type (CicUniv.name_universe i uri))
82 | C.Implicit _ as x -> x
83 | C.Cast (v,t) -> C.Cast (aux v, aux t)
84 | C.Prod (b,s,t) -> C.Prod (b,aux s, aux t)
85 | C.Lambda (b,s,t) -> C.Lambda (b,aux s, aux t)
86 | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t)
87 | C.Appl li -> C.Appl (List.map aux li)
88 | C.MutCase (uri,n1,ty,te,patterns) ->
89 C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns)
91 C.Fix(no, List.map (fun (x,y,b,c) -> (x,y,aux b,aux c)) funs)
92 | C.CoFix (no,funs) ->
93 C.CoFix(no, List.map (fun (x,b,c) -> (x,aux b,aux c)) funs)
95 if is_not_visited u then
97 CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph u in
99 and aux_obj = function
100 | C.Constant (x,Some te,ty,v,y) ->
102 C.Constant (x,Some (aux te),aux ty,v,y)
103 | C.Variable (x,Some te,ty,v,y) ->
105 C.Variable (x,Some (aux te),aux ty,v,y)
106 | C.Constant (x,None, ty, v,y) ->
108 C.Constant (x,None, aux ty, v,y)
109 | C.Variable (x,None, ty, v,y) ->
111 C.Variable (x,None, aux ty, v,y)
112 | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
113 | C.InductiveDefinition (l,v,x,y) ->
115 C.InductiveDefinition (
118 (x,y,aux t, List.map (fun (x,t) -> x,aux t) l'))
122 List.flatten !results, o
124 let rec list_uniq = function
127 | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl)
128 | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
131 list_uniq (List.fast_sort CicUniv.compare l)
133 let profiler = (HExtlib.profile "clean_and_fill").HExtlib.profile
135 let clean_and_fill uri obj ugraph =
136 (* universes of obj fills the universes of the obj with the right uri *)
137 let list_of_universes, obj = universes_of_obj uri obj in
138 let list_of_universes = list_uniq list_of_universes in
139 (* CicUniv.print_ugraph ugraph;*)
140 (* List.iter (fun u -> prerr_endline (CicUniv.string_of_universe u))*)
141 (* list_of_universes;*)
142 let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
143 (* CicUniv.print_ugraph ugraph;*)
144 let ugraph, list_of_universes =
145 CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri
147 ugraph, list_of_universes, obj
149 let clean_and_fill u o g =
150 profiler (clean_and_fill u o) g