From 1760a02665f263ebeb92a56bfb5d64a5c995ccf2 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 25 Mar 2016 20:47:27 -0400 Subject: [PATCH] Trying to fix performance bugs with conversion --- cur-lib/cur/curnel/redex-core.rkt | 90 ++++++++++++++++++++----------- cur-test/cur/tests/redex-core.rkt | 6 +-- 2 files changed, 61 insertions(+), 35 deletions(-) diff --git a/cur-lib/cur/curnel/redex-core.rkt b/cur-lib/cur/curnel/redex-core.rkt index 86a6e2e..c12a391 100644 --- a/cur-lib/cur/curnel/redex-core.rkt +++ b/cur-lib/cur/curnel/redex-core.rkt @@ -357,16 +357,28 @@ (Θv ::= hole (Θv v)) (E ::= hole (E e) (v E) (elim D e (e ...) (v ... E e ...) e) - (elim D e (e ...) (v ...) E))) + (elim D e (e ...) (v ...) E) + ;; NB: These seem necessary, despite fixed conversion relation. + (Π (x : E) e) (Π (x : v) E))) (define-extended-language tt-cbnL tt-cbvL (E ::= hole (E e) (elim D e (e ...) (e ...) E))) -(define (tt-->cbv D) (context-closure (tt--> D) tt-cbvL E)) +(define-extended-language tt-head-redL tt-cbvL + (C-λ ::= Θ (λ (x : t) C-λ)) + (λv ::= x U (Π (x : t) t) (elim D e (e ...) (e ...) (in-hole C-λ x))) + (v ::= (in-hole C-λ λv))) + ;; Lazyness has lots of implications, such as on conversion and test suite. (define (tt-->cbn D) (context-closure (tt--> D) tt-cbnL E)) -;; Full reduction seems to loop forever +;; NB: Note that CIC specifies reduction via "contextual closure". +;; Perhaps they mean compatible-closure. Unfortunately, it's too slow. (define (tt-->full D) (compatible-closure (tt--> D) tt-redL e)) +;; Head reduction +(define (tt-->head-red D) (context-closure (tt--> D) tt-head-redL C-λ)) + +;; CBV, plus under Π +(define (tt-->cbv D) (context-closure (tt--> D) tt-cbvL E)) (define-metafunction tt-redL reduce : Δ e -> e @@ -381,31 +393,35 @@ ;; NB: Also a bijection between Γ and a list of maps from x to t. (Γ ::= ∅ (Γ x : t))) -(define-judgment-form tt-typingL - #:mode (sub I I I I) - #:contract (sub Δ Γ t t) - - [------------- - (sub Δ Γ t t)] - - [(side-condition ,(<= (term i_0) (term i_1))) - ----------------- "≼-Unv" - (sub Δ Γ (Unv i_0) (Unv i_1))] - - [(convert Δ Γ t_0 t_1) - (convert Δ (Γ x_0 : t_0) e_0 (subst e_1 x_1 x_0)) - ----------------- "≼-Π" - (sub Δ Γ (Π (x_0 : t_0) e_0) (Π (x_1 : t_1) e_1))]) - (define-judgment-form tt-typingL #:mode (convert I I I I) #:contract (convert Δ Γ t t) - [(where (t_2 t_3) ((reduce Δ t_0) (reduce Δ t_1))) - (sub Δ Γ t_2 t_3) - ----------------- "≼-αβ" + [----------------- "≡-Base" + (convert Δ Γ t t)] + + [(where (t_!_0 ...) (t_0 t_1)) + (where (t t) ((reduce Δ t_0) (reduce Δ t_1))) + ----------------- "≡-Normal" (convert Δ Γ t_0 t_1)]) +(define-judgment-form tt-typingL + #:mode (subtype I I I I) + #:contract (subtype Δ Γ t t) + + [(convert Δ Γ t_0 t_1) + ------------- "≼-≡" + (subtype Δ Γ t_0 t_1)] + + [(side-condition ,(<= (term i_0) (term i_1))) + ----------------- "≼-Unv" + (subtype Δ Γ (Unv i_0) (Unv i_1))] + + [(convert Δ Γ t_0 t_1) + (subtype Δ (Γ x_0 : t_0) e_0 (subst e_1 x_1 x_0)) + ----------------- "≼-Π" + (subtype Δ Γ (Π (x_0 : t_0) e_0) (Π (x_1 : t_1) e_1))]) + (define-metafunction tt-typingL Γ-in-dom : Γ x -> #t or #f [(Γ-in-dom ∅ x) @@ -515,20 +531,18 @@ ----------------- "DTR-Start" (type-infer Δ Γ x t)] - [(type-infer Δ (Γ x : t_0) e t_1) - (type-infer Δ Γ (Π (x : t_0) t_1) U) + [(type-infer-normal Δ (Γ x : t_0) e t_1) + (type-infer-normal Δ Γ (Π (x : t_0) t_1) U) ----------------- "DTR-Abstraction" (type-infer Δ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))] - [(type-infer Δ Γ t_0 U_1) - (type-infer Δ (Γ x : t_0) t U_2) + [(type-infer-normal Δ Γ t_0 U_1) + (type-infer-normal Δ (Γ x : t_0) t U_2) (unv-pred U_1 U_2 U) ----------------- "DTR-Product" (type-infer Δ Γ (Π (x : t_0) t) U)] - [(type-infer Δ Γ e_0 t) - ;; Cannot rely on type-infer producing normal forms. - (where (Π (x_0 : t_0) t_1) (reduce Δ t)) + [(type-infer-normal Δ Γ e_0 (Π (x_0 : t_0) t_1)) (type-check Δ Γ e_1 t_0) (where t_3 (subst t_1 x_0 e_1)) ----------------- "DTR-Application" @@ -536,20 +550,32 @@ [(type-check Δ Γ e_c (apply D e_i ...)) - (type-infer Δ Γ e_motive (name t_motive (in-hole Ξ U))) - (convert Δ Γ t_motive (Δ-motive-type Δ D U)) + (type-infer-normal Δ Γ e_motive (name t_motive (in-hole Ξ U))) + (subtype Δ Γ t_motive (Δ-motive-type Δ D U)) (where (t_m ...) (Δ-method-types Δ D e_motive)) + (type-check Δ Γ e_m t_m) ... ----------------- "DTR-Elim_D" (type-infer Δ Γ (elim D e_motive (e_i ...) (e_m ...) e_c) (apply e_motive e_i ... e_c))]) +;; Try to keep types in normal form, which simplifies a few things +(define-judgment-form tt-typingL + #:mode (type-infer-normal I I I O) + #:contract (type-infer-normal Δ Γ e t) + + [(type-infer Δ Γ e t) + ----------------- "DTR-Red" + (type-infer-normal Δ Γ e (reduce Δ t))]) + (define-judgment-form tt-typingL #:mode (type-check I I I I) #:contract (type-check Δ Γ e t) [(type-infer Δ Γ e t_0) - (convert Δ Γ t t_0) + (type-infer Δ Γ t U) + (subtype Δ Γ t t_0) ----------------- "DTR-Check" (type-check Δ Γ e t)]) + diff --git a/cur-test/cur/tests/redex-core.rkt b/cur-test/cur/tests/redex-core.rkt index 30c6556..16c4dd0 100644 --- a/cur-test/cur/tests/redex-core.rkt +++ b/cur-test/cur/tests/redex-core.rkt @@ -216,7 +216,7 @@ zero))))) (define-syntax-rule (check-equivalent e1 e2) - (check-holds (convert ∅ ∅ e1 e2))) + (check-holds (subtype ∅ ∅ e1 e2))) (check-equivalent (λ (x : Type) x) (λ (y : Type) y)) (check-equivalent @@ -344,7 +344,7 @@ (term ((λ (x : truth) (Unv 1)) T))) (check-holds - (convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1))) + (subtype ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1))) (check-holds (type-infer ,Δtruth ∅ @@ -509,7 +509,7 @@ ((and B) A)))) (in-hole Ξ (Π (x : (in-hole Θ and)) U)))) (check-holds - (convert ,Δ4 ∅ + (subtype ,Δ4 ∅ (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0)))) (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0)))))) (check-holds