#lang scheme/base (require (for-syntax scheme/base scheme/list "static-rep.ss" "syntax-meta.ss" "../proof/proof.ss" "../proof/syntax.ss") "module.ss") (provide top-interaction-macro module-begin-macro) (define-for-syntax (expand-top-interaction stx) (syntax-case stx () [(_ . body) (syntax/loc stx (#%top-interaction . body))])) (define-for-syntax (get-module-name stx) (syntax-case stx (module-macro) [(module-macro name . _) (identifier? #'name) #'name] [_ #f])) (define-for-syntax (expand-module-begin stx) (syntax-case stx () [(_ body ...) (with-syntax ([exports (datum->syntax stx `(,#'all-defined-out))] [(name ...) (filter-map get-module-name (syntax->list #'(body ...)))]) (syntax/loc stx (#%plain-module-begin (provide exports) body ... (define-values () (annotate-modules [name ...] (values))))))])) (define-for-syntax (module/static->part id mod) (make-part (syntax-e id) (syntax->loc (module/static-source mod)) (map syntax->term (append (map port/static-abstract (module/static-imports mod)) (module/static-definitions mod) (map port/static-concrete (module/static-exports mod)))))) (define-for-syntax (identifier->part id) (module/static->part id (syntax->meta id))) (define-syntax (annotate-modules stx) (syntax-case stx () [(_ [name ...] expr) (annotate-proof (apply make-proof (map identifier->part (syntax->list #'(name ...)))) #'expr)])) (define-syntax top-interaction-macro expand-top-interaction) (define-syntax module-begin-macro expand-module-begin)