Skip to content
Browse files

Assoc on the type level.

eg. (Assoc '{} ':a Number) <: '{:a Number}

Also works with type variables.

  (fn [a] (assoc a :a 1))

is of type

  (All [[x :< (Map Any Any)]]
    [x -> (Assoc x ':a Number)])

and can be applied

  (ann-form (f {:b 1}) '{:a Number :b Number})
  • Loading branch information...
1 parent 4e4a269 commit 0c97ef80b7a3aaef72a7975f3164466323feee62 @frenchy64 frenchy64 committed
View
4 src/main/clojure/clojure/core/typed/base_env.clj
@@ -1450,6 +1450,10 @@ clojure.core.match/backtrack Exception
; (rec x b ... b)])))
;
; clojure.core/assoc
+; (All [[h <: (IPersistentMap Any Any)]
+; a b e ...2]
+; [h k ...2 a b -> (Assoc h k ...2 a b)])
+;
; (Label [rec]
; (All [[h :< (HMap {})] x y [k :< (I AnyValue Keyword)] [e :< k] :dotted [b]]
; [h k v -> (I h (HMap k v))]
View
12 src/main/clojure/clojure/core/typed/check.clj
@@ -1071,7 +1071,9 @@
bbnds (c/Poly-bbnds* fs-names fexpr-type)
_ (assert (r/FnIntersection? fin))
;; Only infer free variables in the return type
- ret-type (loop [[{:keys [dom rng rest drest kws] :as ftype} & ftypes] (.types fin)]
+ ret-type
+ (free-ops/with-bounded-frees (zipmap (map r/F-maker fs-names) bbnds)
+ (loop [[{:keys [dom rng rest drest kws] :as ftype} & ftypes] (.types fin)]
(when ftype
#_(prn "infer poly fn" (prs/unparse-type ftype) (map prs/unparse-type arg-types)
(count dom) (count arg-types))
@@ -1158,7 +1160,7 @@
(if drest
(do (u/tc-delayed-error (str "Cannot infer arguments to polymorphic functions with dotted rest"))
nil)
- (recur ftypes)))))]
+ (recur ftypes))))))]
(if ret-type
ret-type
(polyapp-type-error fexpr args fexpr-type arg-ret-types expected))))
@@ -1176,7 +1178,9 @@
(not (some :kws (:types pbody)))
[pbody fixed-vars fixed-bnds dotted-var dotted-bnd])))]
(let [;_ (prn "polydots, no kw args")
- inferred-rng (some identity
+ inferred-rng
+ (free-ops/with-bounded-frees (zipmap (map r/F-maker fixed-vars) fixed-bnds)
+ (some identity
(for [{:keys [dom rest ^DottedPretype drest rng] :as ftype} (:types pbody)
;only try inference if argument types match
:when (cond
@@ -1208,7 +1212,7 @@
(check-funapp1 fexpr args
substituted-type arg-ret-types expected :check? false))
(u/tc-delayed-error "Error applying dotted type")
- nil)))))]
+ nil))))))]
;(prn "inferred-rng"inferred-rng)
(if inferred-rng
inferred-rng
View
81 src/main/clojure/clojure/core/typed/cs_gen.clj
@@ -231,7 +231,7 @@
(let [vector' (t/inst vector c c Any Any Any Any)]
(doall
(for> :- c
- [[c1 c2] :- '[c c ], (map vector' longer (concat shorter (repeat srest)))]
+ [[c1 c2] :- '[c c], (map vector' longer (concat shorter (repeat srest)))]
(c-meet c1 c2 (:X c1)))))
(c-meet lrest srest (:X lrest))))
@@ -539,7 +539,61 @@
Svals (map first STvals)
Tvals (map second STvals)]
(cs-gen-list V X Y Svals Tvals)))
-
+
+
+; Completeness matters:
+;
+; (Assoc x ':a Number ':b Long) <: (HMap {:a Number :b Long} :complete? true)
+; (Assoc x ':a Number ':b Long ':c Foo) <!: (HMap {:a Number :b Long} :complete? true)
+ (and (r/AssocType? S)
+ (r/HeterogeneousMap? T))
+ (let [_ (prn "cs-gen Assoc HMap")
+ {:keys [target entries]} S
+ {:keys [types absent-keys]} T
+ Assoc-keys (map first entries)
+ Tkeys (keys types)
+ ; All keys must be keyword values
+ _ (when-not (every? c/keyword-value? (concat Tkeys Assoc-keys absent-keys))
+ (fail! S T))
+ ; All keys explicitly not in T should not appear in the Assoc operation
+ absents-satisfied?
+ (if (c/complete-hmap? T)
+ ; if T is partial, we just need to ensure the absent keys in T
+ ; don't appear in the entries of the Assoc.
+ (empty?
+ (set/intersection
+ (set absent-keys)
+ (set (map first entries))))
+ ; if T is complete, all entries of the Assoc should *only* have
+ ; keys that are mandatory keys of T.
+ (empty?
+ (set/difference
+ (set (map first entries))
+ (set Tkeys))))
+ _ (when-not absents-satisfied?
+ (fail! S T))
+ ;; Isolate the entries of Assoc in a new HMap, with a corresponding expected HMap.
+ ; keys on the right overwrite those on the left.
+ assoc-args-hmap (c/-hmap (into {} entries))
+ expected-assoc-args-hmap (c/-hmap (select-keys (:types assoc-args-hmap) (set Assoc-keys)))
+
+ ;; The target of the Assoc needs all the keys not explicitly Assoc'ed.
+ expected-target-hmap
+ (let [types (select-keys (into {} entries)
+ (set/difference (set Assoc-keys) (set Tkeys)))]
+ (if (c/complete-hmap? T)
+ (c/-complete-hmap types)
+ (c/-partial-hmap types absent-keys)))
+
+ ;_ (prn assoc-args-hmap :< expected-assoc-args-hmap)
+ ;_ (prn (:target S) :< expected-target-hmap)
+ ]
+ (cs-gen-list V X Y
+ [assoc-args-hmap
+ (:target S)]
+ [expected-assoc-args-hmap
+ expected-target-hmap]))
+
(and (r/PrimitiveArray? S)
(r/PrimitiveArray? T)
(impl/checking-clojure?))
@@ -626,11 +680,7 @@
(cs-gen-filter V X Y n1 n2))))
;must be *latent* filter sets
-(t/ann cs-gen-filter-set [NoMentions
- ConstrainVars
- ConstrainVars
- fr/Filter
- fr/Filter
+(t/ann cs-gen-filter-set [NoMentions ConstrainVars ConstrainVars fr/Filter fr/Filter
-> cset])
(defn cs-gen-filter-set [V X Y s t]
{:pre [((u/set-c? symbol?) V)
@@ -971,7 +1021,7 @@
;; dbound : index variable
;; vars : listof[type variable] - temporary variables
;; cset : the constraints being manipulated
-;; takes the constraints on vars and creates a dmap entry contstraining dbound to be |vars|
+;; takes the constraints on vars and creates a dmap entry constraining dbound to be |vars|
;; with the constraints that cset places on vars
(t/ann move-vars-to-dmap [cset Symbol (U nil (t/Seqable Symbol)) -> cset])
;FIXME no-check, flow error
@@ -1029,7 +1079,7 @@
;; The domain of this map is pairs (var . dotted-type).
;; The range is this map is a list of symbols generated on demand, as we need
;; more dots.
-(t/ann DOTTED-VAR-STORE (t/Atom1 (t/Map '[r/Type Symbol] Symbol)))
+(t/ann DOTTED-VAR-STORE (t/Atom1 (t/Map '[r/Type Symbol] (t/Seq Symbol))))
(defonce ^:private DOTTED-VAR-STORE (atom {}))
(t/ann reset-dotted-var-store! [-> nil])
@@ -1185,7 +1235,7 @@
new-tys (doall (for> :- r/AnyType
[var :- Symbol, vars]
(subst/substitute (r/make-F var) dbound t-dty)))
- new-t-arr (r/Function-maker (concat (:dom T) new-tys) (:rng T) nil (r/DottedPretype-maker t-dty dbound) nil)
+ new-t-arr (r/Function-maker (concat (:dom T) new-tys) (:rng T) nil (r/DottedPretype1-maker t-dty dbound) nil)
new-cset (cs-gen-Function V (merge X (zipmap vars (repeat (Y dbound))) X) Y S new-t-arr)]
(move-vars+rest-to-dmap new-cset dbound vars)))))
@@ -1420,9 +1470,14 @@
;; like infer, but dotted-var is the bound on the ...
;; and T-dotted is the repeated type
(t/ann infer-dots
- (Fn [ConstrainVars Symbol Bounds
- (U nil (t/Seqable r/Type)) (U nil (t/Seqable r/Type))
- r/Type (U nil r/AnyType) (t/Set Symbol)
+ (Fn [ConstrainVars
+ Symbol
+ Bounds
+ (U nil (t/Seqable r/Type))
+ (U nil (t/Seqable r/Type))
+ r/Type
+ (U nil r/AnyType)
+ (t/Set Symbol)
& :optional {:expected (U nil r/Type)} -> cr/SubstMap]))
(defn infer-dots [X dotted-var dotted-bnd S T T-dotted R must-vars & {:keys [expected]}]
{:pre [((u/hash-c? symbol? r/Bounds?) X)
View
11 src/main/clojure/clojure/core/typed/fold_default.clj
@@ -13,7 +13,7 @@
CountRange Name Value Top TopFunction B F Result
HeterogeneousSeq TCResult TCError FlowSet Extends
NumberCLJS IntegerCLJS ObjectCLJS StringCLJS ArrayCLJS
- BooleanCLJS)
+ BooleanCLJS AssocType)
(clojure.core.typed.filter_rep NoFilter TopFilter BotFilter TypeFilter NotTypeFilter
ImpFilter AndFilter OrFilter FilterSet)
(clojure.core.typed.object_rep NoObject EmptyObject Path)
@@ -187,6 +187,15 @@
(doall (map type-rec extends))
:without (doall (mapv type-rec without)))))
+(add-default-fold-case AssocType
+ (fn [{:keys [target entries dentries] :as ty} _]
+ (-> ty
+ (update-in [:target] type-rec)
+ (update-in [:entries] (fn [es]
+ (doall
+ (for [[k v] es]
+ [(type-rec k) (type-rec v)]))))
+ (update-in [:dentries] #(when % (type-rec %))))))
(def ret-first (fn [a & rest] a))
View
7 src/main/clojure/clojure/core/typed/frees.clj
@@ -13,7 +13,7 @@
PrimitiveArray DataType Protocol TypeFn Poly PolyDots
Mu HeterogeneousVector HeterogeneousList HeterogeneousMap
CountRange Name Value Top TopFunction B F Result AnyValue
- HeterogeneousSeq Scope TCError Extends)
+ HeterogeneousSeq Scope TCError Extends AssocType)
(clojure.core.typed.filter_rep FilterSet TypeFilter NotTypeFilter ImpFilter
AndFilter OrFilter TopFilter BotFilter)
(clojure.core.typed.object_rep Path EmptyObject NoObject)
@@ -258,6 +258,11 @@
[{:keys [extends without]}]
(apply combine-frees (mapv frees (concat extends without))))
+(add-frees-method [::any-var AssocType]
+ [{:keys [target entries]}]
+ (apply combine-frees (frees target)
+ (mapv frees (apply concat entries))))
+
(add-frees-method [::any-var NotType]
[{:keys [type]}]
(frees type))
View
54 src/main/clojure/clojure/core/typed/parse_unparse.clj
@@ -21,7 +21,8 @@
Mu HeterogeneousVector HeterogeneousList HeterogeneousMap
CountRange Name Value Top TopFunction B F Result AnyValue
HeterogeneousSeq KwArgsSeq TCError Extends NumberCLJS BooleanCLJS
- IntegerCLJS ArrayCLJS JSNominal StringCLJS TCResult)
+ IntegerCLJS ArrayCLJS JSNominal StringCLJS TCResult AssocType
+ GetType)
(clojure.core.typed.filter_rep TopFilter BotFilter TypeFilter NotTypeFilter AndFilter OrFilter
ImpFilter)
(clojure.core.typed.object_rep NoObject EmptyObject Path)
@@ -33,7 +34,7 @@
(defonce ^:dynamic *parse-type-in-ns* nil)
(set-validator! #'*parse-type-in-ns* (some-fn nil? symbol?))
-(declare unparse-type unparse-filter)
+(declare unparse-type unparse-filter unparse-filter-set)
; Types print by unparsing them
(do (defmethod print-method clojure.core.typed.impl_protocols.TCType [s writer]
@@ -49,7 +50,9 @@
(prefer-method print-method clojure.core.typed.impl_protocols.TCAnyType clojure.lang.IPersistentMap)
(defmethod print-method clojure.core.typed.impl_protocols.IFilter [s writer]
- (print-method (unparse-filter s) writer))
+ (if (f/FilterSet? s)
+ (print-method (unparse-filter-set s) writer)
+ (print-method (unparse-filter s) writer)))
(prefer-method print-method clojure.core.typed.impl_protocols.IFilter clojure.lang.IRecord)
(prefer-method print-method clojure.core.typed.impl_protocols.IFilter java.util.Map)
(prefer-method print-method clojure.core.typed.impl_protocols.IFilter clojure.lang.IPersistentMap))
@@ -163,13 +166,35 @@
(defmethod parse-type-list 'Not
[[_ tsyn :as all]]
(when-not (= (count all) 2)
- (u/int-error "Wrong arguments to Not (expected 1)"))
+ (u/int-error (str "Wrong arguments to Not (expected 1): " all)))
(r/NotType-maker (parse-type tsyn)))
(defmethod parse-type-list 'Rec
[syn]
(parse-rec-type syn))
+(defmethod parse-type-list 'Assoc
+ [[_ tsyn & entries :as all]]
+ (when-not (and (<= 1 (count (next all)))
+ (even? (count entries)))
+ (u/int-error (str "Wrong arguments to Assoc: " all)))
+ (r/AssocType-maker (parse-type tsyn)
+ (doall (->> entries
+ (map parse-type)
+ (partition 2)
+ (map vec)))
+ nil))
+
+(defmethod parse-type-list 'Get
+ [[_ tsyn keysyn & not-foundsyn :as all]]
+ (when-not (#{2 3} (count (next all)))
+ (u/int-error (str "Wrong arguments to Get: " all)))
+ (r/-get (parse-type tsyn)
+ (parse-type keysyn)
+ :not-found
+ (when (#{3} (count (next all)))
+ (parse-type not-foundsyn))))
+
;dispatch on last element of syntax in binder
(defmulti parse-all-type (fn [bnds type] (last bnds)))
@@ -691,6 +716,12 @@
[[_ & fsyns]]
(apply fl/-and (mapv parse-filter fsyns)))
+(defmethod parse-filter* 'when
+ [[_ & [a c :as args] :as all]]
+ (when-not (#{2} (count args))
+ (u/int-error (str "Wrong number of arguments to when: " all)))
+ (fl/-imp (parse-filter a) (parse-filter c)))
+
(defmulti parse-path-elem #(cond
(symbol? %) %
:else (first %)))
@@ -781,7 +812,7 @@
(let [bnd (dvar/*dotted-scope* drest-bnd)
_ (when-not bnd
(u/int-error (str (pr-str drest-bnd) " is not in scope as a dotted variable")))]
- (r/DottedPretype-maker
+ (r/DottedPretype1-maker
(free-ops/with-frees [bnd] ;with dotted bound in scope as free
(parse-type drest-type))
(:name bnd))))
@@ -1190,6 +1221,19 @@
[v]
(list* 'List* (doall (map unparse-type (:types v)))))
+(defmethod unparse-type* AssocType
+ [{:keys [target entries dentries]}]
+ (assert (not dentries) "dentries for Assoc NYI")
+ (list* 'Assoc (unparse-type target)
+ (doall (map unparse-type (apply concat entries)))))
+
+(defmethod unparse-type* GetType
+ [{:keys [target key not-found]}]
+ (list* 'Get (unparse-type target)
+ (unparse-type key)
+ (when (not= r/-nil not-found)
+ [(unparse-type not-found)])))
+
; CLJS Types
(defmethod unparse-type* NumberCLJS [_] 'number)
View
71 src/main/clojure/clojure/core/typed/subst.clj
@@ -69,24 +69,25 @@
(t/tc-ignore
(derive ::substitute-dots f/fold-rhs-default)
(f/add-fold-case ::substitute-dots
- Function
- (fn [{:keys [dom rng rest drest kws] :as ftype} {{:keys [name sb images rimage]} :locals}]
- (assert (not kws) "TODO substitute keyword args")
- (if (and drest
- (= name (:name drest)))
- (r/Function-maker (concat (map sb dom)
- ;; We need to recur first, just to expand out any dotted usages of this.
- (let [expanded (sb (:pre-type drest))]
- ;(prn "expanded" (unparse-type expanded))
- (map (fn [img] (substitute img name expanded)) images)))
- (sb rng)
- rimage nil nil)
- (r/Function-maker (map sb dom)
- (sb rng)
- (and rest (sb rest))
- (and drest (r/DottedPretype-maker (sb (:pre-type drest))
- (:name drest)))
- nil))))
+ Function
+ (fn [{:keys [dom rng rest drest kws] :as ftype} {{:keys [name sb images rimage]} :locals}]
+ (assert (not kws) "TODO substitute keyword args")
+ (if (and drest
+ (= name (:name drest)))
+ (r/Function-maker (doall
+ (concat (map sb dom)
+ ;; We need to recur first, just to expand out any dotted usages of this.
+ (let [expanded (sb (:pre-type drest))]
+ ;(prn "expanded" (unparse-type expanded))
+ (map (fn [img] (substitute img name expanded)) images))))
+ (sb rng)
+ rimage nil nil)
+ (r/Function-maker (doall (map sb dom))
+ (sb rng)
+ (and rest (sb rest))
+ (and drest (r/DottedPretype1-maker (sb (:pre-type drest))
+ (:name drest)))
+ nil))))
(f/add-fold-case ::substitute-dots
HeterogeneousVector
@@ -135,25 +136,25 @@
(t/tc-ignore
(derive ::substitute-dotted f/fold-rhs-default)
(f/add-fold-case ::substitute-dotted
- F
- (fn [{name* :name :as t} {{:keys [name image]} :locals}]
- (if (= name* name)
- image
- t)))
+ F
+ (fn [{name* :name :as t} {{:keys [name image]} :locals}]
+ (if (= name* name)
+ image
+ t)))
(f/add-fold-case ::substitute-dotted
- Function
- (fn [{:keys [dom rng rest drest kws]} {{:keys [sb name image]} :locals}]
- (assert (not kws))
- (r/Function-maker (map sb dom)
- (sb rng)
- (and rest (sb rest))
- (and drest
- (r/DottedPretype-maker (substitute image (:name drest) (sb (:pretype drest)))
- (if (= name (:name drest))
- name
- (:name drest))))
- nil)))
+ Function
+ (fn [{:keys [dom rng rest drest kws]} {{:keys [sb name image]} :locals}]
+ (assert (not kws))
+ (r/Function-maker (doall (map sb dom))
+ (sb rng)
+ (and rest (sb rest))
+ (and drest
+ (r/DottedPretype1-maker (substitute image (:name drest) (sb (:pretype drest)))
+ (if (= name (:name drest))
+ name
+ (:name drest))))
+ nil)))
(f/add-fold-case ::substitute-dotted
HeterogeneousVector
View
153 src/main/clojure/clojure/core/typed/subtype.clj
@@ -16,7 +16,7 @@
[clojure.set :as set]
[clojure.repl :as repl])
(:import (clojure.core.typed.type_rep Poly TApp Union Intersection Value Function
- Result Protocol TypeFn Name F Bounds HeterogeneousVector
+ Result Protocol TypeFn Name F Bounds
PrimitiveArray DataType RClass HeterogeneousMap
HeterogeneousList HeterogeneousSeq CountRange KwArgs
Extends)
@@ -144,9 +144,13 @@
(r/Poly? t)
(= (.nbound ^Poly s) (.nbound ^Poly t)))
(let [names (repeatedly (.nbound ^Poly s) gensym)
+ bbnds1 (c/Poly-bbnds* names s)
+ bbnds2 (c/Poly-bbnds* names t)
b1 (c/Poly-body* names s)
b2 (c/Poly-body* names t)]
- (if (subtype? b1 b2)
+ (if (and (= bbnds1 bbnds2)
+ (free-ops/with-bounded-frees (zipmap (map r/F-maker names) bbnds1)
+ (subtype? b1 b2)))
*sub-current-seen*
(fail! s t)))
@@ -251,17 +255,17 @@
(r/Extends? t))
(if (and ;all positive information matches.
; Each t should occur in at least one s.
- (every? (fn [t*]
+ (every? (fn extends-t [t*]
(some #(subtype? % t*) (:extends s)))
(:extends t))
;lhs does not explicitly implement any forbidden types.
; No negative t should be a supertype of a positive s
- (not-any? (fn [not-t*]
+ (not-any? (fn extends-not-t [not-t*]
(some #(subtype? % not-t*) (:extends s)))
(:without t))
;lhs explicitly disallows same types as rhs
; Each negative t should be a supertype of some negative s
- (every? (fn [not-t*]
+ (every? (fn extends-without-t[not-t*]
(some #(subtype? % not-t*) (:without s)))
(:without t)))
*sub-current-seen*
@@ -312,6 +316,44 @@
*sub-current-seen*
(fail! s t))
+ (and (r/AssocType? s)
+ (r/AssocType? t)
+ (r/F? (:target s))
+ (r/F? (:target t))
+ (not-any? :dentries [s t]))
+ (if (and (= (:target s) (:target t))
+ (subtype? (apply c/assoc-pairs-noret (c/-complete-hmap {}) (:entries s))
+ (apply c/assoc-pairs-noret (c/-complete-hmap {}) (:entries t))))
+ *sub-current-seen*
+ (fail! s t))
+
+ (and (r/AssocType? s)
+ (r/F? (:target s))
+ (not (r/AssocType? t)))
+ (let [bnds (free-ops/free-with-name-bnds (-> s :target :name))
+ _ (assert bnds
+ (str "Bounds not found for free variable: " (-> s :target :name)
+ free-ops/*free-scope*))]
+ (if (and (subtype? (:upper-bound bnds) t)
+ (subtype? (apply c/assoc-pairs-noret (c/-complete-hmap {}) (:entries s))
+ t))
+ *sub-current-seen*
+ (fail! s t)))
+
+ ; avoids infinite expansion because associng an F is a fixed point
+ (and (r/AssocType? s)
+ (not (r/F? (:target s))))
+ (if (subtype? (apply c/assoc-pairs-noret (:target s) (:entries s)) t)
+ *sub-current-seen*
+ (fail! s t))
+
+ ; avoids infinite expansion because associng an F is a fixed point
+ (and (r/AssocType? t)
+ (not (r/F? (:target t))))
+ (if (subtype? s (apply c/assoc-pairs-noret (:target t) (:entries t)))
+ *sub-current-seen*
+ (fail! s t))
+
(and (r/HeterogeneousVector? s)
(r/HeterogeneousVector? t))
(if (and (cond
@@ -356,7 +398,7 @@
(r/HeterogeneousList? t))
(if (= (count (:types s))
(count (:types t)))
- (or (last (doall (map subtype (:types s) (:types t))))
+ (or (last (map subtype (:types s) (:types t)))
#{})
(fail! s t))
@@ -364,54 +406,56 @@
(r/HeterogeneousSeq? t))
(if (= (count (:types s))
(count (:types t)))
- (or (last (doall (map #(subtype %1 %2) (:types s) (:types t))))
+ (or (last (map subtype (:types s) (:types t)))
#{})
(fail! s t))
- ;every rtype entry must be in ltypes
- ;eg. {:a 1, :b 2, :c 3} <: {:a 1, :b 2}
- (and (r/HeterogeneousMap? s)
- (r/HeterogeneousMap? t))
- (let [; convention: prefix things on left with l, right with r
- {ltypes :types labsent :absent-keys :as s} s
- {rtypes :types rabsent :absent-keys :as t} t]
- (if (and ; if t is complete, s must be complete with the same keys
- (if (c/complete-hmap? t)
- (if (c/complete-hmap? s)
- (= (set (keys ltypes)) (set (keys rtypes)))
- false)
- true)
- ; all absent keys in t should be absent in s
- (every? identity
- (for [rabsent-key rabsent]
- ; Subtyping is good if rabsent-key is:
- ; 1. Absent in s
- ; 2. Not present in s, but s is complete
- (or ((set labsent) rabsent-key)
- (when (c/complete-hmap? s)
- (not ((set (keys ltypes)) rabsent-key))))))
- ; all present keys in t should be present in s
- (every? identity
- (map (fn [[k v]]
- (when-let [t (get ltypes k)]
- (subtype? t v)))
- rtypes)))
- *sub-current-seen*
- (fail! s t)))
+ ;every rtype entry must be in ltypes
+ ;eg. {:a 1, :b 2, :c 3} <: {:a 1, :b 2}
+ (and (r/HeterogeneousMap? s)
+ (r/HeterogeneousMap? t))
+ (let [; convention: prefix things on left with l, right with r
+ {ltypes :types labsent :absent-keys :as s} s
+ {rtypes :types rabsent :absent-keys :as t} t]
+ (if (and ; if t is complete, s must be complete with the same keys
+ (if (c/complete-hmap? t)
+ (if (c/complete-hmap? s)
+ (= (set (keys ltypes)) (set (keys rtypes)))
+ false)
+ true)
+ ; all absent keys in t should be absent in s
+ (every? identity
+ (for [rabsent-key rabsent]
+ ; Subtyping is good if rabsent-key is:
+ ; 1. Absent in s
+ ; 2. Not present in s, but s is complete
+ (or ((set labsent) rabsent-key)
+ (when (c/complete-hmap? s)
+ (not ((set (keys ltypes)) rabsent-key))))))
+ ; all present keys in t should be present in s
+ (every? identity
+ (map (fn [[k v]]
+ (when-let [t (get ltypes k)]
+ (subtype? t v)))
+ rtypes)))
+ *sub-current-seen*
+ (fail! s t)))
(r/HeterogeneousMap? s)
(let [^HeterogeneousMap s s]
; Partial HMaps do not record absence of fields, only subtype to (APersistentMap Any Any)
(if (c/complete-hmap? s)
- (subtype (impl/impl-case
- :clojure (c/RClass-of APersistentMap [(apply c/Un (keys (.types s)))
- (apply c/Un (vals (.types s)))])
- :cljs (c/Protocol-of 'cljs.core/IMap [(apply c/Un (keys (.types s)))
- (apply c/Un (vals (.types s)))]))
+ (subtype (c/In (impl/impl-case
+ :clojure (c/RClass-of APersistentMap [(apply c/Un (keys (.types s)))
+ (apply c/Un (vals (.types s)))])
+ :cljs (c/Protocol-of 'cljs.core/IMap [(apply c/Un (keys (.types s)))
+ (apply c/Un (vals (.types s)))]))
+ (r/make-ExactCountRange (count (:types s))))
t)
- (subtype (impl/impl-case
- :clojure (c/RClass-of APersistentMap [r/-any r/-any])
- :cljs (c/Protocol-of 'cljs.core/IMap [r/-any r/-any]))
+ (subtype (c/In (impl/impl-case
+ :clojure (c/RClass-of APersistentMap [r/-any r/-any])
+ :cljs (c/Protocol-of 'cljs.core/IMap [r/-any r/-any]))
+ (r/make-CountRange (count (:types s))))
t)))
(r/KwArgsSeq? s)
@@ -457,7 +501,7 @@
(let [{var1 :the-var variances* :variances poly1 :poly?} s
{var2 :the-var poly2 :poly?} t]
(if (and (= var1 var2)
- (every? (fn [[v l r]]
+ (every? (fn prcol-variance [[v l r]]
(case v
:covariant (subtypeA* *sub-current-seen* l r)
:contravariant (subtypeA* *sub-current-seen* r l)
@@ -746,6 +790,20 @@
(update-in [:then] fully-resolve-filter)
(update-in [:else] fully-resolve-filter)))
+(defn subtype-type-filter? [s t]
+ {:pre [(fr/TypeFilter? s)
+ (fr/TypeFilter? t)]}
+ (and (= (:path s) (:path t))
+ (= (:id s) (:id t))
+ (subtype? (:type s) (:type t))))
+
+(defn subtype-not-type-filter? [s t]
+ {:pre [(fr/NotTypeFilter? s)
+ (fr/NotTypeFilter? t)]}
+ (and (= (:path s) (:path t))
+ (= (:id s) (:id t))
+ (subtype? (:type t) (:type s))))
+
(defn subtype-Result
[{t1 :t ^FilterSet f1 :fl o1 :o flow1 :flow :as s}
{t2 :t ^FilterSet f2 :fl o2 :o flow2 :flow :as t}]
@@ -779,7 +837,8 @@
(every? fops/atomic-filter? (:fs (:then f1)))
(= 1 (count (filter fr/TypeFilter? (:fs (:then f1)))))
(= fr/-top (:else f2))
- (= flow1 flow2 (r/-flow fr/-top)))
+ (= flow1 flow2 (r/-flow fr/-top))
+ (= o1 o2))
(let [f1-tf (first (filter fr/TypeFilter? (:fs (:then f1))))]
(if (= f1-tf (:then f2))
(subtype t1 t2)
View
6 src/main/clojure/clojure/core/typed/type_ctors.clj
@@ -84,6 +84,12 @@
(defn -complete-hmap [types]
(-hmap types false))
+(t/ann -partial-hmap (Fn [(Seqable r/Type) -> r/Type]
+ [(Seqable r/Type) (IPersistentSet r/Type) -> r/Type]))
+(defn -partial-hmap
+ ([types] (-partial-hmap types #{}))
+ ([types absent-keys] (-hmap types absent-keys true)))
+
(t/def-alias TypeMap
"A regular map with types as keys and vals."
(IPersistentMap r/Type r/Type))
View
58 src/main/clojure/clojure/core/typed/type_rep.clj
@@ -495,6 +495,64 @@
:methods
[p/TCType])
+;; Heterogeneous ops
+
+(declare DottedPretype?)
+
+(u/ann-record AssocType [target :- Type,
+ entries :- (t/Coll '[Type Type])
+ dentries :- (U nil DottedPretype)])
+(u/def-type AssocType [target entries dentries]
+ "An assoc[iate] operation on the type level"
+ [(Type? target)
+ (or (DottedPretype? dentries)
+ (nil? dentries))
+ (and (every? (u/hvector-c? Type? Type?) entries)
+ (sequential? entries))
+ (not (and entries dentries))]
+ :methods
+ [p/TCType])
+
+(u/ann-record DissocType [target :- Type,
+ keys :- (t/Coll Type)
+ dkeys :- (U nil DottedPretype)])
+(u/def-type DissocType [target keys dkeys]
+ "A dissoc[iate] operation on the type level"
+ [(Type? target)
+ (or (DottedPretype? dkeys)
+ (nil? dkeys))
+ (and (every? Type? keys)
+ (sequential? keys))
+ (not (and keys dkeys))]
+ :methods
+ [p/TCType])
+
+(u/ann-record GetType [target :- Type,
+ key :- Type
+ not-found :- Type
+ target-fs :- p/IFilterSet
+ target-object :- p/IRObject])
+(u/def-type GetType [target key not-found target-fs target-object]
+ "get on the type level"
+ [(Type? target)
+ (Type? key)
+ (Type? not-found)
+ (p/IFilterSet? target-fs)
+ (p/IRObject? target-object)]
+ :methods
+ [p/TCType])
+
+(t/ann ^:no-check -get
+ [Type Type & :optional {:not-found (U nil Type)
+ :target-fs (U nil p/IFilterSet)
+ :target-object (U nil p/IRObject)}
+ -> GetType])
+(defn -get
+ [target key & {:keys [not-found target-fs target-object]}]
+ (GetType-maker target key (or not-found -nil)
+ (or target-fs ((-FS-var) @(-top-var) @(-top-var)))
+ (or target-object @(-empty-var))))
+
(u/ann-record DottedPretype [pre-type :- Type,
name :- (U Symbol Number)
partition-count :- Number])
View
26 src/test/clojure/clojure/core/typed/test/core.clj
@@ -1,13 +1,10 @@
(ns clojure.core.typed.test.core
- (:import (clojure.lang ISeq ASeq IPersistentVector Atom IPersistentMap
- Keyword ExceptionInfo Symbol Var))
(:require [clojure.test :refer :all]
[clojure.tools.analyzer :refer [ast analyze-form]]
[clojure.tools.analyzer.hygienic :refer [ast-hy]]
[clojure.repl :refer [pst]]
[clojure.pprint :refer [pprint]]
[clojure.data :refer [diff]]
- [clojure.core.typed :as tc, :refer :all]
[clojure.core.typed.init]
[clojure.core.typed.utils :as u :refer [with-ex-info-handlers top-level-error?]]
[clojure.core.typed.current-impl :as impl]
@@ -34,10 +31,7 @@
[clojure.core.typed.test.rbt]
[clojure.core.typed.test.person]
[clojure.tools.trace :refer [trace-vars untrace-vars
- trace-ns untrace-ns]]))
-
-(load-if-needed)
-
+ trace-ns untrace-ns]])
; we want clojure.lang.Seqable to be scoped here.
; There :refer :all of clojure.core.typed adds another Seqable which
; is less useful here.
@@ -2372,6 +2366,24 @@
1 [1 2 3])
Number))
+(deftest Assoc-test
+ (is-cf {:a 1} (Assoc '{} ':a Number))
+ (is-cf {:a 1} (Assoc (U '{:a Number} '{:a Double}) ':a Long))
+ (is-cf (fn [a] (assoc a 1 2))
+ (All [[x :> (clojure.core.typed/Map Nothing Nothing) :< (clojure.core.typed/Map Number Number)]]
+ [x -> (clojure.core.typed/Map Number Number)]))
+ (is-cf (fn [a] (assoc a :a 1))
+ (All [[x :> (clojure.core.typed/Map Nothing Nothing) :< (clojure.core.typed/Map Any Any)]]
+ [x -> (Assoc x ':a Number)]))
+ (is-cf (let [f (clojure.core.typed/ann-form
+ (fn [a] (assoc a :a 1))
+ (All [[x :< (clojure.core.typed/Map Any Any)]]
+ [x -> (Assoc x ':a Number)]))]
+ (clojure.core.typed/ann-form
+ (f {:b 1})
+ '{:b Number :a Number})))
+ (is-cf (fn [a] (assoc a :a 1))
+ (All [[x :< (clojure.core.typed/Map Any Any)]] [x -> (Assoc x ':a Number)])))
(deftest hvec-ops
(is-cf (first [1 'a]) Number)

0 comments on commit 0c97ef8

Please sign in to comment.
Something went wrong with that request. Please try again.