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 let universes_of_obj t =
  38   let don = ref [] in
  39   let module C = Cic in
  40   let rec aux t =
  41     match t with
  42       C.Const (u,exp_named_subst)
  43     | C.Var (u,exp_named_subst) ->
  44         if List.mem u !don then [] else
  45         (don := u::!don;
  46          aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
  47                     CicUniv.empty_ugraph))
  48     | C.MutInd (u,_,exp_named_subst) ->
  49         if List.mem u !don then
  50           []
  51         else
  52           begin
  53             don := u::!don;
  54             (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
  55                          CicUniv.empty_ugraph) with
  56                | C.InductiveDefinition (l,_,_) ->
  57                    List.fold_left (
  58                      fun y (_,_,t,l') ->
  59                        y @ (aux t) @
  60                        (List.fold_left (
  61                           fun x (_,t) -> x @ (aux t) )
  62                           [] l'))
  63                      [] l
  64               | _ -> assert false) @
  65             List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
  66           end
  67     | C.MutConstruct (u,_,_,exp_named_subst) ->
  68         if List.mem u !don then
  69           []
  70         else
  71           begin
  72             don := u::!don;
  73             (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u
  74                          CicUniv.empty_ugraph) 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 @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 120                               CicUniv.empty_ugraph))
 121            [] v
 122        | C.Constant (_,None,ty,v) -> aux ty @
 123            List.fold_left (
 124              fun l u ->
 125                l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 126                               CicUniv.empty_ugraph))
 127              [] v
 128        | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
 129            List.fold_left (
 130              fun l u ->
 131                l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 132                               CicUniv.empty_ugraph))
 133              [] v
 134        | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
 135            List.fold_left (
 136              fun l u ->
 137                l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 138                               CicUniv.empty_ugraph))
 139              [] v
 140        | C.Variable (_,None ,ty,v) -> aux ty @
 141            List.fold_left (
 142              fun l u ->
 143                l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 144                               CicUniv.empty_ugraph))
 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 @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
 156                               CicUniv.empty_ugraph))
 157               [] v)
 158     )
 159   in
 160     aux_obj (t,CicUniv.empty_ugraph)
 161
 162
 163