(* Author: Pascal Stoop, ETH Zurich
Author: Andreas Lochbihler, Digital Asset *)
signature LAZY = sig type'a lazy; val lazy : (unit -> 'a) -> 'a lazy; val force : 'a lazy -> 'a; val peek : 'a lazy -> 'a option val termify_lazy :
(string -> 'typerep -> 'term) ->
('term -> 'term -> 'term) ->
(string -> 'typerep -> 'term -> 'term) -> 'typerep -> ('typerep -> 'typerep -> 'typerep) -> ('typerep -> 'typerep) ->
('a -> 'term) -> 'typerep -> 'a lazy -> 'term -> 'term; end;
structure Lazy : LAZY = struct
datatype'a content =
Delay of unit -> 'a
| Value of'a
| Exn of exn;
datatype'a lazy = Lazy of 'a content ref;
fun lazy f = Lazy (ref (Delay f));
fun force (Lazy x) = case !x of
Delay f => ( letval res = f (); val _ = x := Value res; in res end handle exn => (x := Exn exn; raise exn))
| Value x => x
| Exn exn => raise exn;
fun peek (Lazy x) = case !x of
Value x => SOME x
| _ => NONE;
fun termify_lazy constapp abs unitT funT lazyT term_of T x _ = app (const"Code_Lazy.delay" (funT (funT unitT T) (lazyT T)))
(case peek x of SOME y => abs "_" unitT (term_of y)
| _ => const"Pure.dummy_pattern" (funT unitT T));
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
