]> matita.cs.unibo.it Git - helm.git/blob - components/cic_proof_checking/cicUnivUtils.ml
unified: some theorems on Lift started
[helm.git] / components / cic_proof_checking / cicUnivUtils.ml
1 (* Copyright (C) 2000, 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://cs.unibo.it/helm/.
24  *)
25
26 (*****************************************************************************)
27 (*                                                                           *)
28 (*                              PROJECT HELM                                 *)
29 (*                                                                           *)
30 (*                     Enrico Tassi <tassi@cs.unibo.it>                      *)
31 (*                                23/04/2004                                 *)
32 (*                                                                           *)
33 (* This module implements some useful function regarding univers graphs      *)
34 (*                                                                           *)
35 (*****************************************************************************)
36
37 (* $Id$ *)
38
39 module C = Cic
40 module H = UriManager.UriHashtbl 
41 let eq  = UriManager.eq
42
43 (* uri is the uri of the actual object that must be 'skipped' *)
44 let universes_of_obj uri t =
45   (* don't the same work twice *)
46   let visited_objs = H.create 31 in
47   let visited u = H.replace visited_objs u true in 
48   let is_not_visited u = not (H.mem visited_objs u) in 
49   visited uri;
50   (* the result *)
51   let results = ref [] in
52   let add_result l = results := l :: !results in
53   (* the iterators *)
54   let rec aux = function
55     | C.Const (u,exp_named_subst) when is_not_visited u ->
56         aux_uri u;
57         visited u;
58         C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
59     | C.Var (u,exp_named_subst) when is_not_visited u ->
60         aux_uri u;
61         visited u;
62         C.Var (u,  List.map (fun (x,t) -> x,aux t) exp_named_subst)
63     | C.Const (u,exp_named_subst) ->
64         C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
65     | C.Var (u,exp_named_subst) ->
66         C.Var (u,  List.map (fun (x,t) -> x,aux t) exp_named_subst)
67     | C.MutInd (u,x,exp_named_subst) when is_not_visited u ->
68         aux_uri u;
69         visited u;
70         C.MutInd (u,x,List.map (fun (x,t) -> x,aux t) exp_named_subst)
71     | C.MutInd (u,x,exp_named_subst) ->
72         C.MutInd (u,x, List.map (fun (x,t) -> x,aux t) exp_named_subst)
73     | C.MutConstruct (u,x,y,exp_named_subst) when is_not_visited u ->
74         aux_uri u;
75         visited u;
76         C.MutConstruct (u,x,y,List.map (fun (x,t) -> x,aux t) exp_named_subst)
77     | C.MutConstruct (x,y,z,exp_named_subst) ->
78         C.MutConstruct (x,y,z,List.map (fun (x,t) -> x,aux t) exp_named_subst)
79     | C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1)
80     | C.Sort (C.Type i) -> add_result [i]; 
81       C.Sort (C.Type (CicUniv.name_universe i uri))
82     | C.Rel _ 
83     | C.Sort _
84     | C.Implicit _ as x -> x
85     | C.Cast (v,t) -> C.Cast (aux v, aux t)
86     | C.Prod (b,s,t) -> C.Prod (b,aux s, aux t)
87     | C.Lambda (b,s,t) ->  C.Lambda (b,aux s, aux t)
88     | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t)
89     | C.Appl li -> C.Appl (List.map aux li)
90     | C.MutCase (uri,n1,ty,te,patterns) ->
91         C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns)
92     | C.Fix (no, funs) -> 
93         C.Fix(no, List.map (fun (x,y,b,c) -> (x,y,aux b,aux c)) funs)
94     | C.CoFix (no,funs) -> 
95         C.CoFix(no, List.map (fun (x,b,c) -> (x,aux b,aux c)) funs)
96   and aux_uri u =
97     if is_not_visited u then
98       let _, _, l = 
99         CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph u in 
100       add_result l
101   and aux_obj = function
102     | C.Constant (x,Some te,ty,v,y) ->
103         List.iter aux_uri v;
104         C.Constant (x,Some (aux te),aux ty,v,y)
105     | C.Variable (x,Some te,ty,v,y) -> 
106         List.iter aux_uri v;
107         C.Variable (x,Some (aux te),aux ty,v,y)
108     | C.Constant (x,None, ty, v,y) ->
109         List.iter aux_uri v;
110         C.Constant (x,None, aux ty, v,y)
111     | C.Variable (x,None, ty, v,y) ->
112         List.iter aux_uri v;
113         C.Variable (x,None, aux ty, v,y)
114     | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
115     | C.InductiveDefinition (l,v,x,y) -> 
116         List.iter aux_uri v; 
117         C.InductiveDefinition (
118           List.map
119            (fun (x,y,t,l') ->
120              (x,y,aux t, List.map (fun (x,t) -> x,aux t) l'))
121           l,v,x,y)  
122   in 
123   let o = aux_obj t in
124   List.flatten !results, o
125
126 let rec list_uniq = function 
127   | [] -> []
128   | h::[] -> [h]
129   | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl) 
130   | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl
131
132 let list_uniq l = 
133   list_uniq (List.fast_sort CicUniv.compare l)
134   
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 
146   in
147   ugraph, list_of_universes, obj
148
149 (*
150 let profiler = (HExtlib.profile "clean_and_fill").HExtlib.profile
151 let clean_and_fill u o g =
152   profiler (clean_and_fill u o) g
153 *)