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