blob: f1d7fdd31024540284729ea3cb3368945cfe66e0 (
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
|
(;module:
lux
(lux (control monad)
(data [text]
text/format
(coll [list "L/" Fold<List> Monoid<List> Monad<List>]))
[macro #+ Monad<Lux>]
[type]
(type ["TC" check]))
(luxc ["&" base]
(lang ["la" analysis #+ Analysis])
["&;" env]
(analyser ["&;" common]
["&;" inference])))
## [Analysers]
(def: #export (analyse-function analyse func-name arg-name body)
(-> &;Analyser Text Text Code (Lux Analysis))
(do Monad<Lux>
[functionT macro;expected-type]
(loop [expected functionT]
(&;with-stacked-errors
(function [_] (format "Functions require function types: " (type;to-text expected)))
(case expected
(#;Named name unnamedT)
(recur unnamedT)
(#;Apply argT funT)
(case (type;apply (list argT) funT)
(#;Some value)
(recur value)
#;None
(&;fail (format "Cannot apply type " (%type funT) " to type " (%type argT))))
(#;UnivQ _)
(do @
[[var-id var] (&;within-type-env
TC;existential)]
(recur (assume (type;apply (list var) expected))))
(#;ExQ _)
(&common;with-var
(function [[var-id var]]
(recur (assume (type;apply (list var) expected)))))
(#;Var id)
(do @
[? (&;within-type-env
(TC;bound? id))]
(if ?
(do @
[expected' (&;within-type-env
(TC;read-var id))]
(recur expected'))
## Inference
(&common;with-var
(function [[input-id inputT]]
(&common;with-var
(function [[output-id outputT]]
(do @
[#let [funT (#;Function inputT outputT)]
funA (recur funT)
funT' (&;within-type-env
(TC;clean output-id funT))
concrete-input? (&;within-type-env
(TC;bound? input-id))
funT'' (if concrete-input?
(&;within-type-env
(TC;clean input-id funT'))
(wrap (type;univ-q +1 (&inference;replace-var input-id +1 funT'))))
_ (&;within-type-env
(TC;check expected funT''))]
(wrap funA))
))))))
(#;Function inputT outputT)
(<| (:: @ map (|>. #la;Function))
&;with-scope
## Functions have access not only to their argument, but
## also to themselves, through a local variable.
(&env;with-local [func-name functionT])
(&env;with-local [arg-name inputT])
(&;with-expected-type outputT)
(analyse body))
_
(&;fail "")
)))))
(def: #export (analyse-apply analyse funcT funcA args)
(-> &;Analyser Type Analysis (List Code) (Lux Analysis))
(&;with-stacked-errors
(function [_] (format "Cannot apply function " (%type funcT)
" to args: " (|> args (L/map %code) (text;join-with " "))))
(do Monad<Lux>
[expected macro;expected-type
[applyT argsA] (&inference;apply-function analyse funcT args)
_ (&;within-type-env
(TC;check expected applyT))]
(wrap (la;apply argsA funcA)))))
|
