From fae24ab4966bee0089c1c3f15a139c3f9dc0d129 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Tue, 22 Sep 2015 23:32:02 -0400 Subject: [PATCH] Styles tweaks * Types now start with a Capital letter, because. * Boolean expression no longer start with the letter b. --- examples/stlc.rkt | 48 ++++++++++++++++----------------- oll.rkt | 20 +++++++------- scribblings/reflection.scrbl | 2 +- stdlib/bool.rkt | 18 +++++++------ stdlib/maybe.rkt | 18 ++++++------- stdlib/nat.rkt | 50 +++++++++++++++++------------------ stdlib/prop.rkt | 46 ++++++++++++++++---------------- stdlib/tactics/sartactics.rkt | 2 +- stdlib/tactics/standard.rkt | 10 +++---- stdlib/typeclass.rkt | 24 ++++++++--------- 10 files changed, 120 insertions(+), 118 deletions(-) diff --git a/examples/stlc.rkt b/examples/stlc.rkt index 69678a1..0a1a570 100644 --- a/examples/stlc.rkt +++ b/examples/stlc.rkt @@ -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 '(() ())) diff --git a/oll.rkt b/oll.rkt index a34ec41..8c5c4d3 100644 --- a/oll.rkt +++ b/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 diff --git a/scribblings/reflection.scrbl b/scribblings/reflection.scrbl index 810020d..332d527 100644 --- a/scribblings/reflection.scrbl +++ b/scribblings/reflection.scrbl @@ -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)] } diff --git a/stdlib/bool.rkt b/stdlib/bool.rkt index 5f57a67..fbb617d 100644 --- a/stdlib/bool.rkt +++ b/stdlib/bool.rkt @@ -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)) diff --git a/stdlib/maybe.rkt b/stdlib/maybe.rkt index 495ac04..55fd9ad 100644 --- a/stdlib/maybe.rkt +++ b/stdlib/maybe.rkt @@ -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)) diff --git a/stdlib/nat.rkt b/stdlib/nat.rkt index 2fde474..d5df010 100644 --- a/stdlib/nat.rkt +++ b/stdlib/nat.rkt @@ -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)) diff --git a/stdlib/prop.rkt b/stdlib/prop.rkt index e9c892b..11b760d 100644 --- a/stdlib/prop.rkt +++ b/stdlib/prop.rkt @@ -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) diff --git a/stdlib/tactics/sartactics.rkt b/stdlib/tactics/sartactics.rkt index 80182c8..c748a2a 100644 --- a/stdlib/tactics/sartactics.rkt +++ b/stdlib/tactics/sartactics.rkt @@ -129,7 +129,7 @@ (require rackunit "../bool.rkt") - (define-theorem meow (forall (x : bool) bool)) + (define-theorem meow (forall (x : Bool) Bool)) #;(proof (interactive)) ) diff --git a/stdlib/tactics/standard.rkt b/stdlib/tactics/standard.rkt index 5e46722..d5af959 100644 --- a/stdlib/tactics/standard.rkt +++ b/stdlib/tactics/standard.rkt @@ -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? diff --git a/stdlib/typeclass.rkt b/stdlib/typeclass.rkt index 82a20a7..c4b95e9 100644 --- a/stdlib/typeclass.rkt +++ b/stdlib/typeclass.rkt @@ -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))