Styles tweaks
* Types now start with a Capital letter, because. * Boolean expression no longer start with the letter b.
This commit is contained in:
William J. Bowman
parent
d177577ac9
commit
fae24ab496
|
|
@ -18,61 +18,61 @@
|
|||
(let (x x) = e in e)))
|
||||
|
||||
;; TODO: Abstract this over stlc-type, and provide from in OLL
|
||||
(data gamma : Type
|
||||
(emp-gamma : gamma)
|
||||
(extend-gamma : (->* gamma var stlc-type gamma)))
|
||||
(data Gamma : Type
|
||||
(emp-gamma : Gamma)
|
||||
(extend-gamma : (->* Gamma Var stlc-type Gamma)))
|
||||
|
||||
(define (lookup-gamma (g : gamma) (x : var))
|
||||
(case* gamma g (lambda* (g : gamma) (maybe stlc-type))
|
||||
(define (lookup-gamma (g : Gamma) (x : Var))
|
||||
(case* Gamma g (lambda* (g : Gamma) (Maybe stlc-type))
|
||||
[emp-gamma (none stlc-type)]
|
||||
[(extend-gamma (g1 : gamma) (v1 : var) (t1 : stlc-type))
|
||||
IH: ((ih-g1 : (maybe stlc-type)))
|
||||
[(extend-gamma (g1 : Gamma) (v1 : Var) (t1 : stlc-type))
|
||||
IH: ((ih-g1 : (Maybe stlc-type)))
|
||||
(if (var-equal? v1 x)
|
||||
(some stlc-type t1)
|
||||
ih-g1)]))
|
||||
|
||||
(define-relation (has-type gamma stlc-term stlc-type)
|
||||
(define-relation (has-type Gamma stlc-term stlc-type)
|
||||
#:output-coq "stlc.v"
|
||||
#:output-latex "stlc.tex"
|
||||
[(g : gamma)
|
||||
[(g : Gamma)
|
||||
------------------------ T-Unit
|
||||
(has-type g (stlc-val-->-stlc-term stlc-unit) stlc-unitty)]
|
||||
|
||||
[(g : gamma)
|
||||
[(g : Gamma)
|
||||
------------------------ T-True
|
||||
(has-type g (stlc-val-->-stlc-term stlc-true) stlc-boolty)]
|
||||
|
||||
[(g : gamma)
|
||||
[(g : Gamma)
|
||||
------------------------ T-False
|
||||
(has-type g (stlc-val-->-stlc-term stlc-false) stlc-boolty)]
|
||||
|
||||
[(g : gamma) (x : var) (t : stlc-type)
|
||||
(== (maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
|
||||
[(g : Gamma) (x : Var) (t : stlc-type)
|
||||
(== (Maybe stlc-type) (lookup-gamma g x) (some stlc-type t))
|
||||
------------------------ T-Var
|
||||
(has-type g (var-->-stlc-term x) t)]
|
||||
(has-type g (Var-->-stlc-term x) t)]
|
||||
|
||||
[(g : gamma) (e1 : stlc-term) (e2 : stlc-term)
|
||||
[(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)
|
||||
[(g : Gamma) (e1 : stlc-term) (e2 : stlc-term)
|
||||
(t1 : stlc-type) (t2 : stlc-type)
|
||||
(t : stlc-type)
|
||||
(x : var) (y : var)
|
||||
(x : Var) (y : Var)
|
||||
(has-type g e1 (stlc-* t1 t2))
|
||||
(has-type (extend-gamma (extend-gamma g x t1) y t2) e2 t)
|
||||
---------------------- T-Let
|
||||
(has-type g (stlc-let x y e1 e2) t)]
|
||||
|
||||
[(g : gamma) (e1 : stlc-term) (t1 : stlc-type) (t2 : stlc-type) (x : var)
|
||||
[(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)
|
||||
[(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)
|
||||
|
|
@ -98,7 +98,7 @@
|
|||
(normalize/syn
|
||||
#`((lambda* (x : stlc-term)
|
||||
(stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
|
||||
(var-->-stlc-term (avar #,oldindex)))))]
|
||||
(Var-->-stlc-term (avar #,oldindex)))))]
|
||||
[(quote (e1 e2))
|
||||
#`(stlc-cons #,(stlc #'e1) #,(stlc #'e2))]
|
||||
[(let (x y) = e1 in e2)
|
||||
|
|
@ -108,8 +108,8 @@
|
|||
#`((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))))
|
||||
(Var-->-stlc-term (avar #,x))
|
||||
(Var-->-stlc-term (avar #,y))))
|
||||
#`(let x i #,(stlc #'e1))]
|
||||
[(e1 e2)
|
||||
#`(stlc-app #,(stlc #'e1) #,(stlc #'e2))]
|
||||
|
|
@ -130,10 +130,10 @@
|
|||
(require rackunit)
|
||||
(check-equal?
|
||||
(begin-stlc (lambda (x : 1) x))
|
||||
(stlc-lambda (avar z) stlc-unitty (var-->-stlc-term (avar z))))
|
||||
(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-app (stlc-lambda (avar z) stlc-unitty (Var-->-stlc-term (avar z)))
|
||||
(stlc-val-->-stlc-term stlc-unit)))
|
||||
(check-equal?
|
||||
(begin-stlc '(() ()))
|
||||
|
|
|
|||
20
oll.rkt
20
oll.rkt
|
|
@ -6,7 +6,7 @@
|
|||
(provide
|
||||
define-relation
|
||||
define-language
|
||||
var
|
||||
Var
|
||||
avar
|
||||
var-equal?
|
||||
generate-coq
|
||||
|
|
@ -216,7 +216,7 @@
|
|||
(define-syntax (define-language syn)
|
||||
(syntax-parse syn
|
||||
[(_ name:id (~do (lang-name #'name))
|
||||
(~do (nts (hash-set (make-immutable-hash) 'var #'var)))
|
||||
(~do (nts (hash-set (make-immutable-hash) 'var #'Var)))
|
||||
(~optional (~seq #:vars (x*:id ...)
|
||||
(~do (nts (for/fold ([ht (nts)])
|
||||
([v (syntax->datum #'(x* ...))])
|
||||
|
|
@ -233,22 +233,22 @@
|
|||
#'())
|
||||
#,output))]))
|
||||
|
||||
(data var : Type (avar : (-> nat var)))
|
||||
(data Var : Type (avar : (-> Nat Var)))
|
||||
|
||||
(define (var-equal? (v1 : var) (v2 : var))
|
||||
(case* var v1 (lambda* (v : var) bool)
|
||||
[(avar (n1 : nat)) IH: ()
|
||||
(case* var v2 (lambda* (v : var) bool)
|
||||
[(avar (n2 : nat)) IH: ()
|
||||
(define (var-equal? (v1 : Var) (v2 : Var))
|
||||
(case* Var v1 (lambda* (v : Var) Bool)
|
||||
[(avar (n1 : Nat)) IH: ()
|
||||
(case* Var v2 (lambda* (v : Var) Bool)
|
||||
[(avar (n2 : Nat)) IH: ()
|
||||
(nat-equal? n1 n2)])]))
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
(check-equal?
|
||||
(var-equal? (avar z) (avar z))
|
||||
btrue)
|
||||
true)
|
||||
(check-equal?
|
||||
(var-equal? (avar z) (avar (s z)))
|
||||
bfalse))
|
||||
false))
|
||||
|
||||
;; See stlc.rkt for examples
|
||||
|
||||
|
|
|
|||
|
|
@ -80,7 +80,7 @@ computing part of the term from another Cur term.
|
|||
@racketmodname[cur/stdlib/nat] are loaded. Also, could be moved outside the privileged code.}
|
||||
|
||||
@examples[#:eval curnel-eval
|
||||
(lambda (x : (run (if btrue bool nat))) x)]
|
||||
(lambda (x : (run (if true Bool Nat))) x)]
|
||||
|
||||
}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,9 +1,10 @@
|
|||
#lang s-exp "../cur.rkt"
|
||||
(provide bool btrue bfalse if bnot)
|
||||
(require "sugar.rkt")
|
||||
(provide Bool true false if not and or)
|
||||
|
||||
(data bool : Type
|
||||
(btrue : bool)
|
||||
(bfalse : bool))
|
||||
(data Bool : Type
|
||||
(true : Bool)
|
||||
(false : Bool))
|
||||
|
||||
(define-syntax (if syn)
|
||||
(syntax-case syn ()
|
||||
|
|
@ -11,10 +12,11 @@
|
|||
;; Compute the motive
|
||||
(let ([M #`(lambda (x : #,(type-infer/syn #'t))
|
||||
#,(type-infer/syn #'s))])
|
||||
(quasisyntax/loc syn (elim bool t #,M s f)))]))
|
||||
(quasisyntax/loc syn (elim Bool t #,M s f)))]))
|
||||
|
||||
(define (not (x : Bool)) (if x false true))
|
||||
|
||||
(define (bnot (x : bool)) (if x bfalse btrue))
|
||||
(module+ test
|
||||
(require rackunit)
|
||||
(check-equal? (bnot btrue) bfalse)
|
||||
(check-equal? (bnot bfalse) btrue))
|
||||
(check-equal? (not true) false)
|
||||
(check-equal? (not false) true))
|
||||
|
|
|
|||
|
|
@ -1,19 +1,19 @@
|
|||
#lang s-exp "../cur.rkt"
|
||||
(require "sugar.rkt")
|
||||
(provide maybe none some)
|
||||
(provide Maybe none some)
|
||||
|
||||
(data maybe : (forall (A : Type) Type)
|
||||
(none : (forall (A : Type) (maybe A)))
|
||||
(some : (forall* (A : Type) (a : A) (maybe A))))
|
||||
(data Maybe : (forall (A : Type) Type)
|
||||
(none : (forall (A : Type) (Maybe A)))
|
||||
(some : (forall* (A : Type) (a : A) (Maybe A))))
|
||||
|
||||
(module+ test
|
||||
(require rackunit "bool.rkt")
|
||||
#;(check-equal?
|
||||
(case* maybe (some bool btrue)
|
||||
(lambda (x : (maybe bool)) bool)
|
||||
(case* Maybe (some Bool true)
|
||||
(lambda (x : (Maybe Bool)) Bool)
|
||||
[(none (A : Type)) IH: ()
|
||||
bfalse]
|
||||
false]
|
||||
[(some (A : Type) (x : A)) IH: ()
|
||||
;; TODO: Don't know how to use dependency yet
|
||||
(if x btrue bfalse)])
|
||||
btrue))
|
||||
(if x true false)])
|
||||
true))
|
||||
|
|
|
|||
|
|
@ -2,50 +2,50 @@
|
|||
(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 )
|
||||
(module+ test
|
||||
(require rackunit))
|
||||
|
||||
(data nat : Type
|
||||
(z : nat)
|
||||
(s : (-> nat nat)))
|
||||
(data Nat : Type
|
||||
(z : Nat)
|
||||
(s : (-> Nat Nat)))
|
||||
|
||||
(define (add1 (n : nat)) (s n))
|
||||
(define (add1 (n : Nat)) (s n))
|
||||
(module+ test
|
||||
(check-equal? (add1 (s z)) (s (s z))))
|
||||
|
||||
(define (sub1 (n : nat))
|
||||
(case* nat n (lambda (x : nat) nat)
|
||||
(define (sub1 (n : Nat))
|
||||
(case* Nat n (lambda (x : Nat) Nat)
|
||||
[z z]
|
||||
[(s (x : nat)) IH: ((ih-n : nat)) x]))
|
||||
[(s (x : Nat)) IH: ((ih-n : Nat)) x]))
|
||||
(module+ test
|
||||
(check-equal? (sub1 (s z)) z))
|
||||
|
||||
(define (plus (n1 : nat) (n2 : nat))
|
||||
(case* nat n1 (lambda (x : nat) nat)
|
||||
(define (plus (n1 : Nat) (n2 : Nat))
|
||||
(case* Nat n1 (lambda (x : Nat) Nat)
|
||||
[z n2]
|
||||
[(s (x : nat)) IH: ((ih-n1 : nat))
|
||||
[(s (x : Nat)) IH: ((ih-n1 : Nat))
|
||||
(s ih-n1)]))
|
||||
(module+ test
|
||||
(check-equal? (plus z z) z)
|
||||
(check-equal? (plus (s (s z)) (s (s z))) (s (s (s (s z))))))
|
||||
|
||||
;; Credit to this function goes to Max
|
||||
(define (nat-equal? (n1 : nat))
|
||||
(elim nat n1 (lambda (x : nat) (-> nat bool))
|
||||
(lambda (n2 : nat)
|
||||
(elim nat n2 (lambda (x : nat) bool)
|
||||
btrue
|
||||
(lambda* (x : nat) (ih-n2 : bool) bfalse)))
|
||||
(lambda* (x : nat) (ih : (-> nat bool))
|
||||
(lambda (n2 : nat)
|
||||
(elim nat n2 (lambda (x : nat) bool)
|
||||
bfalse
|
||||
(lambda* (x : nat) (ih-bla : bool)
|
||||
(define (nat-equal? (n1 : Nat))
|
||||
(elim Nat n1 (lambda (x : Nat) (-> Nat Bool))
|
||||
(lambda (n2 : Nat)
|
||||
(elim Nat n2 (lambda (x : Nat) Bool)
|
||||
true
|
||||
(lambda* (x : Nat) (ih-n2 : Bool) false)))
|
||||
(lambda* (x : Nat) (ih : (-> Nat Bool))
|
||||
(lambda (n2 : Nat)
|
||||
(elim Nat n2 (lambda (x : Nat) Bool)
|
||||
false
|
||||
(lambda* (x : Nat) (ih-bla : Bool)
|
||||
(ih x)))))))
|
||||
(module+ test
|
||||
(check-equal? (nat-equal? z z) btrue)
|
||||
(check-equal? (nat-equal? z (s z)) bfalse)
|
||||
(check-equal? (nat-equal? (s z) (s z)) btrue))
|
||||
(check-equal? (nat-equal? z z) true)
|
||||
(check-equal? (nat-equal? z (s z)) false)
|
||||
(check-equal? (nat-equal? (s z) (s z)) true))
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -3,61 +3,61 @@
|
|||
;; TODO: Handle multiple provide forms properly
|
||||
;; TODO: Handle (all-defined-out) properly
|
||||
(provide
|
||||
true T
|
||||
True T
|
||||
thm:anything-implies-true
|
||||
false
|
||||
not
|
||||
and
|
||||
False
|
||||
Not
|
||||
And
|
||||
conj
|
||||
thm:and-is-symmetric proof:and-is-symmetric
|
||||
thm:proj1 proof:proj1
|
||||
thm:proj2 proof:proj2
|
||||
== refl)
|
||||
|
||||
(data true : Type (T : true))
|
||||
(data True : Type (T : True))
|
||||
|
||||
(define-theorem thm:anything-implies-true (forall (P : Type) true))
|
||||
(define-theorem thm:anything-implies-true (forall (P : Type) True))
|
||||
|
||||
(qed thm:anything-implies-true (lambda (P : Type) T))
|
||||
|
||||
(data false : Type)
|
||||
(data False : Type)
|
||||
|
||||
(define-type (not (A : Type)) (-> A false))
|
||||
(define-type (Not (A : Type)) (-> A False))
|
||||
|
||||
(data and : (forall* (A : Type) (B : Type) Type)
|
||||
(data And : (forall* (A : Type) (B : Type) Type)
|
||||
(conj : (forall* (A : Type) (B : Type)
|
||||
(x : A) (y : B) (and A B))))
|
||||
(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)))
|
||||
(forall* (P : Type) (Q : Type) (ab : (And P Q)) (And Q P)))
|
||||
|
||||
(define proof:and-is-symmetric
|
||||
(lambda* (P : Type) (Q : Type) (ab : (and P Q))
|
||||
(case* and ab
|
||||
(lambda* (P : Type) (Q : Type) (ab : (and P Q))
|
||||
(and Q P))
|
||||
(lambda* (P : Type) (Q : Type) (ab : (And P Q))
|
||||
(case* And ab
|
||||
(lambda* (P : Type) (Q : Type) (ab : (And P Q))
|
||||
(And Q P))
|
||||
((conj (P : Type) (Q : Type) (x : P) (y : Q)) IH: () (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))
|
||||
(forall* (A : Type) (B : Type) (c : (And A B)) A))
|
||||
|
||||
(define proof:proj1
|
||||
(lambda* (A : Type) (B : Type) (c : (and A B))
|
||||
(case* and c
|
||||
(lambda* (A : Type) (B : Type) (c : (and A B)) A)
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B))
|
||||
(case* And c
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B)) A)
|
||||
((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () a))))
|
||||
|
||||
(qed thm:proj1 proof:proj1)
|
||||
|
||||
(define-theorem thm:proj2
|
||||
(forall* (A : Type) (B : Type) (c : (and A B)) B))
|
||||
(forall* (A : Type) (B : Type) (c : (And A B)) B))
|
||||
|
||||
(define proof:proj2
|
||||
(lambda* (A : Type) (B : Type) (c : (and A B))
|
||||
(case* and c
|
||||
(lambda* (A : Type) (B : Type) (c : (and A B)) B)
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B))
|
||||
(case* And c
|
||||
(lambda* (A : Type) (B : Type) (c : (And A B)) B)
|
||||
((conj (A : Type) (B : Type) (a : A) (b : B)) IH: () b))))
|
||||
|
||||
(qed thm:proj2 proof:proj2)
|
||||
|
|
|
|||
|
|
@ -129,7 +129,7 @@
|
|||
(require
|
||||
rackunit
|
||||
"../bool.rkt")
|
||||
(define-theorem meow (forall (x : bool) bool))
|
||||
(define-theorem meow (forall (x : Bool) Bool))
|
||||
#;(proof
|
||||
(interactive))
|
||||
)
|
||||
|
|
|
|||
|
|
@ -103,24 +103,24 @@
|
|||
(require
|
||||
rackunit
|
||||
"../bool.rkt")
|
||||
(define-theorem meow (forall (x : bool) bool))
|
||||
(define-theorem meow (forall (x : Bool) Bool))
|
||||
(proof
|
||||
(intro x)
|
||||
(by-assumption))
|
||||
(define-theorem meow1 (forall (x : bool) bool))
|
||||
(define-theorem meow1 (forall (x : Bool) Bool))
|
||||
(proof
|
||||
(obvious)
|
||||
(print))
|
||||
(define-theorem meow2 (forall (x : bool) bool))
|
||||
(define-theorem meow2 (forall (x : Bool) Bool))
|
||||
(proof
|
||||
(intro x)
|
||||
(restart)
|
||||
(intro x)
|
||||
(by-assumption))
|
||||
(define-theorem meow3 (forall (x : bool) bool))
|
||||
(define-theorem meow3 (forall (x : Bool) Bool))
|
||||
(proof (obvious))
|
||||
;; TODO: Fix this unit test so it doesn't require interaction
|
||||
(define-theorem meow4 (forall (x : bool) bool))
|
||||
(define-theorem meow4 (forall (x : Bool) Bool))
|
||||
#;(proof
|
||||
(interactive))
|
||||
;; TODO: Add check-cur-equal? for unit testing?
|
||||
|
|
|
|||
|
|
@ -74,23 +74,23 @@
|
|||
(module+ test
|
||||
(require rackunit)
|
||||
(typeclass (Eqv (A : Type))
|
||||
(equal? : (forall* (a : A) (b : A) bool)))
|
||||
(impl (Eqv bool)
|
||||
(define (equal? (a : bool) (b : bool))
|
||||
(equal? : (forall* (a : A) (b : A) Bool)))
|
||||
(impl (Eqv Bool)
|
||||
(define (equal? (a : Bool) (b : Bool))
|
||||
(if a
|
||||
(if b btrue bfalse)
|
||||
(if b bfalse btrue))))
|
||||
(impl (Eqv nat)
|
||||
(if b true false)
|
||||
(if b false true))))
|
||||
(impl (Eqv Nat)
|
||||
(define equal? nat-equal?))
|
||||
(check-equal?
|
||||
(equal? z z)
|
||||
btrue)
|
||||
true)
|
||||
(check-equal?
|
||||
(equal? z (s z))
|
||||
bfalse)
|
||||
false)
|
||||
(check-equal?
|
||||
(equal? btrue bfalse)
|
||||
bfalse)
|
||||
(equal? true false)
|
||||
false)
|
||||
(check-equal?
|
||||
(equal? btrue btrue)
|
||||
btrue))
|
||||
(equal? true true)
|
||||
true))
|
||||
|
|
|
|||
Loading…
Reference in New Issue
Block a user