blob: 824071ab3008f0a7c64797fd12d02c25402cd7b1 (
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
|
(;module:
lux
(lux (control monad)
(data text/format
(coll [list "L/" Functor<List>]))
[macro #+ Monad<Lux>]
[type]
(type ["TC" check]))
(luxc ["&" base]
(lang ["la" analysis #+ Analysis])
(analyser ["&;" common])))
(def: #export (bind-var var-id bound-idx type)
(-> Nat Nat Type Type)
(case type
(#;Host name params)
(#;Host name (L/map (bind-var var-id bound-idx) params))
(^template [<tag>]
(<tag> left right)
(<tag> (bind-var var-id bound-idx left)
(bind-var var-id bound-idx right)))
([#;Sum]
[#;Product]
[#;Function]
[#;App])
(#;Var id)
(if (n.= var-id id)
(#;Bound bound-idx)
type)
(^template [<tag>]
(<tag> env quantified)
(<tag> (L/map (bind-var var-id bound-idx) env)
(bind-var var-id (n.+ +2 bound-idx) quantified)))
([#;UnivQ]
[#;ExQ])
(#;Named name unnamedT)
(#;Named name
(bind-var var-id bound-idx unnamedT))
_
type))
(def: #export (apply-function analyse funcT args)
(-> &;Analyser Type (List Code) (Lux [Type (List Analysis)]))
(case args
#;Nil
(:: Monad<Lux> wrap [funcT (list)])
(#;Cons arg args')
(case funcT
(#;Named name unnamedT)
(apply-function analyse unnamedT args)
(#;UnivQ _)
(&common;with-var
(function [[var-id varT]]
(do Monad<Lux>
[[outputT argsA] (apply-function analyse (assume (type;apply-type funcT varT)) args)]
(do @
[? (&;within-type-env
(TC;bound? var-id))
outputT' (if ?
(&;within-type-env
(TC;clean var-id outputT))
(wrap (#;UnivQ (list) (bind-var var-id +1 outputT))))]
(wrap [outputT' argsA])))))
(#;ExQ _)
(do Monad<Lux>
[[ex-id exT] (&;within-type-env
TC;existential)]
(apply-function analyse (assume (type;apply-type funcT exT)) args))
(#;Function inputT outputT)
(do Monad<Lux>
[[outputT' args'A] (apply-function analyse outputT args')
argA (&;with-stacked-errors
(function [_] (format "Expected type: " (%type inputT) "\n"
" For argument: " (%code arg)))
(&;with-expected-type inputT
(analyse arg)))]
(wrap [outputT' (list& argA args'A)]))
_
(&;fail (format "Cannot apply a non-function: " (%type funcT))))
))
|
