diff --git a/collects/tests/typed-scheme/succeed/paths.rkt b/collects/tests/typed-scheme/succeed/paths.rkt new file mode 100644 index 0000000000..aa752e1ac8 --- /dev/null +++ b/collects/tests/typed-scheme/succeed/paths.rkt @@ -0,0 +1,58 @@ +#lang typed/racket + +(: foo-path Path) +(define foo-path (build-path "foo" "bar" 'same 'up)) + +;Check predicates are always true +(+ (if (path? foo-path) 2 'two) + (if (path-for-some-system? foo-path) 3 'three)) + +(: current-system (U 'unix 'windows)) +(define current-system (system-path-convention-type)) + +(: other-system (U 'unix 'windows)) +(define other-system + (case (system-path-convention-type) + ((unix) 'windows) + ((windows) 'unix))) + +(: other-foo-path SomeSystemPath) +(define other-foo-path + (build-path/convention-type other-system + (string->some-system-path "foo" other-system) + (string->some-system-path "bar" other-system) + 'same + 'up)) + + +(path->string foo-path) +(some-system-path->string other-foo-path) +(path->bytes foo-path) +(path->bytes other-foo-path) + +(bytes->path #"foo" other-system) +(string->path "foo") + +(bytes->path-element #"foo" other-system) +(string->path-element "foo") + + +(cleanse-path foo-path) +(cleanse-path other-foo-path) + +(expand-user-path foo-path) + +(absolute-path? other-foo-path) +(relative-path? other-foo-path) +(complete-path? other-foo-path) + + + + +(split-path foo-path) +(split-path other-foo-path) + + +;Original Soundness bug +(when (path? other-foo-path) (error 'path "This shouldn't be raised")) + diff --git a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt index b3cee8beec..07c0b0b833 100644 --- a/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt +++ b/collects/tests/typed-scheme/unit-tests/typecheck-tests.rkt @@ -868,6 +868,25 @@ [tc-e (in-hash #hash((1 . 2))) (-seq -Integer -Integer)] [tc-e (in-hash-keys #hash((1 . 2))) (-seq -Integer)] [tc-e (in-hash-values #hash((1 . 2))) (-seq -Integer)] + + ;;Path tests + (tc-e (bytes->path #"foo" 'unix) -SomeSystemPath) + (tc-e (bytes->path #"foo") -Path) + (tc-e (bytes->path-element #"foo") -Path) + (tc-e (bytes->path-element #"foo" 'windows) -SomeSystemPath) + + (tc-e (cleanse-path "foo") -Path) + (tc-e (cleanse-path (string->some-system-path "foo" 'unix)) -SomeSystemPath) + (tc-e (simplify-path "foo") -Path) + (tc-e (simplify-path "foo" #t) -Path) + (tc-e (simplify-path (string->some-system-path "foo" 'unix) #f) -SomeSystemPath) + (tc-e (path->directory-path "foo") -Path) + (tc-e (path->directory-path (string->some-system-path "foo" 'unix)) -SomeSystemPath) + + + + + ) (test-suite "check-type tests" diff --git a/collects/typed-scheme/base-env/base-env.rkt b/collects/typed-scheme/base-env/base-env.rkt index 96ef4b2495..9cea054ae3 100644 --- a/collects/typed-scheme/base-env/base-env.rkt +++ b/collects/typed-scheme/base-env/base-env.rkt @@ -391,10 +391,8 @@ [string-copy (-> -String -String)] [string->immutable-string (-> -String -String)] -[string->path (-> -String -Path)] -[build-path ((list -SomeSystemPathlike*) -SomeSystemPathlike* . ->* . -Path)] [with-input-from-file (-poly (a) (->key -Pathlike (-> a) #:mode (one-of/c 'binary 'text) #f a))] [with-output-to-file @@ -532,7 +530,6 @@ [seconds->date (-Integer . -> . (make-Name #'date))] [current-seconds (-> -Integer)] [current-print (-Param (Univ . -> . Univ) (Univ . -> . Univ))] -[path->string (-> -Path -String)] [link-exists? (-> -Pathlike B)] [directory-exists? (-> -Pathlike B)] @@ -550,6 +547,88 @@ [file-size (-> -Pathlike -Nat)] +;; path manipulation + +[path? (make-pred-ty -Path)] +[path-string? (-> Univ B)] +[path-for-some-system? (make-pred-ty -SomeSystemPath)] + +[string->path (-> -String -Path)] +[bytes->path (cl->* (-> -Bytes -Path) (-> -Bytes -PathConventionType -SomeSystemPath))] +[path->string (-> -Path -String)] +[path->bytes (-> -SomeSystemPath -Bytes)] + +[string->path-element (-> -String -Path)] +[bytes->path-element (cl->* (-> -Bytes -Path) (-> -Bytes -PathConventionType -SomeSystemPath))] +[path-element->string (-> -Path -String)] +[path-element->bytes (-> -SomeSystemPath -Bytes)] + +[path-convention-type (-> -SomeSystemPath -PathConventionType)] +[system-path-convention-type (-> -PathConventionType)] + + + +[build-path (cl->* + ((list -Pathlike*) -Pathlike* . ->* . -Path) + ((list -SomeSystemPathlike*) -SomeSystemPathlike* . ->* . -SomeSystemPath))] +[build-path/convention-type + ((list -PathConventionType -SomeSystemPathlike*) -SomeSystemPathlike* . ->* . -SomeSystemPath)] + +[absolute-path? (-> -SomeSystemPath B)] +[relative-path? (-> -SomeSystemPath B)] +[complete-path? (-> -SomeSystemPath B)] + +[path->complete-path + (cl->* (-> -Pathlike -Path) + (-> -Pathlike -Pathlike -Path) + (-> -SomeSystemPathlike -SomeSystemPathlike -SomeSystemPath))] + +[path->directory-path + (cl->* (-> -Pathlike -Path) + (-> -SomeSystemPathlike -SomeSystemPath))] + +[resolve-path (-> -Path -Path)] +[cleanse-path + (cl->* (-> -Pathlike -Path) + (-> -SomeSystemPathlike -SomeSystemPath))] +[expand-user-path (-> -Path -Path)] + +[simplify-path + (cl->* + (-Pathlike . -> . -Path) + (-Pathlike B . -> . -Path) + (-SomeSystemPathlike B . -> . -SomeSystemPath))] + +[normal-case-path + (cl->* (-> -Pathlike -Path) + (-> -SomeSystemPathlike -SomeSystemPath))] + +[split-path + (cl->* + (-> -Pathlike + (-values (list + (Un -Path (-val 'relative) (-val #f)) + (Un -Path (-val 'up) (-val 'same)) + B))) + (-> -SomeSystemPathlike + (-values (list + (Un -SomeSystemPath (-val 'relative) (-val #f)) + (Un -SomeSystemPath (-val 'up) (-val 'same)) + B))))] + +[path-replace-suffix + (cl->* + (-> -Pathlike (Un -String -Bytes) -Path) + (-> -SomeSystemPathlike (Un -String -Bytes) -SomeSystemPath))] + +[path-add-suffix + (cl->* + (-> -Pathlike (Un -String -Bytes) -Path) + (-> -SomeSystemPathlike (Un -String -Bytes) -SomeSystemPath))] + + + + [hash? (make-pred-ty (make-HashtableTop))] [hash-eq? (-> (make-HashtableTop) B)] [hash-eqv? (-> (make-HashtableTop) B)] @@ -749,8 +828,6 @@ [object-name (Univ . -> . Univ)] -[path? (make-pred-ty -Path)] -[path-for-some-system? (make-pred-ty -SomeSystemPath)] ;; scheme/function [const (-poly (a) (-> a (->* '() Univ a)))] @@ -855,11 +932,6 @@ [string->some-system-path (-String (Un (-val 'unix) (-val 'windows)) . -> . -SomeSystemPath)] -[simplify-path (-SomeSystemPathlike [B] . ->opt . -SomeSystemPath)] -[path->complete-path - (cl->* (-> -Pathlike -Path) - (-> -SomeSystemPathlike -SomeSystemPathlike -SomeSystemPath))] -[system-path-convention-type (-> (Un (-val 'unix) (-val 'windows)))] ;; scheme/file diff --git a/collects/typed-scheme/types/abbrev.rkt b/collects/typed-scheme/types/abbrev.rkt index b9778e438d..ab4641c28c 100644 --- a/collects/typed-scheme/types/abbrev.rkt +++ b/collects/typed-scheme/types/abbrev.rkt @@ -166,8 +166,10 @@ (define -SomeSystemPath (*Un -Path -OtherSystemPath)) (define -Pathlike (*Un -String -Path)) (define -SomeSystemPathlike (*Un -String -SomeSystemPath)) -;(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same))) +(define -Pathlike* (*Un -String -Path (-val 'up) (-val 'same))) (define -SomeSystemPathlike* (*Un -String -SomeSystemPath(-val 'up) (-val 'same))) +(define -PathConventionType (*Un (-val 'unix) (-val 'windows))) + (define -Pattern (*Un -Bytes -Regexp -PRegexp -Byte-Regexp -Byte-PRegexp -String)) (define -top (make-Top))