src/HOL/Library/Tools/lazy.ML

optional external files as code modules

(* 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 => (
     let val 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 const app 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));

end;