X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic%2FcicParser2.ml;h=15bc2b9350f88f090cc2a538c06bf78c8cd0e128;hb=5325734bc2e4927ed7ec146e35a6f0f2b49f50c1;hp=4865c6e4a584fcb82bf05e2bb300cd549353e9e6;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git diff --git a/helm/ocaml/cic/cicParser2.ml b/helm/ocaml/cic/cicParser2.ml index 4865c6e4a..15bc2b935 100644 --- a/helm/ocaml/cic/cicParser2.ml +++ b/helm/ocaml/cic/cicParser2.ml @@ -42,64 +42,11 @@ 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 + T.Value s -> + List.map UriManager.uri_of_string (Str.split (Str.regexp " ") s) | _ -> raise (IllFormedXml 0) ;; @@ -123,7 +70,7 @@ let name_of_attr a = let module C = Cic in match a with T.Value s -> C.Name s - | T.Implied_value -> C.Anonimous + | T.Implied_value -> C.Anonymous | _ -> raise (IllFormedXml 0) ;; @@ -145,50 +92,46 @@ 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") 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, + (get_content typ)#extension#to_cic_term [], List.map (function n -> - 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 - 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 - Some (name,Cic.ADef term) - | D.T_element "Hidden" -> None - | _ -> raise (IllFormedXml 14) + 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 ((no, canonical_context, typ)::c, v, t) tl + 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 - (revc, Some v, Some t) -> (List.rev revc, v, t) + match rget ([], None) l with + (revc, Some v) -> (List.rev revc, v) | _ -> raise (IllFormedXml 5) ;; @@ -200,12 +143,12 @@ let get_names_arity_constructors l = 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 @@ -220,10 +163,11 @@ let rec get_inductive_types = | 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 *) @@ -231,40 +175,48 @@ let rec get_inductive_types = (* 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 @@ -274,6 +226,7 @@ let rec get_term n = 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 @@ -283,15 +236,14 @@ let rec get_term n = 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) ;;