(* Copyright (C) 2000-2004, 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/
 *)

(*CSC codice cut & paste da cicPp e xmlcommand *)

exception NotImplemented;;

let dtdname ~ask_dtd_to_the_getter dtd =
 if ask_dtd_to_the_getter then
  Helm_registry.get "getter.url" ^ "getdtd?uri=" ^ dtd
 else
  "http://mowgli.cs.unibo.it/dtd/" ^ dtd
;;

let param_attribute_of_params params =
 String.concat " " (List.map UriManager.string_of_uri params)
;;

(*CSC ottimizzazione: al posto di curi cdepth (vedi codice) *)
let print_term ?ids_to_inner_sorts =
 let find_sort name id =
  match ids_to_inner_sorts with
     None -> []
   | Some ids_to_inner_sorts ->
      [None,name,Cic2acic.string_of_sort (Hashtbl.find ids_to_inner_sorts id)]
 in
 let rec aux =
  let module C = Cic in
  let module X = Xml in
  let module U = UriManager in
    function
       C.ARel (id,idref,n,b) ->
        let sort = find_sort "sort" id in
         X.xml_empty "REL"
          (sort @
           [None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
           None,"idref",idref])
     | C.AVar (id,uri,exp_named_subst) ->
        let sort = find_sort "sort" id in
         aux_subst uri
          (X.xml_empty "VAR"
            (sort @ [None,"uri",U.string_of_uri uri;None,"id",id]))
          exp_named_subst
     | C.AMeta (id,n,l) ->
        let sort = find_sort "sort" id in
         X.xml_nempty "META"
          (sort @ [None,"no",(string_of_int n) ; None,"id",id])
          (List.fold_left
            (fun i t ->
              match t with
                 Some t' ->
                  [< i ; X.xml_nempty "substitution" [] (aux t') >]
               | None ->
                  [< i ; X.xml_empty "substitution" [] >]
            ) [< >] l)
     | C.ASort (id,s) ->
        let string_of_sort s =
          Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)
        in
         X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
     | C.AImplicit _ -> raise NotImplemented
     | C.AProd (last_id,_,_,_) as prods ->
        let rec eat_prods =
         function
            C.AProd (id,n,s,t) ->
             let prods,t' = eat_prods t in
              (id,n,s)::prods,t'
          | t -> [],t
        in
         let prods,t = eat_prods prods in
          let sort = find_sort "type" last_id in
           X.xml_nempty "PROD" sort
            [< List.fold_left
                (fun i (id,binder,s) ->
                  let sort = find_sort "type" (Cic2acic.source_id_of_id id) in
                   let attrs =
                    sort @ ((None,"id",id)::
                     match binder with
                        C.Anonymous -> []
                      | C.Name b -> [None,"binder",b])
                   in
                    [< i ; X.xml_nempty "decl" attrs (aux s) >]
                ) [< >] prods ;
               X.xml_nempty "target" [] (aux t)
            >]
     | C.ACast (id,v,t) ->
        let sort = find_sort "sort" id in
         X.xml_nempty "CAST" (sort @ [None,"id",id])
          [< X.xml_nempty "term" [] (aux v) ;
             X.xml_nempty "type" [] (aux t)
          >]
     | C.ALambda (last_id,_,_,_) as lambdas ->
        let rec eat_lambdas =
         function
            C.ALambda (id,n,s,t) ->
             let lambdas,t' = eat_lambdas t in
              (id,n,s)::lambdas,t'
          | t -> [],t
        in
         let lambdas,t = eat_lambdas lambdas in
          let sort = find_sort "sort" last_id in
           X.xml_nempty "LAMBDA" sort
            [< List.fold_left
                (fun i (id,binder,s) ->
                  let sort = find_sort "type" (Cic2acic.source_id_of_id id) in
                   let attrs =
                    sort @ ((None,"id",id)::
                     match binder with
                        C.Anonymous -> []
                      | C.Name b -> [None,"binder",b])
                   in
                    [< i ; X.xml_nempty "decl" attrs (aux s) >]
                ) [< >] lambdas ;
               X.xml_nempty "target" [] (aux t)
            >]
     | C.ALetIn (xid,C.Anonymous,s,t) ->
       assert false
     | C.ALetIn (last_id,C.Name _,_,_) as letins ->
        let rec eat_letins =
         function
            C.ALetIn (id,n,s,t) ->
             let letins,t' = eat_letins t in
              (id,n,s)::letins,t'
          | t -> [],t
        in
         let letins,t = eat_letins letins in
          let sort = find_sort "sort" last_id in
           X.xml_nempty "LETIN" sort
            [< List.fold_left
                (fun i (id,binder,s) ->
                  let sort = find_sort "sort" id in
                   let attrs =
                    sort @ ((None,"id",id)::
                     match binder with
                        C.Anonymous -> []
                      | C.Name b -> [None,"binder",b])
                   in
                    [< i ; X.xml_nempty "def" attrs (aux s) >]
                ) [< >] letins ;
               X.xml_nempty "target" [] (aux t)
            >]
     | C.AAppl (id,li) ->
        let sort = find_sort "sort" id in
         X.xml_nempty "APPLY" (sort @ [None,"id",id])
          [< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
          >]
     | C.AConst (id,uri,exp_named_subst) ->
        let sort = find_sort "sort" id in
         aux_subst uri
          (X.xml_empty "CONST"
            (sort @ [None,"uri",(U.string_of_uri uri) ; None,"id",id])
          ) exp_named_subst
     | C.AMutInd (id,uri,i,exp_named_subst) ->
        aux_subst uri
         (X.xml_empty "MUTIND"
           [None, "uri", (U.string_of_uri uri) ;
            None, "noType", (string_of_int i) ;
            None, "id", id]
         ) exp_named_subst
     | C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
        let sort = find_sort "sort" id in
         aux_subst uri
          (X.xml_empty "MUTCONSTRUCT"
            (sort @
             [None,"uri", (U.string_of_uri uri) ;
              None,"noType",(string_of_int i) ;
              None,"noConstr",(string_of_int j) ;
              None,"id",id])
          ) exp_named_subst
     | C.AMutCase (id,uri,typeno,ty,te,patterns) ->
        let sort = find_sort "sort" id in
         X.xml_nempty "MUTCASE"
          (sort @
           [None,"uriType",(U.string_of_uri uri) ;
            None,"noType", (string_of_int typeno) ;
            None,"id", id])
          [< X.xml_nempty "patternsType" [] [< (aux ty) >] ;
             X.xml_nempty "inductiveTerm" [] [< (aux te) >] ;
             List.fold_right
              (fun x i -> [< X.xml_nempty "pattern" [] [< aux x >] ; i>])
              patterns [<>]
          >]
     | C.AFix (id, no, funs) ->
        let sort = find_sort "sort" id in
         X.xml_nempty "FIX"
          (sort @ [None,"noFun", (string_of_int no) ; None,"id",id])
          [< List.fold_right
              (fun (id,fi,ai,ti,bi) i ->
                [< X.xml_nempty "FixFunction"
                    [None,"id",id ; None,"name", fi ;
                     None,"recIndex", (string_of_int ai)]
                    [< X.xml_nempty "type" [] [< aux ti >] ;
                       X.xml_nempty "body" [] [< aux bi >]
                    >] ;
                   i
                >]
              ) funs [<>]
          >]
     | C.ACoFix (id,no,funs) ->
        let sort = find_sort "sort" id in
         X.xml_nempty "COFIX"
          (sort @ [None,"noFun", (string_of_int no) ; None,"id",id])
          [< List.fold_right
              (fun (id,fi,ti,bi) i ->
                [< X.xml_nempty "CofixFunction" [None,"id",id ; None,"name", fi]
                    [< X.xml_nempty "type" [] [< aux ti >] ;
                       X.xml_nempty "body" [] [< aux bi >]
                    >] ;
                   i
                >]
              ) funs [<>]
          >]
 and aux_subst buri target subst =
(*CSC: I have now no way to assign an ID to the explicit named substitution *)
  let id = None in
   if subst = [] then
    target
   else
    Xml.xml_nempty "instantiate"
     (match id with None -> [] | Some id -> [None,"id",id])
     [< target ;
        List.fold_left
         (fun i (uri,arg) ->
           let relUri =
            let buri_frags =
             Str.split (Str.regexp "/") (UriManager.string_of_uri buri) in
            let uri_frags = 
             Str.split (Str.regexp "/") (UriManager.string_of_uri uri)  in
             let rec find_relUri buri_frags uri_frags =
              match buri_frags,uri_frags with
                 [_], _ -> String.concat "/" uri_frags
               | he1::tl1, he2::tl2 ->
                  assert (he1 = he2) ;
                  find_relUri tl1 tl2
               | _,_ -> assert false (* uri is not relative to buri *)
             in
              find_relUri buri_frags uri_frags
           in
            [< i ; Xml.xml_nempty "arg" [None,"relUri", relUri] (aux arg) >]
         ) [<>] subst
     >]
  in
   aux
;;

let xml_of_attrs attributes =
  let class_of = function
    | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
    | `Elim s ->
        Xml.xml_nempty "class" [None,"value","elim"]
         [< Xml.xml_empty
             "SORT" [None,"value",
                      (Cic2acic.string_of_sort (Cic2acic.sort_of_sort s)) ;
                     None,"id","elimination_sort"] >]
    | `Record field_names ->
        Xml.xml_nempty "class" [None,"value","record"]
         (List.fold_right
           (fun name res ->
             [< Xml.xml_empty "field" [None,"name",name]; res >]
           ) field_names [<>])
    | `Projection -> Xml.xml_empty "class" [None,"value","projection"]
  in
  let flavour_of = function
    | `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
    | `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
    | `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
    | `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
    | `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
    | `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
  in
  let xml_attr_of = function
    | `Generated -> Xml.xml_empty "generated" []
    | `Class c -> class_of c
    | `Flavour f -> flavour_of f
  in
  let xml_attrs =
   List.fold_right 
    (fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
  in
   Xml.xml_nempty "attributes" [] xml_attrs

let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
 let module C = Cic in
 let module X = Xml in
 let module U = UriManager in
  let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in
   match obj with
       C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
        let params' = param_attribute_of_params params in
        let xml_attrs = xml_of_attrs obj_attrs in
        let xml_for_current_proof_body =
(*CSC: Should the CurrentProof also have the list of variables it depends on? *)
(*CSC: I think so. Not implemented yet.                                       *)
         X.xml_nempty "CurrentProof"
          [None,"of",UriManager.string_of_uri uri ; None,"id", id]
          [< xml_attrs;
            List.fold_left
              (fun i (cid,n,canonical_context,t) ->
                [< i ;
                   X.xml_nempty "Conjecture"
                    [None,"id",cid ; None,"no",(string_of_int n)]
                    [< List.fold_left
                        (fun i (hid,t) ->
                          [< (match t with
                                 Some (n,C.ADecl t) ->
                                  X.xml_nempty "Decl"
                                   (match n with
                                       C.Name n' ->
                                        [None,"id",hid;None,"name",n']
                                     | C.Anonymous -> [None,"id",hid])
                                   (print_term ?ids_to_inner_sorts t)
                               | Some (n,C.ADef t) ->
                                  X.xml_nempty "Def"
                                   (match n with
                                       C.Name n' ->
                                        [None,"id",hid;None,"name",n']
                                     | C.Anonymous -> [None,"id",hid])
                                   (print_term ?ids_to_inner_sorts t)
                              | None -> X.xml_empty "Hidden" [None,"id",hid]
                             ) ;
                             i
                          >]
                        ) [< >] canonical_context ;
                       X.xml_nempty "Goal" []
                        (print_term ?ids_to_inner_sorts t)
                    >]
                >])
              [< >] conjectures ;
             X.xml_nempty "body" [] (print_term ?ids_to_inner_sorts bo) >]
        in
        let xml_for_current_proof_type =
         X.xml_nempty "ConstantType"
          [None,"name",n ; None,"params",params' ; None,"id", id]
          (print_term ?ids_to_inner_sorts ty)
        in
        let xmlbo =
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
            X.xml_cdata ("<!DOCTYPE CurrentProof SYSTEM \""^ dtdname ^ "\">\n");
            xml_for_current_proof_body
         >] in
        let xmlty =
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
            xml_for_current_proof_type
         >]
        in
         xmlty, Some xmlbo
     | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
        let params' = param_attribute_of_params params in
        let xml_attrs = xml_of_attrs obj_attrs in
        let xmlbo =
         match bo with
            None -> None
          | Some bo ->
             Some
              [< X.xml_cdata
                  "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
                 X.xml_cdata
                  ("<!DOCTYPE ConstantBody SYSTEM \"" ^ dtdname ^ "\">\n") ;
                 X.xml_nempty "ConstantBody"
                  [None,"for",UriManager.string_of_uri uri ;
                   None,"params",params' ; None,"id", id]
                  [< print_term ?ids_to_inner_sorts bo >]
              >]
        in
        let xmlty =
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
            X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
             X.xml_nempty "ConstantType"
              [None,"name",n ; None,"params",params' ; None,"id", id]
              [< xml_attrs; print_term ?ids_to_inner_sorts ty >]
         >]
        in
         xmlty, xmlbo
     | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
        let params' = param_attribute_of_params params in
        let xml_attrs = xml_of_attrs obj_attrs in
        let xmlbo =
         match bo with
            None -> [< >]
          | Some bo ->
             X.xml_nempty "body" [] [< print_term ?ids_to_inner_sorts bo >]
        in
        let aobj =
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
            X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
             X.xml_nempty "Variable"
              [None,"name",n ; None,"params",params' ; None,"id", id]
              [< xml_attrs; xmlbo;
                 X.xml_nempty "type" [] (print_term ?ids_to_inner_sorts ty)
              >]
         >]
        in
         aobj, None
     | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
        let params' = param_attribute_of_params params in
        let xml_attrs = xml_of_attrs obj_attrs in
         [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
            X.xml_cdata
             ("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
            X.xml_nempty "InductiveDefinition"
             [None,"noParams",string_of_int nparams ;
              None,"id",id ;
              None,"params",params']
             [< xml_attrs;
                (List.fold_left
                  (fun i (id,typename,finite,arity,cons) ->
                    [< i ;
                       X.xml_nempty "InductiveType"
                        [None,"id",id ; None,"name",typename ;
                         None,"inductive",(string_of_bool finite)
                        ]
                        [< X.xml_nempty "arity" []
                            (print_term ?ids_to_inner_sorts arity) ;
                           (List.fold_left
                            (fun i (name,lc) ->
                              [< i ;
                                 X.xml_nempty "Constructor"
                                  [None,"name",name]
                                  (print_term ?ids_to_inner_sorts lc)
                              >]) [<>] cons
                           )
                        >]
                    >]
                  ) [< >] tys
                )
             >]
         >], None
;;

let
 print_inner_types curi ~ids_to_inner_sorts ~ids_to_inner_types
  ~ask_dtd_to_the_getter
=
 let module C2A = Cic2acic in
 let module X = Xml in
  let dtdname = dtdname ~ask_dtd_to_the_getter "cictypes.dtd" in
   [< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
      X.xml_cdata
       ("<!DOCTYPE InnerTypes SYSTEM \"" ^ dtdname ^ "\">\n") ;
      X.xml_nempty "InnerTypes" [None,"of",UriManager.string_of_uri curi]
       (Hashtbl.fold
         (fun id {C2A.annsynthesized = synty ; C2A.annexpected = expty} x ->
           [< x ;
              X.xml_nempty "TYPE" [None,"of",id]
               [< X.xml_nempty "synthesized" []
	         [< print_term ~ids_to_inner_sorts synty >] ;
                 match expty with
                   None -> [<>]
                 | Some expty' -> X.xml_nempty "expected" []
                    [< print_term ~ids_to_inner_sorts expty' >]
               >]
           >]
         ) ids_to_inner_types [<>]
       )
   >]
;;