From 26ac41f10425547fdd8091be9e353b5bfea08954 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Sat, 31 Jan 2015 00:43:07 -0500 Subject: [PATCH] Splitting modules and cleaning up; most tests pass * Split prop, nat, bool, maybe, and stlc into modules * Reverted proofs-for-free stuff to the pre-me-fucking-about version, and cleaned it up. * Fixed redex-curnel test suite. Redefinition of module+ was causing issues. * Moved various var stuff to oll. * Moved stlc examples to seperate module. --- bool.rkt | 19 +++++ maybe.rkt | 7 ++ nat.rkt | 18 ++++- oll.rkt | 81 +++----------------- proofs-for-free-v2.rkt | 169 ----------------------------------------- proofs-for-free.rkt | 100 ++++++++++++++++++++++++ prop.rkt | 61 +++++++++++++++ redex-curnel.rkt | 22 ++++-- stlc.rkt | 131 ++++++++++++++++++++++++++++++++ sugar.rkt | 17 ++++- 10 files changed, 376 insertions(+), 249 deletions(-) create mode 100644 bool.rkt create mode 100644 maybe.rkt delete mode 100644 proofs-for-free-v2.rkt create mode 100644 proofs-for-free.rkt create mode 100644 prop.rkt create mode 100644 stlc.rkt diff --git a/bool.rkt b/bool.rkt new file mode 100644 index 0000000..b2f188f --- /dev/null +++ b/bool.rkt @@ -0,0 +1,19 @@ +#lang s-exp "redex-curnel.rkt" +(provide bool btrue bfalse if bnot) + +(data bool : Type + (btrue : bool) + (bfalse : bool)) + +(define-syntax (if syn) + (syntax-case syn () + [(_ t s f) + #'(case t + [btrue s] + [bfalse f])])) + +(define (bnot (x : bool)) (if x bfalse btrue)) +(module+ test + (require rackunit) + (check-equal? (bnot btrue) bfalse) + (check-equal? (bnot bfalse) btrue)) diff --git a/maybe.rkt b/maybe.rkt new file mode 100644 index 0000000..5640ff2 --- /dev/null +++ b/maybe.rkt @@ -0,0 +1,7 @@ +#lang s-exp "redex-curnel.rkt" +(require "sugar.rkt") +(provide maybe none some) + +(data maybe : (forall (A : Type) Type) + (none : (forall (A : Type) (maybe A))) + (some : (forall* (A : Type) (a : A) (maybe A)))) diff --git a/nat.rkt b/nat.rkt index da9d29c..7cd02ed 100644 --- a/nat.rkt +++ b/nat.rkt @@ -1,8 +1,8 @@ #lang s-exp "redex-curnel.rkt" -(require "sugar.rkt") +(require "sugar.rkt" "bool.rkt") ;; TODO: override (all-defined-out) to enable exporting all these ;; properly. -(provide nat z s add1 sub1 plus) +(provide nat z s add1 sub1 plus nat-equal?) (module+ test (require rackunit)) @@ -31,3 +31,17 @@ (module+ test (check-equal? (plus z z) z) (check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z)))))) + +(define-rec (nat-equal? (n1 : nat) (n2 : nat) : bool) + (case* n1 + [z (case* n2 + [z btrue] + [(s (n3 : nat)) bfalse])] + [(s (n3 : nat)) + (case* n2 + [z btrue] + [(s (n4 : nat)) (nat-equal? n3 n4)])])) +(module+ test + (check-equal? btrue (nat-equal? z z)) + (check-equal? bfalse (nat-equal? z (s z))) + (check-equal? btrue (nat-equal? (s z) (s z)))) diff --git a/oll.rkt b/oll.rkt index 68c037e..1906dbe 100644 --- a/oll.rkt +++ b/oll.rkt @@ -2,9 +2,9 @@ ;; OLL: The OTT-Like Library ;; TODO: Add latex extraction ;; TODO: Automagically create a parser from bnf grammar -(require "sugar.rkt" "nat.rkt") +(require "sugar.rkt" "nat.rkt" racket/trace) -(provide define-relation define-language var avar) +(provide define-relation define-language var avar var-equal?) (begin-for-syntax (define-syntax-class dash @@ -128,7 +128,7 @@ ;; TODO: For better error messages, add context, rename some of these patterns. e.g. ;; (type (meta-vars) ::= ?? ) (define-syntax (define-language syn) - (syntax-parse syn +(syntax-parse syn [(_ name:id (~do (lang-name #'name)) (~do (nts (hash-set (make-immutable-hash) 'var #'var))) (~optional (~seq #:vars (x*:id ...) @@ -140,79 +140,22 @@ (data var : Type (avar : (-> nat var))) -;;Type this: +(define (var-equal? (v1 : var) (v2 : var)) + (case* v1 + [(avar (n1 : nat)) + (case* v2 + [(avar (n2 : nat)) + (nat-equal? n1 n2)])])) -(define-language stlc - #:vars (x) - (val (v) ::= true false) - (type (A B) ::= bool (-> A B)) - (term (e) ::= x v (e e) (lambda (x : A) e) (cons e e) - (let (x x) = e in e))) - -;;This gets generated: - -#; -(begin - (data stlc-val : Type - (stlc-true : stlc-val) - (stlc-false : stlc-val)) - - (data stlc-type : Type - (stlc-bool : stlc-type) - (stlc--> : (->* stlc-type stlc-type stlc-type))) - - (data stlc-term : Type - (var-->-stlc-term : (-> var stlc-term)) - (stlc-val-->-stlc-term : (-> stlc-val stlc-term)) - (stlc-term2151 : (->* stlc-term stlc-term stlc-term)) - (stlc-lambda : (->* var stlc-type stlc-term stlc-term)) - (stlc-cons : (->* stlc-term stlc-term stlc-term)) - (stlc-let : (->* var var stlc-term stlc-term)))) - -;; Define inference rules in a more natural notation, like so: -#; -(define-relation (has-type gamma term type) - [(g : gamma) - ------------------------ T-Unit - (has-type g unitv Unit)] - - [(g : gamma) (x : var) (t : type) - (== (maybe type) (lookup-gamma g x) (some type t)) - ------------------------ T-Var - (has-type g (tvar x) t)] - - [(g : gamma) (e1 : term) (e2 : term) (t1 : type) (t2 : type) - (has-type g e1 t1) - (has-type g e2 t2) - ---------------------- T-Pair - (has-type g (pair e1 e2) (Pair t1 t2))] - - [(g : gamma) (e : term) (t1 : type) (t2 : type) - (has-type g e (Pair t1 t2)) - ----------------------- T-Prj1 - (has-type g (prj z e) t1)] - - [(g : gamma) (e : term) (t1 : type) (t2 : type) - (has-type g e (Pair t1 t2)) - ----------------------- T-Prj2 - (has-type g (prj (s z) e) t1)] - - [(g : gamma) (e1 : term) (t1 : type) (t2 : type) (x : var) - (has-type (extend-gamma g x t1) e1 t2) - ---------------------- T-Fun - (has-type g (lam x t1 e1) (Fun t1 t2))] - - [(g : gamma) (e1 : term) (e2 : term) (t1 : type) (t2 : type) - (has-type g e1 (Fun t1 t2)) - (has-type g e2 t1) - ---------------------- T-App - (has-type g (app e1 e2) t2)]) +;; See stlc.rkt for examples ;; Generate Coq from Cur: (begin-for-syntax (define (output-coq syn) (syntax-parse (cur-expand syn) + ;; TODO: Need to add these to a literal set and export it + ;; Or, maybe overwrite syntax-parse #: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) diff --git a/proofs-for-free-v2.rkt b/proofs-for-free-v2.rkt deleted file mode 100644 index 1e24160..0000000 --- a/proofs-for-free-v2.rkt +++ /dev/null @@ -1,169 +0,0 @@ -#lang s-exp "redex-curnel.rkt" -;; Ignore this file. -(require rackunit racket/trace (for-syntax racket/syntax)) - -;; TODO: Move to standard library -(define-syntax (-> syn) - (syntax-case syn () - [(_ t1 t2) - (with-syntax ([(x) (generate-temporaries '(1))]) - #'(forall (x : t1) t2))])) - -(define-syntax ->* - (syntax-rules () - [(->* a) a] - [(->* a a* ...) - (-> a (->* a* ...))])) - -(define-syntax forall* - (syntax-rules (:) - [(_ (a : t) (ar : tr) ... b) - (forall (a : t) - (forall* (ar : tr) ... b))] - [(_ b) b])) - -(define-syntax lambda* - (syntax-rules (:) - [(_ (a : t) (ar : tr) ... b) - (lambda (a : t) - (lambda* (ar : tr) ... b))] - [(_ b) b])) - -(define-syntax-rule (define-theorem name prop) - (define (name (x : prop)) T)) - -(define-syntax-rule (qed thm pf) - (check-equal? T (thm pf))) - -(define-syntax (define-type syn) - (syntax-case syn (:) - [(_ (name (x : t) ...) e) - #'(define name (forall* (x : t) ... e))] - [(_ id e) - #'(define id e)])) - -;; --------- - -(data true : Type (T : true)) -(data false : Type) -(data equal : (forall* (A : Type) (B : Type) Type)) -(data * : (forall* (a : Type) (b : Type) Type) - (prod : (forall* (a : Type) (b : Type) (* a b)))) -;; --------- -(begin-for-syntax - (define (rename_id i x) - (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))])) -(define-syntax (translate syn) - (syntax-case syn (_t _v Type forall Unv lambda : data) - [(_ _t Type) - #'(lambda* (x1 : Type) (x2 : Type) (->* x1 x2 Type))] - [(_ _v Type) - #'(lambda* (x1 : Type) (x2 : Type) (equal x1 x2))] - [(_ e (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 _t A) #,x1 #,x2)) - ((translate e B) (f1 #,x1) (f2 #,x2)))))] - [(_ e (lambda (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 _t A) #,x1 #,x2)) - ((translate e B) (f1 #,x1) (f2 #,x2)))))] - [(_ e (data id : t (c : tc) ...)) - (let ([t #`(data #,(rename_id 'r #'id) : (translate e t) - ((translate e c) : (translate e tc)) ...) ]) - t)] - [(_ e (f a)) - #`((translate e f) (rename 1 () a) (rename 2 () a) (translate e a))] - [(_ e x) - ;; Not sure this is quite right; Racket's hygiene might `save' me. - (rename_id 'r #'x)] - [_ (raise-syntax-error "translate undefined for" syn)])) - -(define-theorem thm:type_t ((translate _t Type) Type Type)) -(qed thm:type_t (translate _v Type)) -(translate _v Type) -((translate _t Type) Type Type) - -((translate _v Type) true false) - -#;(define true1 true) -#;(define true2 true) - -(data nat : Type - (z : nat) - (s : (-> nat nat))) - -(define nat1 nat) -(define nat2 nat) -(define natr (lambda* (n1 : nat) (n2 : nat) true)) - -(data heap : Type) -(define heap1 heap) -(define heap2 heap) -(data heap-equal : (forall* (h1 : heap) (h2 : heap) Type)) -(define heapr natr) - -(define-type (pre (h : heap)) Type) -(define pre1 pre) -(define pre2 pre) -(define prer (translate _v (forall (h : heap) Type))) -prer - -(define-type (monad (s : pre) - (tp : (-> pre Type)) - (unit : (forall (x : nat) (tp (lambda (h : heap) true))))) - (-> heap (tp s))) - -#;(define monad-type - (forall (s : pre) - (forall (tp : (forall (p : pre) Type)) - (forall (unit : (forall (x : nat) (tp (lambda (h : heap) - true)))) - (forall (h : heap) (tp s)))))) -;monad-type -#;(translate _v (forall (s : pre) - (forall (tp : (forall (p : pre) Type)) - (forall (unit : (forall (x : nat) (tp (lambda (h : heap) true)))) - (forall (h : heap) (tp s)))))) -;; and : (forall (A : Type) (B : Type) Type) -(data and : (forall* (A : Type) (B : Type) Type) - (conj : (forall* (A : Type) (B : Type) (a : A) (b : B) (and A B)))) -((translate _v (forall (A : Type) (forall (B : Type) Type))) and and) -;; conj : (forall (A : Type) (B : Type) (a : A) (b : B) (and A B)) -((translate _v (forall (A : Type) (forall (B : Type) - (forall (a : A) (forall (b : - B) - ((and - A) - B)))))) - conj conj) - -(translate _v T) -((translate _v true) T T) -((translate _v Type) true true) diff --git a/proofs-for-free.rkt b/proofs-for-free.rkt new file mode 100644 index 0000000..91e2af4 --- /dev/null +++ b/proofs-for-free.rkt @@ -0,0 +1,100 @@ +#lang s-exp "redex-curnel.rkt" +(require "sugar.rkt" "prop.rkt") + +;; --------- +(begin-for-syntax + (define (rename_id i x) + (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))])) + +(define-syntax (translate syn) + (syntax-parse (cur-expand syn) + ;; TODO: Need to add these to a literal set and export it + ;; Or, maybe redefine syntax-parse + #:literals (lambda forall data real-app case Type) + [(_ Type) + #'(lambda* (x1 : Type) (x2 : Type) (->* x1 x2 Type))] + [(_ (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)) + ((translate B) (f1 #,x1) (f2 #,x2)))))] + [(_ (lambda (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)) + ((translate B) (f1 #,x1) (f2 #,x2)))))] + [(_ (data id : t (c : tc) ...)) + (let ([t #`(data #,(rename_id 'r #'id) : (translate t) + ((translate c) : (translate tc)) ...)]) + t)] + [(_ (f a)) + #`((translate f) (rename 1 () a) (rename 2 () a) (translate a))] + [(_ x) + ;; 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. + (rename_id 'r #'x)] + [_ (raise-syntax-error "translate undefined for" syn)])) + +(define-type X Type) +(define X1 X) +(define X2 X) +(define (Xr (x1 : X) (x2 : X)) true) + +;; The type of a CPS function +(define-type CPSf (forall* (ans : Type) (k : (-> X ans)) ans)) + +(define (CPSf-relation (f1 : CPSf) (f2 : CPSf)) + (translate (forall* (ans : Type) (k : (-> X ans)) ans)) +(module+ test + (require rackunit) + (check-equal? + (translate (forall* (ans : Type) (k : (-> X ans)) ans)) + (forall* (ans1 : Type) (ans2 : Type) (ansr : (->* ans1 ans2 Type)) + (forall* (k1 : (-> X ans1)) (k2 : (-> X ans2)) + (kr : (forall* (_1 : X) (_2 : X) (_r : (Xr _1 _2)) + (ansr (k1 _1) (k2 _2)))) + (ansr (f1 ans1 k1) (f2 ans2 k2))))))) + +;; By parametricity, every CPSf is related it itself in the CPS relation +(define-type paramCPSf (forall* (f : CPSf) (CPSf-relation f f))) +(define (id (X : Type) (x : X)) x) + +(define-theorem thm:cont-shuffle + (forall* (f : CPSf) + (ans : Type) + (ansr : (-> ans ans Type)) + (k : (-> X ans)) + (ansr (f ans k) (k (f ans (id ans)))))) + +#;(define (rel (x1 : X) (x2 : X)) + (and (Xr x1 x2) + )) + +#;(paramCPSf f X X rel k k) diff --git a/prop.rkt b/prop.rkt new file mode 100644 index 0000000..4a533e4 --- /dev/null +++ b/prop.rkt @@ -0,0 +1,61 @@ +#lang s-exp "redex-curnel.rkt" +(require "sugar.rkt") +;; TODO: Handle multiple provide forms properly +;; TODO: Handle (all-defined-out) properly +(provide + true T + thm:anything-implies-true + false + not + and + conj + thm:any-is-symmetric proof:and-is-symmetric + thm:proj1 proof:proj1 + thm:proj2 proof:proj2 + == refl) + +(data true : Type (T : true)) + +(define-theorem thm:anything-implies-true (forall (P : Type) true)) + +(qed (run thm:anything-implies-true) (lambda (P : Type) T)) + +(data false : Type) + +(define-type (not (A : Type)) (-> A false)) + +(data and : (forall* (A : Type) (B : Type) Type) + (conj : (forall* (A : Type) (B : Type) + (x : A) (y : B) (and A B)))) + +(define-theorem thm:and-is-symmetric + (forall* (P : Type) (Q : Type) (ab : (and P Q)) (and Q P))) + +;; TODO: BAH! pattern matching on inductive families is still broken. +(define proof:and-is-symmetric + (lambda* (P : Type) (Q : Type) (ab : (and P Q)) + (case* ab + ((conj (P : Type) (Q : Type) (x : P) (y : Q)) (conj Q P y x))))) + +#;(qed thm:and-is-symmetric proof:and-is-symmetric) + +(define-theorem thm:proj1 + (forall* (A : Type) (B : Type) (c : (and A B)) A)) + +(define proof:proj1 + (lambda* (A : Type) (B : Type) (c : (and A B)) + (case c (conj (lambda* (A : Type) (B : Type) (a : A) (b : B) a))))) + +(qed thm:proj1 proof:proj1) + +(define-theorem thm:proj2 + (forall* (A : Type) (B : Type) (c : (and A B)) B)) + +(define proof:proj2 + (lambda* (A : Type) (B : Type) (c : (and A B)) + (case c (conj (lambda* (A : Type) (B : Type) (a : A) (b : B) b))))) + +(qed thm:proj2 proof:proj2) + +(data == : (forall* (A : Type) (x : A) (-> A Type)) + (refl : (forall* (A : Type) (x : A) (== A x x)))) diff --git a/redex-curnel.rkt b/redex-curnel.rkt index ad3535e..9213f58 100644 --- a/redex-curnel.rkt +++ b/redex-curnel.rkt @@ -32,7 +32,7 @@ (module+ test (require rackunit) - (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))) @@ -46,8 +46,7 @@ (check-true (e? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (v? (term (λ (x_0 : (Unv 0)) x_0)))) (check-true (t? (term (λ (x_0 : (Unv 0)) x_0)))) - (check-true (t? (term (λ (x_0 : (Unv 0)) x_0)))) - ) + (check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))) ;; 'A' ;; Types of Universes @@ -165,6 +164,7 @@ (check-equal? (term (reduce Type)) (term Type)) (check-equal? (term (reduce ((λ (x : t) x) Type))) (term Type)) (check-equal? (term (reduce ((Π (x : t) x) Type))) (term Type)) + ;; NB: Currently not reducing under binders. I forget why. (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) Type)))) (term (Π (x : t) Type))) (check-equal? (term (reduce (Π (x : t) ((Π (x_0 : t) x_0) x)))) @@ -667,7 +667,8 @@ cur-expand type-infer/syn type-check/syn? - normalize/syn)) + normalize/syn) + run) (begin-for-syntax (current-trace-notify @@ -799,13 +800,18 @@ (let ([t (type-infer/term (cur->datum syn))]) (equal? t (cur->datum type)))) - (define (normalize/syn syn) (denote syn (term (reduce (cur->datum syn))))) + (define (normalize/syn syn) + (denote syn (term (reduce (subst-all ,(cur->datum syn) ,(first (bind-subst)) ,(second (bind-subst))))))) (define (cur-expand syn) (disarm (local-expand syn 'expression (syntax-e #'(Type dep-inductive dep-case dep-lambda dep-app dep-fix dep-forall dep-var)))))) + (define-syntax (run syn) + (syntax-case syn () + [(_ expr) (normalize/syn #'expr)])) + ;; ----------------------------------------------------------------- ;; Require/provide macros @@ -845,6 +851,8 @@ (define sigma-out (term #,(sigma))) (define bind-out '#,(bind-subst)))])) + ;; TODO: This can only handle a single provide form, otherwise + ;; generates multiple *-out (define-syntax (dep-provide syn) (syntax-case syn () [(_ e ...) @@ -1004,7 +1012,7 @@ (add-binding/term! id e) #'(void))]))) -(require 'sugar) +(require (rename-in 'sugar [module+ dep-module+])) (provide (all-from-out 'sugar)) -#;(module+ test +(module+ test (require (submod ".." core test))) diff --git a/stlc.rkt b/stlc.rkt new file mode 100644 index 0000000..c09206a --- /dev/null +++ b/stlc.rkt @@ -0,0 +1,131 @@ +#lang s-exp "redex-curnel.rkt" +(require racket/trace "nat.rkt" "sugar.rkt" "oll.rkt" "maybe.rkt") + +(define-language stlc + #:vars (x) + (val (v) ::= true false unit) + ;; TODO: Allow datum as terminals + (type (A B) ::= boolty unitty (-> A B) (* A A)) + (term (e) ::= x v (app e e) (lambda (x : A) e) (cons e e) + (let (x x) = e in e))) +;; A parser. +;; TODO: We should be able to generate these +;; TODO: When generating a parser, will need something like (#:name app (e e)) +;; so I can name a constructor without screwing with syntax. +(begin-for-syntax + (define index #'z)) +(define-syntax (begin-stlc syn) + (set! index #'z) + (let stlc ([syn (syntax-case syn () [(_ e) #'e])]) + (syntax-parse syn + #:datum-literals (lambda : prj * -> quote let in cons bool) + [(lambda (x : t) e) + (let ([oldindex index]) + (set! index #`(s #,index)) + ;; Replace x with a de bruijn index, by running a CIC term at + ;; compile time. + (normalize/syn + #`((lambda* (x : stlc-term) + (stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e))) + (var-->-stlc-term (avar #,oldindex)))))] + [(quote (e1 e2)) + #`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))] + [(let (x y) = e1 in e2) + (let* ([y index] + [x #`(s #,y)]) + (set! index #`(s (s #,index))) + #`((lambda* (x : stlc-term) (y : stlc-term) + (stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1) + #,(stlc #'e2))) + (var-->-stlc-term (avar #,x)) + (var-->-stlc-term (avar #,y)))) + #`(let x i #,(stlc #'e1))] + [(e1 e2) + #`(stlc-app #,(stlc #'e1) #,(stlc #'e2))] + [() #'(stlc-val-->-stlc-term stlc-unit)] + [#t #'(stlc-val-->-stlc-term stlc-true)] + [#f #'(stlc-val-->-stlc-term stlc-false)] + [(t1 * t2) + #`(stlc-* #,(stlc #'t1) #,(stlc #'t2))] + [(t1 -> t2) + #`(stlc--> #,(stlc #'t1) #,(stlc #'t2))] + [bool #`stlc-boolty] + [e + (if (eq? 1 (syntax->datum #'e)) + #'stlc-unitty + #'e)]))) + +(module+ test + (require rackunit) + (check-equal? + (begin-stlc (lambda (x : 1) x)) + (stlc-lambda (avar z) stlc-unitty (var-->-stlc-term (avar z)))) + (check-equal? + (begin-stlc ((lambda (x : 1) x) ())) + (stlc-app (stlc-lambda (avar z) stlc-unitty (var-->-stlc-term (avar z))) + (stlc-val-->-stlc-term stlc-unit))) + (check-equal? + (begin-stlc '(() ())) + (stlc-cons (stlc-val-->-stlc-term stlc-unit) + (stlc-val-->-stlc-term stlc-unit))) + (check-equal? + (begin-stlc #t) + (stlc-val-->-stlc-term stlc-true))) + +;; TODO: Abstract this over stlc-type, and provide from in OLL +(data gamma : Type + (emp-gamma : gamma) + (ext-gamma : (->* gamma var stlc-type gamma))) + +(define-rec (lookup-gamma (g : gamma) (x : var) : (maybe type)) + (case* g + [emp-gamma (none type)] + [(ext-gamma (g1 : gamma) (v1 : var) (t1 : type)) + (if (var-equal? v1 x) + (some type t1) + (lookup-gamma g1 x))])) + + +(define-relation (has-type gamma stlc-term stlc-type) + [(g : gamma) + ------------------------ T-Unit + (has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)] + + [(g : gamma) + ------------------------ T-True + (has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)] + + [(g : gamma) + ------------------------ T-False + (has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)] + + [(g : gamma) (x : var) (t : style-type) + (== (maybe stlc-type) (lookup-gamma g x) (some stlc-type t)) + ------------------------ T-Var + (has-type g (var-->-stlc-term x) t)] + + [(g : gamma) (e1 : stlc-term) (e2 : stlc-term) + (t1 : stlc-type) (t2 : stlc-type) + (has-type g e1 t1) + (has-type g e2 t2) + ---------------------- T-Pair + (has-type g (stlc-cons e1 e2) (stlc-* t1 t2))] + + [(g : gamma) (e1 : stlc-term) (e2 : stlc-term) + (t1 : stlc-type) (t2 : stlc-type) + (has-type g e1 (stlc-* t1 t2)) + (has-type (extend-gamma (extend-gamma g x t1) t y2) e2 t) + ---------------------- T-Pair + (has-type g (stlc-let x y e1 e2) t)] + + [(g : gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : var) + (has-type (extend-gamma g x t1) e1 t2) + ---------------------- T-Fun + (has-type g (stlc-lambda x t1 e1) (stlc--> t1 t2))] + + [(g : gamma) (e1 : stlc-term) (e2 : stlc-term) + (t1 : stlc-type) (t2 : stlc-type) + (has-type g e1 (stlc--> t1 t2)) + (has-type g e2 t1) + ---------------------- T-App + (has-type g (stlc-app e1 e2) t2)]) diff --git a/sugar.rkt b/sugar.rkt index 7cc0715..7502e39 100644 --- a/sugar.rkt +++ b/sugar.rkt @@ -6,13 +6,16 @@ #%app define case* + define-type define-theorem qed - real-app) + real-app + define-rec) (require (only-in "redex-curnel.rkt" [#%app real-app] [define real-define])) + (define-syntax (-> syn) (syntax-case syn () [(_ t1 t2) @@ -46,6 +49,9 @@ [(_ e1 e2 e3 ...) #'(#%app (#%app e1 e2) e3 ...)])) +(define-syntax-rule (define-type (name (a : t) ...) body) + (define name (forall* (a : t) ... body))) + (define-syntax (define syn) (syntax-case syn () [(define (name (x : t) ...) body) @@ -53,6 +59,11 @@ [(define id body) #'(real-define id body)])) +(define-syntax (define-rec syn) + (syntax-case syn (:) + [(_ (name (a : t) ... : t_res) body) + #'(define name (fix (name : (forall* (a : t) ... t_res)) + (lambda* (a : t) ... body)))])) (begin-for-syntax (define (rewrite-clause clause) (syntax-case clause (:) @@ -67,5 +78,7 @@ (define-syntax-rule (define-theorem name prop) (define name prop)) +;; TODO: Current implementation doesn't do beta/eta while type-checking +;; because reasons. So manually insert a run in the type annotation (define-syntax-rule (qed thm pf) - ((lambda (x : thm) T) pf)) + ((lambda (x : (run thm)) Type) pf))