(* 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>              *)
(*                                 24/01/2000                                 *)
(*                                                                            *)
(* This module is the objects level of a parser for cic objects from xml      *)
(* files to the internal representation. It uses the module cicParser3        *)
(* cicParser3 (terms level) and it is used only through cicParser2 (top       *)
(* level).                                                                    *)
(*                                                                            *)
(******************************************************************************)

exception IllFormedXml of int;;
exception NotImplemented;;

(* Utility functions that transform a Pxp attribute into something useful *)

let uri_list_of_attr a =
 let module T = Pxp_types in
  match a with
     T.Value s ->
      List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s)
   | _ -> raise (IllFormedXml 0)
;;

let string_of_attr a =
 let module T = Pxp_types in
  match a with
     T.Value s -> s
   | _ -> raise (IllFormedXml 0)
;;

let int_of_attr a =
 int_of_string (string_of_attr a)
;;

let bool_of_attr a =
 bool_of_string (string_of_attr a)
;;

let name_of_attr a =
 let module T = Pxp_types in
 let module C = Cic in
  match a with
     T.Value s -> C.Name s
   | T.Implied_value -> C.Anonymous
   | _ -> raise (IllFormedXml 0)
;;

(* Other utility functions *)

let get_content n =
 match n#sub_nodes with
    [ t ] -> t
  | _     -> raise (IllFormedXml 1)
;;

(* Functions that, given the list of sons of a node of the cic dom (objects   *)
(* level), retrieve the internal representation associated to the node.       *)
(* Everytime a cic term subtree is found, it is translated to the internal    *)
(* representation using the method to_cic_term defined in cicParser3.         *)
(* Each function raise IllFormedXml if something goes wrong, but this should  *)
(* be impossible due to the presence of the dtd                               *)
(* The functions should really be obvious looking at their name and the cic   *)
(* dtd                                                                        *)

