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