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 (* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...."      *)
  46 (* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *)
  47 let mk_absolute_uris s =
  48  let l = (Str.split (Str.regexp ":") s) in
  49   let absolute_of_relative n v =
  50    let module P3 = CicParser3 in
  51     let rec mkburi =
  52      function
  53         (0,_) -> "/"
  54       | (n,he::tl) when n > 0 ->
  55          "/" ^ he ^ mkburi (n - 1, tl)
  56       | _ -> raise (IllFormedXml 12)
  57     in
  58      let m = List.length !P3.current_sp - (int_of_string n) in
  59       let buri = mkburi (m, !P3.current_sp) in
  60        UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var")
  61   in
  62    let rec absolutize =
  63     function
  64        [] -> []
  65      | [no ; vs] ->
  66         let vars = (Str.split (Str.regexp " ") vs) in
  67          [(int_of_string no, List.map (absolute_of_relative no) vars)]
  68      | no::vs::tl ->
  69         let vars = (Str.split (Str.regexp " ") vs) in
  70          let rec add_prefix =
  71           function
  72              [no2] -> ([], no2)
  73            | he::tl ->
  74               let (pvars, no2) = add_prefix tl in
  75                ((absolute_of_relative no he)::pvars, no2)
  76            | _ -> raise (IllFormedXml 11)
  77          in
  78           let (pvars, no2) = add_prefix vars in
  79            (int_of_string no, pvars)::(absolutize (no2::tl))
  80      | _ -> raise (IllFormedXml 10)
  81    in
  82     (* last parameter must be applied first *)
  83     absolutize l
  84 ;;
  85
  86 let option_uri_list_of_attr a1 a2 =
  87  let module T = Pxp_types in
  88   let parameters =
  89    match a1 with
  90       T.Value s -> mk_absolute_uris s
  91     | _ -> raise (IllFormedXml 0)
  92   in
  93    match a2 with
  94       T.Value "POSSIBLE" -> Cic.Possible parameters
  95     | T.Implied_value -> Cic.Actual parameters
  96     | _ -> raise (IllFormedXml 0)
  97 ;;
  98
  99 let uri_list_of_attr a =
 100  let module T = Pxp_types in
 101   match a with
 102      T.Value s -> mk_absolute_uris s
 103    | _ -> raise (IllFormedXml 0)
 104 ;;
 105
 106 let string_of_attr a =
 107  let module T = Pxp_types in
 108   match a with
 109      T.Value s -> s
 110    | _ -> raise (IllFormedXml 0)
 111 ;;
 112
 113 let int_of_attr a =
 114  int_of_string (string_of_attr a)
 115 ;;
 116
 117 let bool_of_attr a =
 118  bool_of_string (string_of_attr a)
 119 ;;
 120
 121 let name_of_attr a =
 122  let module T = Pxp_types in
 123  let module C = Cic in
 124   match a with
 125      T.Value s -> C.Name s
 126    | T.Implied_value -> C.Anonimous
 127    | _ -> raise (IllFormedXml 0)
 128 ;;
 129
 130 (* Other utility functions *)
 131
 132 let get_content n =
 133  match n#sub_nodes with
 134     [ t ] -> t
 135   | _     -> raise (IllFormedXml 1)
 136 ;;
 137
 138 (* Functions that, given the list of sons of a node of the cic dom (objects   *)
 139 (* level), retrieve the internal representation associated to the node.       *)
 140 (* Everytime a cic term subtree is found, it is translated to the internal    *)
 141 (* representation using the method to_cic_term defined in cicParser3.         *)
 142 (* Each function raise IllFormedXml if something goes wrong, but this should  *)
 143 (* be impossible due to the presence of the dtd                               *)
 144 (* The functions should really be obvious looking at their name and the cic   *)
 145 (* dtd                                                                        *)
 146
 147 (* called when a CurrentProof is found *)
 148 let get_conjs_value_type l =
 149  let rec rget (c, v, t) l =
 150   let module D = Pxp_document in
 151    match l with
 152       [] -> (c, v, t)
 153     | conj::tl when conj#node_type = D.T_element "Conjecture" ->
 154        let no = int_of_attr (conj#attribute "no") in
 155        let xid = string_of_attr (conj#attribute "id") in
 156        let typ,canonical_context =
 157         match List.rev (conj#sub_nodes) with
 158            [] -> raise (IllFormedXml 13)
 159          | typ::canonical_context ->
 160             (get_content typ)#extension#to_cic_term,
 161             List.map
 162              (function n ->
 163                match n#node_type with
 164                   D.T_element "Decl" ->
 165                    let name = name_of_attr (n#attribute "name") in
 166                    let hid = string_of_attr (n#attribute "id") in
 167                    let term = (get_content n)#extension#to_cic_term in
 168                     hid,Some (name,Cic.ADecl term)
 169                 | D.T_element "Def" ->
 170                    let name = name_of_attr (n#attribute "name") in
 171                    let hid = string_of_attr (n#attribute "id") in
 172                    let term = (get_content n)#extension#to_cic_term in
 173                     hid,Some (name,Cic.ADef term)
 174                 | D.T_element "Hidden" ->
 175                    let hid = string_of_attr (n#attribute "id") in
 176                     hid,None
 177                 | _ -> raise (IllFormedXml 14)
 178              ) canonical_context
 179        in
 180         rget ((xid, no, canonical_context, typ)::c, v, t) tl
 181     | value::tl when value#node_type = D.T_element "body" ->
 182        let v' = (get_content value)#extension#to_cic_term in
 183         (match v with
 184             None -> rget (c, Some v', t) tl
 185           | _    -> raise (IllFormedXml 2)
 186         )
 187     | typ::tl when typ#node_type = D.T_element "type" ->
 188        let t' = (get_content typ)#extension#to_cic_term in
 189         (match t with
 190             None -> rget (c, v, Some t') tl
 191           | _    -> raise (IllFormedXml 3)
 192         )
 193     | _ -> raise (IllFormedXml 4)
 194  in
 195   match rget ([], None, None) l with
 196      (revc, Some v, Some t) -> (List.rev revc, v, t)
 197    | _ -> raise (IllFormedXml 5)
 198 ;;
 199
 200 (* used only by get_inductive_types; called one time for each inductive  *)
 201 (* definitions in a block of inductive definitions                       *)
 202 let get_names_arity_constructors l =
 203  let rec rget (a,c) l =
 204   let module D = Pxp_document in
 205    match l with
 206       [] -> (a, c)
 207     | arity::tl when arity#node_type = D.T_element "arity" ->
 208        let a' = (get_content arity)#extension#to_cic_term in
 209         rget (Some a',c) tl
 210     | con::tl when con#node_type = D.T_element "Constructor" ->
 211        let id = string_of_attr (con#attribute "name")
 212        and ty = (get_content con)#extension#to_cic_term in
 213          rget (a,(id,ty,ref None)::c) tl
 214     | _ -> raise (IllFormedXml 9)
 215  in
 216   match rget (None,[]) l with
 217      (Some a, c) -> (a, List.rev c)
 218    | _ -> raise (IllFormedXml 8)
 219 ;;
 220
 221 (* called when an InductiveDefinition is found *)
 222 let rec get_inductive_types =
 223  function
 224     []     -> []
 225   | he::tl ->
 226      let tyname    = string_of_attr (he#attribute "name")
 227      and inductive = bool_of_attr   (he#attribute "inductive")
 228      and (arity,cons) =
 229       get_names_arity_constructors (he#sub_nodes)
 230      in
 231       (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
 232 ;;
 233
 234 (* This is the main function and also the only one used directly from *)
 235 (* cicParser. Given the root of the dom tree, it returns the internal *)
 236 (* representation of the cic object described in the tree             *)
 237 (* It uses the previous functions and the to_cic_term method defined  *)
 238 (* in cicParser3 (used for subtrees that encode cic terms)            *)
 239 let rec get_term n =
 240  let module D = Pxp_document in
 241  let module C = Cic in
 242   let ntype = n # node_type in
 243   match ntype with
 244     D.T_element "Definition" ->
 245       let id = string_of_attr (n # attribute "name")
 246       and params =
 247        option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode")
 248       and (value, typ) =
 249        let sons = n#sub_nodes in
 250         match sons with
 251           [v ; t] when
 252             v#node_type = D.T_element "body" &&
 253             t#node_type = D.T_element "type" ->
 254              let v' = get_content v
 255              and t' = get_content t in
 256               (v'#extension#to_cic_term, t'#extension#to_cic_term)
 257         | _ -> raise (IllFormedXml 6)
 258       and xid = string_of_attr (n#attribute "id") in
 259        C.ADefinition (xid, id, value, typ, params)
 260   | D.T_element "Axiom" ->
 261       let id = string_of_attr (n # attribute "name")
 262       and params = uri_list_of_attr (n # attribute "params")
 263       and typ =
 264        (get_content (get_content n))#extension#to_cic_term
 265       and xid = string_of_attr (n#attribute "id") in
 266        C.AAxiom (xid, id, typ, params)
 267   | D.T_element "CurrentProof" ->
 268      let name = string_of_attr (n#attribute "name")
 269      and xid = string_of_attr (n#attribute "id") in
 270      let sons = n#sub_nodes in
 271       let (conjs, value, typ) = get_conjs_value_type sons in
 272        C.ACurrentProof (xid, name, conjs, value, typ)
 273   | D.T_element "InductiveDefinition" ->
 274      let sons = n#sub_nodes
 275      and xid = string_of_attr (n#attribute "id") in
 276       let inductiveTypes = get_inductive_types sons
 277       and params = uri_list_of_attr (n#attribute "params")
 278       and nparams = int_of_attr (n#attribute "noParams") in
 279        C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
 280   | D.T_element "Variable" ->
 281      let name = string_of_attr (n#attribute "name")
 282      and xid = string_of_attr (n#attribute "id")
 283      and (body, typ) =
 284       let sons = n#sub_nodes in
 285        match sons with
 286           [b ; t] when
 287             b#node_type = D.T_element "body" &&
 288             t#node_type = D.T_element "type" ->
 289              let b' = get_content b
 290              and t' = get_content t in
 291               (Some (b'#extension#to_cic_term), t'#extension#to_cic_term)
 292         | [t] when t#node_type = D.T_element "type" ->
 293              let t' = get_content t in
 294               (None, t'#extension#to_cic_term)
 295         | _ -> raise (IllFormedXml 6)
 296      in
 297       C.AVariable (xid,name,body,typ)
 298   | D.T_element _
 299   | D.T_data
 300   | _ ->
 301      raise (IllFormedXml 7)
 302 ;;