suzanne.soy/cur
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

All tests pass! Sugar simplified

Browse Source
This commit is contained in:
William J. Bowman 2016-01-18 11:48:51 -05:00
parent d48a5a0647
commit 174e4560d1
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
10 changed files with 38 additions and 38 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
cur-lib/cur/olly.rkt
View File

@ -4,7 +4,8 @@
(require
"stdlib/sugar.rkt"
"stdlib/nat.rkt"
(only-in "cur.rkt" [#%app real-app] [elim real-elim]))
;; TODO: "real-"? More like "curnel-"
(only-in "cur.rkt" [#%app real-app] [elim real-elim] [forall real-forall] [lambda real-lambda]))
(provide
define-relation
@ -38,8 +39,7 @@
x*:expr ...
line:dash lab:id
(name:id y* ...))
#:with rule #'(lab : (forall* d ...
(->* x* ... (name y* ...))))
#:with rule #'(lab : (-> d ... x* ... (name y* ...)))
;; TODO: convert meta-vars such as e1 to e_1
#:attr latex (format "\\inferrule~n{~a}~n{~a}"
(string-trim
@ -62,7 +62,7 @@
#:fail-unless (andmap (curry equal? (syntax->datum #'n))
(syntax->datum #'(rules.name ...)))
"Mismatch between relation declared name and result of inference rule"
(let ([output #`(data n : (->* types* ... Type) rules.rule ...)])
(let ([output #`(data n : (-> types* ... Type) rules.rule ...)])
;; TODO: Pull this out into a separate function and test. Except
;; that might make using attritbutes more difficult.
(when (attribute latex-file)
@ -128,7 +128,7 @@
#:attr arg-context #'())
(pattern ((~var e (right-clause type)) (~var e* (right-clause type)) ...)
#:attr name (fresh-name #'e.name)
#:attr clause-context #`(e.name : (->* #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
#:attr clause-context #`(e.name : (-> #,@(flatten-args #'e.arg-context #'(e*.arg-context ...))
#,(hash-ref (nts) type)))
#:attr arg-context #`(#,@(flatten-args #'e.arg-context #'(e*.arg-context ...)))))
@ -243,7 +243,7 @@
(syntax-parse (cur-expand syn #'define #'begin)
;; TODO: Need to add these to a literal set and export it
;; Or, maybe overwrite syntax-parse
#:literals (lambda forall data real-app real-elim define begin Type)
#:literals (real-lambda real-forall data real-app real-elim define begin Type)
[(begin e ...)
(for/fold ([str ""])
([e (syntax->list #'(e ...))])
@ -266,10 +266,10 @@
(format "~a(~a : ~a) " str (output-coq n) (output-coq t)))
(output-coq #'body)))
"")]
[(lambda ~! (x:id (~datum :) t) body:expr)
[(real-lambda ~! (x:id (~datum :) t) body:expr)
(format "(fun ~a : ~a => ~a)" (output-coq #'x) (output-coq #'t)
(output-coq #'body))]
[(forall ~! (x:id (~datum :) t) body:expr)
[(real-forall ~! (x:id (~datum :) t) body:expr)
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (output-coq #'t)
(output-coq #'body))]
[(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)

16
cur-lib/cur/stdlib/prop.rkt
View File

@ -61,20 +61,20 @@
[(conj (A : Type) (B : Type) (a : A) (b : B)) b])))
#| TODO: Disabled until #22 fixed
(data Or : (forall* (A : Type) (B : Type) Type)
(left : (forall* (A : Type) (B : Type) (a : A) (Or A B)))
(right : (forall* (A : Type) (B : Type) (b : B) (Or A B))))
(data Or : (forall (A : Type) (B : Type) Type)
(left : (forall (A : Type) (B : Type) (a : A) (Or A B)))
(right : (forall (A : Type) (B : Type) (b : B) (Or A B))))
(define-theorem thm:A-or-A
(forall* (A : Type) (o : (Or A A)) A))
(forall (A : Type) (o : (Or A A)) A))
(define proof:A-or-A
(lambda* (A : Type) (c : (Or A A))
(lambda (A : Type) (c : (Or A A))
;; TODO: What should the motive be?
(elim Or Type (lambda* (A : Type) (B : Type) (c : (Or A B)) A)
(lambda* (A : Type) (B : Type) (a : A) a)
(elim Or Type (lambda (A : Type) (B : Type) (c : (Or A B)) A)
(lambda (A : Type) (B : Type) (a : A) a)
;; TODO: How do we know B is A?
(lambda* (A : Type) (B : Type) (b : B) b)
(lambda (A : Type) (B : Type) (b : B) b)
A A c)))
(qed thm:A-or-A proof:A-or-A)

4
cur-lib/cur/stdlib/sugar.rkt
View File

@ -31,7 +31,7 @@
[elim real-elim]
[#%app real-app]
;; Somehow, using real-lambda instead of _lambda causes weird import error
[lambda _lambda]
[lambda real-lambda]
#;[forall real-forall]
[define real-define]))
@ -80,7 +80,7 @@
[(_ d:argument-declaration ...+ body:expr)
(foldr (lambda (src name type r)
(quasisyntax/loc src
(_lambda (#,name : #,type) #,r)))
(real-lambda (#,name : #,type) #,r)))
#'body
(attribute d)
(attribute d.name)

4
cur-test/cur/tests/olly.rkt
View File

@ -67,7 +67,7 @@
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\."
(second (string-split t "\n"))))
(let ([t (output-coq #'(elim nat Type (lambda (x : nat) nat) z
(lambda* (x : nat) (ih-x : nat) ih-x)
(lambda (x : nat) (ih-x : nat) ih-x)
e))])
(check-regexp-match
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)"
@ -75,7 +75,7 @@
(check-regexp-match
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
(parameterize ([coq-defns ""])
(output-coq #'(define thm:plus-commutes (forall* (n : nat) (m : nat)
(output-coq #'(define thm:plus-commutes (forall (n : nat) (m : nat)
(== nat (plus n m) (plus m n)))))
(coq-defns)))
(check-regexp-match

12
cur-test/cur/tests/stdlib/list.rkt
View File

@ -17,24 +17,24 @@
(:: (cons Bool true (nil Bool)) (List Bool)))
(check-equal?
(void)
(:: (lambda* (A : Type) (a : A)
(:: (lambda (A : Type) (a : A)
(ih-a : (-> Nat (Maybe A)))
(n : Nat)
(match n
[z (some A a)]
[(s (n-1 : Nat))
(ih-a n-1)]))
(forall* (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
(forall (A : Type) (a : A) (ih-a : (-> Nat (Maybe A)))
(n : Nat)
(Maybe A))))
(check-equal?
(void)
(:: (lambda* (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
(:: (lambda (A : Type) (n : Nat) (none A)) (forall (A : Type) (-> Nat (Maybe A)))))
(check-equal?
(void)
(:: (elim List Type (lambda* (A : Type) (ls : (List A)) Nat)
(:: (elim List Type (lambda (A : Type) (ls : (List A)) Nat)
(lambda (A : Type) z)
(lambda* (A : Type) (a : A) (ls : (List A)) (ih : Nat)
(lambda (A : Type) (a : A) (ls : (List A)) (ih : Nat)
z)
Bool
(nil Bool))
@ -43,7 +43,7 @@
(check-equal?
(void)
(:: list-ref (forall (A : Type) (->* (List A) Nat (Maybe A)))))
(:: list-ref (forall (A : Type) (-> (List A) Nat (Maybe A)))))
(check-equal?
((list-ref Bool (cons Bool true (nil Bool))) z)
(some Bool true))

4
cur-test/cur/tests/stdlib/maybe.rkt
View File

@ -11,8 +11,8 @@
(some Bool true))
;; Disabled until #22 fixed
#;(check-equal?
(case* Maybe Type (some Bool true) (Bool)
(lambda* (A : Type) (x : (Maybe A)) A)
(case Maybe Type (some Bool true) (Bool)
(lambda (A : Type) (x : (Maybe A)) A)
[(none (A : Type)) IH: ()
false]
[(some (A : Type) (x : A)) IH: ()

4
cur-test/cur/tests/stdlib/prop.rkt
View File

@ -11,8 +11,8 @@
(:: pf:proj1 thm:proj1)
(:: pf:proj2 thm:proj2)
(check-equal?
(elim == Type (λ* (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
(λ* (A : Type) (x : A) z)
(elim == Type (λ (A : Type) (x : A) (y : A) (p : (== A x y)) Nat)
(λ (A : Type) (x : A) z)
Bool
true
true

6
cur-test/cur/tests/stdlib/sugar.rkt
View File

@ -5,19 +5,19 @@
;; TODO: Missing tests for match, others
(check-equal?
((λ* (x : (Type 1)) (y : (∀* (x : (Type 1)) (Type 1))) (y x))
((λ (x : (Type 1)) (y : (∀ (x : (Type 1)) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)
(check-equal?
((λ* (x : (Type 1)) (y : (→* (Type 1) (Type 1))) (y x))
((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)
(check-equal?
((λ* (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
((λ (x : (Type 1)) (y : (→ (Type 1) (Type 1))) (y x))
Type
(λ (x : (Type 1)) x))
Type)

2
cur-test/cur/tests/stdlib/typeclass.rkt
View File

@ -8,7 +8,7 @@
cur/stdlib/typeclass)
(typeclass (Eqv (A : Type))
(equal? : (forall* (a : A) (b : A) Bool)))
(equal? : (forall (a : A) (b : A) Bool)))
(impl (Eqv Bool)
(define (equal? (a : Bool) (b : Bool))
(if a

8
cur-test/cur/tests/stlc.rkt
View File

@ -21,10 +21,10 @@
;; TODO: Abstract this over stlc-type, and provide from in OLL
(data Gamma : Type
(emp-gamma : Gamma)
(extend-gamma : (->* Gamma Var stlc-type Gamma)))
(extend-gamma : (-> Gamma Var stlc-type Gamma)))
(define (lookup-gamma (g : Gamma) (x : Var))
(case* Gamma Type g () (lambda* (g : Gamma) (Maybe stlc-type))
(case* Gamma Type 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)))
@ -97,7 +97,7 @@
;; Replace x with a de bruijn index, by running a CIC term at
;; compile time.
(normalize/syn
#`((lambda* (x : stlc-term)
#`((lambda (x : stlc-term)
(stlc-lambda (avar #,oldindex) #,(stlc #'t) #,(stlc #'e)))
(Var-->-stlc-term (avar #,oldindex)))))]
[(quote (e1 e2))
@ -106,7 +106,7 @@
(let* ([y index]
[x #`(s #,y)])
(set! index #`(s (s #,index)))
#`((lambda* (x : stlc-term) (y : stlc-term)
#`((lambda (x : stlc-term) (y : stlc-term)
(stlc-let (avar #,x) (avar #,y) #,(stlc #'t) #,(stlc #'e1)
#,(stlc #'e2)))
(Var-->-stlc-term (avar #,x))