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_const =
 329   object (self)
 330
 331     inherit cic_term
 332
 333     method to_cic_term =
 334      let module U = UriManager in
 335       let n = self#node in
 336        let value = uri_of_xml_attr (n#attribute "uri")
 337        and id = string_of_xml_attr (n#attribute "id") in
 338         Cic.AConst (id,value, U.relative_depth !current_uri value 0)
 339   end
 340 ;;
 341
 342 class eltype_mutind =
 343   object (self)
 344
 345     inherit cic_term
 346
 347     method to_cic_term =
 348      let module U = UriManager in
 349       let n = self#node in
 350        let name = uri_of_xml_attr (n#attribute "uri")
 351        and noType = int_of_xml_attr (n#attribute "noType")
 352        and id = string_of_xml_attr (n#attribute "id") in
 353         Cic.AMutInd
 354          (id,name, U.relative_depth !current_uri name 0, noType)
 355   end
 356 ;;
 357
 358 class eltype_mutconstruct =
 359   object (self)
 360
 361     inherit cic_term
 362
 363     method to_cic_term =
 364      let module U = UriManager in
 365       let n = self#node in
 366        let name = uri_of_xml_attr (n#attribute "uri")
 367        and noType = int_of_xml_attr (n#attribute "noType")
 368        and noConstr = int_of_xml_attr (n#attribute "noConstr")
 369        and id = string_of_xml_attr (n#attribute "id") in
 370         Cic.AMutConstruct
 371          (id, name, U.relative_depth !current_uri name 0,
 372          noType, noConstr)
 373   end
 374 ;;
 375
 376 class eltype_prod =
 377   object (self)
 378
 379     inherit cic_term
 380
 381     method to_cic_term =
 382      let n = self#node in
 383       let sons = n#sub_nodes
 384       and id = string_of_xml_attr (n#attribute "id") in
 385        match sons with
 386           [s ; t] when
 387             s#node_type = Pxp_document.T_element "source" &&
 388             t#node_type = Pxp_document.T_element "target" ->
 389              let name = cic_attr_of_xml_attr (t#attribute "binder")
 390              and source = s#extension#to_cic_term
 391              and target = t#extension#to_cic_term in
 392               Cic.AProd (id,name,source,target)
 393         | _  -> raise (IllFormedXml 10)
 394   end
 395 ;;
 396
 397 class eltype_mutcase =
 398   object (self)
 399
 400     inherit cic_term
 401
 402     method to_cic_term =
 403      let module U = UriManager in
 404       let n = self#node in
 405        let sons = n#sub_nodes
 406        and id = string_of_xml_attr (n#attribute "id") in
 407         match sons with
 408            ty::te::patterns when
 409              ty#node_type = Pxp_document.T_element "patternsType" &&
 410              te#node_type = Pxp_document.T_element "inductiveTerm" ->
 411               let ci = uri_of_xml_attr (n#attribute "uriType")
 412               and typeno = int_of_xml_attr (n#attribute "noType")
 413               and inductiveType = ty#extension#to_cic_term
 414               and inductiveTerm = te#extension#to_cic_term
 415               and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
 416               in
 417                Cic.AMutCase (id,ci,U.relative_depth !current_uri ci 0,
 418                 typeno,inductiveType,inductiveTerm,lpattern)
 419          | _  -> raise (IllFormedXml 11)
 420   end
 421 ;;
 422
 423 class eltype_lambda =
 424   object (self)
 425
 426     inherit cic_term
 427
 428     method to_cic_term =
 429      let n = self#node in
 430       let sons = n#sub_nodes
 431       and id = string_of_xml_attr (n#attribute "id") in
 432        match sons with
 433           [s ; t] when
 434             s#node_type = Pxp_document.T_element "source" &&
 435             t#node_type = Pxp_document.T_element "target" ->
 436              let name = cic_attr_of_xml_attr (t#attribute "binder")
 437              and source = s#extension#to_cic_term
 438              and target = t#extension#to_cic_term in
 439               Cic.ALambda (id,name,source,target)
 440         | _  -> raise (IllFormedXml 12)
 441   end
 442 ;;
 443
 444 class eltype_letin =
 445   object (self)
 446
 447     inherit cic_term
 448
 449     method to_cic_term =
 450      let n = self#node in
 451       let sons = n#sub_nodes
 452       and id = string_of_xml_attr (n#attribute "id") in
 453        match sons with
 454           [s ; t] when
 455             s#node_type = Pxp_document.T_element "term" &&
 456             t#node_type = Pxp_document.T_element "letintarget" ->
 457              let name = cic_attr_of_xml_attr (t#attribute "binder")
 458              and source = s#extension#to_cic_term
 459              and target = t#extension#to_cic_term in
 460               Cic.ALetIn (id,name,source,target)
 461         | _  -> raise (IllFormedXml 12)
 462   end
 463 ;;
 464
 465 (* The definition of domspec, an hashtable that maps each node type to the *)
 466 (* object that must be linked to it. Used by markup.                       *)
 467
 468 let domspec =
 469  let module D = Pxp_document in
 470   D.make_spec_from_alist
 471    ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
 472    ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
 473    ~element_alist:
 474     [ "REL",           (new D.element_impl (new eltype_rel)) ;
 475       "VAR",           (new D.element_impl (new eltype_var)) ;
 476       "META",          (new D.element_impl (new eltype_meta)) ;
 477       "SORT",          (new D.element_impl (new eltype_sort)) ;
 478       "IMPLICIT",      (new D.element_impl (new eltype_implicit)) ;
 479       "CAST",          (new D.element_impl (new eltype_cast)) ;
 480       "PROD",          (new D.element_impl (new eltype_prod)) ;
 481       "LAMBDA",        (new D.element_impl (new eltype_lambda)) ;
 482       "LETIN",         (new D.element_impl (new eltype_letin)) ;
 483       "APPLY",         (new D.element_impl (new eltype_apply)) ;
 484       "CONST",         (new D.element_impl (new eltype_const)) ;
 485       "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
 486       "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
 487       "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;
 488       "FIX",           (new D.element_impl (new eltype_fix)) ;
 489       "COFIX",         (new D.element_impl (new eltype_cofix)) ;
 490       "arity",         (new D.element_impl (new eltype_transparent)) ;
 491       "term",          (new D.element_impl (new eltype_transparent)) ;
 492       "type",          (new D.element_impl (new eltype_transparent)) ;
 493       "body",          (new D.element_impl (new eltype_transparent)) ;
 494       "source",        (new D.element_impl (new eltype_transparent)) ;
 495       "target",        (new D.element_impl (new eltype_transparent)) ;
 496       "letintarget",   (new D.element_impl (new eltype_transparent)) ;
 497       "patternsType",  (new D.element_impl (new eltype_transparent)) ;
 498       "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
 499       "pattern",       (new D.element_impl (new eltype_transparent))
 500     ]
 501    ()
 502 ;;