blob: 8063f450d908b6431c69ddffd07451bd3d7390dc (
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
|
(.module:
[library
[lux (#- function)
[abstract
monad]
[control
["." maybe]
["ex" exception (#+ exception:)]]
[data
["." text
["%" format (#+ format)]]
[collection
["." list ("#\." fold monoid monad)]]]
["." type
["." check]]
["." meta]]]
["." // #_
["#." scope]
["#." type]
["#." inference]
["/#" // #_
["#." extension]
[//
["/" analysis (#+ Analysis Operation Phase)]
[///
["#" phase]
[reference (#+)
[variable (#+)]]]]]])
(exception: .public (cannot_analyse {expected Type} {function Text} {argument Text} {body Code})
(ex.report ["Type" (%.type expected)]
["Function" function]
["Argument" argument]
["Body" (%.code body)]))
(exception: .public (cannot_apply {functionT Type} {functionC Code} {arguments (List Code)})
(ex.report ["Function type" (%.type functionT)]
["Function" (%.code functionC)]
["Arguments" (|> arguments
list.enumeration
(list\map (.function (_ [idx argC])
(format (%.nat idx) " " (%.code argC))))
(text.join_with text.new_line))]))
(def: .public (function analyse function_name arg_name archive body)
(-> Phase Text Text Phase)
(do {! ///.monad}
[functionT (///extension.lift meta.expected_type)]
(loop [expectedT functionT]
(/.with_stack ..cannot_analyse [expectedT function_name arg_name body]
(case expectedT
(#.Named name unnamedT)
(recur unnamedT)
(#.Apply argT funT)
(case (type.applied (list argT) funT)
(#.Some value)
(recur value)
#.None
(/.failure (ex.error cannot_analyse [expectedT function_name arg_name body])))
(^template [<tag> <instancer>]
[(<tag> _)
(do !
[[_ instanceT] (//type.with_env <instancer>)]
(recur (maybe.assume (type.applied (list instanceT) expectedT))))])
([#.UnivQ check.existential]
[#.ExQ check.var])
(#.Var id)
(do !
[?expectedT' (//type.with_env
(check.read id))]
(case ?expectedT'
(#.Some expectedT')
(recur expectedT')
... Inference
_
(do !
[[input_id inputT] (//type.with_env check.var)
[output_id outputT] (//type.with_env check.var)
.let [functionT (#.Function inputT outputT)]
functionA (recur functionT)
_ (//type.with_env
(check.check expectedT functionT))]
(in functionA))
))
(#.Function inputT outputT)
(<| (\ ! map (.function (_ [scope bodyA])
(#/.Function (list\map (|>> /.variable)
(//scope.environment scope))
bodyA)))
/.with_scope
... Functions have access not only to their argument, but
... also to themselves, through a local variable.
(//scope.with_local [function_name expectedT])
(//scope.with_local [arg_name inputT])
(//type.with_type outputT)
(analyse archive body))
_
(/.failure "")
)))))
(def: .public (apply analyse argsC+ functionT functionA archive functionC)
(-> Phase (List Code) Type Analysis Phase)
(<| (/.with_stack ..cannot_apply [functionT functionC argsC+])
(do ///.monad
[[applyT argsA+] (//inference.general archive analyse functionT argsC+)])
(in (/.apply [functionA argsA+]))))
|
