Added universes handling. The PRE_UNIVERSES tag may help ;)

[helm.git] / helm / ocaml / cic_proof_checking / cicUnivUtils.ml

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
new file mode 100644 (file)
index 0000000..8182f72
--- /dev/null
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -0,0 +1,163 @@
+(* Copyright (C) 2000, HELM Team.
+ * 
+ * This file is part of HELM, an Hypertextual, Electronic
+ * Library of Mathematics, developed at the Computer Science
+ * Department, University of Bologna, Italy.
+ * 
+ * HELM is free software; you can redistribute it and/or
+ * modify it under the terms of the GNU General Public License
+ * as published by the Free Software Foundation; either version 2
+ * of the License, or (at your option) any later version.
+ * 
+ * HELM is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with HELM; if not, write to the Free Software
+ * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
+ * MA  02111-1307, USA.
+ * 
+ * For details, see the HELM World-Wide-Web page,
+ * http://cs.unibo.it/helm/.
+ *)
+
+(*****************************************************************************)
+(*                                                                           *)
+(*                              PROJECT HELM                                 *)
+(*                                                                           *)
+(*                     Enrico Tassi <tassi@cs.unibo.it>                      *)
+(*                                23/04/2004                                 *)
+(*                                                                           *)
+(* This module implements some useful function regarding univers graphs      *)
+(*                                                                           *)
+(*****************************************************************************)
+
+let universes_of_obj t =
+  let don = ref [] in
+  let module C = Cic in
+  let rec aux t =
+    match t with
+      C.Const (u,exp_named_subst) 
+    | C.Var (u,exp_named_subst) ->
+        if List.mem u !don then [] else
+        (don := u::!don;
+         aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u 
+                   CicUniv.empty_ugraph))
+    | C.MutInd (u,_,exp_named_subst) ->
+       if List.mem u !don then 
+         [] 
+       else
+          begin
+           don := u::!don;
+            (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u  
+                        CicUniv.empty_ugraph) with
+               | C.InductiveDefinition (l,_,_) -> 
+                  List.fold_left (
+                    fun y (_,_,t,l') -> 
+                      y @ (aux t) @ 
+                      (List.fold_left (
+                         fun x (_,t) -> x @ (aux t) )
+                         [] l'))
+                    [] l
+             | _ -> assert false) @ 
+           List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
+         end
+    | C.MutConstruct (u,_,_,exp_named_subst) ->
+       if List.mem u !don then 
+         [] 
+       else
+         begin
+           don := u::!don;
+           (match fst(CicEnvironment.get_obj ~not_jet_cooked:true u 
+                        CicUniv.empty_ugraph) with
+              | C.InductiveDefinition (l,_,_) -> 
+                  List.fold_left (
+                    fun x (_,_,_t,l') ->
+                      x @ aux t @  
+                      (List.fold_left (
+                         fun y (_,t) -> y @ (aux t) )
+                         []  l')) 
+                    [] l
+              | _ -> assert false) @ 
+           List.fold_left (fun x (uri,t) -> x @ (aux t) ) [] exp_named_subst
+         end
+    | C.Meta (n,l1) ->
+        List.fold_left 
+          (fun x t -> 
+             match t with 
+                Some t' -> x @ (aux t') 
+               | _ -> x) 
+          [] l1
+    | C.Sort ( C.Type i) -> [i]
+    | C.Rel _ 
+    | C.Sort _
+    | C.Implicit _ -> []
+    | C.Prod (b,s,t) ->
+       aux s @ aux t
+    | C.Cast (v,t) -> 
+       aux v @ aux t
+    | C.Lambda (b,s,t) ->
+       aux s @ aux t 
+    | C.LetIn (b,s,t) ->
+       aux s @ aux t
+    | C.Appl li ->
+       List.fold_left (fun x t -> x @  (aux t)) []  li
+    | C.MutCase (uri,n1,ty,te,patterns) ->
+       aux ty @ aux te @
+       (List.fold_left (fun x t -> x @ (aux t)) [] patterns)
+    | C.Fix (no, funs) ->
+       List.fold_left (fun x (_,_,b,c) -> x @ (aux b) @ (aux c)) [] funs
+    | C.CoFix (no,funs) ->
+       List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs
+  and aux_obj ?(boo=false) (t,_)  = 
+    (match t with
+        C.Constant (_,Some te,ty,v) -> aux te @ aux ty @
+           List.fold_left (
+             fun l u ->
+               l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
+                              CicUniv.empty_ugraph))
+          [] v
+       | C.Constant (_,None,ty,v) -> aux ty @
+           List.fold_left (
+             fun l u ->
+               l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
+                              CicUniv.empty_ugraph))
+            [] v
+       | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
+           List.fold_left (
+             fun l u ->
+               l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
+                              CicUniv.empty_ugraph))
+            [] v
+       | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
+           List.fold_left (
+             fun l u ->
+               l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
+                              CicUniv.empty_ugraph))
+            [] v
+       | C.Variable (_,None ,ty,v) -> aux ty @ 
+           List.fold_left (
+             fun l u ->
+               l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
+                              CicUniv.empty_ugraph))
+            [] v
+       | C.InductiveDefinition (l,v,_) -> 
+          (List.fold_left (
+             fun x (_,_,t,l') ->
+               x @ aux t @ List.fold_left (
+                 fun y (_,t) -> y @ aux t) 
+               [] l') 
+             [] l) @ 
+          (List.fold_left (
+             fun l u -> 
+              l @ aux_obj (CicEnvironment.get_obj ~not_jet_cooked:true u
+                             CicUniv.empty_ugraph))
+             [] v)
+    )
+  in 
+    aux_obj (t,CicUniv.empty_ugraph) 
+
+
+