123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149150151152153154155156157158159160161162163164165166167168169170171172173174175176177178179180181182183184185186187188189190191192193194195196197198199200201202203204205206207208209210211212213214215216217218219220221222223224225226227228229230231232233234235236237238239240241242243244245246247248249250251252253254255256257258259260261262263264265266267268269270271272273274275276277278279280281282283284285286287288289290291292293294295296297298299300301302303304305306307308309310311312313314315316317318319320321322323324325326327328329330331332333334335336337338339340341342343344345346347348349350351352353354355356357358359360361362363364365366367368369370371372373374375376377378379380381382383384385386387388389390391392393394395396397398399400401402403404405406407408409410411412413414415416417418419420421422423424425426427428429430431432433434435436437438439440441442443444445446447448449450451452453454455456457458459460461462463464465466467468469470471472473474475476477478479480481482483484485486487488489490491492493494495496497498499500501502503504505506507508509510511512513514515516517518519520521522523524525526527528529530531532533534535536537538539540541542543544545546547548549550551552553554555556557558559560561562563564565566567568569570571572573574575(**************************************************************************)(* *)(* OCaml *)(* *)(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)(* *)(* Copyright 1996 Institut National de Recherche en Informatique et *)(* en Automatique. *)(* *)(* All rights reserved. This file is distributed under the terms of *)(* the GNU Lesser General Public License version 2.1, with the *)(* special exception on linking described in the file LICENSE. *)(* *)(**************************************************************************)openLocal_storeletlowest_scope=0lethighest_scope=100_000_000(* assumed to fit in 27 bits, see Types.scope_field *)(* A stamp of 0 denotes a persistent identifier *)letcurrentstamp=s_ref0letpredefstamp=s_ref0moduleUnscoped=structtypedesc={name:string;stamp:int}typestate=|Udescofdesc|Ulinkoftandt={mutablestate:state}letcreates=incrcurrentstamp;{state=Udesc{name=s;stamp=!currentstamp}}letrecget_descus=matchus.statewithUdescd->d|Ulinku->get_desculetnameus=(get_descus).nameletrefreshus=create(get_descus).nameletequalus1us2=(get_descus1).name=(get_descus2).nameletstampus=(get_descus).stampletsameus1us2=stampus1=stampus2typechange=t*stateletchange_log=ref(fun_->assertfalse)letundo_change(us,us_d)=us.state<-us_dletrecreprus=matchus.statewith|Ulinkus'->reprus'|Udesc_->usletlinkus1us2=letus1=reprus1inletus2=reprus2inifus1==us2then()elsebegin!change_log(us1,us1.state);us1.state<-Ulinkus2endletequivid_pairsus1us2=(*
The list [id_pairs] does not have a cannonical order of pairs
so we need to check if (us1, us2) or (us2, us1) occurs in the list.
The reason why we do not have a cannonical representation is because
unification identifiers are mutable, they can change once put inside the
list.
*)lets1=stampus1inlets2=stampus2ins1=s2||List.exists(fun(i1,i2)->(stampi1=s1&&stampi2=s2)||stampi2=s1&&stampi1=s2)id_pairsmoduleOps=structtypenonrect=tletcompareus1us2=stampus1-stampus2endmoduleSet=Stdlib.Set.Make(Ops)endtypet=|Localof{name:string;stamp:int}|Scopedof{name:string;stamp:int;scope:int}|Globalofstring|Predefof{name:string;stamp:int}(* the stamp is here only for fast comparison, but the name of
predefined identifiers is always unique. *)|UnscopedofUnscoped.tletcreate_scoped~scopes=incrcurrentstamp;Scoped{name=s;stamp=!currentstamp;scope}letcreate_locals=incrcurrentstamp;Local{name=s;stamp=!currentstamp}letof_unscopedu=Unscopeduletfind_unscoped=functionUnscopedu->Someu|_->Noneletcreate_predefs=incrpredefstamp;Predef{name=s;stamp=!predefstamp}letcreate_persistents=Globalsletname=function|Local{name;_}|Scoped{name;_}|Globalname|Predef{name;_}->name|Unscopedus->Unscoped.nameusletrename=function|Local{name;stamp=_}|Scoped{name;stamp=_;scope=_}->incrcurrentstamp;Local{name;stamp=!currentstamp}|Unscopedus->Unscoped(Unscoped.refreshus)|id->Misc.fatal_errorf"Ident.rename %s"(nameid)letunique_name=function|Local{name;stamp}|Scoped{name;stamp}->name^"_"^Int.to_stringstamp|Unscopedus->letUnscoped.{name;stamp}=Unscoped.get_descusinname^"_"^Int.to_stringstamp|Globalname->(* we're adding a fake stamp, because someone could have named his unit
[Foo_123] and since we're using unique_name to produce symbol names,
we might clash with an ident [Local { "Foo"; 123 }]. *)name^"_0"|Predef{name;_}->(* we know that none of the predef names (currently) finishes in
"_<some number>", and that their name is unique. *)nameletunique_toplevel_name=function|Local{name;stamp}|Scoped{name;stamp}->name^"/"^Int.to_stringstamp|Unscopedus->letUnscoped.{name;stamp}=Unscoped.get_descusinname^"/"^Int.to_stringstamp|Globalname|Predef{name;_}->nameletpersistent=function|Global_->true|_->falseletequali1i2=matchi1,i2with|Local{name=name1;_},Local{name=name2;_}|Scoped{name=name1;_},Scoped{name=name2;_}|Globalname1,Globalname2->name1=name2|Unscopedus1,Unscopedus2->Unscoped.equalus1us2|Predef{stamp=s1;_},Predef{stamp=s2}->(* if they don't have the same stamp, they don't have the same name *)s1=s2|_->falseletsamei1i2=matchi1,i2with|Local{stamp=s1;_},Local{stamp=s2;_}|Scoped{stamp=s1;_},Scoped{stamp=s2;_}|Predef{stamp=s1;_},Predef{stamp=s2}->s1=s2|Unscopedus1,Unscopedus2->Unscoped.sameus1us2|Globalname1,Globalname2->name1=name2|_->falseletstamp=function|Local{stamp;_}|Scoped{stamp;_}->stamp|Unscopedus->Unscoped.stampus|_->0letequivid_pairsi1i2=matchi1,i2with|Local{stamp=s1;_},Local{stamp=s2;_}|Scoped{stamp=s1;_},Scoped{stamp=s2;_}|Predef{stamp=s1;_},Predef{stamp=s2}->s1=s2|Unscopedus1,Unscopedus2->Unscoped.equivid_pairsus1us2|Globalname1,Globalname2->name1=name2|_->falseletcompare_stampid1id2=compare(stampid1)(stampid2)letscope=function|Scoped{scope;_}->scope|Local_->highest_scope|Global_|Predef_->lowest_scope|Unscoped_->lowest_scopeletreinit_level=ref(-1)letreinit()=if!reinit_level<0thenreinit_level:=!currentstampelsecurrentstamp:=!reinit_levelletglobal=function|Local_|Unscoped_|Scoped_->false|Global_|Predef_->trueletis_predef=function|Predef_->true|_->falseletis_unscoped=function|Unscoped_->true|_->falseletcanonical_stamps=s_tableHashtbl.create0letnext_canonical_stamp=s_tableHashtbl.create0letcanonicalizenamestamp=tryHashtbl.find!canonical_stamps(name,stamp)withNot_found->letcanonical_stamp=tryHashtbl.find!next_canonical_stampnamewithNot_found->0inHashtbl.replace!next_canonical_stampname(canonical_stamp+1);Hashtbl.add!canonical_stamps(name,stamp)canonical_stamp;canonical_stampletpp_stampedppf(name,stamp)=letopenFormat_docinifnot!Clflags.unique_idsthenfprintfppf"%s"nameelsebeginletstamp=ifnot!Clflags.canonical_idsthenstampelsecanonicalizenamestampinfprintfppf"%s/%i"namestampendletprint~with_scopeppf=letopenFormat_docinfunction|Globalname->fprintfppf"%s!"name|Predef{name;stamp}->fprintfppf"%a!"pp_stamped(name,stamp)|Local{name;stamp}->fprintfppf"%a"pp_stamped(name,stamp)|Unscopedus->letUnscoped.{name;stamp}=Unscoped.get_descusinfprintfppf"U%a"pp_stamped(name,stamp)|Scoped{name;stamp;scope}->fprintfppf"%a%s"pp_stamped(name,stamp)(ifwith_scopethenasprintf"[%i]"scopeelse"")letprint_with_scopeppfid=print~with_scope:trueppfidletdoc_printppfid=print~with_scope:falseppfidletprintppfid=Format_doc.compatdoc_printppfid(* For the documentation of ['a Ident.tbl], see ident.mli.
The implementation is a copy-paste specialization of
a balanced-tree implementation similar to Map.
['a tbl]
is a slightly more compact version of
[(Ident.t * 'a) list Map.Make(String)]
This implementation comes from Caml Light where duplication was
unavoidable in absence of functors. It works well enough, and so
far we have not had strong incentives to do the deduplication work
(implementation, tests, benchmarks, etc.).
*)type'atbl=Empty|Nodeof'atbl*'adata*'atbl*intand'adata={ident:t;name:string;stamp:int;data:'a;previous:'adataoption}letempty=Empty(* Inline expansion of height for better speed
* let height = function
* Empty -> 0
* | Node(_,_,_,h) -> h
*)(* Before returning the data we check that the corresponding binder
was not mutated since it has been added to the environment
(for example : Unscoped indentifiers and Unscoped.link).
*)letget_datak=assert(stampk.ident=k.stamp);k.dataletmknodeldr=lethl=matchlwithEmpty->0|Node(_,_,_,h)->handhr=matchrwithEmpty->0|Node(_,_,_,h)->hinNode(l,d,r,(ifhl>=hrthenhl+1elsehr+1))letbalanceldr=lethl=matchlwithEmpty->0|Node(_,_,_,h)->handhr=matchrwithEmpty->0|Node(_,_,_,h)->hinifhl>hr+1thenmatchlwith|Node(ll,ld,lr,_)when(matchllwithEmpty->0|Node(_,_,_,h)->h)>=(matchlrwithEmpty->0|Node(_,_,_,h)->h)->mknodellld(mknodelrdr)|Node(ll,ld,Node(lrl,lrd,lrr,_),_)->mknode(mknodellldlrl)lrd(mknodelrrdr)|_->assertfalseelseifhr>hl+1thenmatchrwith|Node(rl,rd,rr,_)when(matchrrwithEmpty->0|Node(_,_,_,h)->h)>=(matchrlwithEmpty->0|Node(_,_,_,h)->h)->mknode(mknodeldrl)rdrr|Node(Node(rll,rld,rlr,_),rd,rr,_)->mknode(mknodeldrll)rld(mknoderlrrdrr)|_->assertfalseelsemknodeldrletrecaddiddata=functionEmpty->letk={ident=id;name=nameid;stamp=stampid;data=data;previous=None}inNode(Empty,k,Empty,1)|Node(l,k,r,h)->letc=String.compare(nameid)k.nameinifc=0thenletnew_k={ident=id;name=nameid;stamp=stampid;data=data;previous=Somek}inNode(l,new_k,r,h)elseifc<0thenbalance(addiddatal)krelsebalancelk(addiddatar)letrecmin_binding=functionEmpty->raiseNot_found|Node(Empty,d,_,_)->d|Node(l,_,_,_)->min_bindinglletrecremove_min_binding=functionEmpty->invalid_arg"Map.remove_min_elt"|Node(Empty,_,r,_)->r|Node(l,d,r,_)->balance(remove_min_bindingl)drletmerget1t2=match(t1,t2)with(Empty,t)->t|(t,Empty)->t|(_,_)->letd=min_bindingt2inbalancet1d(remove_min_bindingt2)letrecremoveid=functionEmpty->Empty|(Node(l,k,r,h)asm)->letc=String.compare(nameid)k.nameinifc=0thenmatchk.previouswith|None->mergelr|Somek->Node(l,k,r,h)elseifc<0thenletll=removeidlinifl==llthenmelsebalancellkrelseletrr=removeidrinifr==rrthenmelsebalancelkrrletrecfind_previousid=functionNone->raiseNot_found|Somek->ifsameidk.identthenget_datakelsefind_previousidk.previousletrecfind_sameid=functionEmpty->raiseNot_found|Node(l,k,r,_)->letc=String.compare(nameid)k.nameinifc=0thenifsameidk.identthenget_datakelsefind_previousidk.previouselsefind_sameid(ifc<0thenlelser)letrecfind_namen=functionEmpty->raiseNot_found|Node(l,k,r,_)->letc=String.comparenk.nameinifc=0thenk.ident,get_datakelsefind_namen(ifc<0thenlelser)letrecget_all=function|None->[]|Somek->(k.ident,get_datak)::get_allk.previousletrecfind_alln=functionEmpty->[]|Node(l,k,r,_)->letc=String.comparenk.nameinifc=0then(k.ident,get_datak)::get_allk.previouselsefind_alln(ifc<0thenlelser)letget_all_seqk()=Seq.unfold(Option.map(funk->(k.ident,get_datak),k.previous))k()letrecfind_all_seqntbl()=matchtblwith|Empty->Seq.Nil|Node(l,k,r,_)->letc=String.comparenk.nameinifc=0thenSeq.Cons((k.ident,get_datak),get_all_seqk.previous)elsefind_all_seqn(ifc<0thenlelser)()letrecfold_auxfstackaccu=functionEmpty->beginmatchstackwith[]->accu|a::l->fold_auxflaccuaend|Node(l,k,r,_)->fold_auxf(l::stack)(fkaccu)rletfold_nameftblaccu=fold_aux(funk->fk.ident(get_datak))[]accutblletrecfold_datafdaccu=matchdwithNone->accu|Somek->fk.ident(get_datak)(fold_datafk.previousaccu)letfold_allftblaccu=fold_aux(funk->fold_dataf(Somek))[]accutbl(* let keys tbl = fold_name (fun k _ accu -> k::accu) tbl [] *)letreciterf=functionEmpty->()|Node(l,k,r,_)->iterfl;fk.ident(get_datak);iterfr(* Idents for sharing keys *)(* They should be 'totally fresh' -> neg numbers *)letkey_name=""letmake_key_generator()=letc=ref1infunction|Local_|Scoped_->letstamp=!cindecrc;Local{name=key_name;stamp=stamp}|global_id->Misc.fatal_errorf"Ident.make_key_generator () %s"(nameglobal_id)letcomparexy=matchx,ywith|Localx,Localy->letc=x.stamp-y.stampinifc<>0thencelsecomparex.namey.name|Local_,_->1|_,Local_->(-1)|Scopedx,Scopedy->letc=x.stamp-y.stampinifc<>0thencelsecomparex.namey.name|Scoped_,_->1|_,Scoped_->(-1)|Globalx,Globaly->comparexy|Global_,_->1|_,Global_->(-1)|Predef{stamp=s1;_},Predef{stamp=s2;_}->compares1s2|Predef_,_->1|_,Predef_->(-1)|Unscopedx,Unscopedy->letx=Unscoped.get_descxinlety=Unscoped.get_descyinletc=x.stamp-y.stampinifc<>0thencelsecomparex.namey.nameletoutputocid=output_stringoc(unique_nameid)lethashi=(Char.code(namei).[0])lxor(stampi)letoriginal_equal=equalincludeIdentifiable.Make(structtypenonrect=tletcompare=compareletoutput=outputletprint=printlethash=hashletequal=sameend)letequal=original_equalletrename_no_exn=function|Local{name;stamp=_}|Scoped{name;stamp=_;scope=_}->incrcurrentstamp;Local{name;stamp=!currentstamp}|id->idletget_currentstamp()=!currentstamp