1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
|
parser:
./a%20b
./"a%20b"
text interpolation and escapes
remove `double`
remove imports/parenthesizeUsing
remove multilet
selection by expression unit tests
success/
imports/
Missing missing
Headers https://example.com/foo using ./headers
HeadersInteriorHash https://example.com/foo using (./headers sha256:0000000000000000000000000000000000000000000000000000000000000000)
HeadersExteriorHash (https://example.com/foo using ./headers) sha256:0000000000000000000000000000000000000000000000000000000000000000
HeadersHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000
HeadersDoubleHashPrecedence https://example.com/foo using ./headers sha256:0000000000000000000000000000000000000000000000000000000000000000 sha256:1111111111111111111111111111111111111111111111111111111111111111
DoubleLitPositive 1.23
DoubleLitNegative -1.23
DoubleLitExponent 1.23e4
DoubleLitExponentNoDot 1e4
DoubleLitExponentNegative 1.23e-4
DoubleLitInfinity Infinity
DoubleLitNegInfinity -Infinity
DoubleLitNaN NaN
DoubleLitSecretelyInt 1.0
DoubleLitZero 0.0
BuiltinListBuild List/Build
FunctionApplicationOneArg f x
FunctionApplicationMultipleArgs f x y z
Annotation x : T
ListLitNonEmpty [x, y]
ListLitNonEmptyAnnotated [x, y] : List T
OptionalLitEmpty []: Optional T
OptionalLitNonEmpty [x]: Optional T
Field r.x
FieldBuiltinName r.List
FieldQuoted r.`x`
Projection r.{x, y, z}
Let let x: T = v in e
LetNested let x: T = v in let y: U = w in e
LetMulti let x: T = v let y: U = w in e
LambdaUnicode λ(x : T) -> y
FunctionTypePi forall(x: T) -> U
FunctionTypePiUnicode ∀(x: T) -> U
FunctionTypePiNested forall(x: T) -> ∀(y: U) -> V
FunctionTypePiUnderscore forall(_: T) -> U
FunctionTypeArrow T -> U
RecordLit { x = 1, y = 2 }
RecordType { x: T, y: U }
operators/
ImportAlt x ? y
ImportAltAssoc w ? x ? y ? z
BoolOr x || y
BoolOrAssoc w || x || y || z
NaturalPlus x + y
NaturalPlusAssoc w + x + y + z
TextAppend x ++ y
TextAppendAssoc w ++ x ++ y ++ z
ListAppend x # y
ListAppendAssoc w # x # y # z
BoolAnd x && y
BoolAndAssoc w && x && y && z
NaturalTimes x * y
NaturalTimesAssoc w * x * y * z
BoolEQ x == y
BoolEQAssoc w == x == y == z
BoolNE x != y
BoolNEAssoc w != x != y != z
RecursiveRecordMerge x //\\ y
RecursiveRecordMergeAssoc w //\\ x //\\ y //\\ z
RecursiveRecordTypeMerge x /\ y
RecursiveRecordTypeMergeAssoc w /\ x /\ y /\ z
RightBiasedRecordMerge x // y
RightBiasedRecordMergeAssoc w // x // y // z
RecursiveRecordMergeUnicode x ∧ y
RecursiveRecordMergeUnicodeAssoc w ∧ x /\ y ∧ z
RightBiasedRecordMergeUnicode x ⫽ y
RightBiasedRecordMergeUnicodeAssoc w ⫽ x // y ⫽ z
RecursiveRecordTypeMergeUnicode x ⩓ y
RecursiveRecordTypeMergeUnicodeAssoc w ⩓ x //\\ y ⩓ z
PrecedenceAll1 a ? b || c + d ++ e # f && g ∧ h ⫽ i ⩓ j * k == l != m n.o
PrecedenceAll2 a b != c == d * e ⩓ f ⫽ g ∧ h && i # j ++ k + l || m ? n
PrecedenceNat a + b * d + e f * (g + h)
PrecedenceBool a && b || c d == e || f != g && h || i
PrecedenceRecord a // b c /\ d ⫽ e.{x} ∧ f
failure/
ProjectionByExpressionNeedsParens r.{ x: T }
import:
success/
recover type error
recover recursive import error
failure/
don't recover cycle
normalization:
variables across import boundaries
TextLitNested1 "${""}${x}"
TextLitNested2 "${"${x}"}"
TextLitNested3 "${"${""}"}${x}"
EquivalenceDouble if b then NaN else NaN
EquivalenceAlpha if b then \(x: T) -> x else \(y: T) -> y
typecheck:
something that involves destructuring a recordtype after merge
success/
MergeEmptyAlternative merge { x = 1 } < x >.x
MergeTrickyShadowing let _ = Bool in merge {_ = \(x: _) -> x} (<_: Bool>._ True)
EquivalenceAlpha \(TODO: forall(x: Type) -> x) -> TODO : forall(y: Type) -> y
failure/
MergeEmptyNeedsDirectAnnotation1 \(x: <>) -> (merge {=} x) : Bool
MergeEmptyNeedsDirectAnnotation2 \(x: <>) -> let y: Bool = merge {=} x in 1
MergeBoolIsNotUnion merge x True
MergeOptionalIsNotUnion merge x (Some 1)
MergeMissingHandler1 merge {=} < x >.x
MergeMissingHandler2 merge {x=...,} <x|y>.x
merge { x = λ(x : Bool) → x } (< x: Bool | y: Natural >.x True)
merge { x = λ(_ : Bool) → _, y = 1 } < x = True | y >
merge { x = True, y = 1 } < x | y >.x
merge {x=...,y=...} <x>.x
merge {x=...,y=...} <x:T>.x
MergeHandlerFreeVar merge { x = None } < x = Bool >
UnionTypeDuplicateVariants1 <x, x>
UnionTypeDuplicateVariants2 <x, x:T>
UnionLitDuplicateVariants <x=1|x:T>
RecordLitDuplicateFields { x: T, x: T }
EquivalenceAlphaTrap \(TODO: forall(_: Type) -> _) -> TODO : forall(x: Type) -> _
equivalence:
|
