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 *)