helm/ocaml/cic/cicParser3.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 terms level of a parser for cic objects from xml        *)
  34 (* files to the internal representation. It is used by the module cicParser2  *)
  35 (* (objects level). It defines an extension of the standard dom using the     *)
  36 (* object-oriented extension machinery of markup: an object with a method     *)
  37 (* to_cic_term that returns the internal representation of the subtree is     *)
  38 (* added to each node of the dom tree                                         *)
  39 (*                                                                            *)
  40 (******************************************************************************)
  41
  42 exception IllFormedXml of int;;
  43
  44 (* The list of tokens of the current section path. *)
  45 (* Used to resolve relative URIs                   *)
  46 let current_sp = ref [];;
  47
  48 (* The uri of the object been parsed *)
  49 let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
  50
  51 (* Utility functions to map a markup attribute to something useful *)
  52
  53 let cic_attr_of_xml_attr =
  54  function
  55     Pxp_types.Value s       -> Cic.Name s
  56   | Pxp_types.Implied_value -> Cic.Anonimous
  57   | _             -> raise (IllFormedXml 1)
  58
  59 let cic_sort_of_xml_attr =
  60  function
  61     Pxp_types.Value "Prop" -> Cic.Prop
  62   | Pxp_types.Value "Set"  -> Cic.Set
  63   | Pxp_types.Value "Type" -> Cic.Type
  64   | _            -> raise (IllFormedXml 2)
  65
  66 let int_of_xml_attr =
  67  function
  68     Pxp_types.Value n -> int_of_string n
  69   | _       -> raise (IllFormedXml 3)
  70
  71 let uri_of_xml_attr =
  72  function
  73     Pxp_types.Value s -> UriManager.uri_of_string s
  74   | _       -> raise (IllFormedXml 4)
  75
  76 let string_of_xml_attr =
  77  function
  78     Pxp_types.Value s -> s
  79   | _       -> raise (IllFormedXml 5)
  80
  81 let binder_of_xml_attr =
  82  function
  83     Pxp_types.Value s -> s
  84   | _       -> raise (IllFormedXml 17)
  85 ;;
  86
  87 (* the "interface" of the class linked to each node of the dom tree *)
  88
  89 class virtual cic_term =
  90   object (self)
  91
  92     (* fields and methods ever required by markup *)
  93     val mutable node = (None : cic_term Pxp_document.node option)
  94
  95     method clone = {< >}
  96     method node =
  97       match node with
  98           None ->
  99             assert false
 100         | Some n -> n
 101     method set_node n =
 102       node <- Some n
 103
 104     (* a method that returns the internal representation of the tree (term) *)
 105     (* rooted in this node                                                  *)
 106     method virtual to_cic_term : Cic.annterm
 107   end
 108 ;;
 109
 110 (* the class of the objects linked to nodes that are not roots of cic terms *)
 111 class eltype_not_of_cic =
 112   object (self)
 113
 114      inherit cic_term
 115
 116      method to_cic_term = raise (IllFormedXml 6)
 117   end
 118 ;;
 119
 120 (* the class of the objects linked to nodes whose content is a cic term *)
 121 (* (syntactic sugar xml entities) e.g. <type> ... </type>               *)
 122 class eltype_transparent =
 123   object (self)
 124
 125     inherit cic_term
 126
 127     method to_cic_term =
 128      let n = self#node in
 129       match n#sub_nodes with
 130          [ t ]  -> t#extension#to_cic_term
 131        | _  -> raise (IllFormedXml 7)
 132   end
 133 ;;
 134
 135 (* A class for each cic node type *)
 136
 137 class eltype_fix =
 138   object (self)
 139
 140     inherit cic_term
 141
 142     method to_cic_term =
 143      let n = self#node in
 144       let nofun = int_of_xml_attr (n#attribute "noFun")
 145       and id = string_of_xml_attr (n#attribute "id")
 146       and functions =
 147        let sons = n#sub_nodes in
 148         List.map
 149          (function
 150              f when f#node_type = Pxp_document.T_element "FixFunction" ->
 151               let name = string_of_xml_attr (f#attribute "name")
 152               and recindex = int_of_xml_attr (f#attribute "recIndex")
 153               and (ty, body) =
 154                match f#sub_nodes with
 155                   [t ; b] when
 156                     t#node_type = Pxp_document.T_element "type" &&
 157                     b#node_type = Pxp_document.T_element "body" ->
 158                      (t#extension#to_cic_term, b#extension#to_cic_term)
 159                 | _ -> raise (IllFormedXml 14)
 160               in
 161                (name, recindex, ty, body)
 162            | _ -> raise (IllFormedXml 13)
 163          ) sons
 164       in
 165        Cic.AFix (id, nofun, functions)
 166   end
 167 ;;
 168
 169 class eltype_cofix =
 170   object (self)
 171
 172     inherit cic_term
 173
 174     method to_cic_term =
 175      let n = self#node in
 176       let nofun = int_of_xml_attr (n#attribute "noFun")
 177       and id = string_of_xml_attr (n#attribute "id")
 178       and functions =
 179        let sons = n#sub_nodes in
 180         List.map
 181          (function
 182              f when f#node_type = Pxp_document.T_element "CofixFunction" ->
 183               let name = string_of_xml_attr (f#attribute "name")
 184               and (ty, body) =
 185                match f#sub_nodes with
 186                   [t ; b] when
 187                     t#node_type = Pxp_document.T_element "type" &&
 188                     b#node_type = Pxp_document.T_element "body" ->
 189                      (t#extension#to_cic_term, b#extension#to_cic_term)
 190                 | _ -> raise (IllFormedXml 16)
 191               in
 192                (name, ty, body)
 193            | _ -> raise (IllFormedXml 15)
 194          ) sons
 195       in
 196        Cic.ACoFix (id, nofun, functions)
 197   end
 198 ;;
 199
 200 class eltype_implicit =
 201   object (self)
 202
 203     inherit cic_term
 204
 205     method to_cic_term =
 206      let n = self#node in
 207       let id = string_of_xml_attr (n#attribute "id") in
 208        Cic.AImplicit id
 209   end
 210 ;;
 211
 212 class eltype_rel =
 213   object (self)
 214
 215     inherit cic_term
 216
 217     method to_cic_term =
 218      let n = self#node in
 219       let value  = int_of_xml_attr (n#attribute "value")
 220       and binder = binder_of_xml_attr (n#attribute "binder")
 221       and id = string_of_xml_attr (n#attribute "id") in
 222        Cic.ARel (id,value,binder)
 223   end
 224 ;;
 225
 226 class eltype_meta =
 227   object (self)
 228
 229     inherit cic_term
 230
 231     method to_cic_term =
 232      let n = self#node in
 233       let value = int_of_xml_attr (n#attribute "no")
 234       and id = string_of_xml_attr (n#attribute "id") in
 235        Cic.AMeta (id,value)
 236   end
 237 ;;
 238
 239 class eltype_var =
 240   object (self)
 241
 242     inherit cic_term
 243
 244     method to_cic_term =
 245      let n = self#node in
 246       let name = string_of_xml_attr (n#attribute "relUri")
 247       and xid = string_of_xml_attr (n#attribute "id") in
 248        match Str.split (Str.regexp ",") name with
 249           [index; id] ->
 250            let get_prefix n =
 251             let rec aux =
 252              function
 253                 (0,_) -> "/"
 254               | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
 255               | _ -> raise (IllFormedXml 19)
 256             in
 257              aux (List.length !current_sp - n,!current_sp)
 258            in
 259             Cic.AVar
 260              (xid,
 261               (UriManager.uri_of_string
 262                ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
 263              )
 264         | _ -> raise (IllFormedXml 18)
 265   end
 266 ;;
 267
 268 class eltype_apply =
 269   object (self)
 270
 271     inherit cic_term
 272
 273     method to_cic_term =
 274      let n = self#node in
 275       let children = n#sub_nodes
 276       and id = string_of_xml_attr (n#attribute "id") in
 277        if List.length children < 2 then raise (IllFormedXml 8)
 278        else
 279         Cic.AAppl
 280          (id,List.map (fun x -> x#extension#to_cic_term) children)
 281   end
 282 ;;
 283
 284 class eltype_cast =
 285   object (self)
 286
 287     inherit cic_term
 288
 289     method to_cic_term =
 290      let n = self#node in
 291       let sons = n#sub_nodes
 292       and id = string_of_xml_attr (n#attribute "id") in
 293        match sons with
 294           [te ; ty] when
 295             te#node_type = Pxp_document.T_element "term" &&
 296             ty#node_type = Pxp_document.T_element "type" ->
 297              let term = te#extension#to_cic_term
 298              and typ  = ty#extension#to_cic_term in
 299               Cic.ACast (id,term,typ)
 300         | _  -> raise (IllFormedXml 9)
 301   end
 302 ;;
 303
 304 class eltype_sort =
 305   object (self)
 306
 307     inherit cic_term
 308
 309     method to_cic_term =
 310      let n = self#node in
 311       let sort = cic_sort_of_xml_attr (n#attribute "value")
 312       and id = string_of_xml_attr (n#attribute "id") in
 313        Cic.ASort (id,sort)
 314   end
 315 ;;
 316
 317 class eltype_abst =
 318   object (self)
 319
 320     inherit cic_term
 321
 322     method to_cic_term =
 323      let n = self#node in
 324       let value = uri_of_xml_attr (n#attribute "uri")
 325       and id = string_of_xml_attr (n#attribute "id") in
 326        Cic.AAbst (id,value)
 327   end
 328 ;;
 329
 330 class eltype_const =
 331   object (self)
 332
 333     inherit cic_term
 334
 335     method to_cic_term =
 336      let module U = UriManager in
 337       let n = self#node in
 338        let value = uri_of_xml_attr (n#attribute "uri")
 339        and id = string_of_xml_attr (n#attribute "id") in
 340         Cic.AConst (id,value, U.relative_depth !current_uri value 0)
 341   end
 342 ;;
 343
 344 class eltype_mutind =
 345   object (self)
 346
 347     inherit cic_term
 348
 349     method to_cic_term =
 350      let module U = UriManager in
 351       let n = self#node in
 352        let name = uri_of_xml_attr (n#attribute "uri")
 353        and noType = int_of_xml_attr (n#attribute "noType")
 354        and id = string_of_xml_attr (n#attribute "id") in
 355         Cic.AMutInd
 356          (id,name, U.relative_depth !current_uri name 0, noType)
 357   end
 358 ;;
 359
 360 class eltype_mutconstruct =
 361   object (self)
 362
 363     inherit cic_term
 364
 365     method to_cic_term =
 366      let module U = UriManager in
 367       let n = self#node in
 368        let name = uri_of_xml_attr (n#attribute "uri")
 369        and noType = int_of_xml_attr (n#attribute "noType")
 370        and noConstr = int_of_xml_attr (n#attribute "noConstr")
 371        and id = string_of_xml_attr (n#attribute "id") in
 372         Cic.AMutConstruct
 373          (id, name, U.relative_depth !current_uri name 0,
 374          noType, noConstr)
 375   end
 376 ;;
 377
 378 class eltype_prod =
 379   object (self)
 380
 381     inherit cic_term
 382
 383     method to_cic_term =
 384      let n = self#node in
 385       let sons = n#sub_nodes
 386       and id = string_of_xml_attr (n#attribute "id") in
 387        match sons with
 388           [s ; t] when
 389             s#node_type = Pxp_document.T_element "source" &&
 390             t#node_type = Pxp_document.T_element "target" ->
 391              let name = cic_attr_of_xml_attr (t#attribute "binder")
 392              and source = s#extension#to_cic_term
 393              and target = t#extension#to_cic_term in
 394               Cic.AProd (id,name,source,target)
 395         | _  -> raise (IllFormedXml 10)
 396   end
 397 ;;
 398
 399 class eltype_mutcase =
 400   object (self)
 401
 402     inherit cic_term
 403
 404     method to_cic_term =
 405      let module U = UriManager in
 406       let n = self#node in
 407        let sons = n#sub_nodes
 408        and id = string_of_xml_attr (n#attribute "id") in
 409         match sons with
 410            ty::te::patterns when
 411              ty#node_type = Pxp_document.T_element "patternsType" &&
 412              te#node_type = Pxp_document.T_element "inductiveTerm" ->
 413               let ci = uri_of_xml_attr (n#attribute "uriType")
 414               and typeno = int_of_xml_attr (n#attribute "noType")
 415               and inductiveType = ty#extension#to_cic_term
 416               and inductiveTerm = te#extension#to_cic_term
 417               and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
 418               in
 419                Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0,
 420                 typeno,inductiveType,inductiveTerm,lpattern)
 421          | _  -> raise (IllFormedXml 11)
 422   end
 423 ;;
 424
 425 class eltype_lambda =
 426   object (self)
 427
 428     inherit cic_term
 429
 430     method to_cic_term =
 431      let n = self#node in
 432       let sons = n#sub_nodes
 433       and id = string_of_xml_attr (n#attribute "id") in
 434        match sons with
 435           [s ; t] when
 436             s#node_type = Pxp_document.T_element "source" &&
 437             t#node_type = Pxp_document.T_element "target" ->
 438              let name = cic_attr_of_xml_attr (t#attribute "binder")
 439              and source = s#extension#to_cic_term
 440              and target = t#extension#to_cic_term in
 441               Cic.ALambda (id,name,source,target)
 442         | _  -> raise (IllFormedXml 12)
 443   end
 444 ;;
 445
 446 class eltype_letin =
 447   object (self)
 448
 449     inherit cic_term
 450
 451     method to_cic_term =
 452      let n = self#node in
 453       let sons = n#sub_nodes
 454       and id = string_of_xml_attr (n#attribute "id") in
 455        match sons with
 456           [s ; t] when
 457             s#node_type = Pxp_document.T_element "term" &&
 458             t#node_type = Pxp_document.T_element "letintarget" ->
 459              let name = cic_attr_of_xml_attr (t#attribute "binder")
 460              and source = s#extension#to_cic_term
 461              and target = t#extension#to_cic_term in
 462               Cic.ALetIn (id,name,source,target)
 463         | _  -> raise (IllFormedXml 12)
 464   end
 465 ;;
 466
 467 (* The definition of domspec, an hashtable that maps each node type to the *)
 468 (* object that must be linked to it. Used by markup.                       *)
 469
 470 let domspec =
 471  let module D = Pxp_document in
 472   D.make_spec_from_alist
 473    ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
 474    ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
 475    ~element_alist:
 476     [ "REL",           (new D.element_impl (new eltype_rel)) ;
 477       "VAR",           (new D.element_impl (new eltype_var)) ;
 478       "META",          (new D.element_impl (new eltype_meta)) ;
 479       "SORT",          (new D.element_impl (new eltype_sort)) ;
 480       "IMPLICIT",      (new D.element_impl (new eltype_implicit)) ;
 481       "CAST",          (new D.element_impl (new eltype_cast)) ;
 482       "PROD",          (new D.element_impl (new eltype_prod)) ;
 483       "LAMBDA",        (new D.element_impl (new eltype_lambda)) ;
 484       "LETIN",         (new D.element_impl (new eltype_letin)) ;
 485       "APPLY",         (new D.element_impl (new eltype_apply)) ;
 486       "CONST",         (new D.element_impl (new eltype_const)) ;
 487       "ABST",          (new D.element_impl (new eltype_abst)) ;
 488       "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
 489       "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
 490       "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;
 491       "FIX",           (new D.element_impl (new eltype_fix)) ;
 492       "COFIX",         (new D.element_impl (new eltype_cofix)) ;
 493       "arity",         (new D.element_impl (new eltype_transparent)) ;
 494       "term",          (new D.element_impl (new eltype_transparent)) ;
 495       "type",          (new D.element_impl (new eltype_transparent)) ;
 496       "body",          (new D.element_impl (new eltype_transparent)) ;
 497       "source",        (new D.element_impl (new eltype_transparent)) ;
 498       "target",        (new D.element_impl (new eltype_transparent)) ;
 499       "letintarget",   (new D.element_impl (new eltype_transparent)) ;
 500       "patternsType",  (new D.element_impl (new eltype_transparent)) ;
 501       "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
 502       "pattern",       (new D.element_impl (new eltype_transparent))
 503     ]
 504    ()
 505 ;;