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