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

(* 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.Anonymous
  | _             -> 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 (CicUniv.fresh ()) (* TASSI: sure? *)
  | _            -> 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 always 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 :
     (UriManager.uri * Cic.annterm) list -> 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 exp_named_subst =
     assert (exp_named_subst = []) ;
     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 exp_named_subst =
     assert (exp_named_subst = []) ;
     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 id = string_of_xml_attr (f#attribute "id")
              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
               (id, 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 exp_named_subst =
     assert (exp_named_subst = []) ;
     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 id = string_of_xml_attr (f#attribute "id")
              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
               (id, 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 exp_named_subst =
     assert (exp_named_subst = []) ;
     let n = self#node in
      let id = string_of_xml_attr (n#attribute "id") in
       Cic.AImplicit (id, None)
  end
;;

class eltype_rel =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     assert (exp_named_subst = []) ;
     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")
      and idref = string_of_xml_attr (n#attribute "idref") in
       Cic.ARel (id,idref,value,binder)
  end
;;

class eltype_meta =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     assert (exp_named_subst = []) ;
     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 exp_named_subst =
     assert (exp_named_subst = []) ;
     let n = self#node in
      let uri = uri_of_xml_attr (n#attribute "uri")
      and xid = string_of_xml_attr (n#attribute "id") in
(*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *)
       Cic.AVar (xid,uri,[])
  end
;;

class eltype_apply =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     assert (exp_named_subst = []) ;
     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 exp_named_subst =
     assert (exp_named_subst = []) ;
     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 exp_named_subst =
     assert (exp_named_subst = []) ;
     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 exp_named_subst =
     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, exp_named_subst)
  end
;;

class eltype_mutind =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     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, noType, exp_named_subst)
  end
;;

class eltype_mutconstruct =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     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, noType, noConstr, exp_named_subst)
  end
;;

class eltype_prod =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     assert (exp_named_subst = []) ;
     let n = self#node in
      let sons = n#sub_nodes in
       let rec get_decls_and_target =
        function
           [t] when t#node_type = Pxp_document.T_element "target" ->
            [],t#extension#to_cic_term []
         | s::tl when s#node_type = Pxp_document.T_element "decl" ->
            let decls,target = get_decls_and_target tl in
             let id = string_of_xml_attr (s#attribute "id") in
             let binder = cic_attr_of_xml_attr (s#attribute "binder") in
              (id,binder,s#extension#to_cic_term [])::decls, target
         | _  -> raise (IllFormedXml 10)
       in
        let decls,target = get_decls_and_target sons in
         List.fold_right
          (fun (id,b,s) t -> Cic.AProd (id,b,s,t))
          decls target
  end
;;

class eltype_mutcase =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     assert (exp_named_subst = []) ;
     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, typeno,inductiveType,inductiveTerm,lpattern)
         | _  -> raise (IllFormedXml 11)
  end
;;

class eltype_lambda =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     assert (exp_named_subst = []) ;
     let n = self#node in
      let sons = n#sub_nodes in
       let rec get_decls_and_target =
        function
           [t] when t#node_type = Pxp_document.T_element "target" ->
            [],t#extension#to_cic_term []
         | s::tl when s#node_type = Pxp_document.T_element "decl" ->
            let decls,target = get_decls_and_target tl in
             let id = string_of_xml_attr (s#attribute "id") in
             let binder = cic_attr_of_xml_attr (s#attribute "binder") in
              (id,binder,s#extension#to_cic_term [])::decls, target
         | _  -> raise (IllFormedXml 12)
       in
        let decls,target = get_decls_and_target sons in
         List.fold_right
          (fun (id,b,s) t -> Cic.ALambda (id,b,s,t))
          decls target
  end
;;

class eltype_letin =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     assert (exp_named_subst = []) ;
     let n = self#node in
      let sons = n#sub_nodes in
       let rec get_defs_and_target =
        function
           [t] when t#node_type = Pxp_document.T_element "target" ->
            [],t#extension#to_cic_term []
         | s::tl when s#node_type = Pxp_document.T_element "def" ->
            let defs,target = get_defs_and_target tl in
             let id = string_of_xml_attr (s#attribute "id") in
             let binder = cic_attr_of_xml_attr (s#attribute "binder") in
              (id,binder,s#extension#to_cic_term [])::defs, target
         | _  -> raise (IllFormedXml 12)
       in
        let defs,target = get_defs_and_target sons in
         List.fold_right
          (fun (id,b,s) t -> Cic.ALetIn (id,b,s,t))
          defs target
  end
;;

class eltype_instantiate =
  object (self)

    inherit cic_term

    method to_cic_term exp_named_subst =
     assert (exp_named_subst = []) ;
     let n = self#node in
(* CSC: this optional attribute should be parsed and reflected in Cic.annterm
      and id = string_of_xml_attr (n#attribute "id")
*)
       match n#sub_nodes with
          t::l  ->
           let baseUri =
            UriManager.buri_of_uri (uri_of_xml_attr (t#attribute "uri")) in
           let exp_named_subst =
            List.map
             (function
                 n when n#node_type = Pxp_document.T_element "arg" ->
                  let relUri = string_of_xml_attr (n#attribute "relUri") in
                  let uri = UriManager.uri_of_string (baseUri ^ "/" ^ relUri) in
                  let arg =
                   match n#sub_nodes with
                      [ t ]  -> t#extension#to_cic_term []
                    | _  -> raise (IllFormedXml 7)
                  in
                   (uri, arg)
               | _ -> raise (IllFormedXml 7)
             ) l
           in
            t#extension#to_cic_term exp_named_subst
        | _  -> raise (IllFormedXml 7)
  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)) ;
      "instantiate",   (new D.element_impl (new eltype_instantiate)) ;
      "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)) ;
      "decl",          (new D.element_impl (new eltype_transparent)) ;
      "def",           (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))
    ]
   ()
;;