(* 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 terms level of a parser for cic objects from xml        *)
(* files to the internal representation. It is used by the module cicParser2  *)
(* (objects level). It defines an extension of the standard dom using the     *)
(* object-oriented extension machinery of markup: an object with a method     *)
(* to_cic_term that returns the internal representation of the subtree is     *)
(* added to each node of the dom tree                                         *)
(*                                                                            *)
(******************************************************************************)

exception IllFormedXml of int;;

(* The list of tokens of the current section path. *)
(* Used to resolve relative URIs                   *)
let current_sp = ref [];;

(* The uri of the object been parsed *)
let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;

(* Utility functions to map a markup attribute to something useful *)

let cic_attr_of_xml_attr =
 function
    Pxp_types.Value s       -> Cic.Name s
  | Pxp_types.Implied_value -> Cic.Anonimous
  | _             -> raise (IllFormedXml 1)

let cic_sort_of_xml_attr =
 function
    Pxp_types.Value "Prop" -> Cic.Prop
  | Pxp_types.Value "Set"  -> Cic.Set
  | Pxp_types.Value "Type" -> Cic.Type
  | _            -> raise (IllFormedXml 2)

let int_of_xml_attr =
 function
    Pxp_types.Value n -> int_of_string n
  | _       -> raise (IllFormedXml 3)

let uri_of_xml_attr =
 function
    Pxp_types.Value s -> UriManager.uri_of_string s
  | _       -> raise (IllFormedXml 4)

let string_of_xml_attr =
 function
    Pxp_types.Value s -> s
  | _       -> raise (IllFormedXml 5)

let binder_of_xml_attr =
 function
    Pxp_types.Value s -> s
  | _       -> raise (IllFormedXml 17)
;;

(* the "interface" of the class linked to each node of the dom tree *)

class virtual cic_term =
  object (self)

    (* fields and methods ever required by markup *)
    val mutable node = (None : cic_term Pxp_document.node option)

    method clone = {< >} 
    method node =
      match node with
          None ->
            assert false
        | Some n -> n
    method set_node n =
      node <- Some n

    (* a method that returns the internal representation of the tree (term) *)
    (* rooted in this node                                                  *)
    method virtual to_cic_term : Cic.annterm
  end
;;

(* the class of the objects linked to nodes that are not roots of cic terms *)
class eltype_not_of_cic =
  object (self)

     inherit cic_term

     method to_cic_term = raise (IllFormedXml 6)
  end
;;

(* the class of the objects linked to nodes whose content is a cic term *)
(* (syntactic sugar xml entities) e.g. <type> ... </type>               *)
class eltype_transparent =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      match n#sub_nodes with
         [ t ]  -> t#extension#to_cic_term
       | _  -> raise (IllFormedXml 7)
  end
;;

(* A class for each cic node type *)

class eltype_fix =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let nofun = int_of_xml_attr (n#attribute "noFun")
      and id = string_of_xml_attr (n#attribute "id")
      and functions =
       let sons = n#sub_nodes in
        List.map
         (function
             f when f#node_type = Pxp_document.T_element "FixFunction" ->
              let name = string_of_xml_attr (f#attribute "name")
              and recindex = int_of_xml_attr (f#attribute "recIndex")
              and (ty, body) =
               match f#sub_nodes with
                  [t ; b] when
                    t#node_type = Pxp_document.T_element "type" &&
                    b#node_type = Pxp_document.T_element "body" ->
                     (t#extension#to_cic_term, b#extension#to_cic_term)
                | _ -> raise (IllFormedXml 14)
              in
               (name, recindex, ty, body)
           | _ -> raise (IllFormedXml 13)
         ) sons
      in
       Cic.AFix (id, nofun, functions)
  end
;;

class eltype_cofix =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let nofun = int_of_xml_attr (n#attribute "noFun")
      and id = string_of_xml_attr (n#attribute "id")
      and functions =
       let sons = n#sub_nodes in
        List.map
         (function
             f when f#node_type = Pxp_document.T_element "CofixFunction" ->
              let name = string_of_xml_attr (f#attribute "name")
              and (ty, body) =
               match f#sub_nodes with
                  [t ; b] when
                    t#node_type = Pxp_document.T_element "type" &&
                    b#node_type = Pxp_document.T_element "body" ->
                     (t#extension#to_cic_term, b#extension#to_cic_term)
                | _ -> raise (IllFormedXml 16)
              in
               (name, ty, body)
           | _ -> raise (IllFormedXml 15)
         ) sons
      in
       Cic.ACoFix (id, nofun, functions)
  end
;;

class eltype_implicit =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let id = string_of_xml_attr (n#attribute "id") in
       Cic.AImplicit id
  end
;;

class eltype_rel =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let value  = int_of_xml_attr (n#attribute "value")
      and binder = binder_of_xml_attr (n#attribute "binder")
      and id = string_of_xml_attr (n#attribute "id") in
       Cic.ARel (id,value,binder)
  end
;;

class eltype_meta =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let value = int_of_xml_attr (n#attribute "no")
      and id = string_of_xml_attr (n#attribute "id")
      in
       let local_context =
        let sons = n#sub_nodes in
         List.map
          (function substitution ->
            match substitution#sub_nodes with
               [] -> None
             | [he] -> Some he#extension#to_cic_term
             | _ -> raise (IllFormedXml 20)
          ) sons
       in
        Cic.AMeta (id,value,local_context)
  end
;;

class eltype_var =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let name = string_of_xml_attr (n#attribute "relUri")
      and xid = string_of_xml_attr (n#attribute "id") in
       match Str.split (Str.regexp ",") name with
          [index; id] ->
           let get_prefix n =
            let rec aux =
             function
                (0,_) -> "/"
              | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
              | _ -> raise (IllFormedXml 19)
            in   
             aux (List.length !current_sp - n,!current_sp)
           in
            Cic.AVar
             (xid, 
              (UriManager.uri_of_string
               ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
             )
        | _ -> raise (IllFormedXml 18)
  end
;;

class eltype_apply =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let children = n#sub_nodes
      and id = string_of_xml_attr (n#attribute "id") in
       if List.length children < 2 then raise (IllFormedXml 8)
       else
        Cic.AAppl
         (id,List.map (fun x -> x#extension#to_cic_term) children)
  end
;;

class eltype_cast =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let sons = n#sub_nodes
      and id = string_of_xml_attr (n#attribute "id") in
       match sons with
          [te ; ty] when
            te#node_type = Pxp_document.T_element "term" &&
            ty#node_type = Pxp_document.T_element "type" ->
             let term = te#extension#to_cic_term
             and typ  = ty#extension#to_cic_term in
              Cic.ACast (id,term,typ)
        | _  -> raise (IllFormedXml 9)
  end
;;

class eltype_sort =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let sort = cic_sort_of_xml_attr (n#attribute "value")
      and id = string_of_xml_attr (n#attribute "id") in
       Cic.ASort (id,sort)
  end
;;

class eltype_const =
  object (self)

    inherit cic_term

    method to_cic_term =
     let module U = UriManager in
      let n = self#node in
       let value = uri_of_xml_attr (n#attribute "uri")
       and id = string_of_xml_attr (n#attribute "id") in
        Cic.AConst (id,value, U.relative_depth !current_uri value 0)
  end
;;

class eltype_mutind =
  object (self)

    inherit cic_term

    method to_cic_term =
     let module U = UriManager in
      let n = self#node in
       let name = uri_of_xml_attr (n#attribute "uri")
       and noType = int_of_xml_attr (n#attribute "noType")
       and id = string_of_xml_attr (n#attribute "id") in
        Cic.AMutInd
         (id,name, U.relative_depth !current_uri name 0, noType)
  end
;;

class eltype_mutconstruct =
  object (self)

    inherit cic_term

    method to_cic_term =
     let module U = UriManager in
      let n = self#node in
       let name = uri_of_xml_attr (n#attribute "uri")
       and noType = int_of_xml_attr (n#attribute "noType")
       and noConstr = int_of_xml_attr (n#attribute "noConstr")
       and id = string_of_xml_attr (n#attribute "id") in
        Cic.AMutConstruct
         (id, name, U.relative_depth !current_uri name 0,
         noType, noConstr)
  end
;;

class eltype_prod =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let sons = n#sub_nodes
      and id = string_of_xml_attr (n#attribute "id") in
       match sons with
          [s ; t] when
            s#node_type = Pxp_document.T_element "source" &&
            t#node_type = Pxp_document.T_element "target" ->
             let name = cic_attr_of_xml_attr (t#attribute "binder")
             and source = s#extension#to_cic_term
             and target = t#extension#to_cic_term in
              Cic.AProd (id,name,source,target)
        | _  -> raise (IllFormedXml 10)
  end
;;

class eltype_mutcase =
  object (self)

    inherit cic_term

    method to_cic_term =
     let module U = UriManager in
      let n = self#node in
       let sons = n#sub_nodes
       and id = string_of_xml_attr (n#attribute "id") in
        match sons with
           ty::te::patterns when
             ty#node_type = Pxp_document.T_element "patternsType" &&
             te#node_type = Pxp_document.T_element "inductiveTerm" ->
              let ci = uri_of_xml_attr (n#attribute "uriType")
              and typeno = int_of_xml_attr (n#attribute "noType")
              and inductiveType = ty#extension#to_cic_term
              and inductiveTerm = te#extension#to_cic_term
              and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
              in
               Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0,
                typeno,inductiveType,inductiveTerm,lpattern)
         | _  -> raise (IllFormedXml 11)
  end
;;

class eltype_lambda =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let sons = n#sub_nodes
      and id = string_of_xml_attr (n#attribute "id") in
       match sons with
          [s ; t] when
            s#node_type = Pxp_document.T_element "source" &&
            t#node_type = Pxp_document.T_element "target" ->
             let name = cic_attr_of_xml_attr (t#attribute "binder")
             and source = s#extension#to_cic_term
             and target = t#extension#to_cic_term in
              Cic.ALambda (id,name,source,target)
        | _  -> raise (IllFormedXml 12)
  end
;;

class eltype_letin =
  object (self)

    inherit cic_term

    method to_cic_term =
     let n = self#node in
      let sons = n#sub_nodes
      and id = string_of_xml_attr (n#attribute "id") in
       match sons with
          [s ; t] when
            s#node_type = Pxp_document.T_element "term" &&
            t#node_type = Pxp_document.T_element "letintarget" ->
             let name = cic_attr_of_xml_attr (t#attribute "binder")
             and source = s#extension#to_cic_term
             and target = t#extension#to_cic_term in
              Cic.ALetIn (id,name,source,target)
        | _  -> raise (IllFormedXml 12)
  end
;;

(* The definition of domspec, an hashtable that maps each node type to the *)
(* object that must be linked to it. Used by markup.                       *)

let domspec =
 let module D = Pxp_document in
  D.make_spec_from_alist
   ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
   ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
   ~element_alist:
    [ "REL",           (new D.element_impl (new eltype_rel)) ;
      "VAR",           (new D.element_impl (new eltype_var)) ;
      "META",          (new D.element_impl (new eltype_meta)) ;
      "SORT",          (new D.element_impl (new eltype_sort)) ;
      "IMPLICIT",      (new D.element_impl (new eltype_implicit)) ;
      "CAST",          (new D.element_impl (new eltype_cast)) ;
      "PROD",          (new D.element_impl (new eltype_prod)) ;
      "LAMBDA",        (new D.element_impl (new eltype_lambda)) ;
      "LETIN",         (new D.element_impl (new eltype_letin)) ;
      "APPLY",         (new D.element_impl (new eltype_apply)) ;
      "CONST",         (new D.element_impl (new eltype_const)) ;
      "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
      "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
      "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;
      "FIX",           (new D.element_impl (new eltype_fix)) ;
      "COFIX",         (new D.element_impl (new eltype_cofix)) ;
      "arity",         (new D.element_impl (new eltype_transparent)) ;
      "term",          (new D.element_impl (new eltype_transparent)) ;
      "type",          (new D.element_impl (new eltype_transparent)) ;
      "body",          (new D.element_impl (new eltype_transparent)) ;
      "source",        (new D.element_impl (new eltype_transparent)) ;
      "target",        (new D.element_impl (new eltype_transparent)) ;
      "letintarget",   (new D.element_impl (new eltype_transparent)) ;
      "patternsType",  (new D.element_impl (new eltype_transparent)) ;
      "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
      "pattern",       (new D.element_impl (new eltype_transparent))
    ]
   ()
;;