*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
*
* This file is part of HELM, an Hypertextual, Electronic
* Library of Mathematics, developed at the Computer Science
X.xml_empty "REL"
[None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
None,"idref",idref ; None,"sort",sort]
| C.AVar (id,uri,exp_named_subst) ->
X.xml_empty "REL"
[None,"value",(string_of_int n) ; None,"binder",b ; None,"id",id ;
None,"idref",idref ; None,"sort",sort]
| C.AVar (id,uri,exp_named_subst) ->
aux_subst uri
(X.xml_empty "VAR"
[None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
exp_named_subst
| C.AMeta (id,n,l) ->
aux_subst uri
(X.xml_empty "VAR"
[None,"uri",U.string_of_uri uri;None,"id",id;None,"sort",sort])
exp_named_subst
| C.AMeta (id,n,l) ->
X.xml_nempty "META"
[None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort]
(List.fold_left
X.xml_nempty "META"
[None,"no",(string_of_int n) ; None,"id",id ; None,"sort",sort]
(List.fold_left
in
X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
| C.AImplicit _ -> raise NotImplemented
in
X.xml_empty "SORT" [None,"value",(string_of_sort s) ; None,"id",id]
| C.AImplicit _ -> raise NotImplemented
let attrs =
(None,"id",id)::(None,"type",sort)::
match binder with
let attrs =
(None,"id",id)::(None,"type",sort)::
match binder with
X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort]
[< X.xml_nempty "term" [] (aux v) ;
X.xml_nempty "type" [] (aux t)
X.xml_nempty "CAST" [None,"id",id ; None,"sort",sort]
[< X.xml_nempty "term" [] (aux v) ;
X.xml_nempty "type" [] (aux t)
let attrs =
(None,"id",id)::(None,"type",sort)::
match binder with
let attrs =
(None,"id",id)::(None,"type",sort)::
match binder with
let attrs =
(None,"id",id)::(None,"sort",sort)::
match binder with
let attrs =
(None,"id",id)::(None,"sort",sort)::
match binder with
X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort]
[< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
>]
| C.AConst (id,uri,exp_named_subst) ->
X.xml_nempty "APPLY" [None,"id",id ; None,"sort",sort]
[< (List.fold_right (fun x i -> [< (aux x) ; i >]) li [<>])
>]
| C.AConst (id,uri,exp_named_subst) ->
aux_subst uri
(X.xml_empty "CONST"
[None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
aux_subst uri
(X.xml_empty "CONST"
[None,"uri",(U.string_of_uri uri) ; None,"id",id ; None,"sort",sort]
None, "id", id]
) exp_named_subst
| C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
None, "id", id]
) exp_named_subst
| C.AMutConstruct (id,uri,i,j,exp_named_subst) ->
aux_subst uri
(X.xml_empty "MUTCONSTRUCT"
[None,"uri", (U.string_of_uri uri) ;
aux_subst uri
(X.xml_empty "MUTCONSTRUCT"
[None,"uri", (U.string_of_uri uri) ;
None,"id",id ; None,"sort",sort]
) exp_named_subst
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
None,"id",id ; None,"sort",sort]
) exp_named_subst
| C.AMutCase (id,uri,typeno,ty,te,patterns) ->
X.xml_nempty "MUTCASE"
[None,"uriType",(U.string_of_uri uri) ;
None,"noType", (string_of_int typeno) ;
X.xml_nempty "MUTCASE"
[None,"uriType",(U.string_of_uri uri) ;
None,"noType", (string_of_int typeno) ;
X.xml_nempty "FIX"
[None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
[< List.fold_right
X.xml_nempty "FIX"
[None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
[< List.fold_right
X.xml_nempty "COFIX"
[None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
[< List.fold_right
X.xml_nempty "COFIX"
[None,"noFun", (string_of_int no) ; None,"id",id ; None,"sort",sort]
[< List.fold_right
- C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params) ->
+ C.ACurrentProof (id,idbody,n,conjectures,bo,ty,params,obj_attrs) ->
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]
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]
(fun i (cid,n,canonical_context,t) ->
[< i ;
X.xml_nempty "Conjecture"
(fun i (cid,n,canonical_context,t) ->
[< i ;
X.xml_nempty "Conjecture"
- | C.AConstant (id,idbody,n,bo,ty,params) ->
+ | C.AConstant (id,idbody,n,bo,ty,params,obj_attrs) ->
X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
X.xml_nempty "ConstantType"
[None,"name",n ; None,"params",params' ; None,"id", id]
X.xml_cdata ("<!DOCTYPE ConstantType SYSTEM \""^ dtdname ^ "\">\n");
X.xml_nempty "ConstantType"
[None,"name",n ; None,"params",params' ; None,"id", id]
- | C.AVariable (id,n,bo,ty,params) ->
+ | C.AVariable (id,n,bo,ty,params,obj_attrs) ->
X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
X.xml_nempty "Variable"
[None,"name",n ; None,"params",params' ; None,"id", id]
X.xml_cdata ("<!DOCTYPE Variable SYSTEM \"" ^ dtdname ^ "\">\n");
X.xml_nempty "Variable"
[None,"name",n ; None,"params",params' ; None,"id", id]
- | C.AInductiveDefinition (id,tys,params,nparams) ->
+ | C.AInductiveDefinition (id,tys,params,nparams,obj_attrs) ->
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
[< X.xml_cdata "<?xml version=\"1.0\" encoding=\"ISO-8859-1\"?>\n" ;
X.xml_cdata
("<!DOCTYPE InductiveDefinition SYSTEM \"" ^ dtdname ^ "\">\n") ;
(fun i (id,typename,finite,arity,cons) ->
[< i ;
X.xml_nempty "InductiveType"
(fun i (id,typename,finite,arity,cons) ->
[< i ;
X.xml_nempty "InductiveType"