aux
;;
-let xml_of_attrs attributes =
+let xml_of_attrs generate_attributes attributes =
let class_of = function
- | `Coercion -> Xml.xml_empty "class" [None,"value","coercion"]
+ | `Coercion n ->
+ Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
| `Elim s ->
Xml.xml_nempty "class" [None,"value","elim"]
[< Xml.xml_empty
| `Record field_names ->
Xml.xml_nempty "class" [None,"value","record"]
(List.fold_right
- (fun (name,coercion) res ->
+ (fun (name,coercion,arity) res ->
[< Xml.xml_empty "field"
- [None,"name",if coercion then name ^ " coercion" else name];
+ [None,"name",
+ if coercion then
+ name ^ " coercion " ^ string_of_int arity
+ else
+ name];
res >]
) field_names [<>])
| `Projection -> Xml.xml_empty "class" [None,"value","projection"]
+ | `InversionPrinciple -> Xml.xml_empty "class" [None,"value","inversion"]
in
let flavour_of = function
| `Definition -> Xml.xml_empty "flavour" [None, "value", "definition"]
+ | `MutualDefinition ->
+ Xml.xml_empty "flavour" [None, "value", "mutual_definition"]
| `Fact -> Xml.xml_empty "flavour" [None, "value", "fact"]
| `Lemma -> Xml.xml_empty "flavour" [None, "value", "lemma"]
| `Remark -> Xml.xml_empty "flavour" [None, "value", "remark"]
| `Theorem -> Xml.xml_empty "flavour" [None, "value", "theorem"]
| `Variant -> Xml.xml_empty "flavour" [None, "value", "variant"]
+ | `Axiom -> Xml.xml_empty "flavour" [None, "value", "axiom"]
in
let xml_attr_of = function
| `Generated -> Xml.xml_empty "generated" []
List.fold_right
(fun attr res -> [< xml_attr_of attr ; res >]) attributes [<>]
in
- Xml.xml_nempty "attributes" [] xml_attrs
+ if generate_attributes then Xml.xml_nempty "attributes" [] xml_attrs else [<>]
-let print_object uri ?ids_to_inner_sorts ~ask_dtd_to_the_getter obj =
+let print_object uri
+ ?ids_to_inner_sorts ?(generate_attributes=true) ~ask_dtd_to_the_getter obj =
let module C = Cic in
let module X = Xml in
let module U = UriManager in
match obj with
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_attrs = xml_of_attrs generate_attributes 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. *)
xmlty, Some xmlbo
| 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 xml_attrs = xml_of_attrs generate_attributes obj_attrs in
let xmlbo =
match bo with
None -> None
xmlty, xmlbo
| 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 xml_attrs = xml_of_attrs generate_attributes obj_attrs in
let xmlbo =
match bo with
None -> [< >]
aobj, None
| 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
+ let xml_attrs = xml_of_attrs generate_attributes obj_attrs in
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;