suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

mlish: add hash, fl prims, str prims, output, and some other prims

Browse Source 
- allow begin exprs to have any type (not just unit)
- add fasta test
This commit is contained in:
Stephen Chang 2016-03-07 00:31:25 -05:00
parent ee6c0c11f7
commit f5a043b7e6
14 changed files with 278 additions and 19 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

8
tapl/ext-stlc.rkt
View File

@ -19,10 +19,14 @@
(define-base-type Bool)
(define-base-type String)
(define-base-type Float)
(define-base-type Char)
(define-typed-syntax #%datum
[(_ . b:boolean) (⊢ (#%datum . b) : Bool)]
[(_ . s:str) (⊢ (#%datum . s) : String)]
[(_ . f) #:when (flonum? (syntax-e #'f)) (⊢ (#%datum . f) : Float)]
[(_ . c:char) (⊢ (#%datum . c) : Char)]
[(_ . x) #'(stlc+lit:#%datum . x)])
(define-primop zero? : (→ Int Bool))
@ -68,7 +72,7 @@
(define-typed-syntax begin
[(_ e_unit ... e)
#:with (e_unit- ...) (⇑s (e_unit ...) as Unit)
#:with ([e_unit- _] ...) (infers+erase #'(e_unit ...)) ;(⇑s (e_unit ...) as Unit)
#:with (e- τ) (infer+erase #'e)
(⊢ (begin e_unit- ... e-) : τ)])
@ -117,4 +121,4 @@
"\n"))
(⊢ (letrec ([x- e-] ...) e_body-) : τ_body)])

106
tapl/mlish.rkt
View File

@ -1,7 +1,8 @@
#lang s-exp "typecheck.rkt"
(require (for-syntax syntax/id-set))
(require racket/fixnum racket/flonum)
(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let and #%datum begin
(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not let let* and #%datum begin
#:rename [~→ ~ext-stlc:→])
(reuse inst ~∀ ∀ ∀? Λ #:from "sysf.rkt")
(require (only-in "stlc+rec-iso.rkt" case fld unfld μ ~× × ×? ∨ var tup proj define-type-alias)
@ -13,7 +14,8 @@
(provide → × tup proj define-type-alias)
(provide define-type match)
(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
(reuse cons nil isnil head tail list List ~List List? #:from "stlc+cons.rkt")
(reuse [cons stlc:cons] nil isnil head tail [list stlc:list] List ~List List? #:from "stlc+cons.rkt")
(provide (rename-out [stlc:list list] [stlc:cons cons]))
;; ML-like language
;; - top level recursive functions
@ -342,6 +344,7 @@
(define-primop <= : (→ Int Int Bool))
(define-primop < : (→ Int Int Bool))
(define-primop > : (→ Int Int Bool))
(define-primop modulo : (→ Int Int Int))
(define-primop zero? : (→ Int Bool))
(define-primop sub1 : (→ Int Int))
(define-primop add1 : (→ Int Int))
@ -401,19 +404,28 @@
;; cond and other conditionals
(define-typed-syntax cond
[(_ [(~and test (~not (~datum else))) body] ...
(~optional [(~and (~datum else) (~parse else_test #'(ext-stlc:#%datum . #t))) else_body]
[(_ [(~and test (~not (~datum else))) b ... body] ...
(~optional
[(~and (~datum else)
(~parse else_test #'(ext-stlc:#%datum . #t)))
else_b ... else_body]
#:defaults ([else_test #'#f])))
#:with (test- ...) (⇑s (test ...) as Bool)
#:with ([body- ty_body] ...) (infers+erase #'(body ...))
#:with (([b- ty_b] ...) ...) (stx-map infers+erase #'((b ...) ...))
#:when (same-types? #'(ty_body ...))
#:with τ_out (stx-car #'(ty_body ...))
#:with [last-body- last-ty] (if (attribute else_body)
(infer+erase #'else_body)
(infer+erase #'(void)))
#:with ([last-b- last-b-ty] ...) (if (attribute else_body)
(infers+erase #'(else_b ...))
(infers+erase #'((void))))
#:when (or (not (attribute else_body))
(typecheck? #'last-ty #'τ_out))
(⊢ (cond [test- body-] ... [else_test last-body-]) : τ_out)])
(⊢ (cond [test- b- ... body-] ...
[else_test last-b- ... last-body-])
: τ_out)])
(define-typed-syntax when
[(_ test body ...)
#:with test- (⇑ test as Bool)
@ -448,7 +460,6 @@
#:with (th- (~∀ () (~ext-stlc:→ τ_out))) (infer+erase #'th)
(⊢ (thread th-) : Thread)])
(define-base-type Char)
(define-primop random : (→ Int Int))
(define-primop integer->char : (→ Int Char))
(define-primop string->number : (→ String Int))
@ -456,6 +467,11 @@
(define-primop sleep : (→ Int Unit))
(define-primop string=? : (→ String String Bool))
(define-typed-syntax string-append
[(_ . strs)
#:with strs- (⇑s strs as String)
(⊢ (string-append . strs-) : String)])
;; vectors
(define-type-constructor Vector)
@ -507,7 +523,7 @@
[(_ end)
#'(in-range/tc (ext-stlc:#%datum . 0) end (ext-stlc:#%datum . 1))]
[(_ start end)
#'(in-range/tc stat end (ext-stlc:#%datum . 1))]
#'(in-range/tc start end (ext-stlc:#%datum . 1))]
[(_ start end step)
#:with (e- ...) (⇑s (start end step) as Int)
(⊢ (in-range e- ...) : (Sequence Int))])
@ -538,6 +554,14 @@
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(x- ...) body- ty_body] (infer/ctx+erase #'([x : ty] ...) #'body)
(⊢ (for*/list ([x- e-] ...) body-) : (List ty_body))])
(define-typed-syntax for/fold
[(_ ([acc init]) ([x:id e] ...) body)
#:with [init- ty_init] (infer+erase #'init)
#:with ([e- (ty)] ...) (⇑s (e ...) as Sequence)
#:with [(acc- x- ...) body- ty_body]
(infer/ctx+erase #'([acc : ty_init][x : ty] ...) #'body)
#:when (typecheck? #'ty_body #'ty_init)
(⊢ (for/fold ([acc- init-]) ([x- e-] ...) body-) : ty_body)])
; printing and displaying
(define-typed-syntax printf
@ -571,9 +595,77 @@
: ty_body)]
[(_ ([x:id e] ...) body ...)
#'(ext-stlc:let ([x e] ...) (begin/tc body ...))])
(define-typed-syntax let*
[(_ ([x:id e] ...) body ...)
#'(ext-stlc:let* ([x e] ...) (begin/tc body ...))])
(define-typed-syntax begin/tc #:export-as begin
[(_ body ... b)
#:with expected (get-expected-type stx)
#:with b_ann (add-expected-type #'b #'expected)
#'(ext-stlc:begin body ... b_ann)])
;; hash
(define-type-constructor Hash #:arity = 2)
(define-typed-syntax in-hash
[(_ e)
#:with [e- (ty_k ty_v)] (⇑ e as Hash)
(⊢ (map (λ (k+v) (list (car k+v) (cdr k+v))) (hash->list e-))
; (⊢ (hash->list e-)
: (Sequence (× ty_k ty_v)))])
(define-typed-syntax hash
[(_ (~seq k v) ...)
#:with ([k- ty_k] ...) (infers+erase #'(k ...))
#:with ([v- ty_v] ...) (infers+erase #'(v ...))
#:when (same-types? #'(ty_k ...))
#:when (same-types? #'(ty_v ...))
#:with ty_key (stx-car #'(ty_k ...))
#:with ty_val (stx-car #'(ty_v ...))
(⊢ (make-immutable-hash (list (cons k- v-) ...)) : (Hash ty_key ty_val))])
(define-base-type String-Port)
(define-primop open-output-string : (→ String-Port))
(define-primop get-output-string : (→ String-Port String))
(define-typed-syntax write-string/tc #:export-as write-string
[(_ str out)
#'(write-string/tc str out (ext-stlc:#%datum . 0) (string-length/tc str))]
[(_ str out start end)
#:with str- (⇑ str as String)
#:with out- (⇑ out as String-Port)
#:with start- (⇑ start as Int)
#:with end- (⇑ end as Int)
(⊢ (write-string str- out- start- end-) : Unit)])
(define-typed-syntax string-length/tc #:export-as string-length
[(_ str)
#:with str- (⇑ str as String)
(⊢ (string-length str-) : Int)])
(define-primop make-string : (→ Int String))
(define-primop string-set! : (→ String Int Char Unit))
(define-primop string-ref : (→ String Int Char))
(define-typed-syntax string-copy!/tc #:export-as string-copy!
[(_ dest dest-start src)
#'(string-copy!/tc
dest dest-start src (ext-stlc:#%datum . 0) (string-length/tc src))]
[(_ dest dest-start src src-start src-end)
#:with dest- (⇑ dest as String)
#:with src- (⇑ src as String)
#:with dest-start- (⇑ dest-start as Int)
#:with src-start- (⇑ src-start as Int)
#:with src-end- (⇑ src-end as Int)
(⊢ (string-copy! dest- dest-start- src- src-start- src-end-) : Unit)])
(define-primop fl+ : (→ Float Float Float))
(define-primop fl* : (→ Float Float Float))
(define-primop flceiling : (→ Float Float))
(define-primop inexact->exact : (→ Float Int))
(define-primop char->integer : (→ Char Int))
(define-primop fx->fl : (→ Int Float))
(define-typed-syntax quotient+remainder
[(_ x y)
#:with x- (⇑ x as Int)
#:with y- (⇑ y as Int)
(⊢ (call-with-values (λ () (quotient/remainder x- y-)) list)
: (× Int Int))])

2
tapl/tests/exist-tests.rkt
View File

@ -298,7 +298,7 @@
;; begin
(typecheck-fail (begin))
(check-type (begin 1) : Int)
(typecheck-fail (begin 1 2 3))
;(typecheck-fail (begin 1 2 3))
(check-type (begin (void) 1) : Int ⇒ 1)
;;ascription

4
tapl/tests/ext-stlc-tests.rkt
View File

@ -25,7 +25,9 @@
(check-type (begin 1) : Int)
(typecheck-fail (begin) #:with-msg "expected more terms")
(typecheck-fail
;; 2016-03-06: begin terms dont need to be Unit
(check-type (begin 1 2 3) : Int)
#;(typecheck-fail
(begin 1 2 3)
#:with-msg "Expected expression 1 to have Unit type, got: Int")

4
tapl/tests/infer-tests.rkt
View File

@ -221,7 +221,9 @@
(check-type (begin 1) : Int)
(typecheck-fail (begin) #:with-msg "expected more terms")
(typecheck-fail
;; 2016-03-06: begin terms dont need to be Unit
(check-type (begin 1 2 3) : Int)
#;(typecheck-fail
(begin 1 2 3)
#:with-msg "Expected expression 1 to have Unit type, got: Int")

4
tapl/tests/mlish-tests.rkt
View File

@ -280,7 +280,9 @@
(check-type (begin 1) : Int)
(typecheck-fail (begin) #:with-msg "expected more terms")
(typecheck-fail
;; 2016-03-06: begin terms dont need to be Unit
(check-type (begin 1 2 3) : Int)
#;(typecheck-fail
(begin 1 2 3)
#:with-msg "Expected expression 1 to have Unit type, got: Int")

152
tapl/tests/mlish/fasta.mlish Normal file
View File

@ -0,0 +1,152 @@
#lang s-exp "../../mlish.rkt"
(require "../rackunit-typechecking.rkt")
(define +alu+
(string-append "GGCCGGGCGCGGTGGCTCACGCCTGTAATCCCAGCACTTTGG"
"GAGGCCGAGGCGGGCGGATCACCTGAGGTCAGGAGTTCGAGA"
"CCAGCCTGGCCAACATGGTGAAACCCCGTCTCTACTAAAAAT"
"ACAAAAATTAGCCGGGCGTGGTGGCGCGCGCCTGTAATCCCA"
"GCTACTCGGGAGGCTGAGGCAGGAGAATCGCTTGAACCCGGG"
"AGGCGGAGGTTGCAGTGAGCCGAGATCGCGCCACTGCACTCC"
"AGCCTGGGCGACAGAGCGAGACTCCGTCTCAAAAA"))
(check-type +alu+ : String)
(define IUB
(hash #\a 0.27 #\c 0.12 #\g 0.12 #\t 0.27 #\B 0.02
#\D 0.02 #\H 0.02 #\K 0.02 #\M 0.02 #\N 0.02
#\R 0.02 #\S 0.02 #\V 0.02 #\W 0.02 #\Y 0.02))
(check-type IUB : (Hash Char Float))
(define HOMOSAPIEN
(hash #\a 0.3029549426680 #\c 0.1979883004921
#\g 0.1975473066391 #\t 0.3015094502008))
(check-type HOMOSAPIEN : (Hash Char Float))
(define line-length 60)
(check-type line-length : Int)
(define (repeat-fasta [header : String][N : Int][sequence : String] -> String)
(let* ([out (open-output-string)]
[len (string-length sequence)]
[buf (make-string (+ len line-length))])
(string-copy! buf 0 sequence)
(string-copy! buf len sequence 0 line-length)
(write-string header out)
(let loop : String ([n N] [start 0])
(if (> n 0)
(let ([end (+ start (min n line-length))])
(write-string buf out start end)
(write-string "\n" out)
(loop (- n line-length) (if (> end len) (- end len) end)))
(get-output-string out)))))
(define IA 3877)
(define IC 29573)
(define IM 139968)
(define IM.0 (fx->fl IM))
(define V
(let ([v (make-vector IM)])
(for ([id (in-range IM)])
(vector-set! v id (modulo (+ IC (* id IA)) IM)))
v))
(check-type V : (Vector Int))
(define (random-next [cur : Int] -> Int) (vector-ref V cur))
(check-type (tup 0 0.0) : (× Int Float))
(check-type (in-hash IUB) : (Sequence (× Char Float)))
(define (make-lookup-table [frequency-table : (Hash Char Float)] -> String)
(let ([v (make-string IM)])
(for/fold ([cs (tup 0 0.0)])
([k+v (in-hash frequency-table)])
(match cs with
[c c. ->
(match k+v with
[key val ->
(let* ([c1. (fl+ c. (fl* IM.0 val))]
[c1 (inexact->exact (flceiling c1.))]
#;[b (char->integer key)])
(for ([i (in-range c c1)]) (string-set! v i key))
(tup c1 c1.))])]))
v))
(define (n-randoms [buf : String][out : String-Port][lookup : String]
[to : Int][R : Int] -> Int)
(let loop : Int ([n 0] [R R])
(if (< n to)
(let ([R (random-next R)])
(string-set! buf n (string-ref lookup R))
(loop (add1 n) R))
(begin (write-string buf out 0 (add1 to)) R))))
(define LF #\newline)
(define (make-line! [buf : String] [lookup : String]
[start : Int] [R : Int] -> Int)
(let ([end (+ start line-length)])
(string-set! buf end LF)
(let loop : Int ([n start] [R R])
(if (< n end)
(let ([R (random-next R)])
(string-set! buf n (string-ref lookup R))
(loop (add1 n) R))
R))))
(define (random-fasta [header : String] [N : Int]
[table : (Hash Char Float)] [R : Int]
-> (× Int String))
(let* ([buf (make-string (add1 line-length))]
[out (open-output-string)]
[lookup-str (make-lookup-table table)]
[full-lines+last (quotient+remainder N line-length)]
[C
(let* ([len+1 (add1 line-length)]
[buflen (* len+1 IM)]
[buf2 (make-string buflen)])
(let loop : String ([R R] [i 0])
(if (< i buflen)
(loop (make-line! buf2 lookup-str i R) (+ i len+1))
buf2)))])
(string-set! buf line-length LF)
(write-string header out)
(tup
(match full-lines+last with
[full-lines last ->
(let loop : Int ([i full-lines] [R R])
(if (> i IM)
(begin (write-string C out) (loop (- i IM) R))
(let loop : Int ([i i] [R R])
(cond
[(> i 0)
(loop
(sub1 i)
(n-randoms buf out lookup-str line-length R))]
[(> last 0)
(string-set! buf last LF)
(n-randoms buf out lookup-str last R)]
[else R]))))])
(get-output-string out))))
(define n 10)
(check-type (repeat-fasta ">ONE Homo sapiens alu\n" (* n 2) +alu+) : String
-> ">ONE Homo sapiens alu\nGGCCGGGCGCGGTGGCTCAC\n")
(define res1
(random-fasta ">TWO IUB ambiguity codes\n" (* n 3) IUB 42))
(define res2
(match res1 with
[R str ->
(random-fasta ">THREE Homo sapiens frequency\n" (* n 5) HOMOSAPIEN R)]))
(check-type (proj res1 1) : String
-> ">TWO IUB ambiguity codes\ntaaaWKatgWRattaNBttctNagggcgWt\n")
;; should be cttBtatcatatgctaKggNcataaaSatg ?
(proj res1 0)
(check-type (proj res2 1) : String
-> (string-append ">THREE Homo sapiens frequency\n"
"agggctccaaatcataaagaggaatatattattacacgattagaaaccca\n"))
;; should be taaatcttgtgcttcgttagaagtctcgactacgtgtagcctagtgtttg ?

1
tapl/tests/run-all-mlish-tests.rkt
View File

@ -6,3 +6,4 @@
(require "mlish/ack.mlish")
(require "mlish/ary.mlish")
(require "mlish/fannkuch.mlish")
(require "mlish/fasta.mlish")

6
tapl/tests/stlc+box-tests.rkt
View File

@ -166,7 +166,11 @@
;; begin
(typecheck-fail (begin))
(check-type (begin 1) : Int)
(typecheck-fail (begin 1 2 3))
;; 2016-03-06: begin terms dont need to be Unit
(check-type (begin 1 2 3) : Int)
#;(typecheck-fail
(begin 1 2 3)
#:with-msg "Expected expression 1 to have Unit type, got: Int")
(check-type (begin (void) 1) : Int ⇒ 1)
;;ascription

2
tapl/tests/stlc+cons-tests.rkt
View File

@ -160,7 +160,7 @@
;; begin
(typecheck-fail (begin))
(check-type (begin 1) : Int)
(typecheck-fail (begin 1 2 3))
;(typecheck-fail (begin 1 2 3))
(check-type (begin (void) 1) : Int ⇒ 1)
;;ascription

2
tapl/tests/stlc+effect-tests.rkt
View File

@ -167,7 +167,7 @@
;; begin
(typecheck-fail (begin))
(check-type (begin 1) : Int)
(typecheck-fail (begin 1 2 3))
;(typecheck-fail (begin 1 2 3))
(check-type (begin (void) 1) : Int ⇒ 1)
;;ascription

2
tapl/tests/stlc+rec-iso-tests.rkt
View File

@ -178,7 +178,7 @@
;; begin
(typecheck-fail (begin))
(check-type (begin 1) : Int)
(typecheck-fail (begin 1 2 3))
;(typecheck-fail (begin 1 2 3))
(check-type (begin (void) 1) : Int ⇒ 1)
;;ascription

2
tapl/tests/stlc+reco+var-tests.rkt
View File

@ -163,7 +163,7 @@
;; begin
(typecheck-fail (begin))
(check-type (begin 1) : Int)
(typecheck-fail (begin 1 2 3))
;(typecheck-fail (begin 1 2 3))
(check-type (begin (void) 1) : Int ⇒ 1)
;;ascription

2
tapl/tests/stlc+tup-tests.rkt
View File

@ -38,7 +38,7 @@
;; begin
(typecheck-fail (begin))
(check-type (begin 1) : Int)
(typecheck-fail (begin 1 2 3))
;(typecheck-fail (begin 1 2 3))
(check-type (begin (void) 1) : Int ⇒ 1)
;;ascription