(* 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
+ T.Value s ->
+ List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s)
| _ -> raise (IllFormedXml 0)
;;
bool_of_string (string_of_attr a)
;;
+let name_of_attr a =
+ let module T = Pxp_types in
+ let module C = Cic in
+ match a with
+ T.Value s -> C.Name s
+ | T.Implied_value -> C.Anonymous
+ | _ -> raise (IllFormedXml 0)
+;;
+
(* Other utility functions *)
let get_content n =
(* dtd *)
(* called when a CurrentProof is found *)
-let get_conjs_value_type l =
- let rec rget (c, v, t) l =
+let get_conjs_value l =
+ let rec rget (c, v) l =
let module D = Pxp_document in
match l with
- [] -> (c, v, t)
+ [] -> (c, v)
| 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
+ let no = int_of_attr (conj#attribute "no") in
+ let id = string_of_attr (conj#attribute "id") in
+ let typ,canonical_context =
+ match List.rev (conj#sub_nodes) with
+ [] -> raise (IllFormedXml 13)
+ | typ::canonical_context ->
+ (get_content typ)#extension#to_cic_term [],
+ List.map
+ (function n ->
+ let id = string_of_attr (n#attribute "id") in
+ match n#node_type with
+ D.T_element "Decl" ->
+ let name = name_of_attr (n#attribute "name") in
+ let term = (get_content n)#extension#to_cic_term [] in
+ id, Some (name,Cic.ADecl term)
+ | D.T_element "Def" ->
+ let name = name_of_attr (n#attribute "name") in
+ let term = (get_content n)#extension#to_cic_term [] in
+ id, Some (name,Cic.ADef term)
+ | D.T_element "Hidden" -> id, None
+ | _ -> raise (IllFormedXml 14)
+ ) canonical_context
+ in
+ rget ((id, no, canonical_context, typ)::c, v) tl
| value::tl when value#node_type = D.T_element "body" ->
- let v' = (get_content value)#extension#to_cic_term in
+ let v' = (get_content value)#extension#to_cic_term [] in
(match v with
- None -> rget (c, Some v', t) tl
+ None -> rget (c, Some v') 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)
+ match rget ([], None) l with
+ (revc, Some v) -> (List.rev revc, v)
| _ -> raise (IllFormedXml 5)
;;
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
+ 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
+ and ty = (get_content con)#extension#to_cic_term [] in
+ rget (a,(id,ty)::c) tl
| _ -> raise (IllFormedXml 9)
in
match rget (None,[]) l with
| he::tl ->
let tyname = string_of_attr (he#attribute "name")
and inductive = bool_of_attr (he#attribute "inductive")
+ and xid = string_of_attr (he#attribute "id")
and (arity,cons) =
get_names_arity_constructors (he#sub_nodes)
in
- (tyname,inductive,arity,cons)::(get_inductive_types tl) (*CSC 0 a caso *)
+ (xid,tyname,inductive,arity,cons)::(get_inductive_types tl)
;;
(* This is the main function and also the only one used directly from *)
(* 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 rec get_term (n : CicParser3.cic_term Pxp_document.node) nbody
+=
+ let module U = UriManager in
let module D = Pxp_document in
let module C = Cic in
- let ntype = n # node_type 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
- C.ADefinition (xid, id, value, typ, params)
- | 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
- C.AAxiom (xid, id, typ, params)
- | 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
- C.ACurrentProof (xid, name, conjs, value, typ)
+ D.T_element "ConstantType" ->
+ let name = string_of_attr (n # attribute "name") in
+ let params = uri_list_of_attr (n#attribute "params") in
+ let xid = string_of_attr (n#attribute "id") in
+ let typ = (get_content n)#extension#to_cic_term [] in
+ (match nbody with
+ None ->
+ (* Axiom *)
+ C.AConstant (xid, None, name, None, typ, params)
+ | Some nbody' ->
+ let nbodytype = nbody'#node_type in
+ match nbodytype with
+ D.T_element "ConstantBody" ->
+(*CSC: the attribute "for" is ignored and not checked
+ let for_ = string_of_attr (nbody'#attribute "for") in
+*)
+ let paramsbody = uri_list_of_attr (nbody'#attribute "params") in
+ let xidbody = string_of_attr (nbody'#attribute "id") in
+ let value = (get_content nbody')#extension#to_cic_term [] in
+ if paramsbody = params then
+ C.AConstant (xid, Some xidbody, name, Some value, typ, params)
+ else
+ raise (IllFormedXml 6)
+ | D.T_element "CurrentProof" ->
+(*CSC: the attribute "of" is ignored and not checked
+ let for_ = string_of_attr (nbody'#attribute "of") in
+*)
+ let xidbody = string_of_attr (nbody'#attribute "id") in
+ let sons = nbody'#sub_nodes in
+ let (conjs, value) = get_conjs_value sons in
+ C.ACurrentProof (xid, xidbody, name, conjs, value, typ, params)
+ | D.T_element _
+ | D.T_data
+ | _ -> raise (IllFormedXml 6)
+ )
| D.T_element "InductiveDefinition" ->
let sons = n#sub_nodes
and xid = string_of_attr (n#attribute "id") in
C.AInductiveDefinition (xid, inductiveTypes, params, nparams)
| D.T_element "Variable" ->
let name = string_of_attr (n#attribute "name")
+ and params = uri_list_of_attr (n#attribute "params")
and xid = string_of_attr (n#attribute "id")
and (body, typ) =
let sons = n#sub_nodes in
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)
+ (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)
+ (None, t'#extension#to_cic_term [])
| _ -> raise (IllFormedXml 6)
in
- C.AVariable (xid,name,body,typ)
+ C.AVariable (xid,name,body,typ,params)
| D.T_element _
| D.T_data
- | _ ->
- raise (IllFormedXml 7)
+ | _ -> raise (IllFormedXml 7)
;;
projects / helm.git / blobdiff