This repository has been archived by the owner on Jan 14, 2023. It is now read-only.
-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathbenchmarks.yaml
145 lines (144 loc) · 5.56 KB
/
benchmarks.yaml
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
133
134
135
136
137
138
139
140
141
142
143
144
145
tools:
# The order in which tools appear affects the order in which we generate
# LaTeX summary tables.
- title: Gtubi
command: [ "./bin/gtubi" ]
- title: InsAndOuts
command: [ "./bin/TypeWhich", "migrate", "--ins-and-outs", "--skip-type-check" ]
- title: MGT
command: [ "./bin/mgt" ]
- title: MaxMigrate
command: [ "./bin/MaxMigrate" ]
- title: TypeWhich2
command: [ "./bin/TypeWhich", "migrate" ]
- title: TypeWhich
command: [ "./bin/TypeWhich", "migrate", "--precise" ]
benchmarks:
- file: adversarial/01-farg-mismatch.gtlc
- file: adversarial/02-rank2-poly-id.gtlc
# Improved i:any to i:any -> any. But, i is always applied, so this is
# compatible.
assert_compatible: |
(fun i:any -> any. (fun a:any. i true) (i 5)) (fun x:any. x)
- file: adversarial/03-unreachable-error.gtlc
# This is an improved type. But, the program always crashes.
assert_compatible: |
(fun b:(any -> any) -> (any -> int) -> any -> int.
b (fun c:any. (fun x:int. x x) 5 5) (fun d:any. 0))
(fun t:any -> any. fun f:any -> int. f)
- file: adversarial/04-f-in-f-out.gtlc
# this is obviously an improved type
assert_compatible: |
(fun f:int -> int. (fun y:int. f) (f 5)) (fun x:int. 10 + x)
- file: adversarial/05-order3-fun.gtlc
context: |
(HOLE) (fun a . a) (fun b . true)
assert_compatible: |
fun f:(any -> any) -> any. fun x:any -> any. x (f x)
results:
MaxMigrate:
assert_unusable: true
- file: adversarial/06-order3-intfun.gtlc
context: |
(HOLE) (fun a . fun b . true) (fun c . 0)
# g is always uses as an int -> int function, f is always applied g and an
# int. However, f may return a non-int.
assert_compatible: |
fun f : (int -> int) -> (int -> any) .
fun g : int -> int. (f g) ((g 10) + 1)
- file: adversarial/07-double-f.gtlc
context: |
(HOLE) (fun x . fun y . y)
- file: adversarial/08-outflows.gtlc
- file: adversarial/09-precision-relation.gtlc
# f receives both true and 5, thus it must receive any as its argument.
# However, the only value of f is (fun x . 5), so it returns an int.
# The value of g is f, but it is used as an int->int function.
assert_compatible: |
(fun f:any -> int. f true + (fun g:int -> int. g 5) f) (fun x:any. 5)
- file: adversarial/10-if-tag.gtlc
context: |
(HOLE) true 1
- file: migeed/01_apply_add.gtlc
# This is what we get out of MGT. It is compatible with the assumption that
# the inner x has a coercion that is "doomed to fail". MGT produces this
# coercion, but does not print it.
assert_compatible: |
fun x : any -> any . x (x + 1)
- file: migeed/02_add_applied.gtlc
# This example is subtle: the core GTLC has neither type-testing nor state.
# So, although we make two calls to x with two different types, there is
# no GTLC function that produce a number on "x true" and a non-number on
# "x (x true + 1)". So, for the function to not crash x must be a constant
# function that produces a number.
assert_compatible: |
fun x : any -> int . x (x true + 1)
context: |
(HOLE) (fun y . 1)
- file: migeed/03_add_two_applies.gtlc
assert_compatible: |
fun x:any -> int. x 4 + x true
context: |
(HOLE) (fun y . 1)
- file: migeed/04_identity_four.gtlc
assert_compatible: |
(fun x:int. x) 4
- file: migeed/05_succ_id_id.gtlc
- file: migeed/06_identity.gtlc
context: |
(HOLE) (fun y . y)
- file: migeed/07_apply2.gtlc
assert_compatible: |
fun x:any. fun y:any -> any -> any. y x x
context: |
(HOLE) 1 (fun z1 . fun z2 . 1)
results:
MaxMigrate:
# The migration produced is "unusable" -- no way to apply it. It is
# explained in the paper itself.
assert_unusable: true
- file: migeed/08_indirect_apply_self.gtlc
assert_compatible: |
fun x:any -> any. (fun y:any -> any. x) x x
results:
# Look at the output that we get for MaxMigrate in results.yaml. It is
# going to be:
# fun x : any . (fun y : int . x) x x
# The annotation on y requires x to be an integer. But the inner application
# expects it to be a function. So, there is no way to use this term.
MaxMigrate:
assert_unusable: true
context: |
(HOLE) (fun z : any . z)
- file: migeed/09_the_long_one.gtlc
context: |
(HOLE) true 1
assert_compatible: |
fun x:any. (fun f:any -> int. (fun xx:any -> int. fun y:int. xx) f (f x)) (fun z:any. 1)
- file: migeed/10_apply_self.gtlc
assert_compatible: |
fun x:any -> any. x x
- file: migeed/11_untypable_in_sys_f.gtlc
assert_compatible: |
(fun x:(any -> any -> any) -> any.
fun y:any -> any -> any.
y (x (fun x:any. x))
(x (fun b:any. fun c:any. b)))
(fun d:any -> any. d d)
- file: migeed/12_self_interpreter.gtlc
assert_compatible: |
(fun h: ((any -> any) ->
(any -> any -> any) ->
((any -> any) -> any -> any) -> any) ->
((any -> any) -> (any -> any -> any) ->
((any -> any) -> any -> any) -> any) -> any .
(fun x:any -> any. h (x x))
(fun x: (any -> any) ->
(any -> any -> any) -> ((any -> any) -> any -> any) -> any .
h x x))
(fun e:any .
fun m: (any -> any) ->
(any -> any -> any) -> ((any -> any) -> any -> any) -> any .
m (fun x:any . x)
(fun m:any . fun n:any . e m (e n))
(fun m:any -> any . fun v:any. e (m v)))