X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Finterface%2FcicParser2.ml;fp=helm%2Finterface%2FcicParser2.ml;h=0000000000000000000000000000000000000000;hb=e108abe5c0b4eb841c4ad332229a6c0e57e70079;hp=562f79bba66150b0e5aea5c2e2c5cd5a5feaf856;hpb=1456c337a60f6677ee742ff7891d43fc382359a9;p=helm.git diff --git a/helm/interface/cicParser2.ml b/helm/interface/cicParser2.ml deleted file mode 100644 index 562f79bba..000000000 --- a/helm/interface/cicParser2.ml +++ /dev/null @@ -1,289 +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 objects level of a parser for cic objects from xml *) -(* files to the internal representation. It uses the module cicParser3 *) -(* cicParser3 (terms level) and it is used only through cicParser2 (top *) -(* level). *) -(* *) -(******************************************************************************) - -exception IllFormedXml of int;; -exception NotImplemented;; - -(* Utility functions that transform a Pxp attribute into something useful *) - -(* mk_absolute_uris "n1: v1 ... vn n2 : u1 ... un ...." *) -(* returns [(n1,[absolute_uri_for_v1 ; ... ; absolute_uri_for_vn]) ; (n2,...) *) -let mk_absolute_uris s = - let l = (Str.split (Str.regexp ":") s) in - let absolute_of_relative n v = - let module P3 = CicParser3 in - let rec mkburi = - function - (0,_) -> "/" - | (n,he::tl) when n > 0 -> - "/" ^ he ^ mkburi (n - 1, tl) - | _ -> raise (IllFormedXml 12) - in - let m = List.length !P3.current_sp - (int_of_string n) in - let buri = mkburi (m, !P3.current_sp) in - UriManager.uri_of_string ("cic:" ^ buri ^ v ^ ".var") - in - let rec absolutize = - function - [] -> [] - | [no ; vs] -> - let vars = (Str.split (Str.regexp " ") vs) in - [(int_of_string no, List.map (absolute_of_relative no) vars)] - | no::vs::tl -> - let vars = (Str.split (Str.regexp " ") vs) in - let rec add_prefix = - function - [no2] -> ([], no2) - | he::tl -> - let (pvars, no2) = add_prefix tl in - ((absolute_of_relative no he)::pvars, no2) - | _ -> raise (IllFormedXml 11) - in - let (pvars, no2) = add_prefix vars in - (int_of_string no, pvars)::(absolutize (no2::tl)) - | _ -> raise (IllFormedXml 10) - in - (* last parameter must be applied first *) - absolutize l -;; - -let option_uri_list_of_attr a1 a2 = - let module T = Pxp_types in - let parameters = - match a1 with - T.Value s -> mk_absolute_uris s - | _ -> raise (IllFormedXml 0) - in - match a2 with - T.Value "POSSIBLE" -> Cic.Possible parameters - | T.Implied_value -> Cic.Actual parameters - | _ -> raise (IllFormedXml 0) -;; - -let uri_list_of_attr a = - let module T = Pxp_types in - match a with - T.Value s -> mk_absolute_uris s - | _ -> raise (IllFormedXml 0) -;; - -let string_of_attr a = - let module T = Pxp_types in - match a with - T.Value s -> s - | _ -> raise (IllFormedXml 0) -;; - -let int_of_attr a = - int_of_string (string_of_attr a) -;; - -let bool_of_attr a = - bool_of_string (string_of_attr a) -;; - -(* Other utility functions *) - -let get_content n = - match n#sub_nodes with - [ t ] -> t - | _ -> raise (IllFormedXml 1) -;; - -let register_id id node = - if !CicParser3.process_annotations then - match !CicParser3.ids_to_targets with - None -> assert false - | Some ids_to_targets -> - Hashtbl.add ids_to_targets id (Cic.Object node) -;; - -(* Functions that, given the list of sons of a node of the cic dom (objects *) -(* level), retrieve the internal representation associated to the node. *) -(* Everytime a cic term subtree is found, it is translated to the internal *) -(* representation using the method to_cic_term defined in cicParser3. *) -(* Each function raise IllFormedXml if something goes wrong, but this should *) -(* be impossible due to the presence of the dtd *) -(* The functions should really be obvious looking at their name and the cic *) -(* dtd *) - -(* called when a CurrentProof is found *) -let get_conjs_value_type l = - let rec rget (c, v, t) l = - let module D = Pxp_document in - match l with - [] -> (c, v, t) - | conj::tl when conj#node_type = D.T_element "Conjecture" -> - let no = int_of_attr (conj#attribute "no") - and typ = (get_content conj)#extension#to_cic_term in - rget ((no, typ)::c, v, t) tl - | value::tl when value#node_type = D.T_element "body" -> - let v' = (get_content value)#extension#to_cic_term in - (match v with - None -> rget (c, Some v', t) tl - | _ -> raise (IllFormedXml 2) - ) - | typ::tl when typ#node_type = D.T_element "type" -> - let t' = (get_content typ)#extension#to_cic_term in - (match t with - None -> rget (c, v, Some t') tl - | _ -> raise (IllFormedXml 3) - ) - | _ -> raise (IllFormedXml 4) - in - match rget ([], None, None) l with - (c, Some v, Some t) -> (c, v, t) - | _ -> raise (IllFormedXml 5) -;; - -(* used only by get_inductive_types; called one time for each inductive *) -(* definitions in a block of inductive definitions *) -let get_names_arity_constructors l = - let rec rget (a,c) l = - let module D = Pxp_document in - match l with - [] -> (a, c) - | arity::tl when arity#node_type = D.T_element "arity" -> - let a' = (get_content arity)#extension#to_cic_term in - rget (Some a',c) tl - | con::tl when con#node_type = D.T_element "Constructor" -> - let id = string_of_attr (con#attribute "name") - and ty = (get_content con)#extension#to_cic_term in - rget (a,(id,ty,ref None)::c) tl - | _ -> raise (IllFormedXml 9) - in - match rget (None,[]) l with - (Some a, c) -> (a, List.rev c) - | _ -> raise (IllFormedXml 8) -;; - -(* called when an InductiveDefinition is found *) -let rec get_inductive_types = - function - [] -> [] - | he::tl -> - let tyname = string_of_attr (he#attribute "name") - and inductive = bool_of_attr (he#attribute "inductive") - and (arity,cons) = - get_names_arity_constructors (he#sub_nodes) - in - (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *) -;; - -(* This is the main function and also the only one used directly from *) -(* cicParser. Given the root of the dom tree, it returns the internal *) -(* representation of the cic object described in the tree *) -(* It uses the previous functions and the to_cic_term method defined *) -(* in cicParser3 (used for subtrees that encode cic terms) *) -let rec get_term n = - let module D = Pxp_document in - let module C = Cic in - let ntype = n # node_type in - match ntype with - D.T_element "Definition" -> - let id = string_of_attr (n # attribute "name") - and params = - option_uri_list_of_attr (n#attribute "params") (n#attribute "paramMode") - and (value, typ) = - let sons = n#sub_nodes in - match sons with - [v ; t] when - v#node_type = D.T_element "body" && - t#node_type = D.T_element "type" -> - let v' = get_content v - and t' = get_content t in - (v'#extension#to_cic_term, t'#extension#to_cic_term) - | _ -> raise (IllFormedXml 6) - and xid = string_of_attr (n#attribute "id") in - let res = C.ADefinition (xid, ref None, id, value, typ, params) in - register_id xid res ; - res - | D.T_element "Axiom" -> - let id = string_of_attr (n # attribute "name") - and params = uri_list_of_attr (n # attribute "params") - and typ = - (get_content (get_content n))#extension#to_cic_term - and xid = string_of_attr (n#attribute "id") in - let res = C.AAxiom (xid, ref None, id, typ, params) in - register_id xid res ; - res - | D.T_element "CurrentProof" -> - let name = string_of_attr (n#attribute "name") - and xid = string_of_attr (n#attribute "id") in - let sons = n#sub_nodes in - let (conjs, value, typ) = get_conjs_value_type sons in - let res = C.ACurrentProof (xid, ref None, name, conjs, value, typ) in - register_id xid res ; - res - | D.T_element "InductiveDefinition" -> - let sons = n#sub_nodes - and xid = string_of_attr (n#attribute "id") in - let inductiveTypes = get_inductive_types sons - and params = uri_list_of_attr (n#attribute "params") - and nparams = int_of_attr (n#attribute "noParams") in - let res = - C.AInductiveDefinition (xid, ref None, inductiveTypes, params, nparams) - in - register_id xid res ; - res - | D.T_element "Variable" -> - let name = string_of_attr (n#attribute "name") - and xid = string_of_attr (n#attribute "id") - and (body, typ) = - let sons = n#sub_nodes in - match sons with - [b ; t] when - b#node_type = D.T_element "body" && - t#node_type = D.T_element "type" -> - let b' = get_content b - and t' = get_content t in - (Some (b'#extension#to_cic_term), t'#extension#to_cic_term) - | [t] when t#node_type = D.T_element "type" -> - let t' = get_content t in - (None, t'#extension#to_cic_term) - | _ -> raise (IllFormedXml 6) - in - let res = C.AVariable (xid,ref None,name,body,typ) in - register_id xid res ; - res - | D.T_element _ - | D.T_data - | _ -> - raise (IllFormedXml 7) -;;