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")
 235       in
 236        let local_context =
 237         let sons = n#sub_nodes in
 238          List.map
 239           (function substitution ->
 240             match substitution#sub_nodes with
 241                [] -> None
 242              | [he] -> Some he#extension#to_cic_term
 243              | _ -> raise (IllFormedXml 20)
 244           ) sons
 245        in
 246         Cic.AMeta (id,value,local_context)
 247   end
 248 ;;
 249
 250 class eltype_var =
 251   object (self)
 252
 253     inherit cic_term
 254
 255     method to_cic_term =
 256      let n = self#node in
 257       let name = string_of_xml_attr (n#attribute "relUri")
 258       and xid = string_of_xml_attr (n#attribute "id") in
 259        match Str.split (Str.regexp ",") name with
 260           [index; id] ->
 261            let get_prefix n =
 262             let rec aux =
 263              function
 264                 (0,_) -> "/"
 265               | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
 266               | _ -> raise (IllFormedXml 19)
 267             in
 268              aux (List.length !current_sp - n,!current_sp)
 269            in
 270             Cic.AVar
 271              (xid,
 272               (UriManager.uri_of_string
 273                ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
 274              )
 275         | _ -> raise (IllFormedXml 18)
 276   end
 277 ;;
 278
 279 class eltype_apply =
 280   object (self)
 281
 282     inherit cic_term
 283
 284     method to_cic_term =
 285      let n = self#node in
 286       let children = n#sub_nodes
 287       and id = string_of_xml_attr (n#attribute "id") in
 288        if List.length children < 2 then raise (IllFormedXml 8)
 289        else
 290         Cic.AAppl
 291          (id,List.map (fun x -> x#extension#to_cic_term) children)
 292   end
 293 ;;
 294
 295 class eltype_cast =
 296   object (self)
 297
 298     inherit cic_term
 299
 300     method to_cic_term =
 301      let n = self#node in
 302       let sons = n#sub_nodes
 303       and id = string_of_xml_attr (n#attribute "id") in
 304        match sons with
 305           [te ; ty] when
 306             te#node_type = Pxp_document.T_element "term" &&
 307             ty#node_type = Pxp_document.T_element "type" ->
 308              let term = te#extension#to_cic_term
 309              and typ  = ty#extension#to_cic_term in
 310               Cic.ACast (id,term,typ)
 311         | _  -> raise (IllFormedXml 9)
 312   end
 313 ;;
 314
 315 class eltype_sort =
 316   object (self)
 317
 318     inherit cic_term
 319
 320     method to_cic_term =
 321      let n = self#node in
 322       let sort = cic_sort_of_xml_attr (n#attribute "value")
 323       and id = string_of_xml_attr (n#attribute "id") in
 324        Cic.ASort (id,sort)
 325   end
 326 ;;
 327
 328 class eltype_abst =
 329   object (self)
 330
 331     inherit cic_term
 332
 333     method to_cic_term =
 334      let n = self#node in
 335       let value = uri_of_xml_attr (n#attribute "uri")
 336       and id = string_of_xml_attr (n#attribute "id") in
 337        Cic.AAbst (id,value)
 338   end
 339 ;;
 340
 341 class eltype_const =
 342   object (self)
 343
 344     inherit cic_term
 345
 346     method to_cic_term =
 347      let module U = UriManager in
 348       let n = self#node in
 349        let value = uri_of_xml_attr (n#attribute "uri")
 350        and id = string_of_xml_attr (n#attribute "id") in
 351         Cic.AConst (id,value, U.relative_depth !current_uri value 0)
 352   end
 353 ;;
 354
 355 class eltype_mutind =
 356   object (self)
 357
 358     inherit cic_term
 359
 360     method to_cic_term =
 361      let module U = UriManager in
 362       let n = self#node in
 363        let name = uri_of_xml_attr (n#attribute "uri")
 364        and noType = int_of_xml_attr (n#attribute "noType")
 365        and id = string_of_xml_attr (n#attribute "id") in
 366         Cic.AMutInd
 367          (id,name, U.relative_depth !current_uri name 0, noType)
 368   end
 369 ;;
 370
 371 class eltype_mutconstruct =
 372   object (self)
 373
 374     inherit cic_term
 375
 376     method to_cic_term =
 377      let module U = UriManager in
 378       let n = self#node in
 379        let name = uri_of_xml_attr (n#attribute "uri")
 380        and noType = int_of_xml_attr (n#attribute "noType")
 381        and noConstr = int_of_xml_attr (n#attribute "noConstr")
 382        and id = string_of_xml_attr (n#attribute "id") in
 383         Cic.AMutConstruct
 384          (id, name, U.relative_depth !current_uri name 0,
 385          noType, noConstr)
 386   end
 387 ;;
 388
 389 class eltype_prod =
 390   object (self)
 391
 392     inherit cic_term
 393
 394     method to_cic_term =
 395      let n = self#node in
 396       let sons = n#sub_nodes
 397       and id = string_of_xml_attr (n#attribute "id") in
 398        match sons with
 399           [s ; t] when
 400             s#node_type = Pxp_document.T_element "source" &&
 401             t#node_type = Pxp_document.T_element "target" ->
 402              let name = cic_attr_of_xml_attr (t#attribute "binder")
 403              and source = s#extension#to_cic_term
 404              and target = t#extension#to_cic_term in
 405               Cic.AProd (id,name,source,target)
 406         | _  -> raise (IllFormedXml 10)
 407   end
 408 ;;
 409
 410 class eltype_mutcase =
 411   object (self)
 412
 413     inherit cic_term
 414
 415     method to_cic_term =
 416      let module U = UriManager in
 417       let n = self#node in
 418        let sons = n#sub_nodes
 419        and id = string_of_xml_attr (n#attribute "id") in
 420         match sons with
 421            ty::te::patterns when
 422              ty#node_type = Pxp_document.T_element "patternsType" &&
 423              te#node_type = Pxp_document.T_element "inductiveTerm" ->
 424               let ci = uri_of_xml_attr (n#attribute "uriType")
 425               and typeno = int_of_xml_attr (n#attribute "noType")
 426               and inductiveType = ty#extension#to_cic_term
 427               and inductiveTerm = te#extension#to_cic_term
 428               and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
 429               in
 430                Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0,
 431                 typeno,inductiveType,inductiveTerm,lpattern)
 432          | _  -> raise (IllFormedXml 11)
 433   end
 434 ;;
 435
 436 class eltype_lambda =
 437   object (self)
 438
 439     inherit cic_term
 440
 441     method to_cic_term =
 442      let n = self#node in
 443       let sons = n#sub_nodes
 444       and id = string_of_xml_attr (n#attribute "id") in
 445        match sons with
 446           [s ; t] when
 447             s#node_type = Pxp_document.T_element "source" &&
 448             t#node_type = Pxp_document.T_element "target" ->
 449              let name = cic_attr_of_xml_attr (t#attribute "binder")
 450              and source = s#extension#to_cic_term
 451              and target = t#extension#to_cic_term in
 452               Cic.ALambda (id,name,source,target)
 453         | _  -> raise (IllFormedXml 12)
 454   end
 455 ;;
 456
 457 class eltype_letin =
 458   object (self)
 459
 460     inherit cic_term
 461
 462     method to_cic_term =
 463      let n = self#node in
 464       let sons = n#sub_nodes
 465       and id = string_of_xml_attr (n#attribute "id") in
 466        match sons with
 467           [s ; t] when
 468             s#node_type = Pxp_document.T_element "term" &&
 469             t#node_type = Pxp_document.T_element "letintarget" ->
 470              let name = cic_attr_of_xml_attr (t#attribute "binder")
 471              and source = s#extension#to_cic_term
 472              and target = t#extension#to_cic_term in
 473               Cic.ALetIn (id,name,source,target)
 474         | _  -> raise (IllFormedXml 12)
 475   end
 476 ;;
 477
 478 (* The definition of domspec, an hashtable that maps each node type to the *)
 479 (* object that must be linked to it. Used by markup.                       *)
 480
 481 let domspec =
 482  let module D = Pxp_document in
 483   D.make_spec_from_alist
 484    ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
 485    ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
 486    ~element_alist:
 487     [ "REL",           (new D.element_impl (new eltype_rel)) ;
 488       "VAR",           (new D.element_impl (new eltype_var)) ;
 489       "META",          (new D.element_impl (new eltype_meta)) ;
 490       "SORT",          (new D.element_impl (new eltype_sort)) ;
 491       "IMPLICIT",      (new D.element_impl (new eltype_implicit)) ;
 492       "CAST",          (new D.element_impl (new eltype_cast)) ;
 493       "PROD",          (new D.element_impl (new eltype_prod)) ;
 494       "LAMBDA",        (new D.element_impl (new eltype_lambda)) ;
 495       "LETIN",         (new D.element_impl (new eltype_letin)) ;
 496       "APPLY",         (new D.element_impl (new eltype_apply)) ;
 497       "CONST",         (new D.element_impl (new eltype_const)) ;
 498       "ABST",          (new D.element_impl (new eltype_abst)) ;
 499       "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
 500       "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
 501       "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;
 502       "FIX",           (new D.element_impl (new eltype_fix)) ;
 503       "COFIX",         (new D.element_impl (new eltype_cofix)) ;
 504       "arity",         (new D.element_impl (new eltype_transparent)) ;
 505       "term",          (new D.element_impl (new eltype_transparent)) ;
 506       "type",          (new D.element_impl (new eltype_transparent)) ;
 507       "body",          (new D.element_impl (new eltype_transparent)) ;
 508       "source",        (new D.element_impl (new eltype_transparent)) ;
 509       "target",        (new D.element_impl (new eltype_transparent)) ;
 510       "letintarget",   (new D.element_impl (new eltype_transparent)) ;
 511       "patternsType",  (new D.element_impl (new eltype_transparent)) ;
 512       "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
 513       "pattern",       (new D.element_impl (new eltype_transparent))
 514     ]
 515    ()
 516 ;;