diff --git a/doc/ops.pl b/doc/ops.pl new file mode 100644 index 0000000..4890d5f --- /dev/null +++ b/doc/ops.pl @@ -0,0 +1,6 @@ +:- op(700, xfy, user:(≤)). +:- op(700, xfy, user:(≥)). +:- op(700, xfy, user:(<:)). +:- op(700, xfy, user:(∈)). +:- op(700, xfy, user:(⋮)). +:- op(700, xfy, user:(⋅)). diff --git a/doc/razbor.pl b/doc/razbor.pl new file mode 100644 index 0000000..d77c594 --- /dev/null +++ b/doc/razbor.pl @@ -0,0 +1,378 @@ +:- use_module(library(pprint)). +:- use_module(library(yall)). + +:- [tox]. + +:- op(1100, xfy, user:(//)). +:- op(990, xfy, user:(→)). +:- op(700, xfy, user:(≠)). + +X ≠ Y :- dif(X, Y). + +L // R :- L *-> true ; R. + +match(X, [V|Cases]) :- + ( V = (Val → Goal), X = Val *-> + call(Goal) + ; X = V *-> + true + ; + match(X, Cases) + ). + +% def path: type. +% def path: list string -> list string -> path. + +% def endinanness: type. +% def big_endian: endinanness. +% def little_endian: endinanness. + +% def rel: type. +% def rexpr: type. + +% def hole: rexpr. +% def sizeof: rexpr. +% def rint: int -> rexpr. +% def ref: path -> rexpr. +% def size: list rel -> rexpr. + +% def (<): rexpr -> rexpr -> rel. +% def (≤): rexpr -> rexpr -> rel. +% def (=): rexpr -> rexpr -> rel. +% def (≥): rexpr -> rexpr -> rel. +% def (>): rexpr -> rexpr -> rel. + +% def value: type. +% def vbool: bool -> value. +% def vint: int -> value. + +% def ty: type. +% def top: ty. +% def bottom: ty. + +% def boolean: ty. +% def integer: ty. + +% def u: int -> endinanness -> ty. +% def s: int -> endinanness -> ty. + +% def arr: ty -> list rel -> ty. +% def str: list rel -> ty. + +% def meet: list ty -> ty. +% def join: list ty -> ty. + +% def ref: path -> ty. + +% def (⋮): ty -> list rel -> ty. +% def (∈): value -> ty -> ty. + +% def prod: list path -> ty. + +% def reduced: ty -> ty. + +% def (<:): path -> ty -> o. +% def ctypeof: path -> ty -> o. + +% def simpl: ty -> ty -> o. +% def subst: ty -> ty -> o. +% def reduce_meet: ty -> ty -> ty -> o. +% def reduce_join: list ty -> list ty -> o. + +as_path(S, path(Mods, Data)) :- + split_string(S, " ", "", [ModsStr, DataStr]) *-> + split_string(ModsStr, ".", "", Mods), + split_string(DataStr, ".", "", Data) + ; + split_string(S, ".", "", Mods), + Data = []. + +ctypeof(P, T) :- + P <: Tx, + subst(Tx, Ty), + simpl(Ty, T). + +print_t(T) :- + WriteOps = [spacing(next_argument)], + print_term(T, [write_options(WriteOps)]). + +print_tox_ctypeof :- + findall(P, P <: _, RawTypes), + maplist(ctypeof_pair, RawTypes, CTypes), + WriteOps = [spacing(next_argument)], + print_term(CTypes, [write_options(WriteOps)]). + +ctypeof_pair(P, P <: T) :- ctypeof(P, T). + +print_ctypeof(PathStr) :- + as_path(PathStr, Path), + ctypeof(Path, T), + WriteOps = [ + right_margin(60), + write_options([ + spacing(next_argument) + ]) + ], + print_term(T, WriteOps). + +is_simple(E) :- + dif(E, prod(_)), + dif(E, join(_)). + +subst_(meet([X|Xs]), meet([Y|Ys])) :- + subst(X, Y), + subst(meet(Xs), meet(Ys)). +subst_(Tx ⋮ P, Ty ⋮ P) :- + subst(Tx, Ty). +subst_(V ∈ Tx, V ∈ Ty) :- + subst(Tx, Ty). +subst_(ref(P), T) :- + ctypeof(P, Tx), + ( is_simple(Tx) *-> + T = (Tx ⋅ [P]) + ; + T = ref(P) + ). +subst(Tx, Ty) :- + subst_(Tx, Ty) // Tx = Ty. + +simpl_(Tx ⋮ P, Ty ⋮ P) :- + simpl(Tx, Ty). +simpl_(V ∈ Tx, V ∈ Ty) :- + simpl(Tx, Ty). +simpl_(meet([]), top). +simpl_(meet([T]), T). +simpl_(meet([X|Xs]), T) :- + reduce_meet(X, meet(Xs), M), + simpl(M, T). +simpl_(join([X|[]]), Y) :- + simpl(X, Y). +simpl_(join([X|Xs]), join(Z)) :- + simpl(X, Y), + simpl(join(Xs), join(Ys)), + reduce_join([Y|Ys], Z). +simpl(Tx, Ty) :- + simpl_(Tx, Ty) // Tx = Ty. + +reduce_join(join([X|Xs]), Y) :- + append(X, Xs, Z), + reduce_join(Z, Y). +reduce_join([X|Ys], [X|Zs]) :- + reduce_join(Ys, Zs). +reduce_join([], []). + +reduce_meet(L, R, M) :- match((L, R, M), [ + (T, T, T), + (top, T, T), + (T, top, T), + (bottom, _, bottom), + (integer, u(S, E), u(S, E)), + (u(S, E), integer, u(S, E)), + + (Tx ⋮ Px, Ty ⋮ Py, T ⋮ P) → ( + reduce_meet(Tx, Ty, T), + append(Px, Py, P) + ), + (Tx ⋮ P, V ∈ Ty, V ∈ (T ⋮ P)) → + reduce_meet(Tx, Ty, T), + (V ∈ Tx, Ty ⋮ P, V ∈ (T ⋮ P)) → + reduce_meet(Tx, Ty, T), + (Tx ⋮ P, Ty, T ⋮ P) → + reduce_meet(Tx, Ty, T), + (Tx, Ty ⋮ P, T ⋮ P) → + reduce_meet(Tx, Ty, T), + (Vx ∈ Tx, Vy ∈ Ty, V ∈ T) → ( + meet_values(Vx, Vy, V), + reduce_meet(Tx, Ty, T) + ), + (Tx, V ∈ Ty, V ∈ T) → + reduce_meet(Tx, Ty, T), + (V ∈ Tx, Ty, V ∈ T) → + reduce_meet(Tx, Ty, T), + + (meet([]), T, T), + (T, meet([]), T), + (meet([X|Xs]), meet(Y), Z) → ( + append(Xs, Y, Ts), + reduce_meet(X, meet(Ts), Z) + ), + (meet([X]), Y, Z) → + reduce_meet(X, Y, Z), + (X, meet([Y]), Z) → + reduce_meet(X, Y, Z), + (meet([X|Xs]), Y, Z) → ( + append(Xs, [Y], Ts), + reduce_meet(X, meet(Ts), Z) + ), + (X, meet([Y|Ys]), Z) → ( + reduce_meet(X, Y, T), + reduce_meet(T, meet(Ys), Z) + ), + + (X, join([Y]), Z) → + reduce_meet(X, Y, Z), + (X, join([Y|Ys]), join([Z|Zs])) → ( + reduce_meet(X, Y, Z), + reduce_meet(X, join(Ys), join(Zs)) + ), + (join([X]), Y, Z) → + reduce_meet(X, Y, Z), + (join([X|Xs]), Y, join([Z|Zs])) → ( + reduce_meet(X, Y, Z), + reduce_meet(join(Xs), Y, join(Zs)) + ), + + (ref(X), Y, reduced(meet([ref(X), Y]))), + (X, ref(Y), reduced(meet([X, ref(Y)]))), + + (prod(X), Y, Z) → fail, + (X, prod(Y), Z) → fail +]) // M = bottom. + +meet_values(V, V, V). + +sizeof(P, S) :- + ctypeof(P, T), + sizeof_type(T, S). + +size_sum(Sx, Sy, S) :- fail. + +size_join(Sx, Sy, S) :- match((Sx, Sy, S), [ + (bottom, Y, Y), + (X, bottom, X), + (join(Xs), join(Ys), join(Zs)) → + append(Xs, Ys, Zs), + (X, join(Ys), join([X|Ys])), + (join(Xs), Y, join([Y|Xs])), + (X, Y, join([X, Y])) +]). + +size_mul(Sx, Sy, S) :- fail. +size_unify(Sx, Sy, S) :- fail. + +exact_size(S, E) :- + member(hole=E, S). + +size_constraint([], []). +size_constraint([P|Ps], [S|Ss]) :- + (P, S) = (sizeof=C, hole=C) *-> + size_constraint(Ps, Ss) + ; + size_constraint(Ps, [S|Ss]). + +sizeof_type(prod(Ts), S) :- + maplist( + [T, S] >> sizeof_type(T, S), + Ts, Ss + ), + foldl( + [Sx, Sy, S] >> size_sum(Sx, Sy, S), + Ss, [], S + ). + +sizeof_type(join(Ts), S) :- + maplist( + [T, S] >> sizeof_type(T, S), + Ts, Ss + ), + foldl( + [Sx, Sy, S] >> size_join(Sx, Sy, S), + Ss, bottom, S + ). + +sizeof_type(T, []) :- + T = top ; T = integer. + +sizeof_type(bottom, bottom). + +sizeof_type(u(S, _), [hole=rint(S)]). +sizeof_type(_ ∈ T, S) :- + sizeof_type(T, S). +sizeof_type(arr(T, N), S) :- + sizeof_type(T, St), + Sn = N, + size_mul(St, Sn, S). +sizeof_type(T ⋅ _, S) :- + sizeof_type(T, S). +sizeof_type(ref(Path), S) :- + sizeof(Path, S). +sizeof_type(T ⋮ P, S) :- + sizeof_type(T, Sx), + size_constraint(P, Sy), + size_unify(Sx, Sy, S). + +is_name(path(_, Data)) :- + last(Data, Name), + \+ atom_number(Name, _). + +has_name(P, N) :- + nameof(P, N), + is_name(N). + +short_nameof(P, S) :- + nameof(P, path(_, D)), + last(D, S). + +constant(V ∈ _, V). + +root_path(path(_, [_])). + +print_mtype(Path) :- + mtype(Path, T), print_t(T) + // ctypeof(Path, T), print_t(T). + +% as_datatype(T, DataType) +mtype(Path, MT) :- + ctypeof(Path, T), + as_mtype(Path, T, MT). + +as_mtype(Path, prod(Prod), struct(Path, Fields)) :- + root_path(Path), + maplist( + ([P, T] >> mtype(P, T)), + Prod, Fields + ). + +as_mtype(Path, join(Join), enum(Path, Fields)) :- + root_path(Path), + maplist( + [R, F] >> ( + ref(P) = R, + short_nameof(P, N), + F = N : P + ), + Join, Fields + ). + +as_mtype(Path, Type, data(Path, F)) :- + root_path(Path), + Type \= prod(_), Type \= join(_), + forget(Type, F). + +as_mtype(Path, Type, ShortName : F) :- + \+ root_path(Path), + Type \= prod(_), Type \= join(_), + nameof(Path, Name), % TODO: use has_name + path(_, D) = Name, + last(D, ShortName), + forget(Type, F). + +forget(T, F) :- match((T, F), [ + (_ ⋅ [Path], Path), + (X ⋮ _, Y) → + forget(X, Y), + (_ ∈ X, Y) → + forget(X, Y), + (arr(Tx, Nx), Y) → + forget_arr(arr(Tx, Nx), Y), + (X, X) +]). + +forget_arr(arr(Tx, Nx), F) :- + forget(Tx, Ty), + % TODO: support ref constants + (exact_size(Nx, rint(Ny)) *-> + F = arr(Ty, Ny) + ; + F = vec(Ty) + ). diff --git a/doc/tox.pl b/doc/tox.pl new file mode 100644 index 0000000..0b8c8c2 --- /dev/null +++ b/doc/tox.pl @@ -0,0 +1,380 @@ +:- [ops]. + +path(["tox"], ["IpAddr"]) <: join([ref(path(["tox"], ["Ipv4Addr"])), ref(path(["tox"], ["Ipv6Addr"]))]). +path(["tox"], ["Ipv4Addr"]) <: prod([path(["tox"], ["Ipv4Addr", "0"]), path(["tox"], ["Ipv4Addr", "1"])]). +path(["tox"], ["Ipv4Addr", "0"]) <: meet([vint(0x02) ∈ integer, u(1, big_endian)]). +path(["tox"], ["Ipv4Addr", "1"]) <: arr(u(1, big_endian), [hole = rint(4)]). +path(["tox"], ["Ipv6Addr"]) <: prod([path(["tox"], ["Ipv6Addr", "0"]), path(["tox"], ["Ipv6Addr", "1"])]). +path(["tox"], ["Ipv6Addr", "0"]) <: meet([vint(0x0a) ∈ integer, u(1, big_endian)]). +path(["tox"], ["Ipv6Addr", "1"]) <: arr(u(1, big_endian), [hole = rint(16)]). +path(["tox"], ["NoSpam"]) <: arr(u(1, big_endian), [hole = rint(4)]). +path(["tox"], ["Nonce"]) <: arr(u(1, big_endian), [hole = rint(24)]). +path(["tox"], ["Packet"]) <: join([ref(path(["tox", "dht"], ["DhtPacket"])), ref(path(["tox", "onion"], ["OnionPacket"]))]). +path(["tox"], ["PublicKey"]) <: arr(u(1, big_endian), [hole = rint(32)]). +path(["tox"], ["Sha512"]) <: arr(u(1, big_endian), [hole = rint(64)]). +path(["tox", "dht"], ["BootstrapInfo"]) <: prod([path(["tox", "dht"], ["BootstrapInfo", "0"]), path(["tox", "dht"], ["BootstrapInfo", "1"]), path(["tox", "dht"], ["BootstrapInfo", "2"])]). +path(["tox", "dht"], ["BootstrapInfo", "0"]) <: meet([vint(0xf0) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["BootstrapInfo", "1"]) <: u(4, big_endian). +path(["tox", "dht"], ["BootstrapInfo", "2"]) <: arr(u(1, big_endian), [hole ≤ ref(path(["tox", "dht"], ["MaxMotdLength"]))]). +path(["tox", "dht"], ["Cookie"]) <: prod([path(["tox", "dht"], ["Cookie", "0"]), path(["tox", "dht"], ["Cookie", "1"]), path(["tox", "dht"], ["Cookie", "2"])]). +path(["tox", "dht"], ["Cookie", "0"]) <: u(8, big_endian). +path(["tox", "dht"], ["Cookie", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["Cookie", "2"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["CookieRequest"]) <: prod([path(["tox", "dht"], ["CookieRequest", "0"]), path(["tox", "dht"], ["CookieRequest", "1"]), path(["tox", "dht"], ["CookieRequest", "2"]), path(["tox", "dht"], ["CookieRequest", "3"])]). +path(["tox", "dht"], ["CookieRequest", "0"]) <: meet([vint(0x18) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["CookieRequest", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["CookieRequest", "2"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["CookieRequest", "3"]) <: arr(u(1, big_endian), [hole = rint(88)]). +path(["tox", "dht"], ["CookieRequestPayload"]) <: prod([path(["tox", "dht"], ["CookieRequestPayload", "0"]), path(["tox", "dht"], ["CookieRequestPayload", "1"]), path(["tox", "dht"], ["CookieRequestPayload", "2"])]). +path(["tox", "dht"], ["CookieRequestPayload", "0"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["CookieRequestPayload", "1"]) <: arr(vint(0) ∈ integer, [hole = rint(32)]). +path(["tox", "dht"], ["CookieRequestPayload", "2"]) <: u(8, big_endian). +path(["tox", "dht"], ["CookieResponse"]) <: prod([path(["tox", "dht"], ["CookieResponse", "0"]), path(["tox", "dht"], ["CookieResponse", "1"]), path(["tox", "dht"], ["CookieResponse", "2"])]). +path(["tox", "dht"], ["CookieResponse", "0"]) <: meet([vint(0x19) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["CookieResponse", "1"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["CookieResponse", "2"]) <: arr(u(1, big_endian), [hole = rint(136)]). +path(["tox", "dht"], ["CookieResponsePayload"]) <: prod([path(["tox", "dht"], ["CookieResponsePayload", "0"]), path(["tox", "dht"], ["CookieResponsePayload", "1"])]). +path(["tox", "dht"], ["CookieResponsePayload", "0"]) <: ref(path(["tox", "dht"], ["EncryptedCookie"])). +path(["tox", "dht"], ["CookieResponsePayload", "1"]) <: u(8, big_endian). +path(["tox", "dht"], ["CryptoData"]) <: prod([path(["tox", "dht"], ["CryptoData", "0"]), path(["tox", "dht"], ["CryptoData", "1"]), path(["tox", "dht"], ["CryptoData", "2"])]). +path(["tox", "dht"], ["CryptoData", "0"]) <: meet([vint(0x1b) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["CryptoData", "1"]) <: arr(u(1, big_endian), [hole = rint(2)]). +path(["tox", "dht"], ["CryptoData", "2"]) <: arr(u(1, big_endian), []). +path(["tox", "dht"], ["CryptoDataPayload"]) <: prod([path(["tox", "dht"], ["CryptoDataPayload", "0"]), path(["tox", "dht"], ["CryptoDataPayload", "1"]), path(["tox", "dht"], ["CryptoDataPayload", "2"])]). +path(["tox", "dht"], ["CryptoDataPayload", "0"]) <: u(4, big_endian). +path(["tox", "dht"], ["CryptoDataPayload", "1"]) <: u(4, big_endian). +path(["tox", "dht"], ["CryptoDataPayload", "2"]) <: arr(u(1, big_endian), []). +path(["tox", "dht"], ["CryptoHandshake"]) <: prod([path(["tox", "dht"], ["CryptoHandshake", "0"]), path(["tox", "dht"], ["CryptoHandshake", "1"]), path(["tox", "dht"], ["CryptoHandshake", "2"]), path(["tox", "dht"], ["CryptoHandshake", "3"])]). +path(["tox", "dht"], ["CryptoHandshake", "0"]) <: meet([vint(0x1a) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["CryptoHandshake", "1"]) <: ref(path(["tox", "dht"], ["EncryptedCookie"])). +path(["tox", "dht"], ["CryptoHandshake", "2"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["CryptoHandshake", "3"]) <: arr(u(1, big_endian), [hole = rint(248)]). +path(["tox", "dht"], ["CryptoHandshakePayload"]) <: prod([path(["tox", "dht"], ["CryptoHandshakePayload", "0"]), path(["tox", "dht"], ["CryptoHandshakePayload", "1"]), path(["tox", "dht"], ["CryptoHandshakePayload", "2"]), path(["tox", "dht"], ["CryptoHandshakePayload", "3"])]). +path(["tox", "dht"], ["CryptoHandshakePayload", "0"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["CryptoHandshakePayload", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["CryptoHandshakePayload", "2"]) <: ref(path(["tox"], ["Sha512"])). +path(["tox", "dht"], ["CryptoHandshakePayload", "3"]) <: ref(path(["tox", "dht"], ["EncryptedCookie"])). +path(["tox", "dht"], ["DhtPacket"]) <: join([ref(path(["tox", "dht"], ["PingRequest"])), ref(path(["tox", "dht"], ["PingResponse"])), ref(path(["tox", "dht"], ["NodesRequest"])), ref(path(["tox", "dht"], ["NodesResponse"])), ref(path(["tox", "dht"], ["CookieRequest"])), ref(path(["tox", "dht"], ["CookieResponse"])), ref(path(["tox", "dht"], ["CryptoHandshake"])), ref(path(["tox", "dht"], ["CryptoData"])), ref(path(["tox", "dht"], ["DhtRequest"])), ref(path(["tox", "dht"], ["LanDiscovery"])), ref(path(["tox", "dht"], ["BootstrapInfo"]))]). +path(["tox", "dht"], ["DhtPkAnnounce"]) <: prod([path(["tox", "dht"], ["DhtPkAnnounce", "0"]), path(["tox", "dht"], ["DhtPkAnnounce", "1"]), path(["tox", "dht"], ["DhtPkAnnounce", "2"]), path(["tox", "dht"], ["DhtPkAnnounce", "3"])]). +path(["tox", "dht"], ["DhtPkAnnounce", "0"]) <: meet([vint(0x9c) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["DhtPkAnnounce", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["DhtPkAnnounce", "2"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["DhtPkAnnounce", "3"]) <: arr(u(1, big_endian), []). +path(["tox", "dht"], ["DhtRequest"]) <: prod([path(["tox", "dht"], ["DhtRequest", "0"]), path(["tox", "dht"], ["DhtRequest", "1"]), path(["tox", "dht"], ["DhtRequest", "2"]), path(["tox", "dht"], ["DhtRequest", "3"]), path(["tox", "dht"], ["DhtRequest", "4"])]). +path(["tox", "dht"], ["DhtRequest", "0"]) <: meet([vint(0x20) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["DhtRequest", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["DhtRequest", "2"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["DhtRequest", "3"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["DhtRequest", "4"]) <: arr(u(1, big_endian), []). +path(["tox", "dht"], ["DhtRequestPayload"]) <: join([ref(path(["tox", "dht"], ["NatPingRequest"])), ref(path(["tox", "dht"], ["NatPingResponse"])), ref(path(["tox", "dht"], ["DhtPkAnnounce"])), ref(path(["tox", "dht"], ["HardeningRequest"])), ref(path(["tox", "dht"], ["HardeningResponse"]))]). +path(["tox", "dht"], ["EncryptedCookie"]) <: prod([path(["tox", "dht"], ["EncryptedCookie", "0"]), path(["tox", "dht"], ["EncryptedCookie", "1"])]). +path(["tox", "dht"], ["EncryptedCookie", "0"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["EncryptedCookie", "1"]) <: arr(u(1, big_endian), [hole = rint(88)]). +path(["tox", "dht"], ["HardeningRequest"]) <: prod([path(["tox", "dht"], ["HardeningRequest", "0"]), path(["tox", "dht"], ["HardeningRequest", "1"]), path(["tox", "dht"], ["HardeningRequest", "2"])]). +path(["tox", "dht"], ["HardeningRequest", "0"]) <: meet([vint(0x30) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["HardeningRequest", "1"]) <: meet([vint(0x02) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["HardeningRequest", "2"]) <: arr(u(1, big_endian), []). +path(["tox", "dht"], ["HardeningResponse"]) <: prod([path(["tox", "dht"], ["HardeningResponse", "0"]), path(["tox", "dht"], ["HardeningResponse", "1"]), path(["tox", "dht"], ["HardeningResponse", "2"])]). +path(["tox", "dht"], ["HardeningResponse", "0"]) <: meet([vint(0x30) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["HardeningResponse", "1"]) <: meet([vint(0x03) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["HardeningResponse", "2"]) <: arr(u(1, big_endian), []). +path(["tox", "dht"], ["LanDiscovery"]) <: prod([path(["tox", "dht"], ["LanDiscovery", "0"]), path(["tox", "dht"], ["LanDiscovery", "1"])]). +path(["tox", "dht"], ["LanDiscovery", "0"]) <: meet([vint(0x21) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["LanDiscovery", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["MaxMotdLength"]) <: vint(256) ∈ integer. +path(["tox", "dht"], ["NatPingRequest"]) <: prod([path(["tox", "dht"], ["NatPingRequest", "0"]), path(["tox", "dht"], ["NatPingRequest", "1"]), path(["tox", "dht"], ["NatPingRequest", "2"])]). +path(["tox", "dht"], ["NatPingRequest", "0"]) <: meet([vint(0xfe) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["NatPingRequest", "1"]) <: meet([vint(0x00) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["NatPingRequest", "2"]) <: u(8, big_endian). +path(["tox", "dht"], ["NatPingResponse"]) <: prod([path(["tox", "dht"], ["NatPingResponse", "0"]), path(["tox", "dht"], ["NatPingResponse", "1"]), path(["tox", "dht"], ["NatPingResponse", "2"])]). +path(["tox", "dht"], ["NatPingResponse", "0"]) <: meet([vint(0xfe) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["NatPingResponse", "1"]) <: meet([vint(0x01) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["NatPingResponse", "2"]) <: u(8, big_endian). +path(["tox", "dht"], ["NodesRequest"]) <: prod([path(["tox", "dht"], ["NodesRequest", "0"]), path(["tox", "dht"], ["NodesRequest", "1"]), path(["tox", "dht"], ["NodesRequest", "2"])]). +path(["tox", "dht"], ["NodesRequest", "0"]) <: meet([vint(0x03) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["NodesRequest", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["NodesRequest", "2"]) <: arr(u(1, big_endian), [hole = rint(56)]). +path(["tox", "dht"], ["NodesRequestPayload"]) <: prod([path(["tox", "dht"], ["NodesRequestPayload", "0"]), path(["tox", "dht"], ["NodesRequestPayload", "1"])]). +path(["tox", "dht"], ["NodesRequestPayload", "0"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["NodesRequestPayload", "1"]) <: u(8, big_endian). +path(["tox", "dht"], ["NodesResponse"]) <: prod([path(["tox", "dht"], ["NodesResponse", "0"]), path(["tox", "dht"], ["NodesResponse", "1"]), path(["tox", "dht"], ["NodesResponse", "2"]), path(["tox", "dht"], ["NodesResponse", "3"]), path(["tox", "dht"], ["NodesResponse", "4"])]). +path(["tox", "dht"], ["NodesResponse", "0"]) <: meet([vint(0x04) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["NodesResponse", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["NodesResponse", "2"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["NodesResponse", "3"]) <: u(1, big_endian). +path(["tox", "dht"], ["NodesResponse", "4"]) <: arr(u(1, big_endian), [hole ≥ rint(25), hole ≤ rint(229)]). +path(["tox", "dht"], ["NodesResponsePayload"]) <: prod([path(["tox", "dht"], ["NodesResponsePayload", "0"]), path(["tox", "dht"], ["NodesResponsePayload", "1"]), path(["tox", "dht"], ["NodesResponsePayload", "2"])]). +path(["tox", "dht"], ["NodesResponsePayload", "0"]) <: meet([top ⋮ [hole ≤ rint(4)], u(1, big_endian)]). +path(["tox", "dht"], ["NodesResponsePayload", "1"]) <: meet([top ⋮ [sizeof = size([hole ≤ rint(204)])], arr(ref(path(["tox", "dht"], ["PackedNode"])), [hole = ref(path(["tox", "dht"], ["NodesResponsePayload", "_number"]))])]). +path(["tox", "dht"], ["NodesResponsePayload", "2"]) <: u(8, big_endian). +path(["tox", "dht"], ["PackedNode"]) <: prod([path(["tox", "dht"], ["PackedNode", "0"]), path(["tox", "dht"], ["PackedNode", "1"]), path(["tox", "dht"], ["PackedNode", "2"])]). +path(["tox", "dht"], ["PackedNode", "0"]) <: ref(path(["tox"], ["IpAddr"])). +path(["tox", "dht"], ["PackedNode", "1"]) <: u(2, big_endian). +path(["tox", "dht"], ["PackedNode", "2"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["PingRequest"]) <: prod([path(["tox", "dht"], ["PingRequest", "0"]), path(["tox", "dht"], ["PingRequest", "1"]), path(["tox", "dht"], ["PingRequest", "2"]), path(["tox", "dht"], ["PingRequest", "3"])]). +path(["tox", "dht"], ["PingRequest", "0"]) <: meet([vint(0x00) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["PingRequest", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["PingRequest", "2"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["PingRequest", "3"]) <: arr(u(1, big_endian), [hole = rint(24)]). +path(["tox", "dht"], ["PingRequestPayload"]) <: prod([path(["tox", "dht"], ["PingRequestPayload", "0"]), path(["tox", "dht"], ["PingRequestPayload", "1"])]). +path(["tox", "dht"], ["PingRequestPayload", "0"]) <: meet([vint(0x00) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["PingRequestPayload", "1"]) <: u(8, big_endian). +path(["tox", "dht"], ["PingResponse"]) <: prod([path(["tox", "dht"], ["PingResponse", "0"]), path(["tox", "dht"], ["PingResponse", "1"]), path(["tox", "dht"], ["PingResponse", "2"]), path(["tox", "dht"], ["PingResponse", "3"])]). +path(["tox", "dht"], ["PingResponse", "0"]) <: meet([vint(0x01) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["PingResponse", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "dht"], ["PingResponse", "2"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "dht"], ["PingResponse", "3"]) <: arr(u(1, big_endian), [hole = rint(24)]). +path(["tox", "dht"], ["PingResponsePayload"]) <: prod([path(["tox", "dht"], ["PingResponsePayload", "0"]), path(["tox", "dht"], ["PingResponsePayload", "1"])]). +path(["tox", "dht"], ["PingResponsePayload", "0"]) <: meet([vint(0x01) ∈ integer, u(1, big_endian)]). +path(["tox", "dht"], ["PingResponsePayload", "1"]) <: u(8, big_endian). +path(["tox", "friend_connection"], ["Alive"]) <: prod([path(["tox", "friend_connection"], ["Alive", "0"])]). +path(["tox", "friend_connection"], ["Alive", "0"]) <: meet([vint(0x10) ∈ integer, u(1, big_endian)]). +path(["tox", "friend_connection"], ["FcPacket"]) <: join([ref(path(["tox", "friend_connection"], ["Alive"])), ref(path(["tox", "friend_connection"], ["ShareRelays"])), ref(path(["tox", "friend_connection"], ["FriendRequests"]))]). +path(["tox", "friend_connection"], ["FriendRequests"]) <: prod([path(["tox", "friend_connection"], ["FriendRequests", "0"]), path(["tox", "friend_connection"], ["FriendRequests", "1"]), path(["tox", "friend_connection"], ["FriendRequests", "2"])]). +path(["tox", "friend_connection"], ["FriendRequests", "0"]) <: meet([vint(0x12) ∈ integer, u(1, big_endian)]). +path(["tox", "friend_connection"], ["FriendRequests", "1"]) <: ref(path(["tox"], ["NoSpam"])). +path(["tox", "friend_connection"], ["FriendRequests", "2"]) <: arr(u(1, big_endian), []). +path(["tox", "friend_connection"], ["ShareRelays"]) <: prod([path(["tox", "friend_connection"], ["ShareRelays", "0"]), path(["tox", "friend_connection"], ["ShareRelays", "1"])]). +path(["tox", "friend_connection"], ["ShareRelays", "0"]) <: meet([vint(0x11) ∈ integer, u(1, big_endian)]). +path(["tox", "friend_connection"], ["ShareRelays", "1"]) <: meet([top ⋮ [sizeof = size([hole ≤ rint(153)])], arr(ref(path(["tox", "dht"], ["PackedNode"])), [])]). +path(["tox", "onion"], ["AnnounceRequest"]) <: prod([path(["tox", "onion"], ["AnnounceRequest", "0"]), path(["tox", "onion"], ["AnnounceRequest", "1"]), path(["tox", "onion"], ["AnnounceRequest", "2"]), path(["tox", "onion"], ["AnnounceRequest", "3"])]). +path(["tox", "onion"], ["AnnounceRequest", "0"]) <: meet([vint(0x83) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["AnnounceRequest", "1"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "onion"], ["AnnounceRequest", "2"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "onion"], ["AnnounceRequest", "3"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["AnnounceResponse"]) <: prod([path(["tox", "onion"], ["AnnounceResponse", "0"]), path(["tox", "onion"], ["AnnounceResponse", "1"]), path(["tox", "onion"], ["AnnounceResponse", "2"]), path(["tox", "onion"], ["AnnounceResponse", "3"])]). +path(["tox", "onion"], ["AnnounceResponse", "0"]) <: meet([vint(0x84) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["AnnounceResponse", "1"]) <: u(8, big_endian). +path(["tox", "onion"], ["AnnounceResponse", "2"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "onion"], ["AnnounceResponse", "3"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["OnionDataRequest"]) <: prod([path(["tox", "onion"], ["OnionDataRequest", "0"]), path(["tox", "onion"], ["OnionDataRequest", "1"]), path(["tox", "onion"], ["OnionDataRequest", "2"]), path(["tox", "onion"], ["OnionDataRequest", "3"]), path(["tox", "onion"], ["OnionDataRequest", "4"])]). +path(["tox", "onion"], ["OnionDataRequest", "0"]) <: meet([vint(0x85) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["OnionDataRequest", "1"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "onion"], ["OnionDataRequest", "2"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "onion"], ["OnionDataRequest", "3"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "onion"], ["OnionDataRequest", "4"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["OnionDataResponse"]) <: prod([path(["tox", "onion"], ["OnionDataResponse", "0"]), path(["tox", "onion"], ["OnionDataResponse", "1"]), path(["tox", "onion"], ["OnionDataResponse", "2"]), path(["tox", "onion"], ["OnionDataResponse", "3"])]). +path(["tox", "onion"], ["OnionDataResponse", "0"]) <: meet([vint(0x86) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["OnionDataResponse", "1"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "onion"], ["OnionDataResponse", "2"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "onion"], ["OnionDataResponse", "3"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["OnionPacket"]) <: join([ref(path(["tox", "onion"], ["OnionRequest0"])), ref(path(["tox", "onion"], ["OnionRequest1"])), ref(path(["tox", "onion"], ["OnionRequest2"])), ref(path(["tox", "onion"], ["AnnounceRequest"])), ref(path(["tox", "onion"], ["AnnounceResponse"])), ref(path(["tox", "onion"], ["OnionDataRequest"])), ref(path(["tox", "onion"], ["OnionDataResponse"])), ref(path(["tox", "onion"], ["OnionResponse3"])), ref(path(["tox", "onion"], ["OnionResponse2"])), ref(path(["tox", "onion"], ["OnionResponse1"]))]). +path(["tox", "onion"], ["OnionRequest0"]) <: prod([path(["tox", "onion"], ["OnionRequest0", "0"]), path(["tox", "onion"], ["OnionRequest0", "1"]), path(["tox", "onion"], ["OnionRequest0", "2"]), path(["tox", "onion"], ["OnionRequest0", "3"])]). +path(["tox", "onion"], ["OnionRequest0", "0"]) <: meet([vint(0x80) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["OnionRequest0", "1"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "onion"], ["OnionRequest0", "2"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "onion"], ["OnionRequest0", "3"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["OnionRequest1"]) <: prod([path(["tox", "onion"], ["OnionRequest1", "0"]), path(["tox", "onion"], ["OnionRequest1", "1"]), path(["tox", "onion"], ["OnionRequest1", "2"]), path(["tox", "onion"], ["OnionRequest1", "3"]), path(["tox", "onion"], ["OnionRequest1", "4"])]). +path(["tox", "onion"], ["OnionRequest1", "0"]) <: meet([vint(0x81) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["OnionRequest1", "1"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "onion"], ["OnionRequest1", "2"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "onion"], ["OnionRequest1", "3"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["OnionRequest1", "4"]) <: arr(u(1, big_endian), [hole = rint(59)]). +path(["tox", "onion"], ["OnionRequest2"]) <: prod([path(["tox", "onion"], ["OnionRequest2", "0"]), path(["tox", "onion"], ["OnionRequest2", "1"]), path(["tox", "onion"], ["OnionRequest2", "2"]), path(["tox", "onion"], ["OnionRequest2", "3"]), path(["tox", "onion"], ["OnionRequest2", "4"])]). +path(["tox", "onion"], ["OnionRequest2", "0"]) <: meet([vint(0x82) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["OnionRequest2", "1"]) <: ref(path(["tox"], ["Nonce"])). +path(["tox", "onion"], ["OnionRequest2", "2"]) <: ref(path(["tox"], ["PublicKey"])). +path(["tox", "onion"], ["OnionRequest2", "3"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["OnionRequest2", "4"]) <: arr(u(1, big_endian), [hole = rint(118)]). +path(["tox", "onion"], ["OnionResponse1"]) <: prod([path(["tox", "onion"], ["OnionResponse1", "0"]), path(["tox", "onion"], ["OnionResponse1", "1"]), path(["tox", "onion"], ["OnionResponse1", "2"])]). +path(["tox", "onion"], ["OnionResponse1", "0"]) <: meet([vint(0x8e) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["OnionResponse1", "1"]) <: arr(u(1, big_endian), [hole = rint(59)]). +path(["tox", "onion"], ["OnionResponse1", "2"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["OnionResponse2"]) <: prod([path(["tox", "onion"], ["OnionResponse2", "0"]), path(["tox", "onion"], ["OnionResponse2", "1"]), path(["tox", "onion"], ["OnionResponse2", "2"])]). +path(["tox", "onion"], ["OnionResponse2", "0"]) <: meet([vint(0x8d) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["OnionResponse2", "1"]) <: arr(u(1, big_endian), [hole = rint(118)]). +path(["tox", "onion"], ["OnionResponse2", "2"]) <: arr(u(1, big_endian), []). +path(["tox", "onion"], ["OnionResponse3"]) <: prod([path(["tox", "onion"], ["OnionResponse3", "0"]), path(["tox", "onion"], ["OnionResponse3", "1"]), path(["tox", "onion"], ["OnionResponse3", "2"])]). +path(["tox", "onion"], ["OnionResponse3", "0"]) <: meet([vint(0x8c) ∈ integer, u(1, big_endian)]). +path(["tox", "onion"], ["OnionResponse3", "1"]) <: arr(u(1, big_endian), [hole = rint(177)]). +path(["tox", "onion"], ["OnionResponse3", "2"]) <: arr(u(1, big_endian), []). +nameof(path(["tox"], ["IpAddr"]), path(["tox"], ["IpAddr"])). +nameof(path(["tox"], ["Ipv4Addr"]), path(["tox"], ["Ipv4Addr"])). +nameof(path(["tox"], ["Ipv4Addr", "0"]), path(["tox"], ["Ipv4Addr", "0"])). +nameof(path(["tox"], ["Ipv4Addr", "1"]), path(["tox"], ["Ipv4Addr", "data"])). +nameof(path(["tox"], ["Ipv6Addr"]), path(["tox"], ["Ipv6Addr"])). +nameof(path(["tox"], ["Ipv6Addr", "0"]), path(["tox"], ["Ipv6Addr", "0"])). +nameof(path(["tox"], ["Ipv6Addr", "1"]), path(["tox"], ["Ipv6Addr", "data"])). +nameof(path(["tox"], ["NoSpam"]), path(["tox"], ["NoSpam"])). +nameof(path(["tox"], ["Nonce"]), path(["tox"], ["Nonce"])). +nameof(path(["tox"], ["Packet"]), path(["tox"], ["Packet"])). +nameof(path(["tox"], ["PublicKey"]), path(["tox"], ["PublicKey"])). +nameof(path(["tox"], ["Sha512"]), path(["tox"], ["Sha512"])). +nameof(path(["tox", "dht"], ["BootstrapInfo"]), path(["tox", "dht"], ["BootstrapInfo"])). +nameof(path(["tox", "dht"], ["BootstrapInfo", "0"]), path(["tox", "dht"], ["BootstrapInfo", "0"])). +nameof(path(["tox", "dht"], ["BootstrapInfo", "1"]), path(["tox", "dht"], ["BootstrapInfo", "version"])). +nameof(path(["tox", "dht"], ["BootstrapInfo", "2"]), path(["tox", "dht"], ["BootstrapInfo", "motd"])). +nameof(path(["tox", "dht"], ["Cookie"]), path(["tox", "dht"], ["Cookie"])). +nameof(path(["tox", "dht"], ["Cookie", "0"]), path(["tox", "dht"], ["Cookie", "time"])). +nameof(path(["tox", "dht"], ["Cookie", "1"]), path(["tox", "dht"], ["Cookie", "real_pk"])). +nameof(path(["tox", "dht"], ["Cookie", "2"]), path(["tox", "dht"], ["Cookie", "dht_pk"])). +nameof(path(["tox", "dht"], ["CookieRequest"]), path(["tox", "dht"], ["CookieRequest"])). +nameof(path(["tox", "dht"], ["CookieRequest", "0"]), path(["tox", "dht"], ["CookieRequest", "0"])). +nameof(path(["tox", "dht"], ["CookieRequest", "1"]), path(["tox", "dht"], ["CookieRequest", "public_key"])). +nameof(path(["tox", "dht"], ["CookieRequest", "2"]), path(["tox", "dht"], ["CookieRequest", "nonce"])). +nameof(path(["tox", "dht"], ["CookieRequest", "3"]), path(["tox", "dht"], ["CookieRequest", "payload"])). +nameof(path(["tox", "dht"], ["CookieRequestPayload"]), path(["tox", "dht"], ["CookieRequestPayload"])). +nameof(path(["tox", "dht"], ["CookieRequestPayload", "0"]), path(["tox", "dht"], ["CookieRequestPayload", "public_key"])). +nameof(path(["tox", "dht"], ["CookieRequestPayload", "1"]), path(["tox", "dht"], ["CookieRequestPayload", "1"])). +nameof(path(["tox", "dht"], ["CookieRequestPayload", "2"]), path(["tox", "dht"], ["CookieRequestPayload", "id"])). +nameof(path(["tox", "dht"], ["CookieResponse"]), path(["tox", "dht"], ["CookieResponse"])). +nameof(path(["tox", "dht"], ["CookieResponse", "0"]), path(["tox", "dht"], ["CookieResponse", "0"])). +nameof(path(["tox", "dht"], ["CookieResponse", "1"]), path(["tox", "dht"], ["CookieResponse", "nonce"])). +nameof(path(["tox", "dht"], ["CookieResponse", "2"]), path(["tox", "dht"], ["CookieResponse", "payload"])). +nameof(path(["tox", "dht"], ["CookieResponsePayload"]), path(["tox", "dht"], ["CookieResponsePayload"])). +nameof(path(["tox", "dht"], ["CookieResponsePayload", "0"]), path(["tox", "dht"], ["CookieResponsePayload", "cookie"])). +nameof(path(["tox", "dht"], ["CookieResponsePayload", "1"]), path(["tox", "dht"], ["CookieResponsePayload", "id"])). +nameof(path(["tox", "dht"], ["CryptoData"]), path(["tox", "dht"], ["CryptoData"])). +nameof(path(["tox", "dht"], ["CryptoData", "0"]), path(["tox", "dht"], ["CryptoData", "0"])). +nameof(path(["tox", "dht"], ["CryptoData", "1"]), path(["tox", "dht"], ["CryptoData", "nonce_last_two"])). +nameof(path(["tox", "dht"], ["CryptoData", "2"]), path(["tox", "dht"], ["CryptoData", "payload"])). +nameof(path(["tox", "dht"], ["CryptoDataPayload"]), path(["tox", "dht"], ["CryptoDataPayload"])). +nameof(path(["tox", "dht"], ["CryptoDataPayload", "0"]), path(["tox", "dht"], ["CryptoDataPayload", "buffer_start"])). +nameof(path(["tox", "dht"], ["CryptoDataPayload", "1"]), path(["tox", "dht"], ["CryptoDataPayload", "packet_number"])). +nameof(path(["tox", "dht"], ["CryptoDataPayload", "2"]), path(["tox", "dht"], ["CryptoDataPayload", "data"])). +nameof(path(["tox", "dht"], ["CryptoHandshake"]), path(["tox", "dht"], ["CryptoHandshake"])). +nameof(path(["tox", "dht"], ["CryptoHandshake", "0"]), path(["tox", "dht"], ["CryptoHandshake", "0"])). +nameof(path(["tox", "dht"], ["CryptoHandshake", "1"]), path(["tox", "dht"], ["CryptoHandshake", "cookie"])). +nameof(path(["tox", "dht"], ["CryptoHandshake", "2"]), path(["tox", "dht"], ["CryptoHandshake", "nonce"])). +nameof(path(["tox", "dht"], ["CryptoHandshake", "3"]), path(["tox", "dht"], ["CryptoHandshake", "payload"])). +nameof(path(["tox", "dht"], ["CryptoHandshakePayload"]), path(["tox", "dht"], ["CryptoHandshakePayload"])). +nameof(path(["tox", "dht"], ["CryptoHandshakePayload", "0"]), path(["tox", "dht"], ["CryptoHandshakePayload", "base_nonce"])). +nameof(path(["tox", "dht"], ["CryptoHandshakePayload", "1"]), path(["tox", "dht"], ["CryptoHandshakePayload", "session_pk"])). +nameof(path(["tox", "dht"], ["CryptoHandshakePayload", "2"]), path(["tox", "dht"], ["CryptoHandshakePayload", "cookie_hash"])). +nameof(path(["tox", "dht"], ["CryptoHandshakePayload", "3"]), path(["tox", "dht"], ["CryptoHandshakePayload", "cookie"])). +nameof(path(["tox", "dht"], ["DhtPacket"]), path(["tox", "dht"], ["DhtPacket"])). +nameof(path(["tox", "dht"], ["DhtPkAnnounce"]), path(["tox", "dht"], ["DhtPkAnnounce"])). +nameof(path(["tox", "dht"], ["DhtPkAnnounce", "0"]), path(["tox", "dht"], ["DhtPkAnnounce", "0"])). +nameof(path(["tox", "dht"], ["DhtPkAnnounce", "1"]), path(["tox", "dht"], ["DhtPkAnnounce", "real_pk"])). +nameof(path(["tox", "dht"], ["DhtPkAnnounce", "2"]), path(["tox", "dht"], ["DhtPkAnnounce", "nonce"])). +nameof(path(["tox", "dht"], ["DhtPkAnnounce", "3"]), path(["tox", "dht"], ["DhtPkAnnounce", "payload"])). +nameof(path(["tox", "dht"], ["DhtRequest"]), path(["tox", "dht"], ["DhtRequest"])). +nameof(path(["tox", "dht"], ["DhtRequest", "0"]), path(["tox", "dht"], ["DhtRequest", "0"])). +nameof(path(["tox", "dht"], ["DhtRequest", "1"]), path(["tox", "dht"], ["DhtRequest", "receiver_pk"])). +nameof(path(["tox", "dht"], ["DhtRequest", "2"]), path(["tox", "dht"], ["DhtRequest", "sender_pk"])). +nameof(path(["tox", "dht"], ["DhtRequest", "3"]), path(["tox", "dht"], ["DhtRequest", "nonce"])). +nameof(path(["tox", "dht"], ["DhtRequest", "4"]), path(["tox", "dht"], ["DhtRequest", "payload"])). +nameof(path(["tox", "dht"], ["DhtRequestPayload"]), path(["tox", "dht"], ["DhtRequestPayload"])). +nameof(path(["tox", "dht"], ["EncryptedCookie"]), path(["tox", "dht"], ["EncryptedCookie"])). +nameof(path(["tox", "dht"], ["EncryptedCookie", "0"]), path(["tox", "dht"], ["EncryptedCookie", "nonce"])). +nameof(path(["tox", "dht"], ["EncryptedCookie", "1"]), path(["tox", "dht"], ["EncryptedCookie", "payload"])). +nameof(path(["tox", "dht"], ["HardeningRequest"]), path(["tox", "dht"], ["HardeningRequest"])). +nameof(path(["tox", "dht"], ["HardeningRequest", "0"]), path(["tox", "dht"], ["HardeningRequest", "0"])). +nameof(path(["tox", "dht"], ["HardeningRequest", "1"]), path(["tox", "dht"], ["HardeningRequest", "1"])). +nameof(path(["tox", "dht"], ["HardeningRequest", "2"]), path(["tox", "dht"], ["HardeningRequest", "2"])). +nameof(path(["tox", "dht"], ["HardeningResponse"]), path(["tox", "dht"], ["HardeningResponse"])). +nameof(path(["tox", "dht"], ["HardeningResponse", "0"]), path(["tox", "dht"], ["HardeningResponse", "0"])). +nameof(path(["tox", "dht"], ["HardeningResponse", "1"]), path(["tox", "dht"], ["HardeningResponse", "1"])). +nameof(path(["tox", "dht"], ["HardeningResponse", "2"]), path(["tox", "dht"], ["HardeningResponse", "2"])). +nameof(path(["tox", "dht"], ["LanDiscovery"]), path(["tox", "dht"], ["LanDiscovery"])). +nameof(path(["tox", "dht"], ["LanDiscovery", "0"]), path(["tox", "dht"], ["LanDiscovery", "0"])). +nameof(path(["tox", "dht"], ["LanDiscovery", "1"]), path(["tox", "dht"], ["LanDiscovery", "public_key"])). +nameof(path(["tox", "dht"], ["MaxMotdLength"]), path(["tox", "dht"], ["MaxMotdLength"])). +nameof(path(["tox", "dht"], ["NatPingRequest"]), path(["tox", "dht"], ["NatPingRequest"])). +nameof(path(["tox", "dht"], ["NatPingRequest", "0"]), path(["tox", "dht"], ["NatPingRequest", "0"])). +nameof(path(["tox", "dht"], ["NatPingRequest", "1"]), path(["tox", "dht"], ["NatPingRequest", "1"])). +nameof(path(["tox", "dht"], ["NatPingRequest", "2"]), path(["tox", "dht"], ["NatPingRequest", "id"])). +nameof(path(["tox", "dht"], ["NatPingResponse"]), path(["tox", "dht"], ["NatPingResponse"])). +nameof(path(["tox", "dht"], ["NatPingResponse", "0"]), path(["tox", "dht"], ["NatPingResponse", "0"])). +nameof(path(["tox", "dht"], ["NatPingResponse", "1"]), path(["tox", "dht"], ["NatPingResponse", "1"])). +nameof(path(["tox", "dht"], ["NatPingResponse", "2"]), path(["tox", "dht"], ["NatPingResponse", "id"])). +nameof(path(["tox", "dht"], ["NodesRequest"]), path(["tox", "dht"], ["NodesRequest"])). +nameof(path(["tox", "dht"], ["NodesRequest", "0"]), path(["tox", "dht"], ["NodesRequest", "0"])). +nameof(path(["tox", "dht"], ["NodesRequest", "1"]), path(["tox", "dht"], ["NodesRequest", "public_key"])). +nameof(path(["tox", "dht"], ["NodesRequest", "2"]), path(["tox", "dht"], ["NodesRequest", "payload"])). +nameof(path(["tox", "dht"], ["NodesRequestPayload"]), path(["tox", "dht"], ["NodesRequestPayload"])). +nameof(path(["tox", "dht"], ["NodesRequestPayload", "0"]), path(["tox", "dht"], ["NodesRequestPayload", "public_key"])). +nameof(path(["tox", "dht"], ["NodesRequestPayload", "1"]), path(["tox", "dht"], ["NodesRequestPayload", "id"])). +nameof(path(["tox", "dht"], ["NodesResponse"]), path(["tox", "dht"], ["NodesResponse"])). +nameof(path(["tox", "dht"], ["NodesResponse", "0"]), path(["tox", "dht"], ["NodesResponse", "0"])). +nameof(path(["tox", "dht"], ["NodesResponse", "1"]), path(["tox", "dht"], ["NodesResponse", "public_key"])). +nameof(path(["tox", "dht"], ["NodesResponse", "2"]), path(["tox", "dht"], ["NodesResponse", "nonce"])). +nameof(path(["tox", "dht"], ["NodesResponse", "3"]), path(["tox", "dht"], ["NodesResponse", "number"])). +nameof(path(["tox", "dht"], ["NodesResponse", "4"]), path(["tox", "dht"], ["NodesResponse", "payload"])). +nameof(path(["tox", "dht"], ["NodesResponsePayload"]), path(["tox", "dht"], ["NodesResponsePayload"])). +nameof(path(["tox", "dht"], ["NodesResponsePayload", "0"]), path(["tox", "dht"], ["NodesResponsePayload", "_number"])). +nameof(path(["tox", "dht"], ["NodesResponsePayload", "1"]), path(["tox", "dht"], ["NodesResponsePayload", "nodes"])). +nameof(path(["tox", "dht"], ["NodesResponsePayload", "2"]), path(["tox", "dht"], ["NodesResponsePayload", "id"])). +nameof(path(["tox", "dht"], ["PackedNode"]), path(["tox", "dht"], ["PackedNode"])). +nameof(path(["tox", "dht"], ["PackedNode", "0"]), path(["tox", "dht"], ["PackedNode", "addr"])). +nameof(path(["tox", "dht"], ["PackedNode", "1"]), path(["tox", "dht"], ["PackedNode", "port"])). +nameof(path(["tox", "dht"], ["PackedNode", "2"]), path(["tox", "dht"], ["PackedNode", "pk"])). +nameof(path(["tox", "dht"], ["PingRequest"]), path(["tox", "dht"], ["PingRequest"])). +nameof(path(["tox", "dht"], ["PingRequest", "0"]), path(["tox", "dht"], ["PingRequest", "0"])). +nameof(path(["tox", "dht"], ["PingRequest", "1"]), path(["tox", "dht"], ["PingRequest", "public_key"])). +nameof(path(["tox", "dht"], ["PingRequest", "2"]), path(["tox", "dht"], ["PingRequest", "nonce"])). +nameof(path(["tox", "dht"], ["PingRequest", "3"]), path(["tox", "dht"], ["PingRequest", "payload"])). +nameof(path(["tox", "dht"], ["PingRequestPayload"]), path(["tox", "dht"], ["PingRequestPayload"])). +nameof(path(["tox", "dht"], ["PingRequestPayload", "0"]), path(["tox", "dht"], ["PingRequestPayload", "0"])). +nameof(path(["tox", "dht"], ["PingRequestPayload", "1"]), path(["tox", "dht"], ["PingRequestPayload", "id"])). +nameof(path(["tox", "dht"], ["PingResponse"]), path(["tox", "dht"], ["PingResponse"])). +nameof(path(["tox", "dht"], ["PingResponse", "0"]), path(["tox", "dht"], ["PingResponse", "0"])). +nameof(path(["tox", "dht"], ["PingResponse", "1"]), path(["tox", "dht"], ["PingResponse", "public_key"])). +nameof(path(["tox", "dht"], ["PingResponse", "2"]), path(["tox", "dht"], ["PingResponse", "nonce"])). +nameof(path(["tox", "dht"], ["PingResponse", "3"]), path(["tox", "dht"], ["PingResponse", "payload"])). +nameof(path(["tox", "dht"], ["PingResponsePayload"]), path(["tox", "dht"], ["PingResponsePayload"])). +nameof(path(["tox", "dht"], ["PingResponsePayload", "0"]), path(["tox", "dht"], ["PingResponsePayload", "0"])). +nameof(path(["tox", "dht"], ["PingResponsePayload", "1"]), path(["tox", "dht"], ["PingResponsePayload", "id"])). +nameof(path(["tox", "friend_connection"], ["Alive"]), path(["tox", "friend_connection"], ["Alive"])). +nameof(path(["tox", "friend_connection"], ["Alive", "0"]), path(["tox", "friend_connection"], ["Alive", "0"])). +nameof(path(["tox", "friend_connection"], ["FcPacket"]), path(["tox", "friend_connection"], ["FcPacket"])). +nameof(path(["tox", "friend_connection"], ["FriendRequests"]), path(["tox", "friend_connection"], ["FriendRequests"])). +nameof(path(["tox", "friend_connection"], ["FriendRequests", "0"]), path(["tox", "friend_connection"], ["FriendRequests", "0"])). +nameof(path(["tox", "friend_connection"], ["FriendRequests", "1"]), path(["tox", "friend_connection"], ["FriendRequests", "nospam"])). +nameof(path(["tox", "friend_connection"], ["FriendRequests", "2"]), path(["tox", "friend_connection"], ["FriendRequests", "message"])). +nameof(path(["tox", "friend_connection"], ["ShareRelays"]), path(["tox", "friend_connection"], ["ShareRelays"])). +nameof(path(["tox", "friend_connection"], ["ShareRelays", "0"]), path(["tox", "friend_connection"], ["ShareRelays", "0"])). +nameof(path(["tox", "friend_connection"], ["ShareRelays", "1"]), path(["tox", "friend_connection"], ["ShareRelays", "relays"])). +nameof(path(["tox", "onion"], ["AnnounceRequest"]), path(["tox", "onion"], ["AnnounceRequest"])). +nameof(path(["tox", "onion"], ["AnnounceRequest", "0"]), path(["tox", "onion"], ["AnnounceRequest", "0"])). +nameof(path(["tox", "onion"], ["AnnounceRequest", "1"]), path(["tox", "onion"], ["AnnounceRequest", "nonce"])). +nameof(path(["tox", "onion"], ["AnnounceRequest", "2"]), path(["tox", "onion"], ["AnnounceRequest", "public_key"])). +nameof(path(["tox", "onion"], ["AnnounceRequest", "3"]), path(["tox", "onion"], ["AnnounceRequest", "payload"])). +nameof(path(["tox", "onion"], ["AnnounceResponse"]), path(["tox", "onion"], ["AnnounceResponse"])). +nameof(path(["tox", "onion"], ["AnnounceResponse", "0"]), path(["tox", "onion"], ["AnnounceResponse", "0"])). +nameof(path(["tox", "onion"], ["AnnounceResponse", "1"]), path(["tox", "onion"], ["AnnounceResponse", "sendback"])). +nameof(path(["tox", "onion"], ["AnnounceResponse", "2"]), path(["tox", "onion"], ["AnnounceResponse", "nonce"])). +nameof(path(["tox", "onion"], ["AnnounceResponse", "3"]), path(["tox", "onion"], ["AnnounceResponse", "payload"])). +nameof(path(["tox", "onion"], ["OnionDataRequest"]), path(["tox", "onion"], ["OnionDataRequest"])). +nameof(path(["tox", "onion"], ["OnionDataRequest", "0"]), path(["tox", "onion"], ["OnionDataRequest", "0"])). +nameof(path(["tox", "onion"], ["OnionDataRequest", "1"]), path(["tox", "onion"], ["OnionDataRequest", "destination_pk"])). +nameof(path(["tox", "onion"], ["OnionDataRequest", "2"]), path(["tox", "onion"], ["OnionDataRequest", "nonce"])). +nameof(path(["tox", "onion"], ["OnionDataRequest", "3"]), path(["tox", "onion"], ["OnionDataRequest", "temporary_pk"])). +nameof(path(["tox", "onion"], ["OnionDataRequest", "4"]), path(["tox", "onion"], ["OnionDataRequest", "payload"])). +nameof(path(["tox", "onion"], ["OnionDataResponse"]), path(["tox", "onion"], ["OnionDataResponse"])). +nameof(path(["tox", "onion"], ["OnionDataResponse", "0"]), path(["tox", "onion"], ["OnionDataResponse", "0"])). +nameof(path(["tox", "onion"], ["OnionDataResponse", "1"]), path(["tox", "onion"], ["OnionDataResponse", "nonce"])). +nameof(path(["tox", "onion"], ["OnionDataResponse", "2"]), path(["tox", "onion"], ["OnionDataResponse", "public_key"])). +nameof(path(["tox", "onion"], ["OnionDataResponse", "3"]), path(["tox", "onion"], ["OnionDataResponse", "payload"])). +nameof(path(["tox", "onion"], ["OnionPacket"]), path(["tox", "onion"], ["OnionPacket"])). +nameof(path(["tox", "onion"], ["OnionRequest0"]), path(["tox", "onion"], ["OnionRequest0"])). +nameof(path(["tox", "onion"], ["OnionRequest0", "0"]), path(["tox", "onion"], ["OnionRequest0", "0"])). +nameof(path(["tox", "onion"], ["OnionRequest0", "1"]), path(["tox", "onion"], ["OnionRequest0", "nonce"])). +nameof(path(["tox", "onion"], ["OnionRequest0", "2"]), path(["tox", "onion"], ["OnionRequest0", "public_key"])). +nameof(path(["tox", "onion"], ["OnionRequest0", "3"]), path(["tox", "onion"], ["OnionRequest0", "payload"])). +nameof(path(["tox", "onion"], ["OnionRequest1"]), path(["tox", "onion"], ["OnionRequest1"])). +nameof(path(["tox", "onion"], ["OnionRequest1", "0"]), path(["tox", "onion"], ["OnionRequest1", "0"])). +nameof(path(["tox", "onion"], ["OnionRequest1", "1"]), path(["tox", "onion"], ["OnionRequest1", "nonce"])). +nameof(path(["tox", "onion"], ["OnionRequest1", "2"]), path(["tox", "onion"], ["OnionRequest1", "public_key"])). +nameof(path(["tox", "onion"], ["OnionRequest1", "3"]), path(["tox", "onion"], ["OnionRequest1", "payload"])). +nameof(path(["tox", "onion"], ["OnionRequest1", "4"]), path(["tox", "onion"], ["OnionRequest1", "onion_return"])). +nameof(path(["tox", "onion"], ["OnionRequest2"]), path(["tox", "onion"], ["OnionRequest2"])). +nameof(path(["tox", "onion"], ["OnionRequest2", "0"]), path(["tox", "onion"], ["OnionRequest2", "0"])). +nameof(path(["tox", "onion"], ["OnionRequest2", "1"]), path(["tox", "onion"], ["OnionRequest2", "nonce"])). +nameof(path(["tox", "onion"], ["OnionRequest2", "2"]), path(["tox", "onion"], ["OnionRequest2", "public_key"])). +nameof(path(["tox", "onion"], ["OnionRequest2", "3"]), path(["tox", "onion"], ["OnionRequest2", "payload"])). +nameof(path(["tox", "onion"], ["OnionRequest2", "4"]), path(["tox", "onion"], ["OnionRequest2", "onion_return"])). +nameof(path(["tox", "onion"], ["OnionResponse1"]), path(["tox", "onion"], ["OnionResponse1"])). +nameof(path(["tox", "onion"], ["OnionResponse1", "0"]), path(["tox", "onion"], ["OnionResponse1", "0"])). +nameof(path(["tox", "onion"], ["OnionResponse1", "1"]), path(["tox", "onion"], ["OnionResponse1", "onion_return"])). +nameof(path(["tox", "onion"], ["OnionResponse1", "2"]), path(["tox", "onion"], ["OnionResponse1", "payload"])). +nameof(path(["tox", "onion"], ["OnionResponse2"]), path(["tox", "onion"], ["OnionResponse2"])). +nameof(path(["tox", "onion"], ["OnionResponse2", "0"]), path(["tox", "onion"], ["OnionResponse2", "0"])). +nameof(path(["tox", "onion"], ["OnionResponse2", "1"]), path(["tox", "onion"], ["OnionResponse2", "onion_return"])). +nameof(path(["tox", "onion"], ["OnionResponse2", "2"]), path(["tox", "onion"], ["OnionResponse2", "payload"])). +nameof(path(["tox", "onion"], ["OnionResponse3"]), path(["tox", "onion"], ["OnionResponse3"])). +nameof(path(["tox", "onion"], ["OnionResponse3", "0"]), path(["tox", "onion"], ["OnionResponse3", "0"])). +nameof(path(["tox", "onion"], ["OnionResponse3", "1"]), path(["tox", "onion"], ["OnionResponse3", "onion_return"])). +nameof(path(["tox", "onion"], ["OnionResponse3", "2"]), path(["tox", "onion"], ["OnionResponse3", "payload"])). +def(path(["tox", "onion"], ["OnionPacket"])). +def(path(["tox", "dht"], ["DhtPacket"])). diff --git a/src/expr.rs b/src/expr.rs index 50271f8..466f868 100644 --- a/src/expr.rs +++ b/src/expr.rs @@ -38,6 +38,15 @@ pub struct Ranged { pub range: Option, } +impl Ranged { + pub fn new(data: T) -> Self { + Ranged { + data, + range: None + } + } +} + #[derive(Debug, Clone, PartialEq)] pub enum RawExpr { Apply { diff --git a/src/lib.rs b/src/lib.rs index 811992c..1119b1d 100644 --- a/src/lib.rs +++ b/src/lib.rs @@ -4,6 +4,7 @@ use pest_derive::Parser; pub mod path; pub mod expr; +pub mod types; pub mod report; #[derive(Parser)] diff --git a/src/main.rs b/src/main.rs index 6297b48..6896629 100644 --- a/src/main.rs +++ b/src/main.rs @@ -7,28 +7,53 @@ type Error = Box; fn main() -> Result<(), Error> { let loader = razbor::expr::ExprLoader::new(); - let (file_table, tox) = loader.load("../tox/tox-ksy/razbor/tox.mexpr"); + let (file_table, tox) = loader.load("../tox/tox-razbor/src/tox.mexpr"); let mods = tox.unwrap(); let converter = razbor::path::ExprConverter::new(); let mut table = converter.convert(&mods).unwrap(); let namer = razbor::path::NameResolver::new(); - let errors = namer.resolve(&mut table).unwrap_err(); - - let mut sourcer = razbor::report::Sourcer::default(); - for err in &errors { - let id = err.file_id(); - let path = &*file_table.files()[id]; - sourcer.load_file(id, path); + namer.resolve(&mut table).unwrap(); + + let ty_conv = razbor::types::ExprToType::new(); + // let errors = ty_conv.into_types(table).unwrap_err(); + let ty_table = ty_conv.into_types(table).unwrap(); + + println!(":- [ops].\n"); + for row in ty_table.rows { + let path = razbor::types::as_makam_path(&row.path); + let ty = razbor::types::as_makam_ty(&row.ty.data); + + println!("{} <: {}.", path, ty); } - for err in &errors { - let snippet = err.to_snippet(&sourcer); - let dl = DisplayList::from(snippet); - let dlf = DisplayListFormatter::new(true, false); - println!("{}", dlf.format(&dl)); + for name_row in ty_table.names { + let path = razbor::types::as_makam_path(&name_row.path); + let name = razbor::types::as_makam_path(&name_row.name.data); + + println!("nameof({}, {}).", path, name); } + for def in ty_table.defs { + let path = razbor::types::as_makam_path(&def); + + println!("def({}).", path) + } + + // let mut sourcer = razbor::report::Sourcer::default(); + // for err in &errors { + // let id = err.file_id(); + // let path = &*file_table.files()[id]; + // sourcer.load_file(id, path); + // } + + // for err in &errors { + // let snippet = err.to_snippet(&sourcer); + // let dl = DisplayList::from(snippet); + // let dlf = DisplayListFormatter::new(true, false); + // println!("{}", dlf.format(&dl)); + // } + Ok(()) } diff --git a/src/path.rs b/src/path.rs index 8a73885..4ec22f7 100644 --- a/src/path.rs +++ b/src/path.rs @@ -13,6 +13,15 @@ pub enum PathSegment { Name(SmolStr), } +impl std::fmt::Display for PathSegment { + fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { + match self { + PathSegment::Pos(n) => write!(f, "{}", n), + PathSegment::Name(name) => write!(f, "{}", name) + } + } +} + #[derive(Debug, Clone, PartialEq, PartialOrd, Eq, Ord, Default)] pub struct RzPath { pub modules: Vec, @@ -230,6 +239,27 @@ impl ExprConverter { drop(self.current_name.data.pop()) } + // This hack provides prod types for Makam + fn record_prod(&mut self, number: usize) { + let paths = (0..number) + .map(|n| { + let mut path = self.current_path.clone(); + path.data.push(PathSegment::Pos(n)); + Ranged::new(RawExpr::Path(path)) + }) + .collect(); + + let prod = RawExpr::Apply { + head: Ranged::new(":prod".into()), + body: paths, + }; + + self.table.rows.push(TypeRow { + ty: Ranged::new(prod), + path: self.current_path.clone(), + }) + } + fn visit_list(&mut self, list: &[Ranged]) { let mut num = 0; for e in list { @@ -248,6 +278,8 @@ impl ExprConverter { num += 1 } + + self.record_prod(num) } fn visit_data(&mut self, data: &Ranged, num: Option) { diff --git a/src/report.rs b/src/report.rs index eb2eda3..9e24574 100644 --- a/src/report.rs +++ b/src/report.rs @@ -34,7 +34,6 @@ fn paragraph_indices( .unwrap_or(newlines.len() - 1); (ls + 2, from + 1, to) - } #[derive(Debug, Clone, PartialEq)] @@ -53,6 +52,15 @@ pub struct Source { file_name: String, } +impl Source { + fn span_range(&self, span: Span) -> (usize, usize) { + ( + span.from - self.content_start, + span.to - self.content_start, + ) + } +} + #[derive(Debug, Clone, PartialEq, Default)] pub struct Sourcer { files: Vec @@ -97,6 +105,34 @@ impl Sourcer { } } +fn basic_error(source: Source, span: Span, label: &str) -> Snippet { + let range = source.span_range(span); + + Snippet { + title: Some(Annotation { + annotation_type: AnnotationType::Error, + label: Some(label.to_owned()), + id: None, + }), + footer: vec![], + slices: vec![ + Slice { + source: source.content, + line_start: source.line_start, + origin: Some(source.file_name), + fold: false, + annotations: vec![ + SourceAnnotation { + label: "".to_owned(), + annotation_type: AnnotationType::Error, + range, + } + ] + } + ], + } +} + pub trait ToSnippet { fn to_snippet(&self, sourcer: &Sourcer) -> Snippet; fn file_id(&self) -> usize; @@ -109,49 +145,51 @@ impl ToSnippet for crate::path::NameResolveError { match self { NotFound(loc) => { let source = sourcer.source(*loc).unwrap(); - let range = ( - loc.span.from - source.content_start, - loc.span.to - source.content_start, - ); - Snippet { - title: Some(Annotation { - annotation_type: AnnotationType::Error, - label: Some("unknown reference".to_owned()), - id: None, - }), - footer: vec![], - slices: vec![ - Slice { - source: source.content, - line_start: source.line_start, - origin: Some(source.file_name), - fold: false, - annotations: vec![ - SourceAnnotation { - label: "".to_owned(), - annotation_type: AnnotationType::Error, - range, - } - ] - } - ], - } + basic_error(source, loc.span, "unknown reference") }, InvalidName(loc) => { let source = sourcer.source(*loc).unwrap(); - let range = ( - loc.span.from - source.content_start, - loc.span.to - source.content_start, - ); + + basic_error(source, loc.span, "invalid name") + }, + } + } + + fn file_id(&self) -> usize { + use crate::path::NameResolveError::*; + match self { + NotFound(loc) | InvalidName(loc) => + loc.file_id + } + } +} + +impl ToSnippet for crate::types::ExprToTypeError { + fn to_snippet(&self, sourcer: &Sourcer) -> Snippet { + use crate::types::ExprToTypeError::*; + + match self { + InvalidArity { name, expected, actual, location } => { + let source = sourcer.source(*location).unwrap(); + let range = source.span_range(location.span); Snippet { title: Some(Annotation { annotation_type: AnnotationType::Error, - label: Some("invalid name".to_owned()), + label: Some("invalid arity".to_owned()), id: None, }), - footer: vec![], + footer: vec![ + Annotation { + label: Some(format!( + "`{}` takes {} arguments, but {} were passed", + name, expected, actual + )), + id: None, + annotation_type: AnnotationType::Note + } + ], slices: vec![ Slice { source: source.content, @@ -169,13 +207,45 @@ impl ToSnippet for crate::path::NameResolveError { ], } }, + InvalidType(loc) => { + let source = sourcer.source(*loc).unwrap(); + + basic_error(source, loc.span, "invalid type") + }, + InvalidSize(loc) => { + let source = sourcer.source(*loc).unwrap(); + + basic_error(source, loc.span, "invalid size") + }, + InvalidRel(loc) => { + let source = sourcer.source(*loc).unwrap(); + + basic_error(source, loc.span, "invalid relation") + }, + InvalidRelExpr(loc) => { + let source = sourcer.source(*loc).unwrap(); + + basic_error(source, loc.span, "invalid expression in relation") + }, + UnsupportedList(loc) => { + let source = sourcer.source(*loc).unwrap(); + + basic_error(source, loc.span, "lists inside types are unsupported") + }, } } fn file_id(&self) -> usize { - use crate::path::NameResolveError::*; + use crate::types::ExprToTypeError::*; + match self { - NotFound(loc) | InvalidName(loc) => + InvalidArity { location, .. } => + location.file_id, + InvalidType(loc) + | InvalidSize(loc) + | InvalidRel(loc) + | InvalidRelExpr(loc) + | UnsupportedList(loc) => loc.file_id } } diff --git a/src/types.rs b/src/types.rs new file mode 100644 index 0000000..c261e41 --- /dev/null +++ b/src/types.rs @@ -0,0 +1,706 @@ +use smol_str::SmolStr; + +use crate::expr::Location; +use crate::path::TypeRow; +use crate::expr::RawExpr; +use crate::expr::Ranged; +use crate::path::PathTable; +use crate::path::RzPath; + +#[derive(Debug, Clone, Copy, PartialEq)] +pub enum Endianness { + Le, + Be, +} + +#[derive(Debug, Clone, PartialEq)] +pub enum TypeExpr { + Top, + Bottom, + + Bool, + + Int, + U(usize, Endianness), + S(usize, Endianness), + + Arr(Box>, Ranged), + Str(Ranged), + + And(Vec>), + Or(Vec>), + + Prod(Vec), + Ref(RzPath), + + Liq(Box, Vec>), + Val(Value, Box), +} + +#[derive(Debug, Clone, PartialEq)] +pub struct Size { + rels: Vec> +} + +#[derive(Debug, Clone, PartialEq)] +pub enum Rel { + Lt(Ranged, Ranged), + Le(Ranged, Ranged), + Eq(Ranged, Ranged), + Ge(Ranged, Ranged), + Gt(Ranged, Ranged), +} + + + +#[derive(Debug, Clone, PartialEq)] +pub enum RelExpr { + Hole, + Sizeof, + Integer(SmolStr), + Ref(RzPath), + Size(Size), +} + +#[derive(Debug, Clone, PartialEq)] +pub enum Value { + Boolean(bool), + Integer(SmolStr), +} + +fn is_rel_name(name: &str) -> bool { + ["lt", "le", "eq", "ge", "gt"] + .contains(&name) +} + +fn as_rel_expr(expr: &Ranged) -> Result, ExprToTypeError> { + let pred_expr = + match &expr.data { + RawExpr::Decimal(num) | RawExpr::Hexdecimal(num) => + RelExpr::Integer(num.clone()), + RawExpr::Name(n) if n == "_" => + RelExpr::Hole, + RawExpr::Apply { head, body } if head.data == "sizeof" => { + if body.get(0).map(|e| &e.data) == Some(&RawExpr::Name("_".into())) { + RelExpr::Sizeof + } + else { + return Err(ExprToTypeError::InvalidRelExpr(expr.range.unwrap())) + } + }, + RawExpr::Path(path) => + RelExpr::Ref(path.clone()), + _ => return Err(ExprToTypeError::InvalidRelExpr(expr.range.unwrap())), + }; + + Ok(Ranged { + data: pred_expr, + range: expr.range + }) +} + +fn as_rel(expr: &Ranged) -> Result, ExprToTypeError> { + match &expr.data { + RawExpr::Apply { head, body } if is_rel_name(&head.data) => { + let (left, right) = body.get(0..2) + .map(|p| (&p[0], &p[1])) + .ok_or(ExprToTypeError::InvalidRel(expr.range.unwrap()))?; + if body.len() > 2 { + return Err(ExprToTypeError::InvalidRel(expr.range.unwrap())) + } + + let left = as_rel_expr(left)?; + let right = as_rel_expr(right)?; + + let cons = + match &*head.data { + "lt" => Rel::Lt, + "le" => Rel::Le, + "eq" => Rel::Eq, + "ge" => Rel::Ge, + "gt" => Rel::Gt, + _ => unreachable!() + }; + + let pred = Ranged { + data: cons(left, right), + range: expr.range, + }; + + Ok(pred) + }, + _ => Err(ExprToTypeError::InvalidRel(expr.range.unwrap())) + } +} + +fn as_rel_list(expr: &Ranged) -> Result>, ExprToTypeError> { + match &expr.data { + RawExpr::Apply { head, body } if head.data == "and" => { + body.iter() + .map(as_rel) + .collect() + }, + _ => as_rel(expr).map(|r| vec![r]) + } +} + +fn as_size(expr: &Ranged) -> Result, ExprToTypeError> { + let mut rels = vec![]; + match &expr.data { + RawExpr::Name(n) if n == "_" => (), + RawExpr::Decimal(num) + | RawExpr::Hexdecimal(num) => + rels.push( + Ranged { + data: Rel::Eq( + Ranged::new(RelExpr::Hole), + Ranged { + data: RelExpr::Integer(num.clone()), + range: expr.range, + } + ), + range: expr.range + } + ), + RawExpr::Path(path) => + rels.push(Ranged { + data: Rel::Eq( + Ranged::new(RelExpr::Hole), + Ranged { + data: RelExpr::Ref(path.clone()), + range: expr.range + } + ), + range: expr.range + }), + RawExpr::Apply { head, body } if head.data == "and" => { + for e in body { + let sz = as_size(e)?; + rels.extend(sz.data.rels); + } + }, + RawExpr::Apply { head, .. } if is_rel_name(&head.data) => { + let rel = as_rel(expr)?; + rels.push(rel) + }, + _ => return Err(ExprToTypeError::InvalidSize(expr.range.unwrap())), + } + + Ok(Ranged { + data: Size { rels }, + range: expr.range, + }) +} + +fn as_simple_type(expr: &Ranged) -> Option> { + use Endianness::*; + + let ty = + match &expr.data { + RawExpr::Name(n) if n == "_" => + TypeExpr::Top, + RawExpr::Name(n) if n == "never" => + TypeExpr::Bottom, + + RawExpr::Name(n) if n == "bool" => + TypeExpr::Bool, + RawExpr::Name(n) if n == "true" => + TypeExpr::Val( + Value::Boolean(true), + Box::new(TypeExpr::Bool) + ), + RawExpr::Name(n) if n == "false" => + TypeExpr::Val( + Value::Boolean(false), + Box::new(TypeExpr::Bool) + ), + + RawExpr::Name(n) if n == "int" => + TypeExpr::Int, + + RawExpr::Name(n) if n == "u1" => + TypeExpr::U(1, Be), + RawExpr::Name(n) if n == "u2" => + TypeExpr::U(2, Be), + RawExpr::Name(n) if n == "u4" => + TypeExpr::U(4, Be), + RawExpr::Name(n) if n == "u8" => + TypeExpr::U(8, Be), + RawExpr::Name(n) if n == "u2le" => + TypeExpr::U(2, Le), + RawExpr::Name(n) if n == "u4le" => + TypeExpr::U(4, Le), + RawExpr::Name(n) if n == "u8le" => + TypeExpr::U(8, Le), + + RawExpr::Name(n) if n == "s1" => + TypeExpr::S(1, Be), + RawExpr::Name(n) if n == "s2" => + TypeExpr::S(2, Be), + RawExpr::Name(n) if n == "s4" => + TypeExpr::S(4, Be), + RawExpr::Name(n) if n == "s8" => + TypeExpr::S(8, Be), + RawExpr::Name(n) if n == "s2le" => + TypeExpr::S(2, Le), + RawExpr::Name(n) if n == "s4le" => + TypeExpr::S(4, Le), + RawExpr::Name(n) if n == "s8le" => + TypeExpr::S(8, Le), + + RawExpr::Decimal(s) | RawExpr::Hexdecimal(s) => + TypeExpr::Val( + Value::Integer(s.clone()), + Box::new(TypeExpr::Int) + ), + _ => return None, + }; + + Some(Ranged { + data: ty, + range: expr.range, + }) +} + +#[derive(Clone, Copy, Debug, PartialEq,)] +pub enum ExprToTypeError { + InvalidType(Location), + InvalidArity { + name: &'static str, + expected: usize, + actual: usize, + location: Location, + }, + InvalidSize(Location), + InvalidRel(Location), + InvalidRelExpr(Location), + UnsupportedList(Location), +} + +#[derive(Clone, Default)] +pub struct ExprToType { + errors: Vec +} + +impl ExprToType { + pub fn new() -> Self { + Default::default() + } + + fn push_err(&mut self, res: Result) -> Result { + res.map_err(|e| self.errors.push(e)) + } + + pub fn into_types( + mut self, + table: PathTable> + ) -> Result>, Vec> { + let PathTable { rows, names, defs } = table; + let rows = rows.into_iter() + .filter_map(|TypeRow { path, ty }| + self.as_type(&ty).map(|ty| TypeRow { path, ty }) + ) + .collect(); + + if self.errors.is_empty() { + Ok(PathTable { rows, names, defs }) + } + else { + Err(self.errors) + } + } + + fn as_type(&mut self, expr: &Ranged) -> Option> { + if let Some(simple) = as_simple_type(expr) { + return Some(simple) + } + + let ty = + match &expr.data { + RawExpr::Apply { head, .. } if is_rel_name(&head.data) => { + let rels = self.push_err(as_rel_list(expr)).ok()?; + + TypeExpr::Liq(Box::new(TypeExpr::Top), rels) + }, + RawExpr::Apply { head, body } if &head.data == "and" => { + let types = body.iter() + .filter_map(|e| self.as_type(e)) + .collect(); + + TypeExpr::And(types) + } + RawExpr::Apply { head, body } if &head.data == "or" => { + let types = body.iter() + .filter_map(|e| self.as_type(e)) + .collect(); + + TypeExpr::Or(types) + } + RawExpr::Apply { head, body } if &head.data == "arr" => { + if body.len() != 2 { + self.errors.push( + ExprToTypeError::InvalidArity { + name: "arr", + expected: 2, + actual: body.len(), + location: expr.range.unwrap() + } + ); + return None + } + + let (ty, num) = (&body[0], &body[1]); + let ty = Box::new(self.as_type(ty)?); + let num = self.push_err(as_size(num)).ok()?; + + TypeExpr::Arr(ty, num) + }, + RawExpr::Apply { head, body } if &head.data == "str" => { + if body.len() != 1 { + self.errors.push( + ExprToTypeError::InvalidArity { + name: "str", + expected: 1, + actual: body.len(), + location: expr.range.unwrap() + } + ); + return None + } + + let num = self.push_err(as_size(&body[0])).ok()?; + + TypeExpr::Str(num) + }, + RawExpr::Apply { head, body } if &head.data == "bytes" => { + if body.len() != 1 { + self.errors.push( + ExprToTypeError::InvalidArity { + name: "bytes", + expected: 1, + actual: body.len(), + location: expr.range.unwrap() + } + ); + return None + } + + let num = self.push_err(as_size(&body[0])).ok()?; + + TypeExpr::Arr( + Box::new(Ranged::new(TypeExpr::U(1, Endianness::Be))), + num + ) + }, + RawExpr::Apply { head, body } if &head.data == "size" => { + if body.len() != 1 { + self.errors.push( + ExprToTypeError::InvalidArity { + name: "size", + expected: 1, + actual: body.len(), + location: expr.range.unwrap() + } + ); + return None + } + + let size = self.push_err(as_size(&body[0])).ok()?; + let rel_size = Ranged { + data: RelExpr::Size(size.data), + range: size.range + }; + + TypeExpr::Liq( + Box::new(TypeExpr::Top), + vec![Ranged::new( + Rel::Eq( + Ranged::new(RelExpr::Sizeof), + rel_size + ) + )] + ) + }, + RawExpr::Apply { head, body } if &head.data == ":prod" => { + let mut paths = vec![]; + for e in body { + match &e.data { + RawExpr::Path(path) => + paths.push(path.clone()), + _ => unreachable!(), + } + } + + TypeExpr::Prod(paths) + } + RawExpr::Path(path) => + TypeExpr::Ref(path.clone()), + RawExpr::List(_) => { + self.errors.push( + ExprToTypeError::UnsupportedList(expr.range.unwrap()) + ); + + return None + }, + _ => { + self.errors.push( + ExprToTypeError::InvalidType(expr.range.unwrap()) + ); + + return None + } + }; + + Some(Ranged { + data: ty, + range: expr.range + }) + } +} + +pub fn as_makam_ty(ty: &TypeExpr) -> String { + use TypeExpr::*; + + match ty { + Top => "top".to_owned(), + Bottom => "bottom".to_owned(), + Bool => "boolean".to_owned(), + Int => "integer".to_owned(), + U(s, Endianness::Be) => + format!("u({}, big_endian)", s), + U(s, Endianness::Le) => + format!("u({}, little_endian)", s), + S(s, Endianness::Be) => + format!("s({}, big_endian)", s), + S(s, Endianness::Le) => + format!("s({}, little_endian)", s), + Arr(ty, num) => { + let ty = as_makam_ty(&ty.data); + let num = as_makam_size(&num.data); + + format!("arr({}, {})", ty, num) + }, + Str(len) => { + let len = as_makam_size(&len.data); + + format!("str({})", len) + }, + And(list) => { + let list = list.iter() + .map(|ty| as_makam_ty(&ty.data)) + .collect::>() + .join(", "); + format!("meet([{}])", list) + }, + Or(list) => { + let list = list.iter() + .map(|ty| as_makam_ty(&ty.data)) + .collect::>() + .join(", "); + format!("join([{}])", list) + }, + Ref(path) => { + let path = as_makam_path(&path); + + format!("ref({})", path) + }, + Prod(paths) => { + let paths = paths.iter() + .map(|path| as_makam_path(&path)) + .collect::>() + .join(", "); + + format!("prod([{}])", paths) + }, + Liq(ty, rels) => { + let ty = as_makam_ty(ty); + let rels = rels.iter() + .map(|p| as_makam_rel(&p.data)) + .collect::>() + .join(", "); + + format!("{} ⋮ [{}]", ty, rels) + }, + Val(value, ty) => { + let value = as_makam_value(value); + let ty = as_makam_ty(ty); + + format!("{} ∈ {}", value, ty) + }, + } +} + +pub fn as_makam_path(path: &RzPath) -> String { + let modules = path.modules.iter() + .map(|m| format!("\"{}\"", m)) + .collect::>() + .join(", "); + let data = path.data.iter() + .map(|m| format!("\"{}\"", m)) + .collect::>() + .join(", "); + + format!("path([{}], [{}])", modules, data) +} + +pub fn as_makam_size(size: &Size) -> String { + let rels = size.rels.iter() + .map(|r| as_makam_rel(&r.data)) + .collect::>() + .join(", "); + + format!("[{}]", rels) +} + +pub fn as_makam_value(value: &Value) -> String { + match value { + Value::Boolean(b) => + format!("vbool({})", b), + Value::Integer(i) => + format!("vint({})", i) + } +} + +pub fn as_makam_rel_expr(expr: &RelExpr) -> String { + match expr { + RelExpr::Hole => "hole".to_owned(), + RelExpr::Sizeof => "sizeof".to_owned(), + RelExpr::Integer(i) => + format!("rint({})", i), + RelExpr::Ref(path) => + format!("ref({})", as_makam_path(&path)), + RelExpr::Size(sz) => + format!("size({})", as_makam_size(&sz)), + } +} + +pub fn as_makam_rel(rel: &Rel) -> String { + match rel { + Rel::Lt(left, right) => { + let left = as_makam_rel_expr(&left.data); + let right = as_makam_rel_expr(&right.data); + + format!("{} < {}", left, right) + } + Rel::Le(left, right) => { + let left = as_makam_rel_expr(&left.data); + let right = as_makam_rel_expr(&right.data); + + format!("{} ≤ {}", left, right) + } + Rel::Eq(left, right) => { + let left = as_makam_rel_expr(&left.data); + let right = as_makam_rel_expr(&right.data); + + format!("{} = {}", left, right) + } + Rel::Ge(left, right) => { + let left = as_makam_rel_expr(&left.data); + let right = as_makam_rel_expr(&right.data); + + format!("{} ≥ {}", left, right) + } + Rel::Gt(left, right) => { + let left = as_makam_rel_expr(&left.data); + let right = as_makam_rel_expr(&right.data); + + format!("{} > {}", left, right) + } + } +} + +// pub enum SimpifyError { +// InnerJoin(Location, Option), +// } + +// #[derive(Debug, Clone, PartialEq)] +// pub struct Simplifier { +// } + +// impl Simplifier { +// pub fn simpify(&mut self, ty: &mut Ranged) -> Result<(), ()> { +// todo!() +// } + +// fn meet(left: &Ranged, right: &Ranged) -> Result, SimpifyError> { +// use TypeExpr::*; + +// match (left, right) { +// ( +// Ranged { data: Or(_), range: join_range }, +// Ranged { range, .. } +// ) +// | ( +// Ranged { range, .. }, +// Ranged { data: Or(_), range: join_range } +// ) => +// return Err(SimpifyError::InnerJoin(join_range.unwrap(), *range)), +// _ => () +// } + +// let ty = +// match (&left.data, &right.data) { +// (Top, e) | (e, Top) => +// e.clone(), +// (Bottom, _) | (_, Bottom) => +// Bottom, + +// (Bool, Bool) => +// Bool, + +// (U(s, e), U(s2, e2)) +// if s == s2 && e == e2 => +// U(*s, *e), +// (S(s, e), S(s2, e2)) +// if s == s2 && e == e2 => +// S(*s, *e), +// (Int, U(s, e)) | (U(s, e), Int) => +// U(*s, *e), +// (Int, S(s, e)) | (S(s, e), Int) => +// S(*s, *e), +// (Int, Int) => +// Int, + +// // (Arr(ty1, num1), Arr(ty2, num2)) => { +// // let ty = Simplifier::meet(&ty1, &ty2)?; +// // let num = Simplifier::meet(&num1, &num2)?; + +// // Arr(Box::new(ty), Box::new(num)) +// // }, +// // (Str(num1), Str(num2)) => { +// // let num = Simplifier::meet(&num1, &num2)?; + +// // Str(Box::new(num)) +// // }, + +// // (Liq(ty1, pred1), Liq(ty2, pred2)) => { +// // todo!() +// // }, +// // (Liq(ty1, pred), Val(v, ty2)) | (Val(v, ty2), Liq(ty1, pred)) => { +// // todo!() +// // }, +// // (Liq(ty1, pred), ty2) => { +// // todo!() +// // }, + +// // (Val(v1, ty1), Val(v2, ty2)) => { +// // todo!() +// // }, +// // (Val(v, ty1), ty2) | (ty2, Val(v, ty1)) => { +// // todo!() +// // }, +// // (And(tys1), And(tys2)) => { +// // todo!() +// // }, +// // (And(tys), ty) | (ty, And(tys)) => { +// // todo!() +// // }, +// _ => Bottom, +// }; + +// Ok(Ranged { +// data: ty, +// range: None, +// }) +// } +// } diff --git a/tests/spec/mod.rs b/tests/spec/mod.rs index d00239c..5f7dce7 100644 --- a/tests/spec/mod.rs +++ b/tests/spec/mod.rs @@ -1 +1,2 @@ mod should_succeed; +mod should_fail; diff --git a/tests/spec/should_fail.rs b/tests/spec/should_fail.rs index f4d0c93..1830711 100644 --- a/tests/spec/should_fail.rs +++ b/tests/spec/should_fail.rs @@ -1,3 +1,5 @@ +use razbor::expr::ExprLoader; + const SPEC_DIR: &'static str = concat!(env!("CARGO_MANIFEST_DIR"), "/tests/spec");