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

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 rec merge_coercions =
 let module C = Cic in
 let aux = (fun (u,t) -> u,merge_coercions t) in
  function
     C.Rel _ | C.Sort _ | C.Implicit _ as t -> t
   | C.Meta (n,subst) ->
      let subst' =
       List.map
        (function None -> None | Some t -> Some (merge_coercions t)) subst
      in
       C.Meta (n,subst')
   | C.Cast (te,ty) -> C.Cast (merge_coercions te, merge_coercions ty)
   | C.Prod (name,so,dest) -> 
       C.Prod (name, merge_coercions so, merge_coercions dest) 
   | C.Lambda (name,so,dest) -> 
       C.Lambda (name, merge_coercions so, merge_coercions dest)
   | C.LetIn (name,so,dest) -> 
       C.LetIn (name, merge_coercions so, merge_coercions dest)
   | Cic.Appl [ c1 ; (Cic.Appl [c2; head]) ] when 
     CoercGraph.is_a_coercion c1 && CoercGraph.is_a_coercion c2 ->
       let source_carr = CoercGraph.source_of c2 in
       let tgt_carr = CoercGraph.target_of c1 in
       (match CoercGraph.look_for_coercion source_carr tgt_carr 
       with
       | CoercGraph.SomeCoercion c -> Cic.Appl [ c ; head ]
       | _ -> assert false) (* the composite coercion must exist *)
   | C.Appl l -> C.Appl (List.map merge_coercions l)
   | C.Var (uri,exp_named_subst) -> 
       let exp_named_subst = List.map aux exp_named_subst in
       C.Var (uri, exp_named_subst)
   | C.Const (uri,exp_named_subst) ->
       let exp_named_subst = List.map aux exp_named_subst in
       C.Const (uri, exp_named_subst)
   | C.MutInd (uri,tyno,exp_named_subst) ->
       let exp_named_subst = List.map aux exp_named_subst in
       C.MutInd (uri,tyno,exp_named_subst)
   | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
       let exp_named_subst = List.map aux exp_named_subst in
       C.MutConstruct (uri,tyno,consno,exp_named_subst)  
   | C.MutCase (uri,tyno,out,te,pl) ->
       let pl = List.map merge_coercions pl in
       C.MutCase (uri,tyno,merge_coercions out,merge_coercions te,pl)
   | C.Fix (fno, fl) ->
       let fl = List.map (fun (name,idx,ty,bo)->(name,idx,merge_coercions ty,merge_coercions bo)) fl in
       C.Fix (fno, fl)
   | C.CoFix (fno, fl) ->
       let fl = List.map (fun (name,ty,bo) -> (name, merge_coercions ty, merge_coercions bo)) fl in
       C.CoFix (fno, fl)

let merge_coercions_in_obj obj =
  let module C = Cic in
  match obj with
  | C.Constant (id, body, ty, params, attrs) -> 
      let body = 
        match body with 
        | None -> None 
        | Some body -> Some (merge_coercions body) 
      in
      let ty = merge_coercions ty in
        C.Constant (id, body, ty, params, attrs)
  | C.Variable (name, body, ty, params, attrs) ->
      let body = 
        match body with 
        | None -> None 
        | Some body -> Some (merge_coercions body) 
      in
      let ty = merge_coercions ty in
        C.Variable (name, body, ty, params, attrs)
  | C.CurrentProof (_name, _conjectures, _body, _ty, _params, _attrs) ->
      assert false
  | C.InductiveDefinition (indtys, params, leftno, attrs) ->
      let indtys = 
        List.map 
          (fun (name, ind, arity, cl) -> 
            let arity = merge_coercions arity in
            let cl = List.map (fun (name, ty) -> (name,merge_coercions ty)) cl in
            (name, ind, arity, cl))
          indtys
      in
        C.InductiveDefinition (indtys, params, leftno, attrs)

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 ~basedir =
  let basedir = basedir ^ "/xml" in
  let innertypesuri, bodyuri, univgraphuri = uris_of_obj uri in
  let innertypesfilename = Str.replace_first (Str.regexp "^cic:") ""
        (UriManager.string_of_uri innertypesuri) ^ ".xml.gz" in
  let innertypespath = basedir ^ "/" ^ innertypesfilename in
  let xmlfilename = Str.replace_first (Str.regexp "^cic:/") ""
        (UriManager.string_of_uri uri) ^ ".xml.gz" in
  let xmlpath = basedir ^ "/" ^ xmlfilename in
  let xmlbodyfilename = Str.replace_first (Str.regexp "^cic:/") ""
        (UriManager.string_of_uri uri) ^ ".body.xml.gz" in
  let xmlbodypath = basedir ^ "/" ^  xmlbodyfilename in
  let xmlunivgraphfilename = Str.replace_first (Str.regexp "^cic:/") ""
        (UriManager.string_of_uri univgraphuri) ^ ".xml.gz" in
  let xmlunivgraphpath = basedir ^ "/" ^ xmlunivgraphfilename in
  xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
  xmlunivgraphpath, univgraphuri

let save_object_to_disk ~basedir uri obj ugraph univlist =
  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 = Cic2acic.plain_acic_object_of_cic_object obj in 
  (* prepare XML *)
  let xml, bodyxml =
   Cic2Xml.print_object
    uri ?ids_to_inner_sorts:None ~ask_dtd_to_the_getter:false annobj 
  in
  let xmlpath, xmlbodypath, innertypespath, bodyuri, innertypesuri, 
      xmlunivgraphpath, univgraphuri = 
    paths_and_uris_of_obj uri basedir 
  in
  List.iter HExtlib.mkdir (List.map Filename.dirname [xmlpath]);
  (* now write to disk *)
  ensure_path_exists xmlpath;
  Xml.pp ~gzip:true xml (Some xmlpath);
  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 body, both write and register *)
    (match bodyxml,bodyuri with
       None,None -> []
     | Some bodyxml,Some bodyuri->
         ensure_path_exists xmlbodypath;
         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 ~basedir =
  let obj = 
    if (*List.mem `Generated (CicUtil.attributes_of_obj obj) &&*)
       not (CoercGraph.is_a_coercion (Cic.Const (uri, [])))
    then
      merge_coercions_in_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 _, ugraph, univlist = 
      CicEnvironment.get_cooked_obj_with_univlist CicUniv.empty_ugraph uri in
    try 
      index_obj ~dbd ~uri; (* 2 must be in the env *)
      try
        (*3*)
        let new_stuff = save_object_to_disk ~basedir uri obj ugraph univlist in
        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 to_remove =
    uri :: 
    (if UriManager.uri_is_ind uri then LibraryDb.xpointers_of_ind uri else []) @
    derived_uris_of_uri uri
  in   
  List.iter 
    (fun uri -> 
      (try
        let file = Http_getter.resolve' uri in
         HExtlib.safe_remove file;
         HExtlib.rmdir_descend (Filename.dirname file)
      with Http_getter_types.Key_not_found _ -> ());
      ignore (LibraryDb.remove_uri uri);
      (*CoercGraph.remove_coercion uri;*)
      CicEnvironment.remove_obj uri)
  to_remove

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

let generate_elimination_principles ~basedir uri =
  let uris = ref [] in
  let elim sort =
    try
      let uri,obj = CicElim.elim_of ~sort uri 0 in
       add_single_obj uri obj ~basedir;
       uris := uri :: !uris
    with CicElim.Can_t_eliminate -> ()
  in
  try
    List.iter elim [ Cic.Prop; Cic.Set; (Cic.Type (CicUniv.fresh ())) ];
    !uris
  with exn ->
   List.iter remove_single_obj !uris;
   raise exn

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

let add_coercion ~basedir ~add_composites uri =
  let coer_ty,_ =
    let coer = CicUtil.term_of_uri uri in
    CicTypeChecker.type_of_aux' [] [] coer CicUniv.empty_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 extract_last_two_p ty =
    let rec aux = function
      | Cic.Prod( _, src, Cic.Prod (n,t1,t2)) -> 
          assert false
          (* not implemented: aux (Cic.Prod(n,t1,t2)) *)
      | Cic.Prod( _, src, tgt) -> src, tgt
      | _ -> assert false
    in
    aux ty
  in
  let ty_src, ty_tgt = extract_last_two_p coer_ty in
  let src_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_src) in
  let tgt_uri = CoercDb.coerc_carr_of_term (CicReduction.whd [] ty_tgt) in
  let new_coercions = CicCoercion.close_coercion_graph src_uri tgt_uri uri in
  let composite_uris = List.map (fun (_,_,uri,_) -> uri) new_coercions in
  (* update the DB *)
  List.iter 
    (fun (src,tgt,uri,_) -> CoercDb.add_coercion (src,tgt,uri)) 
      new_coercions;
  CoercDb.add_coercion (src_uri, tgt_uri, uri);
  (* add the composites obj and they eventual lemmas *)
  let lemmas = 
    if add_composites then
      List.fold_left
        (fun acc (_,_,uri,obj) -> 
          add_single_obj ~basedir uri obj;
          uri::acc) 
        composite_uris new_coercions
    else
      []
  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 ("aggiungo: " ^ 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,if add_composites then composite_uris else []);
  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 -> () (* mhh..... *)
    

let generate_projections ~basedir uri fields =
 let uris = ref [] in
 let projections = CicRecord.projections_of uri (List.map fst fields) in
  try
   List.iter2 
    (fun (uri, name, bo) (_name, coercion) ->
      try
       let ty, ugraph =
         CicTypeChecker.type_of_aux' [] [] bo CicUniv.empty_ugraph in
       let attrs = [`Class `Projection; `Generated] in
       let obj = Cic.Constant (name,Some bo,ty,[],attrs) in
        add_single_obj ~basedir uri obj;
        let composites = 
         if coercion then
            add_coercion ~basedir ~add_composites:true uri
          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 add_obj uri obj ~basedir =
 add_single_obj uri obj ~basedir;
 let uris = ref [] in
 try
  begin
   match obj with
    | Cic.Constant _ -> ()
    | Cic.InductiveDefinition (_,_,_,attrs) ->
        uris := !uris @ generate_elimination_principles ~basedir uri;
        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 ~basedir uri fields))
    | Cic.CurrentProof _
    | Cic.Variable _ -> assert false
  end;
  UriManager.UriHashtbl.add auxiliary_lemmas_hashtbl uri !uris;
  !uris
 with exn ->
  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)