X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2FcicParser3.ml;fp=helm%2Finterface%2FcicParser3.ml;h=0000000000000000000000000000000000000000;hb=c7514aaa249a96c5fdd39b1123fbdb38d92f20b6;hp=54b417fa1b591808f38ff49a2e87f40f11c52db9;hpb=1c7fb836e2af4f2f3d18afd0396701f2094265ff;p=helm.git diff --git a/helm/interface/cicParser3.ml b/helm/interface/cicParser3.ml deleted file mode 100644 index 54b417fa1..000000000 --- a/helm/interface/cicParser3.ml +++ /dev/null @@ -1,564 +0,0 @@ -(* 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 *) -(* 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. ... *) -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)) - ] - () -;;