[MLton-devel] Re: Twelf benchmark
Stephen Weeks
MLton@mlton.org
Sat, 14 Dec 2002 13:30:02 -0800
> P.S.: It would help if you could send me the diffs, or MLton specific
> files so I do not replicate the work that you already did.
Here's where I currently am. It might be easier for you to just use
mlton-server.cm rather than figure out how to install cmcat, which
requires older versions of SML/NJ.
For int-inf, I commented out your implementation, since MLton,
Poly/ML, and SML/NJ all have it (and with wildly different
performance).
For the signals stuff, MLton has replacements for the SML/NJ stuff,
but conts/threads/signals are not super-well tested in MLton. Please
let us know about problems. Also, MLton's basis library will raise
SysErr with EINTR when a system call like read is interrupted by a
signal, rather than restart the call. So, I needed to patch your
getLine function. MLton's library will hopefully someday
automatically restart the call.
In any case, for the benchmark, I plan to make a single file that
works on all compilers, so I'll cut out the signals stuff anyways.
--------------------------------------------------------------------------------
% diff -N -u -r twelf twelf-new
diff -N -u -r twelf/Makefile twelf-new/Makefile
--- twelf/Makefile Mon Oct 16 07:28:12 2000
+++ twelf-new/Makefile Sat Dec 14 13:16:20 2002
@@ -17,6 +17,33 @@
version = "1.3"
+MLTON=mlton
+NAME=mlton-server
+FLAGS=-v
+
+$(NAME): $(NAME).cm $(shell $(MLTON) -stop f $(NAME).cm)
+ @echo 'Compiling $(NAME)'
+ time $(MLTON) $(FLAGS) $(NAME).cm
+ size $(NAME)
+
+$(NAME).sml: $(NAME).cm $(shell $(MLTON) -stop f $(NAME).cm)
+ mlton -stop sml $(NAME).cm
+
+.PHONY: clean-mlton
+clean-mlton:
+ rm -f $(NAME) $(NAME).sml
+ find . -type d | grep '/CM$$' | xargs rm -rf
+ find . -type f | grep '~$$' | xargs rm -rf
+
+.PHONY: cm
+cm:
+ ( \
+ echo 'Group is' && \
+ echo 'src/mlton-stubs.sml' && \
+ cmcat -DMLton server.cm && \
+ echo 'src/mlton-main.sml'; \
+ ) >$(NAME).cm
+
default : twelf-server twelf-emacs
all : twelf-server twelf-sml twelf-emacs
diff -N -u -r twelf/mlton-server.cm twelf-new/mlton-server.cm
--- twelf/mlton-server.cm Wed Dec 31 16:00:00 1969
+++ twelf-new/mlton-server.cm Thu Dec 12 22:40:19 2002
@@ -0,0 +1,279 @@
+Group is
+src/mlton-stubs.sml
+src/lambda/intsyn.sig
+src/lambda/whnf.sig
+src/names/names.sig
+src/print/traverse.sig
+src/print/traverse.fun
+src/meta/funsyn.sig
+src/meta/interpret.sig
+src/timing/timing.sml
+src/timing/timers.sig
+src/timing/timers.fun
+src/timing/timers.sml
+src/stream/stream.sml
+src/paths/paths.sig
+src/frontend/lexer.sig
+src/frontend/twelf.sig
+src/global/global.sig
+src/global/global.sml
+src/trail/trail.sig
+src/trail/notrail.sml
+src/trail/trail.sml
+src/lambda/intsyn.fun
+src/lambda/whnf.fun
+src/lambda/conv.sig
+src/lambda/conv.fun
+src/lambda/constraints.sig
+src/lambda/constraints.fun
+src/lambda/unify.sig
+src/lambda/unify.fun
+src/lambda/abstract.sig
+src/lambda/abstract.fun
+src/lambda/approx.sig
+src/lambda/approx.fun
+src/lambda/lambda.sml
+src/table/table.sig
+src/table/hash-table.sml
+src/table/string-hash.sig
+src/table/string-hash.sml
+src/table/red-black-tree.fun
+src/table/sparse-array.sig
+src/table/sparse-array.fun
+src/table/sparse-array2.sig
+src/table/sparse-array2.fun
+src/table/table.sml
+src/names/names.fun
+src/names/names.sml
+src/paths/paths.fun
+src/paths/origins.sig
+src/paths/origins.fun
+src/paths/paths.sml
+src/formatter/formatter.sig
+src/formatter/formatter.fun
+src/formatter/formatter.sml
+src/print/print-twega.sig
+src/print/print-twega.fun
+src/print/symbol.sig
+src/print/symbol.fun
+src/print/print.sig
+src/print/print.fun
+src/print/clause-print.sig
+src/print/clause-print.fun
+src/print/print.sml
+src/typecheck/strict.sig
+src/typecheck/strict.fun
+src/typecheck/typecheck.sig
+src/typecheck/typecheck.fun
+src/typecheck/typecheck.sml
+src/table/queue.sig
+src/table/queue.sml
+src/index/index.sig
+src/index/index.fun
+src/index/index-skolem.fun
+src/index/index.sml
+src/modes/modesyn.sig
+src/modes/modesyn.fun
+src/modes/modedec.sig
+src/modes/modedec.fun
+src/modes/modecheck.sig
+src/modes/modecheck.fun
+src/modes/modeprint.sig
+src/modes/modeprint.fun
+src/modes/modes.sml
+src/tabling/tabledsyn.sig
+src/tabling/tabledsyn.fun
+src/tabling/tabled.sml
+src/subordinate/subordinate.sig
+src/subordinate/subordinate.fun
+src/subordinate/subordinate.sml
+src/domains/integers.sig
+src/domains/integers.fun
+src/domains/field.sig
+src/domains/ordered-field.sig
+src/domains/rationals.sig
+src/domains/rationals.fun
+src/domains/integers-mod.fun
+src/domains/domains.sml
+src/solvers/cs-manager.sig
+src/solvers/cs-manager.fun
+src/solvers/cs.sig
+src/solvers/cs-eq-field.sig
+src/solvers/cs-eq-field.fun
+src/solvers/cs-ineq-field.fun
+src/solvers/cs-eq-strings.fun
+src/solvers/cs-eq-bools.fun
+src/solvers/cs-eq-integers.sig
+src/solvers/cs-eq-integers.fun
+src/solvers/cs-ineq-integers.fun
+src/solvers/cs-integers-word.fun
+src/solvers/solvers.sml
+src/order/order.sig
+src/order/order.fun
+src/order/order.sml
+src/terminate/checking.sig
+src/terminate/checking.fun
+src/terminate/reduces.sig
+src/terminate/reduces.fun
+src/terminate/terminate.sml
+src/thm/thmsyn.sig
+src/thm/thmsyn.fun
+src/thm/thmprint.sig
+src/thm/thmprint.fun
+src/thm/thm.sig
+src/thm/thm.fun
+src/thm/thm.sml
+src/compile/compsyn.sig
+src/compile/compsyn.fun
+src/compile/cprint.sig
+src/compile/cprint.fun
+src/compile/compile.sig
+src/compile/compile.fun
+src/compile/assign.sig
+src/compile/assign.fun
+src/compile/compile.sml
+src/opsem/absmachine.sig
+src/opsem/absmachine.fun
+src/opsem/ptrecon.sig
+src/opsem/ptrecon.fun
+src/opsem/abstract.sig
+src/opsem/abstract.fun
+src/opsem/index.sig
+src/opsem/index.fun
+src/opsem/tabled.sig
+src/opsem/tabled.fun
+src/opsem/trace.sig
+src/opsem/trace.fun
+src/opsem/tmachine.fun
+src/opsem/swmachine.fun
+src/opsem/opsem.sml
+src/m2/meta-global.sig
+src/m2/meta-global.sml
+src/table/ring.sig
+src/table/ring.sml
+src/m2/metasyn.sig
+src/m2/metasyn.fun
+src/m2/meta-abstract.sig
+src/m2/meta-abstract.fun
+src/m2/meta-print.sig
+src/m2/meta-print.fun
+src/m2/init.sig
+src/m2/init.fun
+src/m2/search.sig
+src/m2/search.fun
+src/m2/lemma.sig
+src/m2/lemma.fun
+src/m2/splitting.sig
+src/m2/splitting.fun
+src/m2/filling.sig
+src/m2/filling.fun
+src/m2/recursion.sig
+src/m2/recursion.fun
+src/m2/qed.sig
+src/m2/qed.fun
+src/m2/strategy.sig
+src/m2/strategy.fun
+src/m2/prover.sig
+src/m2/prover.fun
+src/m2/mpi.sig
+src/m2/mpi.fun
+src/m2/skolem.sig
+src/m2/skolem.fun
+src/m2/m2.sml
+src/modules/modsyn.sig
+src/modules/modsyn.fun
+src/modules/modules.sml
+src/heuristic/heuristic.sig
+src/heuristic/heuristic.sum.fun
+src/meta/global.sig
+src/meta/statesyn.sig
+src/meta/init.sig
+src/meta/strategy.sig
+src/meta/relfun.sig
+src/meta/prover.fun
+src/meta/funprint.sig
+src/meta/print.sig
+src/meta/print.fun
+src/meta/filling.sig
+src/meta/data.sig
+src/meta/splitting.sig
+src/meta/recursion.sig
+src/meta/inference.sig
+src/meta/strategy.fun
+src/meta/statesyn.fun
+src/meta/funtypecheck.sig
+src/meta/uniquesearch.sig
+src/meta/inference.fun
+src/meta/abstract.sig
+src/meta/splitting.fun
+src/meta/uniquesearch.fun
+src/meta/search.sig
+src/meta/search.fun
+src/meta/recursion.fun
+src/meta/mpi.sig
+src/meta/mpi.fun
+src/meta/data.fun
+src/meta/global.fun
+src/meta/filling.fun
+src/meta/init.fun
+src/meta/abstract.fun
+src/meta/funsyn.fun
+src/meta/funnames.sig
+src/meta/funnames.fun
+src/meta/funprint.fun
+src/meta/weaken.sig
+src/meta/weaken.fun
+src/meta/funweaken.sig
+src/meta/funweaken.fun
+src/meta/funtypecheck.fun
+src/meta/relfun.fun
+src/meta/meta.sml
+src/worldcheck/worldsyn.sig
+src/worldcheck/worldsyn.fun
+src/worldcheck/worldprint.sig
+src/worldcheck/worldprint.fun
+src/worldcheck/worldcheck.sml
+src/cover/cover.sig
+src/cover/cover.fun
+src/cover/total.sig
+src/cover/total.fun
+src/cover/cover.sml
+src/frontend/lexer.fun
+src/frontend/parsing.sig
+src/frontend/parsing.fun
+src/frontend/recon-term.sig
+src/frontend/recon-term.fun
+src/frontend/recon-condec.sig
+src/frontend/recon-condec.fun
+src/frontend/recon-query.sig
+src/frontend/recon-query.fun
+src/frontend/recon-mode.sig
+src/frontend/recon-mode.fun
+src/frontend/recon-thm.sig
+src/frontend/recon-thm.fun
+src/frontend/recon-module.sig
+src/frontend/recon-module.fun
+src/frontend/parse-term.sig
+src/frontend/parse-term.fun
+src/frontend/parse-condec.sig
+src/frontend/parse-condec.fun
+src/frontend/parse-query.sig
+src/frontend/parse-query.fun
+src/frontend/parse-fixity.sig
+src/frontend/parse-fixity.fun
+src/frontend/parse-mode.sig
+src/frontend/parse-mode.fun
+src/frontend/parse-thm.sig
+src/frontend/parse-thm.fun
+src/frontend/parse-module.sig
+src/frontend/parse-module.fun
+src/frontend/parser.sig
+src/frontend/parser.fun
+src/frontend/solve.sig
+src/frontend/solve.fun
+src/frontend/twelf.fun
+src/frontend/frontend.sml
+src/server/sigint.sig
+src/server/sigint-any.sml
+src/server/server.sml
+src/mlton-main.sml
diff -N -u -r twelf/src/int-inf/sources.cm twelf-new/src/int-inf/sources.cm
--- twelf/src/int-inf/sources.cm Sun Sep 24 08:01:31 2000
+++ twelf-new/src/int-inf/sources.cm Tue Dec 10 17:31:19 2002
@@ -1,3 +1,3 @@
Group is
- int-inf-sig.sml
- int-inf.sml
+(* int-inf-sig.sml *)
+(* int-inf.sml *)
diff -N -u -r twelf/src/mlton-main.sml twelf-new/src/mlton-main.sml
--- twelf/src/mlton-main.sml Wed Dec 31 16:00:00 1969
+++ twelf-new/src/mlton-main.sml Tue Dec 10 17:57:11 2002
@@ -0,0 +1,4 @@
+val _ =
+ OS.Process.exit
+ (Server.server (CommandLine.name (),
+ CommandLine.arguments ()))
diff -N -u -r twelf/src/mlton-stubs.sml twelf-new/src/mlton-stubs.sml
--- twelf/src/mlton-stubs.sml Wed Dec 31 16:00:00 1969
+++ twelf-new/src/mlton-stubs.sml Tue Dec 10 17:53:44 2002
@@ -0,0 +1,12 @@
+structure OS =
+ struct
+ open OS
+
+ structure Path =
+ struct
+ open Path
+
+ fun mkAbsolute (p, d) =
+ Path.mkAbsolute {path = p, relativeTo = d}
+ end
+ end
diff -N -u -r twelf/src/server/server.sml twelf-new/src/server/server.sml
--- twelf/src/server/server.sml Wed Apr 17 23:13:28 2002
+++ twelf-new/src/server/server.sml Tue Dec 10 18:15:17 2002
@@ -20,7 +20,10 @@
*)
fun readLine () =
let
- val line = TextIO.inputLine (TextIO.stdIn)
+ fun getLine () =
+ TextIO.inputLine (TextIO.stdIn)
+ handle OS.SysErr (_, SOME _) => getLine ()
+ val line = getLine ()
fun triml ss = Substring.dropl Char.isSpace ss
fun trimr ss = Substring.dropr Char.isSpace ss
val line' = triml (trimr (Substring.all line))
diff -N -u -r twelf/src/server/sigint-any.sml twelf-new/src/server/sigint-any.sml
--- twelf/src/server/sigint-any.sml Wed Dec 31 16:00:00 1969
+++ twelf-new/src/server/sigint-any.sml Thu Dec 12 22:39:53 2002
@@ -0,0 +1,6 @@
+structure SigINT:> SIGINT =
+struct
+
+fun interruptLoop (loop:unit -> unit) = loop ()
+
+end
diff -N -u -r twelf/src/server/sigint-mlton.sml twelf-new/src/server/sigint-mlton.sml
--- twelf/src/server/sigint-mlton.sml Wed Dec 31 16:00:00 1969
+++ twelf-new/src/server/sigint-mlton.sml Sat Dec 14 13:17:20 2002
@@ -0,0 +1,17 @@
+structure SigINT :> SIGINT =
+struct
+
+ fun interruptLoop (loop:unit -> unit) =
+ let
+ open MLton
+ val _ =
+ Cont.callcc
+ (fn k =>
+ Signal.handleWith'
+ (Signal.int, fn _ =>
+ Thread.new (fn () => Cont.throw (k, ()))))
+ in
+ loop ()
+ end
+
+end; (* structure SigINT *)
diff -N -u -r twelf/src/server/sources.cm twelf-new/src/server/sources.cm
--- twelf/src/server/sources.cm Sat Sep 5 15:59:40 1998
+++ twelf-new/src/server/sources.cm Fri Dec 13 18:03:19 2002
@@ -1,5 +1,10 @@
Group is
../frontend/sources.cm
sigint.sig
+ sigint-any.sml
+ #if (defined (MLton))
+ sigint-mlton.sml
+ #else
sigint-smlnj.sml
+ #endif
server.sml
diff -N -u -r twelf/src/solvers/solvers.sml twelf-new/src/solvers/solvers.sml
--- twelf/src/solvers/solvers.sml Wed Feb 13 16:03:46 2002
+++ twelf-new/src/solvers/solvers.sml Tue Dec 10 17:32:32 2002
@@ -51,6 +51,7 @@
structure Unify = UnifyTrail
structure CSManager = CSManager);
+val _ = (
CSManager.installSolver (CSEqQ.solver);
CSManager.installSolver (CSIneqQ.solver);
CSManager.installSolver (CSEqStrings.solver);
@@ -58,3 +59,5 @@
CSManager.installSolver (CSEqZ.solver);
CSManager.installSolver (CSIneqZ.solver);
CSManager.installSolver (CSIntWord32.solver);
+()
+)
-------------------------------------------------------
This sf.net email is sponsored by:
With Great Power, Comes Great Responsibility
Learn to use your power at OSDN's High Performance Computing Channel
http://hpc.devchannel.org/
_______________________________________________
MLton-devel mailing list
MLton-devel@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/mlton-devel