From f844cb8b920574c6bb66e178f5b1b5fbac8f5575 Mon Sep 17 00:00:00 2001 From: Asumu Takikawa Date: Tue, 24 Jun 2014 17:30:14 -0400 Subject: [PATCH] Add support for typechecking contracted functions --- .../typecheck/tc-app-combined.rkt | 4 +- .../typecheck/tc-app/signatures.rkt | 3 ++ .../typecheck/tc-app/tc-app-contracts.rkt | 40 +++++++++++++++++++ .../typecheck/tc-app/tc-app-keywords.rkt | 14 ++++++- .../typecheck/tc-app/tc-app-main.rkt | 4 +- .../typed-racket/typecheck/tc-expr-unit.rkt | 8 +++- .../typed-racket/typecheck/tc-toplevel.rkt | 15 +++++++ 7 files changed, 82 insertions(+), 6 deletions(-) create mode 100644 pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt index c207871d24..fe6fb00ba9 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app-combined.rkt @@ -9,6 +9,7 @@ "tc-app/tc-app-objects.rkt" "tc-app/tc-app-special.rkt" "tc-app/tc-app-values.rkt" + "tc-app/tc-app-contracts.rkt" "tc-app/tc-app-main.rkt" "signatures.rkt") @@ -23,4 +24,5 @@ tc-app-hetero@ tc-app-list@ tc-app-apply@ (() tc-app-values@) tc-app-keywords@ - tc-app-objects@ tc-app-eq@ tc-app-lambda@ tc-app-special@)) + tc-app-objects@ tc-app-eq@ tc-app-lambda@ tc-app-special@ + tc-app-contracts@)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/signatures.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/signatures.rkt index ed1a3ee642..e7b325b626 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/signatures.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/signatures.rkt @@ -36,3 +36,6 @@ (define-signature tc-app-special^ ([cond-contracted tc/app-special checker/c])) +(define-signature tc-app-contracts^ + ([cond-contracted tc/app-contracts checker/c])) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt new file mode 100644 index 0000000000..1f57d0bdf5 --- /dev/null +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-contracts.rkt @@ -0,0 +1,40 @@ +#lang racket/unit + +;; This module provides custom type-checking rules for the expansion +;; of contracted values + +(require "../../utils/utils.rkt" + "signatures.rkt" + "utils.rkt" + syntax/parse syntax/stx racket/match + racket/dict + racket/format + (env global-env) + (typecheck signatures) + (types base-abbrev resolve subtype union utils) + (rep type-rep) + (utils tc-utils) + (for-template racket/base + ;; shift -1 because it's provided +1 + racket/contract/private/provide)) + +(import tc-expr^) +(export tc-app-contracts^) + +(define-tc/app-syntax-class (tc/app-contracts expected) + (pattern (ctc-id:id blame e ...) + ;; check that this is an application from the contract system + #:when (contract-rename-id-property #'ctc-id) + (check-contract #'ctc-id #'(e ...) expected))) + +;; Assume that the contracted thing is of the same type the type +;; environment assigned to the exported identifier. Note that this +;; is only sound if the contract is a chaperone contract, so don't +;; put things in the base type environment if they have impersonator +;; contracts installed. +(define (check-contract orig-value-id other-args expected) + (tc-expr/check #`(#%plain-app + #,(contract-rename-id-property orig-value-id) + . #,other-args) + expected)) + diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt index 7fc378b001..9e9af4e091 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-keywords.rkt @@ -10,7 +10,10 @@ (rep type-rep) (utils tc-utils) (r:infer infer) - (for-label racket/base)) + (for-label racket/base) + ;; adjusted -1 since it's provided for-syntax + (only-in (for-template racket/contract/private/provide) + contract-neg-party-property)) (import tc-expr^) @@ -24,10 +27,17 @@ ((#%plain-app cpce s-kp fn kpe kws num) kw-list (#%plain-app list . kw-arg-list) - . pos-args)) + . *pos-args)) #:declare cpce (id-from 'checked-procedure-check-and-extract 'racket/private/kw) #:declare s-kp (id-from 'struct:keyword-procedure 'racket/private/kw) #:declare kpe (id-from 'keyword-procedure-extract 'racket/private/kw) + ;; If this application is of a module boundary contract function or not + ;; If #t, then the contract system has inserted an extra argument which we + ;; need to ignore + #:attr boundary-ctc? (contract-neg-party-property #'fn) + #:with pos-args (if (attribute boundary-ctc?) + (stx-cdr #'*pos-args) + #'*pos-args) (match (tc-expr #'fn) [(tc-result1: (Poly: vars diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt index c2a8c026de..de1df0a981 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-app/tc-app-main.rkt @@ -12,7 +12,8 @@ (import tc-expr^ tc-app-keywords^ tc-app-hetero^ tc-app-list^ tc-app-apply^ tc-app-values^ - tc-app-objects^ tc-app-eq^ tc-app-lambda^ tc-app-special^) + tc-app-objects^ tc-app-eq^ tc-app-lambda^ tc-app-special^ + tc-app-contracts^) (export tc-app^) (define-tc/app-syntax-class (tc/app-regular* expected) @@ -34,6 +35,7 @@ tc/app-objects tc/app-lambda tc/app-special + tc/app-contracts tc/app-regular*) ;; the main dispatching function diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt index d538a2cd77..23e82d9072 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-expr-unit.rkt @@ -17,7 +17,9 @@ (only-in racket/list split-at) (typecheck internal-forms tc-envops) ;; Needed for current implementation of typechecking letrec-syntax+values - (for-template (only-in racket/base letrec-values)) + (for-template (only-in racket/base letrec-values) + ;; see tc-app-contracts.rkt + racket/contract/private/provide) (for-label (only-in '#%paramz [parameterization-key pz:pk]) (only-in racket/private/class-internal find-method/who))) @@ -35,7 +37,9 @@ ;; tc-id : identifier -> tc-results (define/cond-contract (tc-id id) (--> identifier? full-tc-results/c) - (let* ([ty (lookup-type/lexical id)]) + (define rename-id (contract-rename-id-property id)) + (define id* (or rename-id id)) + (let* ([ty (lookup-type/lexical id*)]) (ret ty (make-FilterSet (-not-filter (-val #f) id) (-filter (-val #f) id)) diff --git a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt index 2bbf0a4c95..431ed3c0e6 100644 --- a/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt +++ b/pkgs/typed-racket-pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt @@ -18,6 +18,7 @@ (for-template (only-in syntax/location quote-module-name) racket/base + racket/contract/private/provide (env env-req))) (provide/cond-contract @@ -103,6 +104,10 @@ (register-scoped-tvars #'t.id (parse-literal-alls #'t.type)) (list)] + ;; definitions lifted from contracts should be ignored + [(define-values (lifted) expr) + #:when (contract-lifted-property #'expr) + (list)] ;; values definitions [(define-values (var ...) expr) @@ -150,6 +155,11 @@ #:literals (define-values begin) [(~or _:ignore^ _:ignore-some^) (list)] + ;; definitions lifted from contracts should be ignored + [(define-values (lifted) expr) + #:when (contract-lifted-property #'expr) + (list)] + [(define-values (var ...) expr) (define vars (syntax->list #'(var ...))) (syntax-parse vars @@ -211,6 +221,11 @@ ;; module* is not expanded, so it doesn't have a `#%plain-module-begin` [(module* n spec body ...) 'no-type] + ;; definitions lifted from contracts should be ignored + [(define-values (lifted) expr) + #:when (contract-lifted-property #'expr) + 'no-type] + ;; definitions just need to typecheck their bodies [(define-values () expr) (tc-expr/check #'expr (ret empty))