helm/interface/cicParser3.ml

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