From 09e6f7178dbb15fa04c1649eb2e5af504e790c8f Mon Sep 17 00:00:00 2001 From: Robby Findler Date: Sat, 29 Mar 2014 13:54:55 -0500 Subject: [PATCH] Add in let-poly bugs also, misc clean ups of let-poly --- .../redex/examples/benchmark/apply-diffs.rkt | 1 + .../redex/examples/benchmark/let-poly/1.diff | 12 + .../redex/examples/benchmark/let-poly/2.diff | 25 + .../redex/examples/benchmark/let-poly/3.diff | 13 + .../redex/examples/benchmark/let-poly/4.diff | 14 + .../redex/examples/benchmark/let-poly/5.diff | 18 + .../redex/examples/benchmark/let-poly/6.diff | 14 + .../redex/examples/benchmark/let-poly/7.diff | 21 + .../benchmark/let-poly/let-poly-1.rkt | 499 +++++++++++++++++ .../benchmark/let-poly/let-poly-2.rkt | 497 +++++++++++++++++ .../benchmark/let-poly/let-poly-3.rkt | 500 +++++++++++++++++ .../benchmark/let-poly/let-poly-4.rkt | 501 ++++++++++++++++++ .../let-poly-5.rkt} | 227 ++++---- .../benchmark/let-poly/let-poly-6.rkt | 501 ++++++++++++++++++ .../benchmark/let-poly/let-poly-7.rkt | 500 +++++++++++++++++ .../benchmark/let-poly/let-poly-base.rkt | 496 +++++++++++++++++ .../{let-poly-stlc => let-poly}/tests.rkt | 7 +- .../examples/benchmark/stlc/tests-lib.rkt | 16 +- 18 files changed, 3745 insertions(+), 117 deletions(-) create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt rename pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/{let-poly-stlc/let-poly-stlc-base.rkt => let-poly/let-poly-5.rkt} (79%) create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt create mode 100644 pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt rename pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/{let-poly-stlc => let-poly}/tests.rkt (97%) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/apply-diffs.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/apply-diffs.rkt index 6bdbf5858e..20db42793a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/apply-diffs.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/apply-diffs.rkt @@ -11,6 +11,7 @@ (define directories (list "stlc" "stlc-sub" "poly-stlc" + "let-poly" "rbtrees" "delim-cont" "list-machine" 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 new file mode 100644 index 0000000000..19bc9a83d1 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/1.diff @@ -0,0 +1,12 @@ +3c3 +< (define the-error "no error") +--- +> (define the-error "use a lambda-bound variable where a type variable should have been") +106c106 +< (tc-down (x y Γ) M (λ y κ) σ_ans) +--- +> (tc-down (x y Γ) M (λ x κ) σ_ans) +496a497,499 +> +> (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 new file mode 100644 index 0000000000..6c2cab5500 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/2.diff @@ -0,0 +1,25 @@ +3c3 +< (define the-error "no error") +--- +> (define the-error "the classic polymorphic let + references bug") +114c114 +< [(where N_2 (subst N x v)) +--- +> [(where N_2 (subst N x M)) +116c116 +< (tc-down Γ ((λ y N_2) v) κ σ_2) +--- +> (tc-down Γ ((λ y N_2) M) κ σ_2) +118,122d117 +< (tc-down Γ (let ([x v]) N) κ σ_2)] +< +< [(where #t (not-v? M)) +< (tc-down Γ ((λ x N) M) κ σ_2) +< --------------------------------- +496a492,497 +> +> (define small-counter-example '(let ([x (new nil)]) +> ((λ ignore +> ((hd (get x)) 1)) +> ((set x) ((cons 5) nil))))) +> (test-equal (check small-counter-example) #f) 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 new file mode 100644 index 0000000000..d5f9a34a98 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/3.diff @@ -0,0 +1,13 @@ +3c3 +< (define the-error "no error") +--- +> (define the-error "mix up types in the function case") +137c137 +< (where G (unify τ_2 (τ_1 → x))) +--- +> (where G (unify τ_1 (τ_2 → x))) +496a497,500 +> +> +> (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 new file mode 100644 index 0000000000..2316c01255 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/4.diff @@ -0,0 +1,14 @@ +3c3,5 +< (define the-error "no error") +--- +> (define the-error +> (string-append "misspelled the name of a metafunction in a side-condition, " +> "causing the occurs check to not happen")) +212c214 +< [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] +--- +> [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))] +496a499,501 +> +> (define small-counter-example (term ((λ x (x x)) (λ x x)))) +> (check-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 new file mode 100644 index 0000000000..7c7f60f7c5 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/5.diff @@ -0,0 +1,18 @@ +3c3 +< (define the-error "no error") +--- +> (define the-error "eliminate-G was written as if it always gets a Gx as input") +225,226c225,228 +< [(eliminate-G x τ (σ_1 σ_2 G)) +< ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) +--- +> [(eliminate-G x τ (x σ G)) +> (τ (eliminate-τ x τ σ) (eliminate-G x τ G))] +> [(eliminate-G x τ (y σ G)) +> (y (eliminate-τ x τ σ) (eliminate-G x τ G))]) +496a499,503 +> +> (define small-counter-example (term (cons 1))) +> (test-equal (with-handlers ([exn:fail? (λ (x) #f)]) +> (check small-counter-example)) +> #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 new file mode 100644 index 0000000000..baf68a6e9c --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/6.diff @@ -0,0 +1,14 @@ +3c3 +< (define the-error "no error") +--- +> (define the-error "∨ has an incorrect duplicated variable, leading to an uncovered case") +240c240 +< [(∨ boolean_1 boolean_2) #t]) +--- +> [(∨ boolean boolean) #t]) +496a497,501 +> +> (define small-counter-example (term ((λ x x) 1))) +> (test-equal (with-handlers ([exn:fail? (λ (x) #f)]) +> (check small-counter-example)) +> #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 new file mode 100644 index 0000000000..eb70a91977 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/7.diff @@ -0,0 +1,21 @@ +3c3,5 +< (define the-error "no error") +--- +> (define the-error +> (string-append "used let --> left-left-λ rewrite rule for let, " +> "but the right-hand side is less polymorphic")) +44,45c46 +< (v E) +< (let ([x E]) M)) +--- +> (v E)) +306,307c307,308 +< (--> (Σ (in-hole E (let ([x v]) M))) +< (Σ (in-hole E (subst M x v))) +--- +> (--> (Σ (in-hole E (let ([x M]) N))) +> (Σ (in-hole E ((λ x N) M))) +496a498,500 +> +> (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 new file mode 100644 index 0000000000..4cdf49b60c --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-1.rkt @@ -0,0 +1,499 @@ +#lang racket/base + +(define the-error "use a lambda-bound variable where a type variable should have been") + +(require redex/reduction-semantics + (only-in redex/private/generate-term pick-an-index) + racket/match + racket/list + racket/contract + racket/bool + (only-in "../stlc/tests-lib.rkt" consistent-with?)) + +(provide (all-defined-out)) + +(define-language stlc + (M N ::= + (λ x M) + (M N) + x + c + (let ([x M]) N)) + (Γ (x σ Γ) + ·) + (σ τ ::= + int + (σ → τ) + (list τ) + (ref τ) + x) + (c d ::= c0 c1) + (c0 ::= + integer) + (c1 ::= cons nil hd tl new get set) + (x y r ::= variable-not-otherwise-mentioned) + + (v (λ x M) + c + ((cons v) v) + (cons v) + (+ v) + (set v) + r) + (E hole + (E M) + (v E) + (let ([x E]) M)) + (Σ ::= · (r v Σ)) + + (κ ::= + · + (λ τ κ) + (1 Γ M κ) + (2 τ κ)) + + (G ::= · (τ σ G)) + (Gx ::= · (x σ Gx))) + +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) +(define x? (redex-match? stlc x)) +(define M? (redex-match? stlc M)) +(define Σ-M? (redex-match? stlc (Σ M))) + +#| + +The typing judgment has no rule with multiple +(self-referential) premises. Instead, it explicitly +manipulates a continuation so that it can, when it +discovers a type equality, simply do the substitution +through the continuation. This also makes it possible +to easily generate fresh variables by picking ones +that aren't in the expression or the continuation. + +The 'tc-down' rules recur thru the term to find a type +of the left-most subexpression and the 'tc-up' rules +bring that type back, recurring on the continuation. + +|# + +(define-judgment-form stlc + #:mode (typeof I O) + #:contract (typeof M σ) + + [(tc-down · M · σ) + ------------- + (typeof M σ)]) + +(define-judgment-form stlc + #:mode (tc-down I I I O) + #:contract (tc-down Γ M κ σ) + + [(tc-up (const-type0 c0) κ σ_ans) + ------------------------------ + (tc-down Γ c0 κ σ_ans)] + + [(where x ,(variable-not-in (term (Γ κ)) 'γ)) + (tc-up (const-type1 x c1) κ σ_ans) + ------------------------------ + (tc-down Γ c1 κ σ_ans)] + + [(where τ (lookup-Γ Γ x)) + (tc-up τ κ σ_ans) + --------------------------- + (tc-down Γ x κ σ_ans)] + + [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) + (tc-down (x y Γ) M (λ x κ) σ_ans) + ------------------------------------------------ + (tc-down Γ (λ x M) κ σ_ans)] + + [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2) + -------------------------- + (tc-down Γ (M_1 M_2) κ σ_2)] + + [(where N_2 (subst N x v)) + (where y ,(variable-not-in (term N_2) 'l)) + (tc-down Γ ((λ y N_2) v) κ σ_2) + ------------------------------------------ + (tc-down Γ (let ([x v]) N) κ σ_2)] + + [(where #t (not-v? M)) + (tc-down Γ ((λ x N) M) κ σ_2) + --------------------------------- + (tc-down Γ (let ([x M]) N) κ σ_2)]) + +(define-judgment-form stlc + #:mode (tc-up I I O) + #:contract (tc-up τ κ σ) + + [--------------------- + (tc-up σ_ans · σ_ans)] + + [(tc-down Γ M (2 τ κ) σ_ans) + --------------------------- + (tc-up τ (1 Γ M κ) σ_ans)] + + [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) + (where G (unify τ_2 (τ_1 → x))) + (tc-up (apply-subst-τ G x) + (apply-subst-κ G κ) + σ_ans) + --------------------------------------------------- + (tc-up τ_1 (2 τ_2 κ) σ_ans)] + + [(tc-up (τ_1 → τ_2) κ σ_ans) + --------------------------- + (tc-up τ_2 (λ τ_1 κ) σ_ans)]) + +(define-metafunction stlc + const-type0 : c0 -> σ + [(const-type0 +) (int → (int → int))] + [(const-type0 integer) int]) + +(define-metafunction stlc + const-type1 : x c1 -> σ + [(const-type1 x nil) (list x)] + [(const-type1 x cons) (x → ((list x) → (list x)))] + [(const-type1 x hd) ((list x) → x)] + [(const-type1 x tl) ((list x) → (list x))] + [(const-type1 x new) (x → (ref x))] + [(const-type1 x get) ((ref x) → x)] + [(const-type1 x set) ((ref x) → (x → x))]) + +(define-metafunction stlc + lookup-Γ : Γ x -> σ or #f + [(lookup-Γ (x σ Γ) x) σ] + [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] + [(lookup-Γ · x) #f]) + +(define-metafunction stlc + unify : τ τ -> Gx or ⊥ + [(unify τ σ) (uh (τ σ ·) · #f)]) + +#| + +Algorithm copied from _An Efficient Unification Algorithm_ by +Alberto Martelli and Ugo Montanari (section 2). +http://www.nsl.com/misc/papers/martelli-montanari.pdf + +This isn't the eponymous algorithm; it is an earlier one +in the paper that's simpler. + +The 'uh' function iterates over a set of equations applying the +rules from the paper, moving them from the first argument to +the second argument and tracking when something changes. +It runs until there are no more changes. The (a), (b), +(c), and (d) are the rule labels from the paper. + +|# + +(define-metafunction stlc + uh : G G boolean -> Gx or ⊥ + + [(uh · G #t) (uh G · #f)] + [(uh · G #f) G] + + ;; (a) + [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))] + + ;; (b) + [(uh (x x G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- term reduction + [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)] + [(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh (int int G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- failure + [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))] + + ;; (d) -- x occurs in τ case + [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] + + ;; (d) -- x does not occur in τ case + [(uh (x τ G) G_r boolean) + (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t) + (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))] + + ;; no rules applied; try next equation, if any. + [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)]) + +(define-metafunction stlc + eliminate-G : x τ G -> G + [(eliminate-G x τ ·) ·] + [(eliminate-G x τ (σ_1 σ_2 G)) + ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) + +(define-metafunction stlc + eliminate-τ : x τ σ -> σ + [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))] + [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))] + [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))] + [(eliminate-τ x τ int) int] + [(eliminate-τ x τ x) τ] + [(eliminate-τ x τ y) y]) + +(define-metafunction stlc + ∨ : boolean boolean -> boolean + [(∨ #f #f) #f] + [(∨ boolean_1 boolean_2) #t]) + +(define-metafunction stlc + not-var? : τ -> boolean + [(not-var? x) #f] + [(not-var? τ) #t]) + +(define-metafunction stlc + in-vars-τ? : x τ -> boolean + [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))] + [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x int) #f] + [(in-vars-τ? x x) #t] + [(in-vars-τ? x y) #f]) + +(define-metafunction stlc + in-vars-G? : x G -> boolean + [(in-vars-G? x ·) #f] + [(in-vars-G? x (x τ G)) #t] + [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) + (∨ (in-vars-τ? x τ) + (in-vars-G? x G)))]) + +(define-metafunction stlc + apply-subst-τ : Gx τ -> τ + [(apply-subst-τ · τ) τ] + [(apply-subst-τ (x τ G) σ) + (apply-subst-τ G (eliminate-τ x τ σ))]) + +(define-metafunction stlc + apply-subst-κ : Gx κ -> κ + [(apply-subst-κ Gx ·) ·] + [(apply-subst-κ Gx (λ σ κ)) + (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (1 Γ M κ)) + (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (2 σ κ)) + (2 (apply-subst-τ Gx σ) + (apply-subst-κ Gx κ))]) + +(define-metafunction stlc + apply-subst-Γ : Gx Γ -> Γ + [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] + [(apply-subst-Γ Gx ·) ·]) + +(define-metafunction stlc + not-v? : M -> boolean + [(not-v? v) #f] + [(not-v? M) #t]) + +#| + +The reduction relation rewrites a pair of +a store and an expression to a new store +and a new expression or into the string + "error" (for hd and tl of the empty list) + +|# + +(define red + (reduction-relation + stlc + (--> (Σ (in-hole E ((λ x M) v))) + (Σ (in-hole E (subst M x v))) + "βv") + (--> (Σ (in-hole E (let ([x v]) M))) + (Σ (in-hole E (subst M x v))) + "let") + (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) + (Σ (in-hole E v_1)) + "hd") + (--> (Σ (in-hole E (tl ((cons v_1) v_2)))) + (Σ (in-hole E v_2)) + "tl") + (--> (Σ (in-hole E (hd nil))) + "error" + "hd-err") + (--> (Σ (in-hole E (tl nil))) + "error" + "tl-err") + (--> (Σ (in-hole E ((+ integer_1) integer_2))) + (Σ (in-hole E ,(+ (term integer_1) (term integer_2)))) + "+") + (--> (Σ (in-hole E (new v))) + ((r v Σ) (in-hole E r)) + (fresh r) + "ref") + (--> (Σ (in-hole E ((set x) v))) + ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x))) + "set") + (--> (Σ (in-hole E (get x))) + (Σ (in-hole E (lookup-Σ Σ x))) + "get"))) + +#| + +Capture avoiding substitution + +|# + + +(define-metafunction stlc + subst : M x M -> M + [(subst x x M_x) + M_x] + [(subst (λ x M) x M_x) + (λ x M)] + [(subst (let ([x M]) N) x M_x) + (let ([x (subst M x M_x)]) N)] + [(subst (λ y M) x M_x) + (λ x_new (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (let ([y N]) M) x M_x) + (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (M N) x M_x) + ((subst M x M_x) (subst N x M_x))] + [(subst M x M_z) + M]) + +(define-metafunction stlc + [(replace (any_1 ...) x_1 x_new) + ((replace any_1 x_1 x_new) ...)] + [(replace x_1 x_1 x_new) + x_new] + [(replace any_1 x_1 x_new) + any_1]) + +(define-metafunction stlc + lookup-Σ : Σ x -> v + [(lookup-Σ (x v Σ) x) v] + [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)]) + +(define-metafunction stlc + update-Σ : Σ x v -> Σ + [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] + [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) + +#| + +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) + (error 'Eval "doesn't typecheck: ~s" M)) + (define res (apply-reduction-relation* red (term (· ,M)))) + (unless (= 1 (length res)) + (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) + (define ans (car res)) + (match (car res) + ["error" "error"] + [`(,Σ ,N) + (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (unless (equal? M-t ans-t) + (error 'Eval "internal error: type soundness fails for ~s" M)) + (match N + [(? x?) (cond + [(term (in-dom? ,Σ ,N)) + 'ref] + [else + (error 'Eval "internal error: reduced to a free variable ~s" + M)])] + [(or `((cons ,_) ,_) `nil) 'list] + [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ] + [(? 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. + +|# + +(define/contract (type-check M) + (-> M? (or/c τ? #f)) + (define M-t (judgment-holds (typeof ,M τ) τ)) + (cond + [(empty? M-t) + #f] + [(null? (cdr M-t)) + (car M-t)] + [else + (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + +#| + +Random generators + +|# + +(define (generate-M-term) + (generate-term stlc M 5)) + +(define (generate-typed-term) + (match (generate-term stlc + #:satisfying + (typeof M τ) + 5) + [`(typeof ,M ,τ) + M] + [#f #f])) + +(define (typed-generator) + (let ([g (redex-generator stlc + (typeof M τ) + 5)]) + (λ () + (match (g) + [`(typeof ,M ,τ) + M] + [#f #f])))) + +(define (generate-enum-term) + (generate-term stlc M #:i-th (pick-an-index 0.035))) + +(define (ordered-enum-generator) + (let ([index 0]) + (λ () + (begin0 + (generate-term stlc M #:i-th index) + (set! index (add1 index)))))) + +#| + +Check to see if a combination of preservation +and progress holds for every single term reachable +from the given term. + +|# + +(define (check M) + (or (not M) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (define new-type + (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (and (consistent-with? t-type new-type) + (or (v? (list-ref Σ+M 1)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t)))))))))))) + +(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/let-poly-2.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt new file mode 100644 index 0000000000..cb845886ea --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-2.rkt @@ -0,0 +1,497 @@ +#lang racket/base + +(define the-error "the classic polymorphic let + references bug") + +(require redex/reduction-semantics + (only-in redex/private/generate-term pick-an-index) + racket/match + racket/list + racket/contract + racket/bool + (only-in "../stlc/tests-lib.rkt" consistent-with?)) + +(provide (all-defined-out)) + +(define-language stlc + (M N ::= + (λ x M) + (M N) + x + c + (let ([x M]) N)) + (Γ (x σ Γ) + ·) + (σ τ ::= + int + (σ → τ) + (list τ) + (ref τ) + x) + (c d ::= c0 c1) + (c0 ::= + integer) + (c1 ::= cons nil hd tl new get set) + (x y r ::= variable-not-otherwise-mentioned) + + (v (λ x M) + c + ((cons v) v) + (cons v) + (+ v) + (set v) + r) + (E hole + (E M) + (v E) + (let ([x E]) M)) + (Σ ::= · (r v Σ)) + + (κ ::= + · + (λ τ κ) + (1 Γ M κ) + (2 τ κ)) + + (G ::= · (τ σ G)) + (Gx ::= · (x σ Gx))) + +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) +(define x? (redex-match? stlc x)) +(define M? (redex-match? stlc M)) +(define Σ-M? (redex-match? stlc (Σ M))) + +#| + +The typing judgment has no rule with multiple +(self-referential) premises. Instead, it explicitly +manipulates a continuation so that it can, when it +discovers a type equality, simply do the substitution +through the continuation. This also makes it possible +to easily generate fresh variables by picking ones +that aren't in the expression or the continuation. + +The 'tc-down' rules recur thru the term to find a type +of the left-most subexpression and the 'tc-up' rules +bring that type back, recurring on the continuation. + +|# + +(define-judgment-form stlc + #:mode (typeof I O) + #:contract (typeof M σ) + + [(tc-down · M · σ) + ------------- + (typeof M σ)]) + +(define-judgment-form stlc + #:mode (tc-down I I I O) + #:contract (tc-down Γ M κ σ) + + [(tc-up (const-type0 c0) κ σ_ans) + ------------------------------ + (tc-down Γ c0 κ σ_ans)] + + [(where x ,(variable-not-in (term (Γ κ)) 'γ)) + (tc-up (const-type1 x c1) κ σ_ans) + ------------------------------ + (tc-down Γ c1 κ σ_ans)] + + [(where τ (lookup-Γ Γ x)) + (tc-up τ κ σ_ans) + --------------------------- + (tc-down Γ x κ σ_ans)] + + [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) + (tc-down (x y Γ) M (λ y κ) σ_ans) + ------------------------------------------------ + (tc-down Γ (λ x M) κ σ_ans)] + + [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2) + -------------------------- + (tc-down Γ (M_1 M_2) κ σ_2)] + + [(where N_2 (subst N x M)) + (where y ,(variable-not-in (term N_2) 'l)) + (tc-down Γ ((λ y N_2) M) κ σ_2) + ------------------------------------------ + (tc-down Γ (let ([x M]) N) κ σ_2)]) + +(define-judgment-form stlc + #:mode (tc-up I I O) + #:contract (tc-up τ κ σ) + + [--------------------- + (tc-up σ_ans · σ_ans)] + + [(tc-down Γ M (2 τ κ) σ_ans) + --------------------------- + (tc-up τ (1 Γ M κ) σ_ans)] + + [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) + (where G (unify τ_2 (τ_1 → x))) + (tc-up (apply-subst-τ G x) + (apply-subst-κ G κ) + σ_ans) + --------------------------------------------------- + (tc-up τ_1 (2 τ_2 κ) σ_ans)] + + [(tc-up (τ_1 → τ_2) κ σ_ans) + --------------------------- + (tc-up τ_2 (λ τ_1 κ) σ_ans)]) + +(define-metafunction stlc + const-type0 : c0 -> σ + [(const-type0 +) (int → (int → int))] + [(const-type0 integer) int]) + +(define-metafunction stlc + const-type1 : x c1 -> σ + [(const-type1 x nil) (list x)] + [(const-type1 x cons) (x → ((list x) → (list x)))] + [(const-type1 x hd) ((list x) → x)] + [(const-type1 x tl) ((list x) → (list x))] + [(const-type1 x new) (x → (ref x))] + [(const-type1 x get) ((ref x) → x)] + [(const-type1 x set) ((ref x) → (x → x))]) + +(define-metafunction stlc + lookup-Γ : Γ x -> σ or #f + [(lookup-Γ (x σ Γ) x) σ] + [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] + [(lookup-Γ · x) #f]) + +(define-metafunction stlc + unify : τ τ -> Gx or ⊥ + [(unify τ σ) (uh (τ σ ·) · #f)]) + +#| + +Algorithm copied from _An Efficient Unification Algorithm_ by +Alberto Martelli and Ugo Montanari (section 2). +http://www.nsl.com/misc/papers/martelli-montanari.pdf + +This isn't the eponymous algorithm; it is an earlier one +in the paper that's simpler. + +The 'uh' function iterates over a set of equations applying the +rules from the paper, moving them from the first argument to +the second argument and tracking when something changes. +It runs until there are no more changes. The (a), (b), +(c), and (d) are the rule labels from the paper. + +|# + +(define-metafunction stlc + uh : G G boolean -> Gx or ⊥ + + [(uh · G #t) (uh G · #f)] + [(uh · G #f) G] + + ;; (a) + [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))] + + ;; (b) + [(uh (x x G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- term reduction + [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)] + [(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh (int int G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- failure + [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))] + + ;; (d) -- x occurs in τ case + [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] + + ;; (d) -- x does not occur in τ case + [(uh (x τ G) G_r boolean) + (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t) + (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))] + + ;; no rules applied; try next equation, if any. + [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)]) + +(define-metafunction stlc + eliminate-G : x τ G -> G + [(eliminate-G x τ ·) ·] + [(eliminate-G x τ (σ_1 σ_2 G)) + ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) + +(define-metafunction stlc + eliminate-τ : x τ σ -> σ + [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))] + [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))] + [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))] + [(eliminate-τ x τ int) int] + [(eliminate-τ x τ x) τ] + [(eliminate-τ x τ y) y]) + +(define-metafunction stlc + ∨ : boolean boolean -> boolean + [(∨ #f #f) #f] + [(∨ boolean_1 boolean_2) #t]) + +(define-metafunction stlc + not-var? : τ -> boolean + [(not-var? x) #f] + [(not-var? τ) #t]) + +(define-metafunction stlc + in-vars-τ? : x τ -> boolean + [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))] + [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x int) #f] + [(in-vars-τ? x x) #t] + [(in-vars-τ? x y) #f]) + +(define-metafunction stlc + in-vars-G? : x G -> boolean + [(in-vars-G? x ·) #f] + [(in-vars-G? x (x τ G)) #t] + [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) + (∨ (in-vars-τ? x τ) + (in-vars-G? x G)))]) + +(define-metafunction stlc + apply-subst-τ : Gx τ -> τ + [(apply-subst-τ · τ) τ] + [(apply-subst-τ (x τ G) σ) + (apply-subst-τ G (eliminate-τ x τ σ))]) + +(define-metafunction stlc + apply-subst-κ : Gx κ -> κ + [(apply-subst-κ Gx ·) ·] + [(apply-subst-κ Gx (λ σ κ)) + (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (1 Γ M κ)) + (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (2 σ κ)) + (2 (apply-subst-τ Gx σ) + (apply-subst-κ Gx κ))]) + +(define-metafunction stlc + apply-subst-Γ : Gx Γ -> Γ + [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] + [(apply-subst-Γ Gx ·) ·]) + +(define-metafunction stlc + not-v? : M -> boolean + [(not-v? v) #f] + [(not-v? M) #t]) + +#| + +The reduction relation rewrites a pair of +a store and an expression to a new store +and a new expression or into the string + "error" (for hd and tl of the empty list) + +|# + +(define red + (reduction-relation + stlc + (--> (Σ (in-hole E ((λ x M) v))) + (Σ (in-hole E (subst M x v))) + "βv") + (--> (Σ (in-hole E (let ([x v]) M))) + (Σ (in-hole E (subst M x v))) + "let") + (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) + (Σ (in-hole E v_1)) + "hd") + (--> (Σ (in-hole E (tl ((cons v_1) v_2)))) + (Σ (in-hole E v_2)) + "tl") + (--> (Σ (in-hole E (hd nil))) + "error" + "hd-err") + (--> (Σ (in-hole E (tl nil))) + "error" + "tl-err") + (--> (Σ (in-hole E ((+ integer_1) integer_2))) + (Σ (in-hole E ,(+ (term integer_1) (term integer_2)))) + "+") + (--> (Σ (in-hole E (new v))) + ((r v Σ) (in-hole E r)) + (fresh r) + "ref") + (--> (Σ (in-hole E ((set x) v))) + ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x))) + "set") + (--> (Σ (in-hole E (get x))) + (Σ (in-hole E (lookup-Σ Σ x))) + "get"))) + +#| + +Capture avoiding substitution + +|# + + +(define-metafunction stlc + subst : M x M -> M + [(subst x x M_x) + M_x] + [(subst (λ x M) x M_x) + (λ x M)] + [(subst (let ([x M]) N) x M_x) + (let ([x (subst M x M_x)]) N)] + [(subst (λ y M) x M_x) + (λ x_new (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (let ([y N]) M) x M_x) + (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (M N) x M_x) + ((subst M x M_x) (subst N x M_x))] + [(subst M x M_z) + M]) + +(define-metafunction stlc + [(replace (any_1 ...) x_1 x_new) + ((replace any_1 x_1 x_new) ...)] + [(replace x_1 x_1 x_new) + x_new] + [(replace any_1 x_1 x_new) + any_1]) + +(define-metafunction stlc + lookup-Σ : Σ x -> v + [(lookup-Σ (x v Σ) x) v] + [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)]) + +(define-metafunction stlc + update-Σ : Σ x v -> Σ + [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] + [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) + +#| + +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) + (error 'Eval "doesn't typecheck: ~s" M)) + (define res (apply-reduction-relation* red (term (· ,M)))) + (unless (= 1 (length res)) + (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) + (define ans (car res)) + (match (car res) + ["error" "error"] + [`(,Σ ,N) + (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (unless (equal? M-t ans-t) + (error 'Eval "internal error: type soundness fails for ~s" M)) + (match N + [(? x?) (cond + [(term (in-dom? ,Σ ,N)) + 'ref] + [else + (error 'Eval "internal error: reduced to a free variable ~s" + M)])] + [(or `((cons ,_) ,_) `nil) 'list] + [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ] + [(? 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. + +|# + +(define/contract (type-check M) + (-> M? (or/c τ? #f)) + (define M-t (judgment-holds (typeof ,M τ) τ)) + (cond + [(empty? M-t) + #f] + [(null? (cdr M-t)) + (car M-t)] + [else + (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + +#| + +Random generators + +|# + +(define (generate-M-term) + (generate-term stlc M 5)) + +(define (generate-typed-term) + (match (generate-term stlc + #:satisfying + (typeof M τ) + 5) + [`(typeof ,M ,τ) + M] + [#f #f])) + +(define (typed-generator) + (let ([g (redex-generator stlc + (typeof M τ) + 5)]) + (λ () + (match (g) + [`(typeof ,M ,τ) + M] + [#f #f])))) + +(define (generate-enum-term) + (generate-term stlc M #:i-th (pick-an-index 0.035))) + +(define (ordered-enum-generator) + (let ([index 0]) + (λ () + (begin0 + (generate-term stlc M #:i-th index) + (set! index (add1 index)))))) + +#| + +Check to see if a combination of preservation +and progress holds for every single term reachable +from the given term. + +|# + +(define (check M) + (or (not M) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (define new-type + (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (and (consistent-with? t-type new-type) + (or (v? (list-ref Σ+M 1)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t)))))))))))) + +(define small-counter-example '(let ([x (new nil)]) + ((λ ignore + ((hd (get x)) 1)) + ((set x) ((cons 5) nil))))) +(test-equal (check small-counter-example) #f) 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 new file mode 100644 index 0000000000..14c8ed94c6 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-3.rkt @@ -0,0 +1,500 @@ +#lang racket/base + +(define the-error "mix up types in the function case") + +(require redex/reduction-semantics + (only-in redex/private/generate-term pick-an-index) + racket/match + racket/list + racket/contract + racket/bool + (only-in "../stlc/tests-lib.rkt" consistent-with?)) + +(provide (all-defined-out)) + +(define-language stlc + (M N ::= + (λ x M) + (M N) + x + c + (let ([x M]) N)) + (Γ (x σ Γ) + ·) + (σ τ ::= + int + (σ → τ) + (list τ) + (ref τ) + x) + (c d ::= c0 c1) + (c0 ::= + integer) + (c1 ::= cons nil hd tl new get set) + (x y r ::= variable-not-otherwise-mentioned) + + (v (λ x M) + c + ((cons v) v) + (cons v) + (+ v) + (set v) + r) + (E hole + (E M) + (v E) + (let ([x E]) M)) + (Σ ::= · (r v Σ)) + + (κ ::= + · + (λ τ κ) + (1 Γ M κ) + (2 τ κ)) + + (G ::= · (τ σ G)) + (Gx ::= · (x σ Gx))) + +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) +(define x? (redex-match? stlc x)) +(define M? (redex-match? stlc M)) +(define Σ-M? (redex-match? stlc (Σ M))) + +#| + +The typing judgment has no rule with multiple +(self-referential) premises. Instead, it explicitly +manipulates a continuation so that it can, when it +discovers a type equality, simply do the substitution +through the continuation. This also makes it possible +to easily generate fresh variables by picking ones +that aren't in the expression or the continuation. + +The 'tc-down' rules recur thru the term to find a type +of the left-most subexpression and the 'tc-up' rules +bring that type back, recurring on the continuation. + +|# + +(define-judgment-form stlc + #:mode (typeof I O) + #:contract (typeof M σ) + + [(tc-down · M · σ) + ------------- + (typeof M σ)]) + +(define-judgment-form stlc + #:mode (tc-down I I I O) + #:contract (tc-down Γ M κ σ) + + [(tc-up (const-type0 c0) κ σ_ans) + ------------------------------ + (tc-down Γ c0 κ σ_ans)] + + [(where x ,(variable-not-in (term (Γ κ)) 'γ)) + (tc-up (const-type1 x c1) κ σ_ans) + ------------------------------ + (tc-down Γ c1 κ σ_ans)] + + [(where τ (lookup-Γ Γ x)) + (tc-up τ κ σ_ans) + --------------------------- + (tc-down Γ x κ σ_ans)] + + [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) + (tc-down (x y Γ) M (λ y κ) σ_ans) + ------------------------------------------------ + (tc-down Γ (λ x M) κ σ_ans)] + + [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2) + -------------------------- + (tc-down Γ (M_1 M_2) κ σ_2)] + + [(where N_2 (subst N x v)) + (where y ,(variable-not-in (term N_2) 'l)) + (tc-down Γ ((λ y N_2) v) κ σ_2) + ------------------------------------------ + (tc-down Γ (let ([x v]) N) κ σ_2)] + + [(where #t (not-v? M)) + (tc-down Γ ((λ x N) M) κ σ_2) + --------------------------------- + (tc-down Γ (let ([x M]) N) κ σ_2)]) + +(define-judgment-form stlc + #:mode (tc-up I I O) + #:contract (tc-up τ κ σ) + + [--------------------- + (tc-up σ_ans · σ_ans)] + + [(tc-down Γ M (2 τ κ) σ_ans) + --------------------------- + (tc-up τ (1 Γ M κ) σ_ans)] + + [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) + (where G (unify τ_1 (τ_2 → x))) + (tc-up (apply-subst-τ G x) + (apply-subst-κ G κ) + σ_ans) + --------------------------------------------------- + (tc-up τ_1 (2 τ_2 κ) σ_ans)] + + [(tc-up (τ_1 → τ_2) κ σ_ans) + --------------------------- + (tc-up τ_2 (λ τ_1 κ) σ_ans)]) + +(define-metafunction stlc + const-type0 : c0 -> σ + [(const-type0 +) (int → (int → int))] + [(const-type0 integer) int]) + +(define-metafunction stlc + const-type1 : x c1 -> σ + [(const-type1 x nil) (list x)] + [(const-type1 x cons) (x → ((list x) → (list x)))] + [(const-type1 x hd) ((list x) → x)] + [(const-type1 x tl) ((list x) → (list x))] + [(const-type1 x new) (x → (ref x))] + [(const-type1 x get) ((ref x) → x)] + [(const-type1 x set) ((ref x) → (x → x))]) + +(define-metafunction stlc + lookup-Γ : Γ x -> σ or #f + [(lookup-Γ (x σ Γ) x) σ] + [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] + [(lookup-Γ · x) #f]) + +(define-metafunction stlc + unify : τ τ -> Gx or ⊥ + [(unify τ σ) (uh (τ σ ·) · #f)]) + +#| + +Algorithm copied from _An Efficient Unification Algorithm_ by +Alberto Martelli and Ugo Montanari (section 2). +http://www.nsl.com/misc/papers/martelli-montanari.pdf + +This isn't the eponymous algorithm; it is an earlier one +in the paper that's simpler. + +The 'uh' function iterates over a set of equations applying the +rules from the paper, moving them from the first argument to +the second argument and tracking when something changes. +It runs until there are no more changes. The (a), (b), +(c), and (d) are the rule labels from the paper. + +|# + +(define-metafunction stlc + uh : G G boolean -> Gx or ⊥ + + [(uh · G #t) (uh G · #f)] + [(uh · G #f) G] + + ;; (a) + [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))] + + ;; (b) + [(uh (x x G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- term reduction + [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)] + [(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh (int int G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- failure + [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))] + + ;; (d) -- x occurs in τ case + [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] + + ;; (d) -- x does not occur in τ case + [(uh (x τ G) G_r boolean) + (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t) + (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))] + + ;; no rules applied; try next equation, if any. + [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)]) + +(define-metafunction stlc + eliminate-G : x τ G -> G + [(eliminate-G x τ ·) ·] + [(eliminate-G x τ (σ_1 σ_2 G)) + ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) + +(define-metafunction stlc + eliminate-τ : x τ σ -> σ + [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))] + [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))] + [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))] + [(eliminate-τ x τ int) int] + [(eliminate-τ x τ x) τ] + [(eliminate-τ x τ y) y]) + +(define-metafunction stlc + ∨ : boolean boolean -> boolean + [(∨ #f #f) #f] + [(∨ boolean_1 boolean_2) #t]) + +(define-metafunction stlc + not-var? : τ -> boolean + [(not-var? x) #f] + [(not-var? τ) #t]) + +(define-metafunction stlc + in-vars-τ? : x τ -> boolean + [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))] + [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x int) #f] + [(in-vars-τ? x x) #t] + [(in-vars-τ? x y) #f]) + +(define-metafunction stlc + in-vars-G? : x G -> boolean + [(in-vars-G? x ·) #f] + [(in-vars-G? x (x τ G)) #t] + [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) + (∨ (in-vars-τ? x τ) + (in-vars-G? x G)))]) + +(define-metafunction stlc + apply-subst-τ : Gx τ -> τ + [(apply-subst-τ · τ) τ] + [(apply-subst-τ (x τ G) σ) + (apply-subst-τ G (eliminate-τ x τ σ))]) + +(define-metafunction stlc + apply-subst-κ : Gx κ -> κ + [(apply-subst-κ Gx ·) ·] + [(apply-subst-κ Gx (λ σ κ)) + (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (1 Γ M κ)) + (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (2 σ κ)) + (2 (apply-subst-τ Gx σ) + (apply-subst-κ Gx κ))]) + +(define-metafunction stlc + apply-subst-Γ : Gx Γ -> Γ + [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] + [(apply-subst-Γ Gx ·) ·]) + +(define-metafunction stlc + not-v? : M -> boolean + [(not-v? v) #f] + [(not-v? M) #t]) + +#| + +The reduction relation rewrites a pair of +a store and an expression to a new store +and a new expression or into the string + "error" (for hd and tl of the empty list) + +|# + +(define red + (reduction-relation + stlc + (--> (Σ (in-hole E ((λ x M) v))) + (Σ (in-hole E (subst M x v))) + "βv") + (--> (Σ (in-hole E (let ([x v]) M))) + (Σ (in-hole E (subst M x v))) + "let") + (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) + (Σ (in-hole E v_1)) + "hd") + (--> (Σ (in-hole E (tl ((cons v_1) v_2)))) + (Σ (in-hole E v_2)) + "tl") + (--> (Σ (in-hole E (hd nil))) + "error" + "hd-err") + (--> (Σ (in-hole E (tl nil))) + "error" + "tl-err") + (--> (Σ (in-hole E ((+ integer_1) integer_2))) + (Σ (in-hole E ,(+ (term integer_1) (term integer_2)))) + "+") + (--> (Σ (in-hole E (new v))) + ((r v Σ) (in-hole E r)) + (fresh r) + "ref") + (--> (Σ (in-hole E ((set x) v))) + ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x))) + "set") + (--> (Σ (in-hole E (get x))) + (Σ (in-hole E (lookup-Σ Σ x))) + "get"))) + +#| + +Capture avoiding substitution + +|# + + +(define-metafunction stlc + subst : M x M -> M + [(subst x x M_x) + M_x] + [(subst (λ x M) x M_x) + (λ x M)] + [(subst (let ([x M]) N) x M_x) + (let ([x (subst M x M_x)]) N)] + [(subst (λ y M) x M_x) + (λ x_new (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (let ([y N]) M) x M_x) + (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (M N) x M_x) + ((subst M x M_x) (subst N x M_x))] + [(subst M x M_z) + M]) + +(define-metafunction stlc + [(replace (any_1 ...) x_1 x_new) + ((replace any_1 x_1 x_new) ...)] + [(replace x_1 x_1 x_new) + x_new] + [(replace any_1 x_1 x_new) + any_1]) + +(define-metafunction stlc + lookup-Σ : Σ x -> v + [(lookup-Σ (x v Σ) x) v] + [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)]) + +(define-metafunction stlc + update-Σ : Σ x v -> Σ + [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] + [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) + +#| + +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) + (error 'Eval "doesn't typecheck: ~s" M)) + (define res (apply-reduction-relation* red (term (· ,M)))) + (unless (= 1 (length res)) + (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) + (define ans (car res)) + (match (car res) + ["error" "error"] + [`(,Σ ,N) + (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (unless (equal? M-t ans-t) + (error 'Eval "internal error: type soundness fails for ~s" M)) + (match N + [(? x?) (cond + [(term (in-dom? ,Σ ,N)) + 'ref] + [else + (error 'Eval "internal error: reduced to a free variable ~s" + M)])] + [(or `((cons ,_) ,_) `nil) 'list] + [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ] + [(? 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. + +|# + +(define/contract (type-check M) + (-> M? (or/c τ? #f)) + (define M-t (judgment-holds (typeof ,M τ) τ)) + (cond + [(empty? M-t) + #f] + [(null? (cdr M-t)) + (car M-t)] + [else + (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + +#| + +Random generators + +|# + +(define (generate-M-term) + (generate-term stlc M 5)) + +(define (generate-typed-term) + (match (generate-term stlc + #:satisfying + (typeof M τ) + 5) + [`(typeof ,M ,τ) + M] + [#f #f])) + +(define (typed-generator) + (let ([g (redex-generator stlc + (typeof M τ) + 5)]) + (λ () + (match (g) + [`(typeof ,M ,τ) + M] + [#f #f])))) + +(define (generate-enum-term) + (generate-term stlc M #:i-th (pick-an-index 0.035))) + +(define (ordered-enum-generator) + (let ([index 0]) + (λ () + (begin0 + (generate-term stlc M #:i-th index) + (set! index (add1 index)))))) + +#| + +Check to see if a combination of preservation +and progress holds for every single term reachable +from the given term. + +|# + +(define (check M) + (or (not M) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (define new-type + (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (and (consistent-with? t-type new-type) + (or (v? (list-ref Σ+M 1)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (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 new file mode 100644 index 0000000000..1bf3e8f9c1 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-4.rkt @@ -0,0 +1,501 @@ +#lang racket/base + +(define the-error + (string-append "misspelled the name of a metafunction in a side-condition, " + "causing the occurs check to not happen")) + +(require redex/reduction-semantics + (only-in redex/private/generate-term pick-an-index) + racket/match + racket/list + racket/contract + racket/bool + (only-in "../stlc/tests-lib.rkt" consistent-with?)) + +(provide (all-defined-out)) + +(define-language stlc + (M N ::= + (λ x M) + (M N) + x + c + (let ([x M]) N)) + (Γ (x σ Γ) + ·) + (σ τ ::= + int + (σ → τ) + (list τ) + (ref τ) + x) + (c d ::= c0 c1) + (c0 ::= + integer) + (c1 ::= cons nil hd tl new get set) + (x y r ::= variable-not-otherwise-mentioned) + + (v (λ x M) + c + ((cons v) v) + (cons v) + (+ v) + (set v) + r) + (E hole + (E M) + (v E) + (let ([x E]) M)) + (Σ ::= · (r v Σ)) + + (κ ::= + · + (λ τ κ) + (1 Γ M κ) + (2 τ κ)) + + (G ::= · (τ σ G)) + (Gx ::= · (x σ Gx))) + +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) +(define x? (redex-match? stlc x)) +(define M? (redex-match? stlc M)) +(define Σ-M? (redex-match? stlc (Σ M))) + +#| + +The typing judgment has no rule with multiple +(self-referential) premises. Instead, it explicitly +manipulates a continuation so that it can, when it +discovers a type equality, simply do the substitution +through the continuation. This also makes it possible +to easily generate fresh variables by picking ones +that aren't in the expression or the continuation. + +The 'tc-down' rules recur thru the term to find a type +of the left-most subexpression and the 'tc-up' rules +bring that type back, recurring on the continuation. + +|# + +(define-judgment-form stlc + #:mode (typeof I O) + #:contract (typeof M σ) + + [(tc-down · M · σ) + ------------- + (typeof M σ)]) + +(define-judgment-form stlc + #:mode (tc-down I I I O) + #:contract (tc-down Γ M κ σ) + + [(tc-up (const-type0 c0) κ σ_ans) + ------------------------------ + (tc-down Γ c0 κ σ_ans)] + + [(where x ,(variable-not-in (term (Γ κ)) 'γ)) + (tc-up (const-type1 x c1) κ σ_ans) + ------------------------------ + (tc-down Γ c1 κ σ_ans)] + + [(where τ (lookup-Γ Γ x)) + (tc-up τ κ σ_ans) + --------------------------- + (tc-down Γ x κ σ_ans)] + + [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) + (tc-down (x y Γ) M (λ y κ) σ_ans) + ------------------------------------------------ + (tc-down Γ (λ x M) κ σ_ans)] + + [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2) + -------------------------- + (tc-down Γ (M_1 M_2) κ σ_2)] + + [(where N_2 (subst N x v)) + (where y ,(variable-not-in (term N_2) 'l)) + (tc-down Γ ((λ y N_2) v) κ σ_2) + ------------------------------------------ + (tc-down Γ (let ([x v]) N) κ σ_2)] + + [(where #t (not-v? M)) + (tc-down Γ ((λ x N) M) κ σ_2) + --------------------------------- + (tc-down Γ (let ([x M]) N) κ σ_2)]) + +(define-judgment-form stlc + #:mode (tc-up I I O) + #:contract (tc-up τ κ σ) + + [--------------------- + (tc-up σ_ans · σ_ans)] + + [(tc-down Γ M (2 τ κ) σ_ans) + --------------------------- + (tc-up τ (1 Γ M κ) σ_ans)] + + [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) + (where G (unify τ_2 (τ_1 → x))) + (tc-up (apply-subst-τ G x) + (apply-subst-κ G κ) + σ_ans) + --------------------------------------------------- + (tc-up τ_1 (2 τ_2 κ) σ_ans)] + + [(tc-up (τ_1 → τ_2) κ σ_ans) + --------------------------- + (tc-up τ_2 (λ τ_1 κ) σ_ans)]) + +(define-metafunction stlc + const-type0 : c0 -> σ + [(const-type0 +) (int → (int → int))] + [(const-type0 integer) int]) + +(define-metafunction stlc + const-type1 : x c1 -> σ + [(const-type1 x nil) (list x)] + [(const-type1 x cons) (x → ((list x) → (list x)))] + [(const-type1 x hd) ((list x) → x)] + [(const-type1 x tl) ((list x) → (list x))] + [(const-type1 x new) (x → (ref x))] + [(const-type1 x get) ((ref x) → x)] + [(const-type1 x set) ((ref x) → (x → x))]) + +(define-metafunction stlc + lookup-Γ : Γ x -> σ or #f + [(lookup-Γ (x σ Γ) x) σ] + [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] + [(lookup-Γ · x) #f]) + +(define-metafunction stlc + unify : τ τ -> Gx or ⊥ + [(unify τ σ) (uh (τ σ ·) · #f)]) + +#| + +Algorithm copied from _An Efficient Unification Algorithm_ by +Alberto Martelli and Ugo Montanari (section 2). +http://www.nsl.com/misc/papers/martelli-montanari.pdf + +This isn't the eponymous algorithm; it is an earlier one +in the paper that's simpler. + +The 'uh' function iterates over a set of equations applying the +rules from the paper, moving them from the first argument to +the second argument and tracking when something changes. +It runs until there are no more changes. The (a), (b), +(c), and (d) are the rule labels from the paper. + +|# + +(define-metafunction stlc + uh : G G boolean -> Gx or ⊥ + + [(uh · G #t) (uh G · #f)] + [(uh · G #f) G] + + ;; (a) + [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))] + + ;; (b) + [(uh (x x G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- term reduction + [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)] + [(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh (int int G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- failure + [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))] + + ;; (d) -- x occurs in τ case + [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars? x τ))] + + ;; (d) -- x does not occur in τ case + [(uh (x τ G) G_r boolean) + (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t) + (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))] + + ;; no rules applied; try next equation, if any. + [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)]) + +(define-metafunction stlc + eliminate-G : x τ G -> G + [(eliminate-G x τ ·) ·] + [(eliminate-G x τ (σ_1 σ_2 G)) + ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) + +(define-metafunction stlc + eliminate-τ : x τ σ -> σ + [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))] + [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))] + [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))] + [(eliminate-τ x τ int) int] + [(eliminate-τ x τ x) τ] + [(eliminate-τ x τ y) y]) + +(define-metafunction stlc + ∨ : boolean boolean -> boolean + [(∨ #f #f) #f] + [(∨ boolean_1 boolean_2) #t]) + +(define-metafunction stlc + not-var? : τ -> boolean + [(not-var? x) #f] + [(not-var? τ) #t]) + +(define-metafunction stlc + in-vars-τ? : x τ -> boolean + [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))] + [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x int) #f] + [(in-vars-τ? x x) #t] + [(in-vars-τ? x y) #f]) + +(define-metafunction stlc + in-vars-G? : x G -> boolean + [(in-vars-G? x ·) #f] + [(in-vars-G? x (x τ G)) #t] + [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) + (∨ (in-vars-τ? x τ) + (in-vars-G? x G)))]) + +(define-metafunction stlc + apply-subst-τ : Gx τ -> τ + [(apply-subst-τ · τ) τ] + [(apply-subst-τ (x τ G) σ) + (apply-subst-τ G (eliminate-τ x τ σ))]) + +(define-metafunction stlc + apply-subst-κ : Gx κ -> κ + [(apply-subst-κ Gx ·) ·] + [(apply-subst-κ Gx (λ σ κ)) + (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (1 Γ M κ)) + (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (2 σ κ)) + (2 (apply-subst-τ Gx σ) + (apply-subst-κ Gx κ))]) + +(define-metafunction stlc + apply-subst-Γ : Gx Γ -> Γ + [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] + [(apply-subst-Γ Gx ·) ·]) + +(define-metafunction stlc + not-v? : M -> boolean + [(not-v? v) #f] + [(not-v? M) #t]) + +#| + +The reduction relation rewrites a pair of +a store and an expression to a new store +and a new expression or into the string + "error" (for hd and tl of the empty list) + +|# + +(define red + (reduction-relation + stlc + (--> (Σ (in-hole E ((λ x M) v))) + (Σ (in-hole E (subst M x v))) + "βv") + (--> (Σ (in-hole E (let ([x v]) M))) + (Σ (in-hole E (subst M x v))) + "let") + (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) + (Σ (in-hole E v_1)) + "hd") + (--> (Σ (in-hole E (tl ((cons v_1) v_2)))) + (Σ (in-hole E v_2)) + "tl") + (--> (Σ (in-hole E (hd nil))) + "error" + "hd-err") + (--> (Σ (in-hole E (tl nil))) + "error" + "tl-err") + (--> (Σ (in-hole E ((+ integer_1) integer_2))) + (Σ (in-hole E ,(+ (term integer_1) (term integer_2)))) + "+") + (--> (Σ (in-hole E (new v))) + ((r v Σ) (in-hole E r)) + (fresh r) + "ref") + (--> (Σ (in-hole E ((set x) v))) + ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x))) + "set") + (--> (Σ (in-hole E (get x))) + (Σ (in-hole E (lookup-Σ Σ x))) + "get"))) + +#| + +Capture avoiding substitution + +|# + + +(define-metafunction stlc + subst : M x M -> M + [(subst x x M_x) + M_x] + [(subst (λ x M) x M_x) + (λ x M)] + [(subst (let ([x M]) N) x M_x) + (let ([x (subst M x M_x)]) N)] + [(subst (λ y M) x M_x) + (λ x_new (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (let ([y N]) M) x M_x) + (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (M N) x M_x) + ((subst M x M_x) (subst N x M_x))] + [(subst M x M_z) + M]) + +(define-metafunction stlc + [(replace (any_1 ...) x_1 x_new) + ((replace any_1 x_1 x_new) ...)] + [(replace x_1 x_1 x_new) + x_new] + [(replace any_1 x_1 x_new) + any_1]) + +(define-metafunction stlc + lookup-Σ : Σ x -> v + [(lookup-Σ (x v Σ) x) v] + [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)]) + +(define-metafunction stlc + update-Σ : Σ x v -> Σ + [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] + [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) + +#| + +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) + (error 'Eval "doesn't typecheck: ~s" M)) + (define res (apply-reduction-relation* red (term (· ,M)))) + (unless (= 1 (length res)) + (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) + (define ans (car res)) + (match (car res) + ["error" "error"] + [`(,Σ ,N) + (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (unless (equal? M-t ans-t) + (error 'Eval "internal error: type soundness fails for ~s" M)) + (match N + [(? x?) (cond + [(term (in-dom? ,Σ ,N)) + 'ref] + [else + (error 'Eval "internal error: reduced to a free variable ~s" + M)])] + [(or `((cons ,_) ,_) `nil) 'list] + [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ] + [(? 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. + +|# + +(define/contract (type-check M) + (-> M? (or/c τ? #f)) + (define M-t (judgment-holds (typeof ,M τ) τ)) + (cond + [(empty? M-t) + #f] + [(null? (cdr M-t)) + (car M-t)] + [else + (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + +#| + +Random generators + +|# + +(define (generate-M-term) + (generate-term stlc M 5)) + +(define (generate-typed-term) + (match (generate-term stlc + #:satisfying + (typeof M τ) + 5) + [`(typeof ,M ,τ) + M] + [#f #f])) + +(define (typed-generator) + (let ([g (redex-generator stlc + (typeof M τ) + 5)]) + (λ () + (match (g) + [`(typeof ,M ,τ) + M] + [#f #f])))) + +(define (generate-enum-term) + (generate-term stlc M #:i-th (pick-an-index 0.035))) + +(define (ordered-enum-generator) + (let ([index 0]) + (λ () + (begin0 + (generate-term stlc M #:i-th index) + (set! index (add1 index)))))) + +#| + +Check to see if a combination of preservation +and progress holds for every single term reachable +from the given term. + +|# + +(define (check M) + (or (not M) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (define new-type + (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (and (consistent-with? t-type new-type) + (or (v? (list-ref Σ+M 1)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t)))))))))))) + +(define small-counter-example (term ((λ x (x x)) (λ x x)))) +(test-equal (check small-counter-example) #f) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly-stlc/let-poly-stlc-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt similarity index 79% rename from pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly-stlc/let-poly-stlc-base.rkt rename to pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt index 9c15817cd7..abb964ed15 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly-stlc/let-poly-stlc-base.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-5.rkt @@ -1,6 +1,6 @@ #lang racket/base -(define the-error "no error") +(define the-error "eliminate-G was written as if it always gets a Gx as input") (require redex/reduction-semantics (only-in redex/private/generate-term pick-an-index) @@ -60,6 +60,22 @@ (define M? (redex-match? stlc M)) (define Σ-M? (redex-match? stlc (Σ M))) +#| + +The typing judgment has no rule with multiple +(self-referential) premises. Instead, it explicitly +manipulates a continuation so that it can, when it +discovers a type equality, simply do the substitution +through the continuation. This also makes it possible +to easily generate fresh variables by picking ones +that aren't in the expression or the continuation. + +The 'tc-down' rules recur thru the term to find a type +of the left-most subexpression and the 'tc-up' rules +bring that type back, recurring on the continuation. + +|# + (define-judgment-form stlc #:mode (typeof I O) #:contract (typeof M σ) @@ -87,7 +103,7 @@ (tc-down Γ x κ σ_ans)] [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) - (tc-down (x y Γ) M (λ y κ) σ_ans) ;; BUG: the continuation had 'x' not 'y' in it + (tc-down (x y Γ) M (λ y κ) σ_ans) ------------------------------------------------ (tc-down Γ (λ x M) κ σ_ans)] @@ -95,25 +111,10 @@ -------------------------- (tc-down Γ (M_1 M_2) κ σ_2)] -#| - ;; BUG: this is the classic bug -- it replaces the last two rules below - [(where y ,(variable-not-in (term (x M N κ)) 'l)) - (tc-down Γ ((λ y (subst N x M)) M) κ σ_2) - ----------------------------------------- - (tc-down Γ (let ([x M]) N) κ σ_2)] -|# - -#| -;; BUG: doesn't type check 'v' when x doesn't occur free in N -;; I knew about this and yet STILL forgot to do it properly! - [(tc-down Γ (subst N x v) κ σ_2) - ---------------------------------- - (tc-down Γ (let ([x v]) N) κ σ_2)] -|# - - [(where y ,(variable-not-in (term (x v N κ)) 'l)) - (tc-down Γ ((λ y (subst N x v)) v) κ σ_2) - ---------------------------------- + [(where N_2 (subst N x v)) + (where y ,(variable-not-in (term N_2) 'l)) + (tc-down Γ ((λ y N_2) v) κ σ_2) + ------------------------------------------ (tc-down Γ (let ([x v]) N) κ σ_2)] [(where #t (not-v? M)) @@ -133,29 +134,38 @@ (tc-up τ (1 Γ M κ) σ_ans)] [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) - (where G (unify τ_2 (τ_1 → x))) ;; BUG: swap τ_2 and τ_1 in this line + (where G (unify τ_2 (τ_1 → x))) (tc-up (apply-subst-τ G x) (apply-subst-κ G κ) σ_ans) --------------------------------------------------- (tc-up τ_1 (2 τ_2 κ) σ_ans)] -#| - ;; BUG: this case was written assuming that τ_2 was - ;; already an arrow type (which is wrong only when it is - ;; a variable: - [(where G (unify τ_1 τ_2)) - (tc-up (apply-subst-τ G τ_3) - (apply-subst-κ G κ) - σ_ans) - ----------------------------------- - (tc-up τ_1 (2 (τ_2 → τ_3) κ) σ_ans)] -|# - [(tc-up (τ_1 → τ_2) κ σ_ans) --------------------------- (tc-up τ_2 (λ τ_1 κ) σ_ans)]) +(define-metafunction stlc + const-type0 : c0 -> σ + [(const-type0 +) (int → (int → int))] + [(const-type0 integer) int]) + +(define-metafunction stlc + const-type1 : x c1 -> σ + [(const-type1 x nil) (list x)] + [(const-type1 x cons) (x → ((list x) → (list x)))] + [(const-type1 x hd) ((list x) → x)] + [(const-type1 x tl) ((list x) → (list x))] + [(const-type1 x new) (x → (ref x))] + [(const-type1 x get) ((ref x) → x)] + [(const-type1 x set) ((ref x) → (x → x))]) + +(define-metafunction stlc + lookup-Γ : Γ x -> σ or #f + [(lookup-Γ (x σ Γ) x) σ] + [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] + [(lookup-Γ · x) #f]) + (define-metafunction stlc unify : τ τ -> Gx or ⊥ [(unify τ σ) (uh (τ σ ·) · #f)]) @@ -166,17 +176,21 @@ Algorithm copied from _An Efficient Unification Algorithm_ by Alberto Martelli and Ugo Montanari (section 2). http://www.nsl.com/misc/papers/martelli-montanari.pdf -The two iterate and the terminate rule are just how this code -searches for places to apply the rules; they are not from that -section in the paper. +This isn't the eponymous algorithm; it is an earlier one +in the paper that's simpler. + +The 'uh' function iterates over a set of equations applying the +rules from the paper, moving them from the first argument to +the second argument and tracking when something changes. +It runs until there are no more changes. The (a), (b), +(c), and (d) are the rule labels from the paper. |# (define-metafunction stlc uh : G G boolean -> Gx or ⊥ - ;; iterate + [(uh · G #t) (uh G · #f)] - ;; terminate [(uh · G #f) G] ;; (a) @@ -195,7 +209,6 @@ section in the paper. [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))] ;; (d) -- x occurs in τ case - ;; BUG: had (in-vars? x τ) not (in-vars-τ? x τ) [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] ;; (d) -- x does not occur in τ case @@ -203,17 +216,9 @@ section in the paper. (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t) (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))] - ;; iterate + ;; no rules applied; try next equation, if any. [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)]) -(define-metafunction stlc - eliminate-G : x τ G -> G - [(eliminate-G x τ ·) ·] - [(eliminate-G x τ (σ_1 σ_2 G)) - ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) - -#| -;; BUG: eliminate-G was written as if it was getting a Gx as input: (define-metafunction stlc eliminate-G : x τ G -> G [(eliminate-G x τ ·) ·] @@ -221,7 +226,6 @@ section in the paper. (τ (eliminate-τ x τ σ) (eliminate-G x τ G))] [(eliminate-G x τ (y σ G)) (y (eliminate-τ x τ σ) (eliminate-G x τ G))]) -|# (define-metafunction stlc eliminate-τ : x τ σ -> σ @@ -235,9 +239,6 @@ section in the paper. (define-metafunction stlc ∨ : boolean boolean -> boolean [(∨ #f #f) #f] - - ;; BUG: this case was [(∨ boolean boolean) #t] - ;; (which, of course, means that the two bools have to be the same) [(∨ boolean_1 boolean_2) #t]) (define-metafunction stlc @@ -284,32 +285,20 @@ section in the paper. [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] [(apply-subst-Γ Gx ·) ·]) -(define-metafunction stlc - const-type0 : c -> σ - [(const-type0 +) (int → (int → int))] - [(const-type0 integer) int]) - -(define-metafunction stlc - const-type1 : x c -> σ - [(const-type1 x nil) (list x)] - [(const-type1 x cons) (x → ((list x) → (list x)))] - [(const-type1 x hd) ((list x) → x)] - [(const-type1 x tl) ((list x) → (list x))] - [(const-type1 x new) (x → (ref x))] - [(const-type1 x get) ((ref x) → x)] - [(const-type1 x set) ((ref x) → (x → x))]) - -(define-metafunction stlc - lookup-Γ : Γ x -> σ or #f - [(lookup-Γ (x σ Γ) x) σ] - [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] - [(lookup-Γ · x) #f]) - (define-metafunction stlc not-v? : M -> boolean [(not-v? v) #f] [(not-v? M) #t]) +#| + +The reduction relation rewrites a pair of +a store and an expression to a new store +and a new expression or into the string + "error" (for hd and tl of the empty list) + +|# + (define red (reduction-relation stlc @@ -319,15 +308,6 @@ section in the paper. (--> (Σ (in-hole E (let ([x v]) M))) (Σ (in-hole E (subst M x v))) "let") - #| -;; BUG: this rule in place of the one above, -;; plus no evaluation contexts of 'let' -;; this bug is D because it only fails due to polymorphism -- subtle - (--> (Σ (in-hole E (let ([x M]) N))) - (Σ (in-hole E ((λ x N) M))) - "let") - |# - (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) (Σ (in-hole E v_1)) "hd") @@ -354,6 +334,13 @@ section in the paper. (Σ (in-hole E (lookup-Σ Σ x))) "get"))) +#| + +Capture avoiding substitution + +|# + + (define-metafunction stlc subst : M x M -> M [(subst x x M_x) @@ -393,6 +380,12 @@ section in the paper. [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) +#| + +A top-level evaluator + +|# + (define/contract (Eval M) (-> M? (or/c "error" 'list 'λ 'ref number?)) (define M-t (judgment-holds (typeof ,M τ) τ)) @@ -425,6 +418,12 @@ section in the paper. [(Σ->lets · M) M] [(Σ->lets (x v Σ) M) (let ([x (new v)]) (Σ->lets Σ M))]) +#| + +A top-level type checker. + +|# + (define/contract (type-check M) (-> M? (or/c τ? #f)) (define M-t (judgment-holds (typeof ,M τ) τ)) @@ -436,11 +435,11 @@ section in the paper. [else (error 'type-check "non-unique type: ~s : ~s" M M-t)])) -(define (progress-holds? M) - (if (type-check M) - (or (v? M) - (not (null? (apply-reduction-relation red (term (· ,M)))))) - #t)) +#| + +Random generators + +|# (define (generate-M-term) (generate-term stlc M 5)) @@ -448,37 +447,22 @@ section in the paper. (define (generate-typed-term) (match (generate-term stlc #:satisfying - (typeof · M τ) + (typeof M τ) 5) - [`(typeof · ,M ,τ) + [`(typeof ,M ,τ) M] [#f #f])) (define (typed-generator) (let ([g (redex-generator stlc - (typeof · M τ) + (typeof M τ) 5)]) (λ () (match (g) - [`(typeof · ,M ,τ) + [`(typeof ,M ,τ) M] [#f #f])))) -(define (check M) - (or (not M) - (v? M) - (let ([t-type (type-check M)]) - (implies - t-type - (let ([red-res (apply-reduction-relation red `(· ,M))]) - (and (= (length red-res) 1) - (let ([red-t (car red-res)]) - (or (equal? red-t "error") - (match red-t - [`(,Σ ,N) - (let ([red-type (type-check (term (Σ->lets ,Σ ,N)))]) - (consistent-with? t-type red-type))]))))))))) - (define (generate-enum-term) (generate-term stlc M #:i-th (pick-an-index 0.035))) @@ -489,4 +473,31 @@ section in the paper. (generate-term stlc M #:i-th index) (set! index (add1 index)))))) -;(time (redex-check stlc M (check (term M)) #:attempts 100000)) \ No newline at end of file +#| + +Check to see if a combination of preservation +and progress holds for every single term reachable +from the given term. + +|# + +(define (check M) + (or (not M) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (define new-type + (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (and (consistent-with? t-type new-type) + (or (v? (list-ref Σ+M 1)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t)))))))))))) + +(define small-counter-example (term (cons 1))) +(test-equal (with-handlers ([exn:fail? (λ (x) #f)]) + (check small-counter-example)) + #f) 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 new file mode 100644 index 0000000000..8b8459d20f --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-6.rkt @@ -0,0 +1,501 @@ +#lang racket/base + +(define the-error "∨ has an incorrect duplicated variable, leading to an uncovered case") + +(require redex/reduction-semantics + (only-in redex/private/generate-term pick-an-index) + racket/match + racket/list + racket/contract + racket/bool + (only-in "../stlc/tests-lib.rkt" consistent-with?)) + +(provide (all-defined-out)) + +(define-language stlc + (M N ::= + (λ x M) + (M N) + x + c + (let ([x M]) N)) + (Γ (x σ Γ) + ·) + (σ τ ::= + int + (σ → τ) + (list τ) + (ref τ) + x) + (c d ::= c0 c1) + (c0 ::= + integer) + (c1 ::= cons nil hd tl new get set) + (x y r ::= variable-not-otherwise-mentioned) + + (v (λ x M) + c + ((cons v) v) + (cons v) + (+ v) + (set v) + r) + (E hole + (E M) + (v E) + (let ([x E]) M)) + (Σ ::= · (r v Σ)) + + (κ ::= + · + (λ τ κ) + (1 Γ M κ) + (2 τ κ)) + + (G ::= · (τ σ G)) + (Gx ::= · (x σ Gx))) + +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) +(define x? (redex-match? stlc x)) +(define M? (redex-match? stlc M)) +(define Σ-M? (redex-match? stlc (Σ M))) + +#| + +The typing judgment has no rule with multiple +(self-referential) premises. Instead, it explicitly +manipulates a continuation so that it can, when it +discovers a type equality, simply do the substitution +through the continuation. This also makes it possible +to easily generate fresh variables by picking ones +that aren't in the expression or the continuation. + +The 'tc-down' rules recur thru the term to find a type +of the left-most subexpression and the 'tc-up' rules +bring that type back, recurring on the continuation. + +|# + +(define-judgment-form stlc + #:mode (typeof I O) + #:contract (typeof M σ) + + [(tc-down · M · σ) + ------------- + (typeof M σ)]) + +(define-judgment-form stlc + #:mode (tc-down I I I O) + #:contract (tc-down Γ M κ σ) + + [(tc-up (const-type0 c0) κ σ_ans) + ------------------------------ + (tc-down Γ c0 κ σ_ans)] + + [(where x ,(variable-not-in (term (Γ κ)) 'γ)) + (tc-up (const-type1 x c1) κ σ_ans) + ------------------------------ + (tc-down Γ c1 κ σ_ans)] + + [(where τ (lookup-Γ Γ x)) + (tc-up τ κ σ_ans) + --------------------------- + (tc-down Γ x κ σ_ans)] + + [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) + (tc-down (x y Γ) M (λ y κ) σ_ans) + ------------------------------------------------ + (tc-down Γ (λ x M) κ σ_ans)] + + [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2) + -------------------------- + (tc-down Γ (M_1 M_2) κ σ_2)] + + [(where N_2 (subst N x v)) + (where y ,(variable-not-in (term N_2) 'l)) + (tc-down Γ ((λ y N_2) v) κ σ_2) + ------------------------------------------ + (tc-down Γ (let ([x v]) N) κ σ_2)] + + [(where #t (not-v? M)) + (tc-down Γ ((λ x N) M) κ σ_2) + --------------------------------- + (tc-down Γ (let ([x M]) N) κ σ_2)]) + +(define-judgment-form stlc + #:mode (tc-up I I O) + #:contract (tc-up τ κ σ) + + [--------------------- + (tc-up σ_ans · σ_ans)] + + [(tc-down Γ M (2 τ κ) σ_ans) + --------------------------- + (tc-up τ (1 Γ M κ) σ_ans)] + + [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) + (where G (unify τ_2 (τ_1 → x))) + (tc-up (apply-subst-τ G x) + (apply-subst-κ G κ) + σ_ans) + --------------------------------------------------- + (tc-up τ_1 (2 τ_2 κ) σ_ans)] + + [(tc-up (τ_1 → τ_2) κ σ_ans) + --------------------------- + (tc-up τ_2 (λ τ_1 κ) σ_ans)]) + +(define-metafunction stlc + const-type0 : c0 -> σ + [(const-type0 +) (int → (int → int))] + [(const-type0 integer) int]) + +(define-metafunction stlc + const-type1 : x c1 -> σ + [(const-type1 x nil) (list x)] + [(const-type1 x cons) (x → ((list x) → (list x)))] + [(const-type1 x hd) ((list x) → x)] + [(const-type1 x tl) ((list x) → (list x))] + [(const-type1 x new) (x → (ref x))] + [(const-type1 x get) ((ref x) → x)] + [(const-type1 x set) ((ref x) → (x → x))]) + +(define-metafunction stlc + lookup-Γ : Γ x -> σ or #f + [(lookup-Γ (x σ Γ) x) σ] + [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] + [(lookup-Γ · x) #f]) + +(define-metafunction stlc + unify : τ τ -> Gx or ⊥ + [(unify τ σ) (uh (τ σ ·) · #f)]) + +#| + +Algorithm copied from _An Efficient Unification Algorithm_ by +Alberto Martelli and Ugo Montanari (section 2). +http://www.nsl.com/misc/papers/martelli-montanari.pdf + +This isn't the eponymous algorithm; it is an earlier one +in the paper that's simpler. + +The 'uh' function iterates over a set of equations applying the +rules from the paper, moving them from the first argument to +the second argument and tracking when something changes. +It runs until there are no more changes. The (a), (b), +(c), and (d) are the rule labels from the paper. + +|# + +(define-metafunction stlc + uh : G G boolean -> Gx or ⊥ + + [(uh · G #t) (uh G · #f)] + [(uh · G #f) G] + + ;; (a) + [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))] + + ;; (b) + [(uh (x x G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- term reduction + [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)] + [(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh (int int G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- failure + [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))] + + ;; (d) -- x occurs in τ case + [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] + + ;; (d) -- x does not occur in τ case + [(uh (x τ G) G_r boolean) + (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t) + (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))] + + ;; no rules applied; try next equation, if any. + [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)]) + +(define-metafunction stlc + eliminate-G : x τ G -> G + [(eliminate-G x τ ·) ·] + [(eliminate-G x τ (σ_1 σ_2 G)) + ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) + +(define-metafunction stlc + eliminate-τ : x τ σ -> σ + [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))] + [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))] + [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))] + [(eliminate-τ x τ int) int] + [(eliminate-τ x τ x) τ] + [(eliminate-τ x τ y) y]) + +(define-metafunction stlc + ∨ : boolean boolean -> boolean + [(∨ #f #f) #f] + [(∨ boolean boolean) #t]) + +(define-metafunction stlc + not-var? : τ -> boolean + [(not-var? x) #f] + [(not-var? τ) #t]) + +(define-metafunction stlc + in-vars-τ? : x τ -> boolean + [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))] + [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x int) #f] + [(in-vars-τ? x x) #t] + [(in-vars-τ? x y) #f]) + +(define-metafunction stlc + in-vars-G? : x G -> boolean + [(in-vars-G? x ·) #f] + [(in-vars-G? x (x τ G)) #t] + [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) + (∨ (in-vars-τ? x τ) + (in-vars-G? x G)))]) + +(define-metafunction stlc + apply-subst-τ : Gx τ -> τ + [(apply-subst-τ · τ) τ] + [(apply-subst-τ (x τ G) σ) + (apply-subst-τ G (eliminate-τ x τ σ))]) + +(define-metafunction stlc + apply-subst-κ : Gx κ -> κ + [(apply-subst-κ Gx ·) ·] + [(apply-subst-κ Gx (λ σ κ)) + (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (1 Γ M κ)) + (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (2 σ κ)) + (2 (apply-subst-τ Gx σ) + (apply-subst-κ Gx κ))]) + +(define-metafunction stlc + apply-subst-Γ : Gx Γ -> Γ + [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] + [(apply-subst-Γ Gx ·) ·]) + +(define-metafunction stlc + not-v? : M -> boolean + [(not-v? v) #f] + [(not-v? M) #t]) + +#| + +The reduction relation rewrites a pair of +a store and an expression to a new store +and a new expression or into the string + "error" (for hd and tl of the empty list) + +|# + +(define red + (reduction-relation + stlc + (--> (Σ (in-hole E ((λ x M) v))) + (Σ (in-hole E (subst M x v))) + "βv") + (--> (Σ (in-hole E (let ([x v]) M))) + (Σ (in-hole E (subst M x v))) + "let") + (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) + (Σ (in-hole E v_1)) + "hd") + (--> (Σ (in-hole E (tl ((cons v_1) v_2)))) + (Σ (in-hole E v_2)) + "tl") + (--> (Σ (in-hole E (hd nil))) + "error" + "hd-err") + (--> (Σ (in-hole E (tl nil))) + "error" + "tl-err") + (--> (Σ (in-hole E ((+ integer_1) integer_2))) + (Σ (in-hole E ,(+ (term integer_1) (term integer_2)))) + "+") + (--> (Σ (in-hole E (new v))) + ((r v Σ) (in-hole E r)) + (fresh r) + "ref") + (--> (Σ (in-hole E ((set x) v))) + ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x))) + "set") + (--> (Σ (in-hole E (get x))) + (Σ (in-hole E (lookup-Σ Σ x))) + "get"))) + +#| + +Capture avoiding substitution + +|# + + +(define-metafunction stlc + subst : M x M -> M + [(subst x x M_x) + M_x] + [(subst (λ x M) x M_x) + (λ x M)] + [(subst (let ([x M]) N) x M_x) + (let ([x (subst M x M_x)]) N)] + [(subst (λ y M) x M_x) + (λ x_new (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (let ([y N]) M) x M_x) + (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (M N) x M_x) + ((subst M x M_x) (subst N x M_x))] + [(subst M x M_z) + M]) + +(define-metafunction stlc + [(replace (any_1 ...) x_1 x_new) + ((replace any_1 x_1 x_new) ...)] + [(replace x_1 x_1 x_new) + x_new] + [(replace any_1 x_1 x_new) + any_1]) + +(define-metafunction stlc + lookup-Σ : Σ x -> v + [(lookup-Σ (x v Σ) x) v] + [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)]) + +(define-metafunction stlc + update-Σ : Σ x v -> Σ + [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] + [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) + +#| + +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) + (error 'Eval "doesn't typecheck: ~s" M)) + (define res (apply-reduction-relation* red (term (· ,M)))) + (unless (= 1 (length res)) + (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) + (define ans (car res)) + (match (car res) + ["error" "error"] + [`(,Σ ,N) + (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (unless (equal? M-t ans-t) + (error 'Eval "internal error: type soundness fails for ~s" M)) + (match N + [(? x?) (cond + [(term (in-dom? ,Σ ,N)) + 'ref] + [else + (error 'Eval "internal error: reduced to a free variable ~s" + M)])] + [(or `((cons ,_) ,_) `nil) 'list] + [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ] + [(? 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. + +|# + +(define/contract (type-check M) + (-> M? (or/c τ? #f)) + (define M-t (judgment-holds (typeof ,M τ) τ)) + (cond + [(empty? M-t) + #f] + [(null? (cdr M-t)) + (car M-t)] + [else + (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + +#| + +Random generators + +|# + +(define (generate-M-term) + (generate-term stlc M 5)) + +(define (generate-typed-term) + (match (generate-term stlc + #:satisfying + (typeof M τ) + 5) + [`(typeof ,M ,τ) + M] + [#f #f])) + +(define (typed-generator) + (let ([g (redex-generator stlc + (typeof M τ) + 5)]) + (λ () + (match (g) + [`(typeof ,M ,τ) + M] + [#f #f])))) + +(define (generate-enum-term) + (generate-term stlc M #:i-th (pick-an-index 0.035))) + +(define (ordered-enum-generator) + (let ([index 0]) + (λ () + (begin0 + (generate-term stlc M #:i-th index) + (set! index (add1 index)))))) + +#| + +Check to see if a combination of preservation +and progress holds for every single term reachable +from the given term. + +|# + +(define (check M) + (or (not M) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (define new-type + (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (and (consistent-with? t-type new-type) + (or (v? (list-ref Σ+M 1)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t)))))))))))) + +(define small-counter-example (term ((λ x x) 1))) +(test-equal (with-handlers ([exn:fail? (λ (x) #f)]) + (check small-counter-example)) + #f) 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 new file mode 100644 index 0000000000..e178eef0be --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-7.rkt @@ -0,0 +1,500 @@ +#lang racket/base + +(define the-error + (string-append "used let --> left-left-λ rewrite rule for let, " + "but the right-hand side is less polymorphic")) + +(require redex/reduction-semantics + (only-in redex/private/generate-term pick-an-index) + racket/match + racket/list + racket/contract + racket/bool + (only-in "../stlc/tests-lib.rkt" consistent-with?)) + +(provide (all-defined-out)) + +(define-language stlc + (M N ::= + (λ x M) + (M N) + x + c + (let ([x M]) N)) + (Γ (x σ Γ) + ·) + (σ τ ::= + int + (σ → τ) + (list τ) + (ref τ) + x) + (c d ::= c0 c1) + (c0 ::= + integer) + (c1 ::= cons nil hd tl new get set) + (x y r ::= variable-not-otherwise-mentioned) + + (v (λ x M) + c + ((cons v) v) + (cons v) + (+ v) + (set v) + r) + (E hole + (E M) + (v E)) + (Σ ::= · (r v Σ)) + + (κ ::= + · + (λ τ κ) + (1 Γ M κ) + (2 τ κ)) + + (G ::= · (τ σ G)) + (Gx ::= · (x σ Gx))) + +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) +(define x? (redex-match? stlc x)) +(define M? (redex-match? stlc M)) +(define Σ-M? (redex-match? stlc (Σ M))) + +#| + +The typing judgment has no rule with multiple +(self-referential) premises. Instead, it explicitly +manipulates a continuation so that it can, when it +discovers a type equality, simply do the substitution +through the continuation. This also makes it possible +to easily generate fresh variables by picking ones +that aren't in the expression or the continuation. + +The 'tc-down' rules recur thru the term to find a type +of the left-most subexpression and the 'tc-up' rules +bring that type back, recurring on the continuation. + +|# + +(define-judgment-form stlc + #:mode (typeof I O) + #:contract (typeof M σ) + + [(tc-down · M · σ) + ------------- + (typeof M σ)]) + +(define-judgment-form stlc + #:mode (tc-down I I I O) + #:contract (tc-down Γ M κ σ) + + [(tc-up (const-type0 c0) κ σ_ans) + ------------------------------ + (tc-down Γ c0 κ σ_ans)] + + [(where x ,(variable-not-in (term (Γ κ)) 'γ)) + (tc-up (const-type1 x c1) κ σ_ans) + ------------------------------ + (tc-down Γ c1 κ σ_ans)] + + [(where τ (lookup-Γ Γ x)) + (tc-up τ κ σ_ans) + --------------------------- + (tc-down Γ x κ σ_ans)] + + [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) + (tc-down (x y Γ) M (λ y κ) σ_ans) + ------------------------------------------------ + (tc-down Γ (λ x M) κ σ_ans)] + + [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2) + -------------------------- + (tc-down Γ (M_1 M_2) κ σ_2)] + + [(where N_2 (subst N x v)) + (where y ,(variable-not-in (term N_2) 'l)) + (tc-down Γ ((λ y N_2) v) κ σ_2) + ------------------------------------------ + (tc-down Γ (let ([x v]) N) κ σ_2)] + + [(where #t (not-v? M)) + (tc-down Γ ((λ x N) M) κ σ_2) + --------------------------------- + (tc-down Γ (let ([x M]) N) κ σ_2)]) + +(define-judgment-form stlc + #:mode (tc-up I I O) + #:contract (tc-up τ κ σ) + + [--------------------- + (tc-up σ_ans · σ_ans)] + + [(tc-down Γ M (2 τ κ) σ_ans) + --------------------------- + (tc-up τ (1 Γ M κ) σ_ans)] + + [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) + (where G (unify τ_2 (τ_1 → x))) + (tc-up (apply-subst-τ G x) + (apply-subst-κ G κ) + σ_ans) + --------------------------------------------------- + (tc-up τ_1 (2 τ_2 κ) σ_ans)] + + [(tc-up (τ_1 → τ_2) κ σ_ans) + --------------------------- + (tc-up τ_2 (λ τ_1 κ) σ_ans)]) + +(define-metafunction stlc + const-type0 : c0 -> σ + [(const-type0 +) (int → (int → int))] + [(const-type0 integer) int]) + +(define-metafunction stlc + const-type1 : x c1 -> σ + [(const-type1 x nil) (list x)] + [(const-type1 x cons) (x → ((list x) → (list x)))] + [(const-type1 x hd) ((list x) → x)] + [(const-type1 x tl) ((list x) → (list x))] + [(const-type1 x new) (x → (ref x))] + [(const-type1 x get) ((ref x) → x)] + [(const-type1 x set) ((ref x) → (x → x))]) + +(define-metafunction stlc + lookup-Γ : Γ x -> σ or #f + [(lookup-Γ (x σ Γ) x) σ] + [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] + [(lookup-Γ · x) #f]) + +(define-metafunction stlc + unify : τ τ -> Gx or ⊥ + [(unify τ σ) (uh (τ σ ·) · #f)]) + +#| + +Algorithm copied from _An Efficient Unification Algorithm_ by +Alberto Martelli and Ugo Montanari (section 2). +http://www.nsl.com/misc/papers/martelli-montanari.pdf + +This isn't the eponymous algorithm; it is an earlier one +in the paper that's simpler. + +The 'uh' function iterates over a set of equations applying the +rules from the paper, moving them from the first argument to +the second argument and tracking when something changes. +It runs until there are no more changes. The (a), (b), +(c), and (d) are the rule labels from the paper. + +|# + +(define-metafunction stlc + uh : G G boolean -> Gx or ⊥ + + [(uh · G #t) (uh G · #f)] + [(uh · G #f) G] + + ;; (a) + [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))] + + ;; (b) + [(uh (x x G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- term reduction + [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)] + [(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh (int int G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- failure + [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))] + + ;; (d) -- x occurs in τ case + [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] + + ;; (d) -- x does not occur in τ case + [(uh (x τ G) G_r boolean) + (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t) + (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))] + + ;; no rules applied; try next equation, if any. + [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)]) + +(define-metafunction stlc + eliminate-G : x τ G -> G + [(eliminate-G x τ ·) ·] + [(eliminate-G x τ (σ_1 σ_2 G)) + ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) + +(define-metafunction stlc + eliminate-τ : x τ σ -> σ + [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))] + [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))] + [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))] + [(eliminate-τ x τ int) int] + [(eliminate-τ x τ x) τ] + [(eliminate-τ x τ y) y]) + +(define-metafunction stlc + ∨ : boolean boolean -> boolean + [(∨ #f #f) #f] + [(∨ boolean_1 boolean_2) #t]) + +(define-metafunction stlc + not-var? : τ -> boolean + [(not-var? x) #f] + [(not-var? τ) #t]) + +(define-metafunction stlc + in-vars-τ? : x τ -> boolean + [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))] + [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x int) #f] + [(in-vars-τ? x x) #t] + [(in-vars-τ? x y) #f]) + +(define-metafunction stlc + in-vars-G? : x G -> boolean + [(in-vars-G? x ·) #f] + [(in-vars-G? x (x τ G)) #t] + [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) + (∨ (in-vars-τ? x τ) + (in-vars-G? x G)))]) + +(define-metafunction stlc + apply-subst-τ : Gx τ -> τ + [(apply-subst-τ · τ) τ] + [(apply-subst-τ (x τ G) σ) + (apply-subst-τ G (eliminate-τ x τ σ))]) + +(define-metafunction stlc + apply-subst-κ : Gx κ -> κ + [(apply-subst-κ Gx ·) ·] + [(apply-subst-κ Gx (λ σ κ)) + (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (1 Γ M κ)) + (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (2 σ κ)) + (2 (apply-subst-τ Gx σ) + (apply-subst-κ Gx κ))]) + +(define-metafunction stlc + apply-subst-Γ : Gx Γ -> Γ + [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] + [(apply-subst-Γ Gx ·) ·]) + +(define-metafunction stlc + not-v? : M -> boolean + [(not-v? v) #f] + [(not-v? M) #t]) + +#| + +The reduction relation rewrites a pair of +a store and an expression to a new store +and a new expression or into the string + "error" (for hd and tl of the empty list) + +|# + +(define red + (reduction-relation + stlc + (--> (Σ (in-hole E ((λ x M) v))) + (Σ (in-hole E (subst M x v))) + "βv") + (--> (Σ (in-hole E (let ([x M]) N))) + (Σ (in-hole E ((λ x N) M))) + "let") + (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) + (Σ (in-hole E v_1)) + "hd") + (--> (Σ (in-hole E (tl ((cons v_1) v_2)))) + (Σ (in-hole E v_2)) + "tl") + (--> (Σ (in-hole E (hd nil))) + "error" + "hd-err") + (--> (Σ (in-hole E (tl nil))) + "error" + "tl-err") + (--> (Σ (in-hole E ((+ integer_1) integer_2))) + (Σ (in-hole E ,(+ (term integer_1) (term integer_2)))) + "+") + (--> (Σ (in-hole E (new v))) + ((r v Σ) (in-hole E r)) + (fresh r) + "ref") + (--> (Σ (in-hole E ((set x) v))) + ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x))) + "set") + (--> (Σ (in-hole E (get x))) + (Σ (in-hole E (lookup-Σ Σ x))) + "get"))) + +#| + +Capture avoiding substitution + +|# + + +(define-metafunction stlc + subst : M x M -> M + [(subst x x M_x) + M_x] + [(subst (λ x M) x M_x) + (λ x M)] + [(subst (let ([x M]) N) x M_x) + (let ([x (subst M x M_x)]) N)] + [(subst (λ y M) x M_x) + (λ x_new (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (let ([y N]) M) x M_x) + (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (M N) x M_x) + ((subst M x M_x) (subst N x M_x))] + [(subst M x M_z) + M]) + +(define-metafunction stlc + [(replace (any_1 ...) x_1 x_new) + ((replace any_1 x_1 x_new) ...)] + [(replace x_1 x_1 x_new) + x_new] + [(replace any_1 x_1 x_new) + any_1]) + +(define-metafunction stlc + lookup-Σ : Σ x -> v + [(lookup-Σ (x v Σ) x) v] + [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)]) + +(define-metafunction stlc + update-Σ : Σ x v -> Σ + [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] + [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) + +#| + +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) + (error 'Eval "doesn't typecheck: ~s" M)) + (define res (apply-reduction-relation* red (term (· ,M)))) + (unless (= 1 (length res)) + (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) + (define ans (car res)) + (match (car res) + ["error" "error"] + [`(,Σ ,N) + (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (unless (equal? M-t ans-t) + (error 'Eval "internal error: type soundness fails for ~s" M)) + (match N + [(? x?) (cond + [(term (in-dom? ,Σ ,N)) + 'ref] + [else + (error 'Eval "internal error: reduced to a free variable ~s" + M)])] + [(or `((cons ,_) ,_) `nil) 'list] + [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ] + [(? 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. + +|# + +(define/contract (type-check M) + (-> M? (or/c τ? #f)) + (define M-t (judgment-holds (typeof ,M τ) τ)) + (cond + [(empty? M-t) + #f] + [(null? (cdr M-t)) + (car M-t)] + [else + (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + +#| + +Random generators + +|# + +(define (generate-M-term) + (generate-term stlc M 5)) + +(define (generate-typed-term) + (match (generate-term stlc + #:satisfying + (typeof M τ) + 5) + [`(typeof ,M ,τ) + M] + [#f #f])) + +(define (typed-generator) + (let ([g (redex-generator stlc + (typeof M τ) + 5)]) + (λ () + (match (g) + [`(typeof ,M ,τ) + M] + [#f #f])))) + +(define (generate-enum-term) + (generate-term stlc M #:i-th (pick-an-index 0.035))) + +(define (ordered-enum-generator) + (let ([index 0]) + (λ () + (begin0 + (generate-term stlc M #:i-th index) + (set! index (add1 index)))))) + +#| + +Check to see if a combination of preservation +and progress holds for every single term reachable +from the given term. + +|# + +(define (check M) + (or (not M) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (define new-type + (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (and (consistent-with? t-type new-type) + (or (v? (list-ref Σ+M 1)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t)))))))))))) + +(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-base.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt new file mode 100644 index 0000000000..2a46f75537 --- /dev/null +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/let-poly-base.rkt @@ -0,0 +1,496 @@ +#lang racket/base + +(define the-error "no error") + +(require redex/reduction-semantics + (only-in redex/private/generate-term pick-an-index) + racket/match + racket/list + racket/contract + racket/bool + (only-in "../stlc/tests-lib.rkt" consistent-with?)) + +(provide (all-defined-out)) + +(define-language stlc + (M N ::= + (λ x M) + (M N) + x + c + (let ([x M]) N)) + (Γ (x σ Γ) + ·) + (σ τ ::= + int + (σ → τ) + (list τ) + (ref τ) + x) + (c d ::= c0 c1) + (c0 ::= + integer) + (c1 ::= cons nil hd tl new get set) + (x y r ::= variable-not-otherwise-mentioned) + + (v (λ x M) + c + ((cons v) v) + (cons v) + (+ v) + (set v) + r) + (E hole + (E M) + (v E) + (let ([x E]) M)) + (Σ ::= · (r v Σ)) + + (κ ::= + · + (λ τ κ) + (1 Γ M κ) + (2 τ κ)) + + (G ::= · (τ σ G)) + (Gx ::= · (x σ Gx))) + +(define v? (redex-match? stlc v)) +(define τ? (redex-match? stlc τ)) +(define x? (redex-match? stlc x)) +(define M? (redex-match? stlc M)) +(define Σ-M? (redex-match? stlc (Σ M))) + +#| + +The typing judgment has no rule with multiple +(self-referential) premises. Instead, it explicitly +manipulates a continuation so that it can, when it +discovers a type equality, simply do the substitution +through the continuation. This also makes it possible +to easily generate fresh variables by picking ones +that aren't in the expression or the continuation. + +The 'tc-down' rules recur thru the term to find a type +of the left-most subexpression and the 'tc-up' rules +bring that type back, recurring on the continuation. + +|# + +(define-judgment-form stlc + #:mode (typeof I O) + #:contract (typeof M σ) + + [(tc-down · M · σ) + ------------- + (typeof M σ)]) + +(define-judgment-form stlc + #:mode (tc-down I I I O) + #:contract (tc-down Γ M κ σ) + + [(tc-up (const-type0 c0) κ σ_ans) + ------------------------------ + (tc-down Γ c0 κ σ_ans)] + + [(where x ,(variable-not-in (term (Γ κ)) 'γ)) + (tc-up (const-type1 x c1) κ σ_ans) + ------------------------------ + (tc-down Γ c1 κ σ_ans)] + + [(where τ (lookup-Γ Γ x)) + (tc-up τ κ σ_ans) + --------------------------- + (tc-down Γ x κ σ_ans)] + + [(where y ,(variable-not-in (term (x Γ M κ)) 'α2-)) + (tc-down (x y Γ) M (λ y κ) σ_ans) + ------------------------------------------------ + (tc-down Γ (λ x M) κ σ_ans)] + + [(tc-down Γ M_1 (1 Γ M_2 κ) σ_2) + -------------------------- + (tc-down Γ (M_1 M_2) κ σ_2)] + + [(where N_2 (subst N x v)) + (where y ,(variable-not-in (term N_2) 'l)) + (tc-down Γ ((λ y N_2) v) κ σ_2) + ------------------------------------------ + (tc-down Γ (let ([x v]) N) κ σ_2)] + + [(where #t (not-v? M)) + (tc-down Γ ((λ x N) M) κ σ_2) + --------------------------------- + (tc-down Γ (let ([x M]) N) κ σ_2)]) + +(define-judgment-form stlc + #:mode (tc-up I I O) + #:contract (tc-up τ κ σ) + + [--------------------- + (tc-up σ_ans · σ_ans)] + + [(tc-down Γ M (2 τ κ) σ_ans) + --------------------------- + (tc-up τ (1 Γ M κ) σ_ans)] + + [(where x ,(variable-not-in (term (τ_1 τ_2 κ)) 'α1-)) + (where G (unify τ_2 (τ_1 → x))) + (tc-up (apply-subst-τ G x) + (apply-subst-κ G κ) + σ_ans) + --------------------------------------------------- + (tc-up τ_1 (2 τ_2 κ) σ_ans)] + + [(tc-up (τ_1 → τ_2) κ σ_ans) + --------------------------- + (tc-up τ_2 (λ τ_1 κ) σ_ans)]) + +(define-metafunction stlc + const-type0 : c0 -> σ + [(const-type0 +) (int → (int → int))] + [(const-type0 integer) int]) + +(define-metafunction stlc + const-type1 : x c1 -> σ + [(const-type1 x nil) (list x)] + [(const-type1 x cons) (x → ((list x) → (list x)))] + [(const-type1 x hd) ((list x) → x)] + [(const-type1 x tl) ((list x) → (list x))] + [(const-type1 x new) (x → (ref x))] + [(const-type1 x get) ((ref x) → x)] + [(const-type1 x set) ((ref x) → (x → x))]) + +(define-metafunction stlc + lookup-Γ : Γ x -> σ or #f + [(lookup-Γ (x σ Γ) x) σ] + [(lookup-Γ (x σ Γ) y) (lookup-Γ Γ y)] + [(lookup-Γ · x) #f]) + +(define-metafunction stlc + unify : τ τ -> Gx or ⊥ + [(unify τ σ) (uh (τ σ ·) · #f)]) + +#| + +Algorithm copied from _An Efficient Unification Algorithm_ by +Alberto Martelli and Ugo Montanari (section 2). +http://www.nsl.com/misc/papers/martelli-montanari.pdf + +This isn't the eponymous algorithm; it is an earlier one +in the paper that's simpler. + +The 'uh' function iterates over a set of equations applying the +rules from the paper, moving them from the first argument to +the second argument and tracking when something changes. +It runs until there are no more changes. The (a), (b), +(c), and (d) are the rule labels from the paper. + +|# + +(define-metafunction stlc + uh : G G boolean -> Gx or ⊥ + + [(uh · G #t) (uh G · #f)] + [(uh · G #f) G] + + ;; (a) + [(uh (τ x G) G_r boolean) (uh G (x τ G_r) #t) (where #t (not-var? τ))] + + ;; (b) + [(uh (x x G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- term reduction + [(uh ((τ_1 → τ_2) (σ_1 → σ_2) G) G_r boolean) (uh (τ_1 σ_1 (τ_2 σ_2 G)) G_r #t)] + [(uh ((list τ) (list σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh ((ref τ) (ref σ) G) G_r boolean) (uh (τ σ G) G_r #t)] + [(uh (int int G) G_r boolean) (uh G G_r #t)] + + ;; (c) -- failure + [(uh (τ σ G) G_r boolean) ⊥ (where #t (not-var? τ)) (where #t (not-var? σ))] + + ;; (d) -- x occurs in τ case + [(uh (x τ G) G_r boolean) ⊥ (where #t (in-vars-τ? x τ))] + + ;; (d) -- x does not occur in τ case + [(uh (x τ G) G_r boolean) + (uh (eliminate-G x τ G) (x τ (eliminate-G x τ G_r)) #t) + (where #t (∨ (in-vars-G? x G) (in-vars-G? x G_r)))] + + ;; no rules applied; try next equation, if any. + [(uh (τ σ G) G_r boolean) (uh G (τ σ G_r) boolean)]) + +(define-metafunction stlc + eliminate-G : x τ G -> G + [(eliminate-G x τ ·) ·] + [(eliminate-G x τ (σ_1 σ_2 G)) + ((eliminate-τ x τ σ_1) (eliminate-τ x τ σ_2) (eliminate-G x τ G))]) + +(define-metafunction stlc + eliminate-τ : x τ σ -> σ + [(eliminate-τ x τ (σ_1 → σ_2)) ((eliminate-τ x τ σ_1) → (eliminate-τ x τ σ_2))] + [(eliminate-τ x τ (list σ)) (list (eliminate-τ x τ σ))] + [(eliminate-τ x τ (ref σ)) (ref (eliminate-τ x τ σ))] + [(eliminate-τ x τ int) int] + [(eliminate-τ x τ x) τ] + [(eliminate-τ x τ y) y]) + +(define-metafunction stlc + ∨ : boolean boolean -> boolean + [(∨ #f #f) #f] + [(∨ boolean_1 boolean_2) #t]) + +(define-metafunction stlc + not-var? : τ -> boolean + [(not-var? x) #f] + [(not-var? τ) #t]) + +(define-metafunction stlc + in-vars-τ? : x τ -> boolean + [(in-vars-τ? x (τ_1 → τ_2)) (∨ (in-vars-τ? x τ_1) (in-vars-τ? x τ_2))] + [(in-vars-τ? x (list τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x (ref τ)) (in-vars-τ? x τ)] + [(in-vars-τ? x int) #f] + [(in-vars-τ? x x) #t] + [(in-vars-τ? x y) #f]) + +(define-metafunction stlc + in-vars-G? : x G -> boolean + [(in-vars-G? x ·) #f] + [(in-vars-G? x (x τ G)) #t] + [(in-vars-G? x (σ τ G)) (∨ (in-vars-τ? x σ) + (∨ (in-vars-τ? x τ) + (in-vars-G? x G)))]) + +(define-metafunction stlc + apply-subst-τ : Gx τ -> τ + [(apply-subst-τ · τ) τ] + [(apply-subst-τ (x τ G) σ) + (apply-subst-τ G (eliminate-τ x τ σ))]) + +(define-metafunction stlc + apply-subst-κ : Gx κ -> κ + [(apply-subst-κ Gx ·) ·] + [(apply-subst-κ Gx (λ σ κ)) + (λ (apply-subst-τ Gx σ) (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (1 Γ M κ)) + (1 (apply-subst-Γ Gx Γ) M (apply-subst-κ Gx κ))] + [(apply-subst-κ Gx (2 σ κ)) + (2 (apply-subst-τ Gx σ) + (apply-subst-κ Gx κ))]) + +(define-metafunction stlc + apply-subst-Γ : Gx Γ -> Γ + [(apply-subst-Γ Gx (y σ Γ)) (y (apply-subst-τ Gx σ) (apply-subst-Γ Gx Γ))] + [(apply-subst-Γ Gx ·) ·]) + +(define-metafunction stlc + not-v? : M -> boolean + [(not-v? v) #f] + [(not-v? M) #t]) + +#| + +The reduction relation rewrites a pair of +a store and an expression to a new store +and a new expression or into the string + "error" (for hd and tl of the empty list) + +|# + +(define red + (reduction-relation + stlc + (--> (Σ (in-hole E ((λ x M) v))) + (Σ (in-hole E (subst M x v))) + "βv") + (--> (Σ (in-hole E (let ([x v]) M))) + (Σ (in-hole E (subst M x v))) + "let") + (--> (Σ (in-hole E (hd ((cons v_1) v_2)))) + (Σ (in-hole E v_1)) + "hd") + (--> (Σ (in-hole E (tl ((cons v_1) v_2)))) + (Σ (in-hole E v_2)) + "tl") + (--> (Σ (in-hole E (hd nil))) + "error" + "hd-err") + (--> (Σ (in-hole E (tl nil))) + "error" + "tl-err") + (--> (Σ (in-hole E ((+ integer_1) integer_2))) + (Σ (in-hole E ,(+ (term integer_1) (term integer_2)))) + "+") + (--> (Σ (in-hole E (new v))) + ((r v Σ) (in-hole E r)) + (fresh r) + "ref") + (--> (Σ (in-hole E ((set x) v))) + ((update-Σ Σ x v) (in-hole E (lookup-Σ Σ x))) + "set") + (--> (Σ (in-hole E (get x))) + (Σ (in-hole E (lookup-Σ Σ x))) + "get"))) + +#| + +Capture avoiding substitution + +|# + + +(define-metafunction stlc + subst : M x M -> M + [(subst x x M_x) + M_x] + [(subst (λ x M) x M_x) + (λ x M)] + [(subst (let ([x M]) N) x M_x) + (let ([x (subst M x M_x)]) N)] + [(subst (λ y M) x M_x) + (λ x_new (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (let ([y N]) M) x M_x) + (let ([x_new (subst N x M_x)]) (subst (replace M y x_new) x M_x)) + (where x_new ,(variable-not-in (term (x y M)) + (term y)))] + [(subst (M N) x M_x) + ((subst M x M_x) (subst N x M_x))] + [(subst M x M_z) + M]) + +(define-metafunction stlc + [(replace (any_1 ...) x_1 x_new) + ((replace any_1 x_1 x_new) ...)] + [(replace x_1 x_1 x_new) + x_new] + [(replace any_1 x_1 x_new) + any_1]) + +(define-metafunction stlc + lookup-Σ : Σ x -> v + [(lookup-Σ (x v Σ) x) v] + [(lookup-Σ (x v Σ) y) (lookup-Σ Σ y)]) + +(define-metafunction stlc + update-Σ : Σ x v -> Σ + [(update-Σ (x v_1 Σ) x v_2) (x v_2 Σ)] + [(update-Σ (x v_1 Σ) y v_2) (x v_1 (update-Σ Σ y v_2))]) + +#| + +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) + (error 'Eval "doesn't typecheck: ~s" M)) + (define res (apply-reduction-relation* red (term (· ,M)))) + (unless (= 1 (length res)) + (error 'Eval "internal error: not exactly 1 result ~s => ~s" M res)) + (define ans (car res)) + (match (car res) + ["error" "error"] + [`(,Σ ,N) + (define ans-t (judgment-holds (typeof (Σ->lets ,Σ ,N) τ) τ)) + (unless (equal? M-t ans-t) + (error 'Eval "internal error: type soundness fails for ~s" M)) + (match N + [(? x?) (cond + [(term (in-dom? ,Σ ,N)) + 'ref] + [else + (error 'Eval "internal error: reduced to a free variable ~s" + M)])] + [(or `((cons ,_) ,_) `nil) 'list] + [(or `(λ ,_ ,_) `(cons ,_) `(set ,_) `(+ ,_)) 'λ] + [(? 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. + +|# + +(define/contract (type-check M) + (-> M? (or/c τ? #f)) + (define M-t (judgment-holds (typeof ,M τ) τ)) + (cond + [(empty? M-t) + #f] + [(null? (cdr M-t)) + (car M-t)] + [else + (error 'type-check "non-unique type: ~s : ~s" M M-t)])) + +#| + +Random generators + +|# + +(define (generate-M-term) + (generate-term stlc M 5)) + +(define (generate-typed-term) + (match (generate-term stlc + #:satisfying + (typeof M τ) + 5) + [`(typeof ,M ,τ) + M] + [#f #f])) + +(define (typed-generator) + (let ([g (redex-generator stlc + (typeof M τ) + 5)]) + (λ () + (match (g) + [`(typeof ,M ,τ) + M] + [#f #f])))) + +(define (generate-enum-term) + (generate-term stlc M #:i-th (pick-an-index 0.035))) + +(define (ordered-enum-generator) + (let ([index 0]) + (λ () + (begin0 + (generate-term stlc M #:i-th index) + (set! index (add1 index)))))) + +#| + +Check to see if a combination of preservation +and progress holds for every single term reachable +from the given term. + +|# + +(define (check M) + (or (not M) + (let ([t-type (type-check M)]) + (implies + t-type + (let loop ([Σ+M `(· ,M)]) + (define new-type + (type-check (term (Σ->lets ,(list-ref Σ+M 0) ,(list-ref Σ+M 1))))) + (and (consistent-with? t-type new-type) + (or (v? (list-ref Σ+M 1)) + (let ([red-res (apply-reduction-relation red Σ+M)]) + (and (= (length red-res) 1) + (let ([red-t (car red-res)]) + (or (equal? red-t "error") + (loop red-t)))))))))))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly-stlc/tests.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt similarity index 97% rename from pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly-stlc/tests.rkt rename to pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt index b262ff7e0b..a5a1e7a0fc 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly-stlc/tests.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/let-poly/tests.rkt @@ -1,5 +1,5 @@ #lang racket/base -(require "let-poly-stlc-base.rkt" +(require "let-poly-base.rkt" (only-in "../stlc/tests-lib.rkt" consistent-with?) redex/reduction-semantics) @@ -38,8 +38,9 @@ (test-equal (consistent-with? (term (subst (let ([z 11]) (let ([z1 12]) z)) q 1)) (term (let ([z 11]) (let ([z1 12]) z)))) #t) - - +(test-equal (consistent-with? (term (subst (let ((|| +)) ||) |1| (λ x1 x1))) + (term (let ((|| +)) ||))) + #t) (test-equal (term (unify x int)) (term (x int ·))) diff --git a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt index f2f355868c..186544940a 100644 --- a/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt +++ b/pkgs/redex-pkgs/redex-examples/redex/examples/benchmark/stlc/tests-lib.rkt @@ -14,7 +14,7 @@ [(and (symbol? t1) (symbol? t2) (not (equal? t1 t2)) - (same-first-char? t1 t2)) + (same-first-char-or-empty-and-numbers? t1 t2)) (cond [(equal? t1 t2) #t] [else @@ -26,12 +26,16 @@ #t])])] [else (equal? t1 t2)]))) -(define (same-first-char? t1 t2) +(define (same-first-char-or-empty-and-numbers? t1 t2) (define (first-char s) (string-ref (symbol->string s) 0)) - (and (not (equal? t1 '||)) - (not (equal? t2 '||)) - (equal? (first-char t1) - (first-char t2)))) + (cond + [(equal? t1 '||) + (regexp-match #rx"[^[0-9]*$" (symbol->string t2))] + [(equal? t2 '||) + (regexp-match #rx"[^[0-9]*$" (symbol->string t1))] + [else + (equal? (first-char t1) + (first-char t2))])) (define-syntax-rule (stlc-tests uses-bound-var?