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

Add refinement types.

Browse Source 
Add `parse-commmand-line'

svn: r14372

original commit: cd4305ca4f395a183450b762b2c7e5be0fe4d7db
This commit is contained in:
Sam Tobin-Hochstadt 2009-03-31 03:33:04 +00:00
parent f288f98416
commit 474ead72a9
10 changed files with 111 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

38
collects/tests/typed-scheme/succeed/cmdline.ss Normal file
View File

@ -0,0 +1,38 @@
#lang typed-scheme
(require scheme/cmdline)
(: version-str String)
(define version-str "0.1")
(current-command-line-arguments (vector "counter.mch"))
(: verbose-mode (Parameter Boolean))
(define verbose-mode (make-parameter #f))
(: optimize-level (Parameter Integer))
(define optimize-level (make-parameter 0))
(: model-checking-mode (Parameter Any))
(define model-checking-mode (make-parameter 'sat))
(: file-to-model-check String)
(define file-to-model-check
(command-line
#:program "eboc" ;; Should be name of executable
#:once-each
[("-v" "--verbose") "Compile with verbose messages"
(verbose-mode #t)]
[("-m" "--mode") #{mode : String} "Mode to run the model checker on (sat, satbin)"
(model-checking-mode (string-append mode))]
#:once-any
[("-o" "--optimize-1") "Compile with optimization level 1"
(optimize-level 1)]
["--optimize-2" (; show help on separate lines
"Compile with optimization level 2,"
"which includes all of level 1")
(optimize-level 2)]
#:args (#{filename : String}) ; expect one command-line argument: <filename>
; return the argument as a filename to compile
filename))

15
collects/tests/typed-scheme/succeed/refinement-even.ss Normal file
View File

@ -0,0 +1,15 @@
#lang typed-scheme
(declare-refinement even?)
(define-type-alias Even (Refinement even?))
(: x Integer)
(define x 4)
(: y Even)
(define y (if (even? x) x (error 'bad)))
(: f (Even -> String))
(define (f e) (format "~a" e))
(f y)

3
collects/typed-scheme/env/init-envs.ss vendored
View File

@ -29,6 +29,9 @@
`(make-Struct ,(sub name) ,(sub parent) ,(sub flds) ,(sub proc) ,(sub poly?) (quote-syntax ,pred-id) (syntax-local-certifier))]
[(App: rator rands stx) `(make-App ,(sub rator) ,(sub rands) (quote-syntax ,stx))]
[(Opaque: pred cert) `(make-Opaque (quote-syntax ,pred) (syntax-local-certifier))]
[(Refinement: parent pred cert) `(make-Refinement ,(sub parent)
(quote-syntax ,pred)
(syntax-local-certifier))]
[(Mu-name: n b) `(make-Mu ,(sub n) ,(sub b))]
[(Poly-names: ns b) `(make-Poly (list ,@(map sub ns)) ,(sub b))]
[(PolyDots-names: ns b) `(make-PolyDots (list ,@(map sub ns)) ,(sub b))]

13
collects/typed-scheme/private/base-env.ss
View File

