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