diff --git a/cur-lib/cur/curnel/redex-lang.rkt b/cur-lib/cur/curnel/redex-lang.rkt index 06977cc..12825ab 100644 --- a/cur-lib/cur/curnel/redex-lang.rkt +++ b/cur-lib/cur/curnel/redex-lang.rkt @@ -260,13 +260,15 @@ ;; 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 ;; identifiers in ls. - (define (cur-expand syn . ls) - (disarm - (local-expand + ;; TODO: Holy crap boilerplate + (define (cur-expand syn #:local-env [env '()] . ls) + (parameterize ([gamma (local-env->gamma env)]) + (disarm + (local-expand syn 'expression (append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-top)) - ls))))) + ls)))))) ;; ----------------------------------------------------------------- ;; Require/provide macros diff --git a/cur-lib/cur/olly.rkt b/cur-lib/cur/olly.rkt index 9b80ced..8582306 100644 --- a/cur-lib/cur/olly.rkt +++ b/cur-lib/cur/olly.rkt @@ -43,57 +43,73 @@ (define (cur->coq syn) (parameterize ([coq-defns ""]) (define output - (let cur->coq ([syn syn]) - (syntax-parse (cur-expand syn #'define #'begin) + (let cur->coq ([syn syn] + [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 ;; Or, maybe overwrite syntax-parse #:literals (real-lambda real-forall data real-app real-elim define begin Type) [(begin e ...) (for/fold ([str ""]) ([e (syntax->list #'(e ...))]) - (format "~a~n" (cur->coq e)))] + (format "~a~n" (cur->coq e local-env)))] [(define name:id body) (begin (coq-lift-top-level (format "Definition ~a := ~a.~n" - (cur->coq #'name) - (cur->coq #'body))) + (cur->coq #'name local-env) + (cur->coq #'body local-env))) "")] [(define (name:id (x:id : t) ...) body) (begin + (define-values (args body-local-env) + (for/fold ([str ""] + [local-env local-env]) + ([n (syntax->list #'(x ...))] + [t (syntax->list #'(t ...))]) + (values + (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) - (for/fold ([str ""]) - ([n (syntax->list #'(x ...))] - [t (syntax->list #'(t ...))]) - (format "~a(~a : ~a) " str (cur->coq n) (cur->coq t))) - (cur->coq #'body))) + (cur->coq #'name local-env) + args + (cur->coq #'body body-local-env))) "")] [(real-lambda ~! (x:id (~datum :) t) body:expr) - (format "(fun ~a : ~a => ~a)" (cur->coq #'x) (cur->coq #'t) - (cur->coq #'body))] + (format "(fun ~a : ~a => ~a)" (syntax-e #'x) (cur->coq #'t local-env) + (cur->coq #'body (dict-set local-env #'x #'t)))] [(real-forall ~! (x:id (~datum :) t) body:expr) - (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t) - (cur->coq #'body))] + (format "(forall ~a : ~a, ~a)" (syntax-e #'x) (cur->coq #'t local-env) + (cur->coq #'body (dict-set local-env #'x #'t)))] [(data ~! n:id (~datum :) t (x*:id (~datum :) t*) ...) (begin (coq-lift-top-level (format "Inductive ~a : ~a :=~a." (sanitize-id (format "~a" (syntax-e #'n))) - (cur->coq #'t) - (for/fold ([strs ""]) - ([clause (syntax->list #'((x* : t*) ...))]) - (syntax-parse clause - [(x (~datum :) t) - (format "~a~n| ~a : ~a" strs (syntax-e #'x) - (cur->coq #'t))])))) + (cur->coq #'t local-env) + (call-with-values + (thunk + (for/fold ([strs ""] + [local-env (dict-set local-env #'n #'t)]) + ([clause (syntax->list #'((x* : t*) ...))]) + (syntax-parse clause + [(x (~datum :) t) + (values + (format "~a~n| ~a : ~a" strs (syntax-e #'x) + (cur->coq #'t local-env)) + (dict-set local-env #'x #'t))]))) + (lambda (x y) x)))) "")] [(Type i) "Type"] [(real-elim var t) - (format "~a_rect" (cur->coq #'var))] + (format "~a_rect" (cur->coq #'var local-env))] [(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)))]))) (format "~a~a" diff --git a/cur-lib/cur/stdlib/sugar.rkt b/cur-lib/cur/stdlib/sugar.rkt index c0c8002..337e8d1 100644 --- a/cur-lib/cur/stdlib/sugar.rkt +++ b/cur-lib/cur/stdlib/sugar.rkt @@ -32,14 +32,32 @@ [define real-define])) (begin-for-syntax - (define-syntax-class result-type - (pattern type:expr)) + (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 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 - (pattern (name:id (~datum :) type:expr)) + (pattern (name:id (~datum :) type:cur-term)) (pattern - type:expr + type:cur-term #:attr name (format-id #'type "~a" (gensym 'anon-parameter))))) ;; A multi-arity function type; takes parameter declaration of either @@ -48,7 +66,7 @@ ;; (-> (A : Type) A A) (define-syntax (-> syn) (syntax-parse syn - [(_ d:parameter-declaration ...+ result:result-type) + [(_ d:parameter-declaration ...+ result:cur-term) (foldr (lambda (src name type r) (quasisyntax/loc src (forall (#,name : #,type) #,r))) @@ -83,16 +101,6 @@ (attribute d.type))])) (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 (pattern ((~literal forall) ~! (parameter-name:id (~datum :) parameter-type) body))) @@ -111,18 +119,7 @@ (format "Expected ~a to be a function, but inferred type ~a" (syntax->datum #'e) - (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")))) + (syntax->datum (attribute type)))))) (define-syntax (#%app syn) (syntax-parse syn