Twelf state can get corrupted by twelf bugs

[jcreedcmu]

Since the WebAssembly.Memory is preserved between clicks of the "check" button, if the input twelf code elicits an sml exception because twelf has a genuine bug, and leaves twelf's internal data structures in a bad state, then there's no way to "reboot" the twelf wasm state except by reloading the page. Probably should detect that an exception has been raised somehow, and preemptively start from a the slate.

Steps to Reproduce:

1. Try to check this code

term : type.

true : term.
false : term.
if : term -> term -> term -> term.
zero : term.

ty : type.

bool : ty.
int : ty.


%% relations
is_value : term -> type.

is_value/true : is_value true.
is_value/false : is_value false.
is_value/zero : is_value zero.

eval : term -> term -> type.

eval/if_true : eval (if true X _) X.
eval/if_false : eval (if false _ X) X.
eval/if : eval (if E E1 E2) (if E' E1 E2)
    <- eval E E'.

not_stuck : term -> type.

not_stuck/value : not_stuck X <- is_value X.
not_stuck/eval : not_stuck X <- eval X X'.

of : term -> ty -> type.

of/true : of true bool.
of/false : of false bool.
of/zero : of zero int.
of/if : of X bool -> of Y T -> of Z T -> of (if X Y Z) T.

%% theorems

progress : (of X T) -> (not_stuck X) -> type.
%mode progress +D1 -D2.
%prove 2 T (progress T _).

2. Observe RuntimeError: index out of bounds in developer console (or I thought just once I had observed a Match raised, but I haven't been able to reproduce it)
3. Then try to check simply a:type. in the same tab.
4. Observe, contrary to expectations, RuntimeError: index out of bounds again. Clearly state has gotten corrupted somehow.

[jcreedcmu]

I note that step 1 takes a good few seconds and spins up my fan sometimes, and unpredictably, I need to repeat steps 1 and 3 a couple times before a:type. reliably fails.

[agoode]

The RuntimeError is a bug in MLton, fixed in the latest push to the PR.

MLton/mlton#550

[jcreedcmu]

I think this is fixed by @agoode's latest wasm2 branch and the current timeout behavior, which starts a fresh wasm instance on timeout.