Merge remote-tracking branch 'origin/main' into inspect-builtin

This commit is contained in:
Richard Feldman 2023-08-14 14:59:15 -04:00
commit 15a6bc34f4
No known key found for this signature in database
GPG key ID: F1F21AA5B1D9E43B
183 changed files with 1793 additions and 1694 deletions

View file

@ -1,7 +1,7 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
F a : a | a has Hash
F a : a where a implements Hash
main : F a -> F a
#^^^^{-1} a -[[main(0)]]-> a | a has Hash
#^^^^{-1} a -[[main(0)]]-> a where a implements Hash

View file

@ -1,7 +1,7 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
F a : a | a has Hash & Eq & Decoding
F a : a where a implements Hash & Eq & Decoding
main : F a -> F a
#^^^^{-1} a -[[main(0)]]-> a | a has Hash & Decoding & Eq
#^^^^{-1} a -[[main(0)]]-> a where a implements Hash & Decoding & Eq

View file

@ -1,8 +1,8 @@
app "test" provides [main] to "./platform"
f : x -> x | x has Hash
g : x -> x | x has Decoding & Encoding
f : x -> x where x implements Hash
g : x -> x where x implements Decoding & Encoding
main : x -> x | x has Hash & Decoding & Encoding
main : x -> x where x implements Hash & Decoding & Encoding
main = \x -> x |> f |> g
#^^^^{-1} x -[[main(0)]]-> x | x has Hash & Encoding & Decoding
#^^^^{-1} x -[[main(0)]]-> x where x implements Hash & Encoding & Decoding

View file

@ -1,6 +1,6 @@
app "test" provides [top] to "./platform"
MDict u := (List u) | u has Hash & Eq
MDict u := (List u) where u implements Hash & Eq
bot : MDict k -> MDict k
bot = \@MDict data ->
@ -9,4 +9,4 @@ bot = \@MDict data ->
top : MDict v -> MDict v
top = \x -> bot x
#^^^{-1} MDict v -[[top(0)]]-> MDict v | v has Hash & Eq
#^^^{-1} MDict v -[[top(0)]]-> MDict v where v implements Hash & Eq

View file

@ -1,6 +1,6 @@
app "test" provides [isEqQ] to "./platform"
Q := [ F (Str -> Str), G ] has [Eq { isEq: isEqQ }]
Q := [ F (Str -> Str), G ] implements [Eq { isEq: isEqQ }]
isEqQ = \@Q q1, @Q q2 -> when T q1 q2 is
#^^^^^{-1} Q, Q -[[isEqQ(0)]]-> Bool

View file

@ -1,7 +1,7 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
Q := ({} -> Str) has [Eq {isEq: isEqQ}]
Q := ({} -> Str) implements [Eq {isEq: isEqQ}]
isEqQ = \@Q f1, @Q f2 -> (f1 {} == f2 {})
#^^^^^{-1} ({} -[[]]-> Str), ({} -[[]]-> Str) -[[isEqQ(2)]]-> [False, True]

View file

@ -2,19 +2,19 @@ app "test" provides [myU8] to "./platform"
MDecodeError : [TooShort, Leftover (List U8)]
MDecoder val fmt := List U8, fmt -> { result: Result val MDecodeError, rest: List U8 } | fmt has MDecoderFormatting
MDecoder val fmt := List U8, fmt -> { result: Result val MDecodeError, rest: List U8 } where fmt implements MDecoderFormatting
MDecoding has
decoder : MDecoder val fmt | val has MDecoding, fmt has MDecoderFormatting
MDecoding implements
decoder : MDecoder val fmt where val implements MDecoding, fmt implements MDecoderFormatting
MDecoderFormatting has
u8 : MDecoder U8 fmt | fmt has MDecoderFormatting
MDecoderFormatting implements
u8 : MDecoder U8 fmt where fmt implements MDecoderFormatting
decodeWith : List U8, MDecoder val fmt, fmt -> { result: Result val MDecodeError, rest: List U8 } | fmt has MDecoderFormatting
decodeWith : List U8, MDecoder val fmt, fmt -> { result: Result val MDecodeError, rest: List U8 } where fmt implements MDecoderFormatting
decodeWith = \lst, (@MDecoder doDecode), fmt -> doDecode lst fmt
fromBytes : List U8, fmt -> Result val MDecodeError
| fmt has MDecoderFormatting, val has MDecoding
where fmt implements MDecoderFormatting, val implements MDecoding
fromBytes = \lst, fmt ->
when decodeWith lst decoder fmt is
{ result, rest } ->
@ -23,7 +23,7 @@ fromBytes = \lst, fmt ->
Err e -> Err e
Linear := {} has [MDecoderFormatting {u8}]
Linear := {} implements [MDecoderFormatting {u8}]
u8 = @MDecoder \lst, @Linear {} ->
#^^{-1} Linear#u8(11): MDecoder U8 Linear
@ -31,10 +31,10 @@ u8 = @MDecoder \lst, @Linear {} ->
Ok n -> { result: Ok n, rest: List.dropFirst lst }
Err _ -> { result: Err TooShort, rest: [] }
MyU8 := U8 has [MDecoding {decoder}]
MyU8 := U8 implements [MDecoding {decoder}]
decoder = @MDecoder \lst, fmt ->
#^^^^^^^{-1} MyU8#decoder(12): MDecoder MyU8 fmt | fmt has MDecoderFormatting
#^^^^^^^{-1} MyU8#decoder(12): MDecoder MyU8 fmt where fmt implements MDecoderFormatting
when decodeWith lst u8 fmt is
{ result, rest } ->
{ result: Result.map result (\n -> @MyU8 n), rest }

View file

@ -1,29 +1,29 @@
app "test" provides [myU8Bytes] to "./platform"
MEncoder fmt := List U8, fmt -> List U8 | fmt has Format
MEncoder fmt := List U8, fmt -> List U8 where fmt implements Format
MEncoding has
toEncoder : val -> MEncoder fmt | val has MEncoding, fmt has Format
MEncoding implements
toEncoder : val -> MEncoder fmt where val implements MEncoding, fmt implements Format
Format has
u8 : U8 -> MEncoder fmt | fmt has Format
Format implements
u8 : U8 -> MEncoder fmt where fmt implements Format
appendWith : List U8, MEncoder fmt, fmt -> List U8 | fmt has Format
appendWith : List U8, MEncoder fmt, fmt -> List U8 where fmt implements Format
appendWith = \lst, (@MEncoder doFormat), fmt -> doFormat lst fmt
toBytes : val, fmt -> List U8 | val has MEncoding, fmt has Format
toBytes : val, fmt -> List U8 where val implements MEncoding, fmt implements Format
toBytes = \val, fmt -> appendWith [] (toEncoder val) fmt
Linear := {} has [Format {u8}]
Linear := {} implements [Format {u8}]
u8 = \n -> @MEncoder (\lst, @Linear {} -> List.append lst n)
#^^{-1} Linear#u8(10): U8 -[[u8(10)]]-> MEncoder Linear
MyU8 := U8 has [MEncoding {toEncoder}]
MyU8 := U8 implements [MEncoding {toEncoder}]
toEncoder = \@MyU8 n -> u8 n
#^^^^^^^^^{-1} MyU8#toEncoder(11): MyU8 -[[toEncoder(11)]]-> MEncoder fmt | fmt has Format
#^^^^^^^^^{-1} MyU8#toEncoder(11): MyU8 -[[toEncoder(11)]]-> MEncoder fmt where fmt implements Format
myU8Bytes = toBytes (@MyU8 15) (@Linear {})
#^^^^^^^^^{-1} List U8

View file

@ -3,4 +3,4 @@ app "test" provides [main] to "./platform"
main : Decoder Bool _
main = Decode.custom \bytes, fmt ->
Decode.decodeWith bytes Decode.decoder fmt
# ^^^^^^^^^^^^^^ Decoding#Decode.decoder(4): Decoder Bool fmt | fmt has DecoderFormatting
# ^^^^^^^^^^^^^^ Decoding#Decode.decoder(4): Decoder Bool fmt where fmt implements DecoderFormatting

View file

@ -2,4 +2,4 @@ app "test" provides [main] to "./platform"
main =
\h -> Hash.hash h Bool.true
# ^^^^^^^^^ Hash#Hash.hash(1): a, Bool -[[Hash.hashBool(9)]]-> a | a has Hasher
# ^^^^^^^^^ Hash#Hash.hash(1): a, Bool -[[Hash.hashBool(9)]]-> a where a implements Hasher

View file

@ -1,4 +1,4 @@
app "test" provides [main] to "./platform"
main = Encode.toEncoder Bool.true
# ^^^^^^^^^^^^^^^^ Encoding#Encode.toEncoder(2): Bool -[[] + fmt:Encode.bool(17):1]-> Encoder fmt | fmt has EncoderFormatting
# ^^^^^^^^^^^^^^^^ Encoding#Encode.toEncoder(2): Bool -[[] + fmt:Encode.bool(17):1]-> Encoder fmt where fmt implements EncoderFormatting

View file

@ -2,4 +2,4 @@ app "test" provides [main] to "./platform"
main =
\h -> Hash.hash h 1.1dec
# ^^^^^^^^^ Hash#Hash.hash(1): a, Dec -[[Hash.hashDec(17)]]-> a | a has Hasher
# ^^^^^^^^^ Hash#Hash.hash(1): a, Dec -[[Hash.hashDec(17)]]-> a where a implements Hasher

View file

@ -1,9 +1,9 @@
# +opt infer:print_only_under_alias
app "test" provides [main] to "./platform"
N := U8 has [Decoding]
N := U8 implements [Decoding]
main : Decoder N _
main = Decode.custom \bytes, fmt ->
Decode.decodeWith bytes Decode.decoder fmt
# ^^^^^^^^^^^^^^ N#Decode.decoder(3): List U8, fmt -[[7]]-> { rest : List U8, result : [Err [TooShort], Ok U8] } | fmt has DecoderFormatting
# ^^^^^^^^^^^^^^ N#Decode.decoder(3): List U8, fmt -[[7]]-> { rest : List U8, result : [Err [TooShort], Ok U8] } where fmt implements DecoderFormatting

View file

@ -1,6 +1,6 @@
app "test" provides [main] to "./platform"
N := U8 has [Encoding]
N := U8 implements [Encoding]
main = Encode.toEncoder (@N 15)
# ^^^^^^^^^^^^^^^^ N#Encode.toEncoder(3): N -[[#N_toEncoder(3)]]-> Encoder fmt | fmt has EncoderFormatting
# ^^^^^^^^^^^^^^^^ N#Encode.toEncoder(3): N -[[#N_toEncoder(3)]]-> Encoder fmt where fmt implements EncoderFormatting

View file

@ -1,6 +1,6 @@
app "test" provides [main] to "./platform"
Trivial := {} has [Eq {isEq}]
Trivial := {} implements [Eq {isEq}]
isEq = \@Trivial {}, @Trivial {} -> Bool.true

View file

@ -1,6 +1,6 @@
app "test" provides [main] to "./platform"
N := U8 has [Eq]
N := U8 implements [Eq]
main = Bool.isEq (@N 15) (@N 23)
# ^^^^^^^^^ N#Bool.isEq(3): N, N -[[#N_isEq(3)]]-> Bool

View file

@ -1,8 +1,8 @@
app "test" provides [main] to "./platform"
Noop := {} has [Hash {hash}]
Noop := {} implements [Hash {hash}]
hash = \hasher, @Noop {} -> hasher
main = \hasher -> hash hasher (@Noop {})
#^^^^{-1} hasher -[[main(0)]]-> hasher | hasher has Hasher
#^^^^{-1} hasher -[[main(0)]]-> hasher where hasher implements Hasher

View file

@ -1,6 +1,6 @@
app "test" provides [main] to "./platform"
N := U8 has [Hash]
N := U8 implements [Hash]
main = \hasher, @N n -> Hash.hash hasher (@N n)
# ^^^^^^^^^ N#Hash.hash(3): a, N -[[#N_hash(3)]]-> a | a has Hasher
# ^^^^^^^^^ N#Hash.hash(3): a, N -[[#N_hash(3)]]-> a where a implements Hasher

View file

@ -1,13 +1,13 @@
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
F implements f : a -> (b -> {}) where a implements F, b implements G
G implements g : b -> {} where b implements G
Fo := {} has [F {f}]
Fo := {} implements [F {f}]
f = \@Fo {} -> g
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) where b implements G
Go := {} has [G {g}]
Go := {} implements [G {g}]
g = \@Go {} -> {}
#^{-1} Go#g(8): Go -[[g(8)]]-> {}

View file

