From 474ead72a964437ad4973e263c9f560516a11181 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 original commit: cd4305ca4f395a183450b762b2c7e5be0fe4d7db --- .../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 ++ collects/typed-scheme/rep/type-rep.ss | 11 ++++++ .../typed-scheme/typecheck/internal-forms.ss | 2 + .../typed-scheme/typecheck/tc-toplevel.ss | 13 ++++++- 10 files changed, 111 insertions(+), 3 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 00000000..61faa7b4 --- /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 00000000..8d6d9693 --- /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 0b645105..71a8707f 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 d6f49abe..399202cc 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 8cc2d1ce..187db130 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 3988110b..6bc35521 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 0c2ffdb7..68de4667 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/rep/type-rep.ss b/collects/typed-scheme/rep/type-rep.ss index ea2d2017..1a6aae41 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 b85dd96c..a0ce6e9c 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 f0553c1e..c415f38b 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)))