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.
This commit is contained in:
William J. Bowman
parent
116449ad44
commit
26ac41f104
19
bool.rkt
Normal file
19
bool.rkt
Normal file
|
|
@ -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))
|
||||
7
maybe.rkt
Normal file
7
maybe.rkt
Normal file
|
|
@ -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))))
|
||||
18
nat.rkt
18
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))))
|
||||
|
|
|
|||
81
oll.rkt
81
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)
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
100
proofs-for-free.rkt
Normal file
100
proofs-for-free.rkt
Normal file
|
|
@ -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)
|
||||
61
prop.rkt
Normal file
61
prop.rkt
Normal file
|
|
@ -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))))
|
||||
|
|
@ -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)))
|
||||
|
|
|
|||
131
stlc.rkt
Normal file
131
stlc.rkt
Normal file
|
|
@ -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)])
|
||||
17
sugar.rkt
17
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))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user