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

(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...."      *)
(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
let mk_absolute_uris s =
 let l = (Str.split (Str.regexp ":") s) in
  let absolute_of_relative n v =
   let module P3 = CicParser3 in
    let rec mkburi =
     function
        (0,_) -> "/"
      | (n,he::tl) when n > 0 ->
         "/" ^ he ^ mkburi (n - 1, tl)
      | _ -> raise (IllFormedXml 12)
    in
     let m = List.length !P3.current_sp - (int_of_string n) in
      let buri = mkburi (m, !P3.current_sp) in
       UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
  in
   let rec absolutize =
    function
       [] -> []
     | [no ; vs] ->
        let vars = (Str.split (Str.regexp " ") vs) in
         [(int_of_string no, List.map (absolute_of_relative no) vars)]
     | no::vs::tl -> 
        let vars = (Str.split (Str.regexp " ") vs) in
         let rec add_prefix =
          function
             [no2] -> ([], no2)
           | he::tl ->
              let (pvars, no2) = add_prefix tl in
               ((absolute_of_relative no he)::pvars, no2)
           | _ -> raise (IllFormedXml 11)
         in
          let (pvars, no2) = add_prefix vars in
           (int_of_string no, pvars)::(absolutize (no2::tl))
     | _ -> raise (IllFormedXml 10)
   in
    (* last parameter must be applied first *)
    absolutize l
;;

let option_uri_list_of_attr a1 a2 =
 let module T = Pxp_types in
  let parameters =
   match a1 with
      T.Value s -> mk_absolute_uris s
    | _ -> raise (IllFormedXml 0)
  in
   match a2 with
      T.Value "POSSIBLE" -> Cic.Possible parameters
    | T.Implied_value -> Cic.Actual parameters
    | _ -> raise (IllFormedXml 0)
;;

let uri_list_of_attr a =
 let module T = Pxp_types in
  match a with
     T.Value s -> mk_absolute_uris 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)
;;

(* Other utility functions *)

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

let register_id id node =
 if !CicParser3.process_annotations then
  match !CicParser3.ids_to_targets with
     None -> assert false
   | Some ids_to_targets ->
      Hashtbl.add ids_to_targets id (Cic.Object node)
;;

(* 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_type l =
 let rec rget (c, v, t) l =
  let module D = Pxp_document in
   match l with
      [] -> (c, v, t)
    | conj::tl when conj#node_type = D.T_element "Conjecture" ->
       let no = int_of_attr (conj#attribute "no")
       and typ = (get_content conj)#extension#to_cic_term in
        rget ((no, typ)::c, v, t) 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', t) tl
          | _    -> raise (IllFormedXml 2)
        )
    | typ::tl when typ#node_type = D.T_element "type" ->
       let t' = (get_content typ)#extension#to_cic_term in
        (match t with
            None -> rget (c, v, Some t') tl
          | _    -> raise (IllFormedXml 3)
        )
    | _ -> raise (IllFormedXml 4)
 in
  match rget ([], None, None) l with
     (c, Some v, Some t) -> (c, v, t)
   | _ -> 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,ref None)::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 (arity,cons) =
      get_names_arity_constructors (he#sub_nodes)
     in
      (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
;;

(* 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 =
 let module D = Pxp_document in
 let module C = Cic in
  let ntype = n # node_type in
  match ntype with
    D.T_element "Definition" ->
      let id = string_of_attr (n # attribute "name")
      and params =
       option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
      and (value, typ) = 
       let sons = n#sub_nodes in
        match sons with
          [v ; t] when
            v#node_type = D.T_element "body" &&
            t#node_type = D.T_element "type" ->
             let v' = get_content v
             and t' = get_content t in
              (v'#extension#to_cic_term, t'#extension#to_cic_term)
        | _ -> raise (IllFormedXml 6)
      and xid = string_of_attr (n#attribute "id") in
       let res = C.ADefinition (xid, ref None, id, value, typ, params) in
        register_id xid res ;
        res
  | D.T_element "Axiom" ->
      let id = string_of_attr (n # attribute "name")
      and params = uri_list_of_attr (n # attribute "params")
      and typ = 
       (get_content (get_content n))#extension#to_cic_term
      and xid = string_of_attr (n#attribute "id") in
       let res = C.AAxiom (xid, ref None, id, typ, params) in
        register_id xid res ;
        res
  | D.T_element "CurrentProof" ->
     let name = string_of_attr (n#attribute "name")
     and xid = string_of_attr (n#attribute "id") in
     let sons = n#sub_nodes in
      let (conjs, value, typ) = get_conjs_value_type sons in
       let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in
        register_id xid res ;
        res
  | 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
       let res =
        C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams)
       in
        register_id xid res ;
        res
  | D.T_element "Variable" ->
     let name = string_of_attr (n#attribute "name")
     and xid = string_of_attr (n#attribute "id") in
      let typ = (get_content (get_content n))#extension#to_cic_term in
       let res = C.AVariable (xid,ref None,name,typ) in
        register_id xid res ;
        res
  | D.T_element _
  | D.T_data ->
     raise (IllFormedXml 7)
;;