--- /dev/null
+(******************************************************************************)
+(* *)
+(* PROJECT HELM *)
+(* *)
+(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
+(* 24/01/2000 *)
+(* *)
+(* This module is the terms level of a parser for cic objects from xml *)
+(* files to the internal representation. It is used by the module cicParser2 *)
+(* (objects level). It defines an extension of the standard dom using the *)
+(* object-oriented extension machinery of markup: an object with a method *)
+(* to_cic_term that returns the internal representation of the subtree is *)
+(* added to each node of the dom tree *)
+(* *)
+(******************************************************************************)
+
+exception IllFormedXml of int;;
+
+(* The hashtable from the current identifiers to the object or the terms *)
+let ids_to_targets = ref None;;
+
+(* The list of tokens of the current section path. *)
+(* Used to resolve relative URIs *)
+let current_sp = ref [];;
+
+(* The uri of the object been parsed *)
+let current_uri = ref (UriManager.uri_of_string "cic:/.xml");;
+
+(* True if annotation really matter *)
+let process_annotations = ref false;;
+
+(* Utility functions to map a markup attribute to something useful *)
+
+let cic_attr_of_xml_attr =
+ function
+ Pxp_types.Value s -> Cic.Name s
+ | Pxp_types.Implied_value -> Cic.Anonimous
+ | _ -> raise (IllFormedXml 1)
+
+let cic_sort_of_xml_attr =
+ function
+ Pxp_types.Value "Prop" -> Cic.Prop
+ | Pxp_types.Value "Set" -> Cic.Set
+ | Pxp_types.Value "Type" -> Cic.Type
+ | _ -> raise (IllFormedXml 2)
+
+let int_of_xml_attr =
+ function
+ Pxp_types.Value n -> int_of_string n
+ | _ -> raise (IllFormedXml 3)
+
+let uri_of_xml_attr =
+ function
+ Pxp_types.Value s -> UriManager.uri_of_string s
+ | _ -> raise (IllFormedXml 4)
+
+let string_of_xml_attr =
+ function
+ Pxp_types.Value s -> s
+ | _ -> raise (IllFormedXml 5)
+
+let binder_of_xml_attr =
+ function
+ Pxp_types.Value s -> if !process_annotations then Some s else None
+ | _ -> raise (IllFormedXml 17)
+;;
+
+let register_id id node =
+ if !process_annotations then
+ match !ids_to_targets with
+ None -> assert false
+ | Some ids_to_targets ->
+ Hashtbl.add ids_to_targets id (Cic.Term node)
+;;
+
+(* the "interface" of the class linked to each node of the dom tree *)
+
+class virtual cic_term =
+ object (self)
+
+ (* fields and methods ever required by markup *)
+ val mutable node = (None : cic_term Pxp_document.node option)
+
+ method clone = {< >}
+ method node =
+ match node with
+ None ->
+ assert false
+ | Some n -> n
+ method set_node n =
+ node <- Some n
+
+ (* a method that returns the internal representation of the tree (term) *)
+ (* rooted in this node *)
+ method virtual to_cic_term : Cic.annterm
+ end
+;;
+
+(* the class of the objects linked to nodes that are not roots of cic terms *)
+class eltype_not_of_cic =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term = raise (IllFormedXml 6)
+ end
+;;
+
+(* the class of the objects linked to nodes whose content is a cic term *)
+(* (syntactic sugar xml entities) e.g. <type> ... </type> *)
+class eltype_transparent =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ match n#sub_nodes with
+ [ t ] -> t#extension#to_cic_term
+ | _ -> raise (IllFormedXml 7)
+ end
+;;
+
+(* A class for each cic node type *)
+
+class eltype_fix =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let nofun = int_of_xml_attr (n#attribute "noFun")
+ and id = string_of_xml_attr (n#attribute "id")
+ and functions =
+ let sons = n#sub_nodes in
+ List.map
+ (function
+ f when f#node_type = Pxp_document.T_element "FixFunction" ->
+ let name = string_of_xml_attr (f#attribute "name")
+ and recindex = int_of_xml_attr (f#attribute "recIndex")
+ and (ty, body) =
+ match f#sub_nodes with
+ [t ; b] when
+ t#node_type = Pxp_document.T_element "type" &&
+ b#node_type = Pxp_document.T_element "body" ->
+ (t#extension#to_cic_term, b#extension#to_cic_term)
+ | _ -> raise (IllFormedXml 14)
+ in
+ (name, recindex, ty, body)
+ | _ -> raise (IllFormedXml 13)
+ ) sons
+ in
+ let res = Cic.AFix (id, ref None, nofun, functions) in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_cofix =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let nofun = int_of_xml_attr (n#attribute "noFun")
+ and id = string_of_xml_attr (n#attribute "id")
+ and functions =
+ let sons = n#sub_nodes in
+ List.map
+ (function
+ f when f#node_type = Pxp_document.T_element "CofixFunction" ->
+ let name = string_of_xml_attr (f#attribute "name")
+ and (ty, body) =
+ match f#sub_nodes with
+ [t ; b] when
+ t#node_type = Pxp_document.T_element "type" &&
+ b#node_type = Pxp_document.T_element "body" ->
+ (t#extension#to_cic_term, b#extension#to_cic_term)
+ | _ -> raise (IllFormedXml 16)
+ in
+ (name, ty, body)
+ | _ -> raise (IllFormedXml 15)
+ ) sons
+ in
+ let res = Cic.ACoFix (id, ref None, nofun, functions) in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_implicit =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let id = string_of_xml_attr (n#attribute "id") in
+ let res = Cic.AImplicit (id, ref None) in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_rel =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let value = int_of_xml_attr (n#attribute "value")
+ and binder = binder_of_xml_attr (n#attribute "binder")
+ and id = string_of_xml_attr (n#attribute "id") in
+ let res = Cic.ARel (id,ref None,value,binder) in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_meta =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let value = int_of_xml_attr (n#attribute "no")
+ and id = string_of_xml_attr (n#attribute "id") in
+ let res = Cic.AMeta (id,ref None,value) in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_var =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let name = string_of_xml_attr (n#attribute "relUri")
+ and xid = string_of_xml_attr (n#attribute "id") in
+ match Str.split (Str.regexp ",") name with
+ [index; id] ->
+ let get_prefix n =
+ let rec aux =
+ function
+ (0,_) -> "/"
+ | (n,he::tl) when n > 0 -> "/" ^ he ^ aux (n - 1, tl)
+ | _ -> raise (IllFormedXml 19)
+ in
+ aux (List.length !current_sp - n,!current_sp)
+ in
+ let res =
+ Cic.AVar
+ (xid,ref None,
+ (UriManager.uri_of_string
+ ("cic:" ^ get_prefix (int_of_string index) ^ id ^ ".var"))
+ )
+ in
+ register_id id res ;
+ res
+ | _ -> raise (IllFormedXml 18)
+ end
+;;
+
+class eltype_apply =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let children = n#sub_nodes
+ and id = string_of_xml_attr (n#attribute "id") in
+ if List.length children < 2 then raise (IllFormedXml 8)
+ else
+ let res =
+ Cic.AAppl
+ (id,ref None,List.map (fun x -> x#extension#to_cic_term) children)
+ in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_cast =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let sons = n#sub_nodes
+ and id = string_of_xml_attr (n#attribute "id") in
+ match sons with
+ [te ; ty] when
+ te#node_type = Pxp_document.T_element "term" &&
+ ty#node_type = Pxp_document.T_element "type" ->
+ let term = te#extension#to_cic_term
+ and typ = ty#extension#to_cic_term in
+ let res = Cic.ACast (id,ref None,term,typ) in
+ register_id id res ;
+ res
+ | _ -> raise (IllFormedXml 9)
+ end
+;;
+
+class eltype_sort =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let sort = cic_sort_of_xml_attr (n#attribute "value")
+ and id = string_of_xml_attr (n#attribute "id") in
+ let res = Cic.ASort (id,ref None,sort) in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_abst =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let value = uri_of_xml_attr (n#attribute "uri")
+ and id = string_of_xml_attr (n#attribute "id") in
+ let res = Cic.AAbst (id,ref None,value) in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_const =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let module U = UriManager in
+ let n = self#node in
+ let value = uri_of_xml_attr (n#attribute "uri")
+ and id = string_of_xml_attr (n#attribute "id") in
+ let res =
+ Cic.AConst (id,ref None,value, U.relative_depth !current_uri value 0)
+ in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_mutind =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let module U = UriManager in
+ let n = self#node in
+ let name = uri_of_xml_attr (n#attribute "uri")
+ and noType = int_of_xml_attr (n#attribute "noType")
+ and id = string_of_xml_attr (n#attribute "id") in
+ let res =
+ Cic.AMutInd
+ (id,ref None,name, U.relative_depth !current_uri name 0, noType)
+ in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_mutconstruct =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let module U = UriManager in
+ let n = self#node in
+ let name = uri_of_xml_attr (n#attribute "uri")
+ and noType = int_of_xml_attr (n#attribute "noType")
+ and noConstr = int_of_xml_attr (n#attribute "noConstr")
+ and id = string_of_xml_attr (n#attribute "id") in
+ let res =
+ Cic.AMutConstruct
+ (id, ref None, name, U.relative_depth !current_uri name 0,
+ noType, noConstr)
+ in
+ register_id id res ;
+ res
+ end
+;;
+
+class eltype_prod =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let sons = n#sub_nodes
+ and id = string_of_xml_attr (n#attribute "id") in
+ match sons with
+ [s ; t] when
+ s#node_type = Pxp_document.T_element "source" &&
+ t#node_type = Pxp_document.T_element "target" ->
+ let name = cic_attr_of_xml_attr (t#attribute "binder")
+ and source = s#extension#to_cic_term
+ and target = t#extension#to_cic_term in
+ let res = Cic.AProd (id,ref None,name,source,target) in
+ register_id id res ;
+ res
+ | _ -> raise (IllFormedXml 10)
+ end
+;;
+
+class eltype_mutcase =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let module U = UriManager in
+ let n = self#node in
+ let sons = n#sub_nodes
+ and id = string_of_xml_attr (n#attribute "id") in
+ match sons with
+ ty::te::patterns when
+ ty#node_type = Pxp_document.T_element "patternsType" &&
+ te#node_type = Pxp_document.T_element "inductiveTerm" ->
+ let ci = uri_of_xml_attr (n#attribute "uriType")
+ and typeno = int_of_xml_attr (n#attribute "noType")
+ and inductiveType = ty#extension#to_cic_term
+ and inductiveTerm = te#extension#to_cic_term
+ and lpattern= List.map (fun x -> x#extension#to_cic_term) patterns
+ in
+ let res =
+ Cic.AMutCase (id,ref None,ci,U.relative_depth !current_uri ci 0,
+ typeno,inductiveType,inductiveTerm,lpattern)
+ in
+ register_id id res ;
+ res
+ | _ -> raise (IllFormedXml 11)
+ end
+;;
+
+class eltype_lambda =
+ object (self)
+
+ inherit cic_term
+
+ method to_cic_term =
+ let n = self#node in
+ let sons = n#sub_nodes
+ and id = string_of_xml_attr (n#attribute "id") in
+ match sons with
+ [s ; t] when
+ s#node_type = Pxp_document.T_element "source" &&
+ t#node_type = Pxp_document.T_element "target" ->
+ let name = cic_attr_of_xml_attr (t#attribute "binder")
+ and source = s#extension#to_cic_term
+ and target = t#extension#to_cic_term in
+ let res = Cic.ALambda (id,ref None,name,source,target) in
+ register_id id res ;
+ res
+ | _ -> raise (IllFormedXml 12)
+ end
+;;
+
+(* The definition of domspec, an hashtable that maps each node type to the *)
+(* object that must be linked to it. Used by markup. *)
+
+let domspec =
+ let module D = Pxp_document in
+ D.make_spec_from_alist
+ ~data_exemplar: (new D.data_impl (new eltype_not_of_cic))
+ ~default_element_exemplar: (new D.element_impl (new eltype_not_of_cic))
+ ~element_alist:
+ [ "REL", (new D.element_impl (new eltype_rel)) ;
+ "VAR", (new D.element_impl (new eltype_var)) ;
+ "META", (new D.element_impl (new eltype_meta)) ;
+ "SORT", (new D.element_impl (new eltype_sort)) ;
+ "IMPLICIT", (new D.element_impl (new eltype_implicit)) ;
+ "CAST", (new D.element_impl (new eltype_cast)) ;
+ "PROD", (new D.element_impl (new eltype_prod)) ;
+ "LAMBDA", (new D.element_impl (new eltype_lambda)) ;
+ "APPLY", (new D.element_impl (new eltype_apply)) ;
+ "CONST", (new D.element_impl (new eltype_const)) ;
+ "ABST", (new D.element_impl (new eltype_abst)) ;
+ "MUTIND", (new D.element_impl (new eltype_mutind)) ;
+ "MUTCONSTRUCT", (new D.element_impl (new eltype_mutconstruct)) ;
+ "MUTCASE", (new D.element_impl (new eltype_mutcase)) ;
+ "FIX", (new D.element_impl (new eltype_fix)) ;
+ "COFIX", (new D.element_impl (new eltype_cofix)) ;
+ "arity", (new D.element_impl (new eltype_transparent)) ;
+ "term", (new D.element_impl (new eltype_transparent)) ;
+ "type", (new D.element_impl (new eltype_transparent)) ;
+ "body", (new D.element_impl (new eltype_transparent)) ;
+ "source", (new D.element_impl (new eltype_transparent)) ;
+ "target", (new D.element_impl (new eltype_transparent)) ;
+ "patternsType", (new D.element_impl (new eltype_transparent)) ;
+ "inductiveTerm", (new D.element_impl (new eltype_transparent)) ;
+ "pattern", (new D.element_impl (new eltype_transparent))
+ ]
+ ()
+;;
projects / helm.git / blobdiff