From 6e29bdad31b09722287caf5051887bcaeebfd19d Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sun, 30 Mar 2014 10:06:24 -0500 Subject: [PATCH] adjust check function to properly deal with the store --- .../redex/examples/benchmark/let-poly/1.diff | 2 +- .../redex/examples/benchmark/let-poly/2.diff | 2 +- .../redex/examples/benchmark/let-poly/3.diff | 3 +- .../redex/examples/benchmark/let-poly/4.diff | 4 +- .../redex/examples/benchmark/let-poly/5.diff | 2 +- .../redex/examples/benchmark/let-poly/6.diff | 2 +- .../redex/examples/benchmark/let-poly/7.diff | 2 +- .../benchmark/let-poly/let-poly-1.rkt | 115 ++++++++++++++--- .../benchmark/let-poly/let-poly-2.rkt | 115 ++++++++++++++--- .../benchmark/let-poly/let-poly-3.rkt | 116 ++++++++++++++---- .../benchmark/let-poly/let-poly-4.rkt | 115 ++++++++++++++--- .../benchmark/let-poly/let-poly-5.rkt | 115 ++++++++++++++--- .../benchmark/let-poly/let-poly-6.rkt | 115 ++++++++++++++--- .../benchmark/let-poly/let-poly-7.rkt | 115 ++++++++++++++--- .../benchmark/let-poly/let-poly-base.rkt | 115 ++++++++++++++--- .../examples/benchmark/let-poly/tests.rkt | 53 +++++++- 16 files changed, 820 insertions(+), 171 deletions(-) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff index 19bc9a83d1..420e3cde88 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff @@ -6,7 +6,7 @@ < (tc-down (x y Γ) M (λ y κ) σ_ans) --- > (tc-down (x y Γ) M (λ x κ) σ_ans) -496a497,499 +571a572,574 > > (define small-counter-example '(hd ((λ x x) 1))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff index 6c2cab5500..be23186576 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff @@ -16,7 +16,7 @@ < [(where #t (not-v? M)) < (tc-down Γ ((λ x N) M) κ σ_2) < --------------------------------- -496a492,497 +571a567,572 > > (define small-counter-example '(let ([x (new nil)]) > ((λ ignore diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff index d5f9a34a98..41410541d9 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff @@ -6,8 +6,7 @@ < (where G (unify τ_2 (τ_1 → x))) --- > (where G (unify τ_1 (τ_2 → x))) -496a497,500 -> +571a572,574 > > (define small-counter-example (term (1 cons))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff index 2316c01255..2866bbff00 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff @@ -8,7 +8,7 @@ < [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] --- > [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))] -496a499,501 +571a574,576 > > (define small-counter-example (term ((λ x (x x)) (λ x x)))) -> (check-equal? (check small-counter-example #f)) +> (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff index 7c7f60f7c5..86bf20179a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff @@ -10,7 +10,7 @@ > (τ (eliminate-τ x τ σ) (eliminate-G x τ G))] > [(eliminate-G x τ (y σ G)) > (y (eliminate-τ x τ σ) (eliminate-G x τ G))]) -496a499,503 +571a574,578 > > (define small-counter-example (term (cons 1))) > (test-equal (with-handlers ([exn:fail? (λ (x) #f)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff index baf68a6e9c..773d1a12f9 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff @@ -6,7 +6,7 @@ < [(∨ boolean_1 boolean_2) #t]) --- > [(∨ boolean boolean) #t]) -496a497,501 +571a572,576 > > (define small-counter-example (term ((λ x x) 1))) > (test-equal (with-handlers ([exn:fail? (λ (x) #f)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff index eb70a91977..31dcf22a1b 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff @@ -15,7 +15,7 @@ --- > (--> (Σ (in-hole E (let ([x M]) N))) > (Σ (in-hole E ((λ x N) M))) -496a498,500 +571a573,575 > > (define small-counter-example (term (let ((x (λ y y))) (x x)))) > (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt index 4cdf49b60c..c0511f8ac9 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - racket/bool + racket/bool racket/set (only-in "../stlc/tests-lib.rkt" consistent-with?)) (provide (all-defined-out)) @@ -386,8 +386,8 @@ A top-level evaluator (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) - (define M-t (judgment-holds (typeof ,M τ) τ)) - (unless (pair? M-t) + (define M-t (type-check M)) + (unless M-t (error 'Eval "doesn't typecheck: ~s" M)) (define res (apply-reduction-relation* red (term (· ,M)))) (unless (= 1 (length res)) @@ -396,7 +396,7 @@ A top-level evaluator (match (car res) ["error" "error"] [`(,Σ ,N) - (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (define ans-t (type-check N Σ)) (unless (equal? M-t ans-t) (error 'Eval "internal error: type soundness fails for ~s" M)) (match N @@ -411,31 +411,107 @@ A top-level evaluator [(? number?) N] [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) -(define-metafunction stlc - Σ->lets : Σ M -> M - [(Σ->lets · M) M] - [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) - #| -A top-level type checker. +A type checker; the optional argument is a store to use +for type checking free variables in M. |# -(define/contract (type-check M) - (-> M? (or/c τ? #f)) - (define M-t (judgment-holds (typeof ,M τ) τ)) +(define/contract (type-check M [Σ (term ·)]) + (->* (M?) (any/c) (or/c τ? #f)) + (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) (cond - [(empty? M-t) + [(null? M-ts) #f] - [(null? (cdr M-t)) - (car M-t)] + [(null? (cdr M-ts)) + (car M-ts)] [else - (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) + +;; building an expression out of a store can be done in this model +;; with just topological sort because there are no recursive types, +;; so the store will not contain any cycles +(define (Σ+M->M Σ M) + ;; nodes : edges[r -o> v] + (define nodes (make-hash)) + (define edges (make-hash)) + (let loop ([Σ Σ]) + (match Σ + [`· (void)] + [`(,r ,v ,Σ) + (hash-set! nodes r v) + (loop Σ)])) + + (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) + (for ([(n-src rhs) (in-hash nodes)]) + (for ([(n-dest _) (in-hash nodes)]) + (when (mentions-node? n-dest rhs) + (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) + (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) + edges)) + (let loop ([sorted rev-sorted]) + (cond + [(empty? sorted) M] + [else + (define r (car sorted)) + (term (let ([,r (new ,(hash-ref nodes r))]) + ,(loop (cdr sorted))))]))) + +(define (mentions-node? v r) + (let loop ([v v]) + (cond + [(symbol? v) (equal? r v)] + [(pair? v) (or (loop (car v)) (loop (cdr v)))] + [else #f]))) #| -Random generators +The first algorithm from this page: +http://en.wikipedia.org/wiki/Topological_sorting#Algorithms + +|# +(define/contract (reverse-topo-sort nodes edges) + (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) + + (for ([node (in-list nodes)]) + (unless (hash-ref edges node #f) + (error 'topo-sort "no edge entry for ~s" node))) + + (define incoming-counts (build-incoming-counts nodes edges)) + (define (remove-edge src dest) + (hash-set! edges src (set-remove (hash-ref edges src) dest)) + (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) + + (define l '()) + (define s (for/set ([(n c) (in-hash incoming-counts)] + #:when (zero? c)) + n)) + (let loop () + (unless (set-empty? s) + (define n (set-first s)) + (set! s (set-remove s n)) + (set! l (cons n l)) + (for ([m (in-set (hash-ref edges n))]) + (remove-edge n m) + (when (zero? (hash-ref incoming-counts m)) + (set! s (set-add s m)))) + (loop))) + + l) + +(define (build-incoming-counts nodes edges) + (define incoming-counts (make-hash)) + (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) + (for ([(n neighbors) (in-hash edges)]) + (for ([neighbor (in-set neighbors)]) + (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) + incoming-counts) + + +#| + +Generators |# @@ -485,8 +561,7 @@ from the given term. (implies t-type (let loop ([Σ+M `(· ,M)]) - (define new-type - (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) (let ([red-res (apply-reduction-relation red Σ+M)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt index cb845886ea..48412165c2 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - racket/bool + racket/bool racket/set (only-in "../stlc/tests-lib.rkt" consistent-with?)) (provide (all-defined-out)) @@ -381,8 +381,8 @@ A top-level evaluator (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) - (define M-t (judgment-holds (typeof ,M τ) τ)) - (unless (pair? M-t) + (define M-t (type-check M)) + (unless M-t (error 'Eval "doesn't typecheck: ~s" M)) (define res (apply-reduction-relation* red (term (· ,M)))) (unless (= 1 (length res)) @@ -391,7 +391,7 @@ A top-level evaluator (match (car res) ["error" "error"] [`(,Σ ,N) - (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (define ans-t (type-check N Σ)) (unless (equal? M-t ans-t) (error 'Eval "internal error: type soundness fails for ~s" M)) (match N @@ -406,31 +406,107 @@ A top-level evaluator [(? number?) N] [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) -(define-metafunction stlc - Σ->lets : Σ M -> M - [(Σ->lets · M) M] - [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) - #| -A top-level type checker. +A type checker; the optional argument is a store to use +for type checking free variables in M. |# -(define/contract (type-check M) - (-> M? (or/c τ? #f)) - (define M-t (judgment-holds (typeof ,M τ) τ)) +(define/contract (type-check M [Σ (term ·)]) + (->* (M?) (any/c) (or/c τ? #f)) + (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) (cond - [(empty? M-t) + [(null? M-ts) #f] - [(null? (cdr M-t)) - (car M-t)] + [(null? (cdr M-ts)) + (car M-ts)] [else - (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) + +;; building an expression out of a store can be done in this model +;; with just topological sort because there are no recursive types, +;; so the store will not contain any cycles +(define (Σ+M->M Σ M) + ;; nodes : edges[r -o> v] + (define nodes (make-hash)) + (define edges (make-hash)) + (let loop ([Σ Σ]) + (match Σ + [`· (void)] + [`(,r ,v ,Σ) + (hash-set! nodes r v) + (loop Σ)])) + + (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) + (for ([(n-src rhs) (in-hash nodes)]) + (for ([(n-dest _) (in-hash nodes)]) + (when (mentions-node? n-dest rhs) + (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) + (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) + edges)) + (let loop ([sorted rev-sorted]) + (cond + [(empty? sorted) M] + [else + (define r (car sorted)) + (term (let ([,r (new ,(hash-ref nodes r))]) + ,(loop (cdr sorted))))]))) + +(define (mentions-node? v r) + (let loop ([v v]) + (cond + [(symbol? v) (equal? r v)] + [(pair? v) (or (loop (car v)) (loop (cdr v)))] + [else #f]))) #| -Random generators +The first algorithm from this page: +http://en.wikipedia.org/wiki/Topological_sorting#Algorithms + +|# +(define/contract (reverse-topo-sort nodes edges) + (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) + + (for ([node (in-list nodes)]) + (unless (hash-ref edges node #f) + (error 'topo-sort "no edge entry for ~s" node))) + + (define incoming-counts (build-incoming-counts nodes edges)) + (define (remove-edge src dest) + (hash-set! edges src (set-remove (hash-ref edges src) dest)) + (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) + + (define l '()) + (define s (for/set ([(n c) (in-hash incoming-counts)] + #:when (zero? c)) + n)) + (let loop () + (unless (set-empty? s) + (define n (set-first s)) + (set! s (set-remove s n)) + (set! l (cons n l)) + (for ([m (in-set (hash-ref edges n))]) + (remove-edge n m) + (when (zero? (hash-ref incoming-counts m)) + (set! s (set-add s m)))) + (loop))) + + l) + +(define (build-incoming-counts nodes edges) + (define incoming-counts (make-hash)) + (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) + (for ([(n neighbors) (in-hash edges)]) + (for ([neighbor (in-set neighbors)]) + (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) + incoming-counts) + + +#| + +Generators |# @@ -480,8 +556,7 @@ from the given term. (implies t-type (let loop ([Σ+M `(· ,M)]) - (define new-type - (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) (let ([red-res (apply-reduction-relation red Σ+M)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt index 14c8ed94c6..5dd8f9843c 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - racket/bool + racket/bool racket/set (only-in "../stlc/tests-lib.rkt" consistent-with?)) (provide (all-defined-out)) @@ -386,8 +386,8 @@ A top-level evaluator (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) - (define M-t (judgment-holds (typeof ,M τ) τ)) - (unless (pair? M-t) + (define M-t (type-check M)) + (unless M-t (error 'Eval "doesn't typecheck: ~s" M)) (define res (apply-reduction-relation* red (term (· ,M)))) (unless (= 1 (length res)) @@ -396,7 +396,7 @@ A top-level evaluator (match (car res) ["error" "error"] [`(,Σ ,N) - (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (define ans-t (type-check N Σ)) (unless (equal? M-t ans-t) (error 'Eval "internal error: type soundness fails for ~s" M)) (match N @@ -411,31 +411,107 @@ A top-level evaluator [(? number?) N] [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) -(define-metafunction stlc - Σ->lets : Σ M -> M - [(Σ->lets · M) M] - [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) - #| -A top-level type checker. +A type checker; the optional argument is a store to use +for type checking free variables in M. |# -(define/contract (type-check M) - (-> M? (or/c τ? #f)) - (define M-t (judgment-holds (typeof ,M τ) τ)) +(define/contract (type-check M [Σ (term ·)]) + (->* (M?) (any/c) (or/c τ? #f)) + (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) (cond - [(empty? M-t) + [(null? M-ts) #f] - [(null? (cdr M-t)) - (car M-t)] + [(null? (cdr M-ts)) + (car M-ts)] [else - (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) + +;; building an expression out of a store can be done in this model +;; with just topological sort because there are no recursive types, +;; so the store will not contain any cycles +(define (Σ+M->M Σ M) + ;; nodes : edges[r -o> v] + (define nodes (make-hash)) + (define edges (make-hash)) + (let loop ([Σ Σ]) + (match Σ + [`· (void)] + [`(,r ,v ,Σ) + (hash-set! nodes r v) + (loop Σ)])) + + (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) + (for ([(n-src rhs) (in-hash nodes)]) + (for ([(n-dest _) (in-hash nodes)]) + (when (mentions-node? n-dest rhs) + (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) + (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) + edges)) + (let loop ([sorted rev-sorted]) + (cond + [(empty? sorted) M] + [else + (define r (car sorted)) + (term (let ([,r (new ,(hash-ref nodes r))]) + ,(loop (cdr sorted))))]))) + +(define (mentions-node? v r) + (let loop ([v v]) + (cond + [(symbol? v) (equal? r v)] + [(pair? v) (or (loop (car v)) (loop (cdr v)))] + [else #f]))) #| -Random generators +The first algorithm from this page: +http://en.wikipedia.org/wiki/Topological_sorting#Algorithms + +|# +(define/contract (reverse-topo-sort nodes edges) + (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) + + (for ([node (in-list nodes)]) + (unless (hash-ref edges node #f) + (error 'topo-sort "no edge entry for ~s" node))) + + (define incoming-counts (build-incoming-counts nodes edges)) + (define (remove-edge src dest) + (hash-set! edges src (set-remove (hash-ref edges src) dest)) + (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) + + (define l '()) + (define s (for/set ([(n c) (in-hash incoming-counts)] + #:when (zero? c)) + n)) + (let loop () + (unless (set-empty? s) + (define n (set-first s)) + (set! s (set-remove s n)) + (set! l (cons n l)) + (for ([m (in-set (hash-ref edges n))]) + (remove-edge n m) + (when (zero? (hash-ref incoming-counts m)) + (set! s (set-add s m)))) + (loop))) + + l) + +(define (build-incoming-counts nodes edges) + (define incoming-counts (make-hash)) + (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) + (for ([(n neighbors) (in-hash edges)]) + (for ([neighbor (in-set neighbors)]) + (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) + incoming-counts) + + +#| + +Generators |# @@ -485,8 +561,7 @@ from the given term. (implies t-type (let loop ([Σ+M `(· ,M)]) - (define new-type - (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) (let ([red-res (apply-reduction-relation red Σ+M)]) @@ -495,6 +570,5 @@ from the given term. (or (equal? red-t "error") (loop red-t)))))))))))) - (define small-counter-example (term (1 cons))) (test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt index 1bf3e8f9c1..40472524ca 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt @@ -9,7 +9,7 @@ racket/match racket/list racket/contract - racket/bool + racket/bool racket/set (only-in "../stlc/tests-lib.rkt" consistent-with?)) (provide (all-defined-out)) @@ -388,8 +388,8 @@ A top-level evaluator (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) - (define M-t (judgment-holds (typeof ,M τ) τ)) - (unless (pair? M-t) + (define M-t (type-check M)) + (unless M-t (error 'Eval "doesn't typecheck: ~s" M)) (define res (apply-reduction-relation* red (term (· ,M)))) (unless (= 1 (length res)) @@ -398,7 +398,7 @@ A top-level evaluator (match (car res) ["error" "error"] [`(,Σ ,N) - (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (define ans-t (type-check N Σ)) (unless (equal? M-t ans-t) (error 'Eval "internal error: type soundness fails for ~s" M)) (match N @@ -413,31 +413,107 @@ A top-level evaluator [(? number?) N] [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) -(define-metafunction stlc - Σ->lets : Σ M -> M - [(Σ->lets · M) M] - [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) - #| -A top-level type checker. +A type checker; the optional argument is a store to use +for type checking free variables in M. |# -(define/contract (type-check M) - (-> M? (or/c τ? #f)) - (define M-t (judgment-holds (typeof ,M τ) τ)) +(define/contract (type-check M [Σ (term ·)]) + (->* (M?) (any/c) (or/c τ? #f)) + (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) (cond - [(empty? M-t) + [(null? M-ts) #f] - [(null? (cdr M-t)) - (car M-t)] + [(null? (cdr M-ts)) + (car M-ts)] [else - (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) + +;; building an expression out of a store can be done in this model +;; with just topological sort because there are no recursive types, +;; so the store will not contain any cycles +(define (Σ+M->M Σ M) + ;; nodes : edges[r -o> v] + (define nodes (make-hash)) + (define edges (make-hash)) + (let loop ([Σ Σ]) + (match Σ + [`· (void)] + [`(,r ,v ,Σ) + (hash-set! nodes r v) + (loop Σ)])) + + (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) + (for ([(n-src rhs) (in-hash nodes)]) + (for ([(n-dest _) (in-hash nodes)]) + (when (mentions-node? n-dest rhs) + (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) + (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) + edges)) + (let loop ([sorted rev-sorted]) + (cond + [(empty? sorted) M] + [else + (define r (car sorted)) + (term (let ([,r (new ,(hash-ref nodes r))]) + ,(loop (cdr sorted))))]))) + +(define (mentions-node? v r) + (let loop ([v v]) + (cond + [(symbol? v) (equal? r v)] + [(pair? v) (or (loop (car v)) (loop (cdr v)))] + [else #f]))) #| -Random generators +The first algorithm from this page: +http://en.wikipedia.org/wiki/Topological_sorting#Algorithms + +|# +(define/contract (reverse-topo-sort nodes edges) + (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) + + (for ([node (in-list nodes)]) + (unless (hash-ref edges node #f) + (error 'topo-sort "no edge entry for ~s" node))) + + (define incoming-counts (build-incoming-counts nodes edges)) + (define (remove-edge src dest) + (hash-set! edges src (set-remove (hash-ref edges src) dest)) + (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) + + (define l '()) + (define s (for/set ([(n c) (in-hash incoming-counts)] + #:when (zero? c)) + n)) + (let loop () + (unless (set-empty? s) + (define n (set-first s)) + (set! s (set-remove s n)) + (set! l (cons n l)) + (for ([m (in-set (hash-ref edges n))]) + (remove-edge n m) + (when (zero? (hash-ref incoming-counts m)) + (set! s (set-add s m)))) + (loop))) + + l) + +(define (build-incoming-counts nodes edges) + (define incoming-counts (make-hash)) + (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) + (for ([(n neighbors) (in-hash edges)]) + (for ([neighbor (in-set neighbors)]) + (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) + incoming-counts) + + +#| + +Generators |# @@ -487,8 +563,7 @@ from the given term. (implies t-type (let loop ([Σ+M `(· ,M)]) - (define new-type - (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) (let ([red-res (apply-reduction-relation red Σ+M)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt index abb964ed15..3d556cae25 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - racket/bool + racket/bool racket/set (only-in "../stlc/tests-lib.rkt" consistent-with?)) (provide (all-defined-out)) @@ -388,8 +388,8 @@ A top-level evaluator (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) - (define M-t (judgment-holds (typeof ,M τ) τ)) - (unless (pair? M-t) + (define M-t (type-check M)) + (unless M-t (error 'Eval "doesn't typecheck: ~s" M)) (define res (apply-reduction-relation* red (term (· ,M)))) (unless (= 1 (length res)) @@ -398,7 +398,7 @@ A top-level evaluator (match (car res) ["error" "error"] [`(,Σ ,N) - (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (define ans-t (type-check N Σ)) (unless (equal? M-t ans-t) (error 'Eval "internal error: type soundness fails for ~s" M)) (match N @@ -413,31 +413,107 @@ A top-level evaluator [(? number?) N] [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) -(define-metafunction stlc - Σ->lets : Σ M -> M - [(Σ->lets · M) M] - [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) - #| -A top-level type checker. +A type checker; the optional argument is a store to use +for type checking free variables in M. |# -(define/contract (type-check M) - (-> M? (or/c τ? #f)) - (define M-t (judgment-holds (typeof ,M τ) τ)) +(define/contract (type-check M [Σ (term ·)]) + (->* (M?) (any/c) (or/c τ? #f)) + (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) (cond - [(empty? M-t) + [(null? M-ts) #f] - [(null? (cdr M-t)) - (car M-t)] + [(null? (cdr M-ts)) + (car M-ts)] [else - (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) + +;; building an expression out of a store can be done in this model +;; with just topological sort because there are no recursive types, +;; so the store will not contain any cycles +(define (Σ+M->M Σ M) + ;; nodes : edges[r -o> v] + (define nodes (make-hash)) + (define edges (make-hash)) + (let loop ([Σ Σ]) + (match Σ + [`· (void)] + [`(,r ,v ,Σ) + (hash-set! nodes r v) + (loop Σ)])) + + (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) + (for ([(n-src rhs) (in-hash nodes)]) + (for ([(n-dest _) (in-hash nodes)]) + (when (mentions-node? n-dest rhs) + (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) + (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) + edges)) + (let loop ([sorted rev-sorted]) + (cond + [(empty? sorted) M] + [else + (define r (car sorted)) + (term (let ([,r (new ,(hash-ref nodes r))]) + ,(loop (cdr sorted))))]))) + +(define (mentions-node? v r) + (let loop ([v v]) + (cond + [(symbol? v) (equal? r v)] + [(pair? v) (or (loop (car v)) (loop (cdr v)))] + [else #f]))) #| -Random generators +The first algorithm from this page: +http://en.wikipedia.org/wiki/Topological_sorting#Algorithms + +|# +(define/contract (reverse-topo-sort nodes edges) + (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) + + (for ([node (in-list nodes)]) + (unless (hash-ref edges node #f) + (error 'topo-sort "no edge entry for ~s" node))) + + (define incoming-counts (build-incoming-counts nodes edges)) + (define (remove-edge src dest) + (hash-set! edges src (set-remove (hash-ref edges src) dest)) + (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) + + (define l '()) + (define s (for/set ([(n c) (in-hash incoming-counts)] + #:when (zero? c)) + n)) + (let loop () + (unless (set-empty? s) + (define n (set-first s)) + (set! s (set-remove s n)) + (set! l (cons n l)) + (for ([m (in-set (hash-ref edges n))]) + (remove-edge n m) + (when (zero? (hash-ref incoming-counts m)) + (set! s (set-add s m)))) + (loop))) + + l) + +(define (build-incoming-counts nodes edges) + (define incoming-counts (make-hash)) + (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) + (for ([(n neighbors) (in-hash edges)]) + (for ([neighbor (in-set neighbors)]) + (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) + incoming-counts) + + +#| + +Generators |# @@ -487,8 +563,7 @@ from the given term. (implies t-type (let loop ([Σ+M `(· ,M)]) - (define new-type - (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) (let ([red-res (apply-reduction-relation red Σ+M)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt index 8b8459d20f..8d95d50428 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - racket/bool + racket/bool racket/set (only-in "../stlc/tests-lib.rkt" consistent-with?)) (provide (all-defined-out)) @@ -386,8 +386,8 @@ A top-level evaluator (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) - (define M-t (judgment-holds (typeof ,M τ) τ)) - (unless (pair? M-t) + (define M-t (type-check M)) + (unless M-t (error 'Eval "doesn't typecheck: ~s" M)) (define res (apply-reduction-relation* red (term (· ,M)))) (unless (= 1 (length res)) @@ -396,7 +396,7 @@ A top-level evaluator (match (car res) ["error" "error"] [`(,Σ ,N) - (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (define ans-t (type-check N Σ)) (unless (equal? M-t ans-t) (error 'Eval "internal error: type soundness fails for ~s" M)) (match N @@ -411,31 +411,107 @@ A top-level evaluator [(? number?) N] [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) -(define-metafunction stlc - Σ->lets : Σ M -> M - [(Σ->lets · M) M] - [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) - #| -A top-level type checker. +A type checker; the optional argument is a store to use +for type checking free variables in M. |# -(define/contract (type-check M) - (-> M? (or/c τ? #f)) - (define M-t (judgment-holds (typeof ,M τ) τ)) +(define/contract (type-check M [Σ (term ·)]) + (->* (M?) (any/c) (or/c τ? #f)) + (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) (cond - [(empty? M-t) + [(null? M-ts) #f] - [(null? (cdr M-t)) - (car M-t)] + [(null? (cdr M-ts)) + (car M-ts)] [else - (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) + +;; building an expression out of a store can be done in this model +;; with just topological sort because there are no recursive types, +;; so the store will not contain any cycles +(define (Σ+M->M Σ M) + ;; nodes : edges[r -o> v] + (define nodes (make-hash)) + (define edges (make-hash)) + (let loop ([Σ Σ]) + (match Σ + [`· (void)] + [`(,r ,v ,Σ) + (hash-set! nodes r v) + (loop Σ)])) + + (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) + (for ([(n-src rhs) (in-hash nodes)]) + (for ([(n-dest _) (in-hash nodes)]) + (when (mentions-node? n-dest rhs) + (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) + (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) + edges)) + (let loop ([sorted rev-sorted]) + (cond + [(empty? sorted) M] + [else + (define r (car sorted)) + (term (let ([,r (new ,(hash-ref nodes r))]) + ,(loop (cdr sorted))))]))) + +(define (mentions-node? v r) + (let loop ([v v]) + (cond + [(symbol? v) (equal? r v)] + [(pair? v) (or (loop (car v)) (loop (cdr v)))] + [else #f]))) #| -Random generators +The first algorithm from this page: +http://en.wikipedia.org/wiki/Topological_sorting#Algorithms + +|# +(define/contract (reverse-topo-sort nodes edges) + (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) + + (for ([node (in-list nodes)]) + (unless (hash-ref edges node #f) + (error 'topo-sort "no edge entry for ~s" node))) + + (define incoming-counts (build-incoming-counts nodes edges)) + (define (remove-edge src dest) + (hash-set! edges src (set-remove (hash-ref edges src) dest)) + (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) + + (define l '()) + (define s (for/set ([(n c) (in-hash incoming-counts)] + #:when (zero? c)) + n)) + (let loop () + (unless (set-empty? s) + (define n (set-first s)) + (set! s (set-remove s n)) + (set! l (cons n l)) + (for ([m (in-set (hash-ref edges n))]) + (remove-edge n m) + (when (zero? (hash-ref incoming-counts m)) + (set! s (set-add s m)))) + (loop))) + + l) + +(define (build-incoming-counts nodes edges) + (define incoming-counts (make-hash)) + (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) + (for ([(n neighbors) (in-hash edges)]) + (for ([neighbor (in-set neighbors)]) + (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) + incoming-counts) + + +#| + +Generators |# @@ -485,8 +561,7 @@ from the given term. (implies t-type (let loop ([Σ+M `(· ,M)]) - (define new-type - (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) (let ([red-res (apply-reduction-relation red Σ+M)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt index e178eef0be..37209baafb 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt @@ -9,7 +9,7 @@ racket/match racket/list racket/contract - racket/bool + racket/bool racket/set (only-in "../stlc/tests-lib.rkt" consistent-with?)) (provide (all-defined-out)) @@ -387,8 +387,8 @@ A top-level evaluator (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) - (define M-t (judgment-holds (typeof ,M τ) τ)) - (unless (pair? M-t) + (define M-t (type-check M)) + (unless M-t (error 'Eval "doesn't typecheck: ~s" M)) (define res (apply-reduction-relation* red (term (· ,M)))) (unless (= 1 (length res)) @@ -397,7 +397,7 @@ A top-level evaluator (match (car res) ["error" "error"] [`(,Σ ,N) - (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (define ans-t (type-check N Σ)) (unless (equal? M-t ans-t) (error 'Eval "internal error: type soundness fails for ~s" M)) (match N @@ -412,31 +412,107 @@ A top-level evaluator [(? number?) N] [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) -(define-metafunction stlc - Σ->lets : Σ M -> M - [(Σ->lets · M) M] - [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) - #| -A top-level type checker. +A type checker; the optional argument is a store to use +for type checking free variables in M. |# -(define/contract (type-check M) - (-> M? (or/c τ? #f)) - (define M-t (judgment-holds (typeof ,M τ) τ)) +(define/contract (type-check M [Σ (term ·)]) + (->* (M?) (any/c) (or/c τ? #f)) + (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) (cond - [(empty? M-t) + [(null? M-ts) #f] - [(null? (cdr M-t)) - (car M-t)] + [(null? (cdr M-ts)) + (car M-ts)] [else - (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) + +;; building an expression out of a store can be done in this model +;; with just topological sort because there are no recursive types, +;; so the store will not contain any cycles +(define (Σ+M->M Σ M) + ;; nodes : edges[r -o> v] + (define nodes (make-hash)) + (define edges (make-hash)) + (let loop ([Σ Σ]) + (match Σ + [`· (void)] + [`(,r ,v ,Σ) + (hash-set! nodes r v) + (loop Σ)])) + + (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) + (for ([(n-src rhs) (in-hash nodes)]) + (for ([(n-dest _) (in-hash nodes)]) + (when (mentions-node? n-dest rhs) + (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) + (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) + edges)) + (let loop ([sorted rev-sorted]) + (cond + [(empty? sorted) M] + [else + (define r (car sorted)) + (term (let ([,r (new ,(hash-ref nodes r))]) + ,(loop (cdr sorted))))]))) + +(define (mentions-node? v r) + (let loop ([v v]) + (cond + [(symbol? v) (equal? r v)] + [(pair? v) (or (loop (car v)) (loop (cdr v)))] + [else #f]))) #| -Random generators +The first algorithm from this page: +http://en.wikipedia.org/wiki/Topological_sorting#Algorithms + +|# +(define/contract (reverse-topo-sort nodes edges) + (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) + + (for ([node (in-list nodes)]) + (unless (hash-ref edges node #f) + (error 'topo-sort "no edge entry for ~s" node))) + + (define incoming-counts (build-incoming-counts nodes edges)) + (define (remove-edge src dest) + (hash-set! edges src (set-remove (hash-ref edges src) dest)) + (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) + + (define l '()) + (define s (for/set ([(n c) (in-hash incoming-counts)] + #:when (zero? c)) + n)) + (let loop () + (unless (set-empty? s) + (define n (set-first s)) + (set! s (set-remove s n)) + (set! l (cons n l)) + (for ([m (in-set (hash-ref edges n))]) + (remove-edge n m) + (when (zero? (hash-ref incoming-counts m)) + (set! s (set-add s m)))) + (loop))) + + l) + +(define (build-incoming-counts nodes edges) + (define incoming-counts (make-hash)) + (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) + (for ([(n neighbors) (in-hash edges)]) + (for ([neighbor (in-set neighbors)]) + (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) + incoming-counts) + + +#| + +Generators |# @@ -486,8 +562,7 @@ from the given term. (implies t-type (let loop ([Σ+M `(· ,M)]) - (define new-type - (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) (let ([red-res (apply-reduction-relation red Σ+M)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt index 2a46f75537..7c4de66bb2 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt @@ -7,7 +7,7 @@ racket/match racket/list racket/contract - racket/bool + racket/bool racket/set (only-in "../stlc/tests-lib.rkt" consistent-with?)) (provide (all-defined-out)) @@ -386,8 +386,8 @@ A top-level evaluator (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) - (define M-t (judgment-holds (typeof ,M τ) τ)) - (unless (pair? M-t) + (define M-t (type-check M)) + (unless M-t (error 'Eval "doesn't typecheck: ~s" M)) (define res (apply-reduction-relation* red (term (· ,M)))) (unless (= 1 (length res)) @@ -396,7 +396,7 @@ A top-level evaluator (match (car res) ["error" "error"] [`(,Σ ,N) - (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (define ans-t (type-check N Σ)) (unless (equal? M-t ans-t) (error 'Eval "internal error: type soundness fails for ~s" M)) (match N @@ -411,31 +411,107 @@ A top-level evaluator [(? number?) N] [_ (error 'Eval "internal error: didn't reduce to a value ~s" M)])])) -(define-metafunction stlc - Σ->lets : Σ M -> M - [(Σ->lets · M) M] - [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) - #| -A top-level type checker. +A type checker; the optional argument is a store to use +for type checking free variables in M. |# -(define/contract (type-check M) - (-> M? (or/c τ? #f)) - (define M-t (judgment-holds (typeof ,M τ) τ)) +(define/contract (type-check M [Σ (term ·)]) + (->* (M?) (any/c) (or/c τ? #f)) + (define M-ts (judgment-holds (typeof ,(Σ+M->M Σ M) τ) τ)) (cond - [(empty? M-t) + [(null? M-ts) #f] - [(null? (cdr M-t)) - (car M-t)] + [(null? (cdr M-ts)) + (car M-ts)] [else - (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + (error 'type-check "non-unique type: ~s : ~s" M M-ts)])) + +;; building an expression out of a store can be done in this model +;; with just topological sort because there are no recursive types, +;; so the store will not contain any cycles +(define (Σ+M->M Σ M) + ;; nodes : edges[r -o> v] + (define nodes (make-hash)) + (define edges (make-hash)) + (let loop ([Σ Σ]) + (match Σ + [`· (void)] + [`(,r ,v ,Σ) + (hash-set! nodes r v) + (loop Σ)])) + + (for ([(n rhs) (in-hash nodes)]) (hash-set! edges n (set))) + (for ([(n-src rhs) (in-hash nodes)]) + (for ([(n-dest _) (in-hash nodes)]) + (when (mentions-node? n-dest rhs) + (hash-set! edges n-src (set-add (hash-ref edges n-src) n-dest))))) + (define rev-sorted (reverse-topo-sort (for/list ([(k v) (in-hash nodes)]) k) + edges)) + (let loop ([sorted rev-sorted]) + (cond + [(empty? sorted) M] + [else + (define r (car sorted)) + (term (let ([,r (new ,(hash-ref nodes r))]) + ,(loop (cdr sorted))))]))) + +(define (mentions-node? v r) + (let loop ([v v]) + (cond + [(symbol? v) (equal? r v)] + [(pair? v) (or (loop (car v)) (loop (cdr v)))] + [else #f]))) #| -Random generators +The first algorithm from this page: +http://en.wikipedia.org/wiki/Topological_sorting#Algorithms + +|# +(define/contract (reverse-topo-sort nodes edges) + (-> (listof any/c) (hash/c any/c (set/c any/c)) (listof any/c)) + + (for ([node (in-list nodes)]) + (unless (hash-ref edges node #f) + (error 'topo-sort "no edge entry for ~s" node))) + + (define incoming-counts (build-incoming-counts nodes edges)) + (define (remove-edge src dest) + (hash-set! edges src (set-remove (hash-ref edges src) dest)) + (hash-set! incoming-counts dest (- (hash-ref incoming-counts dest) 1))) + + (define l '()) + (define s (for/set ([(n c) (in-hash incoming-counts)] + #:when (zero? c)) + n)) + (let loop () + (unless (set-empty? s) + (define n (set-first s)) + (set! s (set-remove s n)) + (set! l (cons n l)) + (for ([m (in-set (hash-ref edges n))]) + (remove-edge n m) + (when (zero? (hash-ref incoming-counts m)) + (set! s (set-add s m)))) + (loop))) + + l) + +(define (build-incoming-counts nodes edges) + (define incoming-counts (make-hash)) + (for ([n (in-list nodes)]) (hash-set! incoming-counts n 0)) + (for ([(n neighbors) (in-hash edges)]) + (for ([neighbor (in-set neighbors)]) + (hash-set! incoming-counts neighbor (+ (hash-ref incoming-counts neighbor) 1)))) + incoming-counts) + + +#| + +Generators |# @@ -485,8 +561,7 @@ from the given term. (implies t-type (let loop ([Σ+M `(· ,M)]) - (define new-type - (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (define new-type (type-check (list-ref Σ+M 1) (list-ref Σ+M 0))) (and (consistent-with? t-type new-type) (or (v? (list-ref Σ+M 1)) (let ([red-res (apply-reduction-relation red Σ+M)]) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt index a5a1e7a0fc..30ed1ecbaa 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt @@ -1,7 +1,51 @@ #lang racket/base (require "let-poly-base.rkt" (only-in "../stlc/tests-lib.rkt" consistent-with?) - redex/reduction-semantics) + redex/reduction-semantics + racket/set) + +(test-equal (build-incoming-counts '(x y z) + (make-hash (list (cons 'x (set 'y 'z)) + (cons 'y (set 'z)) + (cons 'z (set))))) + (make-hash (list (cons 'x 0) + (cons 'y 1) + (cons 'z 2)))) +(test-equal (reverse-topo-sort '() (make-hash)) '()) +(test-equal (reverse-topo-sort '(x) + (make-hash (list (cons 'x (set))))) + '(x)) +(test-equal (reverse-topo-sort '(x y) + (make-hash (list (cons 'y (set)) + (cons 'x (set 'y))))) + '(y x)) +(test-equal (reverse-topo-sort '(y x) + (make-hash (list (cons 'y (set)) + (cons 'x (set 'y))))) + '(y x)) +(test-equal (reverse-topo-sort '(x y z) + (make-hash (list (cons 'x (set 'y)) + (cons 'y (set 'z)) + (cons 'z (set))))) + '(z y x)) +(test-equal (reverse-topo-sort '(x y z) + (make-hash (list (cons 'x (set 'y 'z)) + (cons 'y (set 'z)) + (cons 'z (set))))) + '(z y x)) +(define (one-of? a . bs) (for/or ([b (in-list bs)]) (equal? a b))) +(test-equal (one-of? (reverse-topo-sort '(x y z) + (make-hash (list (cons 'x (set 'z)) + (cons 'y (set 'z)) + (cons 'z (set))))) + '(z x y) + '(z y x)) + #t) + +(test-equal (Σ+M->M (term (r1 r2 (r2 1 ·))) (term 2)) + (term (let ([r2 (new 1)]) (let ([r1 (new r2)]) 2)))) +(test-equal (Σ+M->M (term (r2 1 (r1 r2 ·))) (term 2)) + (term (let ([r2 (new 1)]) (let ([r1 (new r2)]) 2)))) (test-equal (term (subst ((+ 1) 1) x 2)) (term ((+ 1) 1))) @@ -192,3 +236,10 @@ (term int)) (test-equal (type-check (term (5 5))) #f) +(test-equal (type-check (term r1) (term (r1 r (r 1 ·)))) + (term (ref (ref int)))) +(test-equal (type-check (term r1) (term (r 1 (r1 r ·)))) + (term (ref (ref int)))) + +(test-equal (check (term 1)) #t) +(test-equal (check (term (new (new hd)))) #t)