helm/ocaml/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 module C = Cic
  38 module H = UriManager.UriHashtbl
  39 let eq  = UriManager.eq
  40
  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
  47   visited uri;
  48   (* the result *)
  49   let results = ref [] in
  50   let add_result l = results := l :: !results in
  51   (* the iterators *)
  52   let rec aux = function
  53     | C.Const (u,exp_named_subst)
  54     | C.Var (u,exp_named_subst) when is_not_visited u ->
  55         visited u;
  56         aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph 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 ->
  62         visited u;
  63         (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
  64         | C.InductiveDefinition (l,_,_,_) ->
  65              List.iter
  66                (fun (_,_,t,l') ->
  67                  aux t;
  68                  List.iter (fun (_,t) -> aux t) l')
  69              l
  70         | _ -> assert false);
  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 ->
  75         visited u;
  76         (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
  77            | C.InductiveDefinition (l,_,_,_) ->
  78                List.iter
  79                  (fun (_,_,t,l') ->
  80                    aux t;
  81                    List.iter (fun (_,t) -> aux t) l')
  82                  l
  83            | _ -> assert false);
  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
  87     | C.Meta (n,l1) ->
  88         List.iter (fun t -> match t with Some t' -> aux t' | _ -> ()) l1
  89     | C.Sort ( C.Type i) -> add_result i
  90     | C.Rel _
  91     | C.Sort _
  92     | C.Implicit _ -> ()
  93     | C.Cast (v,t) -> aux v; aux t
  94     | C.Prod (b,s,t)
  95     | C.Lambda (b,s,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
 102   and aux_obj = function
 103     | C.Constant (_,Some te,ty,v,_)
 104     | C.Variable (_,Some te,ty,v,_) ->
 105         aux te;
 106         aux ty;
 107         List.iter
 108           (fun u ->
 109             if is_not_visited u then
 110               (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
 111         v
 112     | C.Constant (_,None, ty, v,_)
 113     | C.Variable (_,None, ty, v,_) ->
 114         aux ty;
 115         List.iter
 116           (fun u ->
 117             if is_not_visited u then
 118               (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
 119         v
 120     | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
 121     | C.InductiveDefinition (l,v,_,_) ->
 122         List.iter
 123            (fun (_,_,t,l') ->
 124              aux t;
 125              List.iter (fun (_,t) -> aux t) l')
 126         l;
 127         List.iter
 128            (fun u ->
 129              if is_not_visited u then
 130               (aux_obj (fst(CicEnvironment.get_obj CicUniv.empty_ugraph u))))
 131         v
 132   in
 133   aux_obj t;
 134   !results
 135
 136 let clean_and_fill uri obj ugraph =
 137   let list_of_universes = universes_of_obj uri obj in
 138   let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
 139   let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
 140   ugraph
 141