@ -545,6 +545,19 @@
[list->string ((-lst -Char) . -> . -String)]
[string->list (-String . -> . (-lst -Char))]
[sort (-poly (a) ((-lst a) (a a . -> . B) . -> . (-lst a)))]
[find-system-path (Sym . -> . -Path)]
;; scheme/cmdline
[parse-command-line
(let ([mode-sym (one-of/c 'once-each 'once-any 'multi 'final 'help-labels)])
(-polydots (b a)
(cl->* (-Pathlike
(Un (-lst -String) (-vec -String))
(-lst (-pair mode-sym (-lst (-lst Univ))))
((list Univ) [a a] . ->... . b)
(-lst -String)
. -> . b))))]
;; scheme/list
[last-pair (-poly (a) ((-mu x (Un a (-val '()) (-pair a x)))

9
collects/typed-scheme/private/parse-type.ss
View File

@ -10,7 +10,7 @@
"union.ss"
syntax/stx
stxclass stxclass/util
(env type-environments type-name-env type-alias-env)
(env type-environments type-name-env type-alias-env lexical-env)
"type-utils.ss"
(prefix-in t: "base-types-extra.ss")
scheme/match
@ -300,6 +300,13 @@
(map list
(map syntax-e (syntax->list #'(mname ...)))
(map parse-type (syntax->list #'(mty ...)))))]
[(Refinement p?)
(and (eq? (syntax-e #'Refinement) 'Refinement)
(identifier? #'p?))
(match (lookup-type/lexical #'p?)
[(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
(make-Refinement dom #'p? (syntax-local-certifier))]
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
[(Instance t)
(eq? (syntax-e #'Instance) 'Instance)
(let ([v (parse-type #'t)])

7
collects/typed-scheme/private/prims.ss
View File

@ -407,4 +407,9 @@ This file defines two sorts of primitives. All of them are provided into any mod
[(_ [i:id t] ...)
(syntax/loc stx
(begin (: i t) ...
(provide i ...)))]))
(provide i ...)))]))
(define-syntax (declare-refinement stx)
(syntax-parse stx
[(_ p:id)
(quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))]))

3
collects/typed-scheme/private/subtype.ss
View File

@ -293,6 +293,9 @@
;; single values shouldn't actually happen, but they're just like the type
[(list t (Values: (list t*))) (int-err "BUG - singleton values type~a" (make-Values (list t*)))]
[(list (Values: (list t)) t*) (int-err "BUG - singleton values type~a" (make-Values (list t)))]
;; A refinement is a subtype of its parent
[(list (Refinement: par _ _) t)
(subtype* A0 par t)]
;; subtyping on other stuff
[(list (Syntax: t) (Syntax: t*))
(subtype* A0 t t*)]

11
collects/typed-scheme/rep/type-rep.ss
View File

@ -209,6 +209,17 @@
;; value : Type
(dt Hashtable (key value) [#:key 'hash])
;; parent : Type
;; pred : Identifier
;; cert : Certifier
(dt Refinement (parent pred cert)
[#:key (Type-key parent)]
[#:intern (list parent (hash-id pred))]
[#:fold-rhs (*Refinement (type-rec-id parent) pred cert)]
[#:frees (free-vars* parent)
(free-idxs* parent)])
;; t : Type
(dt Syntax (t) [#:key 'syntax])

2
collects/typed-scheme/typecheck/internal-forms.ss
View File

@ -11,4 +11,6 @@
define-typed-struct-internal
define-typed-struct/exec-internal
assert-predicate-internal
declare-refinement-internal
:-internal)

13
collects/typed-scheme/typecheck/tc-toplevel.ss
View File

@ -9,7 +9,7 @@
"tc-structs.ss"
(rep type-rep)
(private type-utils type-effect-convenience parse-type type-annotation mutated-vars type-contract)
(env type-env init-envs type-name-env type-alias-env)
(env type-env init-envs type-name-env type-alias-env lexical-env)
(utils tc-utils)
"provide-handling.ss"
"def-binding.ss"
@ -38,6 +38,17 @@
;; type aliases have already been handled by an earlier pass
[(define-values () (begin (quote-syntax (define-type-alias-internal nm ty)) (#%plain-app values)))
(list)]
;; declare-refinement
[(define-values () (begin (quote-syntax (declare-refinement-internal pred)) (#%plain-app values)))
(match (lookup-type/lexical #'pred)
[(and t (Function: (list (arr: (list dom) rng #f #f '() _ _))))
(register-type #'pred
(make-pred-ty (list dom)
rng
(make-Refinement dom #'pred (syntax-local-certifier))))
(list)]
[t (tc-error "cannot declare refinement for non-predicate ~a" t)])]
;; require/typed
[(define-values () (begin (quote-syntax (require/typed-internal nm ty)) (#%plain-app values)))