add enum generation to stlc

This commit is contained in:
Burke Fetscher 2014-02-17 14:57:27 -06:00
parent 10de717cb4
commit 0010a8ebae
12 changed files with 74 additions and 28 deletions

View File

@ -8,7 +8,6 @@
(define-runtime-path stlc "stlc") (define-runtime-path stlc "stlc")
(define-runtime-path stlc-sub "stlc-sub") (define-runtime-path stlc-sub "stlc-sub")
(define-runtime-path poly-stlc "poly-stlc") (define-runtime-path poly-stlc "poly-stlc")
(define-runtime-path rbtrees "rbtrees") (define-runtime-path rbtrees "rbtrees")
(define-runtime-path delim-cont "delim-cont") (define-runtime-path delim-cont "delim-cont")

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -245,6 +246,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/contract racket/contract
racket/match racket/match
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -245,6 +246,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -246,6 +247,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -246,6 +247,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -245,6 +246,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -245,6 +246,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -244,6 +245,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -245,6 +246,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/match racket/match
racket/contract racket/contract
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -245,6 +246,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -6,6 +6,7 @@
racket/list racket/list
racket/contract racket/contract
racket/match racket/match
math/base
"tut-subst.rkt") "tut-subst.rkt")
(provide (all-defined-out)) (provide (all-defined-out))
@ -246,6 +247,9 @@
[t-type (type-check term)]) [t-type (type-check term)])
(and (and
(= (length red-res) 1) (= (length red-res) 1)
(or (or
(equal? (car red-res) "error") (equal? (car red-res) "error")
(equal? t-type (type-check (car red-res)))))))) (equal? t-type (type-check (car red-res))))))))
(define (generate-enum-term)
(generate-term stlc M #:i-th (random-natural #e10e200)))

View File

@ -11,7 +11,9 @@
(define verbose #f) (define verbose #f)
(define output-file #f) (define output-file #f)
(define all-types '(search grammar search-gen search-gen-ref search-gen-enum search-gen-enum-ref)) (define all-types '(search grammar search-gen search-gen-ref
search-gen-enum search-gen-enum-ref
enum))
(define types '()) (define types '())
(define filename (define filename
@ -24,7 +26,7 @@
[("-o" "--output") out-file "Output file name" [("-o" "--output") out-file "Output file name"
(set! output-file out-file)] (set! output-file out-file)]
#:multi #:multi
[("-t" "--type") t "Generation type to run, one of: search, grammar, search-gen, search-gen-ref, search-gen-enum, search-gen-enum-ref" [("-t" "--type") t "Generation type to run, one of: search, grammar, search-gen, search-gen-ref, search-gen-enum, search-gen-enum-ref, enum"
(set! types (cons (string->symbol t) types))] (set! types (cons (string->symbol t) types))]
#:args filenames #:args filenames
(match filenames (match filenames
@ -100,24 +102,29 @@
((/ dev avg) . > . 0.1))) ((/ dev avg) . > . 0.1)))
(define (test-file fname verbose? no-errs? gen-type seconds) (define (test-file fname verbose? no-errs? gen-type seconds)
(define fpath (string->path fname)) (define tc (dynamic-require fname 'type-check))
(define tc (dynamic-require fpath 'type-check)) (define check (dynamic-require fname 'check))
(define check (dynamic-require fpath 'check)) (define gen-term (dynamic-require fname 'generate-M-term))
(define gen-term (dynamic-require fpath 'generate-M-term)) (define gen-typed-term (dynamic-require fname 'generate-typed-term))
(define gen-typed-term (dynamic-require fpath 'generate-typed-term)) (define typed-generator (dynamic-require fname 'typed-generator))
(define typed-generator (dynamic-require fpath 'typed-generator)) (define gen-enum (dynamic-require fname 'generate-enum-term))
(define err (dynamic-require fpath 'the-error)) (define err (dynamic-require fname 'the-error))
(printf "\n-------------------------------------------------------------------\n") (printf "\n-------------------------------------------------------------------\n")
(printf "~s has the error: ~a\n\n" fname err) (printf "~a has the error: ~a\n\n" fname err)
(printf "Running ~s....\n" fname) (printf "Running ~a....\n" fname)
(printf "Using generator: ~s\n" gen-type) (printf "Using generator: ~s\n" gen-type)
(define (gen-and-type gen)
(λ ()
(λ ()
(define t (gen))
(and (tc t)
t))))
(cond (cond
[(equal? gen-type 'grammar) [(equal? gen-type 'grammar)
(define (gen-and-type) (run-generations fname verbose? no-errs? (gen-and-type gen-term)
(define t (gen-term)) check seconds gen-type)]
(and (tc t) [(equal? gen-type 'enum)
t)) (run-generations fname verbose? no-errs? (gen-and-type gen-enum)
(run-generations fname verbose? no-errs? (λ () gen-and-type)
check seconds gen-type)] check seconds gen-type)]
[(equal? gen-type 'search) [(equal? gen-type 'search)
(run-generations fname verbose? no-errs? (λ () gen-typed-term) (run-generations fname verbose? no-errs? (λ () gen-typed-term)