Fix diffs
This commit is contained in:
parent
0bdf7260ed
commit
f7d554d727
|
@ -2,11 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "app rule the range of the function is matched to the argument")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
54c55
|
||||
55c55
|
||||
< (typeof Γ M_2 σ)
|
||||
---
|
||||
> (typeof Γ M_2 σ_2)
|
||||
237d237
|
||||
238d237
|
||||
<
|
||||
|
|
|
@ -2,5 +2,3 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the ((cons number) v) value has been omitted")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
|
|
|
@ -2,9 +2,7 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the order of the types in the function position of application has been swapped")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
53c54
|
||||
54c54
|
||||
< [(typeof Γ M (σ → σ_2))
|
||||
---
|
||||
> [(typeof Γ M (σ_2 → σ))
|
||||
|
|
|
@ -2,9 +2,7 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the type of cons is incorrect")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
63c64
|
||||
64c64
|
||||
< (int → ((list int) → (list int)))]
|
||||
---
|
||||
> (int → ((list int) → int))]
|
||||
|
|
|
@ -2,11 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "the tail reduction returns the wrong value")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
92c93
|
||||
93c93
|
||||
< (in-hole E v_2)
|
||||
---
|
||||
> (in-hole E v_1)
|
||||
237d237
|
||||
238d237
|
||||
<
|
||||
|
|
|
@ -2,11 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "hd reduction acts on partially applied cons")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
88c89
|
||||
89c89
|
||||
< (--> (in-hole E (hd ((cons v_1) v_2)))
|
||||
---
|
||||
> (--> (in-hole E (hd (cons v_1)))
|
||||
237d237
|
||||
238d237
|
||||
<
|
||||
|
|
|
@ -2,12 +2,10 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "evaluation isn't allowed on the rhs of applications")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
35,36c36
|
||||
36,37c36
|
||||
< (E M)
|
||||
< (v E)))
|
||||
---
|
||||
> (E M)))
|
||||
237d236
|
||||
238d236
|
||||
<
|
||||
|
|
|
@ -2,11 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "lookup always returns int")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
76c77
|
||||
77c77
|
||||
< σ]
|
||||
---
|
||||
> int]
|
||||
237d237
|
||||
238d237
|
||||
<
|
||||
|
|
|
@ -2,11 +2,9 @@
|
|||
< (define the-error "no error")
|
||||
---
|
||||
> (define the-error "variables aren't required to match in lookup")
|
||||
32a33
|
||||
> ((cons v) v)
|
||||
75c76
|
||||
76c76
|
||||
< [(lookup (x σ Γ) x)
|
||||
---
|
||||
> [(lookup (x σ Γ) x_2)
|
||||
237d237
|
||||
238d237
|
||||
<
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)))
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
|
|
|
@ -31,7 +31,6 @@
|
|||
c
|
||||
(cons v)
|
||||
((cons v) v)
|
||||
((cons v) v)
|
||||
(+ v))
|
||||
(E hole
|
||||
(E M)
|
||||
|
|
|
@ -181,7 +181,6 @@
|
|||
(define typed-generator (dynamic-require fpath 'typed-generator))
|
||||
(define gen-enum (dynamic-require fpath 'generate-enum-term))
|
||||
(define ordered-generator (dynamic-require fpath 'ordered-enum-generator))
|
||||
(define fixed (dynamic-require fpath 'fixed))
|
||||
(define err (dynamic-require fpath 'the-error))
|
||||
(printf "\n-------------------------------------------------------------------\n")
|
||||
(printf "~a has the error: ~a\n\n" fpath err)
|
||||
|
@ -194,12 +193,18 @@
|
|||
t)))
|
||||
(cond
|
||||
[(equal? gen-type 'fixed)
|
||||
(define some-failed?
|
||||
(for/or ([t (in-list fixed)])
|
||||
(define ok? (check (and (tc t) t)))
|
||||
(not ok?)))
|
||||
(unless some-failed?
|
||||
(error 'fixed "Expected some term to fail, but didn't find one in ~a" fixed))]
|
||||
(define small-counter-example
|
||||
(dynamic-require
|
||||
fpath 'small-counter-example
|
||||
(λ ()
|
||||
(error 'fixed "contains no small counter example"))))
|
||||
(unless (tc small-counter-example)
|
||||
(error 'fixed "The counter example doesn't type-check: ~e"
|
||||
small-counter-example))
|
||||
(define ok? (check small-counter-example))
|
||||
(when ok?
|
||||
(error 'fixed "Expected ~e to fail on check, but it didn't"
|
||||
small-counter-example))]
|
||||
[(equal? gen-type 'grammar)
|
||||
(run/spawn-generations fpath verbose? no-errs? (λ () (gen-and-type gen-term))
|
||||
check seconds gen-type)]
|
||||
|
|
Loading…
Reference in New Issue
Block a user