From 992bf2ce5a0ee53246331cea04d338160c5f8593 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 27 Apr 2017 21:17:46 -0700 Subject: [PATCH 01/24] small stuff --- typed/rosette.rkt | 8 ++------ typed/rosette/base-forms.rkt | 2 +- typed/rosette/types.rkt | 10 +++++----- 3 files changed, 8 insertions(+), 12 deletions(-) diff --git a/typed/rosette.rkt b/typed/rosette.rkt index e1fb531..88a8000 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -1114,9 +1114,7 @@ [_:id ≫ -------- [⊢ [_ ≫ ro:&& ⇒ : - (Ccase-> (C→ Bool) - (C→ Bool Bool) - (C→ Bool Bool Bool))]]] + (C→* [] [] #:rest (Listof Bool) Bool)]]] [(_ e ...) ≫ [⊢ [e ≫ e- ⇐ : Bool] ...] -------- @@ -1125,9 +1123,7 @@ [_:id ≫ -------- [⊢ [_ ≫ ro:|| ⇒ : - (Ccase-> (C→ Bool) - (C→ Bool Bool) - (C→ Bool Bool Bool))]]] + (C→* [] [] #:rest (Listof Bool) Bool)]]] [(_ e ...) ≫ [⊢ [e ≫ e- ⇐ : Bool] ...] -------- diff --git a/typed/rosette/base-forms.rkt b/typed/rosette/base-forms.rkt index 2b89e74..917f5f2 100644 --- a/typed/rosette/base-forms.rkt +++ b/typed/rosette/base-forms.rkt @@ -537,7 +537,7 @@ -------- [⊢ (ro:apply f- lst-) ⇒ τ_out]] [(_ f:expr lst:expr) ≫ - [⊢ f ≫ f- ⇒ (~Ccase-> τ_f ...)] + [⊢ f ≫ f- ⇒ (~Ccase-> ~! τ_f ...)] [⊢ lst ≫ lst- ⇒ τ_lst] #:with τ_out (for/or ([τ_f (in-list (stx->list #'[τ_f ...]))]) diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 5bd0431..a4a7a85 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -133,7 +133,7 @@ #:with tys+ (stx-map (current-type-eval) #'tys) #:fail-unless (stx-andmap concrete? #'tys+) "CU requires concrete types" - #'(CU* . tys+)])) + (syntax/loc this-syntax (CU* . tys+))])) ;; user-facing symbolic U constructor: flattens and prunes (define-syntax (U stx) @@ -142,7 +142,7 @@ ;; canonicalize by expanding to U*, with only (sorted and pruned) leaf tys #:with ((~or (~U* ty1- ...) (~CU* ty2- ...) ty3-) ...) (stx-map (current-type-eval) #'tys) #:with tys- (prune+sort #'(ty1- ... ... ty2- ... ... ty3- ...)) - #'(U* . tys-)])) + (syntax/loc this-syntax (U* . tys-))])) ;; user-facing symbolic Term constructor: check solvable (define-syntax-parser Term @@ -171,7 +171,7 @@ [(_ τ:type) #:fail-when (and (not (Term*? #'τ.norm)) #'τ) "Constant requires a symbolic term type" - #'(Constant* τ.norm)])) + (syntax/loc this-syntax (Constant* τ.norm))])) ;; --------------------------------- @@ -279,7 +279,7 @@ #:with tys+ (stx-map (current-type-eval) #'tys) #:fail-unless (stx-andmap concrete-function-type? #'tys+) "Ccase-> require concrete function types" - #'(Ccase->* . tys+)])) + (syntax/loc this-syntax (Ccase->* . tys+))])) ;; TODO: What should case-> do when given symbolic function @@ -694,7 +694,7 @@ [((~CList . tys) (~CListof ty)) (for/and ([t (stx->list #'tys)]) (typecheck? t #'ty))] - ;; vectors, only immutable vectors are invariant + ;; vectors, only immutable vectors are covariant [((~CIVectorof ty1) (~CIVectorof ty2)) (typecheck? #'ty1 #'ty2)] [((~CIBoxof ty1) (~CIBoxof ty2)) From ffbc3d2ba5578327ec51eb372ca5d7ee38e50f98 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 20 Apr 2017 00:17:21 -0700 Subject: [PATCH 02/24] start --- typed/rosette/types.rkt | 20 ++++++++++++++++---- 1 file changed, 16 insertions(+), 4 deletions(-) diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index a4a7a85..dc442ed 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -16,6 +16,8 @@ (for-syntax concrete-function-type? ~C→ ~C→* ~Ccase-> C→? Ccase->?) + ;; Propositions for Occurrence typing + @ ;; Parameters CParamof ; TODO: symbolic Param not supported yet ;; List types @@ -228,6 +230,16 @@ (define-internal-type-constructor KwArg) ; #:arity = 2 +(define-internal-type-constructor Result) ; #:arity = 3 +(define-internal-type-constructor Prop/And) ; #:arity <= 0 +(define-internal-type-constructor Prop/IndexType) ; #:arity = 2 + +(define-syntax-parser Prop/Top [:id #'(Prop/And-)]) +(define-syntax-parser @ + #:datum-literals [:] + [(_ i:nat : τ:type) + #'(Prop/IndexType- 'i τ.norm)]) + (begin-for-syntax (begin-for-syntax (define-syntax-class expr* @@ -256,7 +268,7 @@ (~and opt-kws (~parse [pat_kw ...] (convert-opt-kws #'opt-kws))) (~NoRestArg) - pat_out)] + (~Result pat_out _ _))] [(_ [pat_in:expr* ...] [pat_kw:expr ...] #:rest pat_rst:expr pat_out:expr*) #:with opt-kws (generate-temporary 'opt-kws) #'(~C→*/internal @@ -264,7 +276,7 @@ (~and opt-kws (~parse [pat_kw ...] (convert-opt-kws #'opt-kws))) (~RestArg pat_rst) - pat_out)]))) + (~Result pat_out _ _))]))) ) ;; --------------------------------- @@ -445,7 +457,7 @@ [⊢ (C→*/internal- (MandArgs- τ_in- ...) (OptKws- (KwArg- (quote-syntax kw) τ_kw-) ...) (NoRestArg-) - τ_out-) + (Result- τ_out- Prop/Top Prop/Top)) ⇒ :: #%type]] [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] #:rest τ_rst τ_out:expr*) ≫ [⊢ [τ_in ≫ τ_in- ⇐ :: #%type] ...] @@ -456,7 +468,7 @@ [⊢ (C→*/internal- (MandArgs- τ_in- ...) (OptKws- (KwArg- (quote-syntax kw) τ_kw-) ...) (RestArg- τ_rst-) - τ_out-) + (Result- τ_out- Prop/Top Prop/Top)) ⇒ :: #%type]]) (define-typed-syntax C→ From 91e4c54a1c3e6146c5953f60fbd27a0b95bc882e Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 20 Apr 2017 17:10:26 -0700 Subject: [PATCH 03/24] continue --- test/typed-rosette/occurrence.rkt | 25 ++++++++ typed/rosette.rkt | 19 +++++-- typed/rosette/base-forms.rkt | 11 +++- typed/rosette/types.rkt | 95 ++++++++++++++++++++++++++++--- 4 files changed, 134 insertions(+), 16 deletions(-) create mode 100644 test/typed-rosette/occurrence.rkt diff --git a/test/typed-rosette/occurrence.rkt b/test/typed-rosette/occurrence.rkt new file mode 100644 index 0000000..eb6f164 --- /dev/null +++ b/test/typed-rosette/occurrence.rkt @@ -0,0 +1,25 @@ +#lang typed/rosette + +(require typed/rosette/types + (only-in typed/rosette/base-forms unsafe-assign-type) + (prefix-in $ rosette)) + +(define natural? + (unsafe-assign-type $exact-nonnegative-integer? + : (C→* [CInt] [] CBool + : #:+ (@ 0 : CNat) #:- (@ 0 : CNegInt)))) + +(define add1 + (unsafe-assign-type $add1 + : (C→ CNat CPosInt))) + +(define unneg + (unsafe-assign-type $- + : (C→ CNegInt CPosInt))) + +(: f : (C→ CInt CNat)) +(define (f x) + (if (natural? x) + (add1 x) + 1 #;(unneg x))) + diff --git a/typed/rosette.rkt b/typed/rosette.rkt index 88a8000..c0f7a4e 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -232,17 +232,26 @@ ;; specifically, a symbolic non-bool should produce a concrete val (define-typed-syntax if [(_ e_tst e1 e2) ≫ - [⊢ [e_tst ≫ e_tst- ⇒ : ty_tst]] + [⊢ [e_tst ≫ e_tst- + (⇒ : ty_tst) + (⇒ prop+ posprop) + (⇒ prop- negprop)]] #:when (or (concrete? #'ty_tst) ; either concrete ; or non-bool symbolic ; (not a super-type of CFalse) (and (not (typecheck? ((current-type-eval) #'CFalse) #'ty_tst)) (not (typecheck? ((current-type-eval) #'(Constant (Term CFalse))) #'ty_tst)))) - [⊢ [e1 ≫ e1- ⇒ : ty1]] - [⊢ [e2 ≫ e2- ⇒ : ty2]] + #:with [[posx τ_posx] ...] (prop->env #'posprop) + #:with [[negx τ_negx] ...] (prop->env #'negprop) + #:do [(println #'[[posx τ_posx] ...])] + [[posx ≫ posx- : τ_posx] ... ⊢ [e1 ≫ e1- ⇒ : ty1]] + [[negx ≫ negx- : τ_negx] ... ⊢ [e2 ≫ e2- ⇒ : ty2]] #:when (and (concrete? #'ty1) (concrete? #'ty2)) -------- - [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : (CU ty1 ty2)]]] + [⊢ [_ ≫ (ro:if e_tst- + (ro:let ([posx- posx] ...) e1-) + (ro:let ([negx- negx] ...) e2-)) + ⇒ : (CU ty1 ty2)]]] [(_ e_tst e1 e2) ≫ [⊢ [e_tst ≫ e_tst- ⇒ : _]] [⊢ [e1 ≫ e1- ⇒ : ty1]] @@ -250,7 +259,7 @@ #:with τ_out (type-merge #'ty1 #'ty2) -------- [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : τ_out]]]) - + ;; --------------------------------- ;; vector diff --git a/typed/rosette/base-forms.rkt b/typed/rosette/base-forms.rkt index 917f5f2..82de078 100644 --- a/typed/rosette/base-forms.rkt +++ b/typed/rosette/base-forms.rkt @@ -331,7 +331,10 @@ [(_ f:expr a:expr ... (~seq kw:keyword b:expr) ...) ≫ ;[⊢ f ≫ f-- ⇒ (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] τ_out) ~!)] #:with f-- (expand/ro #'f) - #:with (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] τ_out) ~!) + #:with (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] + τ_out + : #:+ posprop #:- negprop) + ~!) (typeof #'f--) #:with f- (replace-stx-loc #'f-- #'f) #:fail-unless (stx-length=? #'[a ...] #'[τ_a ...]) @@ -355,8 +358,12 @@ (typecheck-fail-msg/multi #'[τ_a ... τ_b ...] #'[τ_a* ... τ_b* ...] #'[a ... b ...]) #:with [[kw/b- ...] ...] #'[[kw b-] ...] + #:do [(define prop-inst (prop-instantiate (stx-map get-arg-obj #'[a ...])))] -------- - [⊢ (ro:#%app f- a- ... kw/b- ... ...) ⇒ τ_out]] + [⊢ (ro:#%app f- a- ... kw/b- ... ...) + (⇒ : τ_out) + (⇒ prop+ #,(syntax-local-introduce (prop-inst #'posprop))) + (⇒ prop- #,(syntax-local-introduce (prop-inst #'negprop)))]] [(_ f:expr ab:expr ... (~seq kw:keyword c:expr) ...) ≫ ;[⊢ f ≫ f-- ⇒ (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] #:rest τ_rst τ_out) ~!)] #:with f-- (expand/ro #'f) diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index dc442ed..552615a 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -18,6 +18,7 @@ C→? Ccase->?) ;; Propositions for Occurrence typing @ + (for-syntax prop-instantiate get-arg-obj prop->env) ;; Parameters CParamof ; TODO: symbolic Param not supported yet ;; List types @@ -232,13 +233,23 @@ (define-internal-type-constructor Result) ; #:arity = 3 (define-internal-type-constructor Prop/And) ; #:arity <= 0 +(define-internal-type-constructor Prop/Or) ; #:arity <= 0 (define-internal-type-constructor Prop/IndexType) ; #:arity = 2 +(define-internal-type-constructor Prop/ObjType) ; #:arity = 2 (define-syntax-parser Prop/Top [:id #'(Prop/And-)]) +(define-syntax-parser Prop/Bot [:id #'(Prop/Or-)]) (define-syntax-parser @ #:datum-literals [:] [(_ i:nat : τ:type) - #'(Prop/IndexType- 'i τ.norm)]) + #'(Prop/IndexType- (quote- i) τ.norm)]) + +(define-internal-type-constructor NoObj) ; #:arity = 0 +(define-internal-type-constructor IdObj) ; #:arity = 1 + +(define-syntax-parser IdObj + [(_ x:id) #`(IdObj- (quote-syntax- + #,(attach #'x 'orig (syntax-local-introduce #'x))))]) (begin-for-syntax (begin-for-syntax @@ -247,6 +258,16 @@ (define-syntax-class expr* [pattern (~and :expr (~not [:keyword . _]))]) + (begin-for-syntax + (define-splicing-syntax-class result-prop-pat + #:datum-literals [:] + [pattern (~seq) #:with pat_posprop #'_ #:with pat_negprop #'_] + [pattern (~seq : #:+ pat_posprop #:- pat_negprop)])) + (define-splicing-syntax-class result-prop + #:datum-literals [:] + [pattern (~seq) #:with posprop #'Prop/Top #:with negprop #'Prop/Top] + [pattern (~seq : #:+ posprop #:- negprop)]) + (define-syntax ~C→ (pattern-expander (syntax-parser @@ -261,22 +282,25 @@ (define-syntax ~C→* (pattern-expander (syntax-parser - [(_ [pat_in:expr* ...] [pat_kw:expr ...] pat_out:expr*) + [(_ [pat_in:expr* ...] [pat_kw:expr ...] pat_out:expr* + props:result-prop-pat) #:with opt-kws (generate-temporary 'opt-kws) #'(~C→*/internal (~MandArgs pat_in ...) (~and opt-kws (~parse [pat_kw ...] (convert-opt-kws #'opt-kws))) (~NoRestArg) - (~Result pat_out _ _))] - [(_ [pat_in:expr* ...] [pat_kw:expr ...] #:rest pat_rst:expr pat_out:expr*) + (~Result pat_out props.pat_posprop props.pat_negprop))] + [(_ [pat_in:expr* ...] [pat_kw:expr ...] #:rest pat_rst:expr + pat_out:expr* + props:result-prop-pat) #:with opt-kws (generate-temporary 'opt-kws) #'(~C→*/internal (~MandArgs pat_in ...) (~and opt-kws (~parse [pat_kw ...] (convert-opt-kws #'opt-kws))) (~RestArg pat_rst) - (~Result pat_out _ _))]))) + (~Result pat_out props.pat_posprop props.pat_negprop))]))) ) ;; --------------------------------- @@ -449,7 +473,8 @@ ;; rest ::= τ ;; output ::= τ (define-typed-syntax C→* - [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] τ_out:expr*) ≫ + [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] τ_out:expr* + props:result-prop) ≫ [⊢ [τ_in ≫ τ_in- ⇐ :: #%type] ...] [⊢ [τ_kw ≫ τ_kw- ⇐ :: #%type] ...] [⊢ τ_out ≫ τ_out- ⇐ :: #%type] @@ -457,9 +482,11 @@ [⊢ (C→*/internal- (MandArgs- τ_in- ...) (OptKws- (KwArg- (quote-syntax kw) τ_kw-) ...) (NoRestArg-) - (Result- τ_out- Prop/Top Prop/Top)) + (Result- τ_out- props.posprop props.negprop)) ⇒ :: #%type]] - [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] #:rest τ_rst τ_out:expr*) ≫ + [(_ [τ_in:expr* ...] [[kw:keyword τ_kw:expr*] ...] #:rest τ_rst + τ_out:expr* + props:result-prop) ≫ [⊢ [τ_in ≫ τ_in- ⇐ :: #%type] ...] [⊢ [τ_kw ≫ τ_kw- ⇐ :: #%type] ...] [⊢ τ_rst ≫ τ_rst- ⇐ :: #%type] @@ -468,7 +495,7 @@ [⊢ (C→*/internal- (MandArgs- τ_in- ...) (OptKws- (KwArg- (quote-syntax kw) τ_kw-) ...) (RestArg- τ_rst-) - (Result- τ_out- Prop/Top Prop/Top)) + (Result- τ_out- props.posprop props.negprop)) ⇒ :: #%type]]) (define-typed-syntax C→ @@ -674,6 +701,56 @@ ;; --------------------------------------------------------- +;; Instantiating Propositions for Occurrence Typing + +(begin-for-syntax + (define propProp/Top ((current-type-eval) #'Prop/Top)) + + ;; prop-instantitate : (Listof ObjStx) -> [PropStx -> PropStx] + (define (prop-instantiate arg-objs) + (define (inst p) + (syntax-parse (if (syntax-e p) p propProp/Top) + #:literals [quote-] + [(~Prop/And q ...) + #`(Prop/And- #,@(stx-map inst #'[q ...]))] + [(~Prop/Or q ...) + #`(Prop/Or- #,@(stx-map inst #'[q ...]))] + [(~Prop/IndexType (quote- i:nat) τ) + (syntax-parse (list-ref arg-objs (syntax-e #'i)) + [(~NoObj) #`Prop/Top] + [obj #`(Prop/ObjType- obj τ)])] + [(~Prop/ObjType _ _) + p])) + inst) + + ;; get-arg-obj : Stx -> ObjStx + (define (get-arg-obj stx) + ((current-type-eval) + (syntax-parse stx + [x:id #`(IdObj- (quote-syntax- + #,(attach #'x 'orig-id (syntax-local-introduce #'x))))] + [_ #'(NoObj-)]))) + + ;; prop->env : PropStx -> (Listof (List Id Type)) + (define (prop->env p) + (syntax-parse (if (syntax-e p) p propProp/Top) + #:literals [quote-syntax-] + [(~Prop/And q ...) + (append* (stx-map prop->env #'[q ...]))] + [(~Prop/Or q ...) + ;; TODO: do something more useful + '()] + [(~Prop/ObjType o τ) + (syntax-parse #'o + #:literals [quote-syntax-] + [(~NoObj) '()] + [(~IdObj (quote-syntax- x:id)) + (list (list (syntax-local-introduce (detach #'x 'orig-id)) + #'τ))])])) + ) + +;; --------------------------------------------------------- + ;; Subtyping (begin-for-syntax From fc7f5ef454e5e018a153abfddb16450a2fb92b1b Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 20 Apr 2017 23:13:59 -0700 Subject: [PATCH 04/24] finish basic occurrence typing for simplest cases requires occurrence-orig-binding branch of turnstile --- test/typed-rosette/occurrence.rkt | 2 +- typed/rosette.rkt | 9 ++++++--- typed/rosette/base-forms.rkt | 2 +- typed/rosette/types.rkt | 9 ++++++--- 4 files changed, 14 insertions(+), 8 deletions(-) diff --git a/test/typed-rosette/occurrence.rkt b/test/typed-rosette/occurrence.rkt index eb6f164..e203679 100644 --- a/test/typed-rosette/occurrence.rkt +++ b/test/typed-rosette/occurrence.rkt @@ -21,5 +21,5 @@ (define (f x) (if (natural? x) (add1 x) - 1 #;(unneg x))) + (unneg x))) diff --git a/typed/rosette.rkt b/typed/rosette.rkt index c0f7a4e..8f29757 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -241,11 +241,14 @@ ; (not a super-type of CFalse) (and (not (typecheck? ((current-type-eval) #'CFalse) #'ty_tst)) (not (typecheck? ((current-type-eval) #'(Constant (Term CFalse))) #'ty_tst)))) + #:do [(define scope + (make-syntax-delta-introducer (datum->syntax this-syntax '||) #f))] #:with [[posx τ_posx] ...] (prop->env #'posprop) #:with [[negx τ_negx] ...] (prop->env #'negprop) - #:do [(println #'[[posx τ_posx] ...])] - [[posx ≫ posx- : τ_posx] ... ⊢ [e1 ≫ e1- ⇒ : ty1]] - [[negx ≫ negx- : τ_negx] ... ⊢ [e2 ≫ e2- ⇒ : ty2]] + #:with [posx* ...] (scope #'[posx ...]) + #:with [negx* ...] (scope #'[negx ...]) + [[posx* ≫ posx- : τ_posx] ... ⊢ [e1 ≫ e1- ⇒ : ty1]] + [[negx* ≫ negx- : τ_negx] ... ⊢ [e2 ≫ e2- ⇒ : ty2]] #:when (and (concrete? #'ty1) (concrete? #'ty2)) -------- [⊢ [_ ≫ (ro:if e_tst- diff --git a/typed/rosette/base-forms.rkt b/typed/rosette/base-forms.rkt index 82de078..35c6fab 100644 --- a/typed/rosette/base-forms.rkt +++ b/typed/rosette/base-forms.rkt @@ -358,7 +358,7 @@ (typecheck-fail-msg/multi #'[τ_a ... τ_b ...] #'[τ_a* ... τ_b* ...] #'[a ... b ...]) #:with [[kw/b- ...] ...] #'[[kw b-] ...] - #:do [(define prop-inst (prop-instantiate (stx-map get-arg-obj #'[a ...])))] + #:do [(define prop-inst (prop-instantiate (stx-map get-arg-obj #'[a- ...])))] -------- [⊢ (ro:#%app f- a- ... kw/b- ... ...) (⇒ : τ_out) diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 552615a..0ec9aa2 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -249,7 +249,7 @@ (define-syntax-parser IdObj [(_ x:id) #`(IdObj- (quote-syntax- - #,(attach #'x 'orig (syntax-local-introduce #'x))))]) + #,(attach #'x 'orig-id (syntax-local-introduce #'x))))]) (begin-for-syntax (begin-for-syntax @@ -727,8 +727,11 @@ (define (get-arg-obj stx) ((current-type-eval) (syntax-parse stx - [x:id #`(IdObj- (quote-syntax- - #,(attach #'x 'orig-id (syntax-local-introduce #'x))))] + [x:id #:do [(define x* (detach #'x 'orig-binding))] + #:when x* + ;; syntax-local-introduce ruins it + #`(IdObj- (quote-syntax- + #,(attach x* 'orig-id x*)))] [_ #'(NoObj-)]))) ;; prop->env : PropStx -> (Listof (List Id Type)) From 985d580bc5cb4014771344aef0440e28931204ae Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Mon, 24 Apr 2017 15:17:36 -0700 Subject: [PATCH 05/24] start to restrict existing types instead of overriding them MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit TODO: Is there a better way to restrict non-overlapping types into bottom? Is it safe to say, no matter what, no two “base types” will have any values that overlap? TODO: Is there a better way to deal with known dead code (when propositions are bottom) than what’s done here? TODO: What should this do with Or propositions? (Right now they don’t add any information.) What about Not propositions? --- test/typed-rosette/occurrence.rkt | 39 ++++++++++++++- typed/rosette.rkt | 26 ++++++---- typed/rosette/types.rkt | 80 +++++++++++++++++++++++++++---- 3 files changed, 126 insertions(+), 19 deletions(-) diff --git a/test/typed-rosette/occurrence.rkt b/test/typed-rosette/occurrence.rkt index e203679..5da2a78 100644 --- a/test/typed-rosette/occurrence.rkt +++ b/test/typed-rosette/occurrence.rkt @@ -1,9 +1,15 @@ #lang typed/rosette -(require typed/rosette/types +(require turnstile/rackunit-typechecking + typed/rosette/types (only-in typed/rosette/base-forms unsafe-assign-type) (prefix-in $ rosette)) +(define integer? + (unsafe-assign-type $integer? + : (C→* [(CU CInt CString)] [] CBool + : #:+ (@ 0 : CInt) #:- (@ 0 : CString)))) + (define natural? (unsafe-assign-type $exact-nonnegative-integer? : (C→* [CInt] [] CBool @@ -23,3 +29,34 @@ (add1 x) (unneg x))) +(: f/restricted : (C→ CPosInt CNat)) +(define (f/restricted x) + (if (natural? x) + (add1 x) + (unneg x))) + +;; --------------------------------------------------------- + +;; Testing type restricting behavior + +(: g : (C→ (CU CNegInt CZero) CNat)) +(define (g x) + (if (natural? x) + (ann x : CZero) + (unneg x))) + +;; --------------------------------------------------------- + +;; Testing occurrence typing with case-> + +(: h : (Ccase-> (C→ CInt CInt) + (C→ CString CString))) +(define (h x) + (if (integer? x) + (f x) + (string-append "|" (string-append x "|")))) + +(check-type (h 4) : CInt -> 5) +(check-type (h -4) : CInt -> 4) +(check-type (h "four") : CString -> "|four|") + diff --git a/typed/rosette.rkt b/typed/rosette.rkt index 8f29757..29781d9 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -243,18 +243,24 @@ (not (typecheck? ((current-type-eval) #'(Constant (Term CFalse))) #'ty_tst)))) #:do [(define scope (make-syntax-delta-introducer (datum->syntax this-syntax '||) #f))] - #:with [[posx τ_posx] ...] (prop->env #'posprop) - #:with [[negx τ_negx] ...] (prop->env #'negprop) - #:with [posx* ...] (scope #'[posx ...]) - #:with [negx* ...] (scope #'[negx ...]) - [[posx* ≫ posx- : τ_posx] ... ⊢ [e1 ≫ e1- ⇒ : ty1]] - [[negx* ≫ negx- : τ_negx] ... ⊢ [e2 ≫ e2- ⇒ : ty2]] - #:when (and (concrete? #'ty1) (concrete? #'ty2)) + #:with pos:occurrence-env (prop->env #'posprop) + #:with neg:occurrence-env (prop->env #'negprop) + #:with [posx* ...] (scope #'[pos.x ...]) + #:with [negx* ...] (scope #'[neg.x ...]) + [[posx* ≫ posx- : pos.τ] ... ⊢ [#,(if (attribute pos.bottom?) #'(assert #false) #'e1) ≫ e1- ⇒ : ty1]] + [[negx* ≫ negx- : neg.τ] ... ⊢ [#,(if (attribute neg.bottom?) #'(assert #false) #'e2) ≫ e2- ⇒ : ty2]] + #:with τ_out + (cond [(and (attribute pos.bottom?) (attribute neg.bottom?)) #'CNothing] + [(attribute pos.bottom?) #'ty2] + [(attribute neg.bottom?) #'ty1] + [(and (concrete? #'ty1) (concrete? #'ty2)) #'(CU ty1 ty2)] + ;; else don't need to merge, but do need U + [else #'(U ty1 ty2)]) -------- [⊢ [_ ≫ (ro:if e_tst- - (ro:let ([posx- posx] ...) e1-) - (ro:let ([negx- negx] ...) e2-)) - ⇒ : (CU ty1 ty2)]]] + (ro:let ([posx- pos.x] ...) e1-) + (ro:let ([negx- neg.x] ...) e2-)) + ⇒ : τ_out]]] [(_ e_tst e1 e2) ≫ [⊢ [e_tst ≫ e_tst- ⇒ : _]] [⊢ [e1 ≫ e1- ⇒ : ty1]] diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 0ec9aa2..72e33d6 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -71,7 +71,8 @@ type-merge type-merge* typeCFalse - typeCTrue)) + typeCTrue + occurrence-env)) (require (only-in turnstile/examples/stlc+union define-named-type-alias prune+sort current-sub?) @@ -84,6 +85,7 @@ [U CU*] [~U* ~CU*] [U*? CU*?] [case-> Ccase->*] [~case-> ~Ccase->] [case->? Ccase->?] [→ C→/normal] [~→ ~C→/normal] [→? C→/normal?] + [~PosInt ~CPosInt] [~Zero ~CZero] [~NegInt ~CNegInt] [~True ~CTrue] [~False ~CFalse] [~String ~CString] [~Unit ~CUnit]) @@ -93,6 +95,8 @@ (prefix-in ro: rosette/lib/synthax) (rename-in "../rosette-util.rkt" [bitvector? lifted-bitvector?])) +(require (for-syntax syntax/id-table)) + ;; --------------------------------- ;; Concrete and Symbolic union types @@ -374,6 +378,7 @@ (stx-andmap type-solvable? #'[τ_in ... τ_out])] [_ #false]))) + (define typeCNothing ((current-type-eval) #'CNothing)) (define typeCFalse ((current-type-eval) #'CFalse)) (define typeCTrue ((current-type-eval) #'CTrue)) (define typeCBool ((current-type-eval) #'CBool)) @@ -731,25 +736,84 @@ #:when x* ;; syntax-local-introduce ruins it #`(IdObj- (quote-syntax- - #,(attach x* 'orig-id x*)))] + #,(attach + (attach x* 'orig-id x*) + 'orig-type (typeof #'x))))] [_ #'(NoObj-)]))) - ;; prop->env : PropStx -> (Listof (List Id Type)) + ;; prop->env : PropStx -> (Maybe (Listof (List Id Type))) (define (prop->env p) + (define env + (prop->env/acc p (make-immutable-free-id-table))) + (and env (free-id-table-map env list))) + + ;; prop->env/acc : PropStx (FreeIdTableof Type) -> (Maybe (FreeIdTableof Type)) + (define (prop->env/acc p acc) (syntax-parse (if (syntax-e p) p propProp/Top) #:literals [quote-syntax-] [(~Prop/And q ...) - (append* (stx-map prop->env #'[q ...]))] + (for/fold ([acc acc]) ([q (in-list (stx->list #'[q ...]))]) + #:break (false? acc) + (prop->env/acc q acc))] + [(~Prop/Or q) + #false] [(~Prop/Or q ...) ;; TODO: do something more useful - '()] + acc] [(~Prop/ObjType o τ) (syntax-parse #'o #:literals [quote-syntax-] - [(~NoObj) '()] + [(~NoObj) acc] [(~IdObj (quote-syntax- x:id)) - (list (list (syntax-local-introduce (detach #'x 'orig-id)) - #'τ))])])) + (define x* (syntax-local-introduce (detach #'x 'orig-id))) + (define τ_orig (free-id-table-ref acc x* (λ () (detach #'x 'orig-type)))) + (define τ_new (refine-type τ_orig #'τ)) + (if (typecheck? τ_new typeCNothing) + #false + (free-id-table-set acc x* τ_new))])])) + + ;; refine-type : Type Type -> Type + (define (refine-type orig new) + (cond [(typecheck? new orig) new] + [(Un? new) + ((current-type-eval) + (syntax-parse new + [(~CU* n ...) + #`(CU #,@(for/list ([n (in-list (stx->list #'[n ...]))]) + (refine-type orig n)))]))] + [(Un? orig) + ((current-type-eval) + (syntax-parse orig + [(~CU* o ...) + #`(CU #,@(for/list ([o (in-list (stx->list #'[o ...]))]) + (refine-type o new)))]))] + [else + (syntax-parse (list orig new) + [[~CZero ~CPosInt] ((current-type-eval) #'CNothing)] + [[~CZero ~CNegInt] ((current-type-eval) #'CNothing)] + [[~CZero ~CString] ((current-type-eval) #'CNothing)] + [[~CPosInt ~CZero] ((current-type-eval) #'CNothing)] + [[~CPosInt ~CNegInt] ((current-type-eval) #'CNothing)] + [[~CPosInt ~CString] ((current-type-eval) #'CNothing)] + [[~CNegInt ~CPosInt] ((current-type-eval) #'CNothing)] + [[~CNegInt ~CZero] ((current-type-eval) #'CNothing)] + [[~CNegInt ~CString] ((current-type-eval) #'CNothing)] + [[~CString ~CPosInt] ((current-type-eval) #'CNothing)] + [[~CString ~CZero] ((current-type-eval) #'CNothing)] + [[~CString ~CNegInt] ((current-type-eval) #'CNothing)] + [_ + (printf "refine-type: dontknowwhattodo\n orig: ~a\n new: ~a\n" + (type->str orig) + (type->str new)) + orig])])) + + (define-syntax-class occurrence-env + #:attributes [[x 1] [τ 1] bottom?] + [pattern #false + #:attr bottom? #true + #:with [[x τ] ...] #'[]] + [pattern [[x τ] ...] + #:attr bottom? #false]) ) ;; --------------------------------------------------------- From 55ae65305bdd7b305ecf8df3ec4a98c8f3cf9beb Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Tue, 25 Apr 2017 13:55:31 -0700 Subject: [PATCH 06/24] deal with not-type propositions --- test/typed-rosette/occurrence.rkt | 19 ++++++-- typed/rosette/types.rkt | 75 ++++++++++++++++++++++--------- 2 files changed, 69 insertions(+), 25 deletions(-) diff --git a/test/typed-rosette/occurrence.rkt b/test/typed-rosette/occurrence.rkt index 5da2a78..496f8ba 100644 --- a/test/typed-rosette/occurrence.rkt +++ b/test/typed-rosette/occurrence.rkt @@ -7,13 +7,13 @@ (define integer? (unsafe-assign-type $integer? - : (C→* [(CU CInt CString)] [] CBool - : #:+ (@ 0 : CInt) #:- (@ 0 : CString)))) + : (C→* [CAny] [] CBool + : #:+ (@ 0 : CInt) #:- (!@ 0 : CInt)))) (define natural? (unsafe-assign-type $exact-nonnegative-integer? - : (C→* [CInt] [] CBool - : #:+ (@ 0 : CNat) #:- (@ 0 : CNegInt)))) + : (C→* [CAny] [] CBool + : #:+ (@ 0 : CNat) #:- (!@ 0 : CNat)))) (define add1 (unsafe-assign-type $add1 @@ -47,6 +47,17 @@ ;; --------------------------------------------------------- +;; Unions with Nothings and non-Nothings in them should not +;; be Nothing! + +(typecheck-fail + (λ ([x : (CU CNothing CString)]) + (ann x : CNothing)) + #:with-msg + "expected CNothing, given \\(CU CNothing CString\\)") + +;; --------------------------------------------------------- + ;; Testing occurrence typing with case-> (: h : (Ccase-> (C→ CInt CInt) diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 72e33d6..f2e4bc7 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -17,7 +17,7 @@ ~C→ ~C→* ~Ccase-> C→? Ccase->?) ;; Propositions for Occurrence typing - @ + @ !@ (for-syntax prop-instantiate get-arg-obj prop->env) ;; Parameters CParamof ; TODO: symbolic Param not supported yet @@ -239,7 +239,9 @@ (define-internal-type-constructor Prop/And) ; #:arity <= 0 (define-internal-type-constructor Prop/Or) ; #:arity <= 0 (define-internal-type-constructor Prop/IndexType) ; #:arity = 2 +(define-internal-type-constructor Prop/IndexNotType) ; #:arity = 2 (define-internal-type-constructor Prop/ObjType) ; #:arity = 2 +(define-internal-type-constructor Prop/ObjNotType) ; #:arity = 2 (define-syntax-parser Prop/Top [:id #'(Prop/And-)]) (define-syntax-parser Prop/Bot [:id #'(Prop/Or-)]) @@ -247,6 +249,10 @@ #:datum-literals [:] [(_ i:nat : τ:type) #'(Prop/IndexType- (quote- i) τ.norm)]) +(define-syntax-parser !@ + #:datum-literals [:] + [(_ i:nat : τ:type) + #'(Prop/IndexNotType- (quote- i) τ.norm)]) (define-internal-type-constructor NoObj) ; #:arity = 0 (define-internal-type-constructor IdObj) ; #:arity = 1 @@ -724,8 +730,12 @@ (syntax-parse (list-ref arg-objs (syntax-e #'i)) [(~NoObj) #`Prop/Top] [obj #`(Prop/ObjType- obj τ)])] - [(~Prop/ObjType _ _) - p])) + [(~Prop/IndexNotType (quote- i:nat) τ) + (syntax-parse (list-ref arg-objs (syntax-e #'i)) + [(~NoObj) #`Prop/Top] + [obj #`(Prop/ObjNotType- obj τ)])] + [(~Prop/ObjType _ _) p] + [(~Prop/ObjNotType _ _) p])) inst) ;; get-arg-obj : Stx -> ObjStx @@ -767,45 +777,68 @@ [(~IdObj (quote-syntax- x:id)) (define x* (syntax-local-introduce (detach #'x 'orig-id))) (define τ_orig (free-id-table-ref acc x* (λ () (detach #'x 'orig-type)))) - (define τ_new (refine-type τ_orig #'τ)) + (define τ_new (type-restrict τ_orig #'τ)) + (if (typecheck? τ_new typeCNothing) + #false + (free-id-table-set acc x* τ_new))])] + [(~Prop/ObjNotType o τ) + (syntax-parse #'o + #:literals [quote-syntax-] + [(~NoObj) acc] + [(~IdObj (quote-syntax- x:id)) + (define x* (syntax-local-introduce (detach #'x 'orig-id))) + (define τ_orig (free-id-table-ref acc x* (λ () (detach #'x 'orig-type)))) + (define τ_new (type-remove τ_orig #'τ)) (if (typecheck? τ_new typeCNothing) #false (free-id-table-set acc x* τ_new))])])) - ;; refine-type : Type Type -> Type - (define (refine-type orig new) + ;; type-restrict : Type Type -> Type + (define (type-restrict orig new) (cond [(typecheck? new orig) new] [(Un? new) ((current-type-eval) (syntax-parse new [(~CU* n ...) #`(CU #,@(for/list ([n (in-list (stx->list #'[n ...]))]) - (refine-type orig n)))]))] + (type-restrict orig n)))]))] [(Un? orig) ((current-type-eval) (syntax-parse orig [(~CU* o ...) #`(CU #,@(for/list ([o (in-list (stx->list #'[o ...]))]) - (refine-type o new)))]))] + (type-restrict o new)))]))] [else (syntax-parse (list orig new) - [[~CZero ~CPosInt] ((current-type-eval) #'CNothing)] - [[~CZero ~CNegInt] ((current-type-eval) #'CNothing)] - [[~CZero ~CString] ((current-type-eval) #'CNothing)] - [[~CPosInt ~CZero] ((current-type-eval) #'CNothing)] - [[~CPosInt ~CNegInt] ((current-type-eval) #'CNothing)] - [[~CPosInt ~CString] ((current-type-eval) #'CNothing)] - [[~CNegInt ~CPosInt] ((current-type-eval) #'CNothing)] - [[~CNegInt ~CZero] ((current-type-eval) #'CNothing)] - [[~CNegInt ~CString] ((current-type-eval) #'CNothing)] - [[~CString ~CPosInt] ((current-type-eval) #'CNothing)] - [[~CString ~CZero] ((current-type-eval) #'CNothing)] - [[~CString ~CNegInt] ((current-type-eval) #'CNothing)] + [[~CZero ~CPosInt] typeCNothing] + [[~CZero ~CNegInt] typeCNothing] + [[~CZero ~CString] typeCNothing] + [[~CPosInt ~CZero] typeCNothing] + [[~CPosInt ~CNegInt] typeCNothing] + [[~CPosInt ~CString] typeCNothing] + [[~CNegInt ~CPosInt] typeCNothing] + [[~CNegInt ~CZero] typeCNothing] + [[~CNegInt ~CString] typeCNothing] + [[~CString ~CPosInt] typeCNothing] + [[~CString ~CZero] typeCNothing] + [[~CString ~CNegInt] typeCNothing] [_ (printf "refine-type: dontknowwhattodo\n orig: ~a\n new: ~a\n" (type->str orig) (type->str new)) - orig])])) + new])])) + + ;; type-remove : Type Type -> Type + (define (type-remove orig new-not) + (cond [(typecheck? orig new-not) typeCNothing] + [(Un? orig) + ((current-type-eval) + (syntax-parse orig + [(~CU* o ...) + #`(CU #,@(for/list ([o (in-list (stx->list #'[o ...]))]) + (type-remove o new-not)))]))] + [else + orig])) (define-syntax-class occurrence-env #:attributes [[x 1] [τ 1] bottom?] From 935a73d9569c14e01e6ec1c162738b69c8953e3b Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Tue, 25 Apr 2017 16:23:36 -0700 Subject: [PATCH 07/24] handle Or propositions --- test/typed-rosette/occurrence.rkt | 25 ++++++++++++++++ typed/rosette.rkt | 23 +++++++++++++-- typed/rosette/types.rkt | 48 +++++++++++++++++++++++++++++-- 3 files changed, 91 insertions(+), 5 deletions(-) diff --git a/test/typed-rosette/occurrence.rkt b/test/typed-rosette/occurrence.rkt index 496f8ba..79d8e0d 100644 --- a/test/typed-rosette/occurrence.rkt +++ b/test/typed-rosette/occurrence.rkt @@ -10,6 +10,11 @@ : (C→* [CAny] [] CBool : #:+ (@ 0 : CInt) #:- (!@ 0 : CInt)))) +(define string? + (unsafe-assign-type $string? + : (C→* [CAny] [] CBool + : #:+ (@ 0 : CString) #:- (!@ 0 : CString)))) + (define natural? (unsafe-assign-type $exact-nonnegative-integer? : (C→* [CAny] [] CBool @@ -71,3 +76,23 @@ (check-type (h -4) : CInt -> 4) (check-type (h "four") : CString -> "|four|") +;; --------------------------------------------------------- + +;; Testing occurrence typing with or + +(: f/intstr : (C→ (CU CInt CString) CInt)) +(define (f/intstr x) + (if (integer? x) + x + (string-length x))) + +(: f/or : (C→ CAny CInt)) +(define (f/or x) + (if (or (integer? x) (string? x)) + (f/intstr x) + 0)) + +(check-type (f/or 5) : CInt -> 5) +(check-type (f/or "five") : CInt -> 4) +(check-type (f/or (list 1 2 3 4 5)) : CInt -> 0) + diff --git a/typed/rosette.rkt b/typed/rosette.rkt index 29781d9..4290524 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -1160,18 +1160,35 @@ [⊢ [elast ≫ elast- ⇒ : ty-last]] -------- [⊢ [_ ≫ (ro:and e- ... elast-) ⇒ : #,(type-merge typeCFalse #'ty-last)]]]) + (define-typed-syntax or [(_) ≫ -------- - [⊢ [_ ≫ (ro:or) ⇒ : CFalse]]] + [⊢ [_ ≫ (ro:or) + (⇒ : CFalse) + (⇒ prop+ Prop/Bot) + (⇒ prop- Prop/Top)]]] [(_ e ...) ≫ - [⊢ [e ≫ e- ⇐ : Bool] ...] + [⊢ [e ≫ e- (⇐ : CBool) (⇒ prop+ p+) (⇒ prop- p-)] + ...] -------- - [⊢ [_ ≫ (ro:or e- ...) ⇒ : Bool]]] + [⊢ [_ ≫ (ro:or e- ...) + (⇒ : CBool) + (⇒ prop+ (Prop/Or p+ ...)) + (⇒ prop- (Prop/And p- ...))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- (⇐ : Bool) (⇒ prop+ p+) (⇒ prop- p-)] + ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) + (⇒ : Bool) + (⇒ prop+ (Prop/Or p+ ...)) + (⇒ prop- (Prop/And p- ...))]]] [(_ e ...) ≫ [⊢ [e ≫ e- ⇒ : ty] ...] -------- [⊢ [_ ≫ (ro:or e- ...) ⇒ : #,(type-merge* (cons typeCFalse #'[ty ...]))]]]) + (define-typed-syntax nand [(_) ≫ -------- diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index f2e4bc7..ad8551a 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -18,6 +18,8 @@ C→? Ccase->?) ;; Propositions for Occurrence typing @ !@ + Prop/Or + Prop/And (for-syntax prop-instantiate get-arg-obj prop->env) ;; Parameters CParamof ; TODO: symbolic Param not supported yet @@ -254,6 +256,17 @@ [(_ i:nat : τ:type) #'(Prop/IndexNotType- (quote- i) τ.norm)]) +(define-syntax-parser Prop/Or + [(_ p ...) + (if (stx-andmap syntax-e #'[p ...]) + #'(Prop/Or- p ...) + #'Prop/Top)]) +(define-syntax-parser Prop/And + [(_ p ...) + #:with [p* ...] + (stx-filter syntax-e #'[p ...]) + #'(Prop/And- p* ...)]) + (define-internal-type-constructor NoObj) ; #:arity = 0 (define-internal-type-constructor IdObj) ; #:arity = 1 @@ -768,8 +781,11 @@ [(~Prop/Or q) #false] [(~Prop/Or q ...) - ;; TODO: do something more useful - acc] + (for/fold ([sub #false]) + ([q (in-list (stx->list #'[q ...]))]) + (occurrence-env-id-table-or + sub + (prop->env/acc q acc)))] [(~Prop/ObjType o τ) (syntax-parse #'o #:literals [quote-syntax-] @@ -840,6 +856,34 @@ [else orig])) + ;; occurrence-env-id-table-or : + ;; (Maybe (FreeIdTableof Type)) (Maybe (FreeIdTableof Type)) -> (Maybe (FreeIdTableof Type)) + ;; Combines two possible occurrence-typing type environments with or. + ;; This means we don't know which environment will be true, so the result + ;; will only include identifiers that are included in both environments, + ;; with the types that are a union of the associated types in both. + (define (occurrence-env-id-table-or a b) + (cond [(false? a) b] + [(false? b) a] + [else + (for/fold ([a a]) + ([(id τ_b) (in-free-id-table b)]) + (cond + [(dict-has-key? a id) + (free-id-table-update + a + id + (λ (τ_a) (type-or τ_a τ_b)))] + [else + (free-id-table-remove a id)]))])) + + ;; type-or : Type Type -> Type + (define (type-or a b) + (cond [(and (concrete? a) (concrete? b)) + ((current-type-eval) #`(CU #,a #,b))] + [else + ((current-type-eval) #`(U #,a #,b))])) + (define-syntax-class occurrence-env #:attributes [[x 1] [τ 1] bottom?] [pattern #false From 87c5ddac0bcf166617f886fecc1c7d088107eba5 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Tue, 25 Apr 2017 17:40:36 -0700 Subject: [PATCH 08/24] add with-occurrence-prop macro to deal with converting the prop to an env, dead code, putting the correct scopes on the env identifiers, etc. --- typed/rosette.rkt | 19 +++++-------------- typed/rosette/types.rkt | 32 +++++++++++++++++++++++++++++++- 2 files changed, 36 insertions(+), 15 deletions(-) diff --git a/typed/rosette.rkt b/typed/rosette.rkt index 4290524..22ce92d 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -241,25 +241,16 @@ ; (not a super-type of CFalse) (and (not (typecheck? ((current-type-eval) #'CFalse) #'ty_tst)) (not (typecheck? ((current-type-eval) #'(Constant (Term CFalse))) #'ty_tst)))) - #:do [(define scope - (make-syntax-delta-introducer (datum->syntax this-syntax '||) #f))] - #:with pos:occurrence-env (prop->env #'posprop) - #:with neg:occurrence-env (prop->env #'negprop) - #:with [posx* ...] (scope #'[pos.x ...]) - #:with [negx* ...] (scope #'[neg.x ...]) - [[posx* ≫ posx- : pos.τ] ... ⊢ [#,(if (attribute pos.bottom?) #'(assert #false) #'e1) ≫ e1- ⇒ : ty1]] - [[negx* ≫ negx- : neg.τ] ... ⊢ [#,(if (attribute neg.bottom?) #'(assert #false) #'e2) ≫ e2- ⇒ : ty2]] + [⊢ [(with-occurrence-prop posprop e1) ≫ e1- ⇒ : ty1]] + [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] #:with τ_out - (cond [(and (attribute pos.bottom?) (attribute neg.bottom?)) #'CNothing] - [(attribute pos.bottom?) #'ty2] - [(attribute neg.bottom?) #'ty1] - [(and (concrete? #'ty1) (concrete? #'ty2)) #'(CU ty1 ty2)] + (cond [(and (concrete? #'ty1) (concrete? #'ty2)) #'(CU ty1 ty2)] ;; else don't need to merge, but do need U [else #'(U ty1 ty2)]) -------- [⊢ [_ ≫ (ro:if e_tst- - (ro:let ([posx- pos.x] ...) e1-) - (ro:let ([negx- neg.x] ...) e2-)) + e1- + e2-) ⇒ : τ_out]]] [(_ e_tst e1 e2) ≫ [⊢ [e_tst ≫ e_tst- ⇒ : _]] diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index ad8551a..0f40818 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -20,7 +20,8 @@ @ !@ Prop/Or Prop/And - (for-syntax prop-instantiate get-arg-obj prop->env) + with-occurrence-prop + (for-syntax prop-instantiate get-arg-obj) ;; Parameters CParamof ; TODO: symbolic Param not supported yet ;; List types @@ -893,6 +894,35 @@ #:attr bottom? #false]) ) +;; (with-occurrence-env occurrence-env expr) +(define-typed-syntax with-occurrence-env + [(_ #false body:expr) ≫ + #:with DEAD (syntax/loc #'body + (ro:assert #false "this should be dead code")) + -------- + [⊢ DEAD ⇒ CNothing]] + [(_ ([x:id τ:expr] ...) body:expr) ⇐ τ_body ≫ + #:do [(define scope + (make-syntax-delta-introducer (datum->syntax #'body '||) #f))] + #:with [x* ...] (scope #'[x ...]) + [[x* ≫ x- : τ] ... ⊢ body ≫ body- ⇐ τ_body] + -------- + [⊢ (let- ([x- x] ...) body-)]] + [(_ ([x:id τ:type] ...) body:expr) ≫ + #:do [(define scope + (make-syntax-delta-introducer (datum->syntax #'body '||) #f))] + #:with [x* ...] (scope #'[x ...]) + [[x* ≫ x- : τ] ... ⊢ body ≫ body- ⇒ τ_body] + -------- + [⊢ (let- ([x- x] ...) body-) ⇒ τ_body]]) + +;; (with-occurrence-prop prop expr) +;; The prop must already be expanded +(define-syntax-parser with-occurrence-prop + [(_ prop:expr body:expr) + #:with env:occurrence-env (prop->env #'prop) + #'(with-occurrence-env env body)]) + ;; --------------------------------------------------------- ;; Subtyping From 8dfb75167f2fa5da90fbd7ec6b93a4c193528666 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 26 Apr 2017 13:48:43 -0700 Subject: [PATCH 09/24] support occurrence typing in more symbolic situations --- test/typed-rosette/occurrence.rkt | 56 +++++++++++++++++++++++++++---- typed/rosette.rkt | 9 +++-- typed/rosette/base-forms.rkt | 30 ++++++++++++----- typed/rosette/types.rkt | 52 ++++++++++++++++++++++++++-- 4 files changed, 126 insertions(+), 21 deletions(-) diff --git a/test/typed-rosette/occurrence.rkt b/test/typed-rosette/occurrence.rkt index 79d8e0d..96f60da 100644 --- a/test/typed-rosette/occurrence.rkt +++ b/test/typed-rosette/occurrence.rkt @@ -7,8 +7,19 @@ (define integer? (unsafe-assign-type $integer? - : (C→* [CAny] [] CBool - : #:+ (@ 0 : CInt) #:- (!@ 0 : CInt)))) + : (Ccase-> + (C→* [CAny] [] CBool + : #:+ (@ 0 : CInt) #:- (!@ 0 : CInt)) + (C→* [Any] [] Bool + : #:+ (@ 0 : Int) #:- (!@ 0 : Int))))) + +(define boolean? + (unsafe-assign-type $boolean? + : (Ccase-> + (C→* [CAny] [] CBool + : #:+ (@ 0 : CBool) #:- (!@ 0 : CBool)) + (C→* [Any] [] Bool + : #:+ (@ 0 : Bool) #:- (!@ 0 : Bool))))) (define string? (unsafe-assign-type $string? @@ -17,16 +28,21 @@ (define natural? (unsafe-assign-type $exact-nonnegative-integer? - : (C→* [CAny] [] CBool - : #:+ (@ 0 : CNat) #:- (!@ 0 : CNat)))) + : (Ccase-> + (C→* [CAny] [] CBool + : #:+ (@ 0 : CNat) #:- (!@ 0 : CNat)) + (C→* [Any] [] Bool + : #:+ (@ 0 : Nat) #:- (!@ 0 : Nat))))) (define add1 (unsafe-assign-type $add1 - : (C→ CNat CPosInt))) + : (Ccase-> (C→ CNat CPosInt) + (C→ Nat PosInt)))) (define unneg (unsafe-assign-type $- - : (C→ CNegInt CPosInt))) + : (Ccase-> (C→ CNegInt CPosInt) + (C→ NegInt PosInt)))) (: f : (C→ CInt CNat)) (define (f x) @@ -40,6 +56,12 @@ (add1 x) (unneg x))) +(: f* : (C→ Int Nat)) +(define (f* x) + (if (natural? x) + (add1 x) + (unneg x))) + ;; --------------------------------------------------------- ;; Testing type restricting behavior @@ -50,6 +72,12 @@ (ann x : CZero) (unneg x))) +(: g* : (C→ (Term (CU CNegInt CZero)) Nat)) +(define (g* x) + (if (natural? x) + (ann x : Zero) + (unneg x))) + ;; --------------------------------------------------------- ;; Unions with Nothings and non-Nothings in them should not @@ -96,3 +124,19 @@ (check-type (f/or "five") : CInt -> 4) (check-type (f/or (list 1 2 3 4 5)) : CInt -> 0) +(: bool->int : (C→ Bool Int)) +(define (bool->int b) + (if b 1 0)) + +(: f/intbool* : (C→ (U Int Bool) Int)) +(define (f/intbool* x) + (if (integer? x) + x + (bool->int x))) + +(: f/or* : (C→ Any Int)) +(define (f/or* x) + (if (or (integer? x) (boolean? x)) + (f/intbool* x) + 0)) + diff --git a/typed/rosette.rkt b/typed/rosette.rkt index 22ce92d..bb54b37 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -253,9 +253,12 @@ e2-) ⇒ : τ_out]]] [(_ e_tst e1 e2) ≫ - [⊢ [e_tst ≫ e_tst- ⇒ : _]] - [⊢ [e1 ≫ e1- ⇒ : ty1]] - [⊢ [e2 ≫ e2- ⇒ : ty2]] + [⊢ [e_tst ≫ e_tst- + (⇒ : _) + (⇒ prop+ posprop) + (⇒ prop- negprop)]] + [⊢ [(with-occurrence-prop posprop e1) ≫ e1- ⇒ : ty1]] + [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] #:with τ_out (type-merge #'ty1 #'ty2) -------- [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : τ_out]]]) diff --git a/typed/rosette/base-forms.rkt b/typed/rosette/base-forms.rkt index 35c6fab..1f83e4b 100644 --- a/typed/rosette/base-forms.rkt +++ b/typed/rosette/base-forms.rkt @@ -367,7 +367,8 @@ [(_ f:expr ab:expr ... (~seq kw:keyword c:expr) ...) ≫ ;[⊢ f ≫ f-- ⇒ (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] #:rest τ_rst τ_out) ~!)] #:with f-- (expand/ro #'f) - #:with (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] #:rest τ_rst τ_out) ~!) + #:with (~and (~C→* [τ_a ...] [[kw* τ_kw*] ...] #:rest τ_rst τ_out + : #:+ posprop #:- negprop) ~!) (typeof #'f--) #:with f- (replace-stx-loc #'f-- #'f) #:fail-unless (stx-length>=? #'[ab ...] #'[τ_a ...]) @@ -399,8 +400,12 @@ #'[τ_a* ... τ_c* ... τ_rst*] #'[a ... c ... (list b ...)]) #:with [[kw/c- ...] ...] #'[[kw c-] ...] + #:do [(define prop-inst (prop-instantiate (stx-map get-arg-obj #'[a- ...])))] -------- - [⊢ (ro:#%app ro:apply f- a- ... rst- kw/c- ... ...) ⇒ τ_out]] + [⊢ (ro:#%app ro:apply f- a- ... rst- kw/c- ... ...) + (⇒ : τ_out) + (⇒ prop+ #,(syntax-local-introduce (prop-inst #'posprop))) + (⇒ prop- #,(syntax-local-introduce (prop-inst #'negprop)))]] ;; concrete case-> [(_ f:expr a:expr ... (~seq kw:keyword b:expr) ...) ≫ ;[⊢ f ≫ f- ⇒ (~and (~Ccase-> ~! τ_f ...) ~!)] @@ -413,10 +418,11 @@ #:with [b- ...] (stx-map expand/ro #'[b ...]) #:with [τ_a ...] (stx-map typeof #'(a- ...)) #:with [τ_b ...] (stx-map typeof #'(b- ...)) - #:with τ_out + #:with result-info (for/or ([τ_f (in-list (stx->list #'[τ_f ...]))]) (syntax-parse τ_f - [(~C→* [τ_a* ...] [[kw* τ_kw*] ...] τ_out) + [(~C→* [τ_a* ...] [[kw* τ_kw*] ...] τ_out + : #:+ posprop #:- negprop) (define kws/τs* (for/list ([kw (in-list (syntax->datum #'[kw* ...]))] [τ (in-list (syntax->list #'[τ_kw* ...]))]) @@ -427,8 +433,9 @@ (define p (assoc kw kws/τs*)) (and p (typecheck? τ_b (second p)))) - #'τ_out)] - [(~C→* [τ_a* ...] [[kw* τ_kw*] ...] #:rest τ_rst* τ_out) + (list #'τ_out #'posprop #'negprop))] + [(~C→* [τ_a* ...] [[kw* τ_kw*] ...] #:rest τ_rst* τ_out + : #:+ posprop #:- negprop) #:when (stx-length>=? #'[τ_a ...] #'[τ_a* ...]) #:with [[τ_fst ...] [τ_rst ...]] (split-at* (stx->list #'[τ_a ...]) (list (stx-length #'[τ_a* ...]))) @@ -443,9 +450,9 @@ (define p (assoc kw kws/τs*)) (and p (typecheck? τ_b (second p)))) - #'τ_out)] + (list #'τ_out #'posprop #'negprop))] [_ #false])) - #:fail-unless (syntax-e #'τ_out) + #:fail-unless (syntax-e #'result-info) ; use (failing) typechecks? to get err msg (let* ([τs_given #'(τ_a ...)] [expressions #'(a ...)]) @@ -459,9 +466,14 @@ "\n ") (string-join (stx-map type->str τs_given) ", ") (string-join (map ~s (stx-map syntax->datum expressions)) ", "))) + #:with [τ_out posprop negprop] #'result-info #:with [[kw/b- ...] ...] #'[[kw b-] ...] + #:do [(define prop-inst (prop-instantiate (stx-map get-arg-obj #'[a- ...])))] -------- - [⊢ (ro:#%app f- a- ... kw/b- ... ...) ⇒ τ_out]] + [⊢ (ro:#%app f- a- ... kw/b- ... ...) + (⇒ : τ_out) + (⇒ prop+ #,(syntax-local-introduce (prop-inst #'posprop))) + (⇒ prop- #,(syntax-local-introduce (prop-inst #'negprop)))]] ;; concrete union functions [(_ f:expr a:expr ... (~seq kw:keyword b:expr) ...) ≫ ;[⊢ [f ≫ f-- ⇒ : (~and (~CU* τ_f ...) ~!)]] diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 0f40818..517b11f 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -818,13 +818,47 @@ (syntax-parse new [(~CU* n ...) #`(CU #,@(for/list ([n (in-list (stx->list #'[n ...]))]) - (type-restrict orig n)))]))] + (type-restrict orig n)))] + [(~U* n ...) + (define ns* + (for/list ([n (in-list (stx->list #'[n ...]))]) + (type-restrict orig n))) + (cond + [(and (concrete? orig) (andmap concrete? ns*)) + #`(CU #,@ns*)] + [else + #`(U #,@ns*)])]))] + [(Term*? new) + (syntax-parse new + [(~Term* n) + (define n* (type-restrict orig #'n)) + (cond + [(concrete? orig) n*] + [else ((current-type-eval) #`(Term #,n*))])])] [(Un? orig) ((current-type-eval) (syntax-parse orig [(~CU* o ...) #`(CU #,@(for/list ([o (in-list (stx->list #'[o ...]))]) - (type-restrict o new)))]))] + (type-restrict o new)))] + [(~U* o ...) + ;; TODO: What does a U type mean, and can we safely reduce + ;; cases within U types? + (define os* + (for/list ([o (in-list (stx->list #'[o ...]))]) + (type-restrict o new))) + (cond + [(and (concrete? new) (andmap concrete? os*)) + #`(CU #,@os*)] + [else + #`(U #,@os*)])]))] + [(Term*? orig) + (syntax-parse orig + [(~Term* o) + (define o* (type-restrict #'o new)) + (cond + [(concrete? new) o*] + [else ((current-type-eval) #`(Term #,o*))])])] [else (syntax-parse (list orig new) [[~CZero ~CPosInt] typeCNothing] @@ -853,7 +887,19 @@ (syntax-parse orig [(~CU* o ...) #`(CU #,@(for/list ([o (in-list (stx->list #'[o ...]))]) - (type-remove o new-not)))]))] + (type-remove o new-not)))] + [(~U* o ...) + ;; TODO: What does a U type mean, and can we safely remove + ;; from cases of U types? + (define os* + (for/list ([o (in-list (stx->list #'[o ...]))]) + (type-remove o new-not))) + #`(U #,@os*)]))] + [(Term*? orig) + (syntax-parse orig + [(~Term* o) + (define o* (type-remove #'o new-not)) + ((current-type-eval) #`(Term #,o*))])] [else orig])) From 9ac95deb5ec722558e8c86d32875c23d88784145 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 26 Apr 2017 17:54:13 -0700 Subject: [PATCH 10/24] add propositions to function types in Typed Rosette proper --- test/typed-rosette/occurrence.rkt | 32 ++--------------- typed/rosette.rkt | 60 +++++++++++-------------------- typed/rosette/types.rkt | 8 +++++ 3 files changed, 32 insertions(+), 68 deletions(-) diff --git a/test/typed-rosette/occurrence.rkt b/test/typed-rosette/occurrence.rkt index 96f60da..ecdeec1 100644 --- a/test/typed-rosette/occurrence.rkt +++ b/test/typed-rosette/occurrence.rkt @@ -5,27 +5,6 @@ (only-in typed/rosette/base-forms unsafe-assign-type) (prefix-in $ rosette)) -(define integer? - (unsafe-assign-type $integer? - : (Ccase-> - (C→* [CAny] [] CBool - : #:+ (@ 0 : CInt) #:- (!@ 0 : CInt)) - (C→* [Any] [] Bool - : #:+ (@ 0 : Int) #:- (!@ 0 : Int))))) - -(define boolean? - (unsafe-assign-type $boolean? - : (Ccase-> - (C→* [CAny] [] CBool - : #:+ (@ 0 : CBool) #:- (!@ 0 : CBool)) - (C→* [Any] [] Bool - : #:+ (@ 0 : Bool) #:- (!@ 0 : Bool))))) - -(define string? - (unsafe-assign-type $string? - : (C→* [CAny] [] CBool - : #:+ (@ 0 : CString) #:- (!@ 0 : CString)))) - (define natural? (unsafe-assign-type $exact-nonnegative-integer? : (Ccase-> @@ -34,29 +13,24 @@ (C→* [Any] [] Bool : #:+ (@ 0 : Nat) #:- (!@ 0 : Nat))))) -(define add1 - (unsafe-assign-type $add1 - : (Ccase-> (C→ CNat CPosInt) - (C→ Nat PosInt)))) - (define unneg (unsafe-assign-type $- : (Ccase-> (C→ CNegInt CPosInt) (C→ NegInt PosInt)))) -(: f : (C→ CInt CNat)) +(: f : (C→ CInt CPosInt)) (define (f x) (if (natural? x) (add1 x) (unneg x))) -(: f/restricted : (C→ CPosInt CNat)) +(: f/restricted : (C→ CPosInt CPosInt)) (define (f/restricted x) (if (natural? x) (add1 x) (unneg x))) -(: f* : (C→ Int Nat)) +(: f* : (C→ Int PosInt)) (define (f* x) (if (natural? x) (add1 x) diff --git a/typed/rosette.rkt b/typed/rosette.rkt index bb54b37..f6f9334 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -861,13 +861,13 @@ [not : LiftedPred] [xor : (Ccase-> (C→ CAny CAny CAny) (C→ Any Any Any))] - [false? : LiftedPred] + [false? : (LiftedPredFor False)] [true : CTrue] [false : CFalse] [real->integer : (C→ Num Int)] - [string? : UnliftedPred] - [number? : LiftedPred] + [string? : (UnliftedPredFor CString)] + [number? : (LiftedPredFor Num)] [positive? : LiftedNumPred] [negative? : LiftedNumPred] [zero? : LiftedNumPred] @@ -895,44 +895,26 @@ ;; --------------------------------- ;; more built-in ops +(define-simple-macro + (define-solvable-type-predicate pred? ro-pred? CType Type) + (begin- + (provide- pred?) + (define-syntax- pred? + (make-variable-like-transformer + (attach (⊢ (mark-solvablem ro-pred?) : (LiftedPredFor Type)) + 'typefor + ((current-type-eval) #'(Term CType))))))) + ;(define-rosette-primop boolean? : (C→ Any Bool)) -(define-typed-syntax boolean? - [_:id ≫ - -------- - [⊢ (mark-solvablem - ro:boolean?) - (⇒ : LiftedPred) - (⇒ typefor (Term CBool))]] - [(_ e) ≫ - [⊢ e ≫ e- ⇒ ty] - -------- - [⊢ (ro:boolean? e-) ⇒ #,(if (concrete? #'ty) #'CBool #'Bool)]]) +(define-solvable-type-predicate boolean? ro:boolean? CBool Bool) ;(define-rosette-primop integer? : (C→ Any Bool)) -(define-typed-syntax integer? - [_:id ≫ - -------- - [⊢ (mark-solvablem - ro:integer?) - (⇒ : LiftedPred) - (⇒ typefor (Term CInt))]] - [(_ e) ≫ - [⊢ e ≫ e- ⇒ ty] - -------- - [⊢ (ro:integer? e-) ⇒ #,(if (concrete? #'ty) #'CBool #'Bool)]]) +(define-solvable-type-predicate integer? ro:integer? CInt Int) ;(define-rosette-primop real? : (C→ Any Bool)) -(define-typed-syntax real? - [_:id ≫ - -------- - [⊢ (mark-solvablem - ro:real?) - (⇒ : LiftedPred) - (⇒ typefor (Term CNum))]] - [(_ e) ≫ - [⊢ e ≫ e- ⇒ ty] - -------- - [⊢ (ro:real? e-) ⇒ #,(if (concrete? #'ty) #'CBool #'Bool)]]) +(define-solvable-type-predicate real? ro:real? CNum Num) + + (define-typed-syntax time [(_ e) ≫ @@ -1005,7 +987,7 @@ (provide (typed-out [bv : (Ccase-> (C→ CInt CBVPred CBV) (C→ CInt CPosInt CBV))] - [bv? : LiftedPred] + [bv? : (LiftedPredFor BV)] [bveq : (C→ BV BV Bool)] [bvslt : (C→ BV BV Bool)] @@ -1209,7 +1191,7 @@ (provide (typed-out [sat? : UnliftedPred] [unsat? : UnliftedPred] - [solution? : UnliftedPred] + [solution? : (UnliftedPredFor CSolution)] [unknown? : UnliftedPred] [sat : (Ccase-> (C→ CSolution) (C→ (CHashTable Any Any) CSolution))] @@ -1345,7 +1327,7 @@ ;(define-rosette-primop gen:solver : CSolver) (provide (typed-out - [solver? : UnliftedPred] + [solver? : (UnliftedPredFor CSolver)] [solver-assert : (C→ CSolver (CListof Bool) CUnit)] [solver-clear : (C→ CSolver CUnit)] [solver-minimize : (C→ CSolver (CListof (U Int Num BV)) CUnit)] diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 517b11f..0867f95 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -61,6 +61,7 @@ COutputPort CSolution CSolver CPict CRegexp CSymbol LiftedPred LiftedPred2 LiftedNumPred LiftedIntPred UnliftedPred + LiftedPredFor UnliftedPredFor (for-syntax ~CUnit CUnit? ~CString CString? ~CTrue ~CFalse) @@ -546,6 +547,13 @@ (define-named-type-alias CBVPred LiftedPred) (define-named-type-alias BVPred (add-predm (U LiftedPred) lifted-bitvector?)) +(define-simple-macro (LiftedPredFor τ:type) + (Ccase-> (C→* [CAny] [] CBool : #:+ (@ 0 : τ.norm) #:- (!@ 0 : τ.norm)) + (C→* [Any] [] Bool : #:+ (@ 0 : τ.norm) #:- (!@ 0 : τ.norm)))) + +(define-simple-macro (UnliftedPredFor τ:type) + (C→* [Any] [] CBool : #:+ (@ 0 : τ.norm) #:- (!@ 0 : τ.norm))) + ;; --------------------------------------------------------- ;; Merging From 0ce9ce37993dd016d10543c9dfb310a943b521c9 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 27 Apr 2017 20:53:16 -0700 Subject: [PATCH 11/24] support occurrence props for not --- test/typed-rosette/occurrence2.rkt | 7 +++++++ typed/rosette.rkt | 14 +++++++++++++- typed/rosette/types.rkt | 20 ++++++++++++++++++++ 3 files changed, 40 insertions(+), 1 deletion(-) create mode 100644 test/typed-rosette/occurrence2.rkt diff --git a/test/typed-rosette/occurrence2.rkt b/test/typed-rosette/occurrence2.rkt new file mode 100644 index 0000000..79d94c6 --- /dev/null +++ b/test/typed-rosette/occurrence2.rkt @@ -0,0 +1,7 @@ +#lang typed/rosette + +(: f : (C→ (CU CInt CFalse) CInt)) +(define (f x) + (if (not (false? x)) + (ann x : CInt) + 0)) diff --git a/typed/rosette.rkt b/typed/rosette.rkt index f6f9334..7eb34b5 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -858,7 +858,6 @@ (C→ CNum CNum CNum) (C→ Num Num Num))] - [not : LiftedPred] [xor : (Ccase-> (C→ CAny CAny CAny) (C→ Any Any Any))] [false? : (LiftedPredFor False)] @@ -1165,6 +1164,19 @@ -------- [⊢ [_ ≫ (ro:or e- ...) ⇒ : #,(type-merge* (cons typeCFalse #'[ty ...]))]]]) +(define-typed-syntax not + [:id ≫ + -------- + [⊢ ro:not ⇒ (LiftedPredFor False)]] + [(_ e) ≫ + [⊢ e ≫ e- (⇐ : CBool) (⇒ prop+ p+) (⇒ prop- p-)] + -------- + [⊢ [_ ≫ (ro:not e-) (⇒ : CBool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]] + [(_ e) ≫ + [⊢ e ≫ e- (⇒ : _) (⇒ prop+ p+) (⇒ prop- p-)] + -------- + [⊢ [_ ≫ (ro:not e-) (⇒ : Bool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]]) + (define-typed-syntax nand [(_) ≫ -------- diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 0867f95..19873a5 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -18,6 +18,11 @@ C→? Ccase->?) ;; Propositions for Occurrence typing @ !@ + Prop + Prop/Top + Prop/Bot + Prop/ObjType + Prop/ObjNotType Prop/Or Prop/And with-occurrence-prop @@ -258,6 +263,21 @@ [(_ i:nat : τ:type) #'(Prop/IndexNotType- (quote- i) τ.norm)]) +(define-syntax-parser Prop/ObjType + #:datum-literals [:] + [(_ o : τ:type) + #'(Prop/ObjType- o τ.norm)]) +(define-syntax-parser Prop/ObjNotType + #:datum-literals [:] + [(_ o : τ:type) + #'(Prop/ObjNotType- o τ.norm)]) + +(define-syntax-parser Prop + [(_ p) + (if (syntax-e #'p) + #'p + #'Prop/Top)]) + (define-syntax-parser Prop/Or [(_ p ...) (if (stx-andmap syntax-e #'[p ...]) From 325e7cd5b107a7afdc01bb92c1e719616be40741 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Thu, 27 Apr 2017 21:14:59 -0700 Subject: [PATCH 12/24] add struct type constructor --- typed/rosette/types.rkt | 70 +++++++++++++++++++++++++++++++++++++++-- 1 file changed, 67 insertions(+), 3 deletions(-) diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 19873a5..9dcbe8e 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -10,6 +10,13 @@ ~CU* ~U* CU*? U*? ~Constant* Constant*? remove-Constant concrete?) + ;; Struct types + Struct + (for-syntax typed-struct-id + typed-struct-info + typed-struct-info-predicate + typed-struct-info-accessors + typed-struct-info-field-types) ;; Function types C→ C→* Ccase-> → @@ -104,7 +111,10 @@ (prefix-in ro: rosette/lib/synthax) (rename-in "../rosette-util.rkt" [bitvector? lifted-bitvector?])) -(require (for-syntax syntax/id-table)) +(require (for-syntax racket/struct-info + syntax/id-table + syntax/parse/class/local-value + syntax/parse/class/struct-id)) ;; --------------------------------- ;; Concrete and Symbolic union types @@ -232,6 +242,41 @@ -------- [⊢ (CVector- τ.norm ...) ⇒ :: #%type]) +;; Struct +(define-internal-type-constructor Struct) + +;; Struct types can't be single-shape types because struct inheritance exists. + +(begin-for-syntax + (struct typed-struct-info + [transformer untyped-id predicate accessors field-types some-mutable?] + #:property prop:procedure (struct-field-index transformer) + #:property prop:struct-info + (λ (self) + (extract-struct-info + (syntax-local-value (typed-struct-info-untyped-id self))))) + + (define-syntax-class typed-struct-id + #:attributes [[accessor 1] [τ_fld 1] [τ_fld_merged 1] some-mutable?] + [pattern (~var struct-id (local-value typed-struct-info?)) + #:with [accessor ...] + (typed-struct-info-accessors (attribute struct-id.local-value)) + #:with [τ_fld ...] + (typed-struct-info-field-types (attribute struct-id.local-value)) + #:with [τ_fld_merged ...] + (stx-map type-merge #'[τ_fld ...] #'[τ_fld ...]) + #:attr some-mutable? + (typed-struct-info-some-mutable? (attribute struct-id.local-value))])) + +(define-typed-syntax Struct + [(_ s:typed-struct-id τ:type ...) ≫ + #:fail-unless (stx-length=? #'[s.τ_fld_merged ...] #'[τ.norm ...]) + "wrong number of fields" + [τ.norm τ⊑ s.τ_fld_merged] ... + -------- + [⊢ (Struct- (quote-syntax- s) τ.norm ...) + ⇒ :: #%type]]) + ;; --------------------------------- ;; Pattern Expanders for Types @@ -701,6 +746,18 @@ ;; otherwise, some more complicated merging is ;; needed, using both a U on the outside and ;; possibly more merges in sub-parts + [(and (Struct? a) (Struct? b)) + (syntax-parse (list a b) + #:literals [quote-syntax-] + [[(~Struct (quote-syntax- sa:id) τa ...) + (~Struct (quote-syntax- sb:id) τb ...)] + #:when (free-identifier=? #'sa #'sb) + #:with [τab ...] (stx-map type-merge #'[τa ...] #'[τb ...]) + ((current-type-eval) #'(U (Struct sa τab ...)))] + [_ + ;; TODO: do some merging within if they are related by + ;; sub-structing + ((current-type-eval) #`(U #,a #,b))])] [else ;; TODO: do some merging within ((current-type-eval) #`(U #,a #,b))])) @@ -991,10 +1048,10 @@ [⊢ (let- ([x- x] ...) body-) ⇒ τ_body]]) ;; (with-occurrence-prop prop expr) -;; The prop must already be expanded (define-syntax-parser with-occurrence-prop [(_ prop:expr body:expr) - #:with env:occurrence-env (prop->env #'prop) + #:with env:occurrence-env + (prop->env (expand/df (if (syntax-e #'prop) #'prop #'Prop/Top))) #'(with-occurrence-env env body)]) ;; --------------------------------------------------------- @@ -1013,6 +1070,7 @@ (and (concrete/recur? t1) (CAny? t2)) ((current-type=?) t1 t2) (syntax-parse (list t1 t2) + #:literals [quote-syntax-] ;; Constant clause must appear before U, ow (Const Int) <: Int wont hold [((~Constant* ty1) (~Constant* ty2)) (typecheck? #'ty1 #'ty2)] @@ -1039,6 +1097,12 @@ [((~CPair ty1a ty1b) (~CPair ty2a ty2b)) (and (typecheck? #'ty1a #'ty2a) (typecheck? #'ty1b #'ty2b))] + ;; structs, if they are immutable, they are covariant + [((~Struct (quote-syntax- sa:typed-struct-id) τa ...) + (~Struct (quote-syntax- sb:typed-struct-id) τb ...)) + #:when (free-identifier=? #'sa #'sb) + #:when (not (attribute sa.some-mutable?)) + (typechecks? #'[τa ...] #'[τb ...])] ; 2 U types, subtype = subset [((~CU* . ts1) _) (for/and ([t (stx->list #'ts1)]) From 8e3921407670d8b1e375f3bec4c81b5ef2dc3e4a Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 5 Apr 2017 14:22:23 -0700 Subject: [PATCH 13/24] add predicates for concrete-only types --- typed/rosette/concrete-predicate.rkt | 47 ++++++++++++++++++++++++++++ typed/rosette/types.rkt | 11 ++++--- 2 files changed, 53 insertions(+), 5 deletions(-) create mode 100644 typed/rosette/concrete-predicate.rkt diff --git a/typed/rosette/concrete-predicate.rkt b/typed/rosette/concrete-predicate.rkt new file mode 100644 index 0000000..b9a4dbd --- /dev/null +++ b/typed/rosette/concrete-predicate.rkt @@ -0,0 +1,47 @@ +#lang racket/base + +(provide concrete-boolean? + concrete-integer? + concrete-zero-integer? + concrete-positive-integer? + concrete-negative-integer? + concrete-nonnegative-integer? + concrete-real? + concrete-positive-real? + concrete-negative-real? + concrete-nonnegative-real? + ) + +(require (only-in racket/base + [boolean? concrete-boolean?] + [integer? concrete-integer?] + [real? concrete-real?])) + +;; concrete-zero-integer? : Any -> Bool +(define (concrete-zero-integer? x) + (and (concrete-integer? x) (zero? x))) + +;; concrete-positive-integer? : Any -> Bool +(define (concrete-positive-integer? x) + (and (concrete-integer? x) (positive? x))) + +;; concrete-negative-integer? : Any -> Bool +(define (concrete-negative-integer? x) + (and (concrete-integer? x) (negative? x))) + +;; concrete-nonnegative-integer? : Any -> Bool +(define (concrete-nonnegative-integer? x) + (and (concrete-integer? x) (not (negative? x)))) + +;; concrete-positive-real? : Any -> Bool +(define (concrete-positive-real? x) + (and (concrete-real? x) (positive? x))) + +;; concrete-negative-real? : Any -> Bool +(define (concrete-negative-real? x) + (and (concrete-real? x) (negative? x))) + +;; concrete-nonnegative-real? : Any -> Bool +(define (concrete-nonnegative-real? x) + (and (concrete-real? x) (not (negative? x)))) + diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 9dcbe8e..b53db69 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -109,7 +109,8 @@ [List CListof] [~List ~CListof]) (prefix-in ro: rosette) (prefix-in ro: rosette/lib/synthax) - (rename-in "../rosette-util.rkt" [bitvector? lifted-bitvector?])) + (rename-in "../rosette-util.rkt" [bitvector? lifted-bitvector?]) + "concrete-predicate.rkt") (require (for-syntax racket/struct-info syntax/id-table @@ -448,11 +449,11 @@ ;; --------------------------------- ;; Concrete types -(define-named-type-alias CBool (CU CFalse CTrue)) +(define-named-type-alias CBool (add-predm (CU CFalse CTrue) concrete-boolean?)) -(define-named-type-alias CNat (CU CZero CPosInt)) -(define-named-type-alias CInt (CU CNegInt CNat)) -(define-named-type-alias CNum (CU CFloat CInt)) +(define-named-type-alias CNat (add-predm (CU CZero CPosInt) concrete-nonnegative-integer?)) +(define-named-type-alias CInt (add-predm (CU CNegInt CNat) concrete-integer?)) +(define-named-type-alias CNum (add-predm (CU CFloat CInt) concrete-real?)) (begin-for-syntax (define (concrete-type-solvable? τ) From 5e95f64afe240942bcbd6b2b9c434d8c9816c41e Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Mon, 12 Jun 2017 15:43:53 -0400 Subject: [PATCH 14/24] continue --- sdsl/typed-fsm/fsm.rkt | 2 +- test/rosette-tests.rkt | 16 +- typed/rosette-util.rkt | 7 +- typed/rosette.rkt | 132 +++++------- typed/rosette/base-forms.rkt | 12 +- typed/rosette/forms-pre-match.rkt | 114 ++++++++++ typed/rosette/match-core.rkt | 342 ++++++++++++++++++++++++++++++ typed/rosette/match-pat-forms.rkt | 157 ++++++++++++++ typed/rosette/types.rkt | 189 ++++++++++++++--- 9 files changed, 842 insertions(+), 129 deletions(-) create mode 100644 typed/rosette/forms-pre-match.rkt create mode 100644 typed/rosette/match-core.rkt create mode 100644 typed/rosette/match-pat-forms.rkt diff --git a/sdsl/typed-fsm/fsm.rkt b/sdsl/typed-fsm/fsm.rkt index faec12e..809d21c 100644 --- a/sdsl/typed-fsm/fsm.rkt +++ b/sdsl/typed-fsm/fsm.rkt @@ -1,5 +1,5 @@ #lang turnstile -(extends typed/main #:prefix rosette: #:except #%datum #%app define) +(extends typed/main #:prefix rosette: #:except #%datum #%app define ?) (require (prefix-in ro: rosette) ; untyped (prefix-in rosette: "../../typed/lib/synthax.rkt") (prefix-in rosette: "../../typed/query/debug.rkt") diff --git a/test/rosette-tests.rkt b/test/rosette-tests.rkt index d3c003d..d47c6c6 100644 --- a/test/rosette-tests.rkt +++ b/test/rosette-tests.rkt @@ -361,17 +361,17 @@ (check-type (not #f) : CAny) (check-type (equal? 1 2) : CAny) -;; data structures have type CAny only if elements are concrete +;; data structures have type CAnyDeep only if elements are concrete ;; (even if outer structure is concrete) -(check-type (list 1 2 3) : CAny) -(check-not-type (list i0 b0) : CAny) -(check-type (list (list 1 2) (list 3 4)) : CAny) -(check-type (list (list (list 1 2) 3) 4) : CAny) -(check-not-type (list (list (list i0 2) 3) 4) : CAny) +(check-type (list 1 2 3) : CAnyDeep) +(check-not-type (list i0 b0) : CAnyDeep) +(check-type (list (list 1 2) (list 3 4)) : CAnyDeep) +(check-type (list (list (list 1 2) 3) 4) : CAnyDeep) +(check-not-type (list (list (list i0 2) 3) 4) : CAnyDeep) ;; Boxes are mutable, so they contain possibly-symbolic types -(check-not-type (box 1) : CAny) -(check-not-type (box i0) : CAny) +(check-not-type (box 1) : CAnyDeep) +(check-not-type (box i0) : CAnyDeep) ;; Subtyping between Terms and Unions (check-type (ann (ann 1 : CNum) : (Term CNum)) : Num) diff --git a/typed/rosette-util.rkt b/typed/rosette-util.rkt index 91e5189..ac46918 100644 --- a/typed/rosette-util.rkt +++ b/typed/rosette-util.rkt @@ -18,8 +18,11 @@ (define (assert-pred a pred) (if (type? pred) (type-cast pred a) - (begin - (assert (pred a)) + (let ([pass? (pred a)]) + (when (and (not (union? pass?)) (not (term? pass?)) (false? pass?)) + (printf "assert-pred failed outright\n a: ~v\n pred: ~v\n" + a pred)) + (assert pass?) a))) ;; zero-integer? : Any -> Bool diff --git a/typed/rosette.rkt b/typed/rosette.rkt index 7eb34b5..2fc5b26 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -11,20 +11,24 @@ ;; import typed rosette types "rosette/types.rkt" ;; import base forms - (rename-in "rosette/base-forms.rkt" [#%app app]) + (rename-in (except-in "rosette/base-forms.rkt" list) [#%app app]) + "rosette/match-core.rkt" + "rosette/match-pat-forms.rkt" "rosette/struct-type-properties.rkt" ;; base lang (prefix-in ro: (combine-in rosette rosette/lib/synthax)) (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) -(provide : define set! λ apply ann begin list +(provide : define set! λ apply ann begin let (rename-out [app #%app] [ro:#%module-begin #%module-begin] [λ lambda]) + match match-let _ var ? + (all-from-out "rosette/match-pat-forms.rkt") prop:procedure struct-field-index (for-syntax get-pred expand/ro) - CAny Any CNothing Nothing + CAnyDeep CAny Any CNothing Nothing Term CU U (for-syntax ~CU* ~U*) Constant @@ -200,31 +204,6 @@ #:with es+ (stx-map expand/df #'es) (assign-type #'(ro:#%app f . es+) #'ty-out)])))]]) -;; --------------------------------- -;; quote - -(define-typed-syntax quote - ;; base case: symbol - [(_ x:id) ≫ - -------- - [⊢ (ro:quote x) ⇒ CSymbol]] - ;; recur: list (this clause should come before pair) - [(_ (x ...)) ≫ - [⊢ (quote x) ≫ (_ x-) ⇒ τ] ... - -------- - [⊢ (ro:quote (x- ...)) ⇒ (CList τ ...)]] - ;; recur: pair - [(_ (x . y)) ≫ - [⊢ (quote x) ≫ (_ x-) ⇒ τx] - [⊢ (quote y) ≫ (_ y-) ⇒ τy] - -------- - [⊢ (ro:quote (x- . y-)) ⇒ (CPair τx τy)]] - ;; base case: other datums - [(_ x) ≫ - [⊢ (stlc+union:#%datum . x) ≫ (_ x-) ⇒ τ] - -------- - [⊢ (ro:quote x-) ⇒ τ]]) - ;; --------------------------------- ;; if @@ -601,6 +580,14 @@ "expected function that consumes concrete Nat" -------- [⊢ [_ ≫ (ro:build-list n- f-) ⇒ : (CListof ty2)]]]) + +(define-typed-syntax make-list + [(_ n v) ≫ + [⊢ n ≫ n- ⇐ : CNat] + [⊢ v ≫ v- ⇒ : τ] + -------- + [⊢ (ro:make-list n- v-) ⇒ : (CListof τ)]]) + (define-typed-syntax map #;[_:id ≫ ;; TODO: use polymorphism -------- @@ -712,8 +699,8 @@ [string-length : (C→ CString CNat)] [string-append : (C→ CString CString CString)] - [equal? : LiftedPred2] - [eq? : LiftedPred2] + [equal? : LiftedPredDeep2] + [eq? : LiftedPredDeep2] [distinct? : (Ccase-> (C→* [] [] #:rest (CListof CAny) CBool) (C→* [] [] #:rest (CListof Any) Bool) (C→* [] [] #:rest (Listof Any) Bool))] @@ -1122,60 +1109,7 @@ -------- [⊢ [_ ≫ (ro:|| e- ...) ⇒ : Bool]]]) -(define-typed-syntax and - [(_) ≫ - -------- - [⊢ [_ ≫ (ro:and) ⇒ : CTrue]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇐ : Bool] ...] - -------- - [⊢ [_ ≫ (ro:and e- ...) ⇒ : Bool]]] - [(_ e ... elast) ≫ - [⊢ [e ≫ e- ⇒ : ty] ...] - [⊢ [elast ≫ elast- ⇒ : ty-last]] - -------- - [⊢ [_ ≫ (ro:and e- ... elast-) ⇒ : #,(type-merge typeCFalse #'ty-last)]]]) - -(define-typed-syntax or - [(_) ≫ - -------- - [⊢ [_ ≫ (ro:or) - (⇒ : CFalse) - (⇒ prop+ Prop/Bot) - (⇒ prop- Prop/Top)]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- (⇐ : CBool) (⇒ prop+ p+) (⇒ prop- p-)] - ...] - -------- - [⊢ [_ ≫ (ro:or e- ...) - (⇒ : CBool) - (⇒ prop+ (Prop/Or p+ ...)) - (⇒ prop- (Prop/And p- ...))]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- (⇐ : Bool) (⇒ prop+ p+) (⇒ prop- p-)] - ...] - -------- - [⊢ [_ ≫ (ro:or e- ...) - (⇒ : Bool) - (⇒ prop+ (Prop/Or p+ ...)) - (⇒ prop- (Prop/And p- ...))]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇒ : ty] ...] - -------- - [⊢ [_ ≫ (ro:or e- ...) ⇒ : #,(type-merge* (cons typeCFalse #'[ty ...]))]]]) - -(define-typed-syntax not - [:id ≫ - -------- - [⊢ ro:not ⇒ (LiftedPredFor False)]] - [(_ e) ≫ - [⊢ e ≫ e- (⇐ : CBool) (⇒ prop+ p+) (⇒ prop- p-)] - -------- - [⊢ [_ ≫ (ro:not e-) (⇒ : CBool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]] - [(_ e) ≫ - [⊢ e ≫ e- (⇒ : _) (⇒ prop+ p+) (⇒ prop- p-)] - -------- - [⊢ [_ ≫ (ro:not e-) (⇒ : Bool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]]) +;; and, or, and not are defined in rosette/forms-pre-match.rkt (define-typed-syntax nand [(_) ≫ @@ -1378,6 +1312,21 @@ (define-typed-syntax for/all ;; symbolic e + [(_ ([x:id e]) e_body) ⇐ τ_body ≫ + [⊢ [e ≫ e- ⇒ : (~U* τ_case ...)]] + #:with τ_x (cond [(= 1 (stx-length #'[τ_case ...])) + (stx-car #'[τ_case ...])] + [(stx-andmap concrete? #'[τ_case ...]) + #'(CU τ_case ...)] + [else + #'(U τ_case ...)]) + [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇐ : τ_body]] + ;; Merge the τ_body with itself + #:with τ_out (type-merge #'τ_body #'τ_body) + ;; Check that it's a subtype of τ_body, context is expecting that + [τ_out τ⊑ τ_body] + -------- + [⊢ (ro:for/all ([x- e-]) e_body-)]] [(_ ([x:id e]) e_body) ≫ [⊢ [e ≫ e- ⇒ : (~U* τ_case ...)]] #:with τ_x (cond [(= 1 (stx-length #'[τ_case ...])) @@ -1392,6 +1341,12 @@ -------- [⊢ [_ ≫ (ro:for/all ([x- e-]) e_body-) ⇒ : τ_out]]] ;; known concrete e + [(_ ([x:id e]) e_body) ⇐ τ_body ≫ + [⊢ [e ≫ e- ⇒ : τ_x]] + #:when (concrete? #'τ_x) + [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇐ : τ_body]] + -------- + [⊢ (ro:for/all ([x- e-]) e_body-)]] [(_ ([x:id e]) e_body) ≫ [⊢ [e ≫ e- ⇒ : τ_x]] #:when (concrete? #'τ_x) @@ -1400,6 +1355,15 @@ [⊢ [_ ≫ (ro:for/all ([x- e-]) e_body-) ⇒ : τ_body]]] ;; other, for example a symbolic constant, an Any type, or a symbolic union ;; type that didn't pass the first case + [(_ ([x:id e]) e_body) ⇐ τ_body ≫ + [⊢ [e ≫ e- ⇒ : τ_x]] + [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇐ : τ_body]] + ;; Merge the τ_body with itself + #:with τ_out (type-merge #'τ_body #'τ_body) + ;; Check that it's a subtype of τ_body, context is expecting that + [τ_out τ⊑ τ_body] + -------- + [⊢ (ro:for/all ([x- e-]) e_body-)]] [(_ ([x:id e]) e_body) ≫ [⊢ [e ≫ e- ⇒ : τ_x]] [() ([x ≫ x- : τ_x]) ⊢ [e_body ≫ e_body- ⇒ : τ_body]] diff --git a/typed/rosette/base-forms.rkt b/typed/rosette/base-forms.rkt index 1f83e4b..32ee07d 100644 --- a/typed/rosette/base-forms.rkt +++ b/typed/rosette/base-forms.rkt @@ -513,7 +513,7 @@ #:with (b* ...) (generate-temporaries #'(b ...)) #:with [[kw/b* ...] ...] #'[[kw b*] ...] [([f* ≫ _ : τ_f] [a* ≫ _ : τ_a] ... [b* ≫ _ : τ_b] ...) - ⊢ [(app f* a* ... kw/b* ... ...) ≫ _ ⇒ : τ_out]] + ⊢ [#,(syntax/loc this-syntax (app f* a* ... kw/b* ... ...)) ≫ _ ⇒ : τ_out]] ... #:with [[kw/b- ...] ...] #'[[kw b-] ...] -------- @@ -591,7 +591,7 @@ (define-typed-syntax let #:datum-literals [:] - [(_ name:id ~! ([x:id : τ_x:type e:expr] ...) :-> τ_out:type b ...+) ≫ + [(_ name:id ([x:id : τ_x:type e:expr] ...) :-> ~! τ_out:type b ...+) ≫ [⊢ [e ≫ e- ⇐ τ_x] ...] #:with body (syntax/loc this-syntax (begin b ...)) [[name ≫ name- : (C→ τ_x ... τ_out)] @@ -599,6 +599,14 @@ ⊢ body ≫ body- ⇐ τ_out] -------- [⊢ (let- name- ([x- e-] ...) body-) ⇒ τ_out]] + [(_ name:id ([x:id : τ_x:type e:expr] ...) b ...+) ⇐ τ_out ≫ + [⊢ [e ≫ e- ⇐ τ_x] ...] + #:with body (syntax/loc this-syntax (begin b ...)) + [[name ≫ name- : (C→ τ_x ... τ_out)] + [x ≫ x- : τ_x] ... + ⊢ body ≫ body- ⇐ τ_out] + -------- + [⊢ (let- name- ([x- e-] ...) body-)]] [(_ ([x m:mut-kw e] ...) e_body ...) ⇐ τ_expected ≫ [⊢ [e ≫ e- ⇒ : τ_x] ...] #:with [τ_x* ...] diff --git a/typed/rosette/forms-pre-match.rkt b/typed/rosette/forms-pre-match.rkt new file mode 100644 index 0000000..fb49d41 --- /dev/null +++ b/typed/rosette/forms-pre-match.rkt @@ -0,0 +1,114 @@ +#lang turnstile + +(provide quote + and or not) + +(require "types.rkt" + (rename-in "base-forms.rkt" [#%app app]) + (prefix-in ro: rosette) + (prefix-in stlc+union: turnstile/examples/stlc+union) + ) + +;; ------------------------------------------------------------------------ + +;; quote + +(define-typed-syntax quote + ;; base case: symbol + [(_ x:id) ≫ + -------- + [⊢ (ro:quote x) ⇒ CSymbol]] + ;; recur: list (this clause should come before pair) + [(_ (x ...)) ≫ + [⊢ (quote x) ≫ (_ x-) ⇒ τ] ... + -------- + [⊢ (ro:quote (x- ...)) ⇒ (CList τ ...)]] + ;; recur: pair + [(_ (x . y)) ≫ + [⊢ (quote x) ≫ (_ x-) ⇒ τx] + [⊢ (quote y) ≫ (_ y-) ⇒ τy] + -------- + [⊢ (ro:quote (x- . y-)) ⇒ (CPair τx τy)]] + ;; base case: other datums + [(_ x) ≫ + [⊢ (stlc+union:#%datum . x) ≫ (_ x-) ⇒ τ] + -------- + [⊢ (ro:quote x-) ⇒ τ]]) + +;; ------------------------------------------------------------------------ + +;; and, or, not + +(define-typed-syntax and + [(_) ≫ + -------- + [⊢ (ro:and) + (⇒ : CTrue) + (⇒ prop+ Prop/Top) + (⇒ prop- Prop/Bot)]] + [(_ e:expr) ≫ + [⊢ e ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + -------- + [⊢ e- (⇒ : τ) (⇒ prop+ (Prop p+)) (⇒ prop- (Prop p-))]] + [(_ e:expr ... e_l:expr) ≫ + [⊢ (and e ...) ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + [⊢ (with-occurrence-prop p+ e_l) ≫ e_l- + (⇒ : τ_l) + (⇒ prop+ pl+) + (⇒ prop- pl-)] + #:with τ_out (cond [(and (concrete? #'τ) (concrete? #'τ_l)) + #'(CU CFalse τ_l)] + [(concrete? #'τ) + #'(U CFalse τ_l)] + [else + (type-merge typeCFalse #'τ_l)]) + -------- + [⊢ (ro:and e- e_l-) + (⇒ : τ_out) + (⇒ prop+ (Prop/And (Prop p+) (Prop pl+))) + (⇒ prop- (Prop/Or (Prop p-) (Prop pl-)))]]) + +(define-typed-syntax or + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:or) + (⇒ : CFalse) + (⇒ prop+ Prop/Bot) + (⇒ prop- Prop/Top)]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- (⇐ : CBool) (⇒ prop+ p+) (⇒ prop- p-)] + ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) + (⇒ : CBool) + (⇒ prop+ (Prop/Or p+ ...)) + (⇒ prop- (Prop/And p- ...))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- (⇐ : Bool) (⇒ prop+ p+) (⇒ prop- p-)] + ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) + (⇒ : Bool) + (⇒ prop+ (Prop/Or p+ ...)) + (⇒ prop- (Prop/And p- ...))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : ty] ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) ⇒ : #,(type-merge* (cons typeCFalse #'[ty ...]))]]]) + +(define-typed-syntax not + [:id ≫ + -------- + [⊢ ro:not ⇒ (LiftedPredFor False)]] + [(_ e) ≫ + [⊢ e ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + #:when (concrete? #'τ) + -------- + [⊢ [_ ≫ (ro:not e-) (⇒ : CBool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]] + [(_ e) ≫ + [⊢ e ≫ e- (⇒ : _) (⇒ prop+ p+) (⇒ prop- p-)] + -------- + [⊢ [_ ≫ (ro:not e-) (⇒ : Bool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]]) + +;; ------------------------------------------------------------------------ + diff --git a/typed/rosette/match-core.rkt b/typed/rosette/match-core.rkt new file mode 100644 index 0000000..2624f33 --- /dev/null +++ b/typed/rosette/match-core.rkt @@ -0,0 +1,342 @@ +#lang turnstile + +(provide match match-let + _ var ? + (for-syntax prop:match-pattern-id + match-pattern-id + macro/match-pattern-id + struct-predicate-accessor-pattern-id + ;; syntax classes + pat + pat-info + ;; other helpers + λ/pat-info + map-app3)) + +(require (postfix-in - rosette) + "types.rkt" + (only-in "base-forms.rkt" [#%app app*]) + (for-syntax lens/common + unstable/lens/syntax/stx + syntax/parse/class/local-value)) + +;; ------------------------------------------------------------------------ + +;; Match Patterns + +;; pat ::= derived-pat +;; | literal-pat +;; | id-pat + +;; derived-pat ::= match-pattern-id +;; | (match-pattern-id . rest) + +;; literal-pat ::= bool +;; | string +;; | number + +;; id-pat ::= id ; not match-pattern-id or `...` + +;; derived pats will include patterns like +;; | _ +;; | (var id) +;; | (? pred-expr) +;; | (? pred-expr pat) +;; | (_struct-name pat ...) +;; | (quote datum) +;; | (and pat ...) +;; | (or pat ...) ; TODO: branches conflict? +;; | (not pat) +;; | (list lv-pat ...) + +(begin-for-syntax + (define-values [prop:match-pattern-id + match-pattern-id? + match-pattern-id-ref] + (make-struct-type-property 'match-pattern-id)) + (define-syntax-class match-pat-id + #:attributes [get-get-pat-info] + [pattern (~var id (local-value match-pattern-id?)) + #:attr get-get-pat-info + (get-match-pattern-id-function (attribute id.local-value))]) + (define (get-match-pattern-id-function value) + (cond [(match-pattern-id? value) + (get-match-pattern-id-function + ((match-pattern-id-ref value) value))] + [else value])) + + ;; A PatInfo is a + ;; (StxList (StxListof (StxList Id TypeStx)) + ;; PropStx + ;; ExprStx) + (define-syntax-class pat-info + #:attributes [[x 1] [τ 1] pos-prop maybe-vec test-concrete?] + [pattern [([x:id τ:expr] ...) pos-prop maybe-vec test-concrete?]]) + (define-syntax-rule (λ/pat-info v-pat τ-pat obj-pat body ...) + (λ (v τ obj) + (syntax-parse (list v τ obj) + [[v-pat τ-pat obj-pat] body ...]))) + + ;; map-app3 : A B C (Listof [A B C -> D]) -> (Listof D) + (define (map-app3 a b c fs) + (for/list ([f (in-list fs)]) + (f a b c))) + + (define-syntax-class pat + #:attributes [get-pat-info] + ;; get-pat-info : [Stx TypeStx ObjStx -> PatInfo] + [pattern :derived-pat] + [pattern :literal-pat] + [pattern :id-pat]) + + (define-syntax-class id-pat + #:attributes [get-pat-info] + #:datum-literals [_ ...] + [pattern (~and x:id (~not (~or :match-pat-id ...))) + #:attr get-pat-info + (λ/pat-info v τ o #'[([x τ]) Prop/Top (vector-immutable- v) #t])]) + + (define-syntax-class literal-pat + #:attributes [get-pat-info] + [pattern b:boolean + #:attr get-pat-info + (λ/pat-info v τ o #'[() Prop/Top (if- (eq?- v (quote- b)) #() #f) #f])] + [pattern s:str + #:attr get-pat-info + (λ/pat-info v τ o #'[() Prop/Top (if- (eq?- v (quote- s)) #() #f) #f])] + [pattern n:number + #:attr get-pat-info + (λ/pat-info v τ o #'[() Prop/Top (if- (eq?- v (quote- n)) #() #f) #f])] + ) + + (define-syntax-class derived-pat + #:attributes [get-pat-info] + [pattern (~and stx id:match-pat-id) + #:attr get-pat-info + (derived-pat->get-info (attribute id.get-get-pat-info) #'stx)] + [pattern (~and stx (id:match-pat-id . _)) + #:attr get-pat-info + (derived-pat->get-info (attribute id.get-get-pat-info) #'stx)]) + + (define (derived-pat->get-info get-get-pat-info stx) + (define intro (make-syntax-introducer)) + (define stx* (intro stx)) + (define get-pat-info* (get-get-pat-info stx*)) + (define (get-pat-info v τ o) + (intro (get-pat-info* v τ o))) + get-pat-info) + ) + +;; ------------------------------------------------------------------------ + +;; Match + +(define-typed-syntax match + [(_ val:expr [pat:pat body:expr] ...) ≫ + [⊢ val ≫ val- ⇒ τ_val] + #:with obj (get-arg-obj #'val-) + #:with tmp (generate-temporary #'val) + #:with [p:pat-info ...] + (map-app3 #'tmp #'τ_val #'obj (attribute pat.get-pat-info)) + [[p.x ≫ x- : p.τ] ... + ⊢ (with-occurrence-prop p.pos-prop body) ≫ body- ⇒ τ_body] + ... + #:with τ_out + (cond [(stx-andmap syntax-e #'[p.test-concrete? ...]) + (cond [(stx-andmap concrete? #'[τ_body ...]) + #'(CU τ_body ...)] + [(= 1 (stx-length #'[τ_body ...])) + (stx-car #'[τ_body ...])] + [else + #'(U τ_body ...)])] + [else + (type-merge* #'[τ_body ...])]) + #:with failure- + #'(assert- #false (format- "no matching clause for ~v" tmp)) + #:with matching-expr- + (for/fold ([acc #'failure-]) + ([xs- (in-list (reverse (stx->list #'[[x- ...] ...])))] + [maybe-vec (in-list (reverse (stx->list #'[p.maybe-vec ...])))] + [body- (in-list (reverse (stx->list #'[body- ...])))]) + (with-syntax ([acc acc] + [v-tmp (generate-temporary)] + [maybe-vec maybe-vec] + [(x- ...) xs-] + [(i- ...) (range (stx-length xs-))] + [body- body-]) + #'(let- ([v-tmp maybe-vec]) + (if- v-tmp + (let- ([x- (vector-ref- v-tmp i-)] ...) + body-) + acc)))) + -------- + [⊢ (let- ([tmp val-]) matching-expr-) + ⇒ τ_out]]) + +;; ------------------------------------------------------------------------ + +;; Match-Pattern Ids + +(begin-for-syntax + (define match-pattern-id + (local [(struct match-pattern-id [f] + #:property prop:match-pattern-id + (λ (this) (match-pattern-id-f this)))] + match-pattern-id)) + (define macro/match-pattern-id + (local [(struct macro/match-pattern-id [macro-f match-f] + #:property prop:procedure + (struct-field-index macro-f) + #:property prop:match-pattern-id + (λ (this) (macro/match-pattern-id-match-f this)))] + macro/match-pattern-id))) + +(define-syntax _ + (match-pattern-id + (syntax-parser + [_ (λ/pat-info v τ o #'[() Prop/Top #() #t])]))) + +(define-syntax var + (match-pattern-id + (syntax-parser + [(_ x:id) + (λ/pat-info v τ o #'[([x τ]) Prop/Top (vector-immutable- v) #t])]))) + +;; ------------------------------------------------------------------------ + +;; Predicate Patterns + +(define-syntax ? + (match-pattern-id + (syntax-parser + [(~and + (_ pred:expr) + (~⊢ pred ≫ pred- ⇒ : τ_pred)) + (λ/pat-info v τ o + #:with (~and _ + (~typecheck + [[p? ≫ _ : τ_pred] [x ≫ _ : τ] + ⊢ (app* p? x) ≫ _ (⇒ : τ_tst) (⇒ prop+ p+)])) + #'pred + #:with c? (concrete? #'τ_tst) + #'[() + p+ + (and- (pred- v) #()) + c?])] + [(~and + (_ pred:expr p:pat) + (~⊢ pred ≫ pred- ⇒ : τ_pred)) + (λ/pat-info v τ o + #:with sub:pat-info + ((attribute p.get-pat-info) #'v #'τ #'o) ; τ shauld be replaced by p+ + #:with (~and _ + (~typecheck + [[p? ≫ _ : τ_pred] [x ≫ _ : τ] + ⊢ (p? x) ≫ _ (⇒ : τ_tst) (⇒ prop+ p+)])) + #'pred + #:with c? (and (concrete? #'τ_tst) + (syntax-e #'sub.test-concrete?)) + #'[([sub.x sub.τ] ...) + p+ + (and- (pred- v) + sub.maybe-vec) + c?])]))) + +;; ------------------------------------------------------------------------ + +;; Struct Predicate-Accessor Patterns + +;; It's on the user to supply a predicate that implies that the accessors +;; won't fail, and will produce values of the given field types. +;; The predicate must also return a concrete boolean when given a concrete +;; argument. + +(begin-for-syntax + (struct struct-predicate-accessor-pattern-id + [predicate ; Stx + accessors ; [Listof Stx] + field-types] ; [Listof TypeStx] + #:property prop:match-pattern-id + (λ (this) + (match-define + (struct-predicate-accessor-pattern-id predicate + accessors + field-types) + this) + (define n (length accessors)) + (unless (= n (length field-types)) + (error 'struct-precidate-accessor-pattern-id + "must have the same number of accessors and field types")) + (syntax-parser + [(s:id sub-pat:pat ...) + #:fail-unless (= n (stx-length #'[sub-pat ...])) + (format "expected ~v sub-patterns" n) + (λ/pat-info v τ o + #:do [(define τ-concrete? (concrete? #'τ))] + #:with [sub:pat-info ...] + (for/list ([get-pat-info (in-list (attribute sub-pat.get-pat-info))] + [accessor (in-list accessors)] + [field-type (in-list field-types)]) + (get-pat-info #`(#,accessor v) + (if τ-concrete? + field-type + (type-merge field-type field-type)) + #f)) + #:with c? (and τ-concrete? + (stx-andmap syntax-e #'[sub.test-concrete? ...])) + #`[([sub.x sub.τ] ... ...) + (Prop/And (Prop/ObjType o : (Struct s #,@field-types)) + sub.pos-prop + ...) + (and- (#,predicate v) + (maybe-vector-append- sub.maybe-vec ...)) + c?])]))) + ) + +;; ------------------------------------------------------------------------ + +;; Other Match Forms + +(define-typed-syntax match-let + [(_ ([pat:pat e:expr] ...) body:expr) ≫ + [⊢ [e ≫ e- ⇒ τ_e] ...] + #:with [tmp ...] (generate-temporaries #'[e ...]) + #:with [v-tmp ...] (generate-temporaries #'[pat ...]) + #:with [p:pat-info ...] + (for/list ([get-pat-info (in-list (attribute pat.get-pat-info))] + [v (in-list (stx->list #'[tmp ...]))] + [τ_e (in-list (stx->list #'[τ_e ...]))] + [o_e (in-list (stx-map get-arg-obj #'[e- ...]))]) + (get-pat-info v τ_e o_e)) + #:do [(define flat2-lens (stx-flatten/depth-lens 2))] + #:with [x ...] (lens-view flat2-lens #'[[p.x ...] ...]) + #:with [τ_x ...] (lens-view flat2-lens #'[[p.τ ...] ...]) + [[x ≫ x-- : τ_x] ... + ⊢ (with-occurrence-prop (Prop/And (Prop p.pos-prop) ...) body) ≫ body- + ⇒ τ_body] + #:with [[x- ...] ...] (lens-set flat2-lens #'[[p.x ...] ...] #'[x-- ...]) + #:with [[val_x- ...] ...] + (for/list ([n (in-list (stx-map stx-length #'[[p.x ...] ...]))] + [v-tmp (in-list (stx->list #'[v-tmp ...]))]) + (for/list ([i (in-range n)]) + #`(vector-ref- #,v-tmp '#,i))) + -------- + [⊢ (let- ([tmp e-] ...) + (let- ([v-tmp p.maybe-vec] ...) + (assert- v-tmp "match-let pattern failed") + ... + (let- ([x- val_x-] ... ...) + body-))) + ⇒ τ_body]]) + +;; ------------------------------------------------------------------------ + +;; Helpers + +(define (maybe-vector-append- . vs) + (if- (andmap- vector?- vs) + (apply- vector-append- vs) + #false)) + +;; ------------------------------------------------------------------------ + diff --git a/typed/rosette/match-pat-forms.rkt b/typed/rosette/match-pat-forms.rkt new file mode 100644 index 0000000..607a56e --- /dev/null +++ b/typed/rosette/match-pat-forms.rkt @@ -0,0 +1,157 @@ +#lang turnstile + +(provide quote + and or not + list) + +(require (postfix-in - rosette) + "types.rkt" + (only-in "base-forms.rkt" + [#%app app*] [list list*]) + (only-in "forms-pre-match.rkt" + [quote quote*] + [and and*] [or or*] [not not*]) + "match-core.rkt") + +;; ------------------------------------------------------------------------ + +;; Match Patterns + +;; pat ::= derived-pat +;; | literal-pat +;; | id-pat + +;; derived-pat ::= match-pattern-id +;; | (match-pattern-id . rest) + +;; literal-pat ::= bool +;; | string +;; | number + +;; id-pat ::= id ; not match-pattern-id or `...` + +;; derived pats will include patterns like +;; | _ +;; | (var id) +;; | (quote datum) +;; | (and pat ...) +;; | (or pat ...) ; TODO: branches conflict? +;; | (not pat) +;; | (list lv-pat ...) + +;; ------------------------------------------------------------------------ + +;; Match-Pattern Ids + +(define-syntax quote + (macro/match-pattern-id + (syntax-parser + [(_ datum) #'(quote* datum)]) + (syntax-parser + [(_ datum) + (λ/pat-info v τ o + #:with c? (concrete? #'τ) + #'[() Prop/Top (if- (eq?- v (quote- datum)) #() #f) c?])]))) + +(define-syntax and + (macro/match-pattern-id + (syntax-parser + [(_ e:expr ...) #'(and* e ...)]) + (syntax-parser + [(_ p:pat ...) + (λ/pat-info v τ o + #:with [sub:pat-info ...] + (map-app3 #'v #'τ #'o (attribute p.get-pat-info)) + #:with c? (stx-andmap syntax-e #'[sub.test-concrete? ...]) + #'[([sub.x sub.τ] ... ...) + Prop/Top + (maybe-vector-append- sub.maybe-vec ...) + c?])]))) + +(define-syntax or + (macro/match-pattern-id + (syntax-parser + [(_ e:expr ...) #'(or* e ...)]) + (syntax-parser + [(_ p:pat ...) + (λ/pat-info v τ o + #:with [sub:pat-info ...] + (map-app3 #'v #'τ #'o (attribute p.get-pat-info)) + #:with c? (stx-andmap syntax-e #'[sub.test-concrete? ...]) + #'[() + Prop/Top + (if- (or- sub.maybe-vec ...) #() #f) + c?])]))) + +(define-syntax not + (macro/match-pattern-id + (syntax-parser + [:id #'not*] + [(_ e:expr) #'(not* e)]) + (syntax-parser + [(_ p:pat) + (λ/pat-info v τ o + #:with sub:pat-info ((attribute p.get-pat-info) #'v #'τ #'o) + #:with c? #'sub.test-concrete? + #'[() Prop/Top (if- (not- sub.maybe-vec) #() #f) c?])]))) + +;; ------------------------------------------------------------------------ + +;; Helpers + +(define (maybe-vector-append- . vs) + (if- (andmap- vector?- vs) + (apply- vector-append- vs) + #false)) + +;; ------------------------------------------------------------------------ + +;; List Patterns + +;; list-pat ::= (list lv-pat ...) +;; | (list* lv-pat ... pat) + +;; lv-pat ::= eh-pat ooo +;; | pat + +;; eh-pat ::= pat ; TODO: EH-or patterns? + +;; ooo ::= ... + +;; TODO: implement lv-pats and ellipses + +(define-syntax list + (macro/match-pattern-id + (syntax-parser + [(_ e:expr ...) #'(list* e ...)]) + (syntax-parser + [(_ p:pat ...) + (define n (stx-length #'[p ...])) + (λ/pat-info v τ o + (syntax-parse #'τ + [(~CList τ_elem ...) + #:when (stx-length=? #'[τ_elem ...] #'[p ...]) + #:with [sub:pat-info ...] + (for/list ([get-pat-info (attribute p.get-pat-info)] + [τ_elem (in-list (stx->list #'[τ_elem ...]))] + [i (in-range n)]) + (get-pat-info #`(list-ref v #,i) τ_elem #f)) + #:with c? (stx-andmap syntax-e #'[sub.test-concrete? ...]) + #'[([sub.x sub.τ] ... ...) + Prop/Top + (maybe-vector-append- sub.maybe-vec ...) + c?]] + [_ + #:with [sub:pat-info ...] + (for/list ([get-pat-info (in-list (attribute p.get-pat-info))] + [i (in-range n)]) + (get-pat-info #`(list-ref v #,i) #'Any #f)) + #`[([sub.x sub.τ] ... ...) + Prop/Top + (and- (list?- v) + (=- #,n (length- v)) + (maybe-vector-append- sub.maybe-vec ...)) + #f]]))]))) + +;; ------------------------------------------------------------------------ + diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index b53db69..37f8ac7 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -1,6 +1,6 @@ #lang turnstile -(provide CAny Any +(provide CAnyDeep CAny Any CNothing Nothing Term CU U @@ -9,7 +9,8 @@ ~Term* ~CU* ~U* CU*? U*? ~Constant* Constant*? remove-Constant - concrete?) + concrete? + concrete/shallow-recur?) ;; Struct types Struct (for-syntax typed-struct-id @@ -42,11 +43,13 @@ (for-syntax ~CListof ~CList ~CPair) ;; Other container types CHashTable + (rename-out [CHashTable CHashof]) CSequenceof CBoxof CMBoxof CIBoxof MBoxof IBoxof CVectorof CMVectorof CIVectorof CVector Vectorof MVectorof IVectorof (for-syntax ~CHashTable + (rename-out [~CHashTable ~CHashof]) ~CSequenceof ~CMBoxof ~CIBoxof ~CMVectorof ~CIVectorof) @@ -58,6 +61,7 @@ (for-syntax ~CStructTypeProp) ;; Other base types CUnit Unit + (rename-out [CUnit CVoid] [Unit Void]) CZero Zero CPosInt PosInt CNegInt NegInt @@ -72,9 +76,12 @@ CAsserts COutputPort CSolution CSolver CPict CRegexp CSymbol - LiftedPred LiftedPred2 LiftedNumPred LiftedIntPred UnliftedPred + LiftedPred LiftedPred2 + LiftedPredDeep LiftedPredDeep2 + LiftedNumPred LiftedIntPred UnliftedPred LiftedPredFor UnliftedPredFor (for-syntax ~CUnit CUnit? + (rename-out [~CUnit ~CVoid] [CUnit? CVoid?]) ~CString CString? ~CTrue ~CFalse) ;; The relationship between types and @@ -203,7 +210,7 @@ ;; --------------------------------- (define-base-types - CAny Any CBV CStx CSymbol CRegexp + CAnyDeep CAny Any CBV CStx CSymbol CRegexp CSolution CSolver CPict COutputPort) @@ -250,7 +257,7 @@ (begin-for-syntax (struct typed-struct-info - [transformer untyped-id predicate accessors field-types some-mutable?] + [transformer untyped-id predicate accessors field-types super-id no-super? some-mutable?] #:property prop:procedure (struct-field-index transformer) #:property prop:struct-info (λ (self) @@ -258,7 +265,7 @@ (syntax-local-value (typed-struct-info-untyped-id self))))) (define-syntax-class typed-struct-id - #:attributes [[accessor 1] [τ_fld 1] [τ_fld_merged 1] some-mutable?] + #:attributes [[accessor 1] [τ_fld 1] [τ_fld_merged 1] super-id no-super? some-mutable?] [pattern (~var struct-id (local-value typed-struct-info?)) #:with [accessor ...] (typed-struct-info-accessors (attribute struct-id.local-value)) @@ -266,6 +273,10 @@ (typed-struct-info-field-types (attribute struct-id.local-value)) #:with [τ_fld_merged ...] (stx-map type-merge #'[τ_fld ...] #'[τ_fld ...]) + #:attr no-super? + (typed-struct-info-no-super? (attribute struct-id.local-value)) + #:attr super-id + (typed-struct-info-super-id (attribute struct-id.local-value)) #:attr some-mutable? (typed-struct-info-some-mutable? (attribute struct-id.local-value))])) @@ -362,8 +373,12 @@ (define-syntax ~C→ (pattern-expander (syntax-parser - [(_ pat_in:expr* ... (~and pat_out:expr* (~not (~literal ...)))) - #'(~C→* [pat_in ...] [] pat_out)]))) + [(_ pat_in:expr* ... + (~and pat_out:expr* (~not (~literal ...))) + props:result-prop-pat) + #'(~C→* [pat_in ...] [] + pat_out + : #:+ props.pat_posprop #:- props.pat_negprop)]))) (define (convert-opt-kws opt-kws) (syntax-parse opt-kws @@ -500,6 +515,16 @@ (typecheck? b typeCTrue)] [else #false])) + + ;; concrete/shallow-recur? : Type -> Bool + (define (concrete/shallow-recur? t) + (and (concrete? t) + (syntax-parse t + [(~Struct _ _ ...) #t] + [(~CHashTable _ _) #t] + [(~Any _ . tys) + (stx-andmap concrete/shallow-recur? #'tys)] + [_ #t]))) ) ;; --------------------------------- @@ -602,8 +627,12 @@ (define-named-type-alias LiftedPred (Ccase-> (C→ CAny CBool) (C→ Any Bool))) +(define-named-type-alias LiftedPredDeep (Ccase-> (C→ CAnyDeep CBool) + (C→ Any Bool))) (define-named-type-alias LiftedPred2 (Ccase-> (C→ CAny CAny CBool) (C→ Any Any Bool))) +(define-named-type-alias LiftedPredDeep2 (Ccase-> (C→ CAnyDeep CAnyDeep CBool) + (C→ Any Any Bool))) (define-named-type-alias LiftedNumPred (Ccase-> (C→ CNum CBool) (C→ Num Bool))) (define-named-type-alias LiftedIntPred (Ccase-> (C→ CInt CBool) @@ -898,7 +927,8 @@ ;; type-restrict : Type Type -> Type (define (type-restrict orig new) - (cond [(typecheck? new orig) new] + (cond [(types-no-overlap? orig new) typeCNothing] + [(typecheck? new orig) new] [(Un? new) ((current-type-eval) (syntax-parse new @@ -947,18 +977,13 @@ [else ((current-type-eval) #`(Term #,o*))])])] [else (syntax-parse (list orig new) - [[~CZero ~CPosInt] typeCNothing] - [[~CZero ~CNegInt] typeCNothing] - [[~CZero ~CString] typeCNothing] - [[~CPosInt ~CZero] typeCNothing] - [[~CPosInt ~CNegInt] typeCNothing] - [[~CPosInt ~CString] typeCNothing] - [[~CNegInt ~CPosInt] typeCNothing] - [[~CNegInt ~CZero] typeCNothing] - [[~CNegInt ~CString] typeCNothing] - [[~CString ~CPosInt] typeCNothing] - [[~CString ~CZero] typeCNothing] - [[~CString ~CNegInt] typeCNothing] + #:literals [quote-syntax-] + [[(~Struct (quote-syntax- sa:typed-struct-id) τa ...) + (~Struct (quote-syntax- sb:typed-struct-id) τb ...)] + #:when (and (free-identifier=? #'sa #'sb) + (not (attribute sa.some-mutable?))) + #:with [τab ...] (stx-map type-restrict #'[τa ...] #'[τb ...]) + ((current-type-eval) #'(Struct sa τab ...))] [_ (printf "refine-type: dontknowwhattodo\n orig: ~a\n new: ~a\n" (type->str orig) @@ -989,6 +1014,62 @@ [else orig])) + ;; types-no-overlap? : Type Type -> Bool + (define (types-no-overlap? a b) + (syntax-parse (list a b) + #:literals [quote-syntax-] + [[~CPosInt + (~or ~CZero ~CNegInt ~CString ~CTrue ~CFalse (~Struct _ _ ...))] + #true] + [[~CZero + (~or ~CPosInt ~CNegInt ~CString ~CTrue ~CFalse (~Struct _ _ ...))] + #true] + [[~CNegInt + (~or ~CPosInt ~CZero ~CString ~CTrue ~CFalse (~Struct _ _ ...))] + #true] + [[~CString + (~or ~CPosInt ~CZero ~CNegInt ~CTrue ~CFalse (~Struct _ _ ...))] + #true] + [[~CTrue + (~or ~CPosInt ~CZero ~CNegInt ~CString ~CFalse (~Struct _ _ ...))] + #true] + [[~CFalse + (~or ~CPosInt ~CZero ~CNegInt ~CString ~CTrue (~Struct _ _ ...))] + #true] + [[(~Struct _ _ ...) + (~or ~CPosInt ~CZero ~CNegInt ~CString ~CTrue ~CFalse)] + #true] + [[(~Struct (quote-syntax- sa:id) _ ...) + (~Struct (quote-syntax- sb:id) _ ...)] + (structs-no-overlap? #'sa #'sb)] + [else #false])) + + ;; structs-no-overlap? : StructId StructId -> Bool + (define (structs-no-overlap? a b) + (syntax-parse (list a b) + [[sa:typed-struct-id sb:typed-struct-id] + (cond + [(free-identifier=? #'sa #'sb) #false] + [(and (attribute sa.no-super?) + (attribute sb.no-super?)) + #true] + [(attribute sa.no-super?) + (structs-no-overlap? #'sa #'sb.super-id)] + [(attribute sb.no-super?) + (structs-no-overlap? #'sa.super-id #'sb)] + [else + (structs-no-overlap? #'sa.super-id #'sb.super-id)])])) + + ;; sub-struct? : StructId StructId -> Bool + (define (sub-struct? a b) + (syntax-parse (list a b) + [[sa:typed-struct-id sb:typed-struct-id] + (cond + [(free-identifier=? #'sa #'sb) #true] + [(attribute sa.no-super?) #false] + [else + (sub-struct? #'sa.super-id #'sb)])])) + ;; occurrence-env-id-table-or : ;; (Maybe (FreeIdTableof Type)) (Maybe (FreeIdTableof Type)) -> (Maybe (FreeIdTableof Type)) ;; Combines two possible occurrence-typing type environments with or. @@ -1032,7 +1113,7 @@ #:with DEAD (syntax/loc #'body (ro:assert #false "this should be dead code")) -------- - [⊢ DEAD ⇒ CNothing]] + [⊢ DEAD (⇒ : CNothing) (⇒ prop+ Prop/Bot) (⇒ prop- Prop/Bot)]] [(_ ([x:id τ:expr] ...) body:expr) ⇐ τ_body ≫ #:do [(define scope (make-syntax-delta-introducer (datum->syntax #'body '||) #f))] @@ -1044,9 +1125,15 @@ #:do [(define scope (make-syntax-delta-introducer (datum->syntax #'body '||) #f))] #:with [x* ...] (scope #'[x ...]) - [[x* ≫ x- : τ] ... ⊢ body ≫ body- ⇒ τ_body] + [[x* ≫ x- : τ] ... ⊢ body ≫ body- + (⇒ : τ_body) + (⇒ prop+ p+) + (⇒ prop- p-)] -------- - [⊢ (let- ([x- x] ...) body-) ⇒ τ_body]]) + [⊢ (let- ([x- x] ...) body-) + (⇒ : τ_body) + (⇒ prop+ (Prop p+)) + (⇒ prop- (Prop p-))]]) ;; (with-occurrence-prop prop expr) (define-syntax-parser with-occurrence-prop @@ -1058,7 +1145,7 @@ ;; --------------------------------------------------------- ;; Subtyping - +(require ocelot/the-box) (begin-for-syntax (define (sub? t1 t2) ; need this because recursive calls made with unexpanded types @@ -1068,7 +1155,8 @@ ;; (printf "t2 = ~a\n" (syntax->datum t2)) (or (Any? t2) - (and (concrete/recur? t1) (CAny? t2)) + (and (concrete/shallow-recur? t1) (CAny? t2)) + (and (concrete/recur? t1) (CAnyDeep? t2)) ((current-type=?) t1 t2) (syntax-parse (list t1 t2) #:literals [quote-syntax-] @@ -1101,9 +1189,11 @@ ;; structs, if they are immutable, they are covariant [((~Struct (quote-syntax- sa:typed-struct-id) τa ...) (~Struct (quote-syntax- sb:typed-struct-id) τb ...)) - #:when (free-identifier=? #'sa #'sb) - #:when (not (attribute sa.some-mutable?)) - (typechecks? #'[τa ...] #'[τb ...])] + #:when (sub-struct? #'sa #'sb) + #:when (and (not (attribute sa.some-mutable?)) + (not (attribute sb.some-mutable?))) + (define n (stx-length #'[τb ...])) + (typechecks? (take (stx->list #'[τa ...]) n) #'[τb ...])] ; 2 U types, subtype = subset [((~CU* . ts1) _) (for/and ([t (stx->list #'ts1)]) @@ -1130,13 +1220,48 @@ [((~Ccase-> . ts1) _) (for/or ([t (stx->list #'ts1)]) (typecheck? t t2))] - [((~C→ s1 ... s2) (~C→ t1 ... t2)) + [((~C→ s1 ... s2 : #:+ sp+ #:- sp-) + (~C→ t1 ... t2 : #:+ tp+ #:- tp-)) + (and (typechecks? #'(t1 ...) #'(s1 ...)) + (typecheck? #'s2 #'t2) + (prop-implies? #'sp+ #'tp+) + (prop-implies? #'sp- #'tp-))] + [((~C→* [s1 ...] [] #:rest srst s2 : #:+ sp+ #:- sp-) + (~C→* [t1 ...] [] t2 : #:+ tp+ #:- tp-)) + (define sn (stx-length #'[s1 ...])) + (define-values [t1ns t1rs] + (split-at (stx->list #'[t1 ...]) sn)) + (define t1r ((current-type-eval) #`(CList #,@t1rs))) + (and (typechecks? t1ns #'(s1 ...)) + (typecheck? t1r #'srst) + (typecheck? #'s2 #'t2) + (prop-implies? #'sp+ #'tp+) + (prop-implies? #'sp- #'tp-))] + [((~C→* [s1 ...] [] #:rest srst s2 : #:+ sp+ #:- sp-) + (~C→* [t1 ...] [] #:rest trst t2 : #:+ tp+ #:- tp-)) (and (typechecks? #'(t1 ...) #'(s1 ...)) - (typecheck? #'s2 #'t2))] + (typecheck? #'trst #'srst) + (typecheck? #'s2 #'t2) + (prop-implies? #'sp+ #'tp+) + (prop-implies? #'sp- #'tp-))] [_ #f]))) (current-sub? sub?) (current-typecheck-relation sub?) (define (subs? τs1 τs2) (and (stx-length=? τs1 τs2) - (stx-andmap (current-sub?) τs1 τs2)))) + (stx-andmap (current-sub?) τs1 τs2))) + + (define (prop-implies? p1 p2) + (syntax-parse (list p1 p2) + ;; anything implies true + [[_ (~Prop/And)] #true] + ;; false implies anything + [[(~Prop/Or) _] #false] + [[_ _] + (cond [(type=? p1 p2) #true] + [else #;(printf "prop-implies? fails on ~a and ~a\n" + (type->str p1) + (type->str p2)) + #false])])) + ) From d59ede3fd0405913ce6d513a6ba2eb45f086983d Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Tue, 13 Jun 2017 19:49:46 -0400 Subject: [PATCH 15/24] move structs and generics into typed-rosette --- test/rosette-guide-sec5-tests.rkt | 42 ++-- typed/rosette.rkt | 27 ++- typed/rosette/generic-interfaces.rkt | 123 ++++++++++ typed/rosette/struct.rkt | 340 +++++++++++++++++++++++++++ 4 files changed, 512 insertions(+), 20 deletions(-) create mode 100644 typed/rosette/generic-interfaces.rkt create mode 100644 typed/rosette/struct.rkt diff --git a/test/rosette-guide-sec5-tests.rkt b/test/rosette-guide-sec5-tests.rkt index ca0cf38..7a06f24 100644 --- a/test/rosette-guide-sec5-tests.rkt +++ b/test/rosette-guide-sec5-tests.rkt @@ -5,9 +5,10 @@ ; immutable transparent type (struct point ([x : Int] [y : Int]) #:transparent) -(check-type point : (C→ Int Int (CPoint Int Int))) -(check-type point-x : (C→ (CPoint Int Int) Int)) -(check-type point-y : (C→ (CPoint Int Int) Int)) +(check-type point : (C→ Int Int CPoint)) +(check-type point : (C→ Int Int (Struct point Int Int))) +(check-type point-x : (C→ CPoint Int)) +(check-type point-y : (C→ CPoint Int)) (check-type point? : (C→ Any Bool)) ; opaque immutable type @@ -15,10 +16,12 @@ ; mutable transparent type (struct pnt ([x : Int] [y : Int]) #:mutable #:transparent) -(check-type (point 1 2) : (CPoint Int Int) -> (point 1 2)) +(check-type (point 1 2) : CPoint -> (point 1 2)) +(check-type (point 1 2) : (Struct point Int Int) -> (point 1 2)) + (typecheck-fail (point #f 2) #:with-msg "expected.*Int.*given.*False") -(check-type (pt 1 2) : (CPt Int Int)) ; opaque, incomparable -(check-type (pnt 1 2) : (CPnt Int Int) -> (pnt 1 2)) +(check-type (pt 1 2) : CPt) ; opaque, incomparable +(check-type (pnt 1 2) : CPnt -> (pnt 1 2)) (check-type (eq? (point 1 2) (point 1 2)) : Bool -> #t) ; point structures are values (check-type (eq? (pt 1 2) (pt 1 2)) : Bool -> #f) ; pt structures are references @@ -27,16 +30,18 @@ (define-symbolic b boolean?) (define p (if b (point 1 2) (point 3 4))) ; p holds a symbolic structure -(check-type p : (Point Int Int)) -(check-not-type p : (CPoint Int Int)) +(check-type p : Point) +(check-not-type p : CPoint) (check-type (point-x p) : Int -> (if b 1 3)) ;(ite b 1 3) (check-type (point-y p) : Int -> (if b 2 4)) ;(ite b 2 4) (define sol (solve (assert (= (point-x p) 3)))) -(check-type (evaluate p sol) : (Point Int Int) -> (point 3 4)) ;#(struct:point 3 4) +(check-type (evaluate p sol) : Point -> (point 3 4)) ;#(struct:point 3 4) (check-type (= (point-x (evaluate p sol)) 3) : Bool -> #t) ;; Generics -(define-generics viewable (view viewable -> Nat)) +(define-generics viewable + [(view [viewable : Viewable]) -> Nat]) + (typecheck-fail (struct square (side) #:methods gen:viewable @@ -44,16 +49,17 @@ #:with-msg "Missing type annotations for fields") (struct square ([side : Nat]) #:methods gen:viewable - [(define (view [self : (Square Nat)]) -> Nat (square-side self))]) + [(define (view self) (square-side self))]) (struct circle ([radius : Nat]) #:transparent #:methods gen:viewable - [(define (view [self : (Circle Nat)]) -> Nat (circle-radius self))]) + [(define (view self) (circle-radius self))]) + ;(define-symbolic b boolean?) (define p2 (if b (square 2) (circle 3))) ; p holds a symbolic structure -(check-type p2 : (U (CSquare Nat) (CCircle Nat))) -(check-type p2 : (U (Square Nat) (Circle Nat))) -(check-type (apply-view p2) : Nat -> (if b 2 3)) ;(ite b 2 3) -(define sol2 (solve (assert (= (apply-view p2) 3)))) -(check-type (evaluate p2 sol2) : (U (Square Nat) (Circle Nat)) -> (circle 3)) -(check-type (= (apply-view (evaluate p2 sol2)) 3) : Bool -> #t) +(check-type p2 : (U CSquare CCircle)) +(check-type p2 : (U Square Circle)) +(check-type (view p2) : Nat -> (if b 2 3)) ;(ite b 2 3) +(define sol2 (solve (assert (= (view p2) 3)))) +(check-type (evaluate p2 sol2) : (U Square Circle) -> (circle 3)) +(check-type (= (view (evaluate p2 sol2)) 3) : Bool -> #t) diff --git a/typed/rosette.rkt b/typed/rosette.rkt index 2fc5b26..f92c97d 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -14,7 +14,9 @@ (rename-in (except-in "rosette/base-forms.rkt" list) [#%app app]) "rosette/match-core.rkt" "rosette/match-pat-forms.rkt" + "rosette/struct.rkt" "rosette/struct-type-properties.rkt" + "rosette/generic-interfaces.rkt" ;; base lang (prefix-in ro: (combine-in rosette rosette/lib/synthax)) (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) @@ -26,12 +28,17 @@ [λ lambda]) match match-let _ var ? (all-from-out "rosette/match-pat-forms.rkt") + struct prop:procedure struct-field-index + define-generics + gen:custom-write + gen:equal+hash (for-syntax get-pred expand/ro) CAnyDeep CAny Any CNothing Nothing Term CU U (for-syntax ~CU* ~U*) Constant + Struct C→ C→* → (for-syntax ~C→ ~C→* C→? concrete-function-type?) Ccase-> (for-syntax ~Ccase-> Ccase->?) ; TODO: sym case-> not supported CListof Listof CList CPair Pair @@ -59,6 +66,7 @@ CSolution CSolver CPict CRegexp LiftedPred LiftedPred2 LiftedNumPred LiftedIntPred UnliftedPred) + ;; a legacy auto-providing version of define-typed-syntax ;; TODO: convert everything to new define-typed-syntax (define-syntax (define-typed-syntax stx) @@ -72,6 +80,21 @@ [(_ (name:id . pat) . rst) #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) +;; --------------------------------- + +;; Environments and Variables + +(begin-for-syntax + ;; var-assign/orig-binding : + ;; Id (Listof Sym) (StxListof TypeStx) -> Stx + (define (var-assign/orig-binding x seps τs) + (attachs (attach x 'orig-binding x) + seps + τs + #:ev (current-type-eval))) + + (current-var-assign var-assign/orig-binding)) + ;; --------------------------------- ;; define-symbolic @@ -159,7 +182,7 @@ ;; TODO: get subtyping to work for struct-generated types? ;; TODO: handle mutable structs properly -(define-typed-syntax struct #:datum-literals (:) +#;(define-typed-syntax struct #:datum-literals (:) [(_ name:id (x:id ...) ~! . rst) ≫ #:fail-when #t "Missing type annotations for fields" -------- @@ -192,7 +215,7 @@ (assign-type #'name-x* #'(C→ TyOut ty)))) ...)]]) ;; TODO: add type rules for generics -(define-typed-syntax define-generics #:datum-literals (: ->) +#;(define-typed-syntax define-generics #:datum-literals (: ->) [(_ name:id (f:id x:id ... -> ty-out)) ≫ #:with app-f (format-id #'f "apply-~a" #'f) -------- diff --git a/typed/rosette/generic-interfaces.rkt b/typed/rosette/generic-interfaces.rkt new file mode 100644 index 0000000..12381c6 --- /dev/null +++ b/typed/rosette/generic-interfaces.rkt @@ -0,0 +1,123 @@ +#lang turnstile + +(provide gen:custom-write gen:equal+hash define-generics) + +(require "types.rkt" + "struct.rkt" + (prefix-in ro: (only-in rosette define-generics))) +(module+ test + (require turnstile/rackunit-typechecking + "base-forms.rkt" + (only-in "forms-pre-match.rkt" quote) + (prefix-in ro: (only-in rosette #%app fprintf))) + (define-typed-syntax fprintf + [(_ out:expr fmt:str v:expr ...) ≫ + [⊢ out ≫ out- ⇐ COutputPort] + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:#%app ro:fprintf out- fmt v- ...) ⇒ CVoid]])) + +(define-syntax gen:custom-write + (generic-interface-type-info + #'gen:custom-write- + (λ (τ) + (list + (list 'write-proc + #`(C→ #,τ COutputPort (CU CBool CNat) CVoid)))))) + +(define-syntax gen:equal+hash + (generic-interface-type-info + #'gen:equal+hash- + (λ (τ) + (list + (list 'equal-proc + #`(C→ #,τ #,τ (C→ Any Any CBool) CBool)) + (list 'hash-proc + #`(C→ #,τ (C→ Any CInt) CInt)) + (list 'hash2-proc + #`(C→ #,τ (C→ Any CInt) CInt)))))) + +;; ---------------------------------------------------------------------------- + +(begin-for-syntax + (define-syntax-class -> + [pattern (~or (~datum →) (~datum ->))]) + + (define (method-args-erase args) + (syntax-parse args + #:datum-literals [:] + [([x:id : τ_in] ...) #'(x ...)] + [([x:id : τ_in] ... . [rst:id : τ_rst]) #'(x ... . rst)])) + + (define (method-args->τ args τ_out) + (syntax-parse args + #:datum-literals [:] + [([x:id : τ_in] ...) #`(C→ τ_in ... #,τ_out)] + [([x:id : τ_in] ... . [rst:id : τ_rst]) + #`(C→* [τ_in ...] [] #:rest τ_rst #,τ_out)]))) + +(define-syntax-parser define-generics + [(_ generic-id:id + (~or (~seq #:type-name Name:id) + (~seq (~fail #:unless (id-lower-case? #'generic-id) + (format "Expected lowercase struct name, given ~a" #'generic-id)) + (~parse Name:id (id-upcase #'generic-id)))) + [(method-id:id . method-args) :-> method-τ_out] + ...) + #:with gen-generic-id (format-id #'generic-id "gen:~a" #'generic-id) + #:with [method-args- ...] + (stx-map method-args-erase #'[method-args ...]) + #:with [method-τ ...] + (stx-map method-args->τ #'[method-args ...] #'[method-τ_out ...]) + #:do [(define intro (make-syntax-introducer))] + #:with [generic-id* gen-generic-id* [method-id* ...] [method-args* ...]] + (intro #'[generic-id gen-generic-id [method-id ...] [method-args- ...]]) + #'(begin- + (ro:define-generics generic-id* + (method-id* . method-args*) + ...) + (define-syntax gen-generic-id + (generic-interface-type-info + #'gen-generic-id* + (λ (τ) + (with-syntax ([Name τ]) + (list + (list 'method-id #'method-τ) + ...))))) + (define-syntax method-id + (make-variable-like-transformer + ; TODO: Define Name as a non-Any type that is a + ; supertype of all structs that implement + ; this, but not of anything else. + (with-syntax ([Name #'Any]) + (⊢ method-id* : method-τ)))) + ...)]) + +;; ---------------------------------------------------------------------------- + +(module+ test + (struct foo ([a : Int]) + #:type-name Foo + #:transparent + #:methods gen:custom-write + [(define (write-proc this out mode) + (fprintf out "~v" (foo-a this)))]) + + (define-generics colorable #:type-name Colorable + [(get-color [colorable : Colorable]) -> String] + [(set-color [colorable : Colorable] [color : String]) -> Colorable]) + + (struct point ([x : Float] [y : Float] [color : String]) + #:type-name Point + #:transparent + #:methods gen:colorable + [(define (get-color self) + (point-color self)) + (define (set-color self color) + (point (point-x self) (point-y self) color))]) + + (check-type (get-color (point '1.2 '2.4 '"blue")) : String -> '"blue") + ;; TODO: return Colorable instead of Any + (check-type (set-color (point '1.2 '2.4 '"blue") '"green") : Any + -> (point '1.2 '2.4 '"green")) + ) diff --git a/typed/rosette/struct.rkt b/typed/rosette/struct.rkt new file mode 100644 index 0000000..766b9c8 --- /dev/null +++ b/typed/rosette/struct.rkt @@ -0,0 +1,340 @@ +#lang turnstile + +(provide struct + (for-syntax generic-interface-type-info)) + +(require racket/splicing + (prefix-in ro: (only-in rosette/safe struct)) + (only-in racket/private/generic-methods + generic-property + generic-method-table) + (only-in turnstile/examples/stlc+union + define-named-type-alias) + typed/rosette/types + typed/rosette/base-forms + typed/rosette/forms-pre-match + typed/rosette/match-core + (for-syntax racket/struct-info + racket/syntax + syntax/parse/class/local-value)) +(module+ test + (require turnstile/rackunit-typechecking)) + +(begin-for-syntax + (define (add-pred stx pred) + (set-stx-prop/preserved stx 'pred pred)) + (define (get-pred stx) + (syntax-property stx 'pred))) + +(define-syntax-parser add-predm + [(_ stx pred) (add-pred #'stx #'pred)]) + +;; ---------------------------------------------------------------------------- + +;; Generic Interfaces + +(begin-for-syntax + (struct generic-interface-type-info [untyped-binding get-methods]) + ;; get-methods : [TypeStx -> (Listof (List Symbol TypeStx))] + (define-syntax-class generic-interface-id + #:attributes [id- get-methods] + [pattern generic-interface + #:declare generic-interface (local-value generic-interface-type-info?) + #:do [(match-define (generic-interface-type-info binding methods) + (attribute generic-interface.local-value))] + #:with id- binding + #:attr get-methods methods])) + +;; ---------------------------------------------------------------------------- + +(begin-for-syntax + (define struct-transformer-binding 'struct-transformer-binding) + (define struct-instance-type 'struct-instance-type) + (define struct-accessors 'struct-accessors) + (define struct-field-types 'struct-field-types) + (define-syntax-class super + [pattern super:typed-struct-id + #:with [accessor ...] #'[super.accessor ...] + #:with [τ_fld ...] #'[super.τ_fld ...] + #:with [τ_fld_merged ...] #'[super.τ_fld_merged ...] + #:attr some-mutable? (attribute super.some-mutable?) + #:with [id-:id τ_inst] + (let ([super (local-expand #'super 'expression '())]) + (list (syntax-property super struct-transformer-binding) + (syntax-property super struct-instance-type)))]) + + ;; ----------------------------------- + ;; Struct Options + + (define-splicing-syntax-class struct-options + #:attributes [get-opts- some-mutable?] + [pattern (~seq mut:struct-opt-mutability + trns:struct-opt-opacity + refl:struct-opt-reflection-name + stpr:struct-opt-property ... + gnrc:struct-opt-generic-methods ...) + #:attr some-mutable? (attribute mut.mutable?) + #:attr get-opts- + (lambda (τ) + (apply stx-append + #'[mut.opt- ... trns.opt- ... refl.opt- ... stpr.opt- ... ...] + (for/list ([get-opts- (in-list (attribute gnrc.get-opts-))]) + (get-opts- τ))))]) + + (define-splicing-syntax-class struct-opt-mutability + [pattern (~seq) + #:attr mutable? #false + #:with [opt- ...] #'[]] + [pattern (~seq #:mutable) + #:attr mutable? #true + #:with [opt- ...] #'[#:mutable]]) + + (define-splicing-syntax-class struct-opt-opacity + [pattern (~seq) + #:with [opt- ...] #'[]] + [pattern (~seq #:transparent) + #:with [opt- ...] #'[#:transparent]]) + + (define-splicing-syntax-class struct-opt-reflection-name + [pattern (~seq) + #:with [opt- ...] #'[]] + [pattern (~seq #:reflection-name + (~and sym-expr:expr + (~⊢ sym-expr ≫ sym-expr- ⇐ CSymbol))) + #:with [opt- ...] #'[#:reflection-name sym-expr-]]) + + (define-splicing-syntax-class struct-opt-property + #:attributes [[opt- 1]] + [pattern (~seq #:property + (~and prop:expr + (~⊢ prop ≫ prop- ⇒ (~CStructTypeProp τ_v))) + val) + #:with [opt- ...] #`[#:property prop- (ann val : τ_v)]]) + + (define-splicing-syntax-class struct-opt-generic-methods + #:attributes [get-opts-] + [pattern (~seq #:methods gnrc:generic-interface-id [method-def:expr ...]) + #:attr get-opts- + (λ (τ) + (define id- + ((make-syntax-delta-introducer #'gnrc #'gnrc.id-) #'gnrc.id- 'flip)) + (define type-decls + (for/list ([method/τ (in-list ((attribute gnrc.get-methods) τ))]) + (define method-id + ;((make-syntax-delta-introducer #'gnrc #'gnrc.id-) + (datum->syntax #'gnrc (first method/τ) #'gnrc));) + (define τ_method (second method/τ)) + #`(: #,method-id : #,τ_method))) + (syntax-parse type-decls + [(type-decl ...) + #`[#:property (generic-property #,id-) + (generic-method-table #,id- #:scope gnrc + type-decl ... + method-def ...)]]))]) + + ;; ----------------------------------- + ) + +(define-syntax-parser struct + #:datum-literals [:] + [(_ name:id (field:id ...+) . _) + (raise-syntax-error #f "Missing type annotations for fields" this-syntax)] + [(_ name:id ([field:id : τ:type] ...) + (~or (~seq #:type-name Name:id) + (~seq (~fail #:unless (id-lower-case? #'name) + (format "Expected lowercase struct name, given ~a" #'name)) + (~parse Name:id (id-upcase #'name)))) + opts:struct-options) + #:with CName (format-id #'Name "C~a" #'Name #:source #'Name) + #:with constructor/type (generate-temporary #'name) + #:with name? (format-id #'name "~a?" #'name #:source #'name) + #:with [name-field ...] + (for/list ([field (in-list (syntax->list #'[field ...]))]) + (format-id #'name "~a-~a" #'name field #:source #'name #:props #'name)) + #:with [name* internal-name name?* name-field* ...] + ((make-syntax-introducer) #'[name name name? name-field ...]) + #:with [opt- ...] ((attribute opts.get-opts-) #'CName) + #:with [τ_merged ...] (stx-map type-merge #'[τ.norm ...] #'[τ.norm ...]) + #:with n (datum->syntax #'here (stx-length #'[field ...])) + #:with some-mutable? (attribute opts.some-mutable?) + #'(begin- + (ro:struct name* [field ...] opt- ...) + (define-struct-name name constructor/type internal-name CName name? + [name-field ...] + [τ.norm ...] + #false + #true + some-mutable?) + (define-named-type-alias CName + (Struct name τ.norm ...)) + (define-named-type-alias Name + (add-predm (U (Struct name τ_merged ...)) name?)) + (define-syntax- constructor/type + (make-variable-like-transformer + (⊢ name* : (C→ τ.norm ... CName)))) + (: name? : (LiftedPredFor Name)) + (define name? + (unsafe-assign-type name?* : (LiftedPredFor Name))) + (: name-field : (Ccase-> (C→ CName τ) + (C→ Name τ_merged))) + ... + (define name-field + (unsafe-assign-type name-field* : (Ccase-> (C→ CName τ) + (C→ Name τ_merged)))) + ...)] + ;; Sub-structs + ;; TODO: Allow defining a new type for the sub-struct that + ;; is a distinct subtype of the parent's type. + [(_ name:id super:super ([field:id : τ:type] ...) + (~or (~seq #:type-name Name:id) + (~seq (~fail #:unless (id-lower-case? #'name) + (format "Expected lowercase struct name, given ~a" #'name)) + (~parse Name:id (id-upcase #'name)))) + opts:struct-options) + #:with CName (format-id #'Name "C~a" #'Name #:source #'Name) + #:with name? (format-id #'name "~a?" #'name #:source #'name) + #:with [name-field ...] + (for/list ([field (in-list (syntax->list #'[field ...]))]) + (format-id #'name "~a-~a" #'name field #:source #'name #:props #'name)) + #:with constructor/type (generate-temporary #'name) + #:with [name* internal-name name?* name-field* ...] + ((make-syntax-introducer) #'[name name name? name-field ...]) + #:with [opt- ...] ((attribute opts.get-opts-) #'CName) + #:with [τ_merged ...] (stx-map type-merge #'[τ.norm ...] #'[τ.norm ...]) + #:with some-mutable? (or (attribute super.some-mutable?) + (attribute opts.some-mutable?)) + #'(begin- + (ro:struct name* super [field ...] opt- ...) + (define-struct-name name constructor/type internal-name CName name? + [super.accessor ... name-field ...] + [super.τ_fld ... τ.norm ...] + super + #false + some-mutable?) + (define-named-type-alias CName + (Struct name super.τ_fld ... τ.norm ...)) + (define-named-type-alias Name + (add-predm (U (Struct name super.τ_fld_merged ... τ_merged ...)) name?)) + (define-syntax- constructor/type + (make-variable-like-transformer + (⊢ name* : (C→ super.τ_fld ... τ.norm ... CName)))) + (: name? : LiftedPred) + (define name? + (unsafe-assign-type name?* : (LiftedPredFor Name))) + (: name-field : (Ccase-> (C→ CName τ) + (C→ Name τ_merged))) + ... + (define name-field + (unsafe-assign-type name-field* : + (Ccase-> (C→ CName τ) + (C→ Name τ_merged)))) + ...)] + ) + +(begin-for-syntax + (struct typed-struct-info/match typed-struct-info [] + #:property prop:match-pattern-id + (λ (self) + (struct-predicate-accessor-pattern-id + (typed-struct-info-predicate self) + (typed-struct-info-accessors self) + (typed-struct-info-field-types self)))) + (define (make-typed-struct-info constructor + untyped-id + type + predicate + accessors + field-types + super-id + no-super? + some-mutable?) + (typed-struct-info/match + (make-variable-like-transformer + (set-stx-prop/preserved + (set-stx-prop/preserved + (set-stx-prop/preserved + (set-stx-prop/preserved + constructor + struct-transformer-binding + untyped-id) + struct-instance-type + type) + struct-accessors + accessors) + struct-field-types + field-types)) + untyped-id + predicate + accessors + field-types + super-id + no-super? + some-mutable?))) + +(define-syntax-parser define-struct-name + [(_ name constructor untyped-transformer CName predicate + [accessor ...] + [field-type ...] + (~and super-id (~or :id #false)) + no-super?:boolean + some-mutable?:boolean) + #'(begin- + (define-syntax- name + (make-typed-struct-info (quote-syntax constructor) + (quote-syntax untyped-transformer) + (quote-syntax CName) + (quote-syntax predicate) + (list (quote-syntax accessor) ...) + (list (quote-syntax field-type) ...) + (and (quote super-id) (quote-syntax super-id)) + (quote no-super?) + (quote some-mutable?))) + )]) + +;; ---------------------------------------------------------------------------- + +(module+ test + (struct a () #:transparent) + (struct b () #:transparent) + (struct c () #:transparent) + (struct d () #:transparent) + (struct e () #:transparent) + (struct abc ([a : A] [b : B] [c : C]) #:transparent) + + (check-type (a) : A -> (a)) + (check-type (b) : B -> (b)) + (check-type (c) : C -> (c)) + (check-type (d) : D -> (d)) + (check-type (e) : E -> (e)) + (check-type (abc (a) (b) (c)) : CAbc -> (abc (a) (b) (c))) + (typecheck-fail (abc (a) '3 (c)) + #:with-msg + #;"expected B, given PosInt\n *expression: '3" + "expected: *A, B, C\n *given: *CA, PosInt, CC\n *expressions: \\(a\\), \\(quote 3\\), \\(c\\)") + + ;; predicates + (check-type (a? (a)) : Bool -> '#true) + (check-type (a? (b)) : Bool -> '#false) + (check-type (a? (abc (a) (b) (c))) : Bool -> '#false) + (check-type (abc? (abc (a) (b) (c))) : Bool -> '#true) + + ;; inheritance + ;; This defines a new type, CAbcde, which is a subtype of CAbc. + (struct abcde abc ([d : D] [e : E]) #:transparent) + + (check-type (abcde (a) (b) (c) (d) (e)) : CAbcde + -> (abcde (a) (b) (c) (d) (e))) + (check-type (abcde (a) (b) (c) (d) (e)) : CAbc + -> (abcde (a) (b) (c) (d) (e))) + (typecheck-fail (abcde (a) (b) (c) '3 (e)) + #:with-msg + #;"expected D, given PosInt\n *expression: 3" + "expected: *A, B, C, D, E\n *given: *CA, CB, CC, PosInt, CE\n *expressions: \\(a\\), \\(b\\), \\(c\\), \\(quote 3\\), \\(e\\)") + + ;; inheritance and predicates + (check-type (abc? (abc (a) (b) (c))) : Bool -> '#true) + (check-type (abcde? (abcde (a) (b) (c) (d) (e))) : Bool -> '#true) + (check-type (abc? (abcde (a) (b) (c) (d) (e))) : Bool -> '#true) + (check-type (a? (abcde (a) (b) (c) (d) (e))) : Bool -> '#false) + (check-type (abcde? (abc (a) (b) (c))) : Bool -> '#false) + ) From eb351263f5ac1610ef8df44115e5e28576419114 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Tue, 13 Jun 2017 20:46:35 -0400 Subject: [PATCH 16/24] move formatting functions into typed-rosette --- sdsl/typed-synthcl/synthcl.rkt | 2 +- typed/rosette.rkt | 19 ++++----- typed/rosette/format.rkt | 62 ++++++++++++++++++++++++++++ typed/rosette/generic-interfaces.rkt | 8 +--- 4 files changed, 71 insertions(+), 20 deletions(-) create mode 100644 typed/rosette/format.rkt diff --git a/sdsl/typed-synthcl/synthcl.rkt b/sdsl/typed-synthcl/synthcl.rkt index c1df3c6..574ee32 100644 --- a/sdsl/typed-synthcl/synthcl.rkt +++ b/sdsl/typed-synthcl/synthcl.rkt @@ -580,6 +580,6 @@ (ro:and (ro:sat? cex) (displayln "counterexample found:") (ro:for ([i '(id ...)] [i- (ro:list id- ...)]) - (printf "~a = ~a\n" i (ro:evaluate i- cex))) + (ro:printf "~a = ~a\n" i (ro:evaluate i- cex))) cex)) (begin (displayln "no counterexample found") (ro:unsat))))) ⇒ void]]) diff --git a/typed/rosette.rkt b/typed/rosette.rkt index f92c97d..de25731 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -17,6 +17,7 @@ "rosette/struct.rkt" "rosette/struct-type-properties.rkt" "rosette/generic-interfaces.rkt" + "rosette/format.rkt" ;; base lang (prefix-in ro: (combine-in rosette rosette/lib/synthax)) (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) @@ -27,12 +28,11 @@ [ro:#%module-begin #%module-begin] [λ lambda]) match match-let _ var ? - (all-from-out "rosette/match-pat-forms.rkt") - struct - prop:procedure struct-field-index - define-generics - gen:custom-write - gen:equal+hash + (all-from-out "rosette/match-pat-forms.rkt" + "rosette/struct.rkt" + "rosette/struct-type-properties.rkt" + "rosette/generic-interfaces.rkt" + "rosette/format.rkt") (for-syntax get-pred expand/ro) CAnyDeep CAny Any CNothing Nothing Term @@ -708,17 +708,12 @@ ;; IO and other built-in ops (provide (typed-out [void : (C→ CUnit)] - [printf : (Ccase-> (C→ CString CUnit) - (C→ CString Any CUnit) - (C→ CString Any Any CUnit))] [display : (C→ Any CUnit)] [displayln : (C→ Any CUnit)] [with-output-to-string : (C→ (C→ Any) CString)] [string-contains? : (C→ CString CString CBool)] [pretty-print : (C→ Any CUnit)] - [error : (Ccase-> (C→ (CU CString CSymbol) CNothing) - (C→ CSymbol CString CNothing))] - + [string-length : (C→ CString CNat)] [string-append : (C→ CString CString CString)] diff --git a/typed/rosette/format.rkt b/typed/rosette/format.rkt new file mode 100644 index 0000000..799a728 --- /dev/null +++ b/typed/rosette/format.rkt @@ -0,0 +1,62 @@ +#lang turnstile + +(provide ~v format fprintf printf error) + +(require typed/rosette/types + (only-in typed/rosette/base-forms define unsafe-assign-type) + (prefix-in ro: rosette)) + +;; ---------------------------------------------------------------------------- + +;; Formatting values as strings + +(begin-for-syntax + ;; format-string-matches? : String [Listof Any] -> Bool + (define (format-string-matches? fmt vals) + (with-handlers ([exn:fail? (λ (e) #false)]) + (apply format fmt vals) + #true)) + ) + +(define ~v (unsafe-assign-type ro:~v : (C→ Any CString))) + +(define-typed-syntax format + [(_ fmt:str v:expr ...) ≫ + #:fail-unless + (format-string-matches? (syntax-e #'fmt) (syntax->datum #'[v ...])) + "wrong number of arguments for format string" + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:format fmt v- ...) ⇒ CString]]) + +(define-typed-syntax fprintf + [(_ out:expr fmt:str v:expr ...) ≫ + [⊢ out ≫ out- ⇐ COutputPort] + #:fail-unless + (format-string-matches? (syntax-e #'fmt) (syntax->datum #'[v ...])) + "wrong number of arguments for format string" + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:fprintf out- fmt v- ...) ⇒ CUnit]]) + +(define-typed-syntax printf + [(_ fmt:str v:expr ...) ≫ + #:fail-unless + (format-string-matches? (syntax-e #'fmt) (syntax->datum #'[v ...])) + "wrong number of arguments for format string" + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:printf fmt v- ...) ⇒ CUnit]]) + +(define-typed-syntax error + [(_ sym:expr fmt:str v:expr ...) ≫ + [⊢ sym ≫ sym- ⇐ CSymbol] + #:fail-unless + (format-string-matches? (syntax-e #'fmt) (syntax->datum #'[v ...])) + "wrong number of arguments for format string" + [⊢ [v ≫ v- ⇐ Any] ...] + -------- + [⊢ (ro:error sym- fmt v- ...) ⇒ CNothing]]) + +;; ---------------------------------------------------------------------------- + diff --git a/typed/rosette/generic-interfaces.rkt b/typed/rosette/generic-interfaces.rkt index 12381c6..620d00a 100644 --- a/typed/rosette/generic-interfaces.rkt +++ b/typed/rosette/generic-interfaces.rkt @@ -9,13 +9,7 @@ (require turnstile/rackunit-typechecking "base-forms.rkt" (only-in "forms-pre-match.rkt" quote) - (prefix-in ro: (only-in rosette #%app fprintf))) - (define-typed-syntax fprintf - [(_ out:expr fmt:str v:expr ...) ≫ - [⊢ out ≫ out- ⇐ COutputPort] - [⊢ [v ≫ v- ⇐ Any] ...] - -------- - [⊢ (ro:#%app ro:fprintf out- fmt v- ...) ⇒ CVoid]])) + (only-in "format.rkt" fprintf))) (define-syntax gen:custom-write (generic-interface-type-info From 11ecc6e72a7bbb005bf00ccdd974bed726603981 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Tue, 20 Jun 2017 17:41:15 -0500 Subject: [PATCH 17/24] move for forms into typed-rosette --- sdsl/typed-synthcl/synthcl.rkt | 2 +- typed/rosette.rkt | 51 ++------- typed/rosette/bool.rkt | 169 ++++++++++++++++++++++++++++++ typed/rosette/for-forms.rkt | 122 +++++++++++++++++++++ typed/rosette/forms-pre-match.rkt | 79 +------------- typed/rosette/match-pat-forms.rkt | 5 +- 6 files changed, 303 insertions(+), 125 deletions(-) create mode 100644 typed/rosette/bool.rkt create mode 100644 typed/rosette/for-forms.rkt diff --git a/sdsl/typed-synthcl/synthcl.rkt b/sdsl/typed-synthcl/synthcl.rkt index 574ee32..cbbf641 100644 --- a/sdsl/typed-synthcl/synthcl.rkt +++ b/sdsl/typed-synthcl/synthcl.rkt @@ -199,7 +199,7 @@ (define len-str (caddr split-ty))] #:do [(define sels (length (stx->list #'selector)))] #:with e-out (if (= sels 1) #'(ro:vector-ref vec- (ro:car 'selector)) - #'(for/list ([idx 'selector]) + #'(ro:for/list ([idx 'selector]) (ro:vector-ref vec- idx))) #:with ty-out ((current-type-eval) (if (= sels 1) (format-id #'here "~a" base-str) diff --git a/typed/rosette.rkt b/typed/rosette.rkt index de25731..f312c72 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -12,11 +12,13 @@ "rosette/types.rkt" ;; import base forms (rename-in (except-in "rosette/base-forms.rkt" list) [#%app app]) + (except-in "rosette/bool.rkt" and or not) "rosette/match-core.rkt" "rosette/match-pat-forms.rkt" "rosette/struct.rkt" "rosette/struct-type-properties.rkt" "rosette/generic-interfaces.rkt" + "rosette/for-forms.rkt" "rosette/format.rkt" ;; base lang (prefix-in ro: (combine-in rosette rosette/lib/synthax)) @@ -28,11 +30,14 @@ [ro:#%module-begin #%module-begin] [λ lambda]) match match-let _ var ? - (all-from-out "rosette/match-pat-forms.rkt" + (all-from-out "rosette/bool.rkt" + "rosette/match-pat-forms.rkt" "rosette/struct.rkt" "rosette/struct-type-properties.rkt" "rosette/generic-interfaces.rkt" + "rosette/for-forms.rkt" "rosette/format.rkt") + when unless (for-syntax get-pred expand/ro) CAnyDeep CAny Any CNothing Nothing Term @@ -227,44 +232,6 @@ #:with es+ (stx-map expand/df #'es) (assign-type #'(ro:#%app f . es+) #'ty-out)])))]]) -;; --------------------------------- -;; if - -;; TODO: this is not precise enough -;; specifically, a symbolic non-bool should produce a concrete val -(define-typed-syntax if - [(_ e_tst e1 e2) ≫ - [⊢ [e_tst ≫ e_tst- - (⇒ : ty_tst) - (⇒ prop+ posprop) - (⇒ prop- negprop)]] - #:when (or (concrete? #'ty_tst) ; either concrete - ; or non-bool symbolic - ; (not a super-type of CFalse) - (and (not (typecheck? ((current-type-eval) #'CFalse) #'ty_tst)) - (not (typecheck? ((current-type-eval) #'(Constant (Term CFalse))) #'ty_tst)))) - [⊢ [(with-occurrence-prop posprop e1) ≫ e1- ⇒ : ty1]] - [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] - #:with τ_out - (cond [(and (concrete? #'ty1) (concrete? #'ty2)) #'(CU ty1 ty2)] - ;; else don't need to merge, but do need U - [else #'(U ty1 ty2)]) - -------- - [⊢ [_ ≫ (ro:if e_tst- - e1- - e2-) - ⇒ : τ_out]]] - [(_ e_tst e1 e2) ≫ - [⊢ [e_tst ≫ e_tst- - (⇒ : _) - (⇒ prop+ posprop) - (⇒ prop- negprop)]] - [⊢ [(with-occurrence-prop posprop e1) ≫ e1- ⇒ : ty1]] - [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] - #:with τ_out (type-merge #'ty1 #'ty2) - -------- - [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : τ_out]]]) - ;; --------------------------------- ;; vector @@ -863,12 +830,6 @@ (C→ CNum CNum CNum) (C→ Num Num Num))] - [xor : (Ccase-> (C→ CAny CAny CAny) - (C→ Any Any Any))] - [false? : (LiftedPredFor False)] - - [true : CTrue] - [false : CFalse] [real->integer : (C→ Num Int)] [string? : (UnliftedPredFor CString)] [number? : (LiftedPredFor Num)] diff --git a/typed/rosette/bool.rkt b/typed/rosette/bool.rkt new file mode 100644 index 0000000..184901c --- /dev/null +++ b/typed/rosette/bool.rkt @@ -0,0 +1,169 @@ +#lang turnstile + +(require typed/rosette/types + (only-in typed/rosette/base-forms begin unsafe-assign-type) + (prefix-in ro: rosette) + (postfix-in - rosette)) + +;; --------------------------------- + +;; if + +(provide if) + +;; TODO: this is not precise enough +;; specifically, a symbolic non-bool should produce a concrete val +(define-typed-syntax if + [(_ e_tst e1 e2) ≫ + [⊢ [e_tst ≫ e_tst- + (⇒ : ty_tst) + (⇒ prop+ posprop) + (⇒ prop- negprop)]] + #:when (or (concrete? #'ty_tst) ; either concrete + ; or non-bool symbolic + ; (not a super-type of CFalse) + (and (not (typecheck? ((current-type-eval) #'CFalse) #'ty_tst)) + (not (typecheck? ((current-type-eval) #'(Constant (Term CFalse))) #'ty_tst)))) + [⊢ [(with-occurrence-prop posprop e1) ≫ e1- ⇒ : ty1]] + [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] + #:with τ_out + (cond [(and (concrete? #'ty1) (concrete? #'ty2)) #'(CU ty1 ty2)] + ;; else don't need to merge, but do need U + [else #'(U ty1 ty2)]) + -------- + [⊢ [_ ≫ (ro:if e_tst- + e1- + e2-) + ⇒ : τ_out]]] + [(_ e_tst e1 e2) ≫ + [⊢ [e_tst ≫ e_tst- + (⇒ : _) + (⇒ prop+ posprop) + (⇒ prop- negprop)]] + [⊢ [(with-occurrence-prop posprop e1) ≫ e1- ⇒ : ty1]] + [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] + #:with τ_out (type-merge #'ty1 #'ty2) + -------- + [⊢ [_ ≫ (ro:if e_tst- e1- e2-) ⇒ : τ_out]]]) + +;; ---------------------------------------------------------------------------- + +;; Other Conditionals + +(provide when unless cond else) + +(define-typed-syntax when + [(_ condition:expr body:expr ...+) ≫ + [⊢ condition ≫ condition- ⇐ Bool] + [⊢ (begin body ...) ≫ body- ⇒ τ] + -------- + [⊢ (ro:when condition- body-) ⇒ (U τ Void)]]) + +(define-typed-syntax unless + [(_ condition:expr body:expr ...+) ≫ + [⊢ condition ≫ condition- ⇐ Bool] + [⊢ (begin body ...) ≫ body- ⇒ τ] + -------- + [⊢ (ro:unless condition- body-) ⇒ (U τ Void)]]) + +(define-syntax-parser cond + #:literals [else] + [(_ [else ~! body:expr]) + #'body] + [(_ [(~and b:expr (~not else)) ~! v:expr] rst ... [else body:expr]) + (quasisyntax/loc this-syntax + (if b + v + #,(syntax/loc this-syntax (cond rst ... [else body]))))]) + +;; ------------------------------------------------------------------------ + +;; and, or, not + +(provide and or not) + +(define-typed-syntax and + [(_) ≫ + -------- + [⊢ (ro:and) + (⇒ : CTrue) + (⇒ prop+ Prop/Top) + (⇒ prop- Prop/Bot)]] + [(_ e:expr) ≫ + [⊢ e ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + -------- + [⊢ e- (⇒ : τ) (⇒ prop+ (Prop p+)) (⇒ prop- (Prop p-))]] + [(_ e:expr ... e_l:expr) ≫ + [⊢ (and e ...) ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + [⊢ (with-occurrence-prop p+ e_l) ≫ e_l- + (⇒ : τ_l) + (⇒ prop+ pl+) + (⇒ prop- pl-)] + #:with τ_out (cond [(and (concrete? #'τ) (concrete? #'τ_l)) + #'(CU CFalse τ_l)] + [(concrete? #'τ) + #'(U CFalse τ_l)] + [else + (type-merge typeCFalse #'τ_l)]) + -------- + [⊢ (ro:and e- e_l-) + (⇒ : τ_out) + (⇒ prop+ (Prop/And (Prop p+) (Prop pl+))) + (⇒ prop- (Prop/Or (Prop p-) (Prop pl-)))]]) + +(define-typed-syntax or + [(_) ≫ + -------- + [⊢ [_ ≫ (ro:or) + (⇒ : CFalse) + (⇒ prop+ Prop/Bot) + (⇒ prop- Prop/Top)]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- (⇐ : CBool) (⇒ prop+ p+) (⇒ prop- p-)] + ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) + (⇒ : CBool) + (⇒ prop+ (Prop/Or p+ ...)) + (⇒ prop- (Prop/And p- ...))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- (⇐ : Bool) (⇒ prop+ p+) (⇒ prop- p-)] + ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) + (⇒ : Bool) + (⇒ prop+ (Prop/Or p+ ...)) + (⇒ prop- (Prop/And p- ...))]]] + [(_ e ...) ≫ + [⊢ [e ≫ e- ⇒ : ty] ...] + -------- + [⊢ [_ ≫ (ro:or e- ...) ⇒ : #,(type-merge* (cons typeCFalse #'[ty ...]))]]]) + +(define-typed-syntax not + [:id ≫ + -------- + [⊢ ro:not ⇒ (LiftedPredFor False)]] + [(_ e) ≫ + [⊢ e ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] + #:when (concrete? #'τ) + -------- + [⊢ [_ ≫ (ro:not e-) (⇒ : CBool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]] + [(_ e) ≫ + [⊢ e ≫ e- (⇒ : _) (⇒ prop+ p+) (⇒ prop- p-)] + -------- + [⊢ [_ ≫ (ro:not e-) (⇒ : Bool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]]) + +;; ---------------------------------------------------------------------------- + +;; Bool Functions + +(provide (typed-out [xor : (Ccase-> (C→ CAny CAny CAny) + (C→ Any Any Any))] + [false? : (LiftedPredFor False)] + + [true : CTrue] + [false : CFalse] + )) + +;; ---------------------------------------------------------------------------- + diff --git a/typed/rosette/for-forms.rkt b/typed/rosette/for-forms.rkt new file mode 100644 index 0000000..5e6dee7 --- /dev/null +++ b/typed/rosette/for-forms.rkt @@ -0,0 +1,122 @@ +#lang turnstile + +(provide for/fold for for/list for/and for/or + for*/list + in-list in-naturals in-range) + +(require typed/rosette/types + (except-in typed/rosette/base-forms #%app) + (prefix-in ro: rosette)) + +;; ---------------------------------------------------------------------------- + +;; For Loops + +(define-typed-syntax for/fold + [(_ ([acc:id e_init]) + ([x:id seq:expr] ...) + body:expr ...+) ⇐ τ_acc ≫ + [⊢ e_init ≫ e_init- ⇐ τ_acc] + [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] + [[acc ≫ acc- : τ_acc] + [x ≫ x- : τ_x] ... + ⊢ (begin body ...) ≫ body- ⇐ τ_acc] + -------- + [⊢ (ro:for/fold ([acc- e_init-]) + ([x- seq-] ...) + body-)]] + [(_ ([acc:id : τ_acc e_init]) + ([x:id seq:expr] ...) + body:expr ...+) ≫ + [⊢ e_init ≫ e_init- ⇐ τ_acc] + [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] + [[acc ≫ acc- : τ_acc] + [x ≫ x- : τ_x] ... + ⊢ (begin body ...) ≫ body- ⇐ τ_acc] + -------- + [⊢ (ro:for/fold ([acc- e_init-]) + ([x- seq-] ...) + body-) + ⇒ τ_acc]]) + +(define-typed-syntax for + [(_ ([x:id seq:expr] ...) body:expr ...+) ≫ + [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] + [[x ≫ x- : τ_x] ... ⊢ (begin body ...) ≫ body- ⇐ Void] + -------- + [⊢ (ro:for ([x- seq-] ...) body-) ⇒ Void]]) + +(define-typed-syntax for/list + [(_ ([x:id seq:expr] ...) body:expr) ≫ + [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] + [[x ≫ x- : τ_x] ... ⊢ body ≫ body- ⇒ τ_body] + -------- + [⊢ (ro:for/list ([x- seq-] ...) body-) + ⇒ (CListof τ_body)]]) + +(define-typed-syntax for*/list + #:datum-literals [:] + [(_ ([x:id : τ_x:type seq:expr] ...) body:expr) ≫ + #:do [(define (triangle lst) + (for/list ([i (in-range (stx-length lst))]) + (take (stx->list lst) i)))] + #:with [[x_prev ...] ...] (triangle #'[x ...]) + #:with [[τ_x_prev ...] ...] (triangle #'[τ_x ...]) + [[x_prev ≫ x_prev- : τ_x_prev] ... + ⊢ seq ≫ seq- ⇐ (CSequenceof τ_x)] + ... + [[x ≫ x- : τ_x] ... ⊢ body ≫ body- ⇒ τ_body] + #:with [[x-_prev ...] ...] (triangle #'[x- ...]) + -------- + [⊢ (ro:for*/list ([x- (let- ([x_prev- x-_prev] ...) seq-)] ...) + body-) + ⇒ (CListof τ_body)]]) + +(define-typed-syntax for/and + [(_ ([x:id seq:expr] ...) body:expr) ≫ + [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] + [[x ≫ x- : τ_x] ... ⊢ body ≫ body- ⇒ τ_body] + #:with τ_out (cond [(concrete? #'τ_body) #'(CU CTrue τ_body)] + [else (type-merge* #'[CTrue τ_body τ_body])]) + -------- + [⊢ (ro:for/and ([x- seq-] ...) body-) + ⇒ τ_out]]) + +(define-typed-syntax for/or + [(_ ([x:id seq:expr] ...) body:expr) ≫ + [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] + [[x ≫ x- : τ_x] ... ⊢ body ≫ body- ⇒ τ_body] + #:with τ_out (cond [(concrete? #'τ_body) #'(CU CFalse τ_body)] + [else (type-merge* #'[CFalse τ_body τ_body])]) + -------- + [⊢ (ro:for/or ([x- seq-] ...) body-) + ⇒ τ_out]]) + +;; ---------------------------------------------------------------------------- + +;; Sequences + +(define-typed-syntax in-list + [(_ e:expr) ≫ + [⊢ e ≫ e- ⇒ : (~CListof τ)] + -------- + [⊢ (ro:in-list e-) ⇒ : (CSequenceof τ)]]) + +(define-typed-syntax in-naturals + [(_) ≫ + -------- + [⊢ (ro:in-naturals) ⇒ : (CSequenceof CNat)]]) + +(define-typed-syntax in-range + [(_ e:expr) ≫ + [⊢ e ≫ e- ⇐ CNat] + -------- + [⊢ (ro:in-range e-) ⇒ (CSequenceof CNat)]] + [(_ a:expr b:expr) ≫ + [⊢ a ≫ a- ⇐ CNat] + [⊢ b ≫ b- ⇐ CNat] + -------- + [⊢ (ro:in-range a- b-) ⇒ (CSequenceof CNat)]]) + +;; ---------------------------------------------------------------------------- + diff --git a/typed/rosette/forms-pre-match.rkt b/typed/rosette/forms-pre-match.rkt index fb49d41..64b80a5 100644 --- a/typed/rosette/forms-pre-match.rkt +++ b/typed/rosette/forms-pre-match.rkt @@ -1,10 +1,10 @@ #lang turnstile -(provide quote - and or not) +(provide quote) (require "types.rkt" (rename-in "base-forms.rkt" [#%app app]) + "bool.rkt" (prefix-in ro: rosette) (prefix-in stlc+union: turnstile/examples/stlc+union) ) @@ -37,78 +37,3 @@ ;; ------------------------------------------------------------------------ -;; and, or, not - -(define-typed-syntax and - [(_) ≫ - -------- - [⊢ (ro:and) - (⇒ : CTrue) - (⇒ prop+ Prop/Top) - (⇒ prop- Prop/Bot)]] - [(_ e:expr) ≫ - [⊢ e ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] - -------- - [⊢ e- (⇒ : τ) (⇒ prop+ (Prop p+)) (⇒ prop- (Prop p-))]] - [(_ e:expr ... e_l:expr) ≫ - [⊢ (and e ...) ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] - [⊢ (with-occurrence-prop p+ e_l) ≫ e_l- - (⇒ : τ_l) - (⇒ prop+ pl+) - (⇒ prop- pl-)] - #:with τ_out (cond [(and (concrete? #'τ) (concrete? #'τ_l)) - #'(CU CFalse τ_l)] - [(concrete? #'τ) - #'(U CFalse τ_l)] - [else - (type-merge typeCFalse #'τ_l)]) - -------- - [⊢ (ro:and e- e_l-) - (⇒ : τ_out) - (⇒ prop+ (Prop/And (Prop p+) (Prop pl+))) - (⇒ prop- (Prop/Or (Prop p-) (Prop pl-)))]]) - -(define-typed-syntax or - [(_) ≫ - -------- - [⊢ [_ ≫ (ro:or) - (⇒ : CFalse) - (⇒ prop+ Prop/Bot) - (⇒ prop- Prop/Top)]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- (⇐ : CBool) (⇒ prop+ p+) (⇒ prop- p-)] - ...] - -------- - [⊢ [_ ≫ (ro:or e- ...) - (⇒ : CBool) - (⇒ prop+ (Prop/Or p+ ...)) - (⇒ prop- (Prop/And p- ...))]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- (⇐ : Bool) (⇒ prop+ p+) (⇒ prop- p-)] - ...] - -------- - [⊢ [_ ≫ (ro:or e- ...) - (⇒ : Bool) - (⇒ prop+ (Prop/Or p+ ...)) - (⇒ prop- (Prop/And p- ...))]]] - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇒ : ty] ...] - -------- - [⊢ [_ ≫ (ro:or e- ...) ⇒ : #,(type-merge* (cons typeCFalse #'[ty ...]))]]]) - -(define-typed-syntax not - [:id ≫ - -------- - [⊢ ro:not ⇒ (LiftedPredFor False)]] - [(_ e) ≫ - [⊢ e ≫ e- (⇒ : τ) (⇒ prop+ p+) (⇒ prop- p-)] - #:when (concrete? #'τ) - -------- - [⊢ [_ ≫ (ro:not e-) (⇒ : CBool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]] - [(_ e) ≫ - [⊢ e ≫ e- (⇒ : _) (⇒ prop+ p+) (⇒ prop- p-)] - -------- - [⊢ [_ ≫ (ro:not e-) (⇒ : Bool) (⇒ prop+ (Prop p-)) (⇒ prop- (Prop p+))]]]) - -;; ------------------------------------------------------------------------ - diff --git a/typed/rosette/match-pat-forms.rkt b/typed/rosette/match-pat-forms.rkt index 607a56e..ae8e379 100644 --- a/typed/rosette/match-pat-forms.rkt +++ b/typed/rosette/match-pat-forms.rkt @@ -8,9 +8,10 @@ "types.rkt" (only-in "base-forms.rkt" [#%app app*] [list list*]) - (only-in "forms-pre-match.rkt" - [quote quote*] + (only-in "bool.rkt" [and and*] [or or*] [not not*]) + (only-in "forms-pre-match.rkt" + [quote quote*]) "match-core.rkt") ;; ------------------------------------------------------------------------ From b3bf5e1f74a64bb90057bfa63769d55548524f63 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 5 Jul 2017 02:43:43 -0400 Subject: [PATCH 18/24] changes needed for ocelot --- info.rkt | 3 + typed/rosette.rkt | 451 +++++------------------------- typed/rosette/base-forms.rkt | 17 +- typed/rosette/bool.rkt | 10 +- typed/rosette/function.rkt | 82 ++++++ typed/rosette/hash.rkt | 64 +++++ typed/rosette/list.rkt | 422 ++++++++++++++++++++++++++++ typed/rosette/match-pat-forms.rkt | 34 ++- typed/rosette/types.rkt | 15 +- typed/rosette/vector.rkt | 98 +++++++ 10 files changed, 795 insertions(+), 401 deletions(-) create mode 100644 typed/rosette/function.rkt create mode 100644 typed/rosette/hash.rkt create mode 100644 typed/rosette/list.rkt create mode 100644 typed/rosette/vector.rkt diff --git a/info.rkt b/info.rkt index a3a6a69..2810b7f 100644 --- a/info.rkt +++ b/info.rkt @@ -8,6 +8,9 @@ "rosette" "turnstile" "rackunit-lib" + "lens-common" + "lens-unstable" + "syntax-classes-lib" )) (define build-deps diff --git a/typed/rosette.rkt b/typed/rosette.rkt index f312c72..162357e 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -13,6 +13,7 @@ ;; import base forms (rename-in (except-in "rosette/base-forms.rkt" list) [#%app app]) (except-in "rosette/bool.rkt" and or not) + (except-in "rosette/list.rkt" pair) "rosette/match-core.rkt" "rosette/match-pat-forms.rkt" "rosette/struct.rkt" @@ -20,6 +21,9 @@ "rosette/generic-interfaces.rkt" "rosette/for-forms.rkt" "rosette/format.rkt" + "rosette/vector.rkt" + "rosette/hash.rkt" + "rosette/function.rkt" ;; base lang (prefix-in ro: (combine-in rosette rosette/lib/synthax)) (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) @@ -28,7 +32,8 @@ let (rename-out [app #%app] [ro:#%module-begin #%module-begin] - [λ lambda]) + [λ lambda] + [ro:begin splicing-begin]) match match-let _ var ? (all-from-out "rosette/bool.rkt" "rosette/match-pat-forms.rkt" @@ -36,8 +41,11 @@ "rosette/struct-type-properties.rkt" "rosette/generic-interfaces.rkt" "rosette/for-forms.rkt" - "rosette/format.rkt") - when unless + "rosette/format.rkt" + "rosette/list.rkt" + "rosette/vector.rkt" + "rosette/hash.rkt" + "rosette/function.rkt") (for-syntax get-pred expand/ro) CAnyDeep CAny Any CNothing Nothing Term @@ -85,21 +93,6 @@ [(_ (name:id . pat) . rst) #'(define-typed-syntax name #:export-as name [(_ . pat) . rst])])) -;; --------------------------------- - -;; Environments and Variables - -(begin-for-syntax - ;; var-assign/orig-binding : - ;; Id (Listof Sym) (StxListof TypeStx) -> Stx - (define (var-assign/orig-binding x seps τs) - (attachs (attach x 'orig-binding x) - seps - τs - #:ev (current-type-eval))) - - (current-var-assign var-assign/orig-binding)) - ;; --------------------------------- ;; define-symbolic @@ -232,74 +225,6 @@ #:with es+ (stx-map expand/df #'es) (assign-type #'(ro:#%app f . es+) #'ty-out)])))]]) -;; --------------------------------- -;; vector - -;; mutable constructor -(define-typed-syntax vector - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇒ : τ] ...] - #:with τ* (type-merge* - (stx-map type-merge #'[τ ...] #'[τ ...])) - -------- - [⊢ [_ ≫ (ro:vector e- ...) ⇒ : (CMVectorof (U τ*))]]]) - -(provide (typed-out [vector? : LiftedPred])) - -;; immutable constructor -(define-typed-syntax vector-immutable - [(_ e ...) ≫ - [⊢ [e ≫ e- ⇒ : τ] ...] - -------- - [⊢ [_ ≫ (ro:vector-immutable e- ...) ⇒ : #,(if (stx-andmap concrete? #'(τ ...)) - #'(CIVectorof (CU τ ...)) - #'(CIVectorof (U τ ...)))]]]) - -;; TODO: add CList case? -;; returne mutable vector -(define-typed-syntax list->vector - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:list->vector ⇒ : (Ccase-> (C→ (CListof Any) (CMVectorof Any)) - (C→ (Listof Any) (MVectorof Any)))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof #,(if (concrete? #'τ) #'(U τ) #'τ))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - #:with [τ* ...] (stx-map (λ (τ) (if (concrete? τ) #`(U #,τ) τ)) #'[τ ...]) - -------- - [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVectorof τ*) ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ ...)]] - -------- - [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof (U τ ...))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVector (U τ ...)) ...)]]]) - -(define-typed-syntax vector-ref - [(_ e n) ≫ - [⊢ [e ≫ e- ⇒ : (~or (~CMVectorof τ) (~CIVectorof τ))]] - [⊢ [n ≫ n- ⇐ : Int]] - -------- - [⊢ [_ ≫ (ro:vector-ref e- n-) ⇒ : τ]]] - [(_ e n) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~and (~or (~CMVectorof τ) (~CIVectorof τ))) ...)]] - [⊢ [n ≫ n- ⇐ : Int]] - -------- - [⊢ [_ ≫ (ro:vector-ref e- n-) ⇒ : (U τ ...)]]]) - -(define-typed-syntax vector-set! - [(_ v:expr i:expr x:expr) ≫ - [⊢ v ≫ v- ⇒ (~CMVectorof τ)] - [⊢ i ≫ i- ⇐ Nat] - [⊢ x ≫ x- ⇐ τ] - -------- - [⊢ (ro:vector-set! v- i- x-) ⇒ CUnit]]) - ;; --------------------------------- ;; hash tables @@ -318,173 +243,7 @@ ;; --------------------------------- ;; lists -(provide (typed-out [null? : (Ccase-> (C→ (CListof Any) CBool) - (C→ (Listof Any) Bool))] - [empty? : (Ccase-> (C→ (CListof Any) CBool) - (C→ (Listof Any) Bool))] - [list? : LiftedPred])) - -(define-typed-syntax cons - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:cons ⇒ : (Ccase-> - (C→ Any Any (CPair Any Any)) - (C→ Any (CListof Any) (CListof Any)) - (C→ Any (Listof Any) (Listof Any)))]]] - [(_ e1 e2) ≫ - [⊢ [e2 ≫ e2- ⇒ : (~CListof τ1)]] - [⊢ [e1 ≫ e1- ⇒ : τ2]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) - ⇒ : #,(if (and (concrete? #'τ1) (concrete? #'τ2)) - #'(CListof (CU τ1 τ2)) - #'(CListof (U τ1 τ2)))]]] - [(_ e1 e2) ≫ - [⊢ [e2 ≫ e2- ⇒ : (~U* (~CListof τ) ...)]] - [⊢ [e1 ≫ e1- ⇒ : τ1]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CListof (U τ1 τ)) ...)]]] - [(_ e1 e2) ≫ - [⊢ [e1 ≫ e1- ⇒ : τ1]] - [⊢ [e2 ≫ e2- ⇒ : (~CList τ ...)]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CList τ1 τ ...)]]] - [(_ e1 e2) ≫ - [⊢ [e1 ≫ e1- ⇒ : τ1]] - [⊢ [e2 ≫ e2- ⇒ : (~U* (~CList τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CList τ1 τ ...) ...)]]] - [(_ e1 e2) ≫ - [⊢ [e1 ≫ e1- ⇒ : τ1]] - [⊢ [e2 ≫ e2- ⇒ : τ2]] - -------- - [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CPair τ1 τ2)]]]) - -;; car and cdr additionally support pairs -(define-typed-syntax car - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:car ⇒ : (Ccase-> (C→ (Pair Any Any) Any) - (C→ (Listof Any) Any))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : τ1]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ1 ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CPair τ _)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CPair τ _) ...)]] - -------- - [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]]) - -(define-typed-syntax cdr - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:cdr ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) - (C→ (Listof Any) (Listof Any)))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CListof τ)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CListof τ) ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CList τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CList τ ...) ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CPair _ τ)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CPair _ τ) ...)]] - -------- - [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U τ ...)]]]) - -(define-typed-syntax first - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:first ⇒ : (C→ (Listof Any) Any)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : (U τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : τ1]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:first e-) ⇒ : (U τ1 ...)]]]) - -(define-typed-syntax rest - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:rest ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) - (C→ (Listof Any) (Listof Any)))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (CListof τ)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (U (CListof τ) ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] - -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (CList τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:rest e-) ⇒ : (U (CList τ ...) ...)]]]) - -(define-typed-syntax second - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:second ⇒ : (C→ (Listof Any) Any)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : τ]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : (U τ ...)]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList τ1 τ2 τ ...)]] - -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : τ2]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ2 τ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:second e-) ⇒ : (U τ2 ...)]]]) ;; n must be Int bc Rosette does not have symbolic Nats (define-typed-syntax take @@ -513,28 +272,6 @@ -------- [⊢ [_ ≫ (ro:take e- n-) ⇒ : (U (CList (U τ ...)) ...)]]]) -(define-typed-syntax length - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:length ⇒ : (Ccase-> (C→ (CListof Any) CNat) - (C→ (Listof Any) Nat))]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇐ : (CListof Any)]] - -------- - [⊢ [_ ≫ (ro:length e-) ⇒ : CNat]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof _) ...)]] - -------- - [⊢ [_ ≫ (ro:length e-) ⇒ : Nat]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~CList _ ...)]] - -------- - [⊢ [_ ≫ (ro:length e-) ⇒ : CNat]]] - [(_ e) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList _ ...) ...)]] - -------- - [⊢ [_ ≫ (ro:length e-) ⇒ : Nat]]]) - (define-typed-syntax reverse [_:id ≫ ;; TODO: use polymorphism -------- @@ -559,122 +296,10 @@ -------- [⊢ [_ ≫ (ro:reverse e-) ⇒ : (U (CList . τs/rev) ...)]]]) -(define-typed-syntax build-list - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:build-list ⇒ : (C→ CNat (C→ CNat Any) (CListof Any))]]] - [(_ n f) ≫ - [⊢ [n ≫ n- ⇐ : CNat]] - [⊢ [f ≫ f- ⇒ : (~C→ ty1 ty2)]] - #:fail-unless (typecheck? #'ty1 ((current-type-eval) #'CNat)) - "expected function that consumes concrete Nat" - -------- - [⊢ [_ ≫ (ro:build-list n- f-) ⇒ : (CListof ty2)]]]) - -(define-typed-syntax make-list - [(_ n v) ≫ - [⊢ n ≫ n- ⇐ : CNat] - [⊢ v ≫ v- ⇒ : τ] - -------- - [⊢ (ro:make-list n- v-) ⇒ : (CListof τ)]]) - -(define-typed-syntax map - #;[_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:map ⇒ : (C→ (C→ Any Any) (CListof Any) (CListof Any))]]] - [(_ f lst) ≫ - [⊢ [f ≫ f- ⇒ : (~C→ ~! ty1 ty2)]] - [⊢ [lst ≫ lst- ⇐ : (CListof ty1)]] - -------- - [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]] - [(_ f lst) ≫ - [⊢ [lst ≫ lst- ⇒ : (~CListof ty1)]] - [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match - #:with (~C→ _ ty2) - (for/first ([ty-fn (stx->list #'(ty-fns ...))] - #:when (syntax-parse ty-fn - [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] - [_ #f])) - (displayln (syntax->datum ty-fn)) - ty-fn) - -------- - [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]] - [(_ f lst) ≫ - [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof ty1))]] - [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match - #:with (~C→ _ ty2) - (for/first ([ty-fn (stx->list #'(ty-fns ...))] - #:when (syntax-parse ty-fn - [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] - [_ #f])) - ty-fn) - -------- - [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]]) - -;; TODO: finish andmap -(define-typed-syntax andmap - #;[_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:andmap ⇒ : (C→ (C→ Any Bool) (CListof Any) Bool)]]] - [(_ f lst) ≫ - [⊢ [f ≫ f- ⇒ : (~C→ ~! ty ty-bool)]] - [⊢ [lst ≫ lst- ⇒ : (~CListof _)]] - -------- - [⊢ [_ ≫ (ro:andmap f- lst-) ⇒ : Bool]]] - #;[(_ f lst) ≫ - [⊢ [lst ≫ lst- ⇒ : (~CListof ty)]] - [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match - #:with (~C→ _ ty2) - (for/first ([ty-fn (stx->list #'(ty-fns ...))] - #:when (syntax-parse ty-fn - [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] - [_ #f])) - (displayln (syntax->datum ty-fn)) - ty-fn) - -------- - [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]] - #;[(_ f lst) ≫ - [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof ty1))]] - [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match - #:with (~C→ _ ty2) - (for/first ([ty-fn (stx->list #'(ty-fns ...))] - #:when (syntax-parse ty-fn - [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] - [_ #f])) - ty-fn) - -------- - [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof ty2)]]]) - -(define-typed-syntax sort - [_:id ≫ ;; TODO: use polymorphism - -------- - [⊢ [_ ≫ ro:sort ⇒ : (Ccase-> (C→ (CListof Any) LiftedPred2 (CListof Any)) - (C→ (Listof Any) LiftedPred2 (Listof Any)))]]] - [(_ e cmp) ≫ - [⊢ [e ≫ e- ⇒ : (~CListof τ)]] - [⊢ [cmp ≫ cmp- ⇐ : (C→ τ τ Bool)]] - -------- - [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof τ)]]] - [(_ e cmp) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] - [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ...) (U τ ...) Bool)]] - -------- - [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CListof τ) ...)]]] - [(_ e cmp) ≫ - [⊢ [e ≫ e- ⇒ : (~CList . τs)]] - [⊢ [cmp ≫ cmp- ⇐ : (C→ (U . τs) (U . τs) Bool)]] - -------- - [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof (U . τs))]]] - [(_ e cmp) ≫ - [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] - [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ... ...) (U τ ... ...) Bool)]] - -------- - [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CList (U τ ...)) ...)]]]) - ;; --------------------------------- ;; IO and other built-in ops -(provide (typed-out [void : (C→ CUnit)] +(provide (typed-out [void : (C→* [] [] #:rest (Listof Any) CUnit)] [display : (C→ Any CUnit)] [displayln : (C→ Any CUnit)] [with-output-to-string : (C→ (C→ Any) CString)] @@ -814,6 +439,19 @@ (C→ Num Num))] [truncate : (Ccase-> (C→ CNum CNum) (C→ Num Num))] + [exact-round : (Ccase-> (C→ CNat CNat) + (C→ Nat Nat) + (C→ CNum CInt) + (C→ Num Int))] + [exact-floor : (Ccase-> (C→ CNat CNat) + (C→ Nat Nat) + (C→ CNum CInt) + (C→ Num Int))] + [exact-ceiling : (Ccase-> (C→ CNat CNat) + (C→ Nat Nat) + (C→ CNum CInt) + (C→ Num Int))] + [sgn : (Ccase-> (C→ CZero CZero) (C→ Zero Zero) (C→ CInt CInt) @@ -829,6 +467,9 @@ (C→ Int Int Int) (C→ CNum CNum CNum) (C→ Num Num Num))] + + [exp : (C→ CNum CNum)] + [log : (C→ CNum CNum)] [real->integer : (C→ Num Int)] [string? : (UnliftedPredFor CString)] @@ -838,6 +479,8 @@ [zero? : LiftedNumPred] [even? : LiftedIntPred] [odd? : LiftedIntPred] + [exact-nonnegative-integer? : (LiftedPredFor Nat)] + [inexact->exact : (Ccase-> (C→ CNum CNum) (C→ Num Num))] [exact->inexact : (Ccase-> (C→ CNum CNum) @@ -1359,4 +1002,38 @@ -------- [_ ≻ (for/all ([x e]) (for*/all ([x_rst e_rst] ...) e_body))]]) +;; ------------------------------------------------------------------------ + +;; Errors + +(provide (typed-out + [exn:fail? (C→ Any Bool)] + [raise-argument-error (C→ CSymbol CString Any CNothing)])) + +(define-typed-syntax raise-arguments-error + [(_ name message (~seq field v) ...) ≫ + [⊢ name ≫ name- ⇐ CSymbol] + [⊢ message ≫ message- ⇐ CString] + [⊢ [field ≫ field- ⇐ CString] ...] + [⊢ [v ≫ v- ⇐ Any] ...] + #:with [[field/v- ...] ...] #'[[field- v-] ...] + -------- + [⊢ (ro:raise-arguments-error name- message- field/v- ... ...) + ⇒ CNothing]]) + +;; ------------------------------------------------------------------------ + +;; Other + +(provide define-syntax-rule + define-syntax) + +(define-typed-syntax begin0 + [(_ e0:expr e:expr ...) ≫ + [⊢ e0 ≫ e0- ⇒ τ] + [⊢ [e ≫ e- ⇐ Void] ...] + -------- + [⊢ (ro:begin0 e0- e- ...) ⇒ τ]]) + +;; ------------------------------------------------------------------------ diff --git a/typed/rosette/base-forms.rkt b/typed/rosette/base-forms.rkt index 32ee07d..0ae9c39 100644 --- a/typed/rosette/base-forms.rkt +++ b/typed/rosette/base-forms.rkt @@ -95,6 +95,21 @@ ;; ---------------------------------------------------------------------------- +;; Environments and Variables + +(begin-for-syntax + ;; var-assign/orig-binding : + ;; Id (Listof Sym) (StxListof TypeStx) -> Stx + (define (var-assign/orig-binding x seps τs) + (attachs (attach x 'orig-binding x) + seps + τs + #:ev (current-type-eval))) + + (current-var-assign var-assign/orig-binding)) + +;; ---------------------------------------------------------------------------- + ;; Declaring Types before Definitions (begin-for-syntax @@ -637,7 +652,7 @@ #:datum-literals [:] [(_ e:expr : τ:expr) ≫ -------- - [⊢ e ⇒ : τ]]) + [⊢ (ro:#%expression e) ⇒ : τ]]) (define-syntax-parser unsafe-define/assign-type #:datum-literals [:] diff --git a/typed/rosette/bool.rkt b/typed/rosette/bool.rkt index 184901c..bed030c 100644 --- a/typed/rosette/bool.rkt +++ b/typed/rosette/bool.rkt @@ -28,6 +28,8 @@ [⊢ [(with-occurrence-prop negprop e2) ≫ e2- ⇒ : ty2]] #:with τ_out (cond [(and (concrete? #'ty1) (concrete? #'ty2)) #'(CU ty1 ty2)] + [(typecheck? #'ty1 typeCNothing) #'ty2] + [(typecheck? #'ty2 typeCNothing) #'ty1] ;; else don't need to merge, but do need U [else #'(U ty1 ty2)]) -------- @@ -54,15 +56,15 @@ (define-typed-syntax when [(_ condition:expr body:expr ...+) ≫ - [⊢ condition ≫ condition- ⇐ Bool] - [⊢ (begin body ...) ≫ body- ⇒ τ] + [⊢ condition ≫ condition- (⇐ : Bool) (⇒ prop+ posprop)] + [⊢ (with-occurrence-prop posprop (begin body ...)) ≫ body- ⇒ τ] -------- [⊢ (ro:when condition- body-) ⇒ (U τ Void)]]) (define-typed-syntax unless [(_ condition:expr body:expr ...+) ≫ - [⊢ condition ≫ condition- ⇐ Bool] - [⊢ (begin body ...) ≫ body- ⇒ τ] + [⊢ condition ≫ condition- (⇐ : Bool) (⇒ prop- negprop)] + [⊢ (with-occurrence-prop negprop (begin body ...)) ≫ body- ⇒ τ] -------- [⊢ (ro:unless condition- body-) ⇒ (U τ Void)]]) diff --git a/typed/rosette/function.rkt b/typed/rosette/function.rkt new file mode 100644 index 0000000..dd87256 --- /dev/null +++ b/typed/rosette/function.rkt @@ -0,0 +1,82 @@ +#lang turnstile + +(provide partial partialr) + +(require typed/rosette/types + (prefix-in ro: rosette)) + +;; ---------------------------------------------------------------------------- + +;; Functions + +;; partial* : [A ... B ... -> C] A ... -> [B ... -> C] +(ro:define ((partial* f . as) . bs) + (ro:apply f (ro:append as bs))) + +;; partialr* : [A ... B ... -> C] B ... -> [A ... -> C] +(ro:define ((partialr* f . bs) . as) + (ro:apply f (ro:append as bs))) + +(define-typed-syntax partial + [(_ f:expr a:expr ...) ≫ + [⊢ f ≫ f- ⇒ : (~C→ τ_ab ... τ_c)] + #:do [(define na (stx-length #'[a ...])) + (define-values [τs_a τs_b] + (split-at (stx->list #'[τ_ab ...]) na))] + #:with [τ_a ...] τs_a + #:with [τ_b ...] τs_b + [⊢ [a ≫ a- ⇐ : τ_a] ...] + -------- + [⊢ (partial* f- a- ...) ⇒ : (C→ τ_b ... τ_c)]] + [(_ f:expr a:expr ...) ≫ + [⊢ f ≫ f- ⇒ : (~Ccase-> τ_f ...)] + [⊢ [a ≫ a- ⇒ : τ_a*] ...] + #:do [(define na (stx-length #'[a ...])) + (define results + (filter + list? + (for/list ([τ_f (in-list (stx->list #'[τ_f ...]))]) + (define/syntax-parse (~C→ τ_ab ... τ_c) τ_f) + (define-values [τs_a τs_b] + (split-at (stx->list #'[τ_ab ...]) na)) + (and (typechecks? #'[τ_a* ...] τs_a) + (list τs_b #'τ_c)))))] + #:fail-when (empty? results) "no cases match" + #:with [([τ_b ...] τ_c) ...] results + -------- + [⊢ (partial* f- a- ...) ⇒ : (Ccase-> (C→ τ_b ... τ_c) + ...)]]) + +(define-typed-syntax partialr + [(_ f:expr b:expr ...) ≫ + [⊢ f ≫ f- ⇒ : (~C→ τ_ab ... τ_c)] + #:do [(define na (- (stx-length #'[τ_ab ...]) (stx-length #'[b ...]))) + (define-values [τs_a τs_b] + (split-at (stx->list #'[τ_ab ...]) na))] + #:with [τ_a ...] τs_a + #:with [τ_b ...] τs_b + [⊢ [b ≫ b- ⇐ : τ_b] ...] + -------- + [⊢ (partialr* f- b- ...) ⇒ : (C→ τ_a ... τ_c)]] + [(_ f:expr b:expr ...) ≫ + [⊢ f ≫ f- ⇒ : (~Ccase-> τ_f ...)] + [⊢ [b ≫ b- ⇒ : τ_b*] ...] + #:do [(define nb (stx-length #'[b ...])) + (define results + (filter + list? + (for/list ([τ_f (in-list (stx->list #'[τ_f ...]))]) + (define/syntax-parse (~C→ τ_ab ... τ_c) τ_f) + (define na (- (stx-length #'[τ_ab ...]) nb)) + (define-values [τs_a τs_b] + (split-at (stx->list #'[τ_ab ...]) na)) + (and (typechecks? #'[τ_b* ...] τs_b) + (list τs_a #'τ_c)))))] + #:fail-when (empty? results) "no cases match" + #:with [([τ_a ...] τ_c) ...] results + -------- + [⊢ (partialr* f- b- ...) ⇒ : (Ccase-> (C→ τ_a ... τ_c) + ...)]]) + +;; ---------------------------------------------------------------------------- + diff --git a/typed/rosette/hash.rkt b/typed/rosette/hash.rkt new file mode 100644 index 0000000..acb98db --- /dev/null +++ b/typed/rosette/hash.rkt @@ -0,0 +1,64 @@ +#lang turnstile + +(provide make-hash hash-ref hash-set! hash-ref! hash-remove! hash-copy) + +(require (except-in typed/rosette/base-forms #%app) + typed/rosette/types + (prefix-in ro: rosette)) + +;; ------------------------------------------------------------------------ + +;; Hash Tables + +(define-typed-syntax make-hash + [(_) ⇐ (~CHashof K V) ≫ --- [⊢ (ro:make-hash)]] + [(_) ≫ --- [⊢ (ro:make-hash) ⇒ (CHashof Any Any)]] + [(_ e:expr ~!) ≫ + [⊢ e ≫ e- ⇒ (~CListof (~CPair τ_key τ_val))] + -------- + [⊢ (ro:make-hash e-) ⇒ (CHashof τ_key τ_val)]]) + +(define-typed-syntax hash-ref + [(_ hsh:expr key:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + -------- + [⊢ (ro:hash-ref hsh- key-) ⇒ : τ_val]] + [(_ hsh:expr key:expr fail:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + [⊢ fail ≫ fail- ⇐ : (C→ τ_val)] + -------- + [⊢ (ro:hash-ref hsh- key- fail-) ⇒ : τ_val]]) + +(define-typed-syntax hash-set! + [(_ hsh:expr key:expr val:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + [⊢ val ≫ val- ⇐ : τ_val] + -------- + [⊢ (ro:hash-set! hsh- key- val-) ⇒ : CVoid]]) + +(define-typed-syntax hash-ref! + [(_ hsh:expr key:expr to-set:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + [⊢ to-set ≫ to-set- ⇐ : (C→ τ_val)] + -------- + [⊢ (ro:hash-ref! hsh- key- to-set-) ⇒ : τ_val]]) + +(define-typed-syntax hash-remove! + [(_ hsh:expr key:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + [⊢ key ≫ key- ⇐ : τ_key] + -------- + [⊢ (ro:hash-remove! hsh- key-) ⇒ : CVoid]]) + +(define-typed-syntax hash-copy + [(_ hsh:expr) ≫ + [⊢ hsh ≫ hsh- ⇒ : (~CHashof τ_key τ_val)] + -------- + [⊢ (ro:hash-copy hsh-) ⇒ : (CHashof τ_key τ_val)]]) + +;; ------------------------------------------------------------------------ + diff --git a/typed/rosette/list.rkt b/typed/rosette/list.rkt new file mode 100644 index 0000000..caf7bed --- /dev/null +++ b/typed/rosette/list.rkt @@ -0,0 +1,422 @@ +#lang turnstile + +(provide cons pair car cdr + length list-ref first rest second make-list build-list + map foldl member? + cartesian-product* append* sort + andmap) + +(require (rename-in typed/rosette/base-forms [#%app tro:#%app]) + typed/rosette/types + typed/rosette/bool + typed/rosette/forms-pre-match + (only-in turnstile/examples/stlc+tup + tup proj) + (prefix-in ro: rosette)) + +;; ---------------------------------------------------------------------------- + +;; Basic list and pair stuff + +(provide (typed-out [null? : (Ccase-> (C→ (CListof Any) CBool) + (C→ (Listof Any) Bool))] + [empty? : (Ccase-> (C→ (CListof Any) CBool) + (C→ (Listof Any) Bool))] + [list? : LiftedPred])) + +(define-typed-syntax cons + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:cons ⇒ : (Ccase-> + (C→ Any Any (CPair Any Any)) + (C→ Any (CListof Any) (CListof Any)) + (C→ Any (Listof Any) (Listof Any)))]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e2 ≫ e2- ⇒ : (~CListof τ1)]] + [⊢ [e1 ≫ e1- ⇒ : τ2]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) + ⇒ : #,(if (and (concrete? #'τ1) (concrete? #'τ2)) + #'(CListof (CU τ1 τ2)) + #'(CListof (U τ1 τ2)))]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e2 ≫ e2- ⇒ : (~U* (~CListof τ) ...)]] + [⊢ [e1 ≫ e1- ⇒ : τ1]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CListof (U τ1 τ)) ...)]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : (~CList τ ...)]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CList τ1 τ ...)]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : (~U* (~CList τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (U (CList τ1 τ ...) ...)]]] + [(_ e1:expr e2:expr) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : τ2]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CPair τ1 τ2)]]]) + +(define-typed-syntax pair + [(_ e1:expr e2:expr) ≫ + [⊢ [e1 ≫ e1- ⇒ : τ1]] + [⊢ [e2 ≫ e2- ⇒ : τ2]] + -------- + [⊢ [_ ≫ (ro:cons e1- e2-) ⇒ : (CPair τ1 τ2)]]]) + +;; car and cdr additionally support pairs +(define-typed-syntax car + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:car ⇒ : (Ccase-> (C→ (Pair Any Any) Any) + (C→ (Listof Any) Any))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ1]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ1 ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CPair τ _)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CPair τ _) ...)]] + -------- + [⊢ [_ ≫ (ro:car e-) ⇒ : (U τ ...)]]]) + +(define-typed-syntax cdr + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:cdr ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) + (C→ (Listof Any) (Listof Any)))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CListof τ)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CListof τ) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (CList τ ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U (CList τ ...) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CPair _ τ)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : τ]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CPair _ τ) ...)]] + -------- + [⊢ [_ ≫ (ro:cdr e-) ⇒ : (U τ ...)]]]) + +;; ------------------------------------------------------------------------ + +;; Lists + +(define-typed-syntax length + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:length ⇒ : (Ccase-> (C→ (CListof Any) CNat) + (C→ (Listof Any) Nat))]]] + [(_ lst:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~CListof _)] + -------- + [⊢ (ro:length lst-) ⇒ CNat]] + [(_ lst:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~U* (~CListof _) ...)] + -------- + [⊢ (ro:length lst-) ⇒ Nat]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CList _ ...)]] + -------- + [⊢ [_ ≫ (ro:length lst-) ⇒ : CNat]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CList _ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:length lst-) ⇒ : Nat]]]) + +(define-typed-syntax list-ref + [(_ lst:expr i:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~CListof τ)] + [⊢ i ≫ i- ⇐ CNat] + -------- + [⊢ (ro:list-ref lst- i-) ⇒ τ]] + [(_ lst:expr i:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~or (~CListof τ) + (~U* (~CListof τ)))] + [⊢ i ≫ i- ⇐ Nat] + -------- + [⊢ (ro:list-ref lst- i-) ⇒ (U τ)]]) + +(define-typed-syntax first + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:first ⇒ : (C→ (Listof Any) Any)]]] + [(_ lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:first lst-) ⇒ : τ]]] + [(_ lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:first lst-) ⇒ : (U τ ...)]]] + [(_ lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:first lst-) ⇒ : τ1]]] + [(_ lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:first lst-) ⇒ : (U τ1 ...)]]]) + +(define-typed-syntax rest + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:rest ⇒ : (Ccase-> (C→ (CListof Any) (CListof Any)) + (C→ (Listof Any) (Listof Any)))]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:rest lst-) ⇒ : (CListof τ)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:rest lst-) ⇒ : (U (CListof τ) ...)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CList τ1 τ ...)]] + -------- + [⊢ [_ ≫ (ro:rest lst-) ⇒ : (CList τ ...)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CList τ1 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:rest lst-) ⇒ : (U (CList τ ...) ...)]]]) + +(define-typed-syntax second + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:second ⇒ : (C→ (Listof Any) Any)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:second lst-) ⇒ : τ]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof τ) ...)]] + -------- + [⊢ [_ ≫ (ro:second lst-) ⇒ : (U τ ...)]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CList τ1 τ2 τ ...)]] + -------- + [⊢ [_ ≫ (ro:second lst-) ⇒ : τ2]]] + [(_ lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CList τ1 τ2 τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:second lst-) ⇒ : (U τ2 ...)]]]) + +(define-typed-syntax build-list + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ ro:build-list ⇒ : (C→ CNat (C→ CNat Any) (CListof Any))]] + [(_ n:expr f:expr) ≫ + [⊢ n ≫ n- ⇐ : CNat] + [⊢ f ≫ f- ⇒ : (~C→ X Y)] + #:fail-unless (typecheck? #'X ((current-type-eval) #'CNat)) + "expected function that consumes concrete Nat" + -------- + [⊢ [_ ≫ (ro:build-list n- f-) ⇒ : (CListof Y)]]]) + +(define-typed-syntax make-list + [(_ n:expr v:expr) ≫ + [⊢ n ≫ n- ⇐ : CNat] + [⊢ v ≫ v- ⇒ : τ] + -------- + [⊢ (ro:make-list n- v-) ⇒ : (CListof τ)]]) + +;; ------------------------------------------------------------------------ + +(define-typed-syntax map + #;[_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:map ⇒ : (C→ (C→ Any Any) (CListof Any) (CListof Any))]]] + [(_ f:expr lst:expr) ⇐ (~CListof Y) ≫ + [⊢ f ≫ f- ⇒ (~C→ X Y*)] + ; Y* must be usable as Y, because the Y* value will be used + ; as an element the return value + [Y* τ⊑ Y #:for f] + [⊢ lst ≫ lst- ⇐ (CListof X)] + -------- + [⊢ (ro:map f- lst-)]] + [(_ f:expr lst:expr) ≫ + [⊢ [f ≫ f- ⇒ : (~C→ ~! X Y)]] + [⊢ [lst ≫ lst- ⇐ : (CListof X)]] + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof Y)]]] + [(_ f:expr lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof X)]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ Y) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ X* _) #:when (typecheck? #'X #'X*) #t] + [_ #f])) + ty-fn) + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof Y)]]] + [(_ f:expr lst:expr) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof X))]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ Y) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ X* _) #:when (typecheck? #'X #'X*) #t] + [_ #f])) + ty-fn) + -------- + [⊢ [_ ≫ (ro:map f- lst-) ⇒ : (CListof Y)]]]) + + + +(define-typed-syntax foldl + [(_ f:expr base:expr lst:expr) ⇐ Y ≫ + [⊢ f ≫ f- ⇒ (~C→ X Y* Z)] + ; Z must be usable as Y*, because the Z value will be + ; used as the Y* argument on the next iteration + [Z τ⊑ Y* #:for f] + ; Z must be usable as Y, because the Z value will be used + ; as the return value + [Z τ⊑ Y #:for f] + ; Y must be usable as Y*, because the base Y value will + ; be used as the Y* argument on the first iteration + [Y τ⊑ Y* #:for f] + ; base must be usable as Y, because the base value will + ; be used as the return value + [⊢ base ≫ base- ⇐ Y] + [⊢ lst ≫ lst- ⇐ (CListof X)] + -------- + [⊢ (ro:foldl f- base- lst-)]] + [(_ f:expr base:expr lst:expr) ⇐ Y ≫ + ; TODO: fix this to take X into account when choosing + ; which case to commit to + [⊢ f ≫ f- ⇒ + (~Ccase-> _ ... + (~and (~C→ X Y* Z) + (~fail #:unless (typecheck? #'Z #'Y*)) + (~fail #:unless (typecheck? #'Z #'Y)) + (~fail #:unless (typecheck? #'Y #'Y*))) + _ ...)] + ; base must be usable as Y, because the base value will + ; be used as the return value + [⊢ base ≫ base- ⇐ Y] + [⊢ lst ≫ lst- ⇐ (CListof X)] + -------- + [⊢ (ro:foldl f- base- lst-)]] + [(_ f:expr base:expr lst:expr) ≫ + ; TODO: fix this to try all options in the Ccase-> + [⊢ f ≫ f- ⇒ (~Ccase-> _ ... (~C→ X Y Z))] + ; Z must be usable as Y, because the Z value will be used + ; as the Y argument on the next iteration + [Z τ⊑ Y #:for f] + [⊢ base ≫ base- ⇐ Y] + [⊢ lst ≫ lst- ⇐ (CListof X)] + -------- + [⊢ (ro:foldl f- base- lst-) ⇒ Y]]) + +(define member + (unsafe-assign-type ro:member : + (C→ Any (Listof Any) Any))) + +(: member? : (C→ Any (Listof Any) Bool)) +(define (member? v lov) + (if (tro:#%app member v lov) '#true '#false)) + +(define-typed-syntax cartesian-product* + [(_ lst:expr) ≫ + [⊢ lst ≫ lst- ⇒ (~CListof (~CListof τ))] + -------- + [⊢ (ro:apply ro:cartesian-product lst-)]]) + +(define-typed-syntax append* + [(_ lol:expr) ≫ + [⊢ lol ≫ lol- ⇒ (~CListof (~CListof τ))] + -------- + [⊢ (ro:append* lol-) ⇒ (CListof τ)]]) + +(define-typed-syntax sort + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:sort ⇒ : (Ccase-> (C→ (CListof Any) LiftedPred2 (CListof Any)) + (C→ (Listof Any) LiftedPred2 (Listof Any)))]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ τ τ Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof τ)]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ...) (U τ ...) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CListof τ) ...)]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~CList . τs)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U . τs) (U . τs) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (CListof (U . τs))]]] + [(_ e cmp) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] + [⊢ [cmp ≫ cmp- ⇐ : (C→ (U τ ... ...) (U τ ... ...) Bool)]] + -------- + [⊢ [_ ≫ (ro:sort e- cmp-) ⇒ : (U (CList (U τ ...)) ...)]]]) + +;; ------------------------------------------------------------------------ + +;; TODO: finish andmap +(define-typed-syntax andmap + #;[_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:andmap ⇒ : (C→ (C→ Any Bool) (CListof Any) Bool)]]] + [(_ f lst) ≫ + [⊢ [f ≫ f- ⇒ : (~C→ ~! ty ty-bool)]] + [⊢ [lst ≫ lst- ⇒ : (~CListof _)]] + -------- + [⊢ [_ ≫ (ro:andmap f- lst-) ⇒ : Bool]]] + #;[(_ f lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~CListof ty)]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ ty2) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] + [_ #f])) + (displayln (syntax->datum ty-fn)) + ty-fn) + -------- + [⊢ [_ ≫ (ro:andmap f- lst-) ⇒ : (CListof ty2)]]] + #;[(_ f lst) ≫ + [⊢ [lst ≫ lst- ⇒ : (~U* (~CListof ty1))]] + [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match + #:with (~C→ _ ty2) + (for/first ([ty-fn (stx->list #'(ty-fns ...))] + #:when (syntax-parse ty-fn + [(~C→ t1 _) #:when (typecheck? #'ty1 #'t1) #t] + [_ #f])) + ty-fn) + -------- + [⊢ [_ ≫ (ro:andmap f- lst-) ⇒ : (CListof ty2)]]]) diff --git a/typed/rosette/match-pat-forms.rkt b/typed/rosette/match-pat-forms.rkt index ae8e379..c442377 100644 --- a/typed/rosette/match-pat-forms.rkt +++ b/typed/rosette/match-pat-forms.rkt @@ -2,7 +2,7 @@ (provide quote and or not - list) + list pair) (require (postfix-in - rosette) "types.rkt" @@ -10,6 +10,8 @@ [#%app app*] [list list*]) (only-in "bool.rkt" [and and*] [or or*] [not not*]) + (only-in "list.rkt" + [pair pair*]) (only-in "forms-pre-match.rkt" [quote quote*]) "match-core.rkt") @@ -136,7 +138,7 @@ (for/list ([get-pat-info (attribute p.get-pat-info)] [τ_elem (in-list (stx->list #'[τ_elem ...]))] [i (in-range n)]) - (get-pat-info #`(list-ref v #,i) τ_elem #f)) + (get-pat-info #`(list-ref- v #,i) τ_elem #f)) #:with c? (stx-andmap syntax-e #'[sub.test-concrete? ...]) #'[([sub.x sub.τ] ... ...) Prop/Top @@ -146,7 +148,7 @@ #:with [sub:pat-info ...] (for/list ([get-pat-info (in-list (attribute p.get-pat-info))] [i (in-range n)]) - (get-pat-info #`(list-ref v #,i) #'Any #f)) + (get-pat-info #`(list-ref- v #,i) #'Any #f)) #`[([sub.x sub.τ] ... ...) Prop/Top (and- (list?- v) @@ -154,5 +156,31 @@ (maybe-vector-append- sub.maybe-vec ...)) #f]]))]))) +(define-syntax pair + (macro/match-pattern-id + (syntax-parser + [(_ e1:expr e2:expr) #'(pair* e1 e2)]) + (syntax-parser + [(_ p1:pat p2:pat) + (λ/pat-info v τ o + (syntax-parse #'τ + [(~CPair τ1 τ2) + #:with s1:pat-info ((attribute p1.get-pat-info) #'(car- v) #'τ1 #f) + #:with s2:pat-info ((attribute p2.get-pat-info) #'(cdr- v) #'τ2 #f) + #:with c? (and (attribute s1.test-concrete?) + (attribute s2.test-concrete?)) + #'[([s1.x s1.τ] ... [s2.x s2.τ] ...) + Prop/Top + (maybe-vector-append- s1.maybe-vec s2.maybe-vec) + c?]] + [_ + #:with s1:pat-info ((attribute p1.get-pat-info) #'(car- v) #'Any #f) + #:with s2:pat-info ((attribute p2.get-pat-info) #'(cdr- v) #'Any #f) + #`[([s1.x s1.τ] ... [s2.x s2.τ] ...) + Prop/Top + (and- (pair?- v) + (maybe-vector-append- s1.maybe-vec s2.maybe-vec)) + #f]]))]))) + ;; ------------------------------------------------------------------------ diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 37f8ac7..631a4e6 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -93,6 +93,7 @@ (for-syntax get-pred type-merge type-merge* + typeCNothing typeCFalse typeCTrue occurrence-env)) @@ -730,6 +731,8 @@ ;; type-merge : Type Type -> Type (define (type-merge a b) (cond [(types-same-singleton? a b) a] + [(typecheck? a typeCNothing) b] + [(typecheck? b typeCNothing) a] [else ;; Here it will result in some kind of term or union, ;; so remove immediate Constant wrappers @@ -985,7 +988,7 @@ #:with [τab ...] (stx-map type-restrict #'[τa ...] #'[τb ...]) ((current-type-eval) #'(Struct sa τab ...))] [_ - (printf "refine-type: dontknowwhattodo\n orig: ~a\n new: ~a\n" + (printf "refine-type:\n orig: ~a\n new: ~a\n" (type->str orig) (type->str new)) new])])) @@ -1011,7 +1014,10 @@ [(~Term* o) (define o* (type-remove #'o new-not)) ((current-type-eval) #`(Term #,o*))])] + [(types-no-overlap? orig new-not) + orig] [else + ;; Probably nothing more we can do in the current system orig])) ;; types-no-overlap? : Type Type -> Bool @@ -1145,7 +1151,7 @@ ;; --------------------------------------------------------- ;; Subtyping -(require ocelot/the-box) + (begin-for-syntax (define (sub? t1 t2) ; need this because recursive calls made with unexpanded types @@ -1259,9 +1265,6 @@ [[(~Prop/Or) _] #false] [[_ _] (cond [(type=? p1 p2) #true] - [else #;(printf "prop-implies? fails on ~a and ~a\n" - (type->str p1) - (type->str p2)) - #false])])) + [else #false])])) ) diff --git a/typed/rosette/vector.rkt b/typed/rosette/vector.rkt new file mode 100644 index 0000000..e1ca3f0 --- /dev/null +++ b/typed/rosette/vector.rkt @@ -0,0 +1,98 @@ +#lang turnstile + +(require typed/rosette/types + (prefix-in ro: rosette)) + +;; ------------------------------------------------------------------------ + +(provide (typed-out [vector? : LiftedPred])) + +(provide vector vector-immutable make-vector vector-ref vector-set!) + +;; mutable constructor +(define-typed-syntax vector + [(_ e:expr ...) ≫ + [⊢ [e ≫ e- ⇒ : τ] ...] + #:with τ* (type-merge* + (stx-map type-merge #'[τ ...] #'[τ ...])) + -------- + [⊢ [_ ≫ (ro:vector e- ...) ⇒ : (CMVectorof (U τ*))]]]) + +;; immutable constructor +(define-typed-syntax vector-immutable + [(_ e:expr ...) ≫ + [⊢ [e ≫ e- ⇒ : τ] ...] + -------- + [⊢ [_ ≫ (ro:vector-immutable e- ...) ⇒ : #,(if (stx-andmap concrete? #'(τ ...)) + #'(CIVectorof (CU τ ...)) + #'(CIVectorof (U τ ...)))]]]) + +(define-typed-syntax make-vector + [(_ size:expr v:expr) ≫ + [⊢ size ≫ size- ⇐ CNat] + [⊢ v ≫ v- ⇒ τ] + -------- + [⊢ (ro:make-vector size- v-) ⇒ (CMVectorof τ)]]) + +(define-typed-syntax vector-ref + [(_ v:expr i:expr) ≫ + [⊢ [v ≫ v- ⇒ : (~or (~CMVectorof τ) (~CIVectorof τ))]] + [⊢ [i ≫ i- ⇐ : CInt]] + -------- + [⊢ [_ ≫ (ro:vector-ref v- i-) ⇒ : τ]]] + [(_ v:expr i:expr) ≫ + [⊢ [v ≫ v- ⇒ : (~or (~CMVectorof τ) (~CIVectorof τ))]] + [⊢ [i ≫ i- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:vector-ref v- i-) ⇒ : #,(type-merge #'τ #'τ)]]] + [(_ v:expr i:expr) ≫ + [⊢ [v ≫ v- ⇒ : (~U* (~and (~or (~CMVectorof τ) (~CIVectorof τ))) ...)]] + [⊢ [i ≫ i- ⇐ : Int]] + -------- + [⊢ [_ ≫ (ro:vector-ref v- i-) ⇒ : #,(type-merge* #'[τ ...])]]]) + +(define-typed-syntax vector-set! + [(_ v:expr i:expr x:expr) ≫ + [⊢ v ≫ v- ⇒ (~CMVectorof τ)] + [⊢ i ≫ i- ⇐ Nat] + [⊢ x ≫ x- ⇐ τ] + -------- + [⊢ (ro:vector-set! v- i- x-) ⇒ CUnit]]) + +;; ------------------------------------------------------------------------ + +(provide vector->list list->vector) + +(define-typed-syntax vector->list + [(_ v:expr) ≫ + [⊢ v ≫ v- ⇒ (~CMVectorof τ)] + -------- + [⊢ (ro:vector->list v-) ⇒ (CListof τ)]]) + +;; TODO: add CList case? +;; returne mutable vector +(define-typed-syntax list->vector + [_:id ≫ ;; TODO: use polymorphism + -------- + [⊢ [_ ≫ ro:list->vector ⇒ : (Ccase-> (C→ (CListof Any) (CMVectorof Any)) + (C→ (Listof Any) (MVectorof Any)))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CListof τ)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof #,(if (concrete? #'τ) #'(U τ) #'τ))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CListof τ) ...)]] + #:with [τ* ...] (stx-map (λ (τ) (if (concrete? τ) #`(U #,τ) τ)) #'[τ ...]) + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVectorof τ*) ...)]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~CList τ ...)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (CMVectorof (U τ ...))]]] + [(_ e) ≫ + [⊢ [e ≫ e- ⇒ : (~U* (~CList τ ...) ...)]] + -------- + [⊢ [_ ≫ (ro:list->vector e-) ⇒ : (U (CMVector (U τ ...)) ...)]]]) + +;; ------------------------------------------------------------------------ + From 6cc9c6c6e965ddfa9e5726130214f7d1f8e0c054 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Wed, 5 Jul 2017 18:48:38 -0400 Subject: [PATCH 19/24] more changes for Ocelot including fixing for/list to allow only concrete booleans for `#:when` and `#:unless` conditions --- test/typed-rosette/for-tests.rkt | 145 +++++++++++++++++++++++++++++++ typed/rosette.rkt | 7 +- typed/rosette/for-forms.rkt | 129 +++++++++++++++++++++------ typed/rosette/list.rkt | 9 +- typed/rosette/types.rkt | 3 +- 5 files changed, 261 insertions(+), 32 deletions(-) create mode 100644 test/typed-rosette/for-tests.rkt diff --git a/test/typed-rosette/for-tests.rkt b/test/typed-rosette/for-tests.rkt new file mode 100644 index 0000000..8b2f52e --- /dev/null +++ b/test/typed-rosette/for-tests.rkt @@ -0,0 +1,145 @@ +#lang typed/rosette + +(require turnstile/rackunit-typechecking) + +;; These tests make sure that #:when conditions can refer to +;; identifiers defined in previous clauses. + +(: string=? : (C→ CString CString CBool)) +(define (string=? a b) + (equal? a b)) + +(check-type (for/list () 1) : (CListof CInt) -> (list 1)) +(check-type (for/list () #t) : (CListof CBool) -> (list #t)) +(check-type (for/list () #f) : (CListof CBool) -> (list #f)) + +(check-type (for/list (#:when #t) 1) : (CListof CInt) -> (list 1)) +(check-type (for/list (#:when #f) 1) : (CListof CInt) -> (list)) +(check-type (for/list ([x (in-range 5)]) x) + : (CListof CInt) + -> (list 0 1 2 3 4)) + +(check-type (for/list ([s (in-list (list "a" "b" "c"))] + [i (in-naturals)]) + (list s i)) + : (CListof (CList CString CInt)) + -> (list (list "a" 0) (list "b" 1) (list "c" 2))) + +(check-type (for/list ([s (in-list (list "a" "b" "c"))] + [i (in-naturals)] + #:when (even? i)) + (list s i)) + : (CListof (CList CString CInt)) + -> (list (list "a" 0) (list "c" 2))) + +(check-type (for/list ([s (in-list (list "a" "b" "c" "d" "e"))] + [i (in-naturals)] + #:when (even? i) + [j (in-range i)]) + (list s i j)) + : (CListof (CList CString CInt CInt)) + -> (list (list "c" 2 0) + (list "c" 2 1) + (list "e" 4 0) + (list "e" 4 1) + (list "e" 4 2) + (list "e" 4 3))) + +;; ------------------------------------------------------------------------ + +;; Test based on section 11 of the racket guide + +(check-type (for/list ([book (in-list (list "Guide" "Reference" "Notes"))] + #:when (not (string=? book "Notes")) + [i (in-naturals 1)] + [chapter (in-list (list "Intro" "Details" "Conclusion" "Index"))] + #:when (not (string=? chapter "Index"))) + (list book i chapter)) + : (CListof (CList CString CInt CString)) + -> (list (list "Guide" 1 "Intro") + (list "Guide" 2 "Details") + (list "Guide" 3 "Conclusion") + (list "Reference" 1 "Intro") + (list "Reference" 2 "Details") + (list "Reference" 3 "Conclusion"))) + +(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))] + #:break (string=? book "Story") + [chapter (in-list (list "Intro" "Details" "Conclusion"))]) + (list book chapter)) + : (CListof (CList CString CString)) + -> (list (list "Guide" "Intro") + (list "Guide" "Details") + (list "Guide" "Conclusion"))) + +(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))] + #:when #true + [chapter (in-list (list "Intro" "Details" "Conclusion"))] + #:break (and (string=? book "Story") + (string=? chapter "Conclusion"))) + (list book chapter)) + : (CListof (CList CString CString)) + -> (list (list "Guide" "Intro") + (list "Guide" "Details") + (list "Guide" "Conclusion") + (list "Story" "Intro") + (list "Story" "Details"))) + +(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))] + #:when #true + [chapter (in-list (list "Intro" "Details" "Conclusion"))] + #:final (and (string=? book "Story") + (string=? chapter "Conclusion"))) + (list book chapter)) + : (CListof (CList CString CString)) + -> (list (list "Guide" "Intro") + (list "Guide" "Details") + (list "Guide" "Conclusion") + (list "Story" "Intro") + (list "Story" "Details") + (list "Story" "Conclusion"))) + +(check-type (for/list ([book (in-list (list "Guide" "Story" "Reference"))] + #:final (string=? book "Story") + [chapter (in-list (list "Intro" "Details" "Conclusion"))]) + (list book chapter)) + : (CListof (CList CString CString)) + -> (list (list "Guide" "Intro") + (list "Guide" "Details") + (list "Guide" "Conclusion") + (list "Story" "Intro"))) + +;; ------------------------------------------------------------------------ + +;; Tests based on section 3.18 of the racket reference + +(check-type (for/list ([i (in-list (list 1 2 3))] + [j (in-list (list "a" "b" "c"))] + #:when (odd? i) + [k (in-list (list #t #f))]) + (list i j k)) + : (CListof (CList CInt CString CBool)) + -> (list (list 1 "a" #t) + (list 1 "a" #f) + (list 3 "c" #t) + (list 3 "c" #f))) + +(check-type (for/list ([i (in-list (list 1 2 3))] + [j (in-list (list "a" "b" "c"))] + #:break (not (odd? i)) + [k (in-list (list #t #f))]) + (list i j k)) + : (CListof (CList CInt CString CBool)) + -> (list (list 1 "a" #true) + (list 1 "a" #false))) + +(check-type (for/list ([i (in-list (list 1 2 3))] + [j (in-list (list "a" "b" "c"))] + #:final (not (odd? i)) + [k (in-list (list #t #f))]) + (list i j k)) + : (CListof (CList CInt CString CBool)) + -> (list (list 1 "a" #true) + (list 1 "a" #false) + (list 2 "b" #true))) + diff --git a/typed/rosette.rkt b/typed/rosette.rkt index 162357e..e12ef4c 100644 --- a/typed/rosette.rkt +++ b/typed/rosette.rkt @@ -25,7 +25,8 @@ "rosette/hash.rkt" "rosette/function.rkt" ;; base lang - (prefix-in ro: (combine-in rosette rosette/lib/synthax)) + (prefix-in ro: (combine-in rosette rosette/lib/synthax + "rosette/concrete-predicate.rkt")) (rename-in "rosette-util.rkt" [bitvector? lifted-bitvector?])) (provide : define set! λ apply ann begin @@ -522,7 +523,9 @@ ;(define-rosette-primop real? : (C→ Any Bool)) (define-solvable-type-predicate real? ro:real? CNum Num) - +(provide (typed-out [concrete-boolean? + : (C→* [Any] [] CBool : + #:+ (@ 0 : CBool) #:- (!@ 0 : CBool))])) (define-typed-syntax time [(_ e) ≫ diff --git a/typed/rosette/for-forms.rkt b/typed/rosette/for-forms.rkt index 5e6dee7..c7a2889 100644 --- a/typed/rosette/for-forms.rkt +++ b/typed/rosette/for-forms.rkt @@ -10,48 +10,109 @@ ;; ---------------------------------------------------------------------------- +;; Syntax Classes for For Clauses + +;; NOTE: +;; Rosette's for forms are unlifted, so these for syntax clases require +;; concrete sequence types and guaurd types. + +(begin-for-syntax + (define-splicing-syntax-class (for-clause-group env) + #:attributes [[clause- 1] [env.x 1] [env.τ 1]] + [pattern (~seq (~var clause (for-clause env)) + ...) + #:with [clause- ...] #'[clause.clause- ... ...] + #:with [[env.x env.τ] ...] #'[[clause.env.x clause.env.τ] ... ...]]) + + (define-splicing-syntax-class (guard-clause env) + #:attributes [[clause- 1]] + [pattern (~and (~seq #:when bool:expr) + (~typecheck + #:with [[x τ_x] ...] env + [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ CBool])) + #:with [clause- ...] #`[#:when (let- ([x- x] ...) bool-)]] + [pattern (~and (~seq #:unless bool:expr) + (~typecheck + #:with [[x τ_x] ...] env + [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ CBool])) + #:with [clause- ...] #`[#:unless (let- ([x- x] ...) bool-)]] + [pattern (~and (~seq #:break bool:expr) + (~typecheck + #:with [[x τ_x] ...] env + [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ CBool])) + #:with [clause- ...] #`[#:break (let- ([x- x] ...) bool-)]] + [pattern (~and (~seq #:final bool:expr) + (~typecheck + #:with [[x τ_x] ...] env + [[x ≫ x- : τ_x] ... ⊢ bool ≫ bool- ⇐ CBool])) + #:with [clause- ...] #`[#:final (let- ([x- x] ...) bool-)]]) + + (define-splicing-syntax-class (for-clause env) + #:attributes [[clause- 1] [env.x 1] [env.τ 1]] + [pattern (~and [x:id seq:expr] + (~typecheck + #:with [[y τ_y] ...] env + [[y ≫ y- : τ_y] ... ⊢ seq ≫ seq- ⇒ (~CSequenceof τ_x)])) + #:with [clause- ...] #'[[x (let- ([y- y] ...) seq-)]] + #:with [[env.x env.τ] ...] #'[[x τ_x]]]) + + (define-syntax-class (for-clauses env) + #:attributes [[clause- 1] [env.x 1] [env.τ 1]] + [pattern ((~var group (for-clause-group env))) + #:with [clause- ...] #'[group.clause- ...] + #:with [[env.x env.τ] ...] #'[[group.env.x group.env.τ] ...]] + [pattern ((~var fst (for-clause-group env)) + (~var guard (guard-clause (stx-append env #'[[fst.env.x fst.env.τ] ...]))) + . + (~var rst (for-clauses (stx-append env #'[[fst.env.x fst.env.τ] ...])))) + #:with [clause- ...] #'[fst.clause- ... guard.clause- ... rst.clause- ...] + #:with [[env.x env.τ] ...] #'[[fst.env.x fst.env.τ] ... [rst.env.x rst.env.τ] ...]])) + +;; ---------------------------------------------------------------------------- + ;; For Loops (define-typed-syntax for/fold - [(_ ([acc:id e_init]) - ([x:id seq:expr] ...) - body:expr ...+) ⇐ τ_acc ≫ + [(_ ([acc:id e_init:expr]) + (~var clauses (for-clauses #'[])) + body:expr ...+) ⇐ τ_acc ≫ [⊢ e_init ≫ e_init- ⇐ τ_acc] - [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] - [[acc ≫ acc- : τ_acc] - [x ≫ x- : τ_x] ... + [[acc ≫ acc- : τ_acc] [clauses.env.x ≫ x- : clauses.env.τ] ... ⊢ (begin body ...) ≫ body- ⇐ τ_acc] -------- [⊢ (ro:for/fold ([acc- e_init-]) - ([x- seq-] ...) - body-)]] - [(_ ([acc:id : τ_acc e_init]) - ([x:id seq:expr] ...) - body:expr ...+) ≫ + (clauses.clause- ...) + (ro:let ([x- clauses.env.x] ...) body-))]] + [(_ ([acc:id : τ_acc e_init:expr]) + (~var clauses (for-clauses #'[])) + body:expr ...+) ≫ [⊢ e_init ≫ e_init- ⇐ τ_acc] - [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] - [[acc ≫ acc- : τ_acc] - [x ≫ x- : τ_x] ... + [[acc ≫ acc- : τ_acc] [clauses.env.x ≫ x- : clauses.env.τ] ... ⊢ (begin body ...) ≫ body- ⇐ τ_acc] -------- [⊢ (ro:for/fold ([acc- e_init-]) - ([x- seq-] ...) - body-) + (clauses.clause- ...) + (ro:let ([x- clauses.env.x] ...) body-)) ⇒ τ_acc]]) (define-typed-syntax for - [(_ ([x:id seq:expr] ...) body:expr ...+) ≫ - [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] - [[x ≫ x- : τ_x] ... ⊢ (begin body ...) ≫ body- ⇐ Void] + [(_ (~var clauses (for-clauses #'[])) + body:expr ...+) ≫ + [[clauses.env.x ≫ x- : clauses.env.τ] ... + ⊢ [body ≫ body- ⇒ _] ...] -------- - [⊢ (ro:for ([x- seq-] ...) body-) ⇒ Void]]) + [⊢ (ro:for (clauses.clause- ...) + (ro:let ([x- clauses.env.x] ...) body- ...)) + ⇒ CVoid]]) (define-typed-syntax for/list - [(_ ([x:id seq:expr] ...) body:expr) ≫ - [⊢ [seq ≫ seq- ⇒ (~CSequenceof τ_x)] ...] - [[x ≫ x- : τ_x] ... ⊢ body ≫ body- ⇒ τ_body] + [(_ (~var clauses (for-clauses #'[])) + body:expr ...+) ≫ + [[clauses.env.x ≫ x- : clauses.env.τ] ... + ⊢ (begin body ...) ≫ body- ⇒ τ_body] -------- - [⊢ (ro:for/list ([x- seq-] ...) body-) + [⊢ (ro:for/list (clauses.clause- ...) + (ro:let ([x- clauses.env.x] ...) body-)) ⇒ (CListof τ_body)]]) (define-typed-syntax for*/list @@ -98,14 +159,28 @@ (define-typed-syntax in-list [(_ e:expr) ≫ - [⊢ e ≫ e- ⇒ : (~CListof τ)] + [⊢ e ≫ e- ⇒ : (~CListof ~! τ)] + -------- + [⊢ (ro:in-list e-) ⇒ : (CSequenceof τ)]] + [(_ e:expr) ≫ + [⊢ e ≫ e- ⇒ : (~CList ~! τ ...)] + #:with τ* (cond [(stx-andmap concrete? #'[τ ...]) + #'(CU τ ...)] + [(= 1 (stx-length #'[τ ...])) + (stx-car #'[τ ...])] + [else + #'(U τ ...)]) -------- - [⊢ (ro:in-list e-) ⇒ : (CSequenceof τ)]]) + [⊢ (ro:in-list e-) ⇒ : (CSequenceof τ*)]]) (define-typed-syntax in-naturals [(_) ≫ -------- - [⊢ (ro:in-naturals) ⇒ : (CSequenceof CNat)]]) + [⊢ (ro:in-naturals) ⇒ : (CSequenceof CNat)]] + [(_ e:expr) ≫ + [⊢ e ≫ e- ⇐ CNat] + -------- + [⊢ (ro:in-naturals e-) ⇒ : (CSequenceof CNat)]]) (define-typed-syntax in-range [(_ e:expr) ≫ diff --git a/typed/rosette/list.rkt b/typed/rosette/list.rkt index caf7bed..abe68b4 100644 --- a/typed/rosette/list.rkt +++ b/typed/rosette/list.rkt @@ -393,10 +393,15 @@ -------- [⊢ [_ ≫ ro:andmap ⇒ : (C→ (C→ Any Bool) (CListof Any) Bool)]]] [(_ f lst) ≫ - [⊢ [f ≫ f- ⇒ : (~C→ ~! ty ty-bool)]] + [⊢ [f ≫ f- ⇒ : (~C→ ~! ty ty-bool : #:+ p+ #:- _)]] [⊢ [lst ≫ lst- ⇒ : (~CListof _)]] + #:with prop_out+ + (syntax-parse #'p+ + [(~Prop/IndexType (_ 0) τ_elem) + #`(Prop/ObjType #,(get-arg-obj #'lst-) : (CListof τ_elem))] + [_ #`Prop/Top]) -------- - [⊢ [_ ≫ (ro:andmap f- lst-) ⇒ : Bool]]] + [⊢ [_ ≫ (ro:andmap f- lst-) (⇒ : Bool) (⇒ prop+ prop_out+)]]] #;[(_ f lst) ≫ [⊢ [lst ≫ lst- ⇒ : (~CListof ty)]] [⊢ [f ≫ f- ⇒ : (~Ccase-> ~! ty-fns ...)]] ; find first match diff --git a/typed/rosette/types.rkt b/typed/rosette/types.rkt index 631a4e6..338dfeb 100644 --- a/typed/rosette/types.rkt +++ b/typed/rosette/types.rkt @@ -34,7 +34,8 @@ Prop/Or Prop/And with-occurrence-prop - (for-syntax prop-instantiate get-arg-obj) + (for-syntax prop-instantiate get-arg-obj + ~Prop/IndexType) ;; Parameters CParamof ; TODO: symbolic Param not supported yet ;; List types From 62ea00b25d3282c7b4d747abb0b262484565efb8 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Sat, 8 Jul 2017 11:39:04 -0400 Subject: [PATCH 20/24] fix usage of provide typed-out --- typed/rosette/vector.rkt | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/typed/rosette/vector.rkt b/typed/rosette/vector.rkt index e1ca3f0..66e1635 100644 --- a/typed/rosette/vector.rkt +++ b/typed/rosette/vector.rkt @@ -1,7 +1,8 @@ #lang turnstile (require typed/rosette/types - (prefix-in ro: rosette)) + (prefix-in ro: rosette) + (postfix-in - rosette)) ;; ------------------------------------------------------------------------ From 6d2afc7509e5184afae300b69be891fbf8b49cfc Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Sat, 8 Jul 2017 11:43:00 -0400 Subject: [PATCH 21/24] add dependency on 6.8.0.3 --- .travis.yml | 4 +--- info.rkt | 2 +- 2 files changed, 2 insertions(+), 4 deletions(-) diff --git a/.travis.yml b/.travis.yml index 96a1672..bf5d8b9 100644 --- a/.travis.yml +++ b/.travis.yml @@ -4,9 +4,7 @@ env: global: - RACKET_DIR=~/racket matrix: - - RACKET_VERSION="6.6" - - RACKET_VERSION="6.7" - - RACKET_VERSION="6.8" + - RACKET_VERSION="6.9" - RACKET_VERSION="HEAD" matrix: allow_failures: diff --git a/info.rkt b/info.rkt index 2810b7f..cff0e67 100644 --- a/info.rkt +++ b/info.rkt @@ -3,7 +3,7 @@ (define collection 'multi) (define deps - '(("racket" #:version "6.6") + '(("racket" #:version "6.8.0.3") "base" "rosette" "turnstile" From ef690010ae1dfe64d6c35c78f4addf14bda5de63 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Sun, 9 Jul 2017 01:25:05 -0400 Subject: [PATCH 22/24] fix match --- typed/rosette/match-core.rkt | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/typed/rosette/match-core.rkt b/typed/rosette/match-core.rkt index 2624f33..7d800de 100644 --- a/typed/rosette/match-core.rkt +++ b/typed/rosette/match-core.rkt @@ -135,7 +135,7 @@ [(_ val:expr [pat:pat body:expr] ...) ≫ [⊢ val ≫ val- ⇒ τ_val] #:with obj (get-arg-obj #'val-) - #:with tmp (generate-temporary #'val) + #:with tmp (if (identifier? #'val) #'val- (generate-temporary #'val)) #:with [p:pat-info ...] (map-app3 #'tmp #'τ_val #'obj (attribute pat.get-pat-info)) [[p.x ≫ x- : p.τ] ... @@ -164,13 +164,15 @@ [(x- ...) xs-] [(i- ...) (range (stx-length xs-))] [body- body-]) - #'(let- ([v-tmp maybe-vec]) - (if- v-tmp - (let- ([x- (vector-ref- v-tmp i-)] ...) - body-) - acc)))) + (quasisyntax/loc this-syntax + (let- ([v-tmp maybe-vec]) + #,(syntax/loc this-syntax + (if- v-tmp + (let- ([x- (vector-ref- v-tmp i-)] ...) + body-) + acc)))))) -------- - [⊢ (let- ([tmp val-]) matching-expr-) + [⊢ (for/all- ([tmp val-]) matching-expr-) ⇒ τ_out]]) ;; ------------------------------------------------------------------------ From 6fc64576be3e36277393a93663674e2a7f5a99ae Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Sun, 9 Jul 2017 17:18:29 -0400 Subject: [PATCH 23/24] update travis.yml: test typechecking for Ocelot --- .travis.yml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index bf5d8b9..4744607 100644 --- a/.travis.yml +++ b/.travis.yml @@ -28,4 +28,10 @@ install: script: - raco test --package typed-rosette - - raco setup \ No newline at end of file + # Install the Typed Rosette version of Ocelot + - raco pkg install --auto git://github.com/AlexKnauth/ocelot#typed-rosette + - raco setup + +after_success: + # this currently fails 1 out of 728 tests + - raco test --package ocelot From 12e855b836d3ede89ce2c910bbe38f4b2762b699 Mon Sep 17 00:00:00 2001 From: AlexKnauth Date: Mon, 10 Jul 2017 13:58:25 -0400 Subject: [PATCH 24/24] update .travis.yml: install Typed Ocelot with `-j 1` --- .travis.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.travis.yml b/.travis.yml index 4744607..0f0be8a 100644 --- a/.travis.yml +++ b/.travis.yml @@ -29,7 +29,7 @@ install: script: - raco test --package typed-rosette # Install the Typed Rosette version of Ocelot - - raco pkg install --auto git://github.com/AlexKnauth/ocelot#typed-rosette + - raco pkg install -j 1 --auto git://github.com/AlexKnauth/ocelot#typed-rosette - raco setup after_success: