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

module C = Cic
module H = UriManager.UriHashtbl 
let eq  = UriManager.eq

(* uri is the uri of the actual object that must be 'skipped' *)
let universes_of_obj uri t =
  (* don't the same work twice *)
  let visited_objs = H.create 31 in
  let visited u = H.replace visited_objs u true in 
  let is_not_visited u = not (H.mem visited_objs u) in 
  visited uri;
  (* the result *)
  let results = ref [] in
  let add_result l = results := l :: !results in
  (* the iterators *)
  let rec aux = function
    | C.Const (u,exp_named_subst) when is_not_visited u ->
        aux_uri u;
        visited u;
        C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
    | C.Var (u,exp_named_subst) when is_not_visited u ->
        aux_uri u;
        visited u;
        C.Var (u,  List.map (fun (x,t) -> x,aux t) exp_named_subst)
    | C.Const (u,exp_named_subst) ->
        C.Const (u, List.map (fun (x,t) -> x,aux t) exp_named_subst)
    | C.Var (u,exp_named_subst) ->
        C.Var (u,  List.map (fun (x,t) -> x,aux t) exp_named_subst)
    | C.MutInd (u,x,exp_named_subst) when is_not_visited u ->
        aux_uri u;
        visited u;
        C.MutInd (u,x,List.map (fun (x,t) -> x,aux t) exp_named_subst)
    | C.MutInd (u,x,exp_named_subst) ->
        C.MutInd (u,x, List.map (fun (x,t) -> x,aux t) exp_named_subst)
    | C.MutConstruct (u,x,y,exp_named_subst) when is_not_visited u ->
        aux_uri u;
        visited u;
        C.MutConstruct (u,x,y,List.map (fun (x,t) -> x,aux t) exp_named_subst)
    | C.MutConstruct (x,y,z,exp_named_subst) ->
        C.MutConstruct (x,y,z,List.map (fun (x,t) -> x,aux t) exp_named_subst)
    | C.Meta (n,l1) -> C.Meta (n, List.map (HExtlib.map_option aux) l1)
    | C.Sort (C.Type i) -> add_result [i]; 
      C.Sort (C.Type (CicUniv.name_universe i uri))
    | C.Rel _ 
    | C.Sort _
    | C.Implicit _ as x -> x
    | C.Cast (v,t) -> C.Cast (aux v, aux t)
    | C.Prod (b,s,t) -> C.Prod (b,aux s, aux t)
    | C.Lambda (b,s,t) ->  C.Lambda (b,aux s, aux t)
    | C.LetIn (b,s,t) -> C.LetIn (b,aux s, aux t)
    | C.Appl li -> C.Appl (List.map aux li)
    | C.MutCase (uri,n1,ty,te,patterns) ->
        C.MutCase (uri,n1,aux ty,aux te, List.map aux patterns)
    | C.Fix (no, funs) -> 
        C.Fix(no, List.map (fun (x,y,b,c) -> (x,y,aux b,aux c)) funs)
    | C.CoFix (no,funs) -> 
        C.CoFix(no, List.map (fun (x,b,c) -> (x,aux b,aux c)) funs)
  and aux_uri u =
    if is_not_visited u then
      let _, _, l = 
        CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph u in 
      add_result l
  and aux_obj = function
    | C.Constant (x,Some te,ty,v,y) ->
        List.iter aux_uri v;
        C.Constant (x,Some (aux te),aux ty,v,y)
    | C.Variable (x,Some te,ty,v,y) -> 
        List.iter aux_uri v;
        C.Variable (x,Some (aux te),aux ty,v,y)
    | C.Constant (x,None, ty, v,y) ->
        List.iter aux_uri v;
        C.Constant (x,None, aux ty, v,y)
    | C.Variable (x,None, ty, v,y) ->
        List.iter aux_uri v;
        C.Variable (x,None, aux ty, v,y)
    | C.CurrentProof (_,conjs,te,ty,v,_) -> assert false
    | C.InductiveDefinition (l,v,x,y) -> 
        List.iter aux_uri v; 
        C.InductiveDefinition (
          List.map
           (fun (x,y,t,l') ->
             (x,y,aux t, List.map (fun (x,t) -> x,aux t) l'))
          l,v,x,y)  
  in 
  let o = aux_obj t in
  List.flatten !results, o

let rec list_uniq = function 
  | [] -> []
  | h::[] -> [h]
  | h1::h2::tl when CicUniv.eq h1 h2 -> list_uniq (h2 :: tl) 
  | h1::tl (* when h1 <> h2 *) -> h1 :: list_uniq tl

let list_uniq l = 
  list_uniq (List.fast_sort CicUniv.compare l)
  
let profiler = (HExtlib.profile "clean_and_fill").HExtlib.profile
  
let clean_and_fill uri obj ugraph =
  (* universes of obj fills the universes of the obj with the right uri *)
  let list_of_universes, obj = universes_of_obj uri obj in
  let list_of_universes = list_uniq list_of_universes in
(*  CicUniv.print_ugraph ugraph;*)
(*  List.iter (fun u -> prerr_endline (CicUniv.string_of_universe u))*)
(*  list_of_universes;*)
  let ugraph = CicUniv.clean_ugraph ugraph list_of_universes in
(*  CicUniv.print_ugraph ugraph;*)
  let ugraph, list_of_universes = 
    CicUniv.fill_empty_nodes_with_uri ugraph list_of_universes uri 
  in
  ugraph, list_of_universes, obj

let clean_and_fill u o g =
  profiler (clean_and_fill u o) g