(* called when a CurrentProof is found *)
let get_conjs_value l =
 let rec rget (c, v) l =
  let module D = Pxp_document in
   match l with
      [] -> (c, v)
    | conj::tl when conj#node_type = D.T_element "Conjecture" ->
       let no = int_of_attr (conj#attribute "no") in
       let id = string_of_attr (conj#attribute "id") in
       let typ,canonical_context =
        match List.rev (conj#sub_nodes) with
           [] -> raise (IllFormedXml 13)
         | typ::canonical_context ->
            (get_content typ)#extension#to_cic_term [],
            List.map
             (function n ->
               let id = string_of_attr (n#attribute "id") in
                match n#node_type with
                   D.T_element "Decl" ->
                    let name = name_of_attr (n#attribute "name") in
                    let term = (get_content n)#extension#to_cic_term [] in
                     id, Some (name,Cic.ADecl term)
                 | D.T_element "Def" ->
                    let name = name_of_attr (n#attribute "name") in
                    let term = (get_content n)#extension#to_cic_term [] in
                     id, Some (name,Cic.ADef term)
                 | D.T_element "Hidden" -> id, None
                 | _ -> raise (IllFormedXml 14)
             ) canonical_context
       in
        rget ((id, no, canonical_context, typ)::c, v) tl
    | value::tl when value#node_type = D.T_element "body" ->
       let v' = (get_content value)#extension#to_cic_term [] in
        (match v with
            None -> rget (c, Some v') tl
          | _    -> raise (IllFormedXml 2)
        )
    | _ -> raise (IllFormedXml 4)
 in
  match rget ([], None) l with
     (revc, Some v) -> (List.rev revc, v)
   | _ -> raise (IllFormedXml 5)
;;

(* used only by get_inductive_types; called one time for each inductive  *)
(* definitions in a block of inductive definitions                       *)
let get_names_arity_constructors l =
 let rec rget (a,c) l =
  let module D = Pxp_document in
   match l with
      [] -> (a, c)
    | arity::tl when arity#node_type = D.T_element "arity" ->
       let a' = (get_content arity)#extension#to_cic_term [] in
        rget (Some a',c) tl
    | con::tl when con#node_type = D.T_element "Constructor" ->
       let id = string_of_attr (con#attribute "name")
       and ty = (get_content con)#extension#to_cic_term [] in
         rget (a,(id,ty)::c) tl
    | _ -> raise (IllFormedXml 9)
 in
  match rget (None,[]) l with
     (Some a, c) -> (a, List.rev c)
   | _ -> raise (IllFormedXml 8)
;;

(* called when an InductiveDefinition is found *)
let rec get_inductive_types =
 function
    []     -> []
  | he::tl ->
     let tyname    = string_of_attr (he#attribute "name")
     and inductive = bool_of_attr   (he#attribute "inductive")
     and xid = string_of_attr (he#attribute "id")
     and (arity,cons) =
      get_names_arity_constructors (he#sub_nodes)
     in
      (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
;;

(* This is the main function and also the only one used directly from *)
(* cicParser. Given the root of the dom tree, it returns the internal *)
(* representation of the cic object described in the tree             *)
(* It uses the previous functions and the to_cic_term method defined  *)
(* in cicParser3 (used for subtrees that encode cic terms)            *)
let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
=
 let module U = UriManager in
 let module D = Pxp_document in
 let module C = Cic in
  let ntype = n#node_type in
  match ntype with
    D.T_element "ConstantType" ->
      let name = string_of_attr (n # attribute "name") in
      let params = uri_list_of_attr (n#attribute "params") in
      let xid = string_of_attr (n#attribute "id") in
      let typ = (get_content n)#extension#to_cic_term [] in
       (match nbody with
           None ->
            (* Axiom *)
            C.AConstant (xid, None, name, None, typ, params)
         | Some nbody' ->
            let nbodytype = nbody'#node_type in
            match nbodytype with
             D.T_element "ConstantBody" ->
(*CSC: the attribute "for" is ignored and not checked
              let for_ = string_of_attr (nbody'#attribute "for") in
*)
              let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
              let xidbody = string_of_attr (nbody'#attribute "id") in
              let value = (get_content nbody')#extension#to_cic_term [] in
               if paramsbody = params then
                C.AConstant (xid, Some xidbody, name, Some value, typ, params)
               else
                raise (IllFormedXml 6)
           | D.T_element "CurrentProof" ->
(*CSC: the attribute "of" is ignored and not checked
              let for_ = string_of_attr (nbody'#attribute "of") in
*)
              let xidbody = string_of_attr (nbody'#attribute "id") in
              let sons = nbody'#sub_nodes in
               let (conjs, value) = get_conjs_value sons in
                C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
           | D.T_element _
           | D.T_data
           | _ -> raise (IllFormedXml 6)
       )
  | D.T_element "InductiveDefinition" ->
     let sons = n#sub_nodes
     and xid = string_of_attr (n#attribute "id") in
      let inductiveTypes = get_inductive_types sons
      and params = uri_list_of_attr (n#attribute "params")
      and nparams = int_of_attr (n#attribute "noParams") in
       C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
  | D.T_element "Variable" ->
     let name = string_of_attr (n#attribute "name")
     and params = uri_list_of_attr (n#attribute "params")
     and xid = string_of_attr (n#attribute "id")
     and (body, typ) = 
      let sons = n#sub_nodes in
       match sons with
          [b ; t] when
            b#node_type = D.T_element "body" &&
            t#node_type = D.T_element "type" ->
             let b' = get_content b
             and t' = get_content t in
              (Some (b'#extension#to_cic_term []), t'#extension#to_cic_term [])
        | [t] when t#node_type = D.T_element "type" ->
             let t' = get_content t in
              (None, t'#extension#to_cic_term [])
        | _ -> raise (IllFormedXml 6)
     in
      C.AVariable (xid,name,body,typ,params)
  | D.T_element _
  | D.T_data
  | _ -> raise (IllFormedXml 7)
;;