123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200typeexpectation=|Indentofint|Alignofint|Align_betweenofint*inttypeviolation=expectationletgroup(lst:('a*expectationoption)list):(expectationoption*'alist)list=letrecgrplst=matchlstwith|[]->[]|(a,ea)::lst->matchgrplstwith|[]->[ea,[a]]|(e,elst)::lst->ifea=ethenbegin(e,a::elst)::lstendelsebegin(ea,[a])::(e,elst)::lstendingrplst(* Indentation set of a construct:
It consists of a lower bound, an optional upper bound and an alignment flag.
The upper bound is valid only if the alignment flag is set.
The indentation of a construct is defined as the start position its first
token.
Tokens can appear anywhere starting from the lower bound as long as the
alignment flag is not set. If the alignment flag is set, then a token has to
appear between the lower bound and the optional upper bound.
A token appearing within the allowed indentation set when the alignment flag
is set, restricts the allowed indentation set to exactly the position of the
start of the token and clears the alignment flag. I.e. all subsequent token
belonging to the same parent can appear anywhere starting from the lower
bound of the indentation set.
*)typet={lb:int;(* lower bound of the indentation set *)ub:intoption;(* upper bound of the indentation set *)abs:bool;(* alignment flag; if set, then we are waiting for the
first token which has to be in the indentation set. *)}letexpectation(ind:t):expectationoption=letexpect()=ifind.lb=0thenNoneelseSome(Indentind.lb)inmatchind.ubwith|None->expect()|Someub->ifnotind.absthenexpect()elseifind.lb=ubthenSome(Alignub)elseSome(Align_between(ind.lb,ub))letinitial:t={lb=0;ub=None;abs=false}letcheck_position(pos:int)(ind:t):expectationoption=letcheck_indent()=ifind.lb<=posthenNoneelseSome(Indentind.lb)inmatchind.ubwith|None->check_indent()|Someub->ifnotind.absthencheck_indent()elseifind.lb<=pos&&pos<=ubthenNoneelseifind.lb=ubthenSome(Alignind.lb)elseSome(Align_between(ind.lb,ub))lettoken(pos:int)(ind:t):t=assert(check_positionposind=None);ifnotind.absthen(* Normal case. Token are all wrapped with '>=' i.e. they can appear to
the right of the indentation set of the parent. However, if the token
appears within the indentation set of the parent, then it restricts
the upper bound of the indentation set of the parent. A parent can
by definition never be indented more than all its tokens. *)matchind.ubwith|Someubwhenub<=pos->ind|_->{indwithub=Somepos}else(* First token of an aligned parent. Indentation set consists of exactly
the token position. *){lb=pos;ub=Somepos;abs=false}letalign(ind:t):t={indwithabs=true}letleft_align(ind:t):t={indwithub=Someind.lb;abs=true;}letend_align(ind0:t)(ind:t):t=ifnotind.absthen(* flag is cleared, the aligned sequence is not empty. *)indelse(* the aligned sequence is empty and therefore must not have any effect
*){indwithabs=ind0.abs}letstart_indent(i:int)(ind:t):t=assert(0<=i);ifind.absthen(* No effect on aligned structures which have not yet received a first
token. *)indelse{lb=ind.lb+i;ub=None;abs=false;}letend_indent(i:int)(ind0:t)(ind:t):t=ifind0.absthenindelsematchind.ub,ind0.ubwith|None,_->(* Not yet received any token. *)ind0|Someub,None->(* Received some token, but parent not yet. *)assert(ind0.lb+i<=ub);{ind0withub=ind.ub}|Someub,Someub0->assert(ind0.lb+i<=ub);{ind0withub=Some(minub0(ub-i))}