aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-04-25 14:36:19 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-04-25 14:39:15 +0200
commit38d2881dcd1917a93b202c16a55d57d51006ee88 (patch)
treec3995446d077b16a55367e52af4d45013707b805
parentb35edb34769fecd4dbdf7030222ba3078eab1c93 (diff)
Adding a debug printer for futures.
-rw-r--r--dev/db2
-rw-r--r--dev/top_printers.ml4
-rw-r--r--lib/future.ml14
-rw-r--r--lib/future.mli5
4 files changed, 23 insertions, 2 deletions
diff --git a/dev/db b/dev/db
index 4777a5348..fc63e5111 100644
--- a/dev/db
+++ b/dev/db
@@ -2,6 +2,8 @@ load_printer "gramlib.cma"
load_printer "str.cma"
load_printer "printers.cma"
+install_printer Top_printers.ppfuture
+
install_printer Top_printers.ppid
install_printer Top_printers.ppidset
install_printer Top_printers.ppevar
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 6f2c24176..7d6370b9d 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -31,6 +31,10 @@ let _ = Detyping.set_detype_anonymous (fun _ _ -> raise Not_found)
(* std_ppcmds *)
let pppp x = pp x
+(** Future printer *)
+
+let ppfuture kx = pp (Future.print (fun _ -> str "_") kx)
+
(* name printers *)
let ppid id = pp (pr_id id)
let pplab l = pp (pr_lab l)
diff --git a/lib/future.ml b/lib/future.ml
index 1e878ac32..1f68061ef 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -191,3 +191,17 @@ let map2 ?greedy f x l =
with Failure _ | Invalid_argument _ ->
Errors.anomaly (Pp.str "Future.map2 length mismatch")) in
f xi y) 0 l
+
+let print f kx =
+ let open Pp in
+ let (uid, _, x) = get kx in
+ let uid =
+ if UUID.equal uid UUID.invalid then str "[#]"
+ else str "[" ++ int uid ++ str "]"
+ in
+ match !x with
+ | Delegated _ -> str "Delegated" ++ uid
+ | Closure _ -> str "Closure" ++ uid
+ | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x)
+ | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x)
+ | Exn e -> str "Exn" ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e))
diff --git a/lib/future.mli b/lib/future.mli
index 785b2df53..09d18ff26 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -143,9 +143,10 @@ val purify : ('a -> 'b) -> 'a -> 'b
(* And also let a function alter the state but backtrack if it raises exn *)
val transactify : ('a -> 'b) -> 'a -> 'b
+(** Debug: print a computation given an inner printing function. *)
+val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds
+
(* These functions are needed to get rid of side effects.
Thy are set for the outermos layer of the system, since they have to
deal with the whole system state. *)
val set_freeze : (unit -> Dyn.t) -> (Dyn.t -> unit) -> unit
-
-