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 (* Utility functions that transform a Pxp attribute into something useful *)
  44
  45 let uri_list_of_attr a =
  46  let module T = Pxp_types in
  47   match a with
  48      T.Value s ->
  49       List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s)
  50    | _ -> raise (IllFormedXml 0)
  51 ;;
  52
  53 let string_of_attr a =
  54  let module T = Pxp_types in
  55   match a with
  56      T.Value s -> s
  57    | _ -> raise (IllFormedXml 0)
  58 ;;
  59
  60 let int_of_attr a =
  61  int_of_string (string_of_attr a)
  62 ;;
  63
  64 let bool_of_attr a =
  65  bool_of_string (string_of_attr a)
  66 ;;
  67
  68 let name_of_attr a =
  69  let module T = Pxp_types in
  70  let module C = Cic in
  71   match a with
  72      T.Value s -> C.Name s
  73    | T.Implied_value -> C.Anonymous
  74    | _ -> raise (IllFormedXml 0)
  75 ;;
  76
  77 (* Other utility functions *)
  78
  79 let get_content n =
  80  match n#sub_nodes with
  81     [ t ] -> t
  82   | _     -> raise (IllFormedXml 1)
  83 ;;
  84
  85 (* Functions that, given the list of sons of a node of the cic dom (objects   *)
  86 (* level), retrieve the internal representation associated to the node.       *)
  87 (* Everytime a cic term subtree is found, it is translated to the internal    *)
  88 (* representation using the method to_cic_term defined in cicParser3.         *)
  89 (* Each function raise IllFormedXml if something goes wrong, but this should  *)
  90 (* be impossible due to the presence of the dtd                               *)
  91 (* The functions should really be obvious looking at their name and the cic   *)
  92 (* dtd                                                                        *)
  93
  94 (* called when a CurrentProof is found *)
  95 let get_conjs_value l =
  96  let rec rget (c, v) l =
  97   let module D = Pxp_document in
  98    match l with
  99       [] -> (c, v)
 100     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
 101        let no = int_of_attr (conj#attribute "no") in
 102        let id = string_of_attr (conj#attribute "id") in
 103        let typ,canonical_context =
 104         match List.rev (conj#sub_nodes) with
 105            [] -> raise (IllFormedXml 13)
 106          | typ::canonical_context ->
 107             (get_content typ)#extension#to_cic_term [],
 108             List.map
 109              (function n ->
 110                let id = string_of_attr (n#attribute "id") in
 111                 match n#node_type with
 112                    D.T_element "Decl" ->
 113                     let name = name_of_attr (n#attribute "name") in
 114                     let term = (get_content n)#extension#to_cic_term [] in
 115                      id, Some (name,Cic.ADecl term)
 116                  | D.T_element "Def" ->
 117                     let name = name_of_attr (n#attribute "name") in
 118                     let term = (get_content n)#extension#to_cic_term [] in
 119                      id, Some (name,Cic.ADef term)
 120                  | D.T_element "Hidden" -> id, None
 121                  | _ -> raise (IllFormedXml 14)
 122              ) canonical_context
 123        in
 124         rget ((id, no, canonical_context, typ)::c, v) tl
 125     | value::tl when value#node_type = D.T_element "body" ->
 126        let v' = (get_content value)#extension#to_cic_term [] in
 127         (match v with
 128             None -> rget (c, Some v') tl
 129           | _    -> raise (IllFormedXml 2)
 130         )
 131     | _ -> raise (IllFormedXml 4)
 132  in
 133   match rget ([], None) l with
 134      (revc, Some v) -> (List.rev revc, v)
 135    | _ -> raise (IllFormedXml 5)
 136 ;;
 137
 138 (* used only by get_inductive_types; called one time for each inductive  *)
 139 (* definitions in a block of inductive definitions                       *)
 140 let get_names_arity_constructors l =
 141  let rec rget (a,c) l =
 142   let module D = Pxp_document in
 143    match l with
 144       [] -> (a, c)
 145     | arity::tl when arity#node_type = D.T_element "arity" ->
 146        let a' = (get_content arity)#extension#to_cic_term [] in
 147         rget (Some a',c) tl
 148     | con::tl when con#node_type = D.T_element "Constructor" ->
 149        let id = string_of_attr (con#attribute "name")
 150        and ty = (get_content con)#extension#to_cic_term [] in
 151          rget (a,(id,ty)::c) tl
 152     | _ -> raise (IllFormedXml 9)
 153  in
 154   match rget (None,[]) l with
 155      (Some a, c) -> (a, List.rev c)
 156    | _ -> raise (IllFormedXml 8)
 157 ;;
 158
 159 (* called when an InductiveDefinition is found *)
 160 let rec get_inductive_types =
 161  function
 162     []     -> []
 163   | he::tl ->
 164      let tyname    = string_of_attr (he#attribute "name")
 165      and inductive = bool_of_attr   (he#attribute "inductive")
 166      and xid = string_of_attr (he#attribute "id")
 167      and (arity,cons) =
 168       get_names_arity_constructors (he#sub_nodes)
 169      in
 170       (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
 171 ;;
 172
 173 (* This is the main function and also the only one used directly from *)
 174 (* cicParser. Given the root of the dom tree, it returns the internal *)
 175 (* representation of the cic object described in the tree             *)
 176 (* It uses the previous functions and the to_cic_term method defined  *)
 177 (* in cicParser3 (used for subtrees that encode cic terms)            *)
 178 let rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
 179 =
 180  let module U = UriManager in
 181  let module D = Pxp_document in
 182  let module C = Cic in
 183   let ntype = n#node_type in
 184   match ntype with
 185     D.T_element "ConstantType" ->
 186       let name = string_of_attr (n # attribute "name") in
 187       let params = uri_list_of_attr (n#attribute "params") in
 188       let xid = string_of_attr (n#attribute "id") in
 189       let typ = (get_content n)#extension#to_cic_term [] in
 190        (match nbody with
 191            None ->
 192             (* Axiom *)
 193             C.AConstant (xid, None, name, None, typ, params)
 194          | Some nbody' ->
 195             let nbodytype = nbody'#node_type in
 196             match nbodytype with
 197              D.T_element "ConstantBody" ->
 198 (*CSC: the attribute "for" is ignored and not checked
 199               let for_ = string_of_attr (nbody'#attribute "for") in
 200 *)
 201               let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
 202               let xidbody = string_of_attr (nbody'#attribute "id") in
 203               let value = (get_content nbody')#extension#to_cic_term [] in
 204                if paramsbody = params then
 205                 C.AConstant (xid, Some xidbody, name, Some value, typ, params)
 206                else
 207                 raise (IllFormedXml 6)
 208            | D.T_element "CurrentProof" ->
 209 (*CSC: the attribute "of" is ignored and not checked
 210               let for_ = string_of_attr (nbody'#attribute "of") in
 211 *)
 212               let xidbody = string_of_attr (nbody'#attribute "id") in
 213               let sons = nbody'#sub_nodes in
 214                let (conjs, value) = get_conjs_value sons in
 215                 C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
 216            | D.T_element _
 217            | D.T_data
 218            | _ -> raise (IllFormedXml 6)
 219        )
 220   | D.T_element "InductiveDefinition" ->
 221      let sons = n#sub_nodes
 222      and xid = string_of_attr (n#attribute "id") in
 223       let inductiveTypes = get_inductive_types sons
 224       and params = uri_list_of_attr (n#attribute "params")
 225       and nparams = int_of_attr (n#attribute "noParams") in
 226        C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
 227   | D.T_element "Variable" ->
 228      let name = string_of_attr (n#attribute "name")
 229      and params = uri_list_of_attr (n#attribute "params")
 230      and xid = string_of_attr (n#attribute "id")
 231      and (body, typ) =
 232       let sons = n#sub_nodes in
 233        match sons with
 234           [b ; t] when
 235             b#node_type = D.T_element "body" &&
 236             t#node_type = D.T_element "type" ->
 237              let b' = get_content b
 238              and t' = get_content t in
 239               (Some (b'#extension#to_cic_term []), t'#extension#to_cic_term [])
 240         | [t] when t#node_type = D.T_element "type" ->
 241              let t' = get_content t in
 242               (None, t'#extension#to_cic_term [])
 243         | _ -> raise (IllFormedXml 6)
 244      in
 245       C.AVariable (xid,name,body,typ,params)
 246   | D.T_element _
 247   | D.T_data
 248   | _ -> raise (IllFormedXml 7)
 249 ;;