helm/ocaml/cic/cicParser2.ml

   1 (* Copyright (C) 2000, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://cs.unibo.it/helm/.
  24  *)
  25
  26 (******************************************************************************)
  27 (*                                                                            *)
  28 (*                               PROJECT HELM                                 *)
  29 (*                                                                            *)
  30 (*                Claudio Sacerdoti Coen <sacerdot@@cs.unibo.it>              *)
  31 (*                                 24/01/2000                                 *)
  32 (*                                                                            *)
  33 (* This module is the objects level of a parser for cic objects from xml      *)
  34 (* files to the internal representation. It uses the module cicParser3        *)
  35 (* cicParser3 (terms level) and it is used only through cicParser2 (top       *)
  36 (* level).                                                                    *)
  37 (*                                                                            *)
  38 (******************************************************************************)
  39
  40 exception IllFormedXml of int;;
  41 exception NotImplemented;;
  42
  43   (* TODO ZACK implement attributes parsing from XML. ATM, parsing always
  44   * returns the empty list of attributes reported here *)
  45 let obj_attributes = []
  46 let get_obj_attributes (n: 'a Pxp_document.node) =
  47   obj_attributes
  48
  49 (* Utility functions that transform a Pxp attribute into something useful *)
  50
  51 let uri_list_of_attr a =
  52  let module T = Pxp_types in
  53   match a with
  54      T.Value s ->
  55       List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s)
  56    | _ -> raise (IllFormedXml 0)
  57 ;;
  58
  59 let string_of_attr a =
  60  let module T = Pxp_types in
  61   match a with
  62      T.Value s -> s
  63    | _ -> raise (IllFormedXml 0)
  64 ;;
  65
  66 let int_of_attr a =
  67  int_of_string (string_of_attr a)
  68 ;;
  69
  70 let bool_of_attr a =
  71  bool_of_string (string_of_attr a)
  72 ;;
  73
  74 let name_of_attr a =
  75  let module T = Pxp_types in
  76  let module C = Cic in
  77   match a with
  78      T.Value s -> C.Name s
  79    | T.Implied_value -> C.Anonymous
  80    | _ -> raise (IllFormedXml 0)
  81 ;;
  82
  83 (* Other utility functions *)
  84
  85 let get_content n =
  86  match n#sub_nodes with
  87     [ t ] -> t
  88   | _     -> raise (IllFormedXml 1)
  89 ;;
  90
  91 (* Functions that, given the list of sons of a node of the cic dom (objects   *)
  92 (* level), retrieve the internal representation associated to the node.       *)
  93 (* Everytime a cic term subtree is found, it is translated to the internal    *)
  94 (* representation using the method to_cic_term defined in cicParser3.         *)
  95 (* Each function raise IllFormedXml if something goes wrong, but this should  *)
  96 (* be impossible due to the presence of the dtd                               *)
  97 (* The functions should really be obvious looking at their name and the cic   *)
  98 (* dtd                                                                        *)
  99
 100 (* called when a CurrentProof is found *)
 101 let get_conjs_value l =
 102  let rec rget (c, v) l =
 103   let module D = Pxp_document in
 104    match l with
 105       [] -> (c, v)
 106     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
 107        let no = int_of_attr (conj#attribute "no") in
 108        let id = string_of_attr (conj#attribute "id") in
 109        let typ,canonical_context =
 110         match List.rev (conj#sub_nodes) with
 111            [] -> raise (IllFormedXml 13)
 112          | typ::canonical_context ->
 113             (get_content typ)#extension#to_cic_term [],
 114             List.map
 115              (function n ->
 116                let id = string_of_attr (n#attribute "id") in
 117                 match n#node_type with
 118                    D.T_element "Decl" ->
 119                     let name = name_of_attr (n#attribute "name") in
 120                     let term = (get_content n)#extension#to_cic_term [] in
 121                      id, Some (name,Cic.ADecl term)
 122                  | D.T_element "Def" ->
 123                     let name = name_of_attr (n#attribute "name") in
 124                     let term = (get_content n)#extension#to_cic_term [] in
 125                      id, Some (name,Cic.ADef term)
 126                  | D.T_element "Hidden" -> id, None
 127                  | _ -> raise (IllFormedXml 14)
 128              ) canonical_context
 129        in
 130         rget ((id, no, canonical_context, typ)::c, v) tl
 131     | value::tl when value#node_type = D.T_element "body" ->
 132        let v' = (get_content value)#extension#to_cic_term [] in
 133         (match v with
 134             None -> rget (c, Some v') tl
 135           | _    -> raise (IllFormedXml 2)
 136         )
 137     | _ -> raise (IllFormedXml 4)
 138  in
 139   match rget ([], None) l with
 140      (revc, Some v) -> (List.rev revc, v)
 141    | _ -> raise (IllFormedXml 5)
 142 ;;
 143
 144 (* used only by get_inductive_types; called one time for each inductive  *)
 145 (* definitions in a block of inductive definitions                       *)
 146 let get_names_arity_constructors l =
 147  let rec rget (a,c) l =
 148   let module D = Pxp_document in
 149    match l with
 150       [] -> (a, c)
 151     | arity::tl when arity#node_type = D.T_element "arity" ->
 152        let a' = (get_content arity)#extension#to_cic_term [] in
 153         rget (Some a',c) tl
 154     | con::tl when con#node_type = D.T_element "Constructor" ->
 155        let id = string_of_attr (con#attribute "name")
 156        and ty = (get_content con)#extension#to_cic_term [] in
 157          rget (a,(id,ty)::c) tl
 158     | _ -> raise (IllFormedXml 9)
 159  in
 160   match rget (None,[]) l with
 161      (Some a, c) -> (a, List.rev c)
 162    | _ -> raise (IllFormedXml 8)
 163 ;;
 164
 165 (* called when an InductiveDefinition is found *)
 166 let rec get_inductive_types =
 167  function
 168     []     -> []
 169   | he::tl ->
 170      let tyname    = string_of_attr (he#attribute "name")
 171      and inductive = bool_of_attr   (he#attribute "inductive")
 172      and xid = string_of_attr (he#attribute "id")
 173      and (arity,cons) =
 174       get_names_arity_constructors (he#sub_nodes)
 175      in
 176       (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
 177 ;;
 178
 179 (* This is the main function and also the only one used directly from *)
 180 (* cicParser. Given the root of the dom tree, it returns the internal *)
 181 (* representation of the cic object described in the tree             *)
 182 (* It uses the previous functions and the to_cic_term method defined  *)
 183 (* in cicParser3 (used for subtrees that encode cic terms)            *)
 184 let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
 185 =
 186  let module U = UriManager in
 187  let module D = Pxp_document in
 188  let module C = Cic in
 189   let obj_attrs = get_obj_attributes n in
 190   let ntype = n#node_type in
 191   match ntype with
 192     D.T_element "ConstantType" ->
 193       let name = string_of_attr (n # attribute "name") in
 194       let params = uri_list_of_attr (n#attribute "params") in
 195       let xid = string_of_attr (n#attribute "id") in
 196       let typ = (get_content n)#extension#to_cic_term [] in
 197        (match nbody with
 198            None ->
 199             (* Axiom *)
 200             C.AConstant (xid, None, name, None, typ, params, obj_attrs)
 201          | Some nbody' ->
 202             let nbodytype = nbody'#node_type in
 203             match nbodytype with
 204              D.T_element "ConstantBody" ->
 205 (*CSC: the attribute "for" is ignored and not checked
 206               let for_ = string_of_attr (nbody'#attribute "for") in
 207 *)
 208               let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
 209               let xidbody = string_of_attr (nbody'#attribute "id") in
 210               let value = (get_content nbody')#extension#to_cic_term [] in
 211                if paramsbody = params then
 212                 C.AConstant (xid, Some xidbody, name, Some value, typ, params,
 213                   obj_attrs)
 214                else
 215                 raise (IllFormedXml 6)
 216            | D.T_element "CurrentProof" ->
 217 (*CSC: the attribute "of" is ignored and not checked
 218               let for_ = string_of_attr (nbody'#attribute "of") in
 219 *)
 220               let xidbody = string_of_attr (nbody'#attribute "id") in
 221               let sons = nbody'#sub_nodes in
 222                let (conjs, value) = get_conjs_value sons in
 223                 C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params,
 224                   obj_attrs)
 225            | D.T_element _
 226            | D.T_data
 227            | _ -> raise (IllFormedXml 6)
 228        )
 229   | D.T_element "InductiveDefinition" ->
 230      let sons = n#sub_nodes
 231      and xid = string_of_attr (n#attribute "id") in
 232       let inductiveTypes = get_inductive_types sons
 233       and params = uri_list_of_attr (n#attribute "params")
 234       and nparams = int_of_attr (n#attribute "noParams") in
 235        C.AInductiveDefinition (xid, inductiveTypes, params, nparams, obj_attrs)
 236   | D.T_element "Variable" ->
 237      let name = string_of_attr (n#attribute "name")
 238      and params = uri_list_of_attr (n#attribute "params")
 239      and xid = string_of_attr (n#attribute "id")
 240      and (body, typ) =
 241       let sons = n#sub_nodes in
 242        match sons with
 243           [b ; t] when
 244             b#node_type = D.T_element "body" &&
 245             t#node_type = D.T_element "type" ->
 246              let b' = get_content b
 247              and t' = get_content t in
 248               (Some (b'#extension#to_cic_term []), t'#extension#to_cic_term [])
 249         | [t] when t#node_type = D.T_element "type" ->
 250              let t' = get_content t in
 251               (None, t'#extension#to_cic_term [])
 252         | _ -> raise (IllFormedXml 6)
 253      in
 254       C.AVariable (xid,name,body,typ,params,obj_attrs)
 255   | D.T_element _
 256   | D.T_data
 257   | _ -> raise (IllFormedXml 7)
 258 ;;