Last active
May 20, 2021 21:44
-
-
Save hwayne/c1be058273f9e549666a0cdfe38fd482 to your computer and use it in GitHub Desktop.
TLA+ Type Introspection for safe operations!
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This works because of undocumented behavior in TLC: | |
`Sequences` operators have overrides that also works on strings. | |
So you take the Head of a string to get the first character. | |
Please don't use this in an actual spec, it's for demonstration purposes only. | |
Also, this is likely to get patched out soon. See (https://github.com/tlaplus/tlaplus/issues/512) | |
ALSO also it breaks on lots of stuff, like it says `TypeOf(1..3) = "int"` | |
TypeOf(TLCEval(1..3)) works properly but I'd rather not make this more useable | |
---- MODULE Introspection ---- | |
EXTENDS Integers, TLC, Sequences | |
LOCAL Range(f) == {f[x] : x \in DOMAIN f} | |
RECURSIVE ComplexTypeOf(_) | |
TypeOf(x) == | |
LET fc == Head(ToString(x)) | |
IN CASE fc \in {"T", "F"} -> "bool" | |
[] fc = "{" -> "set" | |
[] fc \in {"1","2","3","4","5","6","7","8","9","0"} -> "int" | |
[] fc = "<" -> "seq" | |
[] fc = "\"" -> "str" \*"\* <- fix github's syntax highlighter | |
[] fc \in {"[", "("} -> "fun" \* Could also be a struct, see ComplexTypeOf | |
ComplexTypeOf(x) == | |
LET type == TypeOf(x) \* type == Print(x, TypeOf(x)) | |
IN | |
CASE type \in {"bool", "str", "int"} -> <<type>> | |
[] type = "set" -> | |
IF x = {} THEN <<"set", "empty">> ELSE | |
LET elem == CHOOSE e \in x: TRUE | |
IN <<"set", TypeOf(elem)>> | |
[] type = "seq" -> | |
<<"seq", TypeOf(x[1])>> | |
[] type = "fun" -> | |
LET dom_type == ComplexTypeOf(DOMAIN x)[2] | |
ran_type == ComplexTypeOf(Range(x))[2] | |
\* We know both are sets, so [2] is what it's a set OF | |
\* Todo better introspection, like for structs with heterogenous ranges | |
IN | |
IF dom_type = "str" THEN <<"struct", ran_type>> | |
ELSE <<type, dom_type, ran_type>> | |
SafeEq(a, b) == | |
TypeOf(a) = TypeOf(b) /\ a = b | |
SafeIn(a, set) == | |
LET type == ComplexTypeOf(set) IN | |
/\ type[1] = "set" | |
/\ TypeOf(a) = type[2] | |
/\ a \in set | |
TestTypeOf == << | |
TypeOf(34), | |
TypeOf("34"), | |
TypeOf([BOOLEAN -> BOOLEAN]), | |
TypeOf(1 :> 2 @@ 2 :> 4), | |
TypeOf("abc") | |
>> | |
TestComplexTypeOf == << | |
ComplexTypeOf([BOOLEAN -> BOOLEAN]), | |
ComplexTypeOf({"a", "b", "c"}), | |
ComplexTypeOf([a |-> 1, b |-> 2]), | |
ComplexTypeOf(1 :> 2 @@ 3 :> 4) | |
>> | |
TestSafeEq == << | |
SafeEq(1, 2), SafeEq(1, "a"), SafeEq(2, 2), SafeEq(2, {2}) | |
>> | |
TestSafeIn == << | |
SafeIn(1, 2), SafeIn(1, {1, 2}), SafeIn(1, {"a", "b"}) | |
\* this fails: ,SafeIn({1}, {{"a"}, {"b"}}) | |
>> | |
==== |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment