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

Fixed coq->cur to setup local-env, tweaked ->

Browse Source 
* Fixed up coq->cur to track local-env while expanding.
* Tweaked -> to give better error messages
This commit is contained in:
William J. Bowman 2016-01-19 16:57:17 -05:00
parent 87bc0e44bc
commit 76933bd3b1
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
3 changed files with 70 additions and 55 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -260,13 +260,15 @@
;; 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
;; expanded until expansion reaches a Curnel form, or one of the ;; expanded until expansion reaches a Curnel form, or one of the
;; identifiers in ls. ;; identifiers in ls.
(define (cur-expand syn . ls) ;; TODO: Holy crap boilerplate
(define (cur-expand syn #:local-env [env '()] . ls)
(parameterize ([gamma (local-env->gamma env)])
(disarm (disarm
(local-expand (local-expand
syn syn
'expression 'expression
(append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-top)) (append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-top))
ls))))) ls))))))
;; ----------------------------------------------------------------- ;; -----------------------------------------------------------------
;; Require/provide macros ;; Require/provide macros

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

@ -43,57 +43,73 @@
(define (cur->coq syn) (define (cur->coq syn)
(parameterize ([coq-defns ""]) (parameterize ([coq-defns ""])
(define output (define output
(let cur->coq ([syn syn]) (let cur->coq ([syn syn]
(syntax-parse (cur-expand syn #'define #'begin) [local-env (make-immutable-hash)])
(syntax-parse (cur-expand #:local-env local-env syn #'define #'begin)
;; TODO: Need to add these to a literal set and export it ;; TODO: Need to add these to a literal set and export it
;; Or, maybe overwrite syntax-parse ;; Or, maybe overwrite syntax-parse
#:literals (real-lambda real-forall data real-app real-elim define begin Type) #:literals (real-lambda real-forall data real-app real-elim define begin Type)
[(begin e ...) [(begin e ...)
(for/fold ([str ""]) (for/fold ([str ""])
([e (syntax->list #'(e ...))]) ([e (syntax->list #'(e ...))])
(format "~a~n" (cur->coq e)))] (format "~a~n" (cur->coq e local-env)))]
[(define name:id body) [(define name:id body)
(begin (begin
(coq-lift-top-level (coq-lift-top-level
(format "Definition ~a := ~a.~n" (format "Definition ~a := ~a.~n"
(cur->coq #'name) (cur->coq #'name local-env)
(cur->coq #'body))) (cur->coq #'body local-env)))
"")] "")]
[(define (name:id (x:id : t) ...) body) [(define (name:id (x:id : t) ...) body)
(begin (begin
(coq-lift-top-level (define-values (args body-local-env)
(format "Function ~a ~a := ~a.~n" (for/fold ([str ""]
(cur->coq #'name) [local-env local-env])
(for/fold ([str ""])
([n (syntax->list #'(x ...))] ([n (syntax->list #'(x ...))]
[t (syntax->list #'(t ...))]) [t (syntax->list #'(t ...))])
(format "~a(~a : ~a) " str (cur->coq n) (cur->coq t))) (values
(cur->coq #'body))) (format
"~a(~a : ~a) "
str
(cur->coq n local-env)
(cur->coq t local-env))
(dict-set local-env n t))))
(coq-lift-top-level
(format "Function ~a ~a := ~a.~n"
(cur->coq #'name local-env)
args
(cur->coq #'body body-local-env)))
"")] "")]
[(real-lambda ~! (x:id (~datum :) t) body:expr) [(real-lambda ~! (x:id (~datum :) t) body:expr)
(format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t) (format "(fun ~a : ~a => ~a)" (syntax-e #'x) (cur->coq #'t local-env)
(cur->coq #'body))] (cur->coq #'body (dict-set local-env #'x #'t)))]
[(real-forall ~! (x:id (~datum :) t) body:expr) [(real-forall ~! (x:id (~datum :) t) body:expr)
(format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t) (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t local-env)
(cur->coq #'body))] (cur->coq #'body (dict-set local-env #'x #'t)))]
[(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...) [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...)
(begin (begin
(coq-lift-top-level (coq-lift-top-level
(format "Inductive ~a : ~a :=~a." (format "Inductive ~a : ~a :=~a."
(sanitize-id (format "~a" (syntax-e #'n))) (sanitize-id (format "~a" (syntax-e #'n)))
(cur->coq #'t) (cur->coq #'t local-env)
(for/fold ([strs ""]) (call-with-values
(thunk
(for/fold ([strs ""]
[local-env (dict-set local-env #'n #'t)])
([clause (syntax->list #'((x* : t*) ...))]) ([clause (syntax->list #'((x* : t*) ...))])
(syntax-parse clause (syntax-parse clause
[(x (~datum :) t) [(x (~datum :) t)
(values
(format "~a~n| ~a : ~a" strs (syntax-e #'x) (format "~a~n| ~a : ~a" strs (syntax-e #'x)
(cur->coq #'t))])))) (cur->coq #'t local-env))
(dict-set local-env #'x #'t))])))
(lambda (x y) x))))
"")] "")]
[(Type i) "Type"] [(Type i) "Type"]
[(real-elim var t) [(real-elim var t)
(format "~a_rect" (cur->coq #'var))] (format "~a_rect" (cur->coq #'var local-env))]
[(real-app e1 e2) [(real-app e1 e2)
(format "(~a ~a)" (cur->coq #'e1) (cur->coq #'e2))] (format "(~a ~a)" (cur->coq #'e1 local-env) (cur->coq #'e2 local-env))]
[e:id (sanitize-id (format "~a" (syntax->datum #'e)))]))) [e:id (sanitize-id (format "~a" (syntax->datum #'e)))])))
(format (format
"~a~a" "~a~a"

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

@ -32,14 +32,32 @@
[define real-define])) [define real-define]))
(begin-for-syntax (begin-for-syntax
(define-syntax-class result-type (define (deduce-type-error term expected)
(pattern type:expr)) (format
"Expected ~a ~a, but ~a."
(syntax->datum term)
expected
(syntax-parse term
[x:id
"seems to be an unbound variable"]
[_ "could not infer a type."])))
(define-syntax-class cur-term
(pattern
e:expr
#:attr type (type-infer/syn #'e)
;; TODO: Reduce to smallest failing example.
#:fail-unless
(attribute type)
(deduce-type-error
#'e
"to be a well-typed Cur term")))
(define-syntax-class parameter-declaration (define-syntax-class parameter-declaration
(pattern (name:id (~datum :) type:expr)) (pattern (name:id (~datum :) type:cur-term))
(pattern (pattern
type:expr type:cur-term
#:attr name (format-id #'type "~a" (gensym 'anon-parameter))))) #:attr name (format-id #'type "~a" (gensym 'anon-parameter)))))
;; A multi-arity function type; takes parameter declaration of either ;; A multi-arity function type; takes parameter declaration of either
@ -48,7 +66,7 @@
;; (-> (A : Type) A A) ;; (-> (A : Type) A A)
(define-syntax (-> syn) (define-syntax (-> syn)
(syntax-parse syn (syntax-parse syn
[(_ d:parameter-declaration ...+ result:result-type) [(_ d:parameter-declaration ...+ result:cur-term)
(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)))
@ -83,16 +101,6 @@
(attribute d.type))])) (attribute d.type))]))
(begin-for-syntax (begin-for-syntax
(define (deduce-type-error term expected)
(format
"Expected ~a ~a, but ~a."
(syntax->datum term)
expected
(syntax-parse term
[x:id
"seems to be an unbound variable"]
[_ "could not infer a type."])))
(define-syntax-class forall-type (define-syntax-class forall-type
(pattern (pattern
((~literal forall) ~! (parameter-name:id (~datum :) parameter-type) body))) ((~literal forall) ~! (parameter-name:id (~datum :) parameter-type) body)))
@ -111,18 +119,7 @@
(format (format
"Expected ~a to be a function, but inferred type ~a" "Expected ~a to be a function, but inferred type ~a"
(syntax->datum #'e) (syntax->datum #'e)
(syntax->datum (attribute type))))) (syntax->datum (attribute type))))))
(define-syntax-class cur-term
(pattern
e:expr
#:attr type (type-infer/syn #'e)
;; TODO: Reduce to smallest failing example.
#:fail-unless
(attribute type)
(deduce-type-error
#'e
"to be a well-typed Cur term"))))
(define-syntax (#%app syn) (define-syntax (#%app syn)
(syntax-parse syn (syntax-parse syn