blob: e77819779f16585db6b81ce60bf1bf960b5044e1 (
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
|
(;module:
lux
(lux (control monad
pipe)
(data text/format
[product])
[macro #+ Monad<Lux>]
[type]
(type ["TC" check]))
(luxc ["&" base]
lang))
(def: #export get-type
(-> Analysis Type)
(|>. product;left
product;left))
(def: #export (replace-type replacement analysis)
(-> Type Analysis Analysis)
(let [[[_type _cursor] _analysis] analysis]
(: Analysis
[[(: Type replacement)
(: Cursor _cursor)]
(: (Analysis' Analysis)
_analysis)])))
(def: #export (clean type analysis)
(-> Type Analysis (Lux Analysis))
(case type
(#;Var id)
(do Monad<Lux>
[=type (&;within-type-env
(TC;clean id type))]
(wrap (replace-type =type analysis)))
(#;Ex id)
(undefined)
_
(&;fail (format "Cannot clean type: " (%type type)))))
(def: #export (with-unknown-type action)
(All [a] (-> (Lux Analysis) (Lux Analysis)))
(do Monad<Lux>
[[var-id var-type] (&;within-type-env
TC;create-var)
analysis (|> (wrap action)
(%> @
[(&;with-expected-type var-type)]
[(clean var-type)]))
_ (&;within-type-env
(TC;delete-var var-id))]
(wrap analysis)))
(def: #export (realize expected)
(-> Type (TC;Check [(List Type) Type]))
(case expected
(#;Named [module name] _expected)
(realize _expected)
(#;UnivQ env body)
(do TC;Monad<Check>
[[var-id var-type] TC;create-var
[tail =expected] (realize (default (undefined)
(type;apply-type expected var-type)))]
(wrap [(list& var-type tail)
=expected]))
(#;ExQ env body)
(do TC;Monad<Check>
[[ex-id ex-type] TC;existential
[tail =expected] (realize (default (undefined)
(type;apply-type expected ex-type)))]
(wrap [(list& ex-type tail)
=expected]))
_
(:: TC;Monad<Check> wrap [(list) expected])))
|
