hash tables
This commit is contained in:
parent
2ddafb240a
commit
39d81686fd
|
@ -714,13 +714,10 @@
|
|||
[(~Discard _)
|
||||
#t]
|
||||
[(X:id Y:id)
|
||||
#;(printf "id case!\n")
|
||||
(free-identifier=? #'X #'Y)]
|
||||
[((~∀ (X:id ...) τ1) (~∀ (Y:id ...) τ2))
|
||||
#:when (stx-length=? #'(X ...) #'(Y ...))
|
||||
#:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2)
|
||||
#;(printf "in ∀!\n")
|
||||
#;(printf "τ2-X/Y = ~a\n" #'τ2-X/Y)
|
||||
(<: #'τ1 #'τ2-X/Y)]
|
||||
[((~Base τ1:id) (~Base τ2:id))
|
||||
(free-identifier=? #'τ1 #'τ2)]
|
||||
|
@ -744,7 +741,6 @@
|
|||
#t]))]
|
||||
;; TODO: clauses for Roles, and so on
|
||||
[_
|
||||
#;(printf "ids? ~a, ~a\n" (identifier? t1) (identifier? t2))
|
||||
#f]))
|
||||
|
||||
;; shortcuts for mapping
|
||||
|
|
|
@ -0,0 +1,68 @@
|
|||
#lang turnstile
|
||||
|
||||
(provide Hash
|
||||
(for-syntax ~Hash)
|
||||
hash
|
||||
hash-set
|
||||
hash-ref
|
||||
hash-has-key?
|
||||
hash-update
|
||||
hash-remove
|
||||
hash-map
|
||||
hash-keys
|
||||
hash-values
|
||||
hash-keys-subset?
|
||||
hash-count
|
||||
hash-empty?
|
||||
hash-union
|
||||
)
|
||||
|
||||
(require "core-types.rkt")
|
||||
(require (only-in "list.rkt" List))
|
||||
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
;; Immutable Hash Tables
|
||||
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
|
||||
|
||||
(define-container-type Hash #:arity = 2)
|
||||
|
||||
(begin-for-syntax
|
||||
(define-splicing-syntax-class key-val-list
|
||||
#:attributes (items)
|
||||
(pattern (~seq k1 v1 rest:key-val-list)
|
||||
#:attr items #`((k1 v1) #,@#'rest.items))
|
||||
(pattern (~seq)
|
||||
#:attr items #'())))
|
||||
|
||||
(define-typed-syntax (hash keys&vals:key-val-list) ≫
|
||||
#:with ((key val) ...) #'keys&vals.items
|
||||
[⊢ key ≫ key- (⇒ : τ-k)] ...
|
||||
[⊢ val ≫ val- (⇒ : τ-val)] ...
|
||||
#:fail-unless (all-pure? #'(key- ... val- ...)) "gotta be pure"
|
||||
#:with together-again (stx-flatten #'((key- val-) ...))
|
||||
--------------------------------------------------
|
||||
[⊢ (hash- #,@#'together-again) (⇒ : (Hash (U τ-k ...) (U τ-val ...)))])
|
||||
|
||||
(require/typed racket/base
|
||||
;; don't have a type for ConsPair
|
||||
#;[make-hash : (∀ (K V) (→fn (List (ConsPair K V)) (Hash K V)))]
|
||||
[hash-set : (∀ (K V) (→fn (Hash K V) K V (Hash K V)))]
|
||||
[hash-ref : (∀ (K V) (→fn (Hash K V) K V))]
|
||||
;; TODO hash-ref/failure
|
||||
[hash-has-key? : (∀ (K V) (→fn (Hash K V) K Bool))]
|
||||
[hash-update : (∀ (K V) (→fn (Hash K V) (→fn V V) K (Hash K V)))]
|
||||
;; TODO hash-update/failure
|
||||
[hash-remove : (∀ (K V) (→fn (Hash K V) K (Hash K V)))]
|
||||
[hash-map : (∀ (K V R) (→fn (Hash K V) (→fn K V R) (List R)))]
|
||||
[hash-keys : (∀ (K V) (→fn (Hash K V) (List K)))]
|
||||
[hash-values : (∀ (K V) (→fn (Hash K V) (List V)))]
|
||||
;; TODO hash->list makes cons pairs
|
||||
#;[hash->list : (∀ (K V) (→fn (Hash K V) (List (ConsPair K V))))]
|
||||
[hash-keys-subset? : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) Bool))]
|
||||
[hash-count : (∀ (K V) (→fn (Hash K V) Int))]
|
||||
[hash-empty? : (∀ (K V) (→fn (Hash K V) Bool))])
|
||||
|
||||
(require/typed racket/hash
|
||||
[hash-union : (∀ (K1 V1 K2 V2) (→fn (Hash K1 V1) (Hash K2 V2) (Hash (U K1 K2) (U V1 V2))))]
|
||||
;; TODO - hash-union with #:combine
|
||||
)
|
|
@ -39,6 +39,8 @@
|
|||
(all-from-out "set.rkt")
|
||||
;; sequences
|
||||
(all-from-out "sequence.rkt")
|
||||
;; hash tables
|
||||
(all-from-out "hash.rkt")
|
||||
;; DEBUG and utilities
|
||||
print-type print-role
|
||||
;; Extensions
|
||||
|
@ -54,6 +56,7 @@
|
|||
(require "set.rkt")
|
||||
(require "prim.rkt")
|
||||
(require "sequence.rkt")
|
||||
(require "hash.rkt")
|
||||
|
||||
(require (prefix-in syndicate: syndicate/actor-lang))
|
||||
|
||||
|
|
|
@ -0,0 +1,34 @@
|
|||
#lang typed/syndicate/roles
|
||||
|
||||
(require rackunit/turnstile)
|
||||
|
||||
(check-type (hash) : (Hash (U) (U)))
|
||||
|
||||
(check-type (hash 1 2) : (Hash Int Int))
|
||||
|
||||
(check-type (hash "greetings" 8) : (Hash String Int))
|
||||
|
||||
(check-type (hash "smelly" 0
|
||||
"feet" 18
|
||||
"robust" 9)
|
||||
: (Hash String Int))
|
||||
|
||||
(check-type (hash "smelly" 0
|
||||
"feet" "grosss"
|
||||
"robust" #t)
|
||||
: (Hash String (U Int String Bool)))
|
||||
|
||||
(define a-hash
|
||||
(hash "smelly" 0
|
||||
"feet" 18
|
||||
"robust" 9))
|
||||
|
||||
(define hash-ref/inst (inst hash-ref String Int))
|
||||
|
||||
(check-type (hash-ref/inst a-hash "smelly")
|
||||
: Int
|
||||
⇒ 0)
|
||||
|
||||
(check-type ((inst hash-count String Int) a-hash)
|
||||
: Int
|
||||
⇒ 3)
|
Loading…
Reference in New Issue