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.Anonymous
  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 always 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 :
 107      (UriManager.uri * Cic.annterm) list -> Cic.annterm
 108   end
 109 ;;
 110
 111 (* the class of the objects linked to nodes that are not roots of cic terms *)
 112 class eltype_not_of_cic =
 113   object (self)
 114
 115      inherit cic_term
 116
 117      method to_cic_term _ = raise (IllFormedXml 6)
 118   end
 119 ;;
 120
 121 (* the class of the objects linked to nodes whose content is a cic term *)
 122 (* (syntactic sugar xml entities) e.g. <type> ... </type>               *)
 123 class eltype_transparent =
 124   object (self)
 125
 126     inherit cic_term
 127
 128     method to_cic_term exp_named_subst =
 129      assert (exp_named_subst = []) ;
 130      let n = self#node in
 131       match n#sub_nodes with
 132          [ t ]  -> t#extension#to_cic_term []
 133        | _  -> raise (IllFormedXml 7)
 134   end
 135 ;;
 136
 137 (* A class for each cic node type *)
 138
 139 class eltype_fix =
 140   object (self)
 141
 142     inherit cic_term
 143
 144     method to_cic_term exp_named_subst =
 145      assert (exp_named_subst = []) ;
 146      let n = self#node in
 147       let nofun = int_of_xml_attr (n#attribute "noFun")
 148       and id = string_of_xml_attr (n#attribute "id")
 149       and functions =
 150        let sons = n#sub_nodes in
 151         List.map
 152          (function
 153              f when f#node_type = Pxp_document.T_element "FixFunction" ->
 154               let name = string_of_xml_attr (f#attribute "name")
 155               and id = string_of_xml_attr (f#attribute "id")
 156               and recindex = int_of_xml_attr (f#attribute "recIndex")
 157               and (ty, body) =
 158                match f#sub_nodes with
 159                   [t ; b] when
 160                     t#node_type = Pxp_document.T_element "type" &&
 161                     b#node_type = Pxp_document.T_element "body" ->
 162                      (t#extension#to_cic_term [], b#extension#to_cic_term [])
 163                 | _ -> raise (IllFormedXml 14)
 164               in
 165                (id, name, recindex, ty, body)
 166            | _ -> raise (IllFormedXml 13)
 167          ) sons
 168       in
 169        Cic.AFix (id, nofun, functions)
 170   end
 171 ;;
 172
 173 class eltype_cofix =
 174   object (self)
 175
 176     inherit cic_term
 177
 178     method to_cic_term exp_named_subst =
 179      assert (exp_named_subst = []) ;
 180      let n = self#node in
 181       let nofun = int_of_xml_attr (n#attribute "noFun")
 182       and id = string_of_xml_attr (n#attribute "id")
 183       and functions =
 184        let sons = n#sub_nodes in
 185         List.map
 186          (function
 187              f when f#node_type = Pxp_document.T_element "CofixFunction" ->
 188               let name = string_of_xml_attr (f#attribute "name")
 189               and id = string_of_xml_attr (f#attribute "id")
 190               and (ty, body) =
 191                match f#sub_nodes with
 192                   [t ; b] when
 193                     t#node_type = Pxp_document.T_element "type" &&
 194                     b#node_type = Pxp_document.T_element "body" ->
 195                      (t#extension#to_cic_term [], b#extension#to_cic_term [])
 196                 | _ -> raise (IllFormedXml 16)
 197               in
 198                (id, name, ty, body)
 199            | _ -> raise (IllFormedXml 15)
 200          ) sons
 201       in
 202        Cic.ACoFix (id, nofun, functions)
 203   end
 204 ;;
 205
 206 class eltype_implicit =
 207   object (self)
 208
 209     inherit cic_term
 210
 211     method to_cic_term exp_named_subst =
 212      assert (exp_named_subst = []) ;
 213      let n = self#node in
 214       let id = string_of_xml_attr (n#attribute "id") in
 215        Cic.AImplicit id
 216   end
 217 ;;
 218
 219 class eltype_rel =
 220   object (self)
 221
 222     inherit cic_term
 223
 224     method to_cic_term exp_named_subst =
 225      assert (exp_named_subst = []) ;
 226      let n = self#node in
 227       let value  = int_of_xml_attr (n#attribute "value")
 228       and binder = binder_of_xml_attr (n#attribute "binder")
 229       and id = string_of_xml_attr (n#attribute "id")
 230       and idref = string_of_xml_attr (n#attribute "idref") in
 231        Cic.ARel (id,idref,value,binder)
 232   end
 233 ;;
 234
 235 class eltype_meta =
 236   object (self)
 237
 238     inherit cic_term
 239
 240     method to_cic_term exp_named_subst =
 241      assert (exp_named_subst = []) ;
 242      let n = self#node in
 243       let value = int_of_xml_attr (n#attribute "no")
 244       and id = string_of_xml_attr (n#attribute "id")
 245       in
 246        let local_context =
 247         let sons = n#sub_nodes in
 248          List.map
 249           (function substitution ->
 250             match substitution#sub_nodes with
 251                [] -> None
 252              | [he] -> Some (he#extension#to_cic_term [])
 253              | _ -> raise (IllFormedXml 20)
 254           ) sons
 255        in
 256         Cic.AMeta (id,value,local_context)
 257   end
 258 ;;
 259
 260 class eltype_var =
 261   object (self)
 262
 263     inherit cic_term
 264
 265     method to_cic_term exp_named_subst =
 266      assert (exp_named_subst = []) ;
 267      let n = self#node in
 268       let uri = uri_of_xml_attr (n#attribute "uri")
 269       and xid = string_of_xml_attr (n#attribute "id") in
 270 (*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *)
 271        Cic.AVar (xid,uri,[])
 272   end
 273 ;;
 274
 275 class eltype_apply =
 276   object (self)
 277
 278     inherit cic_term
 279
 280     method to_cic_term exp_named_subst =
 281      assert (exp_named_subst = []) ;
 282      let n = self#node in
 283       let children = n#sub_nodes
 284       and id = string_of_xml_attr (n#attribute "id") in
 285        if List.length children < 2 then raise (IllFormedXml 8)
 286        else
 287         Cic.AAppl
 288          (id,List.map (fun x -> x#extension#to_cic_term []) children)
 289   end
 290 ;;
 291
 292 class eltype_cast =
 293   object (self)
 294
 295     inherit cic_term
 296
 297     method to_cic_term exp_named_subst =
 298      assert (exp_named_subst = []) ;
 299      let n = self#node in
 300       let sons = n#sub_nodes
 301       and id = string_of_xml_attr (n#attribute "id") in
 302        match sons with
 303           [te ; ty] when
 304             te#node_type = Pxp_document.T_element "term" &&
 305             ty#node_type = Pxp_document.T_element "type" ->
 306              let term = te#extension#to_cic_term []
 307              and typ  = ty#extension#to_cic_term [] in
 308               Cic.ACast (id,term,typ)
 309         | _  -> raise (IllFormedXml 9)
 310   end
 311 ;;
 312
 313 class eltype_sort =
 314   object (self)
 315
 316     inherit cic_term
 317
 318     method to_cic_term exp_named_subst =
 319      assert (exp_named_subst = []) ;
 320      let n = self#node in
 321       let sort = cic_sort_of_xml_attr (n#attribute "value")
 322       and id = string_of_xml_attr (n#attribute "id") in
 323        Cic.ASort (id,sort)
 324   end
 325 ;;
 326
 327 class eltype_const =
 328   object (self)
 329
 330     inherit cic_term
 331
 332     method to_cic_term exp_named_subst =
 333      let module U = UriManager in
 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.AConst (id,value, exp_named_subst)
 338   end
 339 ;;
 340
 341 class eltype_mutind =
 342   object (self)
 343
 344     inherit cic_term
 345
 346     method to_cic_term exp_named_subst =
 347      let module U = UriManager in
 348       let n = self#node in
 349        let name = uri_of_xml_attr (n#attribute "uri")
 350        and noType = int_of_xml_attr (n#attribute "noType")
 351        and id = string_of_xml_attr (n#attribute "id") in
 352         Cic.AMutInd
 353          (id,name, noType, exp_named_subst)
 354   end
 355 ;;
 356
 357 class eltype_mutconstruct =
 358   object (self)
 359
 360     inherit cic_term
 361
 362     method to_cic_term exp_named_subst =
 363      let module U = UriManager in
 364       let n = self#node in
 365        let name = uri_of_xml_attr (n#attribute "uri")
 366        and noType = int_of_xml_attr (n#attribute "noType")
 367        and noConstr = int_of_xml_attr (n#attribute "noConstr")
 368        and id = string_of_xml_attr (n#attribute "id") in
 369         Cic.AMutConstruct
 370          (id, name, noType, noConstr, exp_named_subst)
 371   end
 372 ;;
 373
 374 class eltype_prod =
 375   object (self)
 376
 377     inherit cic_term
 378
 379     method to_cic_term exp_named_subst =
 380      assert (exp_named_subst = []) ;
 381      let n = self#node in
 382       let sons = n#sub_nodes in
 383        let rec get_decls_and_target =
 384         function
 385            [t] when t#node_type = Pxp_document.T_element "target" ->
 386             [],t#extension#to_cic_term []
 387          | s::tl when s#node_type = Pxp_document.T_element "decl" ->
 388             let decls,target = get_decls_and_target tl in
 389              let id = string_of_xml_attr (s#attribute "id") in
 390              let binder = cic_attr_of_xml_attr (s#attribute "binder") in
 391               (id,binder,s#extension#to_cic_term [])::decls, target
 392          | _  -> raise (IllFormedXml 10)
 393        in
 394         let decls,target = get_decls_and_target sons in
 395          List.fold_right
 396           (fun (id,b,s) t -> Cic.AProd (id,b,s,t))
 397           decls target
 398   end
 399 ;;
 400
 401 class eltype_mutcase =
 402   object (self)
 403
 404     inherit cic_term
 405
 406     method to_cic_term exp_named_subst =
 407      assert (exp_named_subst = []) ;
 408      let module U = UriManager in
 409       let n = self#node in
 410        let sons = n#sub_nodes
 411        and id = string_of_xml_attr (n#attribute "id") in
 412         match sons with
 413            ty::te::patterns when
 414              ty#node_type = Pxp_document.T_element "patternsType" &&
 415              te#node_type = Pxp_document.T_element "inductiveTerm" ->
 416               let ci = uri_of_xml_attr (n#attribute "uriType")
 417               and typeno = int_of_xml_attr (n#attribute "noType")
 418               and inductiveType = ty#extension#to_cic_term []
 419               and inductiveTerm = te#extension#to_cic_term []
 420               and lpattern =
 421                List.map (fun x -> x#extension#to_cic_term []) patterns
 422               in
 423                Cic.AMutCase (id,ci, typeno,inductiveType,inductiveTerm,lpattern)
 424          | _  -> raise (IllFormedXml 11)
 425   end
 426 ;;
 427
 428 class eltype_lambda =
 429   object (self)
 430
 431     inherit cic_term
 432
 433     method to_cic_term exp_named_subst =
 434      assert (exp_named_subst = []) ;
 435      let n = self#node in
 436       let sons = n#sub_nodes in
 437        let rec get_decls_and_target =
 438         function
 439            [t] when t#node_type = Pxp_document.T_element "target" ->
 440             [],t#extension#to_cic_term []
 441          | s::tl when s#node_type = Pxp_document.T_element "decl" ->
 442             let decls,target = get_decls_and_target tl in
 443              let id = string_of_xml_attr (s#attribute "id") in
 444              let binder = cic_attr_of_xml_attr (s#attribute "binder") in
 445               (id,binder,s#extension#to_cic_term [])::decls, target
 446          | _  -> raise (IllFormedXml 12)
 447        in
 448         let decls,target = get_decls_and_target sons in
 449          List.fold_right
 450           (fun (id,b,s) t -> Cic.ALambda (id,b,s,t))
 451           decls target
 452   end
 453 ;;
 454
 455 class eltype_letin =
 456   object (self)
 457
 458     inherit cic_term
 459
 460     method to_cic_term exp_named_subst =
 461      assert (exp_named_subst = []) ;
 462      let n = self#node in
 463       let sons = n#sub_nodes in
 464        let rec get_defs_and_target =
 465         function
 466            [t] when t#node_type = Pxp_document.T_element "target" ->
 467             [],t#extension#to_cic_term []
 468          | s::tl when s#node_type = Pxp_document.T_element "def" ->
 469             let defs,target = get_defs_and_target tl in
 470              let id = string_of_xml_attr (s#attribute "id") in
 471              let binder = cic_attr_of_xml_attr (s#attribute "binder") in
 472               (id,binder,s#extension#to_cic_term [])::defs, target
 473          | _  -> raise (IllFormedXml 12)
 474        in
 475         let defs,target = get_defs_and_target sons in
 476          List.fold_right
 477           (fun (id,b,s) t -> Cic.ALetIn (id,b,s,t))
 478           defs target
 479   end
 480 ;;
 481
 482 class eltype_instantiate =
 483   object (self)
 484
 485     inherit cic_term
 486
 487     method to_cic_term exp_named_subst =
 488      assert (exp_named_subst = []) ;
 489      let n = self#node in
 490 (* CSC: this optional attribute should be parsed and reflected in Cic.annterm
 491       and id = string_of_xml_attr (n#attribute "id")
 492 *)
 493        match n#sub_nodes with
 494           t::l  ->
 495            let baseUri =
 496             UriManager.buri_of_uri (uri_of_xml_attr (t#attribute "uri")) in
 497            let exp_named_subst =
 498             List.map
 499              (function
 500                  n when n#node_type = Pxp_document.T_element "arg" ->
 501                   let relUri = string_of_xml_attr (n#attribute "relUri") in
 502                   let uri = UriManager.uri_of_string (baseUri ^ "/" ^ relUri) in
 503                   let arg =
 504                    match n#sub_nodes with
 505                       [ t ]  -> t#extension#to_cic_term []
 506                     | _  -> raise (IllFormedXml 7)
 507                   in
 508                    (uri, arg)
 509                | _ -> raise (IllFormedXml 7)
 510              ) l
 511            in
 512             t#extension#to_cic_term exp_named_subst
 513         | _  -> raise (IllFormedXml 7)
 514   end
 515 ;;
 516
 517
 518 (* The definition of domspec, an hashtable that maps each node type to the *)
 519 (* object that must be linked to it. Used by markup.                       *)
 520
 521 let domspec =
 522  let module D = Pxp_document in
 523   D.make_spec_from_alist
 524    ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
 525    ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
 526    ~element_alist:
 527     [ "REL",           (new D.element_impl (new eltype_rel)) ;
 528       "VAR",           (new D.element_impl (new eltype_var)) ;
 529       "META",          (new D.element_impl (new eltype_meta)) ;
 530       "SORT",          (new D.element_impl (new eltype_sort)) ;
 531       "IMPLICIT",      (new D.element_impl (new eltype_implicit)) ;
 532       "CAST",          (new D.element_impl (new eltype_cast)) ;
 533       "PROD",          (new D.element_impl (new eltype_prod)) ;
 534       "LAMBDA",        (new D.element_impl (new eltype_lambda)) ;
 535       "LETIN",         (new D.element_impl (new eltype_letin)) ;
 536       "APPLY",         (new D.element_impl (new eltype_apply)) ;
 537       "CONST",         (new D.element_impl (new eltype_const)) ;
 538       "MUTIND",        (new D.element_impl (new eltype_mutind)) ;
 539       "MUTCONSTRUCT",  (new D.element_impl (new eltype_mutconstruct)) ;
 540       "MUTCASE",       (new D.element_impl (new eltype_mutcase)) ;
 541       "FIX",           (new D.element_impl (new eltype_fix)) ;
 542       "COFIX",         (new D.element_impl (new eltype_cofix)) ;
 543       "instantiate",   (new D.element_impl (new eltype_instantiate)) ;
 544       "arity",         (new D.element_impl (new eltype_transparent)) ;
 545       "term",          (new D.element_impl (new eltype_transparent)) ;
 546       "type",          (new D.element_impl (new eltype_transparent)) ;
 547       "body",          (new D.element_impl (new eltype_transparent)) ;
 548       "decl",          (new D.element_impl (new eltype_transparent)) ;
 549       "def",           (new D.element_impl (new eltype_transparent)) ;
 550       "target",        (new D.element_impl (new eltype_transparent)) ;
 551       "letintarget",   (new D.element_impl (new eltype_transparent)) ;
 552       "patternsType",  (new D.element_impl (new eltype_transparent)) ;
 553       "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
 554       "pattern",       (new D.element_impl (new eltype_transparent))
 555     ]
 556    ()
 557 ;;