@ -1,13 +1,13 @@
app "test" provides [main] to "./platform"
F has f : a -> ({} -> b) | a has F, b has G
G has g : {} -> b | b has G
F implements f : a -> ({} -> b) where a implements F, b implements G
G implements g : {} -> b where b implements G
Fo := {} has [F {f}]
Fo := {} implements [F {f}]
f = \@Fo {} -> g
#^{-1} Fo#f(7): Fo -[[f(7)]]-> ({} -[[] + b:g(4):1]-> b) | b has G
#^{-1} Fo#f(7): Fo -[[f(7)]]-> ({} -[[] + b:g(4):1]-> b) where b implements G
Go := {} has [G {g}]
Go := {} implements [G {g}]
g = \{} -> @Go {}
#^{-1} Go#g(8): {} -[[g(8)]]-> Go

View file

@ -1,15 +1,15 @@
app "test" provides [f] to "./platform"
J has j : j -> (k -> {}) | j has J, k has K
K has k : k -> {} | k has K
J implements j : j -> (k -> {}) where j implements J, k implements K
K implements k : k -> {} where k implements K
C := {} has [J {j: jC}]
C := {} implements [J {j: jC}]
jC = \@C _ -> k
D := {} has [J {j: jD}]
D := {} implements [J {j: jD}]
jD = \@D _ -> k
E := {} has [K {k}]
E := {} implements [K {k}]
k = \@E _ -> {}
f = \flag, a, c ->
@ -18,5 +18,5 @@ f = \flag, a, c ->
A -> j a
B -> j a
it c
# ^ k | k has K
# ^^ k -[[] + j:j(2):2]-> {} | j has J, k has K
# ^ k where k implements K
# ^^ k -[[] + j:j(2):2]-> {} where j implements J, k implements K

View file

@ -1,32 +1,32 @@
app "test" provides [main] to "./platform"
J has j : j -> (k -> {}) | j has J, k has K
K has k : k -> {} | k has K
J implements j : j -> (k -> {}) where j implements J, k implements K
K implements k : k -> {} where k implements K
C := {} has [J {j: jC}]
C := {} implements [J {j: jC}]
jC = \@C _ -> k
#^^{-1} C -[[jC(8)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
#^^{-1} C -[[jC(8)]]-> (k -[[] + k:k(4):1]-> {}) where k implements K
D := {} has [J {j: jD}]
D := {} implements [J {j: jD}]
jD = \@D _ -> k
#^^{-1} D -[[jD(9)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
#^^{-1} D -[[jD(9)]]-> (k -[[] + k:k(4):1]-> {}) where k implements K
E := {} has [K {k}]
E := {} implements [K {k}]
k = \@E _ -> {}
#^{-1} E#k(10): E -[[k(10)]]-> {}
f = \flag, a, b ->
# ^ j | j has J
# ^ j | j has J
# ^ j where j implements J
# ^ j where j implements J
it =
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} where j implements J, j1 implements J, k implements K
when flag is
A -> j a
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j1:j(2):2]-> {}) | j has J, j1 has J, k has K
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j1:j(2):2]-> {}) where j implements J, j1 implements J, k implements K
B -> j b
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j1:j(2):2 + j:j(2):2]-> {}) | j has J, j1 has J, k has K
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j1:j(2):2 + j:j(2):2]-> {}) where j implements J, j1 implements J, k implements K
it
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} where j implements J, j1 implements J, k implements K
main = (f A (@C {}) (@D {})) (@E {})
# ^ [A, B], C, D -[[f(11)]]-> (E -[[k(10)]]-> {})

View file

