From cd4305ca4f395a183450b762b2c7e5be0fe4d7db Mon Sep 17 00:00:00 2001 From: Sam Tobin-Hochstadt Date: Tue, 31 Mar 2009 03:33:04 +0000 Subject: [PATCH] Add refinement types. Add `parse-commmand-line' svn: r14372 --- .../tests/typed-scheme/succeed/cmdline.ss | 38 +++++++++++++++++++ .../typed-scheme/succeed/refinement-even.ss | 15 ++++++++ collects/typed-scheme/env/init-envs.ss | 3 ++ collects/typed-scheme/private/base-env.ss | 13 +++++++ collects/typed-scheme/private/parse-type.ss | 9 ++++- collects/typed-scheme/private/prims.ss | 7 +++- collects/typed-scheme/private/subtype.ss | 3 ++ .../typed-scheme/private/type-contract.ss | 7 +++- collects/typed-scheme/rep/type-rep.ss | 11 ++++++ .../typed-scheme/typecheck/internal-forms.ss | 2 + .../typed-scheme/typecheck/tc-toplevel.ss | 13 ++++++- 11 files changed, 116 insertions(+), 5 deletions(-) create mode 100644 collects/tests/typed-scheme/succeed/cmdline.ss create mode 100644 collects/tests/typed-scheme/succeed/refinement-even.ss diff --git a/collects/tests/typed-scheme/succeed/cmdline.ss b/collects/tests/typed-scheme/succeed/cmdline.ss new file mode 100644 index 0000000000..61faa7b46f --- /dev/null +++ b/collects/tests/typed-scheme/succeed/cmdline.ss @@ -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: + ; return the argument as a filename to compile + filename)) \ No newline at end of file diff --git a/collects/tests/typed-scheme/succeed/refinement-even.ss b/collects/tests/typed-scheme/succeed/refinement-even.ss new file mode 100644 index 0000000000..8d6d96935f --- /dev/null +++ b/collects/tests/typed-scheme/succeed/refinement-even.ss @@ -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) \ No newline at end of file diff --git a/collects/typed-scheme/env/init-envs.ss b/collects/typed-scheme/env/init-envs.ss index 0b64510527..71a8707f36 100644 --- a/collects/typed-scheme/env/init-envs.ss +++ b/collects/typed-scheme/env/init-envs.ss @@ -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))] diff --git a/collects/typed-scheme/private/base-env.ss b/collects/typed-scheme/private/base-env.ss index d6f49abebd..399202cc27 100644 --- a/collects/typed-scheme/private/base-env.ss +++ b/collects/typed-scheme/private/base-env.ss @@ -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))) diff --git a/collects/typed-scheme/private/parse-type.ss b/collects/typed-scheme/private/parse-type.ss index 8cc2d1cef4..187db130a5 100644 --- a/collects/typed-scheme/private/parse-type.ss +++ b/collects/typed-scheme/private/parse-type.ss @@ -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)]) diff --git a/collects/typed-scheme/private/prims.ss b/collects/typed-scheme/private/prims.ss index 3988110b43..6bc35521bc 100644 --- a/collects/typed-scheme/private/prims.ss +++ b/collects/typed-scheme/private/prims.ss @@ -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 ...)))])) \ No newline at end of file + (provide i ...)))])) + +(define-syntax (declare-refinement stx) + (syntax-parse stx + [(_ p:id) + (quasisyntax/loc stx #,(internal #'(declare-refinement-internal p)))])) \ No newline at end of file diff --git a/collects/typed-scheme/private/subtype.ss b/collects/typed-scheme/private/subtype.ss index 0c2ffdb722..68de466788 100644 --- a/collects/typed-scheme/private/subtype.ss +++ b/collects/typed-scheme/private/subtype.ss @@ -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*)] diff --git a/collects/typed-scheme/private/type-contract.ss b/collects/typed-scheme/private/type-contract.ss index b74c331316..aedd0f9257 100644 --- a/collects/typed-scheme/private/type-contract.ss +++ b/collects/typed-scheme/private/type-contract.ss @@ -65,6 +65,8 @@ #`(listof #,(t->c elem-ty))] [(? (lambda (e) (eq? Any-Syntax e))) #'syntax?] [(Base: sym cnt) cnt] + [(Refinement: par p? cert) + #`(and/c #,(t->c par) (flat-contract #,(cert p?)))] [(Union: elems) (with-syntax ([cnts (map t->c elems)]) @@ -103,7 +105,7 @@ [(Pair: t1 t2) #`(cons/c #,(t->c t1) #,(t->c t2))] [(Opaque: p? cert) - #`(flat-contract #,(cert p?))] + #`(flat-named-contract (quote #,(syntax-e p?)) #,(cert p?))] [(F: v) (cond [(assoc v (vars)) => (if pos? second third)] [else (int-err "unknown var: ~a" v)])] [(Poly: vs (and b (Function: _))) @@ -125,7 +127,8 @@ [(Instance: _) #'(is-a?/c object%)] [(Class: _ _ _) #'(subclass?/c object%)] [(Value: '()) #'null?] - [(Struct: _ _ _ _ #f pred? cert) (cert pred?)] + [(Struct: _ _ _ _ #f pred? cert) + #`(flat-named-contract '#,(syntax-e pred?) #,(cert pred?))] [(Syntax: (Base: 'Symbol _)) #'identifier?] [(Syntax: t) #`(syntax/c #,(t->c t))] [(Value: v) #`(flat-named-contract #,(format "~a" v) (lambda (x) (equal? x '#,v)))] diff --git a/collects/typed-scheme/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index ea2d2017bb..1a6aae4155 100644 --- a/collects/typed-scheme/rep/type-rep.ss +++ b/collects/typed-scheme/rep/type-rep.ss @@ -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]) diff --git a/collects/typed-scheme/typecheck/internal-forms.ss b/collects/typed-scheme/typecheck/internal-forms.ss index b85dd96c1e..a0ce6e9cb0 100644 --- a/collects/typed-scheme/typecheck/internal-forms.ss +++ b/collects/typed-scheme/typecheck/internal-forms.ss @@ -11,4 +11,6 @@ define-typed-struct-internal define-typed-struct/exec-internal assert-predicate-internal + declare-refinement-internal :-internal) + diff --git a/collects/typed-scheme/typecheck/tc-toplevel.ss b/collects/typed-scheme/typecheck/tc-toplevel.ss index f0553c1e21..c415f38b1b 100644 --- a/collects/typed-scheme/typecheck/tc-toplevel.ss +++ b/collects/typed-scheme/typecheck/tc-toplevel.ss @@ -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)))