(* 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) 

let clean_and_fill uri obj ugraph =
  let list_of_universes = universes_of_obj obj in
  let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
  let ugraph = CicUniv.fill_empty_nodes_with_uri ugraph uri in
  ugraph