src/Pure/sequence.ML
author nipkow
Fri Mar 14 10:35:30 1997 +0100 (1997-03-14)
changeset 2792 6c17c5ec3d8b
parent 1501 bb7f99a0a6f0
permissions -rw-r--r--
Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.
     1 (*  Title: 	sequence
     2     ID:         $Id$
     3     Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1988  University of Cambridge
     5 
     6 Unbounded sequences implemented by closures.
     7 
     8 RECOMPUTES if sequence is re-inspected.
     9 
    10 Memoing, using polymorphic refs, was found to be slower!  (More GCs)
    11 *)
    12 
    13 
    14 signature SEQUENCE = 
    15   sig
    16   type 'a seq
    17   val append	: 'a seq * 'a seq -> 'a seq
    18   val chop	: int * 'a seq -> 'a list * 'a seq
    19   val cons	: 'a * 'a seq -> 'a seq
    20   val filters	: ('a -> bool) -> 'a seq -> 'a seq
    21   val flats	: 'a seq seq -> 'a seq
    22   val hd	: 'a seq -> 'a
    23   val interleave: 'a seq * 'a seq -> 'a seq
    24   val its_right	: ('a * 'b seq -> 'b seq) -> 'a seq * 'b seq -> 'b seq
    25   val list_of_s	: 'a seq -> 'a list
    26   val mapp	: ('a -> 'b) -> 'a seq -> 'b seq -> 'b seq
    27   val maps	: ('a -> 'b) -> 'a seq -> 'b seq
    28   val null	: 'a seq
    29   val prints	: (int -> 'a -> unit) -> int -> 'a seq -> unit
    30   val pull	: 'a seq -> ('a * 'a seq) option
    31   val s_of_list	: 'a list -> 'a seq
    32   val seqof	: (unit -> ('a * 'a seq) option) -> 'a seq
    33   val single	: 'a -> 'a seq
    34   val tl	: 'a seq -> 'a seq
    35   end;
    36 
    37 
    38 structure Sequence : SEQUENCE = 
    39 struct
    40     
    41 datatype 'a seq = Seq of unit -> ('a * 'a seq)option;
    42 
    43 (*Return next sequence element as None or Some(x,str) *)
    44 fun pull(Seq f) = f();
    45 
    46 (*Head and tail.  Beware of calling the sequence function twice!!*)
    47 fun hd s = #1 (the (pull s))
    48 and tl s = #2 (the (pull s));
    49 
    50 (*the abstraction for making a sequence*)
    51 val seqof = Seq;
    52 
    53 (*prefix an element to the sequence
    54     use cons(x,s) only if evaluation of s need not be delayed,
    55       otherwise use seqof(fn()=> Some(x,s)) *)
    56 fun cons all = Seq(fn()=>Some all);
    57 
    58 (*the empty sequence*)
    59 val null = Seq(fn()=>None);
    60 
    61 fun single(x) = cons (x, null);
    62 
    63 (*The list of the first n elements, paired with rest of sequence.
    64   If length of list is less than n, then sequence had less than n elements.*)
    65 fun chop (n:int, s: 'a seq): 'a list * 'a seq =
    66   if n<=0 then ([],s)
    67   else case pull(s) of
    68            None => ([],s)
    69          | Some(x,s') => let val (xs,s'') = chop (n-1,s')
    70 		         in  (x::xs, s'')  end;
    71 
    72 (*conversion from sequence to list*)
    73 fun list_of_s (s: 'a seq) : 'a list = case pull(s) of
    74         None => []
    75       | Some(x,s') => x :: list_of_s s';
    76 
    77 
    78 (*conversion from list to sequence*)
    79 fun s_of_list []     = null
    80   | s_of_list (x::l) = cons (x, s_of_list l);
    81 
    82 
    83 (*functional to print a sequence, up to "count" elements
    84   the function prelem should print the element number and also the element*)
    85 fun prints (prelem: int -> 'a -> unit) count (s: 'a seq) : unit =
    86   let fun pr (k,s) = 
    87 	   if k>count then ()
    88 	   else case pull(s) of
    89 	       None => ()
    90 	     | Some(x,s') => (prelem k x;  prs"\n";  pr (k+1, s'))
    91   in  pr(1,s)  end;
    92 
    93 (*Map the function f over the sequence, making a new sequence*)
    94 fun maps f xq = seqof (fn()=> case pull(xq) of
    95         None       => None
    96       | Some(x,yq) => Some(f x,  maps f yq));
    97 
    98 (*Sequence append:  put the elements of xq in front of those of yq*)
    99 fun append (xq,yq)  =
   100   let fun copy xq = seqof (fn()=>
   101 	    case pull xq of  
   102 		 None       => pull yq
   103 	       | Some(x,xq') => Some (x, copy xq'))
   104   in  copy xq end;
   105 
   106 (*Interleave elements of xq with those of yq -- fairer than append*)
   107 fun interleave (xq,yq) = seqof (fn()=>
   108       case pull(xq) of  
   109           None       => pull yq
   110 	| Some(x,xq') => Some (x, interleave(yq, xq')));
   111 
   112 (*map over a sequence xq, append the sequence yq*)
   113 fun mapp f xq yq =
   114   let fun copy s = seqof (fn()=> 
   115             case pull(s) of
   116 	        None       => pull(yq)
   117               | Some(x,xq') => Some(f x, copy xq'))
   118   in  copy xq end;
   119 
   120 (*Flatten a sequence of sequences to a single sequence. *)
   121 fun flats ss = seqof (fn()=> case pull(ss) of
   122         None => None
   123       | Some(s,ss') =>  pull(append(s, flats ss')));
   124 
   125 (*accumulating a function over a sequence;  this is lazy*)
   126 fun its_right (f: 'a * 'b seq -> 'b seq) (s: 'a seq, bstr: 'b seq) : 'b seq =
   127   let fun its s = seqof (fn()=>
   128             case pull(s) of
   129 	        None       => pull bstr
   130 	      | Some(a,s') => pull(f(a, its s')))
   131   in  its s end; 
   132 
   133 fun filters pred xq =
   134   let fun copy s = seqof (fn()=> 
   135             case pull(s) of
   136 	        None       => None
   137               | Some(x,xq') => if pred x then Some(x, copy xq')
   138 			       else pull (copy xq') )
   139   in  copy xq end
   140 
   141 end;