blob: 4b74db183e30e9b749754ded28d86fcbfec15b98 (
plain)
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
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
|
(;module:
lux
(lux [io]
(control [monad #+ do]
pipe)
(data ["e" error]
[maybe]
[product]
[text "text/" Eq<Text>]
text/format
(coll [list "list/" Functor<List>]))
["r" math/random "r/" Monad<Random>]
[meta]
(meta [code]
[type "type/" Eq<Type>])
test)
(luxc ["&" base]
(lang ["la" analysis])
[analyser]
(analyser ["@" function]
["@;" common])
["@;" module])
(.. common)
(test/luxc common))
(def: (check-type expectedT error)
(-> Type (e;Error [Type la;Analysis]) Bool)
(case error
(#e;Success [exprT exprA])
(type/= expectedT exprT)
_
false))
(def: (succeeds? error)
(All [a] (-> (e;Error a) Bool))
(case error
(#e;Success _)
true
(#e;Error _)
false))
(def: (flatten-apply analysis)
(-> la;Analysis [la;Analysis (List la;Analysis)])
(case analysis
(#la;Apply head func)
(let [[func' tail] (flatten-apply func)]
[func' (#;Cons head tail)])
_
[analysis (list)]))
(def: (check-apply expectedT num-args analysis)
(-> Type Nat (Meta [Type la;Analysis]) Bool)
(|> analysis
(meta;run (init-compiler []))
(case> (#e;Success [applyT applyA])
(let [[funcA argsA] (flatten-apply applyA)]
(and (type/= expectedT applyT)
(n.= num-args (list;size argsA))))
(#e;Error error)
false)))
(context: "Function definition."
[func-name (r;text +5)
arg-name (|> (r;text +5) (r;filter (|>. (text/= func-name) not)))
[outputT outputC] gen-primitive
[inputT _] gen-primitive]
($_ seq
(test "Can analyse function."
(|> (&;with-expected-type (type (All [a] (-> a outputT)))
(@;analyse-function analyse func-name arg-name outputC))
(meta;run (init-compiler []))
succeeds?))
(test "Generic functions can always be specialized."
(and (|> (&;with-expected-type (-> inputT outputT)
(@;analyse-function analyse func-name arg-name outputC))
(meta;run (init-compiler []))
succeeds?)
(|> (&;with-expected-type (-> inputT inputT)
(@;analyse-function analyse func-name arg-name (code;symbol ["" arg-name])))
(meta;run (init-compiler []))
succeeds?)))
(test "Can infer function (constant output and unused input)."
(|> (@common;with-unknown-type
(@;analyse-function analyse func-name arg-name outputC))
(meta;run (init-compiler []))
(check-type (type (All [a] (-> a outputT))))))
(test "Can infer function (output = input)."
(|> (@common;with-unknown-type
(@;analyse-function analyse func-name arg-name (code;symbol ["" arg-name])))
(meta;run (init-compiler []))
(check-type (type (All [a] (-> a a))))))
(test "The function's name is bound to the function's type."
(|> (&;with-expected-type (type (Rec self (-> inputT self)))
(@;analyse-function analyse func-name arg-name (code;symbol ["" func-name])))
(meta;run (init-compiler []))
succeeds?))
(test "Can infer recursive types for functions."
(|> (@common;with-unknown-type
(@;analyse-function analyse func-name arg-name (code;symbol ["" func-name])))
(meta;run (init-compiler []))
(check-type (type (Rec self (All [a] (-> a self)))))))
))
(context: "Function application."
[full-args (|> r;nat (:: @ map (|>. (n.% +10) (n.max +2))))
partial-args (|> r;nat (:: @ map (n.% full-args)))
var-idx (|> r;nat (:: @ map (|>. (n.% full-args) (n.max +1))))
inputsTC (r;list full-args gen-primitive)
#let [inputsT (list/map product;left inputsTC)
inputsC (list/map product;right inputsTC)]
[outputT outputC] gen-primitive
#let [funcT (type;function inputsT outputT)
partialT (type;function (list;drop partial-args inputsT) outputT)
varT (#;Bound +1)
polyT (<| (type;univ-q +1)
(type;function (list;concat (list (list;take var-idx inputsT)
(list varT)
(list;drop (n.inc var-idx) inputsT))))
varT)
poly-inputT (maybe;assume (list;nth var-idx inputsT))
partial-poly-inputsT (list;drop (n.inc var-idx) inputsT)
partial-polyT1 (<| (type;function partial-poly-inputsT)
poly-inputT)
partial-polyT2 (<| (type;univ-q +1)
(type;function (#;Cons varT partial-poly-inputsT))
varT)]]
($_ seq
(test "Can analyse monomorphic type application."
(|> (@common;with-unknown-type
(@;analyse-apply analyse funcT (#la;Unit) inputsC))
(check-apply outputT full-args)))
(test "Can partially apply functions."
(|> (@common;with-unknown-type
(@;analyse-apply analyse funcT (#la;Unit)
(list;take partial-args inputsC)))
(check-apply partialT partial-args)))
(test "Can apply polymorphic functions."
(|> (@common;with-unknown-type
(@;analyse-apply analyse polyT (#la;Unit) inputsC))
(check-apply poly-inputT full-args)))
(test "Polymorphic partial application propagates found type-vars."
(|> (@common;with-unknown-type
(@;analyse-apply analyse polyT (#la;Unit)
(list;take (n.inc var-idx) inputsC)))
(check-apply partial-polyT1 (n.inc var-idx))))
(test "Polymorphic partial application preserves quantification for type-vars."
(|> (@common;with-unknown-type
(@;analyse-apply analyse polyT (#la;Unit)
(list;take var-idx inputsC)))
(check-apply partial-polyT2 var-idx)))
))
|
