diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt index 0f29ae9..2dcb666 100644 --- a/curnel/redex-core.rkt +++ b/curnel/redex-core.rkt @@ -95,43 +95,51 @@ ()))))) (check-true (Σ? sigma))) +;; NB: Depends on clause order (define-metafunction ttL - append-Σ : Σ Σ -> Σ - [(append-Σ Σ ∅) Σ] - [(append-Σ Σ_2 (Σ_1 (x : t ((x_c : t_c) ...)))) - ((append-Σ Σ_2 Σ_1) (x : t ((x_c : t_c) ...)))]) + Σ-ref : Σ x -> t or #f + [(Σ-ref ∅ x) #f] + [(Σ-ref (Σ (x : t ((x_1 : t_1) ...))) x) t] + [(Σ-ref (Σ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t] + [(Σ-ref (Σ (x_0 : t_0 ((x_1 : t_1) ...))) x) (Σ-ref Σ x)]) + +(define-metafunction ttL + Σ-union : Σ Σ -> Σ + [(Σ-union Σ ∅) Σ] + [(Σ-union Σ_2 (Σ_1 (x : t ((x_c : t_c) ...)))) + ((Σ-union Σ_2 Σ_1) (x : t ((x_c : t_c) ...)))]) ;; Returns the inductively defined type that x constructs ;; NB: Depends on clause order (define-metafunction ttL - constructor-of : Σ x -> x - [(constructor-of (Σ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c) + Σ-key-by-constructor : Σ x -> x + [(Σ-key-by-constructor (Σ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c) x] - [(constructor-of (Σ (x_1 : t_1 ((x_c : t) ...))) x) - (constructor-of Σ x)]) + [(Σ-key-by-constructor (Σ (x_1 : t_1 ((x_c : t) ...))) x) + (Σ-key-by-constructor Σ x)]) (module+ test (check-equal? - (term (constructor-of ,Σ zero)) + (term (Σ-key-by-constructor ,Σ zero)) (term nat)) (check-equal? - (term (constructor-of ,Σ s)) + (term (Σ-key-by-constructor ,Σ s)) (term nat))) ;; Returns the constructors for the inductively defined type x_D in the signature Σ (define-metafunction ttL - constructors-for : Σ x -> ((x : t) ...) or #f + Σ-ref-constructors : Σ x -> ((x : t) ...) or #f ;; NB: Depends on clause order - [(constructors-for ∅ x_D) #f] - [(constructors-for (Σ (x_D : t_D ((x : t) ...))) x_D) + [(Σ-ref-constructors ∅ x_D) #f] + [(Σ-ref-constructors (Σ (x_D : t_D ((x : t) ...))) x_D) ((x : t) ...)] - [(constructors-for (Σ (x_1 : t_1 ((x : t) ...))) x_D) - (constructors-for Σ x_D)]) + [(Σ-ref-constructors (Σ (x_1 : t_1 ((x : t) ...))) x_D) + (Σ-ref-constructors Σ x_D)]) (module+ test (check-equal? - (term (constructors-for ,Σ nat)) + (term (Σ-ref-constructors ,Σ nat)) (term ((zero : nat) (s : (Π (x : nat) nat))))) (check-equal? - (term (constructors-for ,sigma false)) + (term (Σ-ref-constructors ,sigma false)) (term ()))) ;; 'A' @@ -151,13 +159,13 @@ #:contract (unv-kind U U U) [---------------- - (unv-kind (Unv 0) (Unv 0) (Unv 0))] + (unv-kind (Unv 0) (Unv 0) (Unv 0))] [---------------- - (unv-kind (Unv 0) (Unv i) (Unv i))] + (unv-kind (Unv 0) (Unv i) (Unv i))] [---------------- - (unv-kind (Unv i) (Unv 0) (Unv 0))] + (unv-kind (Unv i) (Unv 0) (Unv 0))] [(where i_3 ,(max (term i_1) (term i_2))) ---------------- @@ -286,7 +294,7 @@ method-lookup : Σ x x (Θ e) -> e [(method-lookup Σ x_D x_ci Θ) (select-arg x_ci (x_0 ...) Θ) - (where ((x_0 : t_0) ...) (constructors-for Σ x_D))]) + (where ((x_0 : t_0) ...) (Σ-ref-constructors Σ x_D))]) (module+ test (check-equal? (term (method-lookup ,Σ nat s @@ -299,14 +307,14 @@ ;; TODO: Poorly documented, and poorly tested. ;; Probably the source of issue #20 (define-metafunction tt-redL - elim-recur : x U e Θ Θ Θ (x ...) -> Θ - [(elim-recur x_D U e_P Θ - (in-hole Θ_m (hole e_mi)) - (in-hole Θ_i (hole (in-hole Θ_r x_ci))) - (x_c0 ... x_ci x_c1 ...)) - ((elim-recur x_D U e_P Θ Θ_m Θ_i (x_c0 ... x_ci x_c1 ...)) - (in-hole (Θ (in-hole Θ_r x_ci)) ((elim x_D U) e_P)))] - [(elim-recur x_D U e_P Θ Θ_i Θ_nr (x ...)) hole]) + elim-recur : x U e Θ Θ Θ (x ...) -> Θ + [(elim-recur x_D U e_P Θ + (in-hole Θ_m (hole e_mi)) + (in-hole Θ_i (hole (in-hole Θ_r x_ci))) + (x_c0 ... x_ci x_c1 ...)) + ((elim-recur x_D U e_P Θ Θ_m Θ_i (x_c0 ... x_ci x_c1 ...)) + (in-hole (Θ (in-hole Θ_r x_ci)) ((elim x_D U) e_P)))] + [(elim-recur x_D U e_P Θ Θ_i Θ_nr (x ...)) hole]) (module+ test (check-true (redex-match? tt-redL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero)))) @@ -379,10 +387,10 @@ Θv) ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other ;; arguments. - (judgment-holds (telescope-match Θv_p (parameters-of Σ x_D))) + (judgment-holds (telescope-match Θv_p (Σ-ref-parameters Σ x_D))) ;; Ensure x_ci is actually a constructor for x_D (where ((x_c* : t_c*) ...) - (constructors-for Σ x_D)) + (Σ-ref-constructors Σ x_D)) (where (_ ... x_ci _ ...) (x_c* ...)) ;; There should be a number of methods equal to the number of constructors; to ensure E @@ -404,11 +412,11 @@ reduce : Σ e -> e [(reduce Σ e) e_r - (where (_ e_r) ,(let ([r (apply-reduction-relation* tt--> (term (Σ e)) - #:cache-all? #t)]) - (unless (null? (cdr r)) - (error "Church-rosser broken" r)) - (car r)))]) + (where (_ e_r) + ,(let ([r (apply-reduction-relation* tt--> (term (Σ e)) #:cache-all? #t)]) + (unless (null? (cdr r)) + (error "Church-rosser broken" r)) + (car r)))]) ;; TODO: Move equivalence up here, and use in these tests. (module+ test (check-equal? (term (reduce ∅ (Unv 0))) (term (Unv 0))) @@ -490,32 +498,24 @@ (define Γ? (redex-match? tt-typingL Γ)) (define-metafunction tt-typingL - append-Γ : Γ Γ -> Γ - [(append-Γ Γ ∅) Γ] - [(append-Γ Γ_2 (Γ_1 x : t)) - ((append-Γ Γ_2 Γ_1) x : t)]) + Γ-union : Γ Γ -> Γ + [(Γ-union Γ ∅) Γ] + [(Γ-union Γ_2 (Γ_1 x : t)) + ((Γ-union Γ_2 Γ_1) x : t)]) ;; NB: Depends on clause order (define-metafunction tt-typingL - lookup-Γ : Γ x -> t or #f - [(lookup-Γ ∅ x) #f] - [(lookup-Γ (Γ x : t) x) t] - [(lookup-Γ (Γ x_0 : t_0) x_1) (lookup-Γ Γ x_1)]) - -;; NB: Depends on clause order -(define-metafunction tt-redL - lookup-Σ : Σ x -> t or #f - [(lookup-Σ ∅ x) #f] - [(lookup-Σ (Σ (x : t ((x_1 : t_1) ...))) x) t] - [(lookup-Σ (Σ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t] - [(lookup-Σ (Σ (x_0 : t_0 ((x_1 : t_1) ...))) x) (lookup-Σ Σ x)]) + Γ-ref : Γ x -> t or #f + [(Γ-ref ∅ x) #f] + [(Γ-ref (Γ x : t) x) t] + [(Γ-ref (Γ x_0 : t_0) x_1) (Γ-ref Γ x_1)]) ;; NB: Depends on clause order (define-metafunction tt-typingL - remove : Γ x -> Γ - [(remove ∅ x) ∅] - [(remove (Γ x : t) x) Γ] - [(remove (Γ x_0 : t_0) x_1) (remove Γ x_1)]) + Γ-remove : Γ x -> Γ + [(Γ-remove ∅ x) ∅] + [(Γ-remove (Γ x : t) x) Γ] + [(Γ-remove (Γ x_0 : t_0) x_1) (Γ-remove Γ x_1)]) ;; TODO: Add positivity checking. (define-metafunction ttL @@ -688,17 +688,17 @@ ;; TODO: Define generic traversals of Σ and Γ ? (define-metafunction tt-redL - parameters-of : Σ x -> Ξ - [(parameters-of (Σ (x_D : (in-hole Ξ U) ((x : t) ...))) x_D) + Σ-ref-parameters : Σ x -> Ξ + [(Σ-ref-parameters (Σ (x_D : (in-hole Ξ U) ((x : t) ...))) x_D) Ξ] - [(parameters-of (Σ (x_1 : t_1 ((x : t) ...))) x_D) - (parameters-of Σ x_D)]) + [(Σ-ref-parameters (Σ (x_1 : t_1 ((x : t) ...))) x_D) + (Σ-ref-parameters Σ x_D)]) (module+ test (check-equal? - (term (parameters-of ,Σ nat)) + (term (Σ-ref-parameters ,Σ nat)) (term hole)) (check-equal? - (term (parameters-of ,Σ4 and)) + (term (Σ-ref-parameters ,Σ4 and)) (term (Π (A : Type) (Π (B : Type) hole))))) ;; Holds when an apply context Θ provides arguments that match the @@ -734,14 +734,14 @@ (λ (x : nat) (λ (ih-x : nat) x))) (methods-for nat (λ (x : nat) nat) - (constructors-for ,Σ nat)))) + (Σ-ref-constructors ,Σ nat)))) (check-holds (telescope-types (,Σ4 (true : (Unv 0) ((tt : true)))) ∅ (hole (λ (A : (Unv 0)) (λ (B : (Unv 0)) (λ (a : A) (λ (b : B) tt))))) (methods-for and (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true))) - (constructors-for ,Σ4 and)))) + (Σ-ref-constructors ,Σ4 and)))) (check-holds (telescope-types ,sigma (∅ x : false) hole @@ -761,11 +761,11 @@ ----------------- "DTR-Axiom" (type-infer Σ Γ U_0 U_1)] - [(where t (lookup-Σ Σ x)) + [(where t (Σ-ref Σ x)) ----------------- "DTR-Inductive" (type-infer Σ Γ x t)] - [(where t (lookup-Γ Γ x)) + [(where t (Γ-ref Γ x)) ----------------- "DTR-Start" (type-infer Σ Γ x t)] @@ -787,7 +787,7 @@ (type-infer Σ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))] [(type-infer Σ Γ x_D (in-hole Ξ t_D)) - (where Ξ (parameters-of Σ x_D)) + (where Ξ (Σ-ref-parameters Σ x_D)) ;; A fresh name to bind the discriminant (where x ,(variable-not-in (term (Σ Γ x_D Ξ)) 'x-D)) ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e., @@ -797,7 +797,7 @@ ;; A fresh name for the motive (where x_P ,(variable-not-in (term (Σ Γ x_D Ξ Ξ_P*D x)) 'x-P)) ;; The types of the methods for this inductive. - (where Ξ_m (methods-for x_D x_P (constructors-for Σ x_D))) + (where Ξ_m (methods-for x_D x_P (Σ-ref-constructors Σ x_D))) ----------------- "DTR-Elim_D" (type-infer Σ Γ (elim x_D U) ;; The type of (elim x_D U) is something like: @@ -1158,7 +1158,7 @@ (term (((((hole (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))) (check-equal? - (term (parameters-of ,Σ= ==)) + (term (Σ-ref-parameters ,Σ= ==)) (term (Π (A : Type) (Π (a : A) (Π (b : A) hole))))) (check-equal? (term (reduce ,Σ= ,refl-elim)) diff --git a/curnel/redex-lang.rkt b/curnel/redex-lang.rkt index 87ec328..0874887 100644 --- a/curnel/redex-lang.rkt +++ b/curnel/redex-lang.rkt @@ -11,7 +11,7 @@ racket/syntax (except-in racket/provide-transform export) racket/require-transform - (except-in "redex-core.rkt" remove) + "redex-core.rkt" redex/reduction-semantics)) (provide ;; Basic syntax @@ -86,6 +86,7 @@ (error 'core-error "We built a bad sigma ~s" x)) x))) + ;; These should be provided by core, so details of envs can be hidden. (define (extend-Γ/term env x t) (term (,(env) ,x : ,t))) @@ -269,8 +270,8 @@ (define (cur-identifier-bound? id) (let ([x (syntax->datum id)]) (and (x? x) - (or (term (lookup-Γ ,(gamma) ,x)) - (term (lookup-Σ ,(sigma) ,x)))))) + (or (term (Γ-ref ,(gamma) ,x)) + (term (Σ-ref ,(sigma) ,x)))))) (define (filter-cur-exports syn modes) (partition (compose cur-identifier-bound? export-local-id) @@ -336,7 +337,7 @@ ;; TODO: Do not DIY gensym (set! gn (add1 gn)) (set! out-gammas - #`(#,@out-gammas (gamma (term (append-Γ + #`(#,@out-gammas (gamma (term (Γ-union ,(gamma) ,#,new-id))))) (cons (struct-copy import imp [local-id new-id]) @@ -349,7 +350,7 @@ ;; TODO: Do not DIY gensym (set! sn (add1 sn)) (set! out-sigmas - #`(#,@out-sigmas (sigma (term (append-Σ + #`(#,@out-sigmas (sigma (term (Σ-union ,(sigma) ,#,new-id))))) (cons (struct-copy import imp [local-id new-id])