clean up requires/provides, see other mlish language additions below
- fix bug where recursive tyvar did not have #%type tag - records - optional field names in type definitions - reuse prefixes by default - list fns - provide explicit inst (need it for ho poly fns) - if now allows non-false instead of bool - small inference fixes - add rw ocaml tests, ch6, up to "polymorphic variants"
This commit is contained in:
Stephen Chang
parent
dc3767c844
commit
5c5f500f39
|
|
@ -55,7 +55,8 @@
|
|||
(define-typed-syntax if
|
||||
[(~and ifstx (_ e_tst e1 e2))
|
||||
#:with τ-expected (get-expected-type #'ifstx)
|
||||
#:with e_tst- (⇑ e_tst as Bool)
|
||||
; #:with e_tst- (⇑ e_tst as Bool)
|
||||
#:with [e_tst- _] (infer+erase #'e_tst)
|
||||
#:with e1_ann #'(add-expected e1 τ-expected)
|
||||
#:with e2_ann #'(add-expected e2 τ-expected)
|
||||
#:with (e1- τ1) (infer+erase #'e1_ann)
|
||||
|
|
|
|||
|
|
@ -1,7 +1,8 @@
|
|||
#lang s-exp "typecheck.rkt"
|
||||
(extends "sysf.rkt" #:except #%datum ∀ Λ inst)
|
||||
(reuse String #%datum #:from "stlc+reco+var.rkt")
|
||||
(reuse current-kind? ∀★ ∀★? ★ ★? kind? ∀ Λ inst define-type-alias #:from "fomega.rkt")
|
||||
(require (only-in "fomega.rkt" current-kind? ∀★? ★? kind?))
|
||||
(reuse ★ ∀ Λ inst define-type-alias ∀★ #:from "fomega.rkt")
|
||||
|
||||
; same as fomega2.rkt --- λ and #%app works as both regular and type versions,
|
||||
; → is both type and kind --- but reuses parts of fomega.rkt,
|
||||
|
|
|
|||
|
|
@ -1,6 +1,6 @@
|
|||
#lang s-exp "typecheck.rkt"
|
||||
(extends "stlc+reco+sub.rkt" #:except +)
|
||||
(reuse ∀? [∀ sysf:∀] [~∀ ~sysf:∀] #:from "sysf.rkt")
|
||||
(require (rename-in (only-in "sysf.rkt" ∀? ∀ ~∀) [~∀ ~sysf:∀] [∀ sysf:∀]))
|
||||
|
||||
;; System F<:
|
||||
;; Types:
|
||||
|
|
|
|||
|
|
@ -1,8 +1,9 @@
|
|||
#lang s-exp "typecheck.rkt"
|
||||
(extends "ext-stlc.rkt" #:except #%app λ → + - void = zero? sub1 add1 not
|
||||
#:rename [~→ ~ext-stlc:→])
|
||||
(reuse ∀ ~∀ ∀? Λ #:from "sysf.rkt")
|
||||
(reuse cons [head hd] [tail tl] nil [isnil nil?] List ~List list #:from "stlc+cons.rkt")
|
||||
(require (only-in "sysf.rkt" ∀ ~∀ ∀? Λ))
|
||||
(reuse cons [head hd] [tail tl] nil [isnil nil?] List list #:from "stlc+cons.rkt")
|
||||
(require (only-in "stlc+cons.rkt" ~List))
|
||||
(reuse tup × proj #:from "stlc+tup.rkt")
|
||||
(reuse define-type-alias #:from "stlc+reco+var.rkt")
|
||||
(provide hd tl nil?)
|
||||
|
|
|
|||
|
|
@ -4,19 +4,22 @@
|
|||
|
||||
(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)
|
||||
#;(prefix-in stlc+rec-iso: (only-in "stlc+rec-iso.rkt" define)))
|
||||
;(reuse cons [head hd] [tail tl] nil [isnil nil?] List ~List list #:from "stlc+cons.rkt")
|
||||
;(reuse tup × proj #:from "stlc+tup.rkt")
|
||||
;(reuse define-type-alias #:from "stlc+reco+var.rkt")
|
||||
;(provide hd tl nil?)
|
||||
(provide → × tup proj define-type-alias)
|
||||
(provide define-type match)
|
||||
;(reuse [inst sysf:inst] #:from "sysf.rkt")
|
||||
(require (rename-in (only-in "sysf.rkt" inst) [inst sysf:inst]))
|
||||
(provide inst)
|
||||
(require (only-in "ext-stlc.rkt" →?))
|
||||
(require (only-in "sysf.rkt" ~∀ ∀ ∀? Λ))
|
||||
(reuse × tup proj define-type-alias #:from "stlc+rec-iso.rkt")
|
||||
(require (only-in "stlc+rec-iso.rkt" ~× ×?))
|
||||
(provide → define-type match)
|
||||
(provide (rename-out [ext-stlc:and and] [ext-stlc:#%datum #%datum]))
|
||||
(reuse reverse [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]))
|
||||
(reuse member length reverse list-ref cons nil isnil head tail list #:from "stlc+cons.rkt")
|
||||
(require (only-in "stlc+cons.rkt" ~List List? List))
|
||||
(provide List)
|
||||
(reuse ref deref := Ref #:from "stlc+box.rkt")
|
||||
(require (rename-in (only-in "stlc+reco+var.rkt" tup proj ×)
|
||||
[tup rec] [proj get] [× ××]))
|
||||
(provide rec get ××)
|
||||
|
||||
;; ML-like language
|
||||
;; - top level recursive functions
|
||||
|
|
@ -53,7 +56,7 @@
|
|||
#:when (free-identifier=? #'y x)
|
||||
#'τ]
|
||||
[(_ . rst) (lookup x #'rst)]
|
||||
[() false]))
|
||||
[() #f]))
|
||||
;; solve for tyvars Xs used in tys, based on types of args in stx
|
||||
;; infer types of args left-to-right:
|
||||
;; - use intermediate results to help infer remaining arg types
|
||||
|
|
@ -122,7 +125,7 @@
|
|||
((current-type-eval) #`(∀ #,Xs (ext-stlc:→ τ ... τ_out)))
|
||||
Xs))
|
||||
#:with g (add-orig (generate-temporary #'f) #'f)
|
||||
#:with e_ann #'(add-expected e τ_out)
|
||||
#:with e_ann #'(add-expected e τ_out) ; must be macro bc t_out may have (currently unbound) tyvars
|
||||
#:with (τ+orig ...) (stx-map (λ (t) (add-orig t t)) #'(τ ... τ_out))
|
||||
#:with (~∀ Xs (~ext-stlc:→ in ...)) ((current-type-eval) #'(∀ Ys (ext-stlc:→ τ+orig ...)))
|
||||
#`(begin
|
||||
|
|
@ -144,20 +147,23 @@
|
|||
#:with Name2 (add-orig #'(NewName) #'Name)
|
||||
#`(begin
|
||||
(define-type Name2 . #,(subst #'Name2 #'Name #'rst))
|
||||
(define-type-alias Name Name2))]
|
||||
(stlc+rec-iso:define-type-alias Name Name2))]
|
||||
[(_ (Name:id X:id ...)
|
||||
;; constructors must have the form (Cons τ ...)
|
||||
;; but the first ~or clause accepts 0-arg constructors as ids
|
||||
;; the ~and is required to bind the duplicate Cons ids (see Ryan's email)
|
||||
(~and (~or (~and IdCons:id (~parse (Cons τ ...) #'(IdCons)))
|
||||
(Cons τ ...))) ...)
|
||||
(~and (~or (~and IdCons:id
|
||||
(~parse (Cons [fld (~datum :) τ] ...) #'(IdCons)))
|
||||
(Cons [fld (~datum :) τ] ...)
|
||||
(~and (Cons τ ...)
|
||||
(~parse (fld ...) (generate-temporaries #'(τ ...)))))) ...)
|
||||
#:with RecName (generate-temporary #'Name)
|
||||
#:with NameExpander (format-id #'Name "~~~a" #'Name)
|
||||
#:with (StructName ...) (generate-temporaries #'(Cons ...))
|
||||
#:with ((e_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
|
||||
#:with ((e_arg- ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
|
||||
#:with ((τ_arg ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
|
||||
#:with ((fld ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
|
||||
; #:with ((fld ...) ...) (stx-map generate-temporaries #'((τ ...) ...))
|
||||
#:with ((acc ...) ...) (stx-map (λ (S fs) (stx-map (λ (f) (format-id S "~a-~a" S f)) fs))
|
||||
#'(StructName ...) #'((fld ...) ...))
|
||||
#:with (Cons? ...) (stx-map mk-? #'(StructName ...))
|
||||
|
|
@ -167,7 +173,11 @@
|
|||
#`(begin
|
||||
(define-type-constructor Name
|
||||
#:arity = #,(stx-length #'(X ...))
|
||||
#:extra-info (X ...) (λ (RecName) ('Cons Cons? [acc τ/rec] ...) ...)
|
||||
#:extra-info (X ...)
|
||||
(λ (RecName)
|
||||
(let-syntax ([RecName (make-rename-transformer
|
||||
(assign-type #'RecName #'#%type))])
|
||||
('Cons Cons? [acc τ/rec] ...) ...))
|
||||
#:no-provide)
|
||||
(struct StructName (fld ...) #:reflection-name 'Cons #:transparent) ...
|
||||
(define-syntax (Cons stx)
|
||||
|
|
@ -246,6 +256,7 @@
|
|||
(define-syntax (match stx)
|
||||
(syntax-parse stx #:datum-literals (with ->)
|
||||
[(_ e with . clauses)
|
||||
;; e is tuple
|
||||
#:with [e- ty_e] (infer+erase #'e)
|
||||
#:when (×? #'ty_e)
|
||||
#:with (~× ty ...) #'ty_e
|
||||
|
|
@ -259,6 +270,7 @@
|
|||
(⊢ (let ([z e-])
|
||||
(let ([x- (acc z)] ...) e_body-))
|
||||
: ty_body)]
|
||||
;; e is variant
|
||||
[(_ e with . clauses)
|
||||
#:fail-when (null? (syntax->list #'clauses)) "no clauses"
|
||||
#:with [e- τ_e] (infer+erase #'e)
|
||||
|
|
@ -267,8 +279,11 @@
|
|||
-> e_c_un] ...) ; un = unannotated with expected ty
|
||||
#'clauses ; clauses must stay in same order
|
||||
;; len #'clauses maybe > len #'info, due to guards
|
||||
#:with ((~literal #%plain-lambda) (RecName) . info-body)
|
||||
(get-extra-info #'τ_e)
|
||||
#:with ((~literal #%plain-lambda) (RecName)
|
||||
((~literal let-values) ()
|
||||
((~literal let-values) ()
|
||||
. info-body)))
|
||||
(get-extra-info #'τ_e)
|
||||
#:with info-unfolded (subst #'τ_e #'RecName #'info-body)
|
||||
#:with ((_ ((~literal quote) ConsAll) . _) ...) #'info-body
|
||||
#:fail-unless (set=? (syntax->datum #'(Clause ...))
|
||||
|
|
@ -411,7 +426,8 @@
|
|||
else_b ... else_body]
|
||||
#:defaults ([else_test #'#f])))
|
||||
#:with (test- ...) (⇑s (test ...) as Bool)
|
||||
#:with ([body- ty_body] ...) (infers+erase #'(body ...))
|
||||
#:with ty-expected (get-expected-type stx)
|
||||
#:with ([body- ty_body] ...) (infers+erase #'((add-expected body ty-expected) ...))
|
||||
#:with (([b- ty_b] ...) ...) (stx-map infers+erase #'((b ...) ...))
|
||||
#:when (same-types? #'(ty_body ...))
|
||||
#:with τ_out (stx-car #'(ty_body ...))
|
||||
|
|
@ -630,6 +646,11 @@
|
|||
#:with s- (⇑ str as String)
|
||||
#:with ([e- ty] ...) (infers+erase #'(e ...))
|
||||
(⊢ (printf s- e- ...) : Unit)])
|
||||
(define-typed-syntax format
|
||||
[(_ str e ...)
|
||||
#:with s- (⇑ str as String)
|
||||
#:with ([e- ty] ...) (infers+erase #'(e ...))
|
||||
(⊢ (format s- e- ...) : String)])
|
||||
(define-typed-syntax display
|
||||
[(_ e)
|
||||
#:with [e- _] (infer+erase #'e)
|
||||
|
|
@ -663,7 +684,7 @@
|
|||
(define-typed-syntax begin/tc #:export-as begin
|
||||
[(_ body ... b)
|
||||
#:with expected (get-expected-type stx)
|
||||
#:with b_ann (add-expected-type #'b #'expected)
|
||||
#:with b_ann #'(add-expected b expected)
|
||||
#'(ext-stlc:begin body ... b_ann)])
|
||||
|
||||
;; hash
|
||||
|
|
@ -674,7 +695,7 @@
|
|||
#: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)))])
|
||||
: (Sequence (stlc+rec-iso:× ty_k ty_v)))])
|
||||
|
||||
; mutable hashes
|
||||
(define-typed-syntax hash
|
||||
|
|
@ -767,7 +788,7 @@
|
|||
#:with x- (⇑ x as Int)
|
||||
#:with y- (⇑ y as Int)
|
||||
(⊢ (call-with-values (λ () (quotient/remainder x- y-)) list)
|
||||
: (× Int Int))])
|
||||
: (stlc+rec-iso:× Int Int))])
|
||||
(define-primop quotient : (→ Int Int Int))
|
||||
|
||||
(define-typed-syntax set!
|
||||
|
|
@ -783,7 +804,7 @@
|
|||
#:with x-ty (format-id #'x "~a-ty" #'x) ; TODO: use hash-code to generate this tmp
|
||||
#'(begin
|
||||
(provide x)
|
||||
(define-type-alias x-ty ty_x)
|
||||
(stlc+rec-iso:define-type-alias x-ty ty_x)
|
||||
(provide x-ty))])
|
||||
(define-typed-syntax require-typed
|
||||
[(_ x:id #:from mod)
|
||||
|
|
@ -796,3 +817,19 @@
|
|||
(define-base-type Regexp)
|
||||
(define-primop regexp-match : (→ Regexp String (List String)))
|
||||
(define-primop regexp : (→ String Regexp))
|
||||
|
||||
(define-typed-syntax equal?
|
||||
[(_ e1 e2)
|
||||
#:with [e1- ty1] (infer+erase #'e1)
|
||||
#:with [e2- ty2] (infer+erase #'(add-expected e2 ty1))
|
||||
#:fail-unless (typecheck? #'ty1 #'ty2) "arguments to equal? have different types"
|
||||
(⊢ (equal? e1- e2-) : Bool)])
|
||||
|
||||
(define-syntax (inst stx)
|
||||
(syntax-parse stx
|
||||
[(_ e ty ...)
|
||||
#:with [e- ty_e] (infer+erase #'(sysf:inst e ty ...))
|
||||
#:with ty_out (if (→? #'ty_e)
|
||||
#'(∀ () ty_e)
|
||||
#'ty_e)
|
||||
(⊢ e- : ty_out)]))
|
||||
|
|
|
|||
|
|
@ -18,7 +18,14 @@
|
|||
; minimal type inference
|
||||
[ni:id #:with expected-τ (get-expected-type #'ni)
|
||||
#:when (syntax-e #'expected-τ) ; 'expected-type property exists (ie, not false)
|
||||
#:with (~List τ) (local-expand #'expected-τ 'expression null) ; canonicalize
|
||||
#:with ty_lst (local-expand #'expected-τ 'expression null) ; canonicalize
|
||||
#:fail-unless (List? #'ty_lst)
|
||||
(raise (exn:fail:type:infer
|
||||
(format "~a (~a:~a): Inferred ~a type for nil, which is not a List."
|
||||
(syntax-source stx) (syntax-line stx) (syntax-column stx)
|
||||
(type->str #'ty_lst))
|
||||
(current-continuation-marks)))
|
||||
#:with (~List τ) #'ty_lst
|
||||
(⊢ null : (List τ))]
|
||||
[_:id #:fail-when #t
|
||||
(raise (exn:fail:type:infer
|
||||
|
|
@ -66,3 +73,19 @@
|
|||
#:with (e- τ-lst) (infer+erase #'e)
|
||||
#:when (List? #'τ-lst)
|
||||
(⊢ (reverse e-) : τ-lst)])
|
||||
(define-typed-syntax length
|
||||
[(_ e)
|
||||
#:with (e- τ-lst) (infer+erase #'e)
|
||||
#:when (List? #'τ-lst)
|
||||
(⊢ (length e-) : Int)])
|
||||
(define-typed-syntax list-ref
|
||||
[(_ e n)
|
||||
#:with (e- (ty)) (⇑ e as List)
|
||||
#:with n- (⇑ n as Int)
|
||||
(⊢ (list-ref e- n-) : ty)])
|
||||
(define-typed-syntax member
|
||||
[(_ v e)
|
||||
#:with (e- (ty)) (⇑ e as List)
|
||||
#:with [v- ty_v] (infer+erase #'(add-expected v ty))
|
||||
#:when (typecheck? #'ty_v #'ty)
|
||||
(⊢ (member v- e-) : Bool)])
|
||||
|
|
|
|||
|
|
@ -1,7 +1,8 @@
|
|||
#lang s-exp "typecheck.rkt"
|
||||
(extends "stlc+sub.rkt" #:except #%datum)
|
||||
(extends "stlc+cons.rkt" #:except + #%datum and tup × proj ~× list)
|
||||
(reuse tup × proj ~× #:from "stlc+tup.rkt")
|
||||
(reuse tup × proj #:from "stlc+tup.rkt")
|
||||
(require (only-in "stlc+tup.rkt" ~×))
|
||||
|
||||
;; Calculus for occurrence typing.
|
||||
;; - Types can be simple, or sets of simple types
|
||||
|
|
@ -232,7 +233,7 @@
|
|||
;; -- THIS CASE BELONGS IN A NEW FILE
|
||||
[(_ [τ0+:type ? (unop x-stx:id n-stx:nat)] e1 e2)
|
||||
;; 1. Check that we're using a known eliminator
|
||||
#:when (free-identifier=? #'proj #'unop)
|
||||
#:when (free-identifier=? #'stlc+tup:proj #'unop)
|
||||
;; 2. Make sure we're filtering with a valid type
|
||||
#:with f (type->filter #'τ0+)
|
||||
;; 3. Typecheck the eliminator call. Remember the type & apply the filter.
|
||||
|
|
@ -242,8 +243,8 @@
|
|||
;; 4. Build the +/- types for our identifier; the thing we apply the elim. + test to
|
||||
;; We know that x has a pair type because (proj x n) typechecked
|
||||
#:with (x (~× τi* ...)) (infer+erase #'x-stx)
|
||||
#:with τ+ #`(× #,@(replace-at (syntax->list #'(τi* ...)) (syntax-e #'n-stx) #'τ0+))
|
||||
#:with τ- #`(× #,@(replace-at (syntax->list #'(τi* ...)) (syntax-e #'n-stx) #'τ0-))
|
||||
#:with τ+ #`(stlc+tup:× #,@(replace-at (syntax->list #'(τi* ...)) (syntax-e #'n-stx) #'τ0+))
|
||||
#:with τ- #`(stlc+tup:× #,@(replace-at (syntax->list #'(τi* ...)) (syntax-e #'n-stx) #'τ0-))
|
||||
;; 5. Check the branches with the refined types
|
||||
#:with [x1 e1+ τ1] (infer/ctx+erase #'([x-stx : τ+]) #'e1)
|
||||
#:with [x2 e2+ τ2] (infer/ctx+erase #'([x-stx : τ-]) #'e2)
|
||||
|
|
|
|||
|
|
@ -13,11 +13,16 @@
|
|||
|
||||
(define-typed-syntax tup
|
||||
[(_ e ...)
|
||||
#:with ([e- τ] ...) (infers+erase #'(e ...))
|
||||
#:with ty-expected (get-expected-type stx)
|
||||
#:with (e_ann ...) (if (syntax-e #'ty-expected)
|
||||
(syntax-parse (local-expand #'ty-expected 'expression null)
|
||||
[(~× ty_exp ...) #'((add-expected e ty_exp) ...)])
|
||||
#'(e ...))
|
||||
#:with ([e- τ] ...) (infers+erase #'(e_ann ...))
|
||||
(⊢ (list e- ...) : (× τ ...))])
|
||||
(define-typed-syntax proj
|
||||
[(_ e_tup n:nat)
|
||||
#:with [e_tup- τs_tup] (⇑ e_tup as ×)
|
||||
#:fail-unless (< (syntax-e #'n) (stx-length #'τs_tup)) "index too large"
|
||||
(⊢ (list-ref e_tup- n) : #,(stx-list-ref #'τs_tup (syntax-e #'n)))])
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -112,10 +112,8 @@
|
|||
(or #t "2")
|
||||
#:with-msg
|
||||
"Expected expression \"2\" to have Bool type, got: String")
|
||||
(typecheck-fail
|
||||
(if "true" 1 2)
|
||||
#:with-msg
|
||||
"Expected expression \"true\" to have Bool type, got: String")
|
||||
;; 2016-03-10: change if to work with non-false vals
|
||||
(check-type (if "true" 1 2) : Int -> 1)
|
||||
(typecheck-fail
|
||||
(if #t 1 "2")
|
||||
#:with-msg
|
||||
|
|
|
|||
|
|
@ -310,10 +310,8 @@
|
|||
(or #t "2")
|
||||
#:with-msg
|
||||
"Expected expression \"2\" to have Bool type, got: String")
|
||||
(typecheck-fail
|
||||
(if "true" 1 2)
|
||||
#:with-msg
|
||||
"Expected expression \"true\" to have Bool type, got: String")
|
||||
;; 2016-03-10: change if to work with non-false vals
|
||||
(check-type (if "true" 1 2) : Int -> 1)
|
||||
(typecheck-fail
|
||||
(if #t 1 "2")
|
||||
#:with-msg
|
||||
|
|
|
|||
|
|
@ -367,10 +367,8 @@
|
|||
(or #t "2")
|
||||
#:with-msg
|
||||
"Expected expression \"2\" to have Bool type, got: String")
|
||||
(typecheck-fail
|
||||
(if "true" 1 2)
|
||||
#:with-msg
|
||||
"Expected expression \"true\" to have Bool type, got: String")
|
||||
;; 2016-03-09: now ok
|
||||
(check-type (if "true" 1 2) : Int -> 1)
|
||||
(typecheck-fail
|
||||
(if #t 1 "2")
|
||||
#:with-msg
|
||||
|
|
|
|||
|
|
@ -103,11 +103,20 @@
|
|||
[ths (map (λ ([c : Color]) (creature c ch-meet ch-res)) inits)])
|
||||
(map (λ ([c : Color]) (channel-get ch-res)) inits)))
|
||||
|
||||
(check-type (go 100 (list Blue Red Yellow))
|
||||
: (List Result)
|
||||
-> (list (list 67 0)
|
||||
(list 66 0)
|
||||
(list 67 0)))
|
||||
(define res1 (go 100 (list Blue Red Yellow)))
|
||||
|
||||
(define (check-res1 [r : Result] -> Bool)
|
||||
(match r with
|
||||
[met same -> (or (= met 66) (= met 67))]))
|
||||
|
||||
(check-type (length res1) : Int -> 3)
|
||||
|
||||
(check-type (check-res1 (list-ref res1 0)) : Bool -> #t)
|
||||
(check-type (check-res1 (list-ref res1 1)) : Bool -> #t)
|
||||
(check-type (check-res1 (list-ref res1 2)) : Bool -> #t)
|
||||
;; -> (list (list 67 0)
|
||||
;; (list 66 0)
|
||||
;; (list 67 0)))
|
||||
|
||||
(check-type (go 1000 (list Blue Red Yellow Red Yellow Blue))
|
||||
: (List Result)
|
||||
|
|
|
|||
295
tapl/tests/mlish/term.mlish
Normal file
295
tapl/tests/mlish/term.mlish
Normal file
|
|
@ -0,0 +1,295 @@
|
|||
#lang s-exp "../../mlish.rkt"
|
||||
(require "../rackunit-typechecking.rkt")
|
||||
|
||||
;; from chap 6 of RW OCaml
|
||||
|
||||
;; checks:
|
||||
;; - nested recursive types (see expr)
|
||||
;; - labeled adts
|
||||
;; - records
|
||||
;; - ho polymorphic fn argument
|
||||
|
||||
(define-type BasicColor
|
||||
Black
|
||||
Red
|
||||
Green
|
||||
Yellow
|
||||
Blue
|
||||
Magenta
|
||||
Cyan
|
||||
White)
|
||||
|
||||
(check-type Cyan : BasicColor)
|
||||
|
||||
(check-type (list Blue Magenta Red) : (List BasicColor))
|
||||
|
||||
(define (basic-color->int [c : BasicColor] -> Int)
|
||||
(match c with
|
||||
[Black -> 0] [Red -> 1] [Green -> 2] [Yellow -> 3]
|
||||
[Blue -> 4] [Magenta -> 5] [Cyan -> 6] [White -> 7]))
|
||||
|
||||
(define (map [f : (→ X Y)] [lst : (List X)] -> (List Y))
|
||||
(if (isnil lst)
|
||||
nil
|
||||
(cons (f (head lst)) (map f (tail lst)))))
|
||||
|
||||
(check-type (map basic-color->int (list Blue Red))
|
||||
: (List Int) -> (list 4 1))
|
||||
|
||||
(define (color-by-number [n : Int] [txt : String] -> String)
|
||||
(format "\e[38;5;~am~a\e[0m" n txt))
|
||||
|
||||
(define blue
|
||||
(color-by-number (basic-color->int Blue) "Blue"))
|
||||
|
||||
(check-type blue : String -> "\e[38;5;4mBlue\e[0m")
|
||||
|
||||
(printf "Hello ~a World!\n" blue)
|
||||
|
||||
(define-type Weight Regular Bold)
|
||||
(define-type Color
|
||||
(Basic BasicColor Weight)
|
||||
(RGB Int Int Int)
|
||||
(Gray Int))
|
||||
|
||||
(check-type (list (RGB 250 70 70) (Basic Green Regular))
|
||||
: (List Color))
|
||||
|
||||
(define (color->int [c : Color] -> Int)
|
||||
(match c with
|
||||
[Basic bc w ->
|
||||
(let ([base (match w with [Bold -> 8] [Regular -> 0])])
|
||||
(+ base (basic-color->int bc)))]
|
||||
[RGB r g b ->
|
||||
(+ 16 (+ b (+ (* g 6) (* r 36))))]
|
||||
[Gray i -> (+ 232 i)]))
|
||||
|
||||
(define (color-print [c : Color] [s : String] -> Unit)
|
||||
(printf "~a\n" (color-by-number (color->int c) s)))
|
||||
|
||||
(color-print (Basic Red Bold) "A bold red!")
|
||||
(color-print (Gray 4) "A muted gray...")
|
||||
|
||||
;; refactoring Color and Weight
|
||||
(define-type NewColor
|
||||
(NewBasic BasicColor)
|
||||
(NewBold BasicColor)
|
||||
(NewRGB Int Int Int)
|
||||
(NewGray Int))
|
||||
|
||||
(typecheck-fail
|
||||
(match (NewGray 1) with
|
||||
[Basic bc w ->
|
||||
(let ([base (match w with [Bold -> 8] [Regular -> 0])])
|
||||
(+ base (basic-color->int bc)))]
|
||||
[RGB r g b ->
|
||||
(+ 16 (+ b (+ (* g 6) (* r 36))))]
|
||||
[Gray i -> (+ 232 i)])
|
||||
#:with-msg
|
||||
"clauses not exhaustive; missing: NewGray, NewRGB, NewBold, NewBasic")
|
||||
|
||||
(typecheck-fail
|
||||
(match (NewGray 1) with
|
||||
[NewBasic bc w ->
|
||||
(let ([base (match w with [Bold -> 8] [Regular -> 0])])
|
||||
(+ base (basic-color->int bc)))]
|
||||
[NewRGB r g b ->
|
||||
(+ 16 (+ b (+ (* g 6) (* r 36))))]
|
||||
[NewGray i -> (+ 232 i)])
|
||||
#:with-msg "clauses not exhaustive; missing: NewBold")
|
||||
|
||||
(typecheck-fail
|
||||
(match (NewGray 1) with
|
||||
[NewBasic bc w ->
|
||||
(let ([base (match w with [Bold -> 8] [Regular -> 0])])
|
||||
(+ base (basic-color->int bc)))]
|
||||
[NewBold bc -> 1]
|
||||
[NewRGB r g b ->
|
||||
(+ 16 (+ b (+ (* g 6) (* r 36))))]
|
||||
[NewGray i -> (+ 232 i)])) ; todo: better err msg for arity
|
||||
|
||||
(check-type
|
||||
(match (NewGray 1) with
|
||||
[NewBasic bc -> (basic-color->int bc)]
|
||||
[NewBold bc -> (+ 8 (basic-color->int bc))]
|
||||
[NewRGB r g b ->
|
||||
(+ 16 (+ b (+ (* g 6) (* r 36))))]
|
||||
[NewGray i -> (+ 232 i)]) : Int)
|
||||
|
||||
;; 2016-03-09: match currently does not support else
|
||||
(define-type Details
|
||||
(Logon [user : String] [credentials : String])
|
||||
(Heartbeat [status : String])
|
||||
(LogEntry [important? : Bool] [msg : String]))
|
||||
|
||||
(define-type-alias SessionID String)
|
||||
(define-type-alias Time String)
|
||||
(define-type-alias Common (× SessionID Time))
|
||||
|
||||
(define-type-alias Msg (× Common Details))
|
||||
|
||||
(define (foldl [f : (→ X Y Y)] [init : Y] [lst : (List X)] -> Y)
|
||||
(if (isnil lst)
|
||||
init
|
||||
(foldl f (f (head lst) init) (tail lst))))
|
||||
|
||||
(define (msgs-for-user [user : String] [msgs : (List Msg)] -> (List Msg))
|
||||
(match
|
||||
(foldl
|
||||
(λ ([m : Msg] [res : (× (List Msg) (List SessionID))])
|
||||
(match res with
|
||||
[ms_out ids_out ->
|
||||
(match m with
|
||||
[common details ->
|
||||
(match common with
|
||||
[id t ->
|
||||
(match details with
|
||||
[Logon u c -> (if (string=? u user)
|
||||
(tup (cons m ms_out) (cons id ids_out))
|
||||
res)]
|
||||
[Heartbeat st -> (if (member id ids_out)
|
||||
(tup (cons m ms_out) ids_out)
|
||||
res)]
|
||||
[LogEntry i? lmgs -> (if (member id ids_out)
|
||||
(tup (cons m ms_out) ids_out)
|
||||
res)])])])]))
|
||||
(tup nil nil)
|
||||
msgs) with
|
||||
[msgs ids -> (reverse msgs)]))
|
||||
|
||||
;; this is incomplete (and wrong, eg logentry has wrong arity) code in the book
|
||||
(define (handle-msg [state : Int] [msg : Msg] -> String)
|
||||
(match msg with
|
||||
[common details ->
|
||||
(match details with
|
||||
[LogEntry i? lmsg -> lmsg]
|
||||
[Logon u c -> u]
|
||||
[Heartbeat s -> s])]))
|
||||
|
||||
;; expr example
|
||||
(define-type (Expr X)
|
||||
(Base X)
|
||||
(Const Bool)
|
||||
(And (List (Expr X)))
|
||||
(Or (List (Expr X)))
|
||||
(Not (Expr X)))
|
||||
|
||||
(define-type MailField To From CC Date Subject)
|
||||
|
||||
(define-type-alias MailPred (×× [field : MailField]
|
||||
[contains? : String]))
|
||||
|
||||
(define (test [f : MailField] [c? : String] -> (Expr MailPred))
|
||||
(Base (rec [field = f] [contains? = c?])))
|
||||
|
||||
(check-type (rec [field = To] [contains = "doligez"])
|
||||
: (×× [field : MailField] [contains : String]))
|
||||
|
||||
(check-type (get (rec [field = To] [contains = "doligez"]) field)
|
||||
: MailField -> To)
|
||||
|
||||
(check-type
|
||||
(And (list (Or (list (Base (rec [field = To] [contains? = "doligez"]))
|
||||
(Base (rec [field = CC] [contains? = "doligez"]))))
|
||||
(Base (rec [field = Subject] [contains? = "runtime"]))))
|
||||
: (Expr MailPred))
|
||||
|
||||
(define (andmap [f : (→ X Bool)] [lst : (List X)] -> Bool)
|
||||
(if (isnil lst)
|
||||
#t
|
||||
(and (f (head lst)) (andmap f (tail lst)))))
|
||||
(define (ormap [f : (→ X Bool)] [lst : (List X)] -> Bool)
|
||||
(if (isnil lst)
|
||||
#f
|
||||
(or (f (head lst)) (ormap f (tail lst)))))
|
||||
|
||||
(define (filter [p? : (→ X Bool)] [lst : (List X)] -> (List X))
|
||||
(if (isnil lst)
|
||||
nil
|
||||
(if (p? (head lst))
|
||||
(cons (head lst) (filter p? (tail lst)))
|
||||
(filter p? (tail lst)))))
|
||||
|
||||
(define (eval [e : (Expr X)] [eval-base : (→ X Bool)] -> Bool)
|
||||
(let ([eval2 (λ ([e : (Expr X)]) (eval e eval-base))])
|
||||
(match e with
|
||||
[Base base -> (eval-base base)]
|
||||
[Const b -> b]
|
||||
[And es -> (andmap eval2 es)]
|
||||
[Or es -> (ormap eval2 es)]
|
||||
[Not e -> (not (eval2 e))])))
|
||||
|
||||
(define (andfn [lst : (List (Expr X))] -> (Expr X))
|
||||
(if (member (Const #f) lst)
|
||||
(Const #f)
|
||||
(let ([lst2
|
||||
(filter (λ ([x : (Expr X)]) (not (equal? x (Const #t)))) lst)])
|
||||
(if (isnil lst2)
|
||||
(Const #t)
|
||||
(if (isnil (tail lst2))
|
||||
(head lst2)
|
||||
(And lst2))))))
|
||||
|
||||
(define (orfn [lst : (List (Expr X))] -> (Expr X))
|
||||
(if (member (Const #t) lst)
|
||||
(Const #t)
|
||||
(let ([lst2
|
||||
(filter (λ ([x : (Expr X)]) (not (equal? x (Const #f)))) lst)])
|
||||
(if (isnil lst2)
|
||||
(Const #f)
|
||||
(if (isnil (tail lst2))
|
||||
(head lst2)
|
||||
(And lst2))))))
|
||||
|
||||
(define (notfn [e : (Expr X)] -> (Expr X))
|
||||
(match e with
|
||||
[Base b -> (Not e)]
|
||||
[Const b -> (Const (not b))]
|
||||
[And es -> (Not e)]
|
||||
[Or es -> (Not e)]
|
||||
[Not e2 -> (Not e)]))
|
||||
|
||||
(define (simplify [e : (Expr X)] -> (Expr X))
|
||||
(match e with
|
||||
[Base b -> e]
|
||||
[Const x -> e]
|
||||
[And es -> (andfn (map (inst simplify X) es))]
|
||||
[Or es -> (orfn (map (inst simplify X) es))]
|
||||
[Not e -> (notfn (simplify e))]))
|
||||
|
||||
(check-type
|
||||
(simplify (Not (And (list (Or (list (Base "it's snowing")
|
||||
(Const #t)))
|
||||
(Base "it's raining")))))
|
||||
: (Expr String)
|
||||
-> (Not (Base "it's raining")))
|
||||
|
||||
(check-type
|
||||
(simplify (Not (And (list (Or (list (Base "it's snowing")
|
||||
(Const #t)))
|
||||
(Not (Not (Base "it's raining")))))))
|
||||
: (Expr String)
|
||||
-> (Not (Not (Not (Base "it's raining")))))
|
||||
|
||||
(define (notfn2 [e : (Expr X)] -> (Expr X))
|
||||
(match e with
|
||||
[Const b -> (Const (not b))]
|
||||
[Base b -> (Not e)]
|
||||
[And es -> (Not e)]
|
||||
[Or es -> (Not e)]
|
||||
[Not e -> e]))
|
||||
|
||||
(define (simplify2 [e : (Expr X)] -> (Expr X))
|
||||
(match e with
|
||||
[Base b -> e]
|
||||
[Const x -> e]
|
||||
[And es -> (andfn (map (inst simplify2 X) es))]
|
||||
[Or es -> (orfn (map (inst simplify2 X) es))]
|
||||
[Not e -> (notfn2 (simplify2 e))]))
|
||||
|
||||
(check-type
|
||||
(simplify2 (Not (And (list (Or (list (Base "it's snowing")
|
||||
(Const #t)))
|
||||
(Not (Not (Base "it's raining")))))))
|
||||
: (Expr String)
|
||||
-> (Not (Base "it's raining")))
|
||||
|
|
@ -13,3 +13,6 @@
|
|||
(require "mlish/knuc.mlish")
|
||||
(require "mlish/matrix.mlish")
|
||||
(require "mlish/nbody.mlish")
|
||||
|
||||
;; from rw ocaml
|
||||
(require "mlish/term.mlish")
|
||||
|
|
|
|||
|
|
@ -111,12 +111,25 @@
|
|||
(define-syntax reuse
|
||||
(syntax-parser
|
||||
[(_ (~or x:id [old:id new:id]) ... #:from base-lang)
|
||||
#:with pre (or (let ([dat (syntax-e #'base-lang)])
|
||||
(and (string? dat)
|
||||
(string->symbol (drop-file-ext dat))))
|
||||
#'base-lang)
|
||||
#:with pre: (format-id #'pre "~a:" #'pre)
|
||||
#`(begin
|
||||
(require (rename-in (only-in base-lang x ... old ...) [old new] ...))
|
||||
(require (rename-in (only-in base-lang old ...) [old new] ...))
|
||||
(require (prefix-in pre: (only-in base-lang x ...)))
|
||||
(provide (filtered-out
|
||||
(let* ([excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))])
|
||||
(let* ([pre-str #,(string-append (drop-file-ext (syntax-e #'base-lang)) ":")]
|
||||
[pre-str-len (string-length pre-str)]
|
||||
[drop-pre (λ (s) (substring s pre-str-len))]
|
||||
[excluded (map (compose symbol->string syntax->datum) (syntax->list #'(new ...)))])
|
||||
(λ (name)
|
||||
(and (not (member name excluded)) name)))
|
||||
(define out-name
|
||||
(or (and (string-prefix? name pre-str)
|
||||
(drop-pre name))
|
||||
name))
|
||||
(and (not (member out-name excluded)) out-name)))
|
||||
(all-from-out base-lang))))]))
|
||||
|
||||
(define-syntax add-expected
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user