blob: 229e27bee1ef7885ea83b3ec0365893fc9439afb (
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
|
(.module:
[lux "*"
[abstract
["." monad {"+" [do]}]]
[data
["%" text/format {"+" [format]}]
["." name]]
["r" math/random {"+" [Random]}]
["_" test {"+" [Test]}]
[control
pipe
["." maybe]
["." try]]
[data
["." product]
["." text ("#\." equivalence)]
[number
["n" nat]]
[collection
["." list ("#\." functor)]]]
["." type]
["." macro
["." code]]]
[//
["_." primitive]
["_." structure]]
[\\
["." /
["/#" //
["#." module]
["#." type]
["/#" // "_"
["/#" //
["#." analysis {"+" [Analysis Operation]}]
[///
["#." reference]
["." phase]
[meta
["." archive]]]]]]]])
(def: (check_apply expectedT num_args analysis)
(-> Type Nat (Operation Analysis) Bit)
(|> analysis
(//type.with_type expectedT)
(phase.result _primitive.state)
(case> (#try.Success applyA)
(let [[funcA argsA] (////analysis.application applyA)]
(n.= num_args (list.size argsA)))
(#try.Failure _)
false)))
(def: abstraction
(do r.monad
[func_name (r.unicode 5)
arg_name (|> (r.unicode 5) (r.only (|>> (text\= func_name) not)))
[outputT outputC] _primitive.primitive
[inputT _] _primitive.primitive
.let [g!arg (code.local_identifier arg_name)]]
(<| (_.context (%.name (name_of /.function)))
($_ _.and
(_.test "Can analyse function."
(and (|> (//type.with_type (All (_ a) (-> a outputT))
(/.function _primitive.phase func_name arg_name archive.empty outputC))
_structure.check_succeeds)
(|> (//type.with_type (All (_ a) (-> a a))
(/.function _primitive.phase func_name arg_name archive.empty g!arg))
_structure.check_succeeds)))
(_.test "Generic functions can always be specialized."
(and (|> (//type.with_type (-> inputT outputT)
(/.function _primitive.phase func_name arg_name archive.empty outputC))
_structure.check_succeeds)
(|> (//type.with_type (-> inputT inputT)
(/.function _primitive.phase func_name arg_name archive.empty g!arg))
_structure.check_succeeds)))
(_.test "The function's name is bound to the function's type."
(|> (//type.with_type (Rec self (-> inputT self))
(/.function _primitive.phase func_name arg_name archive.empty (code.local_identifier func_name)))
_structure.check_succeeds))
))))
(def: apply
(do [! r.monad]
[full_args (|> r.nat (\ ! each (|>> (n.% 10) (n.max 2))))
partial_args (|> r.nat (\ ! each (n.% full_args)))
var_idx (|> r.nat (\ ! each (|>> (n.% full_args) (n.max 1))))
inputsTC (r.list full_args _primitive.primitive)
.let [inputsT (list\each product.left inputsTC)
inputsC (list\each product.right inputsTC)]
[outputT outputC] _primitive.primitive
.let [funcT (type.function inputsT outputT)
partialT (type.function (list.after partial_args inputsT) outputT)
varT (#.Parameter 1)
polyT (<| (type.univ_q 1)
(type.function (list.together (list (list.first var_idx inputsT)
(list varT)
(list.after (++ var_idx) inputsT))))
varT)
poly_inputT (maybe.trusted (list.item var_idx inputsT))
partial_poly_inputsT (list.after (++ var_idx) inputsT)
partial_polyT1 (<| (type.function partial_poly_inputsT)
poly_inputT)
partial_polyT2 (<| (type.univ_q 1)
(type.function (#.Item varT partial_poly_inputsT))
varT)
dummy_function (#////analysis.Function (list) (#////analysis.Reference (////reference.local 1)))]]
(<| (_.context (%.name (name_of /.apply)))
($_ _.and
(_.test "Can analyse monomorphic type application."
(|> (/.apply _primitive.phase inputsC funcT dummy_function archive.empty (' []))
(check_apply outputT full_args)))
(_.test "Can partially apply functions."
(|> (/.apply _primitive.phase (list.first partial_args inputsC) funcT dummy_function archive.empty (' []))
(check_apply partialT partial_args)))
(_.test "Can apply polymorphic functions."
(|> (/.apply _primitive.phase inputsC polyT dummy_function archive.empty (' []))
(check_apply poly_inputT full_args)))
(_.test "Polymorphic partial application propagates found type-vars."
(|> (/.apply _primitive.phase (list.first (++ var_idx) inputsC) polyT dummy_function archive.empty (' []))
(check_apply partial_polyT1 (++ var_idx))))
(_.test "Polymorphic partial application preserves quantification for type-vars."
(|> (/.apply _primitive.phase (list.first var_idx inputsC) polyT dummy_function archive.empty (' []))
(check_apply partial_polyT2 var_idx)))
))))
(def: .public test
Test
(<| (_.context (name.module (name_of /._)))
($_ _.and
..abstraction
..apply
)))
|
