From b79e64523a9d63494d5f8b66c9cd1eb87854e226 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Fri, 30 Jan 2015 17:55:09 -0500 Subject: [PATCH] Reflection, now with the ability to run code! --- nat.rkt | 3 -- oll.rkt | 16 +++--- redex-curnel.rkt | 125 +++++++++++++++++++++++++++++------------------ sugar.rkt | 3 +- 4 files changed, 87 insertions(+), 60 deletions(-) diff --git a/nat.rkt b/nat.rkt index e24f36e..da9d29c 100644 --- a/nat.rkt +++ b/nat.rkt @@ -31,6 +31,3 @@ (module+ test (check-equal? (plus z z) z) (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z)))))) - -(add1 (s z)) -(sub1 (s z)) diff --git a/oll.rkt b/oll.rkt index 4e45489..13e904e 100644 --- a/oll.rkt +++ b/oll.rkt @@ -166,13 +166,14 @@ (begin-for-syntax (define (output-coq syn) (syntax-parse (cur-expand syn) - [((~literal lambda) ~! (x:id (~datum :) t) body:expr) + #:literals (lambda forall data real-app case) + [(lambda ~! (x:id (~datum :) t) body:expr) (format "(fun ~a : ~a => ~a)" (syntax-e #'x) (output-coq #'t) (output-coq #'body))] - [((~literal forall) ~! (x:id (~datum :) t) body:expr) + [(forall ~! (x:id (~datum :) t) body:expr) (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t) (output-coq #'body))] - [((~literal data) ~! n:id (~datum :) t (x*:id (~datum :) t*) ...) + [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...) (format "Inductive ~a : ~a :=~n~a." (syntax-e #'n) (output-coq #'t) @@ -187,11 +188,8 @@ #:left? #f))] ;; TODO: Add "case". Will be slightly tricky since the syntax is ;; quite different from Coq. - [(e1 e* ...) - (format "(~a~a)" (output-coq #'e1) - (for/fold ([strs ""]) - ([arg (syntax->list #'(e* ...))]) - (format "~a ~a" strs (output-coq arg))))] + [(real-app e1 e2) + (format "(~a ~a)" (output-coq #'e1) (output-coq #'e2))] [e:id (format "~a" (syntax->datum #'e))]))) (define-syntax (generate-coq syn) @@ -222,5 +220,5 @@ "Inductive meow : (forall temp. : gamma, (forall temp. : term, (forall temp. : type, Type))) :=" (first (string-split t "\n"))) (check-regexp-match - "T-Bla : (forall g : gamma, (forall e : term, (forall t : type, (meow g e t))))\\." + "T-Bla : (forall g : gamma, (forall e : term, (forall t : type, (((meow g) e) t))))\\." (second (string-split t "\n")))))) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index 0475a26..ad3535e 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -32,21 +32,7 @@ (module+ test (require rackunit) - ;; TODO: Rename these signatures, and use them in all future tests. - (define Σ (term (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)))) - - (define Σ0 (term ∅)) - (define Σ2 (term (((∅ nat : Type) z : nat) s : (Π (x : nat) nat)))) - (define Σ3 (term (∅ and : (Π (A : Type) (Π (B : Type) Type))))) - (define Σ4 (term (,Σ3 conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((and A) B)))))))) - (define Σ? (redex-match? cic-typingL Σ)) - - (check-true (Σ? Σ0)) - (check-true (Σ? Σ2)) - (check-true (Σ? Σ4)) - (check-true (Σ? Σ3)) - (check-true (Σ? Σ4)) - (check-true (x? (term T))) + (check-true (x? (term T))) (check-true (x? (term truth))) (check-true (x? (term zero))) (check-true (x? (term s))) @@ -130,6 +116,12 @@ ;; NB: ;; TODO: Why do I not have tests for substitutions?!?!?!?!?!?!?!!?!?!?!?!?!?!!??!?! + (define-metafunction cicL + subst-all : t (x ...) (e ...) -> t + [(subst-all t () ()) t] + [(subst-all t (x_0 x ...) (e_0 e ...)) + (subst-all (subst t x_0 e_0) (x ...) (e ...))]) + (define-extended-language cic-redL cicL (E hole (E t) (case E (x e) ...))) @@ -190,6 +182,23 @@ (define-extended-language cic-typingL cicL (Σ Γ ::= ∅ (Γ x : t))) + (define Σ? (redex-match? cic-typingL Σ)) + (define Γ? (redex-match? cic-typingL Γ)) + (module+ test + ;; TODO: Rename these signatures, and use them in all future tests. + (define Σ (term (((∅ nat : Type) zero : nat) s : (Π (x : nat) nat)))) + + (define Σ0 (term ∅)) + (define Σ2 (term (((∅ nat : Type) z : nat) s : (Π (x : nat) nat)))) + (define Σ3 (term (∅ and : (Π (A : Type) (Π (B : Type) Type))))) + (define Σ4 (term (,Σ3 conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) ((and A) B)))))))) + + (check-true (Σ? Σ0)) + (check-true (Σ? Σ2)) + (check-true (Σ? Σ4)) + (check-true (Σ? Σ3)) + (check-true (Σ? Σ4))) + (define-metafunction cic-typingL append-env : Γ Γ -> Γ [(append-env Γ ∅) Γ] @@ -684,14 +693,14 @@ (define gamma (make-parameter (term ∅) (lambda (x) - (unless (redex-match? cic-typingL Γ x) + (unless (Γ? x) (error 'core-error "We built a bad gamma ~s" x)) x))) (define sigma (make-parameter (term ∅) (lambda (x) - (unless (redex-match? cic-typingL Σ x) + (unless (Σ? x) (error 'core-error "We built a bad sigma ~s" x)) x))) @@ -705,6 +714,13 @@ (define (extend-env/syn! env x t) (env (extend-env/syn env x t))) + (define bind-subst (make-parameter (list null null))) + + (define (add-binding/term! x t) + (let ([vars (first (bind-subst))] + [exprs (second (bind-subst))]) + (bind-subst (list (cons x vars) (cons t exprs))))) + ;; TODO: Still absurdly slow. Probably doing n^2 checks of sigma and ;; gamma. And lookup on sigma, gamma are linear, so probably n^2 lookup time. (define (type-infer/term t) @@ -713,11 +729,12 @@ (define (syntax->curnel-syntax syn) (denote syn (cur->datum syn))) - (define (denote syn t) #`(term (reduce #,(datum->syntax syn t)))) + (define (denote syn t) + #`(term (reduce (subst-all #,(datum->syntax syn t) #,(first (bind-subst)) #,(second (bind-subst)))))) ;; TODO: Blanket disarming is probably a bad idea. (define orig-insp (variable-reference->module-declaration-inspector - (#%variable-reference))) + (#%variable-reference))) (define (disarm syn) (syntax-disarm syn orig-insp)) ;; Locally expand everything down to core forms. @@ -726,7 +743,7 @@ (if (identifier? syn) syn (local-expand syn 'expression - (append (syntax-e #'(term reduce dep-var #%app λ Π μ case + (append (syntax-e #'(term reduce subst-all dep-var #%app λ Π μ case Type))))))) ;; Only type-check at the top-level, to prevent exponential @@ -742,10 +759,11 @@ (parameterize ([inner-expand? #t]) (let cur->datum ([syn syn]) (syntax-parse (core-expand syn) - #:literals (term reduce #%app) + #:literals (term reduce #%app subst-all) #:datum-literals (case Π λ μ : Type) [x:id (syntax->datum #'x)] - [(reduce e) (syntax->datum #'e)] + [(subst-all e _ _) (syntax->datum #'e)] + [(reduce e) (cur->datum #'e)] [(term e) (cur->datum #'e)] ;; TODO: should really check that b is one of the binders ;; Maybe make a syntax class for the binders, core forms, @@ -819,13 +837,13 @@ #`(extend-env/term! #,env #,(export-out-sym e) #,t)))) ~cur)])))) - (define-syntax (export-gamma syn) + (define-syntax (export-envs syn) (syntax-case syn () - [(_ name) #`(begin-for-syntax (define name (term #,(gamma))))])) - - (define-syntax (export-sigma syn) - (syntax-case syn () - [(_ name) #`(begin-for-syntax (define name (term #,(sigma))))])) + [(_ gamma-out sigma-out bind-out) + #`(begin-for-syntax + (define gamma-out (term #,(gamma))) + (define sigma-out (term #,(sigma))) + (define bind-out '#,(bind-subst)))])) (define-syntax (dep-provide syn) (syntax-case syn () @@ -837,18 +855,16 @@ ;; TODO: rename out will need to rename variables in gamma and ;; sigma. (syntax-local-lift-module-end-declaration - #`(export-gamma gamma-out)) - (syntax-local-lift-module-end-declaration - #`(export-sigma sigma-out)) + #`(export-envs gamma-out sigma-out bind-out)) #`(provide (extend-env-and-provide e ...) - (for-syntax gamma-out sigma-out)))])) + (for-syntax gamma-out sigma-out bind-out)))])) (begin-for-syntax - (define out-gammas - #`()) - (define out-sigmas - #`()) + (define out-gammas #`()) + (define out-sigmas #`()) + (define out-binds #`()) (define gn 0) (define sn 0) + (define bn 0) (define (filter-cur-imports syn) (for/fold ([imports '()] [sources '()]) @@ -882,6 +898,22 @@ ,#,new-id))))) (cons (struct-copy import imp [local-id new-id]) imports))] + ;; TODO: Many shared code between these two clauses + [(equal? (import-src-sym imp) 'bind-out) + (let ([new-id (format-id (import-orig-stx imp) + "bind-out~a" bn)]) + ;; TODO: Fewer set!s + ;; TODO: Do not DIY gensym + (set! bn (add1 bn)) + (set! out-binds + #`(#,@out-binds (bind-subst (list (append + (first #,new-id) + (first (bind-subst))) + (append + (second #,new-id) + (second (bind-subst))))))) + (cons (struct-copy import imp [local-id new-id]) + imports))] [else (cons imp imports)])) (append sources more-sources)))))) @@ -892,21 +924,17 @@ ;; TODO: rename in will need to rename variables in gamma and ;; sigma. - (define-syntax (update-gammas syn) + (define-syntax (import-envs syn) (syntax-case syn () - [(_) #`(begin-for-syntax #,@out-gammas)])) - (define-syntax (update-sigmas syn) - (syntax-case syn () - [(_) #`(begin-for-syntax #,@out-sigmas)])) - + [(_) #`(begin-for-syntax #,@out-gammas #,@out-sigmas + #,@out-binds)])) (define-syntax (dep-require syn) (syntax-case syn () [(_ e ...) #`(begin (require (extend-env-and-require e ...)) - (update-gammas) - (update-sigmas))])) + (import-envs))])) (define-syntax (dep-module+ syn) (syntax-case syn () @@ -914,7 +942,8 @@ #`(module+ name (begin-for-syntax (gamma (term #,(gamma))) - (sigma (term #,(sigma)))) + (sigma (term #,(sigma))) + (bind-subst '#,(bind-subst))) body ...)])) ;; ----------------------------------------------------------------- @@ -969,8 +998,10 @@ ;; TODO: Can't actually run programs until I do something about ;; #'e. Maybe denote final terms into Racket. Or keep an ;; environment and have denote do a giant substitution - (let () #;[t (core-expand #'e)] - (extend-env/syn! gamma #'id (type-infer/syn #'e)) + (let ([e (cur->datum #'e)] + [id (syntax->datum #'id)]) + (extend-env/term! gamma id (type-infer/term e)) + (add-binding/term! id e) #'(void))]))) (require 'sugar) diff --git a/sugar.rkt b/sugar.rkt index 3fa05bf..7cc0715 100644 --- a/sugar.rkt +++ b/sugar.rkt @@ -7,7 +7,8 @@ define case* define-theorem - qed) + qed + real-app) (require (only-in "redex-curnel.rkt" [#%app real-app] [define real-define]))