src/Tools/Metis/src/Lazy.sig
author wenzelm
Sat, 07 Apr 2012 16:41:59 +0200
changeset 47389 e8552cba702d
parent 39502 cffceed8e7fa
child 72004 913162a47d9f
permissions -rw-r--r--
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     1
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     2
(* SUPPORT FOR LAZY EVALUATION                                               *)
39502
cffceed8e7fa fix license
blanchet
parents: 39501
diff changeset
     3
(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License            *)
39348
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     4
(* ========================================================================= *)
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     5
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     6
signature Lazy =
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     7
sig
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     8
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
     9
type 'a lazy
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    10
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    11
val quickly : 'a -> 'a lazy
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    12
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    13
val delay : (unit -> 'a) -> 'a lazy
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    14
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    15
val force : 'a lazy -> 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    16
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    17
val memoize : (unit -> 'a) -> unit -> 'a
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    18
6f9c9899f99f new version of the Metis files
blanchet
parents:
diff changeset
    19
end