+++ /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 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)
-;;
projects / helm.git / blobdiff