1234567891011121314151617181920212223242526272829303132333435363738394041424344454647484950515253545556575859606162636465666768697071727374757677787980818283848586878889909192939495969798991001011021031041051061071081091101111121131141151161171181191201211221231241251261271281291301311321331341351361371381391401411421431441451461471481491501511521531541551561571581591601611621631641651661671681691701711721731741751761771781791801811821831841851861871881891901911921931941951961971981992002012022032042052062072082092102112122132142152162172182192202212222232242252262272282292302312322332342352362372382392402412422432442452462472482492502512522532542552562572582592602612622632642652662672682692702712722732742752762772782792802812822832842852862872882892902912922932942952962972982993003013023033043053063073083093103113123133143153163173183193203213223233243253263273283293303313323333343353363373383393403413423433443453463473483493503513523533543553563573583593603613623633643653663673683693703713723733743753763773783793803813823833843853863873883893903913923933943953963973983994004014024034044054064074084094104114124134144154164174184194204214224234244254264274284294304314324334344354364374384394404414424434444454464474484494504514524534544554564574584594604614624634644654664674684694704714724734744754764774784794804814824834844854864874884894904914924934944954964974984995005015025035045055065075085095105115125135145155165175185195205215225235245255265275285295305315325335345355365375385395405415425435445455465475485495505515525535545555565575585595605615625635645655665675685695705715725735745755765775785795805815825835845855865875885895905915925935945955965975985996006016026036046056066076086096106116126136146156166176186196206216226236246256266276286296306316326336346356366376386396406416426436446456466476486496506516526536546556566576586596606616626636646656666676686696706716726736746756766776786796806816826836846856866876886896906916926936946956966976986997007017027037047057067077087097107117127137147157167177187197207217227237247257267277287297307317327337347357367377387397407417427437447457467477487497507517527537547557567577587597607617627637647657667677687697707717727737747757767777787797807817827837847857867877887897907917927937947957967977987998008018028038048058068078088098108118128138148158168178188198208218228238248258268278288298308318328338348358368378388398408418428438448458468478488498508518528538548558568578588598608618628638648658668678688698708718728738748758768778788798808818828838848858868878888898908918928938948958968978988999009019029039049059069079089099109119129139149159169179189199209219229239249259269279289299309319329339349359369379389399409419429439449459469479489499509519529539549559569579589599609619629639649659669679689699709719729739749759769779789799809819829839849859869879889899909919929939949959969979989991000100110021003100410051006100710081009101010111012101310141015101610171018101910201021102210231024102510261027102810291030103110321033103410351036103710381039104010411042104310441045104610471048104910501051105210531054105510561057105810591060106110621063106410651066106710681069107010711072107310741075107610771078107910801081108210831084108510861087108810891090109110921093109410951096109710981099110011011102110311041105110611071108110911101111111211131114111511161117111811191120112111221123112411251126112711281129113011311132113311341135113611371138113911401141114211431144114511461147114811491150115111521153115411551156115711581159116011611162116311641165116611671168116911701171117211731174117511761177117811791180118111821183118411851186118711881189119011911192119311941195119611971198119912001201120212031204120512061207120812091210121112121213121412151216121712181219122012211222122312241225122612271228122912301231123212331234123512361237123812391240124112421243124412451246124712481249125012511252125312541255125612571258125912601261126212631264126512661267126812691270127112721273127412751276127712781279128012811282128312841285128612871288128912901291129212931294129512961297129812991300130113021303130413051306130713081309131013111312131313141315131613171318131913201321132213231324132513261327132813291330133113321333133413351336133713381339134013411342134313441345134613471348134913501351135213531354135513561357135813591360136113621363136413651366136713681369137013711372137313741375137613771378137913801381138213831384138513861387138813891390139113921393139413951396139713981399140014011402140314041405140614071408140914101411141214131414141514161417141814191420142114221423142414251426142714281429143014311432143314341435143614371438143914401441144214431444144514461447144814491450145114521453145414551456145714581459146014611462146314641465146614671468146914701471147214731474147514761477147814791480148114821483148414851486148714881489149014911492149314941495149614971498149915001501150215031504150515061507150815091510151115121513151415151516151715181519152015211522152315241525152615271528152915301531153215331534153515361537153815391540154115421543154415451546154715481549155015511552155315541555155615571558155915601561156215631564156515661567156815691570157115721573157415751576157715781579158015811582158315841585158615871588158915901591159215931594159515961597159815991600160116021603160416051606160716081609161016111612161316141615161616171618161916201621162216231624162516261627162816291630163116321633163416351636163716381639164016411642164316441645164616471648164916501651165216531654165516561657165816591660166116621663166416651666166716681669167016711672167316741675167616771678167916801681168216831684168516861687168816891690169116921693169416951696169716981699170017011702170317041705170617071708170917101711171217131714171517161717171817191720172117221723172417251726172717281729173017311732173317341735173617371738173917401741174217431744174517461747174817491750175117521753175417551756175717581759176017611762176317641765176617671768176917701771177217731774177517761777177817791780178117821783178417851786178717881789179017911792179317941795179617971798179918001801180218031804180518061807180818091810181118121813181418151816181718181819182018211822182318241825182618271828182918301831183218331834183518361837183818391840184118421843184418451846184718481849185018511852185318541855185618571858185918601861(* camlp5r *)(* grammar.ml,v *)(* Copyright (c) INRIA 2007-2017 *)openGramextopenFormatopenUtil(* Functorial interface *)typenorectypemayrecmoduletypeS=sigtypetetype'cpatterntypety_pattern=TPattern:'apattern->ty_patternmoduleParsable:sigtypet(** [Parsable.t] Stream tokenizers with Coq-specific funcitonality *)valmake:?loc:Loc.t->?fix_loc:(Loc.t->Loc.t)->charStream.t->t(** [make ?loc strm] Build a parsable from stream [strm], resuming
at position [?loc] *)valcomments:t->((int*int)*string)listvalloc:t->Loc.t(** [loc pa] Return parsing position for [pa] *)valconsume:t->int->unit(** [consume pa n] Discard [n] tokens from [pa], updating the
parsing position *)endmoduleEntry:sigtype'atvalmake:string->'atvalcreate:string->'atvalparse:'at->Parsable.t->'avalname:'at->stringtype'aparser_fun={parser_fun:teLStream.t->'a}valof_parser:string->'aparser_fun->'atvalparse_token_stream:'at->teLStream.t->'avalprint:Format.formatter->'at->unitvalis_empty:'at->booltypeany_t=Any:'at->any_tvalaccumulate_in:'at->any_tlistCString.Map.tendmodulerecSymbol:sigtype('self,'trec,'a)tvalnterm:'aEntry.t->('self,norec,'a)tvalnterml:'aEntry.t->string->('self,norec,'a)tvallist0:('self,'trec,'a)t->('self,'trec,'alist)tvallist0sep:('self,'trec,'a)t->('self,norec,unit)t->bool->('self,'trec,'alist)tvallist1:('self,'trec,'a)t->('self,'trec,'alist)tvallist1sep:('self,'trec,'a)t->('self,norec,unit)t->bool->('self,'trec,'alist)tvalopt:('self,'trec,'a)t->('self,'trec,'aoption)tvalself:('self,mayrec,'self)tvalnext:('self,mayrec,'self)tvaltoken:'cpattern->('self,norec,'c)tvaltokens:ty_patternlist->('self,norec,unit)tvalrules:'aRules.tlist->('self,norec,'a)tendandRule:sigtype('self,'trec,'f,'r)tvalstop:('self,norec,'r,'r)tvalnext:('self,_,'a,'r)t->('self,_,'b)Symbol.t->('self,mayrec,'b->'a,'r)tvalnext_norec:('self,norec,'a,'r)Rule.t->('self,norec,'b)Symbol.t->('self,norec,'b->'a,'r)tendandRules:sigtype'atvalmake:(_,norec,'f,Loc.t->'a)Rule.t->'f->'atendmoduleProduction:sigtype'atvalmake:('a,_,'f,Loc.t->'a)Rule.t->'f->'atendtype'asingle_extend_statement=stringoption*Gramext.g_assocoption*'aProduction.tlisttype'aextend_statement=|Reuseofstringoption*'aProduction.tlist|FreshofGramext.position*'asingle_extend_statementlistvalgeneralize_symbol:('a,'tr,'c)Symbol.t->('a,norec,'c)Symbol.toption(* Used in custom entries, should tweak? *)vallevel_of_nonterm:('a,norec,'c)Symbol.t->stringoptionendmoduletypeExtS=sigincludeSvalsafe_extend:'aEntry.t->'aextend_statement->unitvalsafe_delete_rule:'aEntry.t->'aProduction.t->unitmoduleUnsafe:sigvalclear_entry:'aEntry.t->unitendend(* Implementation *)moduleGMake(L:Plexing.S)=structtypete=L.tetype'cpattern='cL.patterntypety_pattern=TPattern:'apattern->ty_patterntype'aparser_t=L.teLStream.t->'a(** Used to propagate possible presence of SELF/NEXT in a rule (binary and) *)type('a,'b,'c)ty_and_rec=|NoRec2:(norec,norec,norec)ty_and_rec|MayRec2:('a,'b,mayrec)ty_and_rec(** Used to propagate possible presence of SELF/NEXT in a tree (ternary and) *)type('a,'b,'c,'d)ty_and_rec3=|NoRec3:(norec,norec,norec,norec)ty_and_rec3|MayRec3:('a,'b,'c,mayrec)ty_and_rec3type'aty_entry={ename:string;mutableestart:int->'aparser_t;mutableecontinue:int->int->'a->'aparser_t;mutableedesc:'aty_desc;}and'aty_desc=|Dlevelsof'aty_levellist|Dparserof'aparser_tand'aty_level=Level:(_,_,'a)ty_rec_level->'aty_leveland('trecs,'trecp,'a)ty_rec_level={assoc:g_assoc;lname:stringoption;lsuffix:('a,'trecs,'a->Loc.t->'a)ty_tree;lprefix:('a,'trecp,Loc.t->'a)ty_tree;}and('self,'trec,'a)ty_symbol=|Stoken:'cpattern->('self,norec,'c)ty_symbol|Stokens:ty_patternlist->('self,norec,unit)ty_symbol|Slist1:('self,'trec,'a)ty_symbol->('self,'trec,'alist)ty_symbol|Slist1sep:('self,'trec,'a)ty_symbol*('self,norec,unit)ty_symbol*bool->('self,'trec,'alist)ty_symbol|Slist0:('self,'trec,'a)ty_symbol->('self,'trec,'alist)ty_symbol|Slist0sep:('self,'trec,'a)ty_symbol*('self,norec,unit)ty_symbol*bool->('self,'trec,'alist)ty_symbol|Sopt:('self,'trec,'a)ty_symbol->('self,'trec,'aoption)ty_symbol|Sself:('self,mayrec,'self)ty_symbol|Snext:('self,mayrec,'self)ty_symbol|Snterm:'aty_entry->('self,norec,'a)ty_symbol(* norec but the entry can nevertheless introduce a loop with the current entry*)|Snterml:'aty_entry*string->('self,norec,'a)ty_symbol|Stree:('self,'trec,Loc.t->'a)ty_tree->('self,'trec,'a)ty_symboland('self,_,_,'r)ty_rule=|TStop:('self,norec,'r,'r)ty_rule|TNext:('trr,'trs,'tr)ty_and_rec*('self,'trr,'a,'r)ty_rule*('self,'trs,'b)ty_symbol->('self,'tr,'b->'a,'r)ty_ruleand('self,'trec,'a)ty_tree=|Node:('trn,'trs,'trb,'tr)ty_and_rec3*('self,'trn,'trs,'trb,'b,'a)ty_node->('self,'tr,'a)ty_tree|LocAct:'k*'klist->('self,norec,'k)ty_tree|DeadEnd:('self,norec,'k)ty_treeand('self,'trec,'trecs,'trecb,'a,'r)ty_node={node:('self,'trec,'a)ty_symbol;son:('self,'trecs,'a->'r)ty_tree;brother:('self,'trecb,'r)ty_tree;}type'aty_rules=|TRules:(_,norec,'act,Loc.t->'a)ty_rule*'act->'aty_rulestype'aty_production=|TProd:('a,_,'act,Loc.t->'a)ty_rule*'act->'aty_productionletrecderive_eps:typesra.(s,r,a)ty_symbol->bool=functionSlist0_->true|Slist0sep(_,_,_)->true|Sopt_->true|Street->tree_derive_epst|Slist1_->false|Slist1sep(_,_,_)->false|Snterm_->false|Snterml(_,_)->false|Snext->false|Sself->false|Stoken_->false|Stokens_->falseandtree_derive_eps:typestra.(s,tr,a)ty_tree->bool=functionLocAct(_,_)->true|Node(_,{node=s;brother=bro;son=son})->derive_epss&&tree_derive_epsson||tree_derive_epsbro|DeadEnd->false(** FIXME: find a way to do that type-safely *)leteq_entry:typea1a2.a1ty_entry->a2ty_entry->(a1,a2)eqoption=fune1e2->if(Obj.magice1)==(Obj.magice2)thenSome(Obj.magicRefl)elseNonelettok_pattern_eq_listpl1pl2=letf(TPatternp1)(TPatternp2)=Option.has_some(L.tok_pattern_eqp1p2)inifList.for_all2eqfpl1pl2thenSomeReflelseNoneletreceq_symbol:typesr1r2a1a2.(s,r1,a1)ty_symbol->(s,r2,a2)ty_symbol->(a1,a2)eqoption=funs1s2->matchs1,s2withSnterme1,Snterme2->eq_entrye1e2|Snterml(e1,l1),Snterml(e2,l2)->ifString.equall1l2theneq_entrye1e2elseNone|Slist0s1,Slist0s2->beginmatcheq_symbols1s2withNone->None|SomeRefl->SomeReflend|Slist0sep(s1,sep1,b1),Slist0sep(s2,sep2,b2)->ifb1=b2thenmatcheq_symbols1s2with|None->None|SomeRefl->matcheq_symbolsep1sep2with|None->None|SomeRefl->SomeReflelseNone|Slist1s1,Slist1s2->beginmatcheq_symbols1s2withNone->None|SomeRefl->SomeReflend|Slist1sep(s1,sep1,b1),Slist1sep(s2,sep2,b2)->ifb1=b2thenmatcheq_symbols1s2with|None->None|SomeRefl->matcheq_symbolsep1sep2with|None->None|SomeRefl->SomeReflelseNone|Sopts1,Sopts2->beginmatcheq_symbols1s2withNone->None|SomeRefl->SomeReflend|Stree_,Stree_->None|Sself,Sself->SomeRefl|Snext,Snext->SomeRefl|Stokenp1,Stokenp2->L.tok_pattern_eqp1p2|Stokenspl1,Stokenspl2->tok_pattern_eq_listpl1pl2|_->Noneletis_before:types1s2r1r2a1a2.(s1,r1,a1)ty_symbol->(s2,r2,a2)ty_symbol->bool=funs1s2->matchs1,s2with|Stokenp1,Stokenp2->snd(L.tok_pattern_stringsp1)<>None&&snd(L.tok_pattern_stringsp2)=None|Stoken_,_->true|_->false(** Ancillary datatypes *)type'aty_rec=MayRec:mayrecty_rec|NoRec:norecty_rectype('a,'b,'c)ty_and_ex=|NR00:(mayrec,mayrec,mayrec)ty_and_ex|NR01:(mayrec,norec,mayrec)ty_and_ex|NR10:(norec,mayrec,mayrec)ty_and_ex|NR11:(norec,norec,norec)ty_and_extype('a,'b)ty_mayrec_and_ex=|MayRecNR:('a,'b,_)ty_and_ex->('a,'b)ty_mayrec_and_extype('s,'a)ty_mayrec_symbol=|MayRecSymbol:('s,_,'a)ty_symbol->('s,'a)ty_mayrec_symboltype('s,'a)ty_mayrec_tree=|MayRecTree:('s,'tr,'a)ty_tree->('s,'a)ty_mayrec_treetype('s,'a,'r)ty_mayrec_rule=|MayRecRule:('s,_,'a,'r)ty_rule->('s,'a,'r)ty_mayrec_ruletype('self,'trec,_)ty_symbols=|TNil:('self,norec,unit)ty_symbols|TCns:('trh,'trt,'tr)ty_and_rec*('self,'trh,'a)ty_symbol*('self,'trt,'b)ty_symbols->('self,'tr,'a*'b)ty_symbols(** ('i, 'p, 'f, 'r) rel_prod0 ~
∃ α₁ ... αₙ.
p ≡ αₙ * ... α₁ * 'i ∧
f ≡ α₁ -> ... -> αₙ -> 'r
*)type('i,_,'f,_)rel_prod0=|Rel0:('i,'i,'f,'f)rel_prod0|RelS:('i,'p,'f,'a->'r)rel_prod0->('i,'a*'p,'f,'r)rel_prod0type('p,'k,'r)rel_prod=(unit,'p,'k,'r)rel_prod0type('s,'tr,'i,'k,'r)any_symbols=|AnyS:('s,'tr,'p)ty_symbols*('i,'p,'k,'r)rel_prod0->('s,'tr,'i,'k,'r)any_symbolstype('s,'tr,'k,'r)ty_belast_rule=|Belast:('trr,'trs,'tr)ty_and_rec*('s,'trr,'k,'a->'r)ty_rule*('s,'trs,'a)ty_symbol->('s,'tr,'k,'r)ty_belast_rule(* unfortunately, this is quadratic, but ty_rules aren't too long
* (99% of the time of length less or equal 10 and maximum is 22
* when compiling Coq and its standard library) *)letrecget_symbols:typestreckr.(s,trec,k,r)ty_rule->(s,trec,unit,k,r)any_symbols=letrecbelast_rule:typestrrtrstrakr.(trr,trs,tr)ty_and_rec->(s,trr,k,r)ty_rule->(s,trs,a)ty_symbol->(s,tr,a->k,r)ty_belast_rule=funarrs->matchar,rwith|NoRec2,TStop->Belast(NoRec2,TStop,s)|MayRec2,TStop->Belast(MayRec2,TStop,s)|NoRec2,TNext(NoRec2,r,s')->letBelast(NoRec2,r,s')=belast_ruleNoRec2rs'inBelast(NoRec2,TNext(NoRec2,r,s),s')|MayRec2,TNext(_,r,s')->letBelast(_,r,s')=belast_ruleMayRec2rs'inBelast(MayRec2,TNext(MayRec2,r,s),s')infunction|TStop->AnyS(TNil,Rel0)|TNext(MayRec2,r,s)->letBelast(MayRec2,r,s)=belast_ruleMayRec2rsinletAnyS(r,pf)=get_symbolsrinAnyS(TCns(MayRec2,s,r),RelSpf)|TNext(NoRec2,r,s)->letBelast(NoRec2,r,s)=belast_ruleNoRec2rsinletAnyS(r,pf)=get_symbolsrinAnyS(TCns(NoRec2,s,r),RelSpf)letget_rec_symbols(typestrp)(s:(s,tr,p)ty_symbols):trty_rec=matchswithTCns(MayRec2,_,_)->MayRec|TCns(NoRec2,_,_)->NoRec|TNil->NoRecletget_rec_tree(typestrf)(s:(s,tr,f)ty_tree):trty_rec=matchswithNode(MayRec3,_)->MayRec|Node(NoRec3,_)->NoRec|LocAct_->NoRec|DeadEnd->NoRecletand_symbols_tree(typestrstrtpf)(s:(s,trs,p)ty_symbols)(t:(s,trt,f)ty_tree):(trs,trt)ty_mayrec_and_ex=matchget_rec_symbolss,get_rec_treetwith|MayRec,MayRec->MayRecNRNR00|MayRec,NoRec->MayRecNRNR01|NoRec,MayRec->MayRecNRNR10|NoRec,NoRec->MayRecNRNR11letand_and_tree(typestr'trttrtrntrstrbf)(ar:(tr',trt,tr)ty_and_rec)(arn:(trn,trs,trb,trt)ty_and_rec3)(t:(s,trb,f)ty_tree):(tr',trb,tr)ty_and_rec=matchar,arn,get_rec_treetwith|MayRec2,_,MayRec->MayRec2|MayRec2,_,NoRec->MayRec2|NoRec2,NoRec3,NoRec->NoRec2letinsert_tree(typestrstrttrpka)entry_name(ar:(trs,trt,tr)ty_and_ex)(gsymbols:(s,trs,p)ty_symbols)(pf:(p,k,a)rel_prod)(action:k)(tree:(s,trt,a)ty_tree):(s,tr,a)ty_tree=letrecinsert:typetrstrttrpfk.(trs,trt,tr)ty_and_ex->(s,trs,p)ty_symbols->(p,k,f)rel_prod->(s,trt,f)ty_tree->k->(s,tr,f)ty_tree=funarsymbolspftreeaction->matchsymbols,pfwithTCns(ars,s,sl),RelSpf->(* descent in tree at symbol [s] *)insert_in_treeararssslpftreeaction|TNil,Rel0->(* insert the action *)letnode(typetb)({node=s;son=son;brother=bro}:(_,_,_,tb,_,_)ty_node)=letar:(norec,tb,tb)ty_and_ex=matchget_rec_treebrowithMayRec->NR10|NoRec->NR11in{node=s;son=son;brother=insertarTNilRel0broaction}inmatchar,treewith|NR10,Node(_,n)->Node(MayRec3,noden)|NR11,Node(NoRec3,n)->Node(NoRec3,noden)|NR11,LocAct(old_action,action_list)->(* What to do about this warning? For now it is disabled *)iffalsethenbeginletmsg="<W> Grammar extension: "^(ifentry_name=""then""else"in ["^entry_name^"%s], ")^"some rule has been masked"inFeedback.msg_warning(Pp.strmsg)end;LocAct(action,old_action::action_list)|NR11,DeadEnd->LocAct(action,[])andinsert_in_tree:typetrstrs'trs''trttrapfk.(trs'',trt,tr)ty_and_ex->(trs,trs',trs'')ty_and_rec->(s,trs,a)ty_symbol->(s,trs',p)ty_symbols->(p,k,a->f)rel_prod->(s,trt,f)ty_tree->k->(s,tr,f)ty_tree=funararssslpftreeaction->letar:(trs'',trt,tr)ty_and_rec=matcharwithNR11->NoRec2|NR00->MayRec2|NR01->MayRec2|NR10->MayRec2inmatchtry_insertararssslpftreeactionwithSomet->t|None->letnodear={node=s;son=insertarslpfDeadEndaction;brother=tree}inmatchar,ars,get_rec_symbolsslwith|MayRec2,MayRec2,MayRec->Node(MayRec3,nodeNR01)|MayRec2,_,NoRec->Node(MayRec3,nodeNR11)|NoRec2,NoRec2,NoRec->Node(NoRec3,nodeNR11)andtry_insert:typetrstrs'trs''trttrapfk.(trs'',trt,tr)ty_and_rec->(trs,trs',trs'')ty_and_rec->(s,trs,a)ty_symbol->(s,trs',p)ty_symbols->(p,k,a->f)rel_prod->(s,trt,f)ty_tree->k->(s,tr,f)ty_treeoption=funararssymbsymblpftreeaction->matchtreewithNode(arn,{node=symb1;son=son;brother=bro})->(* merging rule [symb; symbl -> action] in tree [symb1; son | bro] *)beginmatcheq_symbolsymbsymb1with|SomeRefl->(* reducing merge of [symb; symbl -> action] with [symb1; son] to merge of [symbl -> action] with [son] *)letMayRecNRarss=and_symbols_treesymblsoninletson=insertarsssymblpfsonactioninletnode={node=symb1;son=son;brother=bro}in(* propagate presence of SELF/NEXT *)beginmatchar,ars,arn,arsswith|MayRec2,_,_,_->Some(Node(MayRec3,node))|NoRec2,NoRec2,NoRec3,NR11->Some(Node(NoRec3,node))end|None->letar'=and_and_treeararnbroinifis_beforesymb1symb||derive_epssymb&¬(derive_epssymb1)then(* inserting new rule after current rule, i.e. in [bro] *)letbro=matchtry_insertar'arssymbsymblpfbroactionwithSomebro->(* could insert in [bro] *)bro|None->(* not ok to insert in [bro] or after; we insert now *)letMayRecNRarss=and_symbols_treesymblDeadEndinletson=insertarsssymblpfDeadEndactioninletnode={node=symb;son=son;brother=bro}in(* propagate presence of SELF/NEXT *)matchar,ars,arn,arsswith|MayRec2,_,_,_->Node(MayRec3,node)|NoRec2,NoRec2,NoRec3,NR11->Node(NoRec3,node)inletnode={node=symb1;son=son;brother=bro}in(* propagate presence of SELF/NEXT *)matchar,arnwith|MayRec2,_->Some(Node(MayRec3,node))|NoRec2,NoRec3->Some(Node(NoRec3,node))else(* should insert in [bro] or before the tree [symb1; son | bro] *)matchtry_insertar'arssymbsymblpfbroactionwithSomebro->(* could insert in [bro] *)letnode={node=symb1;son=son;brother=bro}inbeginmatchar,arnwith|MayRec2,_->Some(Node(MayRec3,node))|NoRec2,NoRec3->Some(Node(NoRec3,node))end|None->(* should insert before [symb1; son | bro] *)Noneend|LocAct(_,_)->None|DeadEnd->Noneininsertargsymbolspftreeactionletinsert_tree_norec(typespka)entry_name(gsymbols:(s,norec,p)ty_symbols)(pf:(p,k,a)rel_prod)(action:k)(tree:(s,norec,a)ty_tree):(s,norec,a)ty_tree=insert_treeentry_nameNR11gsymbolspfactiontreeletinsert_tree(typestrstrtpka)entry_name(gsymbols:(s,trs,p)ty_symbols)(pf:(p,k,a)rel_prod)(action:k)(tree:(s,trt,a)ty_tree):(s,a)ty_mayrec_tree=letMayRecNRar=and_symbols_treegsymbolstreeinMayRecTree(insert_treeentry_nameargsymbolspfactiontree)letsrules(typeselfa)(rl:aty_ruleslist):(self,norec,a)ty_symbol=letrecretype_tree:typesa.(s,norec,a)ty_tree->(self,norec,a)ty_tree=function|Node(NoRec3,{node=s;son=son;brother=bro})->Node(NoRec3,{node=retype_symbols;son=retype_treeson;brother=retype_treebro})|LocAct(k,kl)->LocAct(k,kl)|DeadEnd->DeadEndandretype_symbol:typesa.(s,norec,a)ty_symbol->(self,norec,a)ty_symbol=function|Stokenp->Stokenp|Stokensl->Stokensl|Slist1s->Slist1(retype_symbols)|Slist1sep(s,sep,b)->Slist1sep(retype_symbols,retype_symbolsep,b)|Slist0s->Slist0(retype_symbols)|Slist0sep(s,sep,b)->Slist0sep(retype_symbols,retype_symbolsep,b)|Sopts->Sopt(retype_symbols)|Snterme->Snterme|Snterml(e,l)->Snterml(e,l)|Street->Stree(retype_treet)inletrecretype_rule:typeskr.(s,norec,k,r)ty_rule->(self,norec,k,r)ty_rule=function|TStop->TStop|TNext(NoRec2,r,s)->TNext(NoRec2,retype_ruler,retype_symbols)inlett=List.fold_left(funtree(TRules(symbols,action))->letsymbols=retype_rulesymbolsinletAnyS(symbols,pf)=get_symbolssymbolsininsert_tree_norec""symbolspfactiontree)DeadEndrlinStreetletis_level_labelledn(Levellev)=matchlev.lnamewithSomen1->n=n1|None->falseletinsert_level(typestrpk)entry_name(symbols:(s,tr,p)ty_symbols)(pf:(p,k,Loc.t->s)rel_prod)(action:k)(slev:sty_level):sty_level=matchsymbolswith|TCns(_,Sself,symbols)->(* Insert a rule of the form "SELF; ...." *)letLevelslev=slevinletRelSpf=pfinletMayRecTreelsuffix=insert_treeentry_namesymbolspfactionslev.lsuffixinLevel{assoc=slev.assoc;lname=slev.lname;lsuffix=lsuffix;lprefix=slev.lprefix}|_->(* Insert a rule not starting with SELF *)letLevelslev=slevinletMayRecTreelprefix=insert_treeentry_namesymbolspfactionslev.lprefixinLevel{assoc=slev.assoc;lname=slev.lname;lsuffix=slev.lsuffix;lprefix=lprefix}letempty_levlnameassoc=letassoc=matchassocwithSomea->a|None->LeftAinLevel{assoc=assoc;lname=lname;lsuffix=DeadEnd;lprefix=DeadEnd}leterr_no_levelleve=letmsg=sprintf"Grammar.extend: No level labelled \"%s\" in entry \"%s\""leveinfailwithmsgletget_positionentrypositionlevs=matchpositionwithFirst->[],levs|Last->levs,[]|Beforen->letrecget=function[]->err_no_levelnentry.ename|lev::levs->ifis_level_labellednlevthen[],lev::levselselet(levs1,levs2)=getlevsinlev::levs1,levs2ingetlevs|Aftern->letrecget=function[]->err_no_levelnentry.ename|lev::levs->ifis_level_labellednlevthen[lev],levselselet(levs1,levs2)=getlevsinlev::levs1,levs2ingetlevsletget_levelentrynamelevs=matchnamewith|Somen->letrecget=function[]->err_no_levelnentry.ename|lev::levs->ifis_level_labellednlevthen[],lev,levselselet(levs1,rlev,levs2)=getlevsinlev::levs1,rlev,levs2ingetlevs|None->beginmatchlevswithlev::levs->[],lev,levs|[]->letmsg=sprintf"Grammar.extend: No top level in entry \"%s\""entry.enameinfailwithmsgendletchange_to_self0(types)(typetrec)(typea)(entry:sty_entry):(s,trec,a)ty_symbol->(s,a)ty_mayrec_symbol=function|Snterme->beginmatcheq_entryeentrywith|None->MayRecSymbol(Snterme)|SomeRefl->MayRecSymbol(Sself)end|x->MayRecSymbolxletrecchange_to_self:typestrecar.sty_entry->(s,trec,a,r)ty_rule->(s,a,r)ty_mayrec_rule=funer->matchrwith|TStop->MayRecRuleTStop|TNext(_,r,t)->letMayRecRuler=change_to_selferinletMayRecSymbolt=change_to_self0etinMayRecRule(TNext(MayRec2,r,t))letinsert_tokentok=L.tok_usingtokletinsert_tokenssymbols=letrecinsert:typestreca.(s,trec,a)ty_symbol->unit=function|Slist0s->inserts|Slist1s->inserts|Slist0sep(s,t,_)->inserts;insertt|Slist1sep(s,t,_)->inserts;insertt|Sopts->inserts|Street->tinsertt|Stokentok->insert_tokentok|Stokens(TPatterntok::_)->insert_tokentok(* Only the first token is liable to trigger a keyword effect *)|Stokens[]->assertfalse|Snterm_->()|Snterml(_,_)->()|Snext->()|Sself->()andtinsert:typestra.(s,tr,a)ty_tree->unit=functionNode(_,{node=s;brother=bro;son=son})->inserts;tinsertbro;tinsertson|LocAct(_,_)->()|DeadEnd->()andlinsert:typestrp.(s,tr,p)ty_symbols->unit=function|TNil->()|TCns(_,s,r)->inserts;linsertrinlinsertsymbolstype'asingle_extend_statement=stringoption*Gramext.g_assocoption*'aty_productionlisttype'aextend_statement=|Reuseofstringoption*'aty_productionlist|FreshofGramext.position*'asingle_extend_statementlistletadd_prodentrylev(TProd(symbols,action))=letMayRecRulesymbols=change_to_selfentrysymbolsinletAnyS(symbols,pf)=get_symbolssymbolsininsert_tokenssymbols;insert_levelentry.enamesymbolspfactionlevletlevels_of_rulesentryst=letelev=matchentry.edescwithDlevelselev->elev|Dparser_->letmsg=sprintf"Grammar.extend: entry not extensible: \"%s\""entry.enameinfailwithmsginmatchstwith|Reuse(name,[])->elev|Reuse(name,prods)->let(levs1,lev,levs2)=get_levelentrynameelevinletlev=List.fold_left(funlevprod->add_prodentrylevprod)levprodsinlevs1@[lev]@levs2|Fresh(position,rules)->let(levs1,levs2)=get_positionentrypositionelevinletfoldlevs(lname,assoc,prods)=letlev=empty_levlnameassocinletlev=List.fold_left(funlevprod->add_prodentrylevprod)levprodsinlev::levsinletlevs=List.fold_leftfold[]rulesinlevs1@List.revlevs@levs2letlogically_eq_symbolsentry=letreceq_symbols:types1s2trec1trec2a1a2.(s1,trec1,a1)ty_symbol->(s2,trec2,a2)ty_symbol->bool=funs1s2->matchs1,s2withSnterme1,Snterme2->e1.ename=e2.ename|Snterme1,Sself->e1.ename=entry.ename|Sself,Snterme2->entry.ename=e2.ename|Snterml(e1,l1),Snterml(e2,l2)->e1.ename=e2.ename&&l1=l2|Slist0s1,Slist0s2->eq_symbolss1s2|Slist0sep(s1,sep1,b1),Slist0sep(s2,sep2,b2)->eq_symbolss1s2&&eq_symbolssep1sep2&&b1=b2|Slist1s1,Slist1s2->eq_symbolss1s2|Slist1sep(s1,sep1,b1),Slist1sep(s2,sep2,b2)->eq_symbolss1s2&&eq_symbolssep1sep2&&b1=b2|Sopts1,Sopts2->eq_symbolss1s2|Street1,Street2->eq_treest1t2|Stokenp1,Stokenp2->L.tok_pattern_eqp1p2<>None|Stokenspl1,Stokenspl2->tok_pattern_eq_listpl1pl2<>None|Sself,Sself->true|Snext,Snext->true|_->falseandeq_trees:types1s2tr1tr2a1a2.(s1,tr1,a1)ty_tree->(s2,tr2,a2)ty_tree->bool=funt1t2->matcht1,t2withNode(_,n1),Node(_,n2)->eq_symbolsn1.noden2.node&&eq_treesn1.sonn2.son&&eq_treesn1.brothern2.brother|LocAct_,LocAct_->true|LocAct_,DeadEnd->true|DeadEnd,LocAct_->true|DeadEnd,DeadEnd->true|_->falseineq_symbols(* [delete_rule_in_tree] returns
[Some (dsl, t)] if success
[dsl] =
Some (list of deleted nodes) if branch deleted
None if action replaced by previous version of action
[t] = remaining tree
[None] if failure *)type'sex_symbols=|ExS:('s,'tr,'p)ty_symbols->'sex_symbolsletdelete_rule_in_treeentry=letrecdelete_in_tree:typestrtr'pr.(s,tr,p)ty_symbols->(s,tr',r)ty_tree->(sex_symbolsoption*(s,r)ty_mayrec_tree)option=funsymbolstree->matchsymbols,treewith|TCns(_,s,sl),Node(_,n)->iflogically_eq_symbolsentrysn.nodethendelete_sonslnelsebeginmatchdelete_in_treesymbolsn.brotherwithSome(dsl,MayRecTreet)->Some(dsl,MayRecTree(Node(MayRec3,{node=n.node;son=n.son;brother=t})))|None->Noneend|TCns(_,s,sl),_->None|TNil,Node(_,n)->beginmatchdelete_in_treeTNiln.brotherwithSome(dsl,MayRecTreet)->Some(dsl,MayRecTree(Node(MayRec3,{node=n.node;son=n.son;brother=t})))|None->Noneend|TNil,DeadEnd->None|TNil,LocAct(_,[])->Some(Some(ExSTNil),MayRecTreeDeadEnd)|TNil,LocAct(_,action::list)->Some(None,MayRecTree(LocAct(action,list)))anddelete_son:typesptrtrntrstrbar.(s,tr,p)ty_symbols->(s,trn,trs,trb,a,r)ty_node->(sex_symbolsoption*(s,r)ty_mayrec_tree)option=funsln->matchdelete_in_treesln.sonwithSome(Some(ExSdsl),MayRecTreeDeadEnd)->Some(Some(ExS(TCns(MayRec2,n.node,dsl))),MayRecTreen.brother)|Some(Some(ExSdsl),MayRecTreet)->lett=Node(MayRec3,{node=n.node;son=t;brother=n.brother})inSome(Some(ExS(TCns(MayRec2,n.node,dsl))),MayRecTreet)|Some(None,MayRecTreet)->lett=Node(MayRec3,{node=n.node;son=t;brother=n.brother})inSome(None,MayRecTreet)|None->Noneindelete_in_treeletrecdelete_rule_in_suffixentrysymbols=functionLevellev::levs->beginmatchdelete_rule_in_treeentrysymbolslev.lsuffixwithSome(dsl,MayRecTreet)->beginmatcht,lev.lprefixwithDeadEnd,DeadEnd->levs|_->letlev={assoc=lev.assoc;lname=lev.lname;lsuffix=t;lprefix=lev.lprefix}inLevellev::levsend|None->letlevs=delete_rule_in_suffixentrysymbolslevsinLevellev::levsend|[]->raiseNot_foundletrecdelete_rule_in_prefixentrysymbols=functionLevellev::levs->beginmatchdelete_rule_in_treeentrysymbolslev.lprefixwithSome(dsl,MayRecTreet)->beginmatcht,lev.lsuffixwithDeadEnd,DeadEnd->levs|_->letlev={assoc=lev.assoc;lname=lev.lname;lsuffix=lev.lsuffix;lprefix=t}inLevellev::levsend|None->letlevs=delete_rule_in_prefixentrysymbolslevsinLevellev::levsend|[]->raiseNot_foundletdelete_rule_in_level_list(typestrp)(entry:sty_entry)(symbols:(s,tr,p)ty_symbols)levs=matchsymbolswithTCns(_,Sself,symbols)->delete_rule_in_suffixentrysymbolslevs|TCns(_,Snterme,symbols')->beginmatcheq_entryeentrywith|None->delete_rule_in_prefixentrysymbolslevs|SomeRefl->delete_rule_in_suffixentrysymbols'levsend|_->delete_rule_in_prefixentrysymbolslevsletrecflatten_tree:typestra.(s,tr,a)ty_tree->sex_symbolslist=functionDeadEnd->[]|LocAct(_,_)->[ExSTNil]|Node(_,{node=n;brother=b;son=s})->List.map(fun(ExSl)->ExS(TCns(MayRec2,n,l)))(flatten_trees)@flatten_treebletutf8_print=reftrueletutf8_string_escapeds=letb=Buffer.create(String.lengths)inletrecloopi=ifi=String.lengthsthenBuffer.contentsbelsebeginbeginmatchs.[i]with'"'->Buffer.add_stringb"\\\""|'\\'->Buffer.add_stringb"\\\\"|'\n'->Buffer.add_stringb"\\n"|'\t'->Buffer.add_stringb"\\t"|'\r'->Buffer.add_stringb"\\r"|'\b'->Buffer.add_stringb"\\b"|c->Buffer.add_charbcend;loop(i+1)endinloop0letstring_escapeds=if!utf8_printthenutf8_string_escapedselseString.escapedsletprint_strppfs=fprintfppf"\"%s\""(string_escapeds)letprint_tokenbppfp=matchL.tok_pattern_stringspwith|"",Somes->print_strppfs|con,Someprm->ifbthenfprintfppf"%s@ %a"conprint_strprmelsefprintfppf"(%s@ %a)"conprint_strprm|con,None->fprintfppf"%s"conletprint_tokensppf=function|[]->assertfalse|TPatternp::pl->fprintfppf"[%a%a]"(print_tokentrue)p(funppf->List.iter(functionTPatternp->fprintfppf";@ ";print_tokentrueppfp))plletrecprint_symbol:typestrr.formatter->(s,tr,r)ty_symbol->unit=funppf->function|Slist0s->fprintfppf"LIST0 %a"print_symbol1s|Slist0sep(s,t,osep)->fprintfppf"LIST0 %a SEP %a%s"print_symbol1sprint_symbol1t(ifosepthen" OPT_SEP"else"")|Slist1s->fprintfppf"LIST1 %a"print_symbol1s|Slist1sep(s,t,osep)->fprintfppf"LIST1 %a SEP %a%s"print_symbol1sprint_symbol1t(ifosepthen" OPT_SEP"else"")|Sopts->fprintfppf"OPT %a"print_symbol1s|Stokenp->print_tokentrueppfp|Stokens[TPatternp]->print_tokentrueppfp|Stokenspl->print_tokensppfpl|Snterml(e,l)->fprintfppf"%s%s@ LEVEL@ %a"e.ename""print_strl|s->print_symbol1ppfsandprint_symbol1:typestrr.formatter->(s,tr,r)ty_symbol->unit=funppf->function|Snterme->fprintfppf"%s%s"e.ename""|Sself->pp_print_stringppf"SELF"|Snext->pp_print_stringppf"NEXT"|Stokenp->print_tokenfalseppfp|Stokens[TPatternp]->print_tokenfalseppfp|Stokenspl->print_tokensppfpl|Street->print_levelppfpp_print_space(flatten_treet)|s->fprintfppf"(%a)"print_symbolsandprint_rule:typestrp.formatter->(s,tr,p)ty_symbols->unit=funppfsymbols->fprintfppf"@[<hov 0>";letrecfold:typestrp._->(s,tr,p)ty_symbols->unit=funsepsymbols->matchsymbolswith|TNil->()|TCns(_,symbol,symbols)->fprintfppf"%t%a"sepprint_symbolsymbol;fold(funppf->fprintfppf";@ ")symbolsinlet()=fold(funppf->())symbolsinfprintfppf"@]"andprint_level:types._->_->sex_symbolslist->_=funppfpp_print_spacerules->fprintfppf"@[<hov 0>[ ";let()=Format.pp_print_list~pp_sep:(funppf()->fprintfppf"%a| "pp_print_space())(funppf(ExSrule)->print_ruleppfrule)ppfrulesinfprintfppf" ]@]"letprint_levelsppfelev=Format.pp_print_list~pp_sep:(funppf()->fprintfppf"@,| ")(funppf(Levellev)->letrules=List.map(fun(ExSt)->ExS(TCns(MayRec2,Sself,t)))(flatten_treelev.lsuffix)@flatten_treelev.lprefixinfprintfppf"@[<hov 2>";beginmatchlev.lnamewithSomen->fprintfppf"%a@;<1 2>"print_strn|None->()end;beginmatchlev.assocwithLeftA->fprintfppf"LEFTA"|RightA->fprintfppf"RIGHTA"|NonA->fprintfppf"NONA"end;fprintfppf"@]@;<1 2>";print_levelppfpp_force_newlinerules)ppfelevletprint_entryppfe=fprintfppf"@[<v 0>[ ";beginmatche.edescwithDlevelselev->print_levelsppfelev|Dparser_->fprintfppf"<parser>"end;fprintfppf" ]@]"letname_of_symbol:typestra.sty_entry->(s,tr,a)ty_symbol->string=funentry->functionSnterme->"["^e.ename^"]"|Snterml(e,l)->"["^e.ename^" level "^l^"]"|Sself->"["^entry.ename^"]"|Snext->"["^entry.ename^"]"|Stokentok->L.tok_texttok|Stokenstokl->String.concat" "(List.map(functionTPatterntok->L.tok_texttok)tokl)|Slist0_->assertfalse|Slist1sep_->assertfalse|Slist1_->assertfalse|Slist0sep_->assertfalse|Sopt_->assertfalse|Stree_->assertfalsetype('r,'f)tok_list=|TokNil:('f,'f)tok_list|TokCns:'apattern*('r,'f)tok_list->('a->'r,'f)tok_listtype('s,'f)tok_tree=TokTree:'apattern*('s,_,'a->'r)ty_tree*('r,'f)tok_list->('s,'f)tok_treeletrecget_token_list:typestrarf.sty_entry->apattern->(r,f)tok_list->(s,tr,a->r)ty_tree->(s,f)tok_treeoption=funentrylast_tokrev_tokltree->matchtreewithNode(_,{node=Stokentok;son=son;brother=DeadEnd})->get_token_listentrytok(TokCns(last_tok,rev_tokl))son|_->matchrev_toklwith|TokNil->None|_->Some(TokTree(last_tok,tree,rev_tokl))letrecname_of_symbol_failed:typestra.sty_entry->(s,tr,a)ty_symbol->_=funentry->function|Slist0s->name_of_symbol_failedentrys|Slist0sep(s,_,_)->name_of_symbol_failedentrys|Slist1s->name_of_symbol_failedentrys|Slist1sep(s,_,_)->name_of_symbol_failedentrys|Sopts->name_of_symbol_failedentrys|Street->name_of_tree_failedentryt|s->name_of_symbolentrysandname_of_tree_failed:typestra.sty_entry->(s,tr,a)ty_tree->_=funentry->functionNode(_,{node=s;brother=bro;son=son})->lettokl=matchswithStokentok->get_token_listentrytokTokNilson|_->NoneinbeginmatchtoklwithNone->lettxt=name_of_symbol_failedentrysinlettxt=matchs,sonwithSopt_,Node_->txt^" or "^name_of_tree_failedentryson|_->txtinlettxt=matchbrowithDeadEnd->txt|LocAct(_,_)->txt|Node_->txt^" or "^name_of_tree_failedentrybrointxt|Some(TokTree(last_tok,_,rev_tokl))->letrecbuild_str:typeab.string->(a,b)tok_list->string=funs->function|TokNil->s|TokCns(tok,t)->build_str(L.tok_texttok^" "^s)tinbuild_str(L.tok_textlast_tok)rev_toklend|DeadEnd->"???"|LocAct(_,_)->"action"lettree_failed(typestra)(entry:sty_entry)(prev_symb_result:a)(prev_symb:(s,tr,a)ty_symbol)tree=lettxt=name_of_tree_failedentrytreeinlettxt=matchprev_symbwithSlist0s->lettxt1=name_of_symbol_failedentrysintxt1^" or "^txt^" expected"|Slist1s->lettxt1=name_of_symbol_failedentrysintxt1^" or "^txt^" expected"|Slist0sep(s,sep,_)->beginmatchprev_symb_resultwith[]->lettxt1=name_of_symbol_failedentrysintxt1^" or "^txt^" expected"|_->lettxt1=name_of_symbol_failedentrysepintxt1^" or "^txt^" expected"end|Slist1sep(s,sep,_)->beginmatchprev_symb_resultwith[]->lettxt1=name_of_symbol_failedentrysintxt1^" or "^txt^" expected"|_->lettxt1=name_of_symbol_failedentrysepintxt1^" or "^txt^" expected"end|Sopt_->txt^" expected"|Stree_->txt^" expected"|_->txt^" expected after "^name_of_symbol_failedentryprev_symbintxt^" (in ["^entry.ename^"])"letsymb_failedentryprev_symb_resultprev_symbsymb=lettree=Node(MayRec3,{node=symb;brother=DeadEnd;son=DeadEnd})intree_failedentryprev_symb_resultprev_symbtreeletlevel_numberentrylab=letreclookuplevn=function[]->failwith("unknown level "^lab)|lev::levs->ifis_level_labelledlablevthenlevnelselookup(succlevn)levsinmatchentry.edescwithDlevelselev->lookup0elev|Dparser_->raiseNot_foundletrectop_symb:typestra.sty_entry->(s,tr,a)ty_symbol->(s,norec,a)ty_symbol=funentry->functionSself->Sntermentry|Snext->Sntermentry|Snterml(e,_)->Snterme|Slist1sep(s,sep,b)->Slist1sep(top_symbentrys,sep,b)|_->raiseStream.Failureletentry_of_symb:typestra.sty_entry->(s,tr,a)ty_symbol->aty_entry=funentry->functionSself->entry|Snext->entry|Snterme->e|Snterml(e,_)->e|_->raiseStream.Failurelettop_tree:typestra.sty_entry->(s,tr,a)ty_tree->(s,tr,a)ty_tree=funentry->functionNode(MayRec3,{node=s;brother=bro;son=son})->Node(MayRec3,{node=top_symbentrys;brother=bro;son=son})|Node(NoRec3,{node=s;brother=bro;son=son})->Node(NoRec3,{node=top_symbentrys;brother=bro;son=son})|LocAct(_,_)->raiseStream.Failure|DeadEnd->raiseStream.Failureletskip_if_emptybppstrm=ifLStream.countstrm==bpthenfuna->pstrmelseraiseStream.Failureletcontinueentrybpasymbsonp1(strm__:_LStream.t)=leta=(entry_of_symbentrysymb).econtinue0bpastrm__inletact=tryp1strm__withStream.Failure->raise(Stream.Error(tree_failedentryasymbson))infun_->acta(** Recover from a success on [symb] with result [a] followed by a
failure on [son] in a rule of the form [a = symb; son] *)letdo_recoverparser_of_treeentrynlevnalevnbpasymbson(strm__:_LStream.t)=try(* Try to replay the son with the top occurrence of NEXT (by
default at level nlevn) and trailing SELF (by default at alevn)
replaced with self at top level;
This allows for instance to recover from a failure on the
second SELF of « SELF; "\/"; SELF » by doing as if it were
« SELF; "\/"; same-entry-at-top-level » with application e.g. to
accept "A \/ forall x, x = x" w/o requiring the expected
parentheses as in "A \/ (forall x, x = x)". *)parser_of_treeentrynlevnalevn(top_treeentryson)strm__withStream.Failure->try(* Discard the rule if what has been consumed before failing is
the empty sequence (due to some OPT or LIST0); example:
« OPT "!"; ident » fails to see an ident and the OPT was resolved
into the empty sequence, with application e.g. to being able to
safely write « LIST1 [ OPT "!"; id = ident -> id] ». *)skip_if_emptybp(fun(strm__:_LStream.t)->raiseStream.Failure)strm__withStream.Failure->(* In case of success on just SELF, NEXT or an explicit call to
a subentry followed by a failure on the rest (son), retry
parsing as if this entry had been called at its toplevel;
example: « "{"; entry-at-some-level; "}" » fails on "}" and
is retried with « "{"; same-entry-at-top-level; "}" », allowing
e.g. to parse « {1 + 1} » while « {(1 + 1)} » would
have been expected according to the level. *)continueentrybpasymbson(parser_of_treeentrynlevnalevnson)strm__letrecoverparser_of_treeentrynlevnalevnbpasymbsonstrm=do_recoverparser_of_treeentrynlevnalevnbpasymbsonstrmletitem_skipped=reffalseletcall_and_pushpsalstrm=item_skipped:=false;leta=psstrminletal=if!item_skippedthenalelsea::alinitem_skipped:=false;allettoken_ematchtok=lettematch=L.tok_matchtokinfuntok->tematchtok(**
nlevn: level for Snext
alevn: level for recursive calls on the left-hand side of the rule (depending on associativity)
*)letrecparser_of_tree:typestrr.sty_entry->int->int->(s,tr,r)ty_tree->rparser_t=funentrynlevnalevn->functionDeadEnd->(fun(strm__:_LStream.t)->raiseStream.Failure)|LocAct(act,_)->(fun(strm__:_LStream.t)->act)|Node(_,{node=Sself;son=LocAct(act,_);brother=DeadEnd})->(* SELF on the right-hand side of the last rule *)(fun(strm__:_LStream.t)->leta=entry.estartalevnstrm__inacta)|Node(_,{node=Sself;son=LocAct(act,_);brother=bro})->(* SELF on the right-hand side of a rule *)letp2=parser_of_treeentrynlevnalevnbroin(fun(strm__:_LStream.t)->matchtrySome(entry.estartalevnstrm__)withStream.Failure->NonewithSomea->acta|_->p2strm__)|Node(_,{node=Stokentok;son=son;brother=DeadEnd})->parser_of_token_listentrynlevnalevntokson|Node(_,{node=Stokentok;son=son;brother=bro})->letp2=parser_of_treeentrynlevnalevnbroinletp1=parser_of_token_listentrynlevnalevntoksonin(fun(strm__:_LStream.t)->tryp1strm__withStream.Failure->p2strm__)|Node(_,{node=s;son=son;brother=DeadEnd})->letps=parser_of_symbolentrynlevnsinletp1=parser_of_treeentrynlevnalevnsoninletp1=parser_contp1entrynlevnalevnssonin(fun(strm__:_LStream.t)->letbp=LStream.countstrm__inleta=psstrm__inletact=tryp1bpastrm__withStream.Failure->raise(Stream.Error(tree_failedentryasson))inacta)|Node(_,{node=s;son=son;brother=bro})->letps=parser_of_symbolentrynlevnsinletp1=parser_of_treeentrynlevnalevnsoninletp1=parser_contp1entrynlevnalevnssoninletp2=parser_of_treeentrynlevnalevnbroin(fun(strm:_LStream.t)->letbp=LStream.countstrminmatchtrySome(psstrm)withStream.Failure->NonewithSomea->beginmatch(trySome(p1bpastrm)withStream.Failure->None)withSomeact->acta|None->raise(Stream.Error(tree_failedentryasson))end|None->p2strm)andparser_cont:typestrtr'ar.(a->r)parser_t->sty_entry->int->int->(s,tr,a)ty_symbol->(s,tr',a->r)ty_tree->int->a->(a->r)parser_t=funp1entrynlevnalevnssonbpa(strm__:_LStream.t)->tryp1strm__withStream.Failure->recoverparser_of_treeentrynlevnalevnbpassonstrm__(** [parser_of_token_list] attempts to look-ahead an arbitrary-long
finite sequence of tokens. E.g., in
[ [ "foo"; "bar1"; "bar3"; ... -> action1
| "foo"; "bar2"; ... -> action2
| other-rules ] ]
compiled as:
[ [ "foo"; ["bar1"; "bar3"; ... -> action1
|"bar2"; ... -> action2]
| other-rules ] ]
this is able to look ahead "foo"; "bar1"; "bar3" and if not found
"foo"; "bar1", then, if still not found, "foo"; "bar2" _without_
consuming the tokens until it is sure that a longest chain of tokens
(before finding non-terminals or the end of the production) is found
(and backtracking to [other-rules] if no such longest chain can be
found). *)andparser_of_token_list:typestrltr.sty_entry->int->int->ltpattern->(s,tr,lt->r)ty_tree->rparser_t=funentrynlevnalevntoktree->letrecloop:typetrltr.int->ltpattern->(s,tr,r)ty_tree->lt->rparser_t=funnlast_toktree->matchtreewith|Node(_,{node=Stokentok;son=son;brother=bro})->lettematch=token_ematchtokinletp2=loopnlast_tokbroinletp1=loop(n+1)toksoninfunlast_astrm->(match(trySome(tematch(LStream.peek_nthnstrm))withStream.Failure->None)with|Somea->(matchtrySome(p1astrm)withStream.Failure->Nonewith|Someact->acta|None->p2last_astrm)|None->p2last_astrm)|DeadEnd->funlast_astrm->raiseStream.Failure|_->letps=parser_of_treeentrynlevnalevntreeinfunlast_astrm->for_i=1tondoLStream.junkstrmdone;matchtrySome(psstrm)withStream.Failure->(* Tolerance: retry w/o granting the level constraint (see recover) *)trySome(parser_of_treeentrynlevnalevn(top_treeentrytree)strm)withStream.Failure->Nonewith|Someact->act|None->raise(Stream.Error(tree_failedentrylast_a(Stokenlast_tok)tree))inletps=loop1toktreeinlettematch=token_ematchtokinfunstrm->matchLStream.peekstrmwith|Sometok->leta=tematchtokinletact=psastrminacta|None->raiseStream.Failureandparser_of_symbol:typestra.sty_entry->int->(s,tr,a)ty_symbol->aparser_t=funentrynlevn->function|Slist0s->letps=call_and_push(parser_of_symbolentrynlevns)inletrecloopal(strm__:_LStream.t)=matchtrySome(psalstrm__)withStream.Failure->NonewithSomeal->loopalstrm__|_->alin(fun(strm__:_LStream.t)->leta=loop[]strm__inList.reva)|Slist0sep(symb,sep,false)->letps=call_and_push(parser_of_symbolentrynlevnsymb)inletpt=parser_of_symbolentrynlevnsepinletreckontal(strm__:_LStream.t)=matchtrySome(ptstrm__)withStream.Failure->NonewithSomev->letal=trypsalstrm__withStream.Failure->raise(Stream.Error(symb_failedentryvsepsymb))inkontalstrm__|_->alin(fun(strm__:_LStream.t)->matchtrySome(ps[]strm__)withStream.Failure->NonewithSomeal->leta=kontalstrm__inList.reva|_->[])|Slist0sep(symb,sep,true)->letps=call_and_push(parser_of_symbolentrynlevnsymb)inletpt=parser_of_symbolentrynlevnsepinletreckontal(strm__:_LStream.t)=matchtrySome(ptstrm__)withStream.Failure->NonewithSomev->beginmatch(trySome(psalstrm__)withStream.Failure->None)withSomeal->kontalstrm__|_->alend|_->alin(fun(strm__:_LStream.t)->matchtrySome(ps[]strm__)withStream.Failure->NonewithSomeal->leta=kontalstrm__inList.reva|_->[])|Slist1s->letps=call_and_push(parser_of_symbolentrynlevns)inletrecloopal(strm__:_LStream.t)=matchtrySome(psalstrm__)withStream.Failure->NonewithSomeal->loopalstrm__|_->alin(fun(strm__:_LStream.t)->letal=ps[]strm__inleta=loopalstrm__inList.reva)|Slist1sep(symb,sep,false)->letps=call_and_push(parser_of_symbolentrynlevnsymb)inletpt=parser_of_symbolentrynlevnsepinletreckontal(strm__:_LStream.t)=matchtrySome(ptstrm__)withStream.Failure->NonewithSomev->letal=trypsalstrm__withStream.Failure->leta=tryparse_top_symbentrysymbstrm__withStream.Failure->raise(Stream.Error(symb_failedentryvsepsymb))ina::alinkontalstrm__|_->alin(fun(strm__:_LStream.t)->letal=ps[]strm__inleta=kontalstrm__inList.reva)|Slist1sep(symb,sep,true)->letps=call_and_push(parser_of_symbolentrynlevnsymb)inletpt=parser_of_symbolentrynlevnsepinletreckontal(strm__:_LStream.t)=matchtrySome(ptstrm__)withStream.Failure->NonewithSomev->beginmatch(trySome(psalstrm__)withStream.Failure->None)withSomeal->kontalstrm__|_->matchtrySome(parse_top_symbentrysymbstrm__)withStream.Failure->NonewithSomea->kont(a::al)strm__|_->alend|_->alin(fun(strm__:_LStream.t)->letal=ps[]strm__inleta=kontalstrm__inList.reva)|Sopts->letps=parser_of_symbolentrynlevnsin(fun(strm__:_LStream.t)->matchtrySome(psstrm__)withStream.Failure->NonewithSomea->Somea|_->None)|Street->letpt=parser_of_treeentry10tin(fun(strm__:_LStream.t)->letbp=LStream.countstrm__inleta=ptstrm__inletep=LStream.countstrm__inletloc=LStream.interval_locbpepstrm__inaloc)|Snterme->(fun(strm__:_LStream.t)->e.estart0strm__)|Snterml(e,l)->(fun(strm__:_LStream.t)->e.estart(level_numberel)strm__)|Sself->(fun(strm__:_LStream.t)->entry.estart0strm__)|Snext->(fun(strm__:_LStream.t)->entry.estartnlevnstrm__)|Stokentok->parser_of_tokenentrytok|Stokenstokl->parser_of_tokensentrytoklandparser_of_token:typesa.sty_entry->apattern->aparser_t=funentrytok->letf=L.tok_matchtokinfunstrm->matchLStream.peekstrmwithSometok->letr=ftokinLStream.junkstrm;r|None->raiseStream.Failureandparser_of_tokens:types.sty_entry->ty_patternlist->unitparser_t=funentrytokl->letrecloopn=function|[]->funstrm->for_i=1tondoLStream.junkstrmdone;()|TPatterntok::tokl->lettematch=token_ematchtokinfunstrm->ignore(tematch(LStream.peek_nthnstrm));loop(n+1)toklstrminloop0toklandparse_top_symb:typestra.sty_entry->(s,tr,a)ty_symbol->aparser_t=funentrysymb->parser_of_symbolentry0(top_symbentrysymb)(** [start_parser_of_levels entry clevn levels levn strm] goes
top-down from level [clevn] to the last level, ignoring rules
between [levn] and [clevn], as if starting from
[max(clevn,levn)]. On each rule of the form [prefix] (where
[prefix] is a rule not starting with [SELF]), it tries to consume
the stream [strm].
The interesting case is [entry.estart] which is
[start_parser_of_levels entry 0 entry.edesc], thus practically
going from [levn] to the end.
More schematically, assuming each level has the form
level n: [ a = SELF; b = suffix_tree_n -> action_n(a,b)
| a = prefix_tree_n -> action'_n(a) ]
then the main loop does the following:
estart n =
if prefix_tree_n matches the stream as a then econtinue n (action'_n(a))
else start (n+1)
econtinue n a =
if suffix_tree_n matches the stream as b then econtinue n (action_n(a,b))
else if n=0 then a else econtinue (n-1) a
*)letrecstart_parser_of_levelsentryclevn=function[]->(funlevn(strm__:_LStream.t)->raiseStream.Failure)|Levellev::levs->letp1=start_parser_of_levelsentry(succclevn)levsinmatchlev.lprefixwithDeadEnd->p1|tree->letalevn=matchlev.assocwithLeftA|NonA->succclevn|RightA->clevninletp2=parser_of_treeentry(succclevn)alevntreeinmatchlevswith[]->(funlevnstrm->(* this code should be there but is commented to preserve
compatibility with previous versions... with this code,
the grammar entry e: [[ "x"; a = e | "y" ]] should fail
because it should be: e: [RIGHTA[ "x"; a = e | "y" ]]...
if levn > clevn then match strm with parser []
else
*)let(strm__:_LStream.t)=strminletbp=LStream.countstrm__inletact=p2strm__inletep=LStream.countstrm__inleta=act(LStream.interval_locbpepstrm__)inentry.econtinuelevnbpastrm)|_->funlevnstrm->iflevn>clevnthen(* Skip rules before [levn] *)p1levnstrmelselet(strm__:_LStream.t)=strminletbp=LStream.countstrm__inmatchtrySome(p2strm__)withStream.Failure->NonewithSomeact->letep=LStream.countstrm__inleta=act(LStream.interval_locbpepstrm__)inentry.econtinuelevnbpastrm|_->p1levnstrm__(** [continue_parser_of_levels entry clevn levels levn bp a strm] goes
bottom-up from the last level to level [clevn], ignoring rules
between [levn] and [clevn], as if stopping at [max(clevn,levn)].
It tries to consume the stream [strm] on the suffix of rules of
the form [SELF; suffix] knowing that [a] is what consumed [SELF]
at level [levn] (or [levn+1] depending on associativity).
The interesting case is [entry.econtinue levn bp a] which is [try
continue_parser_of_levels entry 0 entry.edesc levn bp a with
Failure -> a], thus practically going from the end to [levn].
*)letreccontinue_parser_of_levelsentryclevn=function[]->(funlevnbpa(strm__:_LStream.t)->raiseStream.Failure)|Levellev::levs->letp1=continue_parser_of_levelsentry(succclevn)levsinmatchlev.lsuffixwithDeadEnd->p1|tree->letalevn=matchlev.assocwithLeftA|NonA->succclevn|RightA->clevninletp2=parser_of_treeentry(succclevn)alevntreeinfunlevnbpastrm->iflevn>clevnthen(* Skip rules before [levn] *)p1levnbpastrmelselet(strm__:_LStream.t)=strmintryp1levnbpastrm__withStream.Failure->letact=p2strm__inletep=LStream.countstrm__inleta=acta(LStream.interval_locbpepstrm__)inentry.econtinuelevnbpastrmletcontinue_parser_of_entryentry=matchentry.edescwithDlevelselev->letp=continue_parser_of_levelsentry0elevin(funlevnbpa(strm__:_LStream.t)->tryplevnbpastrm__withStream.Failure->a)|Dparserp->funlevnbpa(strm__:_LStream.t)->raiseStream.Failureletempty_entryenamelevnstrm=raise(Stream.Error("entry ["^ename^"] is empty"))letstart_parser_of_entryentry=matchentry.edescwithDlevels[]->empty_entryentry.ename|Dlevelselev->start_parser_of_levelsentry0elev|Dparserp->funlevnstrm->pstrm(* Extend syntax *)letinit_entry_functionsentry=entry.estart<-(funlevstrm->letf=start_parser_of_entryentryinentry.estart<-f;flevstrm);entry.econtinue<-(funlevbpastrm->letf=continue_parser_of_entryentryinentry.econtinue<-f;flevbpastrm)letextend_entryentrystatement=letelev=levels_of_rulesentrystatementinentry.edesc<-Dlevelselev;init_entry_functionsentry(* Deleting a rule *)letdelete_ruleentrysl=matchentry.edescwithDlevelslevs->letlevs=delete_rule_in_level_listentrysllevsinentry.edesc<-Dlevelslevs;entry.estart<-(funlevstrm->letf=start_parser_of_entryentryinentry.estart<-f;flevstrm);entry.econtinue<-(funlevbpastrm->letf=continue_parser_of_entryentryinentry.econtinue<-f;flevbpastrm)|Dparser_->()(* Normal interface *)moduleParsable=structtypet={pa_tok_strm:L.teLStream.t;lexer_state:L.State.tref}letparse_parsableentryp=letefun=entry.estart0inletts=p.pa_tok_strminletget_parsing_loc()=(* Build the loc spanning from just after what is consumed (count)
up to the further token known to have been read (max_peek).
Being a parsing error, there needs to be a next token that
caused the failure, except when the rule is empty (e.g. an
empty custom entry); thus, we need to ensure that the token
at location cnt has been peeked (which in turn ensures that
the max peek is at least the current position) *)let_=LStream.peektsinletloc'=LStream.max_peek_loctsinletloc=LStream.get_loc(LStream.countts)tsinLoc.mergelocloc'intryefuntswith|Stream.Failureasexn->letexn,info=Exninfo.captureexninletloc=get_parsing_loc()inletinfo=Loc.add_locinfolocinletexn=Stream.Error("illegal begin of "^entry.ename)inExninfo.iraise(exn,info)|Stream.Error_asexn->letexn,info=Exninfo.captureexninletloc=get_parsing_loc()inletinfo=Loc.add_locinfolocinExninfo.iraise(exn,info)|exc->(* An error produced by the evaluation of the right-hand side *)(* of a rule, or a signal such as Sys.Break; we leave to the *)(* error the responsibility of locating itself *)letexc,info=Exninfo.captureexcinExninfo.iraise(exc,info)letparse_parsableep=L.State.set!(p.lexer_state);tryletc=parse_parsableepinp.lexer_state:=L.State.get();cwithexn->letexn,info=Exninfo.captureexninL.State.drop();Exninfo.iraise(exn,info)letmake?loc?fix_loccs=letlexer_state=ref(L.State.init())inL.State.set!lexer_state;letts=L.tok_func?loc?fix_loccsinlexer_state:=L.State.get();{pa_tok_strm=ts;lexer_state}letcommentsp=L.State.get_comments!(p.lexer_state)letloct=LStream.current_loct.pa_tok_strmletconsume{pa_tok_strm}len=LStream.njunklenpa_tok_strmendmoduleEntry=structtype'at='aty_entryletmaken={ename=n;estart=empty_entryn;econtinue=(fun___(strm__:_LStream.t)->raiseStream.Failure);edesc=Dlevels[]}letcreate=makeletparse(e:'at)p:'a=Parsable.parse_parsableepletparse_token_stream(e:'at)ts:'a=e.estart0tsletnamee=e.enametype'aparser_fun={parser_fun:teLStream.t->'a}letof_parsern{parser_fun=(p:teLStream.t->'a)}:'at={ename=n;estart=(fun_->p);econtinue=(fun___(strm__:_LStream.t)->raiseStream.Failure);edesc=Dparserp}letprintppfe=fprintfppf"%a@."print_entryeletis_emptye=matche.edescwith|Dparser_->failwith"Arbitrary parser entry"|Dlevelselev->List.is_emptyelevtypeany_t=Any:'at->any_tletreciter_infe=matche.edescwith|Dparser_->()|Dlevelselev->List.iter(fun(Levellev)->letrules=List.map(fun(ExSt)->ExS(TCns(MayRec2,Sself,t)))(flatten_treelev.lsuffix)@flatten_treelev.lprefixinList.iter(fun(ExSrule)->iter_in_symbolsfrule)rules)elevanditer_in_symbols:typestrp._->(s,tr,p)ty_symbols->unit=funfsymbols->matchsymbolswith|TNil->()|TCns(_,symbol,symbols)->iter_in_symbolfsymbol;iter_in_symbolsfsymbolsanditer_in_symbol:typestrr._->(s,tr,r)ty_symbol->unit=funf->function|Snterml(e,_)|Snterme->f(Anye)|Slist0s->iter_in_symbolfs|Slist0sep(s,t,_)->iter_in_symbolfs;iter_in_symbolft|Slist1s->iter_in_symbolfs|Slist1sep(s,t,_)->iter_in_symbolfs;iter_in_symbolft|Sopts->iter_in_symbolfs|Stoken_|Stokens_->()|Sself|Snext->()|Street->List.iter(fun(ExSrule)->iter_in_symbolsfrule)(flatten_treet)letsame_entry(Anye)(Anye')=(Obj.magice)==(Obj.magice')letaccumulate_ine=letinitial=Anyeinlettodo=ref[initial]inletvisited=ref(String.Map.singleton(namee)[initial])inwhilenot(List.is_empty!todo)doletAnye=List.hd!todointodo:=List.tl!todo;iter_in(fun(Anyeasany)->letvisited'=String.Map.updatee.ename(function|None->Some[any]|Somevlasv->letany=anyinifList.mem_fsame_entryanyvlthenvelseSome(any::vl))!visitedinifnot(!visited==visited')thenbeginvisited:=visited';todo:=any::!todoend)edone;!visitedendmodulerecSymbol:sigtype('self,'trec,'a)t=('self,'trec,'a)ty_symbolvalnterm:'aEntry.t->('self,norec,'a)tvalnterml:'aEntry.t->string->('self,norec,'a)tvallist0:('self,'trec,'a)t->('self,'trec,'alist)tvallist0sep:('self,'trec,'a)t->('self,norec,unit)t->bool->('self,'trec,'alist)tvallist1:('self,'trec,'a)t->('self,'trec,'alist)tvallist1sep:('self,'trec,'a)t->('self,norec,unit)t->bool->('self,'trec,'alist)tvalopt:('self,'trec,'a)t->('self,'trec,'aoption)tvalself:('self,mayrec,'self)tvalnext:('self,mayrec,'self)tvaltoken:'cpattern->('self,norec,'c)tvaltokens:ty_patternlist->('self,norec,unit)tvalrules:'aRules.tlist->('self,norec,'a)tend=structtype('self,'trec,'a)t=('self,'trec,'a)ty_symbolletnterme=Sntermeletntermlel=Snterml(e,l)letlist0s=Slist0sletlist0sepssepb=Slist0sep(s,sep,b)letlist1s=Slist1sletlist1sepssepb=Slist1sep(s,sep,b)letopts=Soptsletself=Sselfletnext=Snextlettokentok=Stokentoklettokenstokl=Stokenstoklletrules(t:'aRules.tlist)=srulestendandRule:sigtype('self,'trec,'f,'r)t=('self,'trec,'f,'r)ty_rulevalstop:('self,norec,'r,'r)tvalnext:('self,_,'a,'r)t->('self,_,'b)Symbol.t->('self,mayrec,'b->'a,'r)tvalnext_norec:('self,norec,'a,'r)Rule.t->('self,norec,'b)Symbol.t->('self,norec,'b->'a,'r)tend=structtype('self,'trec,'f,'r)t=('self,'trec,'f,'r)ty_ruleletstop=TStopletnextrs=TNext(MayRec2,r,s)letnext_norecrs=TNext(NoRec2,r,s)endandRules:sigtype'at='aty_rulesvalmake:(_,norec,'f,Loc.t->'a)Rule.t->'f->'atend=structtype'at='aty_rulesletmakepact=TRules(p,act)endmoduleProduction=structtype'at='aty_productionletmakepact=TProd(p,act)endmoduleUnsafe=structletclear_entrye=e.estart<-(fun_(strm__:_LStream.t)->raiseStream.Failure);e.econtinue<-(fun___(strm__:_LStream.t)->raiseStream.Failure);matche.edescwithDlevels_->e.edesc<-Dlevels[]|Dparser_->()endletsafe_extend(e:'aEntry.t)data=extend_entryedataletsafe_delete_rulee(TProd(r,_act))=letAnyS(symbols,_)=get_symbolsrindelete_ruleesymbolsletlevel_of_nontermsym=matchsymwith|Snterml(_,l)->Somel|_->NoneexceptionSelfSymbolletrecgeneralize_symbol:typeatrs.(s,tr,a)Symbol.t->(s,norec,a)ty_symbol=function|Stokentok->Stokentok|Stokenstokl->Stokenstokl|Slist1e->Slist1(generalize_symbole)|Slist1sep(e,sep,b)->lete=generalize_symboleinletsep=generalize_symbolsepinSlist1sep(e,sep,b)|Slist0e->Slist0(generalize_symbole)|Slist0sep(e,sep,b)->lete=generalize_symboleinletsep=generalize_symbolsepinSlist0sep(e,sep,b)|Sopte->Sopt(generalize_symbole)|Sself->raiseSelfSymbol|Snext->raiseSelfSymbol|Snterme->Snterme|Snterml(e,l)->Snterml(e,l)|Streer->Stree(generalize_treer)andgeneralize_tree:typeatrs.(s,tr,a)ty_tree->(s,norec,a)ty_tree=funr->matchrwith|Node(fi,n)->letfi=matchfiwith|NoRec3->NoRec3|MayRec3->raiseSelfSymbolinletn=matchnwith|{node;son;brother}->letnode=generalize_symbolnodeinletson=generalize_treesoninletbrother=generalize_treebrotherin{node;son;brother}inNode(fi,n)|LocAct_asr->r|DeadEndasr->rletgeneralize_symbols=trySome(generalize_symbols)withSelfSymbol->Noneend