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 (* uri is the uri of the actual object that must be 'skipped' *)
  38 let universes_of_obj uri t =
  39   let eq  = UriManager.eq in
  40   let don = ref [] in
  41   let module C = Cic in
  42   let rec aux t =
  43     match t with
  44       C.Const (u,exp_named_subst)
  45     | C.Var (u,exp_named_subst) ->
  46         if List.mem u !don then [] else
  47         (don := u::!don;
  48          aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
  49                     CicUniv.empty_ugraph))
  50     | C.MutInd (u,_,exp_named_subst) ->
  51         if List.mem u !don || eq u uri then
  52           []
  53         else
  54           begin
  55             don := u::!don;
  56             (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
  57                          CicUniv.empty_ugraph)
  58               with
  59                | C.InductiveDefinition (l,_,_) ->
  60                    List.fold_left (
  61                      fun y (_,_,t,l') ->
  62                        y @ (aux t) @
  63                        (List.fold_left (
  64                           fun x (_,t) -> x @ (aux t) )
  65                           [] l'))
  66                      [] l
  67               | _ -> assert false) @
  68             List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
  69           end
  70     | C.MutConstruct (u,_,_,exp_named_subst) ->
  71         if List.mem u !don || eq u uri then
  72           []
  73         else
  74           begin
  75             don := u::!don;
  76             (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
  77                          CicUniv.empty_ugraph) with
  78                | C.InductiveDefinition (l,_,_) ->
  79                    List.fold_left (
  80                      fun x (_,_,_t,l') ->
  81                        x @ aux t @
  82                        (List.fold_left (
  83                           fun y (_,t) -> y @ (aux t) )
  84                           []  l'))
  85                      [] l
  86                | _ -> assert false) @
  87             List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
  88           end
  89     | C.Meta (n,l1) ->
  90         List.fold_left
  91           (fun x t ->
  92              match t with
  93                  Some t' -> x @ (aux t')
  94                | _ -> x)
  95           [] l1
  96     | C.Sort ( C.Type i) -> [i]
  97     | C.Rel _
  98     | C.Sort _
  99     | C.Implicit _ -> []
 100     | C.Prod (b,s,t) ->
 101         aux s @ aux t
 102     | C.Cast (v,t) ->
 103         aux v @ aux t
 104     | C.Lambda (b,s,t) ->
 105         aux s @ aux t
 106     | C.LetIn (b,s,t) ->
 107         aux s @ aux t
 108     | C.Appl li ->
 109         List.fold_left (fun x t -> x @  (aux t)) []  li
 110     | C.MutCase (uri,n1,ty,te,patterns) ->
 111         aux ty @ aux te @
 112         (List.fold_left (fun x t -> x @ (aux t)) [] patterns)
 113     | C.Fix (no, funs) ->
 114         List.fold_left (fun x (_,_,b,c) -> x @ (aux b) @ (aux c)) [] funs
 115     | C.CoFix (no,funs) ->
 116         List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs
 117   and aux_obj ?(boo=false) (t,_)  =
 118     (match t with
 119          C.Constant (_,Some te,ty,v) -> aux te @ aux ty @
 120            List.fold_left (
 121              fun l u ->
 122                l @ if eq u uri then [] else
 123                  (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 124                               CicUniv.empty_ugraph)))
 125            [] v
 126        | C.Constant (_,None,ty,v) -> aux ty @
 127            List.fold_left (
 128              fun l u ->
 129                l @ if eq u uri then [] else
 130                  (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 131                               CicUniv.empty_ugraph)))
 132              [] v
 133        | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
 134            List.fold_left (
 135              fun l u ->
 136                l @ if eq u uri then [] else
 137                  (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 138                               CicUniv.empty_ugraph)))
 139              [] v
 140        | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
 141            List.fold_left (
 142              fun l u ->
 143                l @ if eq u uri then [] else
 144                  (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 145                               CicUniv.empty_ugraph)))
 146              [] v
 147        | C.Variable (_,None ,ty,v) -> aux ty @
 148            List.fold_left (
 149              fun l u ->
 150                l @ if eq u uri then [] else
 151                  (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 152                               CicUniv.empty_ugraph)))
 153              [] v
 154        | C.InductiveDefinition (l,v,_) ->
 155            (List.fold_left (
 156               fun x (_,_,t,l') ->
 157                 x @ aux t @ List.fold_left (
 158                   fun y (_,t) -> y @ aux t)
 159                 [] l')
 160               [] l) @
 161            (List.fold_left
 162               (fun l u ->
 163                l @ if eq u uri then [] else
 164                  (aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 165                               CicUniv.empty_ugraph)))
 166               [] v)
 167     )
 168   in
 169     aux_obj (t,CicUniv.empty_ugraph)
 170
 171 let clean_and_fill uri obj ugraph =
 172   let list_of_universes = universes_of_obj uri obj in
 173   let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
 174   let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
 175   ugraph
 176