/usr/share/hol88-2.02.19940316/Library/arith/streams.ml is in hol88-library-source 2.02.19940316-31.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 | %****************************************************************************%
% FILE : streams.ml %
% DESCRIPTION : Datatype and functions for streams (lazy lists). %
% %
% READS FILES : <none> %
% WRITES FILES : <none> %
% %
% AUTHOR : R.J.Boulton %
% DATE : 20th April 1991 %
% %
% LAST MODIFIED : R.J.Boulton %
% DATE : 22nd April 1991 %
%****************************************************************************%
%----------------------------------------------------------------------------%
% Datatype for lazy lists %
%----------------------------------------------------------------------------%
rectype * stream = Stream of * # (void -> * stream);;
%----------------------------------------------------------------------------%
% stream_map : (* -> **) -> (void -> * stream) -> (void -> ** stream) %
%----------------------------------------------------------------------------%
letrec stream_map f s () =
case s ()
of (Stream (x,s')) . (Stream (f x,stream_map f s'));;
%----------------------------------------------------------------------------%
% stream_append : (void -> * stream) -> %
% (void -> * stream) -> %
% (void -> * stream) %
%----------------------------------------------------------------------------%
letrec stream_append s1 s2 () =
(case s1 ()
of (Stream (x,s1')) . (Stream (x,stream_append s1' s2)))
? s2 ();;
%----------------------------------------------------------------------------%
% stream_flat : (void -> (void -> * stream) stream) -> void -> * stream %
%----------------------------------------------------------------------------%
letrec stream_flat ss () =
case ss ()
of (Stream (s,ss')) . (stream_append s (stream_flat ss') ());;
%----------------------------------------------------------------------------%
% permutations : * list -> void -> * list stream %
%----------------------------------------------------------------------------%
letrec permutations l () =
letrec remove_el n l =
if ((null l) or (n < 1))
then failwith `remove_el`
else if (n = 1)
then (hd l,tl l)
else let (x,l') = remove_el (n - 1) (tl l)
in (x,(hd l).l')
in
let one_smaller_subsets l =
letrec one_smaller_subsets' l n () =
if (null l)
then fail
else Stream (remove_el n l,one_smaller_subsets' l (n + 1))
in one_smaller_subsets' l 1
in
if (null l) then fail
if (null (tl l)) then Stream ([hd l],\(). fail)
else let oss = one_smaller_subsets l
in let subperms = stream_map (I # permutations) oss
in stream_flat
(stream_map (\(x,sofl). stream_map (\l. x.l) sofl) subperms) ();;
|