(* 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                                 *)
(*                                                                            *)
(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
(*                                 03/04/2001                                 *)
(*                                                                            *)
(*                            Missing description                             *)
(*                                                                            *)
(******************************************************************************)

let iteri foo =
 let counter = ref 0 in
  List.iter (function e -> incr counter ; foo e !counter)
;;

let pathname_of_uri uristring =
 "forward" ^
  Str.replace_first (Str.regexp "^cic:") "" uristring
;;

let make_dirs dirpath =
 ignore (Unix.system ("mkdir -p \"" ^ dirpath ^ "\""))
;;

module UriHash =
 struct
  type classification =
     Backbone
   | Branch
   | InConclusion
   | InHypothesis
   | InBody
  ;;

let soften_classification =
 function
    Backbone -> InConclusion
  | Branch -> InHypothesis
  | InBody -> assert false
  | k -> k
;;

  let hash = Hashtbl.create 117 ;;

  let add_uri uri kind =
   let old_kinds =
    try
     Hashtbl.find hash uri
    with
     Not_found -> []
   in
    let new_kinds = 
     match kind,old_kinds with
        InBody,[] -> [InBody]
      | InBody,_  -> old_kinds
      | k,_ when List.mem k old_kinds -> old_kinds
      | k,_ -> k::old_kinds
    in
     Hashtbl.replace hash uri new_kinds
  ;;

  (* It also removes every element in the hash *)
  let uris_fold foo init =
   let xml_element_name_of_kind =
    function
       Backbone     -> "MainConclusion"
     | Branch       -> "MainHypothesis"
     | InConclusion -> "InConclusion"
     | InHypothesis -> "InHypothesis"
     | InBody       -> "InBody"
   in
    let res =
     Hashtbl.fold
      (fun uri kinds i ->
        List.fold_left
         (fun j kind ->
           foo j uri (xml_element_name_of_kind kind)
         ) i kinds
      ) hash init
    in
     Hashtbl.clear hash ;
     res
  ;;
 end
;;

let output_content () =
 UriHash.uris_fold
  (fun i uri kind ->
    [< Xml.xml_nempty "h:refObj" []
        (Xml.xml_empty "h:Occurrence"
          ["rdf:about","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#" ^ kind ;
           "rdf:value",uri]
        ) ;
       i
    >]
  ) [<>]
;;

let output_file cic_string_uri rdf_string_uri =
 let module U = UriManager in
 let module X = Xml in
  let content = output_content () in
  let rdf_uri = U.uri_of_string rdf_string_uri in
   make_dirs (pathname_of_uri (U.buri_of_uri rdf_uri)) ;
   X.pp
    [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
       X.xml_nempty "rdf:RDF"
        ["xml:lang","en" ;
         "xmlns:rdf","http://www.w3.org/1999/02/22-rdf-syntax-ns#";
         "xmlns:h","http://www.cs.unibo.it/helm/schemas/schema-h.rdf#"]

        (try
          Stream.empty content ; (* raise Stream.failure if not empty *)
          X.xml_empty "h:Object" ["rdf:about",cic_string_uri]
         with
          Stream.Failure ->
           X.xml_nempty "h:Object" ["rdf:about",cic_string_uri] content
        )
    >]
    (Some (pathname_of_uri rdf_string_uri ^ ".xml"))
;;

let get_obj uri =
 let cicfilename = Getter.getxml uri in
  let res = CicParser.obj_of_xml cicfilename uri in
   Unix.unlink cicfilename ;
   res
;;

let add_every_constructor uri typeno kind =
 let module C = Cic in
  match (get_obj uri) with
      (C.InductiveDefinition (itys,_,_)) ->
        let string_uri = UriManager.string_of_uri uri in
        let sn = string_of_int (typeno + 1) in
        let (_,_,_,cons) = List.nth itys typeno in
         iteri
          (fun (_,cty,_) m ->
            let sm = string_of_int m in
             UriHash.add_uri
              (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
              kind
          ) cons
   | _ -> assert false
;;

let process_type term =
 let module U = UriManager in
 let module H = UriHash in
 let module C = Cic in
  let rec process_type_aux kind =
   function
    | C.Var uri ->
       H.add_uri (U.string_of_uri uri) kind
    | C.Cast (te,_) ->
       (* type ignored *)
       process_type_aux kind te
    | C.Prod (_,sou,ta) ->
       let (source_kind,target_kind) =
        match kind with
           H.Backbone -> (H.Branch,H.Backbone)
         | H.Branch -> (H.InHypothesis,H.InHypothesis)
         | H.InBody -> assert false
         | k -> (k,k)
       in
        process_type_aux source_kind sou ;
        process_type_aux target_kind ta
    | C.Lambda (_,sou,ta) ->
        let kind' = H.soften_classification kind in
         process_type_aux kind' sou ;
         process_type_aux kind' ta
    | C.LetIn (_,te,ta)->
       let kind' = H.soften_classification kind in
        process_type_aux kind' te ;
        process_type_aux kind ta
    | C.Appl (he::tl) ->
       let kind' = H.soften_classification kind in
        process_type_aux kind he ;
        List.iter (process_type_aux kind') tl
    | C.Appl _ -> assert false
    | C.Const (uri,_) ->
       UriHash.add_uri (U.string_of_uri uri) kind
    | C.MutInd (uri,_,typeno) ->
       H.add_uri
        (U.string_of_uri uri ^ "#xpointer(1/" ^
          string_of_int (typeno + 1) ^ ")")
        kind
    | C.MutConstruct (uri,_,typeno,consno) ->
       H.add_uri
        (U.string_of_uri uri ^ "#xpointer(1/" ^
          string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
        kind
    | C.MutCase (uri,_,typeno,_,term,patterns) ->
       (* outtype ignored *)
       let kind' = H.soften_classification kind in
        add_every_constructor uri typeno kind' ;
        process_type_aux kind' term ;
        List.iter (process_type_aux kind') patterns
    | C.Fix (_,funs) ->
       let kind' = H.soften_classification kind in
        List.iter
         (function (_,_,bo,ty) ->
           process_type_aux kind' bo ;
           process_type_aux kind' ty ;
         ) funs
    | C.CoFix (_,funs) ->
       let kind' = H.soften_classification kind in
        List.iter
         (function (_,bo,ty) ->
           process_type_aux kind' bo ;
           process_type_aux kind' ty ;
         ) funs
    | _ -> ()
in
 process_type_aux H.Backbone (CicMiniReduction.letin_nf term)
;;

let process_body =
 let module U = UriManager in
 let module H = UriHash in
 let module C = Cic in
  let rec process_body_aux =
   function
      C.Var uri ->
       H.add_uri (U.string_of_uri uri) H.InBody
    | C.Cast (te,ty) ->
       process_body_aux te ;
       process_body_aux ty
    | C.Prod (_,sou,ta) ->
       process_body_aux sou ;
       process_body_aux ta
    | C.Lambda (_,sou,ta) ->
       process_body_aux sou ;
       process_body_aux ta
    | C.LetIn (_,te,ta)->
       process_body_aux te ;
       process_body_aux ta
    | C.Appl l ->
       List.iter process_body_aux l
    | C.Const (uri,_) ->
       UriHash.add_uri (U.string_of_uri uri) H.InBody
    | C.MutInd (uri,_,typeno) ->
       H.add_uri
        (U.string_of_uri uri ^ "#xpointer(1/" ^
          string_of_int (typeno + 1) ^ ")")
        H.InBody
    | C.MutConstruct (uri,_,typeno,consno) ->
       H.add_uri
        (U.string_of_uri uri ^ "#xpointer(1/" ^
          string_of_int (typeno + 1) ^ "/" ^ string_of_int consno ^ ")")
        H.InBody
    | C.MutCase (uri,_,typeno,outtype,term,patterns) ->
       add_every_constructor uri typeno H.InBody ;
       process_body_aux outtype ;
       process_body_aux term ;
       List.iter process_body_aux patterns
    | C.Fix (_,funs) ->
       List.iter
        (function (_,_,bo,ty) ->
          process_body_aux bo ;
          process_body_aux ty ;
        ) funs
    | C.CoFix (_,funs) ->
       List.iter
        (function (_,bo,ty) ->
          process_body_aux bo ;
          process_body_aux ty ;
        ) funs
    | _ -> ()
in
 process_body_aux
;;

let process_obj string_uri =
 let module U = UriManager in
 let module C = Cic in
  function
     (C.Definition (_,bo,ty,_)) ->
       process_type ty ;
       process_body bo ;
       output_file string_uri string_uri
   | (C.Axiom (_,ty,_)) ->
       process_type ty ;
       output_file string_uri string_uri
   | (C.Variable (_,bo,ty)) ->
       process_type ty ;
       begin
        match bo with
           (Some bo') -> process_body bo'
         | _ -> ()
       end ;
       output_file string_uri string_uri
   | (C.InductiveDefinition _) as id ->
       begin
        let id' =
         CicSubstitution.undebrujin_inductive_def
          (U.uri_of_string string_uri) id
        in
         match id' with
            (C.InductiveDefinition (itys,_,_)) -> 
              iteri
               (fun (_,_,ty,cons) n ->
                 let sn = string_of_int n in
                  process_type ty ;
                  output_file
                   (string_uri ^ "#xpointer(1/" ^ sn ^ ")")
                   (string_uri ^ "," ^ sn) ;
                  iteri
                   (fun (_,cty,_) m ->
                     let sm = string_of_int m in
                      process_type cty ;
                      output_file
                       (string_uri ^ "#xpointer(1/" ^ sn ^ "/" ^ sm ^ ")")
                       (string_uri ^ "," ^ sn ^ "," ^ sm)
                   ) cons
               ) itys
          | _ -> assert false
       end
   | (C.CurrentProof _) -> assert false
;;

let mk_forward string_uri =
 let module U = UriManager in
  print_endline ("Now computing metadata of " ^ string_uri) ;
  flush stdout ;
  let uri = U.uri_of_string string_uri in
  let obj = get_obj uri in
   process_obj string_uri obj
;;

let _ =
 let usage_msg = "usage: mk_forward[.opt] URI" in
 let uri = ref "" in
  Arg.parse []
   (fun x ->
     if x = "" then
      begin
       prerr_string "No URI provided.\n" ;
       Arg.usage [] usage_msg ;
       exit (-1)
      end
     else if !uri = "" then
      uri := x
     else
      begin
       prerr_string "More than two arguments provided.\n" ;
       Arg.usage [] usage_msg ;
       exit (-1)
      end
   ) usage_msg ;
   if !uri = "" then
    begin
     prerr_string "No URI provided.\n" ;
     Arg.usage [] usage_msg ;
     exit (-1)
    end ;
   mk_forward !uri
;;