From 2ddf7ce3520e408ded714db7972df921522b0147 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 20 Feb 2015 19:12:06 -0500 Subject: [PATCH] Fixed several bugs, found several more Trying to fix proofs for free examples; found several bugs but more still exist. Added TODOs --- proofs-for-free.rkt | 64 ++++++++++++++++++++++++--------------------- redex-curnel.rkt | 15 +++++++---- stdlib/sugar.rkt | 4 +-- 3 files changed, 45 insertions(+), 38 deletions(-) diff --git a/proofs-for-free.rkt b/proofs-for-free.rkt index 9815121..ac591d1 100644 --- a/proofs-for-free.rkt +++ b/proofs-for-free.rkt @@ -1,5 +1,6 @@ #lang s-exp "redex-curnel.rkt" -(require "stdlib/sugar.rkt" "stdlib/prop.rkt") +(require "stdlib/sugar.rkt" "stdlib/prop.rkt" racket/trace + (for-syntax racket/syntax)) ;; --------- (begin-for-syntax @@ -7,40 +8,42 @@ (format-id x "~a~a" x i))) (define-syntax (rename syn) - (syntax-case syn (Type forall Unv lambda :) - [(_ i ls Type) #'Type] - [(_ i ls (Unv n)) #'(Unv n)] - [(_ i (xr ...) (lambda (x : t) e)) - #'(lambda (x : (rename i (xr ...) t)) - (rename i (xr ... x) e))] - [(_ i (xr ...) (forall (x : t) e)) - #'(forall (x : (rename i (xr ...) t)) - (rename i (xr ... x) e))] - [(_ i ls (e1 e2)) - #'((rename i ls e1) (rename i ls e2))] - [(_ i ls x) - (if (member (syntax->datum #'x) (syntax->datum #'ls)) - #'x - (rename_id (syntax->datum #'i) #'x))])) + (syntax-case syn () + [(_ i ls e) + (syntax-case #`(ls #,(cur-expand #'e)) (Type forall Unv lambda :) + [(_ Type) #'Type] + [(_ (Unv n)) #'(Unv n)] + [((xr ...) (lambda (x : t) e)) + #'(lambda (x : (rename i (xr ...) t)) + (rename i (xr ... x) e))] + [((xr ...) (forall (x : t) e)) + #'(forall (x : (rename i (xr ...) t)) + (rename i (xr ... x) e))] + [(ls (e1 e2)) + #'((rename i ls e1) (rename i ls e2))] + [(ls x) + (if (member (syntax->datum #'x) (syntax->datum #'ls)) + #'x + (rename_id (syntax->datum #'i) #'x))])])) -(define-syntax (translate syn) - (syntax-parse (cur-expand syn) +(trace-define-syntax (translate syn) + (syntax-parse (cur-expand (syntax-case syn () [(_ e) #'e])) ;; TODO: Need to add these to a literal set and export it ;; Or, maybe redefine syntax-parse #:datum-literals (:) #:literals (lambda forall data real-app case Type) - [(_ Type) + [Type #'(lambda* (x1 : Type) (x2 : Type) (->* x1 x2 Type))] - [(_ (forall (x : A) B)) + [(forall (x : A) B) (let ([x1 (rename_id 1 #'x)] [x2 (rename_id 2 #'x)] [xr (rename_id 'r #'x)]) #`(lambda* (f1 : (rename 1 () (forall (x : A) B))) (f2 : (rename 2 () (forall (x : A) B))) (forall* (#,x1 : (rename 1 () A)) (#,x2 : (rename 2 () A)) - (#,xr : ((translate A) #,x1 #,x2)) + (#,xr : (run ((translate A) #,x1 #,x2))) ((translate B) (f1 #,x1) (f2 #,x2)))))] - [(_ (lambda (x : A) B)) + [(lambda (x : A) B) (let ([x1 (rename_id 1 #'x)] [x2 (rename_id 2 #'x)] [xr (rename_id 'r #'x)]) @@ -48,15 +51,15 @@ (f2 : (rename 2 () (forall (x : A) B))) (forall* (#,x1 : (rename 1 () A)) (#,x2 : (rename 2 () A)) - (#,xr : ((translate A) #,x1 #,x2)) + (#,xr : (run ((translate A) #,x1 #,x2))) ((translate B) (f1 #,x1) (f2 #,x2)))))] - [(_ (data id : t (c : tc) ...)) + [(data id : t (c : tc) ...) (let ([t #`(data #,(rename_id 'r #'id) : (translate t) ((translate c) : (translate tc)) ...)]) t)] - [(_ (f a)) + [(f a) #`((translate f) (rename 1 () a) (rename 2 () a) (translate a))] - [(_ x) + [x:id ;; TODO: Look up x and generate the relation. Otherwise I need to ;; manually translate all dependencies. ;; Not sure this is quite right; Racket's hygiene might `save' me. @@ -66,15 +69,16 @@ (define-type X Type) (define X1 X) (define X2 X) -(define (Xr (x1 : X) (x2 : X)) true) +(define (Xr (x1 : X1) (x2 : X2)) true) ;; The type of a CPS function (define-type CPSf (forall* (ans : Type) (k : (-> X ans)) ans)) (define (CPSf-relation (f1 : CPSf) (f2 : CPSf)) - ;; Run performs substitution, among other things, at compile. - (translate (run CPSf))) -(module+ test + ;; TODO: Fix run so I can simply use (run CPSf) to perform + ;; substitution + (translate (forall* (ans : Type) (k : (-> X ans)) ans))) +#;(module+ test (require rackunit) (check-equal? (translate (forall* (ans : Type) (k : (-> X ans)) ans)) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index da1e3e4..fe8b6ba 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -9,6 +9,8 @@ (provide (all-defined-out)) + (set-cache-size! 10000) + ;; References: ;; http://www3.di.uminho.pt/~mjf/pub/SFV-CIC-2up.pdf ;; https://www.cs.uoregon.edu/research/summerschool/summer11/lectures/oplss-herbelin1.pdf @@ -358,6 +360,7 @@ ----------------- "DTR-Inductive" (types Σ Γ x t)] + ;; TODO: Require alpha-equiv here, at least. [(where t (lookup Γ x)) ----------------- "DTR-Start" (types Σ Γ x t)] @@ -412,12 +415,12 @@ ;; searches it. ;; Perhaps something closer to Zombies = type would be better. ;; For now, reduce types - #;[(types Γ e (in-hole E t)) + #;[(types Σ Γ e (in-hole E t)) (where t_0 (in-hole E t)) (where t_1 ,(car (apply-reduction-relation* ==β (term t_0)))) - (types Γ t_1 U) + (types Σ Γ t_1 U) ----------------- "DTR-Conversion" - (types Γ e t_1)]) + (types Σ Γ e t_1)]) (module+ test (check-true (judgment-holds (types ∅ ∅ (Unv 0) (Unv 1)))) (check-true (judgment-holds (types ∅ (∅ x : (Unv 0)) (Unv 0) (Unv 1)))) @@ -693,8 +696,8 @@ (define (core-expand syn) (disarm (local-expand syn 'expression - (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case - Unv #%datum)))))) + (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case + Unv #%datum)))))) ;; Only type-check at the top-level, to prevent exponential ;; type-checking. Redex is expensive enough. @@ -764,6 +767,8 @@ dep-fix dep-forall dep-var)) ls))))) + ;; TODO: OOps, run doesn't return a cur term but a redex term + ;; wrapped in syntax bla. This is bad. (define-syntax (run syn) (syntax-case syn () [(_ expr) (normalize/syn #'expr)])) diff --git a/stdlib/sugar.rkt b/stdlib/sugar.rkt index 8a5affb..a3ed30b 100644 --- a/stdlib/sugar.rkt +++ b/stdlib/sugar.rkt @@ -18,9 +18,7 @@ (define-syntax (-> syn) (syntax-case syn () - [(_ t1 t2) - (with-syntax ([(x) (generate-temporaries '(1))]) - #`(forall (x : t1) t2))])) + [(_ t1 t2) #`(forall (#,(gensym) : t1) t2)])) (define-syntax ->* (syntax-rules ()