From 6a6d9950d0c3a7974bc0f0d8a85369b733138647 Mon Sep 17 00:00:00 2001 From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:29:48 +0000 Subject: [PATCH] attributes support (not yet in the pretty printer) --- helm/ocaml/cic_transformations/cic2Xml.ml | 27 +++++++++++++++-------- 1 file changed, 18 insertions(+), 9 deletions(-) diff --git a/helm/ocaml/cic_transformations/cic2Xml.ml b/helm/ocaml/cic_transformations/cic2Xml.ml index b3467ad9e..5d614db05 100644 --- a/helm/ocaml/cic_transformations/cic2Xml.ml +++ b/helm/ocaml/cic_transformations/cic2Xml.ml @@ -265,20 +265,25 @@ let print_term ~ids_to_inner_sorts = aux ;; + (* TODO ZACK implement attributes pretty printing *) +let xml_of_attrs attributes = [< >] + let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = let module C = Cic in let module X = Xml in let module U = UriManager in let dtdname = dtdname ~ask_dtd_to_the_getter "cic.dtd" in match obj with - C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) -> + C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) -> let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs obj_attrs in let xml_for_current_proof_body = (*CSC: Should the CurrentProof also have the list of variables it depends on? *) (*CSC: I think so. Not implemented yet. *) X.xml_nempty "CurrentProof" [None,"of",UriManager.string_of_uri uri ; None,"id", id] - [< List.fold_left + [< xml_attrs; + List.fold_left (fun i (cid,n,canonical_context,t) -> [< i ; X.xml_nempty "Conjecture" @@ -309,7 +314,7 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = (print_term ids_to_inner_sorts t) >] >]) - [<>] conjectures ; + [< >] conjectures ; X.xml_nempty "body" [] (print_term ids_to_inner_sorts bo) >] in let xml_for_current_proof_type = @@ -329,8 +334,9 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = >] in xmlty, Some xmlbo - | C.AConstant (id,idbody,n,bo,ty,params) -> + | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) -> let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs obj_attrs in let xmlbo = match bo with None -> None @@ -351,12 +357,13 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\n"); X.xml_nempty "ConstantType" [None,"name",n ; None,"params",params' ; None,"id", id] - [< print_term ids_to_inner_sorts ty >] + [< xml_attrs; print_term ids_to_inner_sorts ty >] >] in xmlty, xmlbo - | C.AVariable (id,n,bo,ty,params) -> + | C.AVariable (id,n,bo,ty,params,obj_attrs) -> let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs obj_attrs in let xmlbo = match bo with None -> [< >] @@ -368,14 +375,15 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = X.xml_cdata ("\n"); X.xml_nempty "Variable" [None,"name",n ; None,"params",params' ; None,"id", id] - [< xmlbo ; + [< xml_attrs; xmlbo; X.xml_nempty "type" [] (print_term ids_to_inner_sorts ty) >] >] in aobj, None - | C.AInductiveDefinition (id,tys,params,nparams) -> + | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) -> let params' = param_attribute_of_params params in + let xml_attrs = xml_of_attrs obj_attrs in [< X.xml_cdata "\n" ; X.xml_cdata ("\n") ; @@ -383,7 +391,8 @@ let print_object uri ~ids_to_inner_sorts ~ask_dtd_to_the_getter obj = [None,"noParams",string_of_int nparams ; None,"id",id ; None,"params",params'] - [< (List.fold_left + [< xml_attrs; + (List.fold_left (fun i (id,typename,finite,arity,cons) -> [< i ; X.xml_nempty "InductiveType" -- 2.39.2