From 24d694cf46ee2cd3fd87dcd17073b4aa25dc794c Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Thu, 17 Aug 2017 19:13:59 -0400 Subject: [PATCH] for tycons, make all args explicit (eg tyvars) for all elim args --- turnstile/examples/dep-ind.rkt | 73 +++++++++++-------- .../examples/tests/dep-ind-list-tests.rkt | 58 +++++++-------- 2 files changed, 72 insertions(+), 59 deletions(-) diff --git a/turnstile/examples/dep-ind.rkt b/turnstile/examples/dep-ind.rkt index 1c4ebf1..6928d03 100644 --- a/turnstile/examples/dep-ind.rkt +++ b/turnstile/examples/dep-ind.rkt @@ -549,6 +549,7 @@ #:with ((~Π ([_ : _] ...) (~Π ([X : τ_in/tmp] ...) τ_out/tmp)) ...) #'(TY- ...) #:with (C* ...) (generate-temporaries #'(C ...)) + #:with (Cty ...) (generate-temporaries #'(C ...)) #:with (C** ...) (generate-temporaries #'(C ...)) #:with (Ccase ...) (generate-temporaries #'(C ...)) #:with (C- ...) (generate-temporaries #'(C ...)) @@ -574,6 +575,10 @@ fs ts))) #'((fld ...) ...) #'((τ_in/tmp ...) ...)) + #:with ((CArecur ...) ...) (stx-map + (lambda (cas recurs) cas) + #'((CA ...) ...) + #'((recur-fld ...) ...)) #:with ((fld- ...) ...) (stx-map generate-temporaries #'((X ...) ...)) #:with Name- (mk-- #'Name) #:with Name-patexpand (mk-~ #'Name) @@ -589,29 +594,16 @@ [⊢ (Name- A- ...) ⇒ k_out]) (struct C* (fld ...) #:transparent) ... (define C (unsafe-assign-type (lambda (A ...) C*) : TY)) ... - #;(define-typed-syntax C - [:id ≫ --- [⊢ C* ⇒ TY]] - [(_ fld ...) ≫ - ;; TODO: need to subst X in τ_out? - #:with (~Π ([_ : τ_in] ...) τ_out) #'TY - [⊢ fld ≫ fld- ⇐ τ_in] ... - -------- - [⊢ (C* fld- ...) ⇒ τ_out]]) - (define-typed-syntax (elim-Name A ... x P C* ...) ≫ - [⊢ A ≫ A- ⇐ k_in] ... - #:with ((~Π ([CA : Ck] ...) (~Π ([X : τ_in/X] ...) _)) ...) - #;((~Π ([_ : τ_in] ...) τ_out) ...) + (define-typed-syntax (elim-Name x P C* ...) ≫ + #:with ((~Π ([CA : Ck] ...) (~Π ([_ : τ_in] ...) _)) ...) (stx-map (current-type-eval) #'(TY ...)) - #:with ((τ_in ...) ...) - (stx-map (lambda (tins cas) (substs #'(A- ...) cas tins)) - #'((τ_in/X ...) ...) - #'((CA ...) ...)) - ;; [⊢ x ≫ x- ⇒ tyx] - ;; #:do[(displayln (stx->datum #'tyx))] - ;; [⊢ x ≫ _ ⇒ (Name-patexpand B ...)] - ;; #:do[(displayln (stx->datum #'(B ...)))] - [⊢ x ≫ x- ⇐ (Name A- ...)] - [⊢ P ≫ P- ⇐ (→ (Name A- ...) #%type)] ; prop / motive + ;; #:with ((τ_in ...) ...) + ;; (stx-map (lambda (tins cas) (substs #'(A- ...) cas tins)) + ;; #'((τ_in/X ...) ...) + ;; #'((CA ...) ...)) + [⊢ x ≫ x- ⇒ (Name-patexpand B ...)] +; [⊢ x ≫ x- ⇐ (Name A ...)] + [⊢ P ≫ P- ⇐ (Π ([A : k_in] ...) (→ (Name A ...) #%type))] ; prop / motive ; [⊢ z ≫ z- ⇐ (app P- Zero)] ; zero ; [⊢ C ≫ C- ⇐ (Π ([k : Nat]) (→ (app P- k) (app P- (Succ k))))] ; succ ;; TODO: the (app P- fld) ... is wrong, should only include recur args @@ -621,25 +613,46 @@ ;; 1) args of the tycon ;; 2) args of the con ;; 3) IH for each recursive arg - [⊢ C* ≫ C- ⇐ ;(Π ([CA : Ck] ...) - (Π ([fld : τ_in] ...) - (→ (app P- recur-fld) ... (app P- (app (app C A- ...) fld ...))))] ... + + ;; manually construct Cty, bc `syntax` isnt smart enough to figure out ellipses + #:with (Cty ...) + (stx-map + (lambda (CA-Cks CAs Cks fld-tins flds tins rflds c) + #`(Π #,CA-Cks + (Π #,fld-tins + (→ #,@(stx-map + (lambda (rf) #`(app (app P- #,@CAs) #,rf)) + rflds) + (app (app P- #,@CAs) (app (app #,c #,@CAs) #,@flds)))))) + #'(([CA : Ck] ...) ...) + #'((CA ...) ...) + #'((Ck ...) ...) + #'(([fld : τ_in] ...) ...) + #'((fld ...) ...) + #'((τ_in ...) ...) + #'((recur-fld ...) ...) + #'(C ...)) + [⊢ C* ≫ C- ⇐ Cty] ... + ;; [⊢ C* ≫ C- ⇐ (Π ([CA : Ck] ...) + ;; (Π ([fld : τ_in] ...) + ;; (→ (app (app P- CA ...) recur-fld) ... ; IHs + ;; (app (app P- CA ...) (app (app C CA ...) fld ...)))))] ... ----------- - [⊢ (match-Name A- ... x- P- C- ...) ⇒ (app P- x-)]) + [⊢ (match-Name x- P- C- ...) ⇒ (app (app P- B ...) x-)]) ; (struct match-Name/delayed (m)) (define-syntax match-Name (syntax-parser #;[(_ . args) #:do[(printf "trying to match:\n~a\n" (stx->datum #'args))] #:when #f #'(void)] - [(_ A ... n P Ccase ...) + [(_ n P Ccase ...) (syntax-parse #'n [((~literal #%plain-app) ((~literal #%plain-app) C-:id CA ...) fld ...) - ; #:do[(printf "matched ~a\n" #'C-)] + ; #:do[(printf "matched ~a\n" #'C-)] ;; TODO: check C- matches actual C ;; for now, it's just an arity match - #'(app/eval (app/eval Ccase fld ...) (match-Name A ... recur-fld P Ccase ...) ...)] ... - [_ #'(#%app match/delayed 'match-Name (void A ... n P Ccase ...))])])) + #'(app/eval (app/eval (app/eval Ccase CA ...) fld ...) (match-Name recur-fld P Ccase ...) ...)] ... + [_ #'(#%app match/delayed 'match-Name (void n P Ccase ...))])])) )]]) ;; ;; #:with res (if (typecheck? #'n- (expand/df #'Z)) ;; ;; #'z- diff --git a/turnstile/examples/tests/dep-ind-list-tests.rkt b/turnstile/examples/tests/dep-ind-list-tests.rkt index 5c74f37..3a762af 100644 --- a/turnstile/examples/tests/dep-ind-list-tests.rkt +++ b/turnstile/examples/tests/dep-ind-list-tests.rkt @@ -20,54 +20,54 @@ ;; length 0 (check-type - (elim-List Nat - ((null Nat)) - (λ ([l : (List Nat)]) Nat) - (λ () (λ () (Z))) - (λ ([x : Nat][xs : (List Nat)]) - (λ ([IH : Nat]) - (S IH)))) + (elim-List ((null Nat)) + (λ ([A : *]) (λ ([l : (List A)]) Nat)) + (λ ([A : *]) (λ () (λ () (Z)))) + (λ ([A : *]) + (λ ([x : A][xs : (List A)]) + (λ ([IH : Nat]) + (S IH))))) : Nat -> (Z)) ;; length 1 (check-type - (elim-List Nat - ((cons Nat) (Z) ((null Nat))) - (λ ([l : (List Nat)]) Nat) - (λ () (λ () (Z))) - (λ ([x : Nat][xs : (List Nat)]) - (λ ([IH : Nat]) - (S IH)))) + (elim-List ((cons Nat) (Z) ((null Nat))) + (λ ([A : *]) (λ ([l : (List A)]) Nat)) + (λ ([A : *]) (λ () (λ () (Z)))) + (λ ([A : *]) + (λ ([x : A][xs : (List A)]) + (λ ([IH : Nat]) + (S IH))))) : Nat -> (S (Z))) ;; length 2 (check-type - (elim-List Nat - ((cons Nat) (S (Z)) ((cons Nat) (Z) ((null Nat)))) - (λ ([l : (List Nat)]) Nat) - (λ () (λ () (Z))) - (λ ([x : Nat][xs : (List Nat)]) - (λ ([IH : Nat]) - (S IH)))) + (elim-List ((cons Nat) (S (Z)) ((cons Nat) (Z) ((null Nat)))) + (λ ([A : *]) (λ ([l : (List A)]) Nat)) + (λ ([A : *]) (λ () (λ () (Z)))) + (λ ([A : *]) + (λ ([x : A][xs : (List A)]) + (λ ([IH : Nat]) + (S IH))))) : Nat -> (S (S (Z)))) (define-type-alias len (λ ([lst : (List Nat)]) - (elim-List Nat - lst - (λ ([l : (List Nat)]) Nat) - (λ () (λ () (Z))) - (λ ([x : Nat][xs : (List Nat)]) - (λ ([IH : Nat]) - (S IH)))))) + (elim-List lst + (λ ([A : *]) (λ ([l : (List A)]) Nat)) + (λ ([A : *]) (λ () (λ () (Z)))) + (λ ([A : *]) + (λ ([x : A][xs : (List A)]) + (λ ([IH : Nat]) + (S IH))))))) (check-type (len ((null Nat))) : Nat -> (Z)) (check-type (len ((cons Nat) (Z) ((null Nat)))) : Nat -> (S (Z))) -;; ;; lists parameterized over length +;; ;; "lists" parameterized over length ;; (define-datatype Vect : (→ * Nat *) ;; [nil : (Π ([A : *][k : Nat]) (→ (Vect A (Z))))] ;; [cns : (Π ([A : *][k : Nat]) (→ A (Vect A k) (Vect A (S k))))])