X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser3.ml;fp=helm%2Focaml%2Fcic%2FcicParser3.ml;h=0000000000000000000000000000000000000000;hp=8e6d276d5c9ea003bc31a6df3197965b4ce5b080;hb=1696761e4b8576e8ed81caa905fd108717019226;hpb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1 diff --git a/helm/ocaml/cic/cicParser3.ml b/helm/ocaml/cic/cicParser3.ml deleted file mode 100644 index 8e6d276d5..000000000 --- a/helm/ocaml/cic/cicParser3.ml +++ /dev/null @@ -1,550 +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;; - -(* 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.Anonymous - | _ -> 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 (CicUniv.fresh ()) (* TASSI: sure? *) - | _ -> 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 -> s - | _ -> raise (IllFormedXml 17) -;; - -(* the "interface" of the class linked to each node of the dom tree *) - -class virtual cic_term = - object (self) - - (* fields and methods always 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 : - (UriManager.uri * Cic.annterm) list -> 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 exp_named_subst = - assert (exp_named_subst = []) ; - 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 exp_named_subst = - assert (exp_named_subst = []) ; - 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 id = string_of_xml_attr (f#attribute "id") - 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 - (id, name, recindex, ty, body) - | _ -> raise (IllFormedXml 13) - ) sons - in - Cic.AFix (id, nofun, functions) - end -;; - -class eltype_cofix = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - 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 id = string_of_xml_attr (f#attribute "id") - 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 - (id, name, ty, body) - | _ -> raise (IllFormedXml 15) - ) sons - in - Cic.ACoFix (id, nofun, functions) - end -;; - -class eltype_implicit = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let id = string_of_xml_attr (n#attribute "id") in - Cic.AImplicit (id, None) - end -;; - -class eltype_rel = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - 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") - and idref = string_of_xml_attr (n#attribute "idref") in - Cic.ARel (id,idref,value,binder) - end -;; - -class eltype_meta = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - 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 local_context = - let sons = n#sub_nodes in - List.map - (function substitution -> - match substitution#sub_nodes with - [] -> None - | [he] -> Some (he#extension#to_cic_term []) - | _ -> raise (IllFormedXml 20) - ) sons - in - Cic.AMeta (id,value,local_context) - end -;; - -class eltype_var = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let uri = uri_of_xml_attr (n#attribute "uri") - and xid = string_of_xml_attr (n#attribute "id") in -(*CSC: BIG BUG: [] MUST BE REPLACED WITH THE PARSED EXPLICIT NAMED SUBSTITUTION *) - Cic.AVar (xid,uri,[]) - end -;; - -class eltype_apply = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - 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 - Cic.AAppl - (id,List.map (fun x -> x#extension#to_cic_term []) children) - end -;; - -class eltype_cast = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - 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 - Cic.ACast (id,term,typ) - | _ -> raise (IllFormedXml 9) - end -;; - -class eltype_sort = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - 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 - Cic.ASort (id,sort) - end -;; - -class eltype_const = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - 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 - Cic.AConst (id,value, exp_named_subst) - end -;; - -class eltype_mutind = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - 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 - Cic.AMutInd - (id,name, noType, exp_named_subst) - end -;; - -class eltype_mutconstruct = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - 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 - Cic.AMutConstruct - (id, name, noType, noConstr, exp_named_subst) - end -;; - -class eltype_prod = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let sons = n#sub_nodes in - let rec get_decls_and_target = - function - [t] when t#node_type = Pxp_document.T_element "target" -> - [],t#extension#to_cic_term [] - | s::tl when s#node_type = Pxp_document.T_element "decl" -> - let decls,target = get_decls_and_target tl in - let id = string_of_xml_attr (s#attribute "id") in - let binder = cic_attr_of_xml_attr (s#attribute "binder") in - (id,binder,s#extension#to_cic_term [])::decls, target - | _ -> raise (IllFormedXml 10) - in - let decls,target = get_decls_and_target sons in - List.fold_right - (fun (id,b,s) t -> Cic.AProd (id,b,s,t)) - decls target - end -;; - -class eltype_mutcase = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - 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 - Cic.AMutCase (id,ci, typeno,inductiveType,inductiveTerm,lpattern) - | _ -> raise (IllFormedXml 11) - end -;; - -class eltype_lambda = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let sons = n#sub_nodes in - let rec get_decls_and_target = - function - [t] when t#node_type = Pxp_document.T_element "target" -> - [],t#extension#to_cic_term [] - | s::tl when s#node_type = Pxp_document.T_element "decl" -> - let decls,target = get_decls_and_target tl in - let id = string_of_xml_attr (s#attribute "id") in - let binder = cic_attr_of_xml_attr (s#attribute "binder") in - (id,binder,s#extension#to_cic_term [])::decls, target - | _ -> raise (IllFormedXml 12) - in - let decls,target = get_decls_and_target sons in - List.fold_right - (fun (id,b,s) t -> Cic.ALambda (id,b,s,t)) - decls target - end -;; - -class eltype_letin = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in - let sons = n#sub_nodes in - let rec get_defs_and_target = - function - [t] when t#node_type = Pxp_document.T_element "target" -> - [],t#extension#to_cic_term [] - | s::tl when s#node_type = Pxp_document.T_element "def" -> - let defs,target = get_defs_and_target tl in - let id = string_of_xml_attr (s#attribute "id") in - let binder = cic_attr_of_xml_attr (s#attribute "binder") in - (id,binder,s#extension#to_cic_term [])::defs, target - | _ -> raise (IllFormedXml 12) - in - let defs,target = get_defs_and_target sons in - List.fold_right - (fun (id,b,s) t -> Cic.ALetIn (id,b,s,t)) - defs target - end -;; - -class eltype_instantiate = - object (self) - - inherit cic_term - - method to_cic_term exp_named_subst = - assert (exp_named_subst = []) ; - let n = self#node in -(* CSC: this optional attribute should be parsed and reflected in Cic.annterm - and id = string_of_xml_attr (n#attribute "id") -*) - match n#sub_nodes with - t::l -> - let baseUri = - UriManager.buri_of_uri (uri_of_xml_attr (t#attribute "uri")) in - let exp_named_subst = - List.map - (function - n when n#node_type = Pxp_document.T_element "arg" -> - let relUri = string_of_xml_attr (n#attribute "relUri") in - let uri = UriManager.uri_of_string (baseUri ^ "/" ^ relUri) in - let arg = - match n#sub_nodes with - [ t ] -> t#extension#to_cic_term [] - | _ -> raise (IllFormedXml 7) - in - (uri, arg) - | _ -> raise (IllFormedXml 7) - ) l - in - t#extension#to_cic_term exp_named_subst - | _ -> raise (IllFormedXml 7) - 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)) ; - "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)) ; - "instantiate", (new D.element_impl (new eltype_instantiate)) ; - "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)) ; - "decl", (new D.element_impl (new eltype_transparent)) ; - "def", (new D.element_impl (new eltype_transparent)) ; - "target", (new D.element_impl (new eltype_transparent)) ; - "letintarget", (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)) - ] - () -;;