Move code for top-interaction commands to their own file.
Also adds some more test cases.
This commit is contained in:
parent
5d7710733d
commit
7e0553e037
|
@ -27,6 +27,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
||||||
-lambda -define)
|
-lambda -define)
|
||||||
;; provide the contracted bindings as primitives
|
;; provide the contracted bindings as primitives
|
||||||
(all-from-out "base-contracted.rkt")
|
(all-from-out "base-contracted.rkt")
|
||||||
|
(all-from-out "top-interaction.rkt")
|
||||||
:
|
:
|
||||||
(rename-out [define-typed-struct define-struct:]
|
(rename-out [define-typed-struct define-struct:]
|
||||||
[lambda: λ:]
|
[lambda: λ:]
|
||||||
|
@ -52,6 +53,7 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
||||||
(rename-in racket/contract/base [-> c->] [case-> c:case->])
|
(rename-in racket/contract/base [-> c->] [case-> c:case->])
|
||||||
;; contracted bindings to replace built-in ones
|
;; contracted bindings to replace built-in ones
|
||||||
(except-in "base-contracted.rkt" initialize-contracted)
|
(except-in "base-contracted.rkt" initialize-contracted)
|
||||||
|
"top-interaction.rkt"
|
||||||
"base-types.rkt"
|
"base-types.rkt"
|
||||||
"base-types-extra.rkt"
|
"base-types-extra.rkt"
|
||||||
'struct-extraction
|
'struct-extraction
|
||||||
|
@ -316,16 +318,6 @@ This file defines two sorts of primitives. All of them are provided into any mod
|
||||||
#:typed-side #f
|
#:typed-side #f
|
||||||
(type->contract-fail typ #'ty)))))])]))
|
(type->contract-fail typ #'ty)))))])]))
|
||||||
|
|
||||||
(define-for-syntax (fail stx)
|
|
||||||
(syntax-parse stx
|
|
||||||
[_:id
|
|
||||||
(raise-syntax-error #f "must be applied to arguments" stx)]
|
|
||||||
[_ (raise-syntax-error #f "only valid at the top-level of an interaction" stx)]))
|
|
||||||
(define-syntax :type fail)
|
|
||||||
(define-syntax :print-type fail)
|
|
||||||
(define-syntax :query-type/args fail)
|
|
||||||
(define-syntax :query-type/result fail)
|
|
||||||
|
|
||||||
(define-syntax (require/opaque-type stx)
|
(define-syntax (require/opaque-type stx)
|
||||||
(define-syntax-class name-exists-kw
|
(define-syntax-class name-exists-kw
|
||||||
(pattern #:name-exists))
|
(pattern #:name-exists))
|
||||||
|
|
|
@ -0,0 +1,117 @@
|
||||||
|
#lang racket/base
|
||||||
|
|
||||||
|
(require
|
||||||
|
"../utils/utils.rkt"
|
||||||
|
(for-syntax
|
||||||
|
racket/base
|
||||||
|
racket/match
|
||||||
|
racket/format
|
||||||
|
racket/string
|
||||||
|
racket/list
|
||||||
|
syntax/stx
|
||||||
|
syntax/parse
|
||||||
|
"../tc-setup.rkt"
|
||||||
|
(private parse-type syntax-properties)
|
||||||
|
(types utils abbrev printer)
|
||||||
|
(typecheck tc-toplevel tc-app-helper)
|
||||||
|
(rep type-rep)
|
||||||
|
(utils tc-utils)))
|
||||||
|
(provide
|
||||||
|
(for-syntax
|
||||||
|
interactive-command?
|
||||||
|
interactive-command-procedure)
|
||||||
|
|
||||||
|
:type :print-type :query-type/args :query-type/result)
|
||||||
|
|
||||||
|
(define-for-syntax (fail _ stx)
|
||||||
|
(syntax-parse stx
|
||||||
|
[_:id
|
||||||
|
(raise-syntax-error #f "must be applied to arguments" stx)]
|
||||||
|
[_ (raise-syntax-error #f "only valid at the top-level of an interaction" stx)]))
|
||||||
|
|
||||||
|
(begin-for-syntax
|
||||||
|
(struct interactive-command (procedure)
|
||||||
|
#:property prop:procedure fail))
|
||||||
|
|
||||||
|
|
||||||
|
(define-syntax :type
|
||||||
|
(interactive-command
|
||||||
|
(λ (stx init)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_ (~optional (~and #:verbose verbose-kw)) ty:expr)
|
||||||
|
(parameterize ([current-print-type-fuel
|
||||||
|
(if (attribute verbose-kw) +inf.0 1)]
|
||||||
|
;; This makes sure unions are totally flat for the
|
||||||
|
;; infinite fuel case. If fuel that's not 0, 1, or +inf.0
|
||||||
|
;; is ever used, more may need to be done.
|
||||||
|
[current-type-names
|
||||||
|
(if (attribute verbose-kw) '() (current-type-names))]
|
||||||
|
[current-print-unexpanded (box '())])
|
||||||
|
(define type (format "~a" (parse-type #'ty)))
|
||||||
|
(define unexpanded
|
||||||
|
(remove-duplicates (unbox (current-print-unexpanded))))
|
||||||
|
(define cue (if (null? unexpanded)
|
||||||
|
""
|
||||||
|
(format "[can expand further: ~a]"
|
||||||
|
(string-join (map ~a unexpanded)))))
|
||||||
|
#`(display #,(format "~a\n~a" type cue)))]
|
||||||
|
[form
|
||||||
|
(raise-syntax-error #f "must be applied to exactly one argument" #'form)]))))
|
||||||
|
|
||||||
|
;; TODO what should be done with stx
|
||||||
|
;; Prints the _entire_ type. May be quite large.
|
||||||
|
(define-syntax :print-type
|
||||||
|
(interactive-command
|
||||||
|
(λ (stx init)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_ e)
|
||||||
|
(tc-setup #'stx #'e 'top-level expanded init tc-toplevel-form before type
|
||||||
|
#`(display
|
||||||
|
#,(parameterize ([print-multi-line-case-> #t])
|
||||||
|
(format "~a\n" (match type
|
||||||
|
[(tc-result1: t f o) t]
|
||||||
|
[(tc-results: t) (-values t)]
|
||||||
|
[(tc-any-results:) ManyUniv])))))]
|
||||||
|
[form
|
||||||
|
(raise-syntax-error #f "must be applied to exactly one argument" #'form)]))))
|
||||||
|
|
||||||
|
;; given a function and input types, display the result type
|
||||||
|
(define-syntax :query-type/args
|
||||||
|
(interactive-command
|
||||||
|
(λ (stx init)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_ op arg-type ...)
|
||||||
|
(with-syntax ([(dummy-arg ...) (generate-temporaries #'(arg-type ...))])
|
||||||
|
(tc-setup #'stx
|
||||||
|
;; create a dummy function with the right argument types
|
||||||
|
#`(lambda #,(stx-map type-label-property
|
||||||
|
#'(dummy-arg ...) #'(arg-type ...))
|
||||||
|
(op dummy-arg ...))
|
||||||
|
'top-level expanded init tc-toplevel-form before type
|
||||||
|
#`(display
|
||||||
|
#,(format "~a\n"
|
||||||
|
(match type
|
||||||
|
[(tc-result1: (and t (Function: _)) f o) t])))))]
|
||||||
|
[form
|
||||||
|
(raise-syntax-error #f "must be applied to at least one argument" #'form)]))))
|
||||||
|
|
||||||
|
;; given a function and a desired return type, fill in the blanks
|
||||||
|
(define-syntax :query-type/result
|
||||||
|
(interactive-command
|
||||||
|
(λ (stx init)
|
||||||
|
(syntax-parse stx
|
||||||
|
[(_ op desired-type)
|
||||||
|
(let ([expected (parse-type #'desired-type)])
|
||||||
|
(tc-setup #'stx #'op 'top-level expanded init tc-toplevel-form before type
|
||||||
|
(match type
|
||||||
|
[(tc-result1: (and t (Function: _)) f o)
|
||||||
|
(let ([cleaned (cleanup-type t expected)])
|
||||||
|
#`(display
|
||||||
|
#,(match cleaned
|
||||||
|
[(Function: '())
|
||||||
|
"Desired return type not in the given function's range."]
|
||||||
|
[(Function: arrs)
|
||||||
|
(format "~a\n" cleaned)])))]
|
||||||
|
[_ (error (format "~a: not a function" (syntax->datum #'op) ))])))]
|
||||||
|
[form
|
||||||
|
(raise-syntax-error #f "must be applied to exactly two arguments" #'form)]))))
|
|
@ -3,15 +3,13 @@
|
||||||
(require (rename-in "utils/utils.rkt")
|
(require (rename-in "utils/utils.rkt")
|
||||||
(for-syntax racket/base)
|
(for-syntax racket/base)
|
||||||
(for-template racket/base)
|
(for-template racket/base)
|
||||||
(private with-types type-contract parse-type syntax-properties)
|
(private with-types type-contract)
|
||||||
(except-in syntax/parse id)
|
(except-in syntax/parse id)
|
||||||
racket/match racket/syntax racket/list syntax/stx
|
racket/match racket/syntax
|
||||||
racket/format
|
(types utils abbrev generalize)
|
||||||
(only-in racket/string string-join)
|
|
||||||
(types utils abbrev generalize printer)
|
|
||||||
(typecheck provide-handling tc-toplevel tc-app-helper)
|
(typecheck provide-handling tc-toplevel tc-app-helper)
|
||||||
(rep type-rep)
|
(rep type-rep)
|
||||||
(for-template (only-in (base-env prims) :type :print-type :query-type/args :query-type/result))
|
(for-template (base-env top-interaction))
|
||||||
(utils utils tc-utils arm)
|
(utils utils tc-utils arm)
|
||||||
"tc-setup.rkt")
|
"tc-setup.rkt")
|
||||||
|
|
||||||
|
@ -53,69 +51,8 @@
|
||||||
(syntax-parse stx
|
(syntax-parse stx
|
||||||
[(_ . ((~datum module) . rest))
|
[(_ . ((~datum module) . rest))
|
||||||
#'(module . rest)]
|
#'(module . rest)]
|
||||||
[(_ . ((~literal :type)
|
[(_ . (~and form ((~var command (static interactive-command? #f)) . _)))
|
||||||
(~optional (~and #:verbose verbose-kw))
|
((interactive-command-procedure (attribute command.value)) #'form init)]
|
||||||
ty:expr))
|
|
||||||
(parameterize ([current-print-type-fuel
|
|
||||||
(if (attribute verbose-kw) +inf.0 1)]
|
|
||||||
;; This makes sure unions are totally flat for the
|
|
||||||
;; infinite fuel case. If fuel that's not 0, 1, or +inf.0
|
|
||||||
;; is ever used, more may need to be done.
|
|
||||||
[current-type-names
|
|
||||||
(if (attribute verbose-kw) '() (current-type-names))]
|
|
||||||
[current-print-unexpanded (box '())])
|
|
||||||
(define type (format "~a" (parse-type #'ty)))
|
|
||||||
(define unexpanded
|
|
||||||
(remove-duplicates (unbox (current-print-unexpanded))))
|
|
||||||
(define cue (if (null? unexpanded)
|
|
||||||
""
|
|
||||||
(format "[can expand further: ~a]"
|
|
||||||
(string-join (map ~a unexpanded)))))
|
|
||||||
#`(display #,(format "~a\n~a" type cue)))]
|
|
||||||
[(_ . (~and form ((~literal :type) . _)))
|
|
||||||
(raise-syntax-error #f "must be applied to exactly one argument" #'form)]
|
|
||||||
;; Prints the _entire_ type. May be quite large.
|
|
||||||
[(_ . ((~literal :print-type) e))
|
|
||||||
(tc-setup #'stx #'e 'top-level expanded init tc-toplevel-form before type
|
|
||||||
#`(display
|
|
||||||
#,(parameterize ([print-multi-line-case-> #t])
|
|
||||||
(format "~a\n" (match type
|
|
||||||
[(tc-result1: t f o) t]
|
|
||||||
[(tc-results: t) (cons 'Values t)]
|
|
||||||
[(tc-any-results:) ManyUniv])))))]
|
|
||||||
[(_ . (~and form ((~literal :print-type) . _)))
|
|
||||||
(raise-syntax-error #f "must be applied to exactly one argument" #'form)]
|
|
||||||
;; given a function and input types, display the result type
|
|
||||||
[(_ . ((~literal :query-type/args) op arg-type ...))
|
|
||||||
(with-syntax ([(dummy-arg ...) (generate-temporaries #'(arg-type ...))])
|
|
||||||
(tc-setup #'stx
|
|
||||||
;; create a dummy function with the right argument types
|
|
||||||
#`(lambda #,(stx-map type-label-property
|
|
||||||
#'(dummy-arg ...) #'(arg-type ...))
|
|
||||||
(op dummy-arg ...))
|
|
||||||
'top-level expanded init tc-toplevel-form before type
|
|
||||||
#`(display
|
|
||||||
#,(format "~a\n"
|
|
||||||
(match type
|
|
||||||
[(tc-result1: (and t (Function: _)) f o) t])))))]
|
|
||||||
[(_ . (~and form ((~literal :query-type/args) . _)))
|
|
||||||
(raise-syntax-error #f "must be applied to at least one argument" #'form)]
|
|
||||||
;; given a function and a desired return type, fill in the blanks
|
|
||||||
[(_ . ((~literal :query-type/result) op desired-type))
|
|
||||||
(let ([expected (parse-type #'desired-type)])
|
|
||||||
(tc-setup #'stx #'op 'top-level expanded init tc-toplevel-form before type
|
|
||||||
(match type
|
|
||||||
[(tc-result1: (and t (Function: _)) f o)
|
|
||||||
(let ([cleaned (cleanup-type t expected)])
|
|
||||||
#`(display
|
|
||||||
#,(match cleaned
|
|
||||||
[(Function: '())
|
|
||||||
"Desired return type not in the given function's range."]
|
|
||||||
[(Function: arrs)
|
|
||||||
(format "~a\n" cleaned)])))]
|
|
||||||
[_ (error (format "~a: not a function" (syntax->datum #'op) ))])))]
|
|
||||||
[(_ . (~and form ((~literal :query-type/result) . _)))
|
|
||||||
(raise-syntax-error #f "must be applied to exactly two arguments" #'form)]
|
|
||||||
[(_ . form)
|
[(_ . form)
|
||||||
(init)
|
(init)
|
||||||
(tc-setup
|
(tc-setup
|
||||||
|
|
|
@ -43,6 +43,7 @@
|
||||||
(eval `(#%top-interaction .
|
(eval `(#%top-interaction .
|
||||||
,(syntax->datum #'form)) (force promised-ns)))))))]))
|
,(syntax->datum #'form)) (force promised-ns)))))))]))
|
||||||
|
|
||||||
|
;; Add 'only at the toplevel tests'
|
||||||
(define (interactive-tests)
|
(define (interactive-tests)
|
||||||
(test-suite "Interactive tests"
|
(test-suite "Interactive tests"
|
||||||
(test-form #rx"1"
|
(test-form #rx"1"
|
||||||
|
@ -51,8 +52,10 @@
|
||||||
(:type Byte))
|
(:type Byte))
|
||||||
(test-form (regexp-quote "(U 0 1 Byte-Larger-Than-One")
|
(test-form (regexp-quote "(U 0 1 Byte-Larger-Than-One")
|
||||||
(:type #:verbose Byte))
|
(:type #:verbose Byte))
|
||||||
(test-form-exn #rx"applied to arguments"
|
(test-form-exn #rx":type.*applied to arguments"
|
||||||
:type)
|
:type)
|
||||||
|
(test-form-exn #rx":type.*only valid at the top-level"
|
||||||
|
(list (:type)))
|
||||||
(test-form-exn #rx"exactly one argument"
|
(test-form-exn #rx"exactly one argument"
|
||||||
(:type))
|
(:type))
|
||||||
(test-form-exn #rx"exactly one argument"
|
(test-form-exn #rx"exactly one argument"
|
||||||
|
@ -60,20 +63,34 @@
|
||||||
(test-form-exn #rx"exactly one argument"
|
(test-form-exn #rx"exactly one argument"
|
||||||
(:type #:verbose))
|
(:type #:verbose))
|
||||||
|
|
||||||
(test-form-exn #rx"applied to arguments"
|
(test-form #rx"Positive-Index"
|
||||||
|
(:print-type (+ 1 1)))
|
||||||
|
(test-form (regexp-quote "(values One One)")
|
||||||
|
(:print-type (values 1 1)))
|
||||||
|
(test-form-exn #rx":print-type.*applied to arguments"
|
||||||
:print-type)
|
:print-type)
|
||||||
|
(test-form-exn #rx":print-type.*only valid at the top-level"
|
||||||
|
(list (:print-type)))
|
||||||
(test-form-exn #rx"exactly one argument"
|
(test-form-exn #rx"exactly one argument"
|
||||||
(:print-type))
|
(:print-type))
|
||||||
(test-form-exn #rx"exactly one argument"
|
(test-form-exn #rx"exactly one argument"
|
||||||
(:print-type 1 2))
|
(:print-type 1 2))
|
||||||
|
|
||||||
(test-form-exn #rx"applied to arguments"
|
(test-form (regexp-quote "(4 Zero -> Zero)")
|
||||||
|
(:query-type/args * 4 0))
|
||||||
|
(test-form-exn #rx":query-type/args.*applied to arguments"
|
||||||
:query-type/args)
|
:query-type/args)
|
||||||
|
(test-form-exn #rx":query-type/args.*only valid at the top-level"
|
||||||
|
(list (:query-type/args)))
|
||||||
(test-form-exn #rx"at least one argument"
|
(test-form-exn #rx"at least one argument"
|
||||||
(:query-type/args))
|
(:query-type/args))
|
||||||
|
|
||||||
(test-form-exn #rx"applied to arguments"
|
(test-form (regexp-quote "(case-> (One -> One) (-> One))")
|
||||||
|
(:query-type/result * 1))
|
||||||
|
(test-form-exn #rx":query-type/result.*applied to arguments"
|
||||||
:query-type/result)
|
:query-type/result)
|
||||||
|
(test-form-exn #rx":query-type/result.*only valid at the top-level"
|
||||||
|
(list (:query-type/result)))
|
||||||
(test-form-exn #rx"exactly two arguments"
|
(test-form-exn #rx"exactly two arguments"
|
||||||
(:query-type/result))
|
(:query-type/result))
|
||||||
(test-form-exn #rx"exactly two arguments"
|
(test-form-exn #rx"exactly two arguments"
|
||||||
|
|
Loading…
Reference in New Issue
Block a user