(* Copyright (C) 2004-2005, 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://helm.cs.unibo.it/
 *)

(* $Id$ *)

let object_declaration_hook = ref (fun _ _ -> ());;
let set_object_declaration_hook f =
 object_declaration_hook := f

exception AlreadyDefined of UriManager.uri

let auxiliary_lemmas_hashtbl = UriManager.UriHashtbl.create 29

(* uri |-->  (derived_coercions_in_the_coercion_DB, derived_coercions_in_lib)
 * 
 * in case of remove_coercion uri, the first component is removed from the
 * coercion DB, while the second is passed to remove_obj (and is not [] only if
 * add_coercion is called with add_composites 
 * *)
let coercion_hashtbl = UriManager.UriHashtbl.create 3

let uris_of_obj uri =
 let innertypesuri = UriManager.innertypesuri_of_uri uri in
 let bodyuri = UriManager.bodyuri_of_uri uri in
 let univgraphuri = UriManager.univgraphuri_of_uri uri in
  innertypesuri,bodyuri,univgraphuri

let paths_and_uris_of_obj uri =
  let resolved = Http_getter.filename' ~local:true ~writable:true uri in
  let basepath = Filename.dirname resolved in
  let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
  let innertypesfilename=(UriManager.nameext_of_uri innertypesuri)^".xml.gz"in
  let innertypespath = basepath ^ "/" ^ innertypesfilename in
  let xmlfilename = (UriManager.nameext_of_uri uri) ^ ".xml.gz" in
  let xmlpath = basepath ^ "/" ^ xmlfilename in
  let xmlbodyfilename = (UriManager.nameext_of_uri uri) ^ ".body.xml.gz" in
  let xmlbodypath = basepath ^ "/" ^  xmlbodyfilename in
  let xmlunivgraphfilename=(UriManager.nameext_of_uri univgraphuri)^".xml.gz"in
  let xmlunivgraphpath = basepath ^ "/" ^ xmlunivgraphfilename in
  xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
  xmlunivgraphpath, univgraphuri

let save_object_to_disk uri obj ugraph univlist =
  let write f x =
    if not (Helm_registry.get_opt_default 
              Helm_registry.bool "matita.nodisk" ~default:false) 
    then      
      f x
  in
  let ensure_path_exists path =
    let dir = Filename.dirname path in
    HExtlib.mkdir dir
  in
  (* generate annobj, ids_to_inner_sorts and ids_to_inner_types *)
  let annobj, innertypes, ids_to_inner_sorts, generate_attributes =
   if Helm_registry.get_bool "matita.system" &&
      not (Helm_registry.get_bool "matita.noinnertypes")
   then
    let annobj, _, _, ids_to_inner_sorts, ids_to_inner_types, _, _ =
     Cic2acic.acic_object_of_cic_object obj 
    in
    let innertypesxml = 
     Cic2Xml.print_inner_types
      uri ~ids_to_inner_sorts ~ids_to_inner_types ~ask_dtd_to_the_getter:false
    in
    annobj, Some innertypesxml, Some ids_to_inner_sorts, false
   else 
    let annobj = Cic2acic.plain_acic_object_of_cic_object obj in  
    annobj, None, None, true 
  in 
  (* prepare XML *)
  let xml, bodyxml =
   Cic2Xml.print_object
    uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter:false 
    ~generate_attributes annobj 
  in    
  let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
      xmlunivgraphpath, univgraphuri = 
    paths_and_uris_of_obj uri 
  in
  write (List.iter HExtlib.mkdir) (List.map Filename.dirname [xmlpath]);
  (* now write to disk *)
  write ensure_path_exists xmlpath;
  write (Xml.pp ~gzip:true xml) (Some xmlpath);
  write (CicUniv.write_xml_of_ugraph xmlunivgraphpath ugraph) univlist;
  (* we return a list of uri,path we registered/created *)
  (uri,xmlpath) ::
  (univgraphuri,xmlunivgraphpath) ::
    (* now the optional inner types, both write and register *)
    (match innertypes with 
     | None -> []
     | Some innertypesxml ->
         write ensure_path_exists innertypespath;
         write (Xml.pp ~gzip:true innertypesxml) (Some innertypespath);
         [innertypesuri, innertypespath]
    ) @
    (* now the optional body, both write and register *)
    (match bodyxml,bodyuri with
       None,_ -> []
     | Some bodyxml,Some bodyuri->
         write ensure_path_exists xmlbodypath;
         write (Xml.pp ~gzip:true bodyxml) (Some xmlbodypath);
         [bodyuri, xmlbodypath]
     | _-> assert false) 


let typecheck_obj =
 let profiler = HExtlib.profile "add_obj.typecheck_obj" in
  fun uri obj -> profiler.HExtlib.profile (CicTypeChecker.typecheck_obj uri) obj

let index_obj =
 let profiler = HExtlib.profile "add_obj.index_obj" in
  fun ~dbd ~uri ->
   profiler.HExtlib.profile (fun uri -> MetadataDb.index_obj ~dbd ~uri) uri

let add_single_obj uri obj refinement_toolkit =
  let module RT = RefinementTool in
  let obj = 
    if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
       not (CoercDb.is_a_coercion' (Cic.Const (uri, [])))
    then
      refinement_toolkit.RT.pack_coercion_obj obj
    else
      obj 
  in
  let dbd = LibraryDb.instance () in
  if CicEnvironment.in_library uri then
    raise (AlreadyDefined uri)
  else begin
    (*CicUniv.reset_spent_time ();
    let before = Unix.gettimeofday () in*)
    typecheck_obj uri obj; (* 1 *)
    (*let after = Unix.gettimeofday () in
    let univ_time = CicUniv.get_spent_time () in
    let total_time = after -. before in
    prerr_endline 
      (Printf.sprintf "QED: %%univ = %2.5f, total = %2.5f, univ = %2.5f, %s\n" 
      (univ_time *. 100. /. total_time) (total_time) (univ_time)
      (UriManager.name_of_uri uri));*)
    let obj, ugraph, univlist = 
      try CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri 
      with CicEnvironment.Object_not_found _ -> assert false
    in
    try 
      index_obj ~dbd ~uri; (* 2 must be in the env *)
      try
        (*3*)
        let new_stuff = save_object_to_disk uri obj ugraph univlist in
        (* EXPERIMENTAL: pretty print the object in natural language *)
	(try !object_declaration_hook uri obj
	 with exc ->
	  prerr_endline ("Error: object_declaration_hook failed"^
          Printexc.to_string exc));
        try 
         HLog.message
          (Printf.sprintf "%s defined" (UriManager.string_of_uri uri))
        with exc ->
          List.iter HExtlib.safe_remove (List.map snd new_stuff); (* -3 *)
          raise exc
      with exc ->
        ignore(LibraryDb.remove_uri uri); (* -2 *)
        raise exc
    with exc ->
      CicEnvironment.remove_obj uri; (* -1 *)
      raise exc
  end

let remove_single_obj uri =
  let derived_uris_of_uri uri =
   let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
    innertypesuri::univgraphuri::(match bodyuri with None -> [] | Some u -> [u])
  in
  let uris_to_remove =
   if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else [uri]
  in
  let files_to_remove = uri :: derived_uris_of_uri uri in   
  List.iter 
   (fun uri -> 
     (try
       let file = Http_getter.resolve' ~local:true ~writable:true uri in
        HExtlib.safe_remove file;
        HExtlib.rmdir_descend (Filename.dirname file)
     with Http_getter_types.Key_not_found _ -> ());
   ) files_to_remove ;
  List.iter 
   (fun uri -> 
     ignore (LibraryDb.remove_uri uri);
     (*CoercGraph.remove_coercion uri;*)
   ) uris_to_remove ;
  CicEnvironment.remove_obj uri

(*** GENERATION OF AUXILIARY LEMMAS ***)

let generate_elimination_principles uri refinement_toolkit =
  let uris = ref [] in
  let elim i =
    let elim sort =
      try
	let uri,obj = CicElim.elim_of ~sort uri i in
	  add_single_obj uri obj refinement_toolkit;
	  uris := uri :: !uris
      with CicElim.Can_t_eliminate -> ()
    in
      try
	List.iter 
	  elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
      with exn ->
	List.iter remove_single_obj !uris;
	raise exn 
  in
  let obj, _ = (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) in
    match obj with
      | Cic.InductiveDefinition (indTypes, _, _, _) ->
	  let counter = ref 0 in
	    List.iter (fun _ -> elim !counter; counter := !counter+1) indTypes;
	    !uris
      | _  -> 
	  failwith (Printf.sprintf "not an inductive definition (%s)"
		      (UriManager.string_of_uri uri))

(* COERCIONS ***********************************************************)
  
let remove_all_coercions () =
  UriManager.UriHashtbl.clear coercion_hashtbl;
  CoercDb.remove_coercion (fun (_,_,_,_) -> true)

let stack = ref [];;

let h2l h =
  UriManager.UriHashtbl.fold 
  (fun k v acc -> (k,v) :: acc) h []
;;

let push () =
  stack := (CoercDb.dump (), h2l coercion_hashtbl) :: !stack;
  remove_all_coercions ()
;;

let pop () =
  match !stack with
  | [] -> raise (Failure "Unable to POP from librarySync.ml")
  | (db,h) :: tl -> 
      stack := tl;
      remove_all_coercions ();
      CoercDb.restore db;
      List.iter (fun (k,v) -> UriManager.UriHashtbl.add coercion_hashtbl k v)
      h
;;

let add_coercion ~add_composites refinement_toolkit uri arity saturations
 baseuri
=
  let coer_ty,_ =
    let coer = CicUtil.term_of_uri uri in
    CicTypeChecker.type_of_aux' [] [] coer CicUniv.oblivion_ugraph 
  in
  (* we have to get the source and the tgt type uri
   * in Coq syntax we have already their names, but
   * since we don't support Funclass and similar I think
   * all the coercion should be of the form
   * (A:?)(B:?)T1->T2
   * So we should be able to extract them from the coercion type
   * 
   * Currently only (_:T1)T2 is supported.
   * should we saturate it with metas in case we insert it?
   * 
   *)
  let spine2list ty =
    let rec aux = function
      | Cic.Prod( _, src, tgt) -> src::aux tgt
      | t -> [t]
    in
    aux ty
  in
  let src_carr, tgt_carr = 
    let get_classes arity saturations l = 
      (* this is the ackerman's function revisited *)
      let rec aux = function
         0,0,None,tgt::src::_ -> src,Some (`Class tgt)
       | 0,0,target,src::_ -> src,target
       | 0,saturations,None,tgt::tl -> aux (0,saturations,Some (`Class tgt),tl)
       | 0,saturations,target,_::tl -> aux (0,saturations - 1,target,tl)
       | arity,saturations,None,_::tl -> 
            aux (arity, saturations, Some `Funclass, tl)
       | arity,saturations,target,_::tl -> 
            aux (arity - 1, saturations, target, tl)
       | _ -> assert false
      in
       aux (arity,saturations,None,List.rev l)
    in
    let types = spine2list coer_ty in
    let src,tgt = get_classes arity saturations types in
     CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] src),
     match tgt with
        None -> assert false
      | Some `Funclass -> CoercDb.Fun arity
      | Some (`Class tgt) ->
         CoercDb.coerc_carr_of_term (CicReduction.whd ~delta:false [] tgt)
  in
  let already_in_obj src_carr tgt_carr uri obj = 
     List.exists 
      (fun (s,t,ul) -> 
        List.exists 
         (fun u,_ -> 
           let bo = 
            match obj with 
            | Cic.Constant (_, Some bo, _, _, _) -> bo
            | _ -> assert false
           in
           CoercDb.eq_carr s src_carr && 
           CoercDb.eq_carr t tgt_carr &&
           if fst (CicReduction.are_convertible [] (CicUtil.term_of_uri u) bo
           CicUniv.oblivion_ugraph)
           then true else
            (HLog.warn
              ("Coercions " ^ 
                UriManager.string_of_uri u ^ " and " ^ UriManager.string_of_uri
                uri^" are not convertible, but are between the same nodes.\n"^
                "From now on unification can fail randomly.");
             false))
         ul)
      (CoercDb.to_list ())
  in
  if not add_composites then
    (CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
    UriManager.UriHashtbl.add coercion_hashtbl uri ([],[]);
    [])
  else
    let new_coercions = 
      CicCoercion.close_coercion_graph src_carr tgt_carr uri saturations
       baseuri
    in
    let new_coercions = 
      List.filter (fun (s,t,u,_,obj,_) -> not(already_in_obj s t u obj))
      new_coercions 
    in
    let composite_uris = List.map (fun (_,_,uri,_,_,_) -> uri) new_coercions in
    (* update the DB *)
    List.iter 
      (fun (src,tgt,uri,saturations,_,_) ->
        CoercDb.add_coercion (src,tgt,uri,saturations)) 
      new_coercions;
    CoercDb.add_coercion (src_carr, tgt_carr, uri, saturations);
    (* add the composites obj and they eventual lemmas *)
    let lemmas = 
        List.fold_left
          (fun acc (_,tgt,uri,saturations,obj,arity) -> 
            add_single_obj uri obj refinement_toolkit;
             (uri,arity,saturations)::acc) 
          [] new_coercions
    in
    (* store that composite_uris are related to uri. the first component is
     * the stuff in the DB while the second is stuff for remove_obj *)
    (* 
       prerr_endline ("adding: " ^ 
         string_of_bool add_composites ^ UriManager.string_of_uri uri);
       List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
        composite_uris; 
    *)
    UriManager.UriHashtbl.add 
      coercion_hashtbl uri (composite_uris,composite_uris);
    (*
    prerr_endline ("lemmas:");
      List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
      lemmas;
    prerr_endline ("lemmas END");*)
    lemmas
;;

let remove_coercion uri =
  try
    let (composites_in_db, composites_in_lib) = 
      UriManager.UriHashtbl.find coercion_hashtbl uri 
    in
    (*prerr_endline ("removing: " ^UriManager.string_of_uri uri);
    List.iter (fun u -> prerr_endline (UriManager.string_of_uri u))
      composites_in_db;*)
    UriManager.UriHashtbl.remove coercion_hashtbl uri;
    CoercDb.remove_coercion 
      (fun (_,_,u,_) -> UriManager.eq uri u);
    (* remove from the DB *) 
    List.iter 
      (fun u -> CoercDb.remove_coercion (fun (_,_,u1,_) -> UriManager.eq u u1))
      composites_in_db;
    (* remove composites from the lib *)
    List.iter remove_single_obj composites_in_lib
  with
    Not_found -> HLog.warn "Coercion removal raise Not_found" (* mhh..... *)
    

let generate_projections refinement_toolkit uri fields =
 let uris = ref [] in
 let projections = 
   CicRecord.projections_of uri 
     (List.map (fun (x,_,_) -> x) fields) 
 in
  try
   List.iter2 
    (fun (uri, name, bo) (_name, coercion, arity) ->
      let saturations = 0 in
      try
       let ty, _ =
         CicTypeChecker.type_of_aux' [] [] bo CicUniv.oblivion_ugraph in
       let attrs = [`Class `Projection; `Generated] in
       let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
        add_single_obj uri obj refinement_toolkit;
        let composites = 
         if coercion then
            begin
(*prerr_endline ("composite for " ^ UriManager.string_of_uri uri);*)
              (*CSC: I think there is a bug here. The composite coercions
                are not remembered in the .moo file. Thus they are re-generated
                every time. Right? *)
              let x = 
                add_coercion ~add_composites:true refinement_toolkit uri arity
                 saturations (UriManager.buri_of_uri uri)
              in
(*prerr_endline ("are: ");
  List.iter (fun u -> prerr_endline (UriManager.string_of_uri u)) x;
  prerr_endline "---";
*)
              (*CSC: I throw the arity away. See comment above *)
              List.map (fun u,_,_ -> u) x
            end
          else  
            []
        in
        uris := uri :: composites @ !uris
      with
         CicTypeChecker.TypeCheckerFailure s ->
          HLog.message
           ("Unable to create projection " ^ name ^ " cause: " ^ Lazy.force s);
       | CicEnvironment.Object_not_found uri ->
          let depend = UriManager.name_of_uri uri in
           HLog.message
            ("Unable to create projection " ^ name ^ " because it requires " ^
               depend)
    ) projections fields;
   !uris
  with exn ->
   List.iter remove_single_obj !uris;
   raise exn

let build_inversion_principle = ref (fun a b -> assert false);;

let generate_inversion refinement_toolkit uri obj =
  List.map 
    (fun (ind_uri,ind_obj) -> 
       add_single_obj ind_uri ind_obj refinement_toolkit;ind_uri)
    (!build_inversion_principle uri obj)

let
 generate_sibling_mutual_definitions refinement_toolkit uri attrs name_to_avoid
=
 function
    Cic.Fix (_,funs) ->
     snd (
      List.fold_right
       (fun (name,idx,ty,bo) (n,uris) ->
         if name = name_to_avoid then
          (n+1,uris)
         else
          let uri =
           UriManager.uri_of_string
            (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
          let bo = Cic.Fix (n,funs) in 
          let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
           add_single_obj uri obj refinement_toolkit;
           (n+1,uri::uris)
       ) funs (1,[]))
  | Cic.CoFix (_,funs) ->
     snd (
      List.fold_right
       (fun (name,ty,bo) (n,uris) ->
         if name = name_to_avoid then
          (n+1,uris)
         else
          let uri =
           UriManager.uri_of_string
            (UriManager.buri_of_uri uri ^ "/" ^ name ^ ".con") in
          let bo = Cic.CoFix (n,funs) in 
          let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
           add_single_obj uri obj refinement_toolkit;
           (n+1,uri::uris)
       ) funs (1,[]))
  | _ -> assert false

let add_obj refinement_toolkit uri obj =
 add_single_obj uri obj refinement_toolkit;
 let uris = ref [] in
 let not_debug = not (Helm_registry.get_bool "matita.debug") in
 try
  begin
   match obj with
    | Cic.Constant (name,Some bo,_,_,attrs) when
       List.mem (`Flavour `MutualDefinition) attrs ->
        uris :=
         !uris @
           generate_sibling_mutual_definitions refinement_toolkit uri attrs
            name bo
    | Cic.Constant _ -> ()
    | Cic.InductiveDefinition (inductivefuns,_,_,attrs) ->
       let _,inductive,_,_ = List.hd inductivefuns in
       if inductive then
        begin
         uris := !uris @ 
           generate_elimination_principles uri refinement_toolkit;
         uris := !uris @ generate_inversion refinement_toolkit uri obj;
        end ;
       let rec get_record_attrs =
         function
         | [] -> None
         | (`Class (`Record fields))::_ -> Some fields
         | _::tl -> get_record_attrs tl
       in
        (match get_record_attrs attrs with
        | None -> () (* not a record *)
        | Some fields ->
           uris := !uris @ 
             (generate_projections refinement_toolkit uri fields))
    | Cic.CurrentProof _
    | Cic.Variable _ -> assert false
  end;
  UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
  !uris
 with 
 | exn when not_debug ->
    List.iter remove_single_obj !uris;
    raise exn

let remove_obj uri =
 let uris =
  try
   let res = UriManager.UriHashtbl.find auxiliary_lemmas_hashtbl uri in
    UriManager.UriHashtbl.remove auxiliary_lemmas_hashtbl uri;
    res
  with
    Not_found -> [] (*assert false*)
 in
  List.iter remove_single_obj (uri::uris)