123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128(************************************************************************)(* * The Coq Proof Assistant / The Coq Development Team *)(* v * Copyright INRIA, CNRS and contributors *)(* <O___,, * (see version control and CREDITS file for authors & dates) *)(* \VV/ **************************************************************)(* // * This file is distributed under the terms of the *)(* * GNU Lesser General Public License Version 2.1 *)(* * (see LICENSE file for the text of the license) *)(************************************************************************)openXml_datatypeexceptionMarshal_errorofstring*xml(** Utility functions *)letrecget_attrattr=function|[]->raiseNot_found|(k,v)::lwhenCString.equalkattr->v|_::l->get_attrattrlletmassocxl=tryget_attrxlwithNot_found->raise(Marshal_error("attribute "^x,PCData"not there"))letconstructortcargs=Element(t,["val",c],args)letdo_matchtmf=function|Element(s,attrs,args)whenCString.equalst->letc=massoc"val"attrsinmfcargs|x->raise(Marshal_error(t,x))letsingleton=function|[x]->x|l->raise(Marshal_error("singleton",PCData("list of length "^string_of_int(List.lengthl))))letempty=function|[]->()|l->raise(Marshal_error("empty",PCData("list of length "^string_of_int(List.lengthl))))letraw_string=function|[]->""|[PCDatas]->s|x::_->raise(Marshal_error("raw string",x))(** Base types *)letof_unit()=Element("unit",[],[])letto_unit:xml->unit=function|Element("unit",[],[])->()|x->raise(Marshal_error("unit",x))letof_bool(b:bool):xml=ifbthenconstructor"bool""true"[]elseconstructor"bool""false"[]letto_bool:xml->bool=do_match"bool"(funs_->matchswith|"true"->true|"false"->false|x->raise(Marshal_error("bool",PCDatax)))letof_list(f:'a->xml)(l:'alist)=Element("list",[],List.mapfl)letto_list(f:xml->'a):xml->'alist=function|Element("list",[],l)->List.mapfl|x->raise(Marshal_error("list",x))letof_option(f:'a->xml):'aoption->xml=function|None->Element("option",["val","none"],[])|Somex->Element("option",["val","some"],[fx])letto_option(f:xml->'a):xml->'aoption=function|Element("option",["val","none"],[])->None|Element("option",["val","some"],[x])->Some(fx)|x->raise(Marshal_error("option",x))letof_string(s:string):xml=Element("string",[],[PCDatas])letto_string:xml->string=function|Element("string",[],l)->raw_stringl|x->raise(Marshal_error("string",x))letof_int(i:int):xml=Element("int",[],[PCData(string_of_inti)])letto_int:xml->int=function|Element("int",[],[PCDatas])->(tryint_of_stringswithFailure_->raise(Marshal_error("int",PCDatas)))|x->raise(Marshal_error("int",x))letof_pair(f:'a->xml)(g:'b->xml)(x:'a*'b):xml=Element("pair",[],[f(fstx);g(sndx)])letto_pair(f:xml->'a)(g:xml->'b):xml->'a*'b=function|Element("pair",[],[x;y])->(fx,gy)|x->raise(Marshal_error("pair",x))letof_union(f:'a->xml)(g:'b->xml):('a,'b)CSig.union->xml=function|CSig.Inlx->Element("union",["val","in_l"],[fx])|CSig.Inrx->Element("union",["val","in_r"],[gx])letto_union(f:xml->'a)(g:xml->'b):xml->('a,'b)CSig.union=function|Element("union",["val","in_l"],[x])->CSig.Inl(fx)|Element("union",["val","in_r"],[x])->CSig.Inr(gx)|x->raise(Marshal_error("union",x))(** More elaborate types *)letof_edit_idi=Element("edit_id",["val",string_of_inti],[])letto_edit_id=function|Element("edit_id",["val",i],[])->letid=int_of_stringiinassert(id<=0);id|x->raise(Marshal_error("edit_id",x))letof_locloc=letstart,stop=Loc.unloclocinElement("loc",[("start",string_of_intstart);("stop",string_of_intstop)],[])letto_locxml=matchxmlwith|Element("loc",l,[])->letstart=massoc"start"linletstop=massoc"stop"lin(tryLoc.make_loc(int_of_stringstart,int_of_stringstop)withNot_found|Invalid_argument_->raise(Marshal_error("loc",PCData(start^":"^stop))))|x->raise(Marshal_error("loc",x))letof_xmlx=Element("xml",[],[x])letto_xmlxml=matchxmlwith|Element("xml",[],[x])->x|x->raise(Marshal_error("xml",x))