diff --git a/graph-lib/graph/fold-queues.lp2.rkt b/graph-lib/graph/fold-queues.lp2.rkt index 386e0f0..4db68bf 100644 --- a/graph-lib/graph/fold-queues.lp2.rkt +++ b/graph-lib/graph/fold-queues.lp2.rkt @@ -114,9 +114,9 @@ database type opaque, and use an accessor with signature (let* ([new-h (hash-set h elt i)] [new-s (cons elt s)] [new-i (+ i 1)] - [new-i-index (if (index? new-i) - new-i - (error "Too many elements"))] + ;; The assert is always true, as this is what + ;; the `length` function would return. + [new-i-index (assert new-i index?)] [name/queue (list new-h rs new-s new-i-index)]) (values i (list name/queue …)))))] diff --git a/graph-lib/graph/graph-5-multi-ctors.lp2.rkt b/graph-lib/graph/graph-5-multi-ctors.lp2.rkt index 3d021f8..f6d5c59 100644 --- a/graph-lib/graph/graph-5-multi-ctors.lp2.rkt +++ b/graph-lib/graph/graph-5-multi-ctors.lp2.rkt @@ -9,7 +9,11 @@ @section{Introduction} -We define a wrapper around the @tc[graph] macro, which +We define a wrapper around the @tc[graph] macro, which allows defining sevral +mappings which return the same node type. In other words, nodes now have named +constructors. + +The new signature separates the mapping declarations from the node definitions: @chunk[ (define-graph/multi-ctor name:id @@ -18,13 +22,13 @@ We define a wrapper around the @tc[graph] macro, which (~commit ) …)] -Where @tc[] is: +Where @tc[] hasn't changed: @chunk[ (~describe "[field : type]" [field:id c:colon field-type:expr])] -And @tc[] is: +And @tc[] is now: @chunk[ (~describe "[(mapping [param : type] …) : result . body]" @@ -102,8 +106,6 @@ Where the type for the merged mapping is: (U (List 'grouped-mapping grouped-param-type …) …)] @chunk[ - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (begin (: mapping/placeholder (→ param-type … (name/wrapped #:placeholder result-node))) @@ -126,8 +128,6 @@ Where the type for the merged mapping is: We then select in the grouped mapping which one to call. @chunk[ - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; - ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; (cond [(eq? (car node/arg↓) 'grouped-mapping) (apply grouped-mapping/function diff --git a/graph-lib/graph/graph.lp2.rkt b/graph-lib/graph/graph.lp2.rkt index 65c5410..ac679c3 100644 --- a/graph-lib/graph/graph.lp2.rkt +++ b/graph-lib/graph/graph.lp2.rkt @@ -437,7 +437,7 @@ library. We replace all occurrences of a @tc[node] name with its Δ-Queues …)]) (let-values ([(r new-Δ-queues) (f (cdr mapping-result) Δ-queues)]) - (values (cons 'node/with-indices-tag r) + (values (apply node/make-with-indices r) new-Δ-queues))))] Where @tc[] is the @tc[field-type] in which node types @@ -567,8 +567,15 @@ via @tc[(g Street)]. We will be able to use this type expander in function types, for example: @chunk[ - (λ ([x : (gr Street)]) - x)] + (define (type-example [x : (gr Street)]) + : (gr Street) + x) + (check-equal?: (let* ([v1 (car (structure-get (cadr (force g)) streets))] + [v2 (ann (type-example (force v1)) (gr Street))] + [v3 (structure-get (cadr v2) sname)]) + v3) + : String + "Ada Street")] @section{Putting it all together} @@ -668,7 +675,8 @@ not match the one from @tc[typed/racket] @chunk[ (module* test typed/racket (require (submod "..") - (only-in "../lib/low.rkt" cars cdrs) + (only-in "../lib/low.rkt" cars cdrs check-equal?:) + (only-in "structure.lp2.rkt" structure-get) "../type-expander/type-expander.lp2.rkt" typed/rackunit) diff --git a/graph-lib/graph/remember.rkt b/graph-lib/graph/remember.rkt index 3fc4026..a44c376 100644 --- a/graph-lib/graph/remember.rkt +++ b/graph-lib/graph/remember.rkt @@ -85,3 +85,5 @@ (structure ba v) (structure ab v) (structure ab v) +(structure a c) +(structure a c) diff --git a/graph-lib/graph/rewrite-type.lp2.rkt b/graph-lib/graph/rewrite-type.lp2.rkt index c0747b4..ca2ca55 100644 --- a/graph-lib/graph/rewrite-type.lp2.rkt +++ b/graph-lib/graph/rewrite-type.lp2.rkt @@ -487,13 +487,11 @@ functions is undefined. #,@(stx-map (λ (ta) ) #'(a ...)) [else - (begin - val - (typecheck-fail #,type - #,(~a "Unhandled union case in " - (syntax->datum #'(U a …)) - ", whole type was:" - (syntax->datum whole-type))))]))] + (typecheck-fail #,type + #,(~a "Unhandled union case in " + (syntax->datum #'(U a …)) + ", whole type was:" + (syntax->datum whole-type)))]))] [((~literal quote) a) #'(inst values 'a acc-type)] [x:id diff --git a/graph-lib/graph/structure.lp2.rkt b/graph-lib/graph/structure.lp2.rkt index ede2bad..56269ac 100644 --- a/graph-lib/graph/structure.lp2.rkt +++ b/graph-lib/graph/structure.lp2.rkt @@ -121,7 +121,7 @@ handle the empty structure as a special case. (if (not (stx-null? #'(type …))) #'(inst (make-structure-constructor field ...) type ...) #'(make-structure-constructor field ...))) - (: (?? name? default-name?) (→ Any Any)) + (: (?? name? default-name?) (→ Any Boolean)) (define ((?? name? default-name?) x) (match x [(structure [field _] …) #t] @@ -131,7 +131,8 @@ handle the empty structure as a special case. @chunk[ (define-structure empty-st) (define-structure st [a Number] [b String]) - (define-structure st2 [b String] [a Number])] + (define-structure st2 [b String] [a Number] #:? custom-is-st2?) + (define-structure st3 [c String] [a Number] #:? custom-is-st3?)] Test constructor: @@ -169,6 +170,30 @@ Test equality: (check-equal? (ann (st2 "j" 2) st2) (st2 "j" 2)) (check-equal? (ann (st 1 "k") st) (st2 "k" 1))] +Test predicate: + +@chunk[ + (check-equal? (st? (ann (st 1 "i") (U st st2))) #t) + (check-equal? (custom-is-st2? (ann (st 1 "i") (U st st2))) #t) + (check-equal? (custom-is-st3? (ann (st 1 "i") (U st st2))) #f) + (check-equal? (st? (ann (st 1 "i") (U Number st st2))) #t) + (check-equal? (st? (ann 1 (U Number st st2))) #f) + ;; Occurrence typing won't work well, if only because fields could be of + ;; a type for which TR doesn't know how to make-predicate. + #|(define (check-occurrence-typing [x : (U Number st st3)]) + (if (st? x) + (match (ann x st) [(st the-a the-b) (cons the-b the-a)]) + 'other)) + (check-equal? + (check-occurrence-typing (ann (st 1 "i") (U Number st st3))) + '("i" . 1)) + (check-equal? + (check-occurrence-typing (ann (st2 "j" 2) (U Number st st3))) + 'other) + (check-equal? + (check-occurrence-typing (ann 9 (U Number st st3))) + 'other)|#] + @section{Pre-declaring structs} We wish to pre-declare all @tc[struct] types for various reasons: @@ -644,7 +669,7 @@ chances that we could write a definition for that identifier. "../lib/low.rkt" "../type-expander/type-expander.lp2.rkt" typed/rackunit) - + diff --git a/graph-lib/type-expander/type-expander.lp2.rkt b/graph-lib/type-expander/type-expander.lp2.rkt index b9fe1b3..30875b4 100644 --- a/graph-lib/type-expander/type-expander.lp2.rkt +++ b/graph-lib/type-expander/type-expander.lp2.rkt @@ -114,6 +114,8 @@ else. (define-syntax-class fa (pattern (~or (~literal ∀) (~literal All)))) (syntax-parse stx + [(~datum :) ;; TODO: This is a hack, we should use ~literal. + #':] [:type-expander (expand-type (apply-type-expander #'expander #'expander))] [:type-expander-nested-application @@ -171,7 +173,10 @@ identifier. [(_ t) #'(id (Pairof (id t) t))])) (test-expander (∀ (A) (→ A (id (double (id A))))) - (∀ (A) (→ A (Pairof A A))))] + (∀ (A) (→ A (Pairof A A)))) + + (test-expander (→ Any Boolean : (double (id A))) + (→ Any Boolean : (Pairof A A)))] Curry expander arguments: