123456789101112131415161718192021222324252627282930313233343536373839404142434445464748495051525354555657585960616263646566676869707172737475767778798081828384858687888990919293949596979899100101102103104105106107108109110111112113114115116117118119120121122123124125126127128129130131132133134135136137138139140141142143144145146147148149(******************************************************************************)(* *)(* Fix *)(* *)(* François Pottier, Inria Paris *)(* *)(* Copyright Inria. All rights reserved. This file is distributed under the *)(* terms of the GNU Library General Public License version 2, with a *)(* special exception on linking, as described in the file LICENSE. *)(* *)(******************************************************************************)openSigs(* [rev_take accu n xs] is [accu @ rev (take n xs)], where [take n xs]
takes the first [n] elements of the list [xs]. The length of [xs] must
be at least [n]. *)letrecrev_takeaccunxs=matchn,xswith|0,_->accu|_,[]->(* The list is too short. This cannot happen. *)assertfalse|_,x::xs->rev_take(x::accu)(n-1)xsmoduleMake(M:MINIMAL_IMPERATIVE_MAPS)=structtypekey=M.keyletaddxytable=M.addxytable;y(* [memoize] could be defined as a special case of [fix] via the declaration
[let memoize f = fix (fun _ x -> f x)]. The following direct definition is
perhaps easier to understand and may give rise to more efficient code. *)type'at='aM.tletvisibly_memoize(f:key->'a):(key->'a)*'at=lettable=M.create()inletfx=tryM.findxtablewithNot_found->addx(fx)tableinf,tableletmemoize(f:key->'a):key->'a=letf,_table=visibly_memoizefinfletfix(ff:(key->'a)->(key->'a)):key->'a=lettable=M.create()inletrecfx=tryM.findxtablewithNot_found->addx(fffx)tableinf(* In the implementation of [defensive_fix], we choose to use two tables.
A permanent table, [table] maps keys to values. Once a pair [x, y] has
been added to this table, it remains present forever: [x] is stable,
and a call to [f x] returns [y] immediately. A transient table, [marked],
is used only while a call is in progress. This table maps keys to integers:
for each key [x], it records the depth of the stack at the time [x] was
pushed onto the stack. Finally, [stack] is a list of the keys currently
under examination (most recent key first), and [depth] is the length of
the list [stack]. Recording integer depths in the table [marked] allows
us to identify the desired cycle, a prefix of the list [stack], without
requiring an equality test on keys. *)exceptionCycleofkeylist*keyletdefensive_fix(ff:(key->'a)->(key->'a)):key->'a=(* Create the permanent table. *)lettable=M.create()in(* Define the main recursive function. *)letrecfstackdepthmarked(x:key):'a=tryM.findxtablewithNot_found->matchM.findxmarkedwith|i->(* [x] is marked, and was pushed onto the stack at a time when the
stack depth was [i]. We have found a cycle. Fail. Cut a prefix
of the reversed stack, which represents the cycle that we have
detected, and reverse it on the fly. *)raise(Cycle(rev_take[](depth-i)stack,x))|exceptionNot_found->(* [x] is not marked. Mark it while we work on it. There is no need
to unmark [x] afterwards; inserting it into [table] indicates
that it has stabilized. There also is no need to catch and
re-raise the exception [Cycle]; we just let it escape. *)M.addxdepthmarked;letstack=x::stackanddepth=depth+1inlety=ff(fstackdepthmarked)xinaddxytableinfunx->(* Create the transient table. *)letmarked=M.create()andstack=[]anddepth=0in(* Answer this query. *)fstackdepthmarkedx(* The combinator [curried] can be used to obtain a curried version of [fix]
or [defensive_fix] in a concrete instance where the type [key] is a
product type. *)(* [curried] could be defined as a toplevel function; it does not depend on
any of the code above. However, it seems convenient to place it here. *)letcurryfxy=f(x,y)letuncurryf(x,y)=fxyletcurried(fix:('a*'b->'c)fix):('a->'b->'c)fix=funff->letfff=uncurry(ff(curryf))incurry(fixff)endmoduleForOrderedType(T:OrderedType)=Make(Glue.PersistentMapsToImperativeMaps(Map.Make(T)))moduleForHashedType(T:HashedType)=Make(Glue.HashTablesAsImperativeMaps(T))moduleForType(T:TYPE)=ForHashedType(Glue.TrivialHashedType(T))moduleChar=ForType(Glue.CHAR)moduleInt=ForType(Glue.INT)moduleString=ForType(Glue.STRING)