diff options
author | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-09 15:58:32 +0000 |
---|---|---|
committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-02-09 15:58:32 +0000 |
commit | c580f69cc36cc4cc908febb900a55ae751039a0c (patch) | |
tree | 17a176851279624a58a2a75ca1dea071ec78bcca /lib/util.mli | |
parent | 6160f53e89800a785d773c4130b08fbe7c345651 (diff) |
memoized is_ground_env
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11893 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/util.mli')
-rw-r--r-- | lib/util.mli | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/lib/util.mli b/lib/util.mli index 023b8a15e..1be7f807a 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -298,6 +298,21 @@ val pr_located : ('a -> std_ppcmds) -> 'a located -> std_ppcmds val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds val surround : std_ppcmds -> std_ppcmds +(*s Memoization. *) + +(* General comments on memoization: + - cache is created whenever the function is supplied (because of + ML's polymorphic value restriction). + - cache is never flushed (unless the memoized fun is GC'd) + *) +(* One cell memory: memorizes only the last call *) +val memo1_1 : ('a -> 'b) -> ('a -> 'b) +val memo1_2 : ('a -> 'b -> 'c) -> ('a -> 'b -> 'c) +(* with custom equality (used to deal with various arities) *) +val memo1_eq : ('a -> 'a -> bool) -> ('a -> 'b) -> ('a -> 'b) + +(* Memorizes the last [n] distinct calls. Efficient only for small [n]. *) +val memon_eq : ('a -> 'a -> bool) -> int -> ('a -> 'b) -> ('a -> 'b) (*s Size of an ocaml value (in words, bytes and kilobytes). *) |