src/HOL/TPTP/TPTP_Parser/ml-yacc/lib/stream.sml
author wenzelm
Wed, 04 Oct 2017 12:00:53 +0200
changeset 66787 64b47495676d
parent 46845 6431a93ffeb6
permissions -rw-r--r--
obsolete;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
46845
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     1
(* ML-Yacc Parser Generator (c) 1989 Andrew W. Appel, David R. Tarditi *)
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     2
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     3
(* Stream: a structure implementing a lazy stream.  The signature STREAM
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     4
   is found in base.sig *)
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     5
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     6
structure Stream :> STREAM =
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     7
struct
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     8
   datatype 'a str = EVAL of 'a * 'a str ref | UNEVAL of (unit->'a)
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
     9
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    10
   type 'a stream = 'a str ref
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    11
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    12
   fun get(ref(EVAL t)) = t
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    13
     | get(s as ref(UNEVAL f)) = 
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    14
	    let val t = (f(), ref(UNEVAL f)) in s := EVAL t; t end
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    15
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    16
   fun streamify f = ref(UNEVAL f)
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    17
   fun cons(a,s) = ref(EVAL(a,s))
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    18
6431a93ffeb6 added ml-yacc library sources;
sultana
parents:
diff changeset
    19
end;