TLA+ Type Introspection for safe operations!

Introspection.tla

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"}})
>>

====