--- /dev/null
+(******************************************************************************)
+(* *)
+(* 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") in
+ let typ = (get_content (get_content n))#extension#to_cic_term in
+ let res = C.AVariable (xid,ref None,name,typ) in
+ register_id xid res ;
+ res
+ | D.T_element _
+ | D.T_data ->
+ raise (IllFormedXml 7)
+;;
projects / helm.git / blobdiff