) [< >] lambdas ;
X.xml_nempty "target" [] (aux t)
>]
- | C.ALetIn (xid,C.Anonymous,s,t) ->
+ | C.ALetIn (xid,C.Anonymous,s,ty,t) ->
assert false
- | C.ALetIn (last_id,C.Name _,_,_) as letins ->
+ | C.ALetIn (last_id,C.Name _,_,_,_) as letins ->
let rec eat_letins =
function
- C.ALetIn (id,n,s,t) ->
+ C.ALetIn (id,n,s,ty,t) ->
let letins,t' = eat_letins t in
- (id,n,s)::letins,t'
+ (id,n,s,ty)::letins,t'
| t -> [],t
in
let letins,t = eat_letins letins in
let sort = find_sort "sort" last_id in
X.xml_nempty "LETIN" sort
[< List.fold_left
- (fun i (id,binder,s) ->
+ (fun i (id,binder,s,ty) ->
let sort = find_sort "sort" id in
let attrs =
sort @ ((None,"id",id)::
C.Anonymous -> []
| C.Name b -> [None,"binder",b])
in
- [< i ; X.xml_nempty "def" attrs (aux s) >]
+ [< i ; X.xml_nempty "def" attrs [< aux s ; aux ty >] >]
) [< >] letins ;
X.xml_nempty "target" [] (aux t)
>]
aux
;;
-let xml_of_attrs attributes =
+let xml_of_attrs generate_attributes attributes =
let class_of = function
| `Coercion n ->
Xml.xml_empty "class" [None,"value","coercion";None,"arity",string_of_int n]
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"]
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. *)
[None,"id",hid;None,"name",n']
| C.Anonymous -> [None,"id",hid])
(print_term ?ids_to_inner_sorts t)
- | Some (n,C.ADef t) ->
+ | Some (n,C.ADef (t,_)) ->
X.xml_nempty "Def"
(match n with
C.Name n' ->
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") ;