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