@ -1,43 +1,43 @@
app "test" provides [main] to "./platform"
J has j : j -> (k -> {}) | j has J, k has K
K has k : k -> {} | k has K
J implements j : j -> (k -> {}) where j implements J, k implements K
K implements k : k -> {} where k implements K
C := {} has [J {j: jC}]
C := {} implements [J {j: jC}]
jC = \@C _ -> k
#^^{-1} C -[[jC(9)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
#^^{-1} C -[[jC(9)]]-> (k -[[] + k:k(4):1]-> {}) where k implements K
D := {} has [J {j: jD}]
D := {} implements [J {j: jD}]
jD = \@D _ -> k
#^^{-1} D -[[jD(10)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
#^^{-1} D -[[jD(10)]]-> (k -[[] + k:k(4):1]-> {}) where k implements K
E := {} has [K {k: kE}]
E := {} implements [K {k: kE}]
kE = \@E _ -> {}
#^^{-1} E -[[kE(11)]]-> {}
F := {} has [K {k: kF}]
F := {} implements [K {k: kF}]
kF = \@F _ -> {}
#^^{-1} F -[[kF(12)]]-> {}
f = \flag, a, b ->
# ^ j | j has J
# ^ j | j has J
# ^ j where j implements J
# ^ j where j implements J
it =
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} where j implements J, j1 implements J, k implements K
when flag is
A -> j a
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j1:j(2):2]-> {}) | j has J, j1 has J, k has K
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j:j(2):2 + j1:j(2):2]-> {}) where j implements J, j1 implements J, k implements K
B -> j b
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j1:j(2):2 + j:j(2):2]-> {}) | j has J, j1 has J, k has K
# ^ J#j(2): j -[[] + j:j(2):1]-> (k -[[] + j1:j(2):2 + j:j(2):2]-> {}) where j implements J, j1 implements J, k implements K
it
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} | j has J, j1 has J, k has K
# ^^ k -[[] + j:j(2):2 + j1:j(2):2]-> {} where j implements J, j1 implements J, k implements K
main =
#^^^^{-1} {}
it = \x ->
# ^^ k -[[it(21)]]-> {} | k has K
# ^^ k -[[it(21)]]-> {} where k implements K
(f A (@C {}) (@D {})) x
# ^ [A, B], C, D -[[f(13)]]-> (k -[[] + k:k(4):1]-> {}) | k has K
# ^ [A, B], C, D -[[f(13)]]-> (k -[[] + k:k(4):1]-> {}) where k implements K
if Bool.true
then it (@E {})
# ^^ E -[[it(21)]]-> {}

View file

@ -1,13 +1,13 @@
app "test" provides [main] to "./platform"
F has f : a, b -> ({} -> ({} -> {})) | a has F, b has G
G has g : b -> ({} -> {}) | b has G
F implements f : a, b -> ({} -> ({} -> {})) where a implements F, b implements G
G implements g : b -> ({} -> {}) where b implements G
Fo := {} has [F {f}]
Fo := {} implements [F {f}]
f = \@Fo {}, b -> \{} -> g b
#^{-1} Fo#f(7): Fo, b -[[f(7)]]-> ({} -[[13 b]]-> ({} -[[] + b:g(4):2]-> {})) | b has G
#^{-1} Fo#f(7): Fo, b -[[f(7)]]-> ({} -[[13 b]]-> ({} -[[] + b:g(4):2]-> {})) where b implements G
Go := {} has [G {g}]
Go := {} implements [G {g}]
g = \@Go {} -> \{} -> {}
#^{-1} Go#g(8): Go -[[g(8)]]-> ({} -[[14]]-> {})

View file

@ -1,13 +1,13 @@
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
F implements f : a -> (b -> {}) where a implements F, b implements G
G implements g : b -> {} where b implements G
Fo := {} has [F {f}]
Fo := {} implements [F {f}]
f = \@Fo {} -> g
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) where b implements G
Go := {} has [G {g}]
Go := {} implements [G {g}]
g = \@Go {} -> {}
#^{-1} Go#g(8): Go -[[g(8)]]-> {}

View file

@ -1,19 +1,19 @@
app "test" provides [main] to "./platform"
F has f : a -> (b -> {}) | a has F, b has G
G has g : b -> {} | b has G
F implements f : a -> (b -> {}) where a implements F, b implements G
G implements g : b -> {} where b implements G
Fo := {} has [F {f}]
Fo := {} implements [F {f}]
f = \@Fo {} -> g
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
#^{-1} Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) where b implements G
Go := {} has [G {g}]
Go := {} implements [G {g}]
g = \@Go {} -> {}
#^{-1} Go#g(8): Go -[[g(8)]]-> {}
main =
#^^^^{-1} b -[[] + b:g(4):1]-> {} | b has G
#^^^^{-1} b -[[] + b:g(4):1]-> {} where b implements G
h = f (@Fo {})
# ^ Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) | b has G
# ^ b -[[] + b:g(4):1]-> {} | b has G
# ^ Fo#f(7): Fo -[[f(7)]]-> (b -[[] + b:g(4):1]-> {}) where b implements G
# ^ b -[[] + b:g(4):1]-> {} where b implements G
h

View file

@ -2,4 +2,4 @@ app "test" provides [main] to "./platform"
main =
\h -> Hash.hash h 7
# ^^^^^^^^^ Hash#Hash.hash(1): a, I64 -[[Hash.hashI64(13)]]-> a | a has Hasher
# ^^^^^^^^^ Hash#Hash.hash(1): a, I64 -[[Hash.hashI64(13)]]-> a where a implements Hasher

View file

