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

[UNTESTED, DESIGN BUGS] Design for typed macros

Browse Source 
Started working on a promising design for lifting type checking into the
macros for easy syntax extensions over the typed language. Works on some
examples, but running into performance issues and haven't
tested/finished design.
This commit is contained in:
William J. Bowman 2016-01-20 17:52:37 -05:00
parent 76933bd3b1
commit 83fb144c24
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
4 changed files with 156 additions and 70 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
cur-lib/cur/curnel/redex-lang.rkt
View File

@ -58,6 +58,8 @@
(all-from-out syntax/parse) (all-from-out syntax/parse)
(all-from-out racket) (all-from-out racket)
(all-from-out racket/syntax) (all-from-out racket/syntax)
raise-curnel-type-error
raise-curnel-syntax-error
cur->datum cur->datum
cur-expand cur-expand
type-infer/syn type-infer/syn
@ -66,6 +68,32 @@
step/syn step/syn
cur-equal?)) cur-equal?))
;; Exceptions
(begin-for-syntax
(provide
(struct-out exn:cur)
(struct-out exn:cur:curnel)
(struct-out exn:cur:curnel:type)
(struct-out exn:cur:curnel:syntax))
(define-struct (exn:cur exn) () #:transparent)
(define-struct (exn:cur:curnel exn:cur) () #:transparent)
(define-struct (exn:cur:curnel:type exn:cur) () #:transparent)
(define-struct (exn:cur:curnel:syntax exn:cur) () #:transparent)
(define (raise-curnel-type-error name v . other)
(raise
(make-exn:cur:curnel:type
(for/fold ([msg (format "~a: Cur type error;~n Typing judgment did not hold in Curnel~n term: ~a" name v)])
([t other])
(format "~a~n additional context: ~a" msg t))
(current-continuation-marks))))
(define (raise-curnel-syntax-error name v [more ""])
(raise
(make-exn:cur:curnel:syntax
(format "~a: Cur syntax error;~n Term is invalid Curnel syntax;~a~n term: ~a" name more v)
(current-continuation-marks)))))
(begin-for-syntax (begin-for-syntax
;; TODO: Gamma and Delta seem to get reset inside a module+ ;; TODO: Gamma and Delta seem to get reset inside a module+
(define gamma (define gamma
@ -73,7 +101,7 @@
(term ∅) (term ∅)
(lambda (x) (lambda (x)
(unless (Γ? x) (unless (Γ? x)
(error 'core-error "We built a bad term environment ~s" x)) (raise-curnel-syntax-error 'term-environment "term is not a well-formed Γ"))
x))) x)))
(define delta (define delta
@ -81,7 +109,7 @@
(term ∅) (term ∅)
(lambda (x) (lambda (x)
(unless (Δ? x) (unless (Δ? x)
(error 'core-error "We built a bad inductive declaration ~s" x)) (raise-curnel-syntax-error 'inductive-delcaration x "term is not a well-formed Δ"))
x))) x)))
;; These should be provided by core, so details of envs can be hidden. ;; These should be provided by core, so details of envs can be hidden.
@ -118,7 +146,7 @@
(list null null) (list null null)
(lambda (x) (lambda (x)
(unless (subst? x) (unless (subst? x)
(error 'core-error "We build a bad subst ~s" x)) (raise-curnel-syntax-error 'top-level-bindings x))
x))) x)))
(define (add-binding/term! x t) (define (add-binding/term! x t)
@ -156,8 +184,6 @@
(define (cur->datum syn) (define (cur->datum syn)
;; Main loop; avoid type ;; Main loop; avoid type
(define reified-term (define reified-term
;; TODO: This results in less good error messages. Add an
;; algorithm to find the smallest ill-typed term.
(parameterize ([inner-expand? #t]) (parameterize ([inner-expand? #t])
(let cur->datum ([syn syn]) (let cur->datum ([syn syn])
(syntax-parse (core-expand syn) (syntax-parse (core-expand syn)
@ -185,7 +211,7 @@
(term (,(cur->datum #'e1) ,(cur->datum #'e2)))])))) (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
(unless (or (inner-expand?) (type-infer/term reified-term)) (unless (or (inner-expand?) (type-infer/term reified-term))
#;(printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma)) #;(printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma))
(raise-syntax-error 'cur "term is ill-typed:" reified-term syn)) (raise-curnel-type-error 'cur->datum reified-term syn))
reified-term) reified-term)
(define (datum->cur syn t) (define (datum->cur syn t)
@ -223,8 +249,8 @@
(term (reduce #,(delta) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst))))))) (term (reduce #,(delta) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst)))))))
;; Reflection tools ;; Reflection tools
;; TODO: Reflection tools should catch errors from eval-cur et al. to ;; TODO: Reflection tools should catch internal errors, e.g., from eval-cur et al. to
;; ensure users can provide better error messages. ;; ensure users can provide better error messages. But should not catch errors caused by user macros.
(define (local-env->gamma env) (define (local-env->gamma env)
(for/fold ([gamma (gamma)]) (for/fold ([gamma (gamma)])
@ -247,14 +273,14 @@
(and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t)) (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
;; TODO: Document local-env ;; TODO: Document local-env
(define (type-infer/syn syn #:local-env [env '()]) (define (type-infer/syn #:local-env [env '()] syn)
(parameterize ([gamma (local-env->gamma env)]) (parameterize ([gamma (local-env->gamma env)])
(with-handlers ([values (lambda _ #f)]) (with-handlers ([exn:cur:curnel:type? (lambda _ #f)])
(let ([t (type-infer/term (eval-cur syn))]) (let ([t (type-infer/term (eval-cur syn))])
(and t (datum->cur syn t)))))) (and t (datum->cur syn t))))))
(define (type-check/syn? syn type) (define (type-check/syn? syn type)
(with-handlers ([values (lambda _ #f)]) (with-handlers ([exn:cur:curnel:type? (lambda _ #f)])
(type-check/term? (eval-cur syn) (eval-cur type)))) (type-check/term? (eval-cur syn) (eval-cur type))))
;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is

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

@ -96,13 +96,12 @@
(thunk (thunk
(for/fold ([strs ""] (for/fold ([strs ""]
[local-env (dict-set local-env #'n #'t)]) [local-env (dict-set local-env #'n #'t)])
([clause (syntax->list #'((x* : t*) ...))]) ([x (attribute x*)]
(syntax-parse clause [t (attribute t*)])
[(x (~datum :) t)
(values (values
(format "~a~n| ~a : ~a" strs (syntax-e #'x) (format "~a~n| ~a : ~a" strs (syntax-e x)
(cur->coq #'t local-env)) (cur->coq t local-env))
(dict-set local-env #'x #'t))]))) (dict-set local-env x t))))
(lambda (x y) x)))) (lambda (x y) x))))
"")] "")]
[(Type i) "Type"] [(Type i) "Type"]
@ -207,6 +206,7 @@
lab:rule-name lab:rule-name
(~var t (conclusion name indices (attribute lab)))) (~var t (conclusion name indices (attribute lab))))
#:with constr-decl #:with constr-decl
;; TODO: quasisyntax/loc
#'(lab : (-> h ... (t.name t.arg ...))) #'(lab : (-> h ... (t.name t.arg ...)))
;; TODO: convert meta-vars such as e1 to e_1 ;; TODO: convert meta-vars such as e1 to e_1
#:attr latex #:attr latex

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

@ -31,7 +31,39 @@
[lambda real-lambda] [lambda real-lambda]
[define real-define])) [define real-define]))
;; Exceptions and such
(begin-for-syntax (begin-for-syntax
(define-struct (exn:cur:type exn:cur) () #:transparent)
(define (raise-cur-type-infer-error name v . other)
(format
"~aCur type error;~n Could not infer any type~n term: ~a~a"
(if name (format "~a:" name) "")
v
(for/fold ([str ""])
([other other])
(format "~a~n context: ~a" str other)))))
(begin-for-syntax
#| TODO
| Design of "typed" macros for Cur.
|
| We can use syntax classes to emulate typed macros. The syntax
| class calls the type-checker to ensure the term parsed term is
| well-typed. This *must* not expand the the matched type as a side-effect.
| Unfortunately, to handle binding, patterns that have variables
| must thread binding information through while parsing in syntax
| parse. This would be simple if we had implicit monad syntax for
| it, but otherwise we must explicitly thread the environment
| information through the syntax classes. How annoying.
|
| Ideas:
| Could create a "env" compile-time parameter...
| Could expose Gamma, in some way...
| Could use Racket namespaces? Might requrie abandoning Redex
|
|
|#
(define (deduce-type-error term expected) (define (deduce-type-error term expected)
(format (format
"Expected ~a ~a, but ~a." "Expected ~a ~a, but ~a."
@ -42,38 +74,68 @@
"seems to be an unbound variable"] "seems to be an unbound variable"]
[_ "could not infer a type."]))) [_ "could not infer a type."])))
(define-syntax-class cur-term (define-syntax-class cur-syntax
(pattern e:expr))
(define-syntax-class well-typed-cur-term
(pattern (pattern
e:expr e:cur-syntax
#:attr type (type-infer/syn #'e) #:attr type (type-infer/syn #'e)
;; TODO: Reduce to smallest failing example. #:fail-unless (attribute type)
#:fail-unless (raise-cur-type-infer-error #f #'e))))
(attribute type)
(deduce-type-error
#'e
"to be a well-typed Cur term")))
;; For delaying a type-check until the term is under a binder
;; NB: This is an impressively awesome solution..... need to write something about it.
(define-syntax (delayed-check syn)
(syntax-parse syn
[(_ e:well-typed-cur-term) #'e]))
(begin-for-syntax
(define-syntax-class parameter-declaration (define-syntax-class parameter-declaration
(pattern (name:id (~datum :) type:cur-term)) #:commit
(pattern
(name:id (~datum :) ~! type:cur-syntax))
(pattern (pattern
type:cur-term type:cur-syntax
#:attr name (format-id #'type "~a" (gensym 'anon-parameter))))) ;; NB: Anonymous parameters are not bound in the local env
#:attr name (format-id #'type "~a" (gensym 'anon-parameter))))
(define-syntax-class well-typed-parameter-declaration
#:commit
(pattern
(name:id (~datum :) ~! _type:cur-syntax)
#:attr type #'(delayed-check _type))
(pattern
_type:cur-syntax
;; TODO: Duplicate code in parameter-declaration
#:attr type #'(delayed-check _type)
#:attr name (format-id #'type "~a" (gensym 'anon-parameter))))
(define-syntax-class well-typed-parameter-list
(pattern
(d:well-typed-parameter-declaration ...+)
#:attr names (attribute d.name)
#:attr types (attribute d.type))))
;; A multi-arity function type; takes parameter declaration of either ;; A multi-arity function type; takes parameter declaration of either
;; a binding (name : type), or type whose name is generated. ;; a binding (name : type), or type whose name is generated.
;; E.g. ;; E.g.
;; (-> (A : Type) A A) ;; (-> (A : Type) A A)
(define-syntax (-> syn) (define-syntax (-> syn)
(syntax-parse syn (syntax-parse syn
[(_ d:parameter-declaration ...+ result:cur-term) [(_ d:parameter-declaration ...+ e:cur-syntax)
#:with ds #'(d ...)
#:declare ds well-typed-parameter-list
(foldr (lambda (src name type r) (foldr (lambda (src name type r)
(quasisyntax/loc src (quasisyntax/loc src
(forall (#,name : #,type) #,r))) (forall (#,name : #,type) #,r)))
#'result #'(delayed-check e)
(attribute d) (syntax->list (attribute ds))
(attribute d.name) (attribute ds.names)
(attribute d.type))])) (attribute ds.types))]))
;; TODO: Add forall macro that allows specifying *names*, with types ;; TODO: Add forall macro that allows specifying *names*, with types
;; inferred. unlike -> which require types but not names ;; inferred. unlike -> which require types but not names
@ -82,23 +144,18 @@
;; TODO: Allows argument-declarations to have types inferred, similar ;; TODO: Allows argument-declarations to have types inferred, similar
;; to above TODO forall ;; to above TODO forall
(begin-for-syntax
;; eta-expand syntax-class for error messages
(define-syntax-class argument-declaration
(pattern
e:parameter-declaration
#:attr name #'e.name
#:attr type #'e.type)))
(define-syntax (lambda syn) (define-syntax (lambda syn)
(syntax-parse syn (syntax-parse syn
[(_ d:argument-declaration ...+ body:expr) [(_ d:parameter-declaration ... e:cur-syntax)
#:with ds #'(d ...)
#:declare ds well-typed-parameter-list
(foldr (lambda (src name type r) (foldr (lambda (src name type r)
(quasisyntax/loc src (quasisyntax/loc src
(real-lambda (#,name : #,type) #,r))) (real-lambda (#,name : #,type) #,r)))
#'body #'(delayed-check e)
(attribute d) (syntax->list (attribute ds))
(attribute d.name) (attribute ds.names)
(attribute d.type))])) (attribute ds.types))]))
(begin-for-syntax (begin-for-syntax
(define-syntax-class forall-type (define-syntax-class forall-type
@ -123,7 +180,7 @@
(define-syntax (#%app syn) (define-syntax (#%app syn)
(syntax-parse syn (syntax-parse syn
[(_ f:cur-function ~! e:cur-term ...+) [(_ f:well-typed-cur-term ~! e:well-typed-cur-term ...+)
;; Have to thread each argument through, to handle dependency. ;; Have to thread each argument through, to handle dependency.
(for/fold ([type (attribute f.type)]) (for/fold ([type (attribute f.type)])
([arg (attribute e)] ([arg (attribute e)]

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

@ -6,6 +6,9 @@
(require (require
rackunit rackunit
cur/stdlib/sugar cur/stdlib/sugar
cur/stdlib/nat
cur/stdlib/bool
cur/stdlib/prop
cur/olly) cur/olly)
(begin-for-syntax (begin-for-syntax
@ -30,28 +33,28 @@
"(forall .+ : Type, Type)" "(forall .+ : Type, Type)"
(cur->coq #'(-> Type Type))) (cur->coq #'(-> Type Type)))
(let ([t (cur->coq (let ([t (cur->coq
#'(define-relation (meow gamma term type) #'(define-relation (meow Nat Bool Nat)
[(g : gamma) (e : term) (t : type) [(n : Nat) (b : Bool) (m : Nat)
--------------- T-Bla --------------- T-Bla
(meow g e t)]))]) (meow n b m)]))])
(check-regexp-match (check-regexp-match
"Inductive meow : \\(forall .+ : gamma, \\(forall .+ : term, \\(forall .+ : type, Type\\)\\)\\) :=" "Inductive meow : \\(forall .+ : Nat, \\(forall .+ : Bool, \\(forall .+ : Nat, Type\\)\\)\\) :="
(first (string-split t "\n"))) (first (string-split t "\n")))
(check-regexp-match (check-regexp-match
"\\| T-Bla : \\(forall g : gamma, \\(forall e : term, \\(forall t : type, \\(\\(\\(meow g\\) e\\) t\\)\\)\\)\\)\\." "\\| T-Bla : \\(forall n : Nat, \\(forall b : Bool, \\(forall m : Nat, \\(\\(\\(meow n\\) b\\) m\\)\\)\\)\\)\\."
(second (string-split t "\n")))) (second (string-split t "\n"))))
(let ([t (cur->coq (let ([t (cur->coq
#'(elim nat Type (lambda (x : nat) nat) z #'(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))]) z))])
(check-regexp-match (check-regexp-match
"\\(\\(\\(\\(nat_rect \\(fun x : nat => nat\\)\\) z\\) \\(fun x : nat => \\(fun ih_x : nat => ih_x\\)\\)\\) e\\)" "\\(\\(\\(\\(Nat_rect \\(fun x : Nat => Nat\\)\\) z\\) \\(fun x : Nat => \\(fun ih_x : Nat => ih_x\\)\\)\\) z\\)"
t)) t))
(check-regexp-match (check-regexp-match
"Definition thm_plus_commutes := \\(forall n : nat, \\(forall m : nat, \\(\\(\\(== nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n" "Definition thm_plus_commutes := \\(forall n : Nat, \\(forall m : Nat, \\(\\(\\(== Nat\\) \\(\\(plus n\\) m\\)\\) \\(\\(plus m\\) n\\)\\)\\)\\).\n"
(cur->coq (cur->coq
#'(define thm:plus-commutes (forall (n : nat) (m : nat) #'(define thm:plus-commutes (forall (n : Nat) (m : Nat)
(== nat (plus n m) (plus m n)))))) (== Nat (plus n m) (plus m n))))))
(check-regexp-match (check-regexp-match
"Function add1 \\(n : nat\\) := \\(s n\\).\n" "Function add1 \\(n : Nat\\) := \\(s n\\).\n"
(cur->coq #'(define (add1 (n : nat)) (s n))))) (cur->coq #'(define (add1 (n : Nat)) (s n)))))