1app load ["Future", "metisLib", "computeLib" , "numLib"];
2open metisLib
3
4val _ = mlibUseful.trace_level := 3
5fun METIS_PROVE thl g =
6  metisLib.METIS_PROVE thl g
7  handle e => (let open PolyML.Exception
8               in
9                 case exceptionLocation e of
10                   NONE => (print "No location\n"; reraise e)
11                 | SOME {file,startLine,...} =>
12                   (print ("Exn at: "^file^":"^Int.toString startLine^
13                           "\n"); reraise e)
14               end)
15(*
16fun METIS_PROVE thl g =
17  Exn.trace General.exnMessage print (fn () => metisLib.METIS_PROVE thl g)
18*)
19
20val EVAL = computeLib.CBV_CONV computeLib.the_compset
21val realtime = Portable.realtime
22
23signature CMAP = sig
24  val cmap : ('a -> 'b) -> 'a list -> 'b list
25end
26structure CMap : CMAP =
27struct
28  open Future
29  fun cmap f l =
30    joins (forks default_params (List.map (fn x => fn () => f x) l))
31end;
32
33val cmap = CMap.cmap
34(*
35fun HOLfact i = EVAL ���FACT ^(numSyntax.mk_numeral (Arbnum.fromInt (i + 30)))���
36*)
37fun hello i = (OS.Process.sleep (Time.fromMilliseconds ((i mod 5) * 100));
38               print ("Hello: " ^ LargeInt.toString i ^ "\n");
39               i);
40
41val args = List.tabulate(15, (fn i => fn () => hello (LargeInt.fromInt i)));
42
43val _ = print "\n\nHellos (roughly 3s, serially)\n"
44val results = realtime Future.joins (Future.forks Future.default_params args);
45fun countl n = List.tabulate(n, fn x => x)
46fun fact (n:IntInf.int) = if n <= 2 then 1 else n * fact (n - 1)
47
48
49(* val _ = print "\nFactorials serially\n"
50
51
52val large_facts = realtime (cmap HOLfact) (countl 40)
53*)
54val _ = print "\nMetis calls serially\n"
55fun f () = METIS_PROVE (map snd (DB.thms "arithmetic")) ���1+1=2���;
56
57val metis_results = realtime (cmap f) [(), ()];
58
59val _ = print "\nNow trying in multi-threaded mode\n";
60val _ = Multithreading.max_threads_update 0;
61val _ = print ("Multithreading number = " ^
62               Int.toString (Multithreading.max_threads()) ^ "\n")
63
64val results = realtime Future.joins (Future.forks Future.default_params args);
65
66(* val _ = print "\nFactorials\n"
67val large_facts' = realtime (cmap HOLfact) (countl 40)
68*)
69
70val metis_results = realtime (cmap f) [(), ()]
71