hash tables
This commit is contained in:
parent
af56bc283d
commit
899d8c460d
|
@ -714,13 +714,10 @@
|
||||||
[(~Discard _)
|
[(~Discard _)
|
||||||
#t]
|
#t]
|
||||||
[(X:id Y:id)
|
[(X:id Y:id)
|
||||||
#;(printf "id case!\n")
|
|
||||||
(free-identifier=? #'X #'Y)]
|
(free-identifier=? #'X #'Y)]
|
||||||
[((~∀ (X:id ...) τ1) (~∀ (Y:id ...) τ2))
|
[((~∀ (X:id ...) τ1) (~∀ (Y:id ...) τ2))
|
||||||
#:when (stx-length=? #'(X ...) #'(Y ...))
|
#:when (stx-length=? #'(X ...) #'(Y ...))
|
||||||
#:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2)
|
#:with τ2-X/Y (substs #'(X ...) #'(Y ...) #'τ2)
|
||||||
#;(printf "in ∀!\n")
|
|
||||||
#;(printf "τ2-X/Y = ~a\n" #'τ2-X/Y)
|
|
||||||
(<: #'τ1 #'τ2-X/Y)]
|
(<: #'τ1 #'τ2-X/Y)]
|
||||||
[((~Base τ1:id) (~Base τ2:id))
|
[((~Base τ1:id) (~Base τ2:id))
|
||||||
(free-identifier=? #'τ1 #'τ2)]
|
(free-identifier=? #'τ1 #'τ2)]
|
||||||
|
@ -744,7 +741,6 @@
|
||||||
#t]))]
|
#t]))]
|
||||||
;; TODO: clauses for Roles, and so on
|
;; TODO: clauses for Roles, and so on
|
||||||
[_
|
[_
|
||||||
#;(printf "ids? ~a, ~a\n" (identifier? t1) (identifier? t2))
|
|
||||||
#f]))
|
#f]))
|
||||||
|
|
||||||
;; shortcuts for mapping
|
;; 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")
|
(all-from-out "set.rkt")
|
||||||
;; sequences
|
;; sequences
|
||||||
(all-from-out "sequence.rkt")
|
(all-from-out "sequence.rkt")
|
||||||
|
;; hash tables
|
||||||
|
(all-from-out "hash.rkt")
|
||||||
;; DEBUG and utilities
|
;; DEBUG and utilities
|
||||||
print-type print-role
|
print-type print-role
|
||||||
;; Extensions
|
;; Extensions
|
||||||
|
@ -54,6 +56,7 @@
|
||||||
(require "set.rkt")
|
(require "set.rkt")
|
||||||
(require "prim.rkt")
|
(require "prim.rkt")
|
||||||
(require "sequence.rkt")
|
(require "sequence.rkt")
|
||||||
|
(require "hash.rkt")
|
||||||
|
|
||||||
(require (prefix-in syndicate: syndicate/actor-lang))
|
(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