@ -3,4 +3,4 @@ app "test"
provides [main] to "./platform"
main = toEncoder { a: "" }
# ^^^^^^^^^ Encoding#toEncoder(2): { a : Str } -[[#Derived.toEncoder_{a}(0)]]-> Encoder fmt | fmt has EncoderFormatting
# ^^^^^^^^^ Encoding#toEncoder(2): { a : Str } -[[#Derived.toEncoder_{a}(0)]]-> Encoder fmt where fmt implements EncoderFormatting

View file

@ -2,8 +2,8 @@ app "test"
imports [Encode.{ toEncoder, custom }]
provides [main] to "./platform"
A := {} has [Encoding {toEncoder}]
A := {} implements [Encoding {toEncoder}]
toEncoder = \@A _ -> custom \b, _ -> b
main = toEncoder { a: @A {} }
# ^^^^^^^^^ Encoding#toEncoder(2): { a : A } -[[#Derived.toEncoder_{a}(0)]]-> Encoder fmt | fmt has EncoderFormatting
# ^^^^^^^^^ Encoding#toEncoder(2): { a : A } -[[#Derived.toEncoder_{a}(0)]]-> Encoder fmt where fmt implements EncoderFormatting

View file

@ -1,9 +1,9 @@
app "test" provides [main] to "./platform"
Id1 has id1 : a -> a | a has Id1
Id2 has id2 : a -> a | a has Id2
Id1 implements id1 : a -> a where a implements Id1
Id2 implements id2 : a -> a where a implements Id2
A := {} has [Id1 {id1}, Id2 {id2}]
A := {} implements [Id1 {id1}, Id2 {id2}]
id1 = \@A {} -> @A {}
#^^^{-1} A#id1(6): A -[[id1(6)]]-> A

View file

@ -1,8 +1,8 @@
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
Id implements id : a -> a where a implements Id
A := {} has [Id {id}]
A := {} implements [Id {id}]
id = \@A {} -> @A {}
#^^{-1} A#id(4): A -[[id(4)]]-> A

View file

@ -1,8 +1,8 @@
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
Id implements id : a -> a where a implements Id
A := {} has [Id {id}]
A := {} implements [Id {id}]
id = \@A {} -> @A {}
#^^{-1} A#id(4): A -[[id(4)]]-> A

View file

@ -1,16 +1,16 @@
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
Id implements id : a -> a where a implements Id
A := {} has [Id {id}]
A := {} implements [Id {id}]
id = \@A {} -> @A {}
#^^{-1} A#id(4): A -[[id(4)]]-> A
main =
alias1 = \x -> id x
# ^^ Id#id(2): a -[[] + a:id(2):1]-> a | a has Id
# ^^ Id#id(2): a -[[] + a:id(2):1]-> a where a implements Id
alias2 = \x -> alias1 x
# ^^^^^^ a -[[alias1(6)]]-> a | a has Id
# ^^^^^^ a -[[alias1(6)]]-> a where a implements Id
a : A
a = alias2 (@A {})

View file

@ -1,8 +1,8 @@
app "test" provides [main] to "./platform"
Id has id : a -> a | a has Id
Id implements id : a -> a where a implements Id
A := {} has [Id {id}]
A := {} implements [Id {id}]
id = \@A {} -> @A {}
#^^{-1} A#id(4): A -[[id(4)]]-> A

View file

@ -1,10 +1,10 @@
app "test" provides [main] to "./platform"
Bounce has
ping : a -> a | a has Bounce
pong : a -> a | a has Bounce
Bounce implements
ping : a -> a where a implements Bounce
pong : a -> a where a implements Bounce
A := {} has [Bounce {ping: pingA, pong: pongA}]
A := {} implements [Bounce {ping: pingA, pong: pongA}]
pingA = \@A {} -> pong (@A {})
# ^^^^ A#pong(6): A -[[pongA(6)]]-> A

View file

@ -1,10 +1,10 @@
app "test" provides [main] to "./platform"
Bounce has
ping : a -> a | a has Bounce
pong : a -> a | a has Bounce
Bounce implements
ping : a -> a where a implements Bounce
pong : a -> a where a implements Bounce
A := {} has [Bounce {ping, pong}]
A := {} implements [Bounce {ping, pong}]
ping = \@A {} -> pong (@A {})
# ^^^^ A#pong(6): A -[[pong(6)]]-> A

View file

@ -1,8 +1,8 @@
app "test" provides [main] to "./platform"
Diverge has diverge : a -> a | a has Diverge
Diverge implements diverge : a -> a where a implements Diverge
A := {} has [Diverge {diverge}]
A := {} implements [Diverge {diverge}]
diverge : A -> A
diverge = \@A {} -> diverge (@A {})

View file

@ -3,9 +3,9 @@ app "test" provides [main] to "./platform"
Thunk a : {} -> a
Id has id : a -> Thunk a | a has Id
Id implements id : a -> Thunk a where a implements Id
A := {} has [Id {id}]
A := {} implements [Id {id}]
id = \@A {} -> \{} -> @A {}
#^^{-1} A#id(5): {} -[[id(5)]]-> ({} -[[8]]-> {})

View file

@ -3,15 +3,15 @@ app "test" provides [main] to "./platform"
Thunk a : {} -> a
Id has id : a -> Thunk a | a has Id
Id implements id : a -> Thunk a where a implements Id
A := {} has [Id {id}]
A := {} implements [Id {id}]
id = \@A {} -> \{} -> @A {}
#^^{-1} A#id(5): {} -[[id(5)]]-> ({} -[[8]]-> {})
main =
alias = \x -> id x
# ^^ Id#id(3): a -[[] + a:id(3):1]-> ({} -[[] + a:id(3):2]-> a) | a has Id
# ^^ Id#id(3): a -[[] + a:id(3):1]-> ({} -[[] + a:id(3):2]-> a) where a implements Id
a : A
a = (alias (@A {})) {}

View file

@ -3,9 +3,9 @@ app "test" provides [main] to "./platform"
Thunk a := {} -> a
Id has id : a -> Thunk a | a has Id
Id implements id : a -> Thunk a where a implements Id
A := {} has [Id {id}]
A := {} implements [Id {id}]
id = \@A {} -> @Thunk (\{} -> @A {})
#^^{-1} A#id(5): {} -[[id(5)]]-> ({} -[[8]]-> {})

View file

@ -1,8 +1,8 @@
app "test" provides [main] to "./platform"
Default has default : {} -> a | a has Default
Default implements default : {} -> a where a implements Default
A := {} has [Default {default}]
A := {} implements [Default {default}]
default = \{} -> @A {}
main =

View file

@ -1,19 +1,19 @@
app "test" provides [main] to "./platform"
X has
consume : a -> {} | a has X
X implements
consume : a -> {} where a implements X
O := {} has [X {consume: consumeO}]
O := {} implements [X {consume: consumeO}]
consumeO = \@O {} -> {}
P := {} has [X {consume: consumeP}]
P := {} implements [X {consume: consumeP}]
consumeP = \@P {} -> {}
caller = \x -> consume x
# ^ a | a has X
# ^^^^^^^ X#consume(2): a -[[] + a:consume(2):1]-> {} | a has X
# ^ a where a implements X
# ^^^^^^^ X#consume(2): a -[[] + a:consume(2):1]-> {} where a implements X
main = {
a: caller (@O {}),

View file

@ -1,9 +1,9 @@
app "test" provides [hash] to "./platform"
MHash has
hash : a -> U64 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
Id := U64 has [MHash {hash}]
Id := U64 implements [MHash {hash}]
hash : Id -> U64
#^^^^{-1} Id#hash(3): Id -[[hash(3)]]-> U64

View file

@ -1,9 +1,9 @@
app "test" provides [hash] to "./platform"
MHash has
hash : a -> U64 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
Id := U64 has [MHash {hash}]
Id := U64 implements [MHash {hash}]
hash : Id -> U64
hash = \@Id n -> n

View file

@ -1,8 +1,8 @@
app "test" provides [hashEq] to "./platform"
MHash has
hash : a -> U64 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
hashEq : a, a -> Bool | a has MHash
hashEq : a, a -> Bool where a implements MHash
hashEq = \x, y -> hash x == hash y
#^^^^^^{-1} a, a -[[hashEq(0)]]-> Bool | a has MHash
#^^^^^^{-1} a, a -[[hashEq(0)]]-> Bool where a implements MHash

View file

@ -1,7 +1,7 @@
app "test" provides [hashEq] to "./platform"
MHash has
hash : a -> U64 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
hashEq = \x, y -> hash x == hash y
#^^^^^^{-1} a, a1 -[[hashEq(0)]]-> Bool | a has MHash, a1 has MHash
#^^^^^^{-1} a, a1 -[[hashEq(0)]]-> Bool where a implements MHash, a1 implements MHash

View file

@ -1,11 +1,11 @@
app "test" provides [result] to "./platform"
MHash has
hash : a -> U64 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
hashEq = \x, y -> hash x == hash y
Id := U64 has [MHash {hash}]
Id := U64 implements [MHash {hash}]
hash = \@Id n -> n
result = hashEq (@Id 100) (@Id 101)

View file

@ -1,14 +1,14 @@
app "test" provides [result] to "./platform"
MHash has
hash : a -> U64 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
mulMHashes = \x, y -> hash x * hash y
Id := U64 has [MHash { hash: hashId }]
Id := U64 implements [MHash { hash: hashId }]
hashId = \@Id n -> n
Three := {} has [MHash { hash: hashThree }]
Three := {} implements [MHash { hash: hashThree }]
hashThree = \@Three _ -> 3
result = mulMHashes (@Id 100) (@Three {})

View file

@ -1,9 +1,9 @@
app "test" provides [zero] to "./platform"
MHash has
hash : a -> U64 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
Id := U64 has [MHash {hash}]
Id := U64 implements [MHash {hash}]
hash = \@Id n -> n

View file

@ -1,9 +1,9 @@
app "test" provides [thething] to "./platform"
MHash has
hash : a -> U64 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
thething =
#^^^^^^^^{-1} a -[[] + a:hash(2):1]-> U64 | a has MHash
#^^^^^^^^{-1} a -[[] + a:hash(2):1]-> U64 where a implements MHash
itis = hash
itis

View file

@ -1,8 +1,8 @@
app "test" provides [zeroEncoder] to "./platform"
MEncoder fmt := List U8, fmt -> List U8 | fmt has Format
MEncoder fmt := List U8, fmt -> List U8 where fmt implements Format
Format has it : fmt -> {} | fmt has Format
Format implements it : fmt -> {} where fmt implements Format
zeroEncoder = @MEncoder \lst, _ -> lst
#^^^^^^^^^^^{-1} MEncoder a | a has Format
#^^^^^^^^^^^{-1} MEncoder a where a implements Format

View file

@ -1,6 +1,6 @@
app "test" provides [main] to "./platform"
MHash has hash : a -> U64 | a has MHash
MHash implements hash : a -> U64 where a implements MHash
main = hash
# ^^^^ MHash#hash(2): a -[[] + a:hash(2):1]-> U64 | a has MHash
# ^^^^ MHash#hash(2): a -[[] + a:hash(2):1]-> U64 where a implements MHash

View file

@ -1,14 +1,14 @@
app "test" provides [hash, hash32, eq, le] to "./platform"
MHash has
hash : a -> U64 | a has MHash
hash32 : a -> U32 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
hash32 : a -> U32 where a implements MHash
Ord has
eq : a, a -> Bool | a has Ord
le : a, a -> Bool | a has Ord
Ord implements
eq : a, a -> Bool where a implements Ord
le : a, a -> Bool where a implements Ord
Id := U64 has [MHash {hash, hash32}, Ord {eq, le}]
Id := U64 implements [MHash {hash, hash32}, Ord {eq, le}]
hash = \@Id n -> n
#^^^^{-1} Id#hash(7): Id -[[hash(7)]]-> U64

View file

@ -1,10 +1,10 @@
app "test" provides [hash, hash32] to "./platform"
MHash has
hash : a -> U64 | a has MHash
hash32 : a -> U32 | a has MHash
MHash implements
hash : a -> U64 where a implements MHash
hash32 : a -> U32 where a implements MHash
Id := U64 has [MHash {hash, hash32}]
Id := U64 implements [MHash {hash, hash32}]
hash = \@Id n -> n
#^^^^{-1} Id#hash(4): Id -[[hash(4)]]-> U64

View file

@ -1,8 +1,8 @@
app "test" provides [hash] to "./platform"
MHash has hash : a -> U64 | a has MHash
MHash implements hash : a -> U64 where a implements MHash
Id := U64 has [MHash {hash}]
Id := U64 implements [MHash {hash}]
hash = \@Id n -> n
#^^^^{-1} Id#hash(3): Id -[[hash(3)]]-> U64

View file

@ -2,7 +2,7 @@ app "test"
imports [TotallyNotJson]
provides [main] to "./platform"
HelloWorld := {} has [Encoding {toEncoder}]
HelloWorld := {} implements [Encoding {toEncoder}]
toEncoder = \@HelloWorld {} ->
Encode.custom \bytes, fmt ->