+++ /dev/null
-(* Copyright (C) 2000, HELM Team.
- *
- * This file is part of HELM, an Hypertextual, Electronic
- * Library of Mathematics, developed at the Computer Science
- * Department, University of Bologna, Italy.
- *
- * HELM is free software; you can redistribute it and/or
- * modify it under the terms of the GNU General Public License
- * as published by the Free Software Foundation; either version 2
- * of the License, or (at your option) any later version.
- *
- * HELM is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with HELM; if not, write to the Free Software
- * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
- * MA 02111-1307, USA.
- *
- * For details, see the HELM World-Wide-Web page,
- * http://cs.unibo.it/helm/.
- *)
-
-(******************************************************************************)
-(* *)
-(* 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
-;;
-
-class eltype_letin =
- 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 "term" &&
- t#node_type = Pxp_document.T_element "letintarget" ->
- 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.ALetIn (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)) ;
- "LETIN", (new D.element_impl (new eltype_letin)) ;
- "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