Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Browse files

Fix datatypes annotating their constructor fns

  • Loading branch information...
commit fe99e6a1f554cc56bad2d00735cbfab52deba0f8 1 parent daac268
@frenchy64 authored
View
7 README.md
@@ -20,8 +20,13 @@ Leiningen (Clojars):
0.1.2-SNAPSHOT
- Fix objects and filters being lost during polymorphic and dotted function applications
- - Add tests for (if (seq a) (first a) 0) filter example.
+ - Add tests for (if (seq a) (first a) 0) filter example.
- Can annotate datatypes outside current namespace
+ - Improve type of `seq`, `next`, `conj`
+ - tc-pr-env -> print-env
+ - tc-pr-filters -> print-filterset
+ - Alter APersistentMap
+ - Check that local binding occurrences match with expected types
0.1.1
View
100 src/typed/core.clj
@@ -64,11 +64,11 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Special functions
-(defn tc-pr-env
+(defn print-env
"Print the current type environment, and debug-string"
[debug-string] nil)
-(defn tc-pr-filters
+(defn print-filterset
"Print the filter set attached to form, and debug-string"
[debug-string frm]
frm)
@@ -1916,7 +1916,7 @@
(defmethod unparse-filter* TypeFilter
[{:keys [type path id]}]
(concat (list 'is (unparse-type type) id)
- (when path
+ (when (seq path)
[(map unparse-path-elem path)])))
(defmethod unparse-filter* NotTypeFilter
@@ -2162,19 +2162,25 @@
[n (parse-type t)])
(defn gen-datatype* [provided-name fields variances args ancests]
- `(let [provided-name# '~provided-name
- local-name# (if (namespace provided-name#)
- (symbol (apply str (last (partition-by #(= \. %) (str provided-name#)))))
- provided-name#)
- s# (if (namespace provided-name#)
- provided-name#
- (symbol (str (munge (-> *ns* ns-name)) \. local-name#)))
+ `(let [provided-name-str# (str '~provided-name)
+ _# (prn "provided-name-str" provided-name-str#)
+ munged-ns-str# (if (some #(= \. %) provided-name-str#)
+ (apply str (butlast (apply concat (butlast (partition-by #(= \. %) provided-name-str#)))))
+ (str (munge (-> *ns* ns-name))))
+ _# (prn "munged-ns-str" munged-ns-str#)
+ demunged-ns-str# (str (clojure.repl/demunge munged-ns-str#))
+ _# (prn "demunged-ns-str" demunged-ns-str#)
+ local-name# (if (some #(= \. %) provided-name-str#)
+ (symbol (apply str (last (partition-by #(= \. %) (str provided-name-str#)))))
+ provided-name-str#)
+ _# (prn "local-name" local-name#)
+ s# (symbol (str munged-ns-str# \. local-name#))
fs# (apply array-map (apply concat (with-frees (mapv make-F '~args)
(mapv parse-field '~fields))))
as# (set (with-frees (mapv make-F '~args)
(mapv parse-type '~ancests)))
_# (add-datatype-ancestors s# as#)
- pos-ctor-name# (symbol (str (-> *ns* ns-name)) (str "->" local-name#))
+ pos-ctor-name# (symbol demunged-ns-str# (str "->" local-name#))
args# '~args
vs# '~variances
dt# (if args#
@@ -6179,6 +6185,7 @@
(alter-class APersistentMap [[a :variance :covariant] [b :variance :covariant]]
:replace
{IPersistentCollection (IPersistentCollection (IMapEntry a b))
+ IPersistentMap (IPersistentMap a b)
Seqable (Seqable (IMapEntry a b))
IFn (All [d]
(Fn [Any -> (U nil b)]
@@ -6505,7 +6512,7 @@
(ann clojure.core/class [Any -> (Option Class) :object {:id 0 :path [Class]}])
(ann clojure.core/seq (All [x]
- [(Option (Seqable x)) -> (Option (ISeq x))
+ [(Option (Seqable x)) -> (Option (I (ISeq x) (CountRange 1)))
:filters {:then (is (CountRange 1) 0)
:else (| (is nil 0)
(is (ExactCount 0) 0))}]))
@@ -6585,7 +6592,7 @@
(ann clojure.core/next
(All [x]
- [(Option (Seqable x)) -> (U nil (ISeq x))
+ [(Option (Seqable x)) -> (Option (I (ISeq x) (CountRange 1)))
:filters {:then (& (is (CountRange 2) 0)
(! nil 0))
:else (| (is (CountRange 0 1) 0)
@@ -6594,6 +6601,9 @@
(ann clojure.core/conj
(All [x y]
(Fn [(IPersistentVector x) x x * -> (IPersistentVector x)]
+ [(APersistentMap x y)
+ (U nil (IMapEntry x y) (Vector* x y))
+ (U nil (IMapEntry x y) (Vector* x y)) * -> (APersistentMap x y)]
[(IPersistentMap x y)
(U nil (IMapEntry x y) (Vector* x y))
(U nil (IMapEntry x y) (Vector* x y)) * -> (IPersistentMap x y)]
@@ -6708,10 +6718,12 @@
(let [t (unparse-type (ret-t r))
fs (unparse-filter-set (ret-f r))
o (unparse-object (ret-o r))]
- (if (and (= (-FS -top -top) fs)
- (= o -empty))
+ (if (and (= (-FS -top -top) (ret-f r))
+ (= (ret-o r) -empty))
t
- [t fs o])))
+ (if (= (ret-o r) -empty)
+ [t fs]
+ [t fs o]))))
(defn ret
"Convenience function for returning the type of an expression"
@@ -7726,7 +7738,7 @@
(declare check-anon-fn)
;debug printing
-(defmethod invoke-special #'tc-pr-env
+(defmethod invoke-special #'print-env
[{[debug-string] :args :as expr} & [expected]]
(assert (= :string (:op debug-string)))
;DO NOT REMOVE
@@ -7737,15 +7749,15 @@
expr-type (ret -nil -false-filter -empty)))
;filter printing
-(defmethod invoke-special #'tc-pr-filters
+(defmethod invoke-special #'print-filterset
[{[debug-string form] :args :as expr} & [expected]]
- (assert (and debug-string form) "Wrong arguments to tc-pr-filters")
+ (assert (and debug-string form) "Wrong arguments to print-filterset")
(let [cform (check form expected)
t (expr-type cform)]
(assert (= :string (:op debug-string)))
;DO NOT REMOVE
(prn (:val debug-string))
- (prn (:fl t))
+ ;(prn (:fl t))
(if (FilterSet? (:fl t))
(do (pprint (unparse-filter-set (:fl t)))
(flush))
@@ -8597,15 +8609,19 @@
(defmethod check :local-binding-expr
[{:keys [local-binding] :as expr} & [expected]]
- (let [sym (:sym local-binding)]
+ (let [sym (:sym local-binding)
+ t (type-of sym)
+ _ (assert (or (not expected)
+ (subtype? t (ret-t expected)))
+ (error-msg "Local binding " sym " expected type " (unparse-type (ret-t expected))
+ ", but actual type " (unparse-type t)))]
(assoc expr
- expr-type (let [t (type-of sym)]
- (ret t
- (-FS (if (subtype? t (Un -false -nil))
- -bot
- (-not-filter (Un -nil -false) sym))
- (-filter (Un -nil -false) sym))
- (->Path nil sym))))))
+ expr-type (ret t
+ (-FS (if (subtype? t (Un -false -nil))
+ -bot
+ (-not-filter (Un -nil -false) sym))
+ (-filter (Un -nil -false) sym))
+ (->Path nil sym)))))
(declare Method-symbol->Type)
@@ -9148,7 +9164,7 @@
;; and the resulting type should be the empty type
:else (do (prn (error-msg "Not checking unreachable code"))
(ret (Un)))))]
- (let [{fs+ :then fs- :else :as f1} (:fl tst)
+ (let [{fs+ :then fs- :else :as f1} (ret-f tst)
; _ (prn "check-if: fs+" (unparse-filter fs+))
; _ (prn "check-if: fs-" (unparse-filter fs-))
flag+ (atom true)
@@ -9346,10 +9362,9 @@
{:keys [dom rng] :as expected-fn} (-> expected-fin :types first)
_ (assert (not (:rest expected-fn)))
cbody (with-locals (zipmap (map :sym required-params) dom)
- #_(print-env)
- (check body (ret (:t rng)
- (:fl rng)
- (:o rng))))]
+ (check body (ret (Result-type* rng)
+ (Result-filter* rng)
+ (Result-object* rng))))]
(assoc expr
expr-type (expr-type cbody))))
@@ -9367,15 +9382,16 @@
etype (expr-type cthe-expr)
ctests (mapv check (:tests expr))
cdefault (check (:default expr))
- cthens-and-envs (for [[tst-ret thn] (map vector (map expr-type ctests) (:thens expr))]
- (let [{{fs+ :then} :fl :as rslt} (tc-equiv := etype tst-ret)
- flag+ (atom true)
- env-thn (env+ *lexical-env* [fs+] flag+)
- then-ret (with-lexical-env env-thn
- (check thn))]
- [(assoc thn
- expr-type (expr-type then-ret))
- env-thn]))
+ cthens-and-envs (doall
+ (for [[tst-ret thn] (map vector (map expr-type ctests) (:thens expr))]
+ (let [{{fs+ :then} :fl :as rslt} (tc-equiv := etype tst-ret)
+ flag+ (atom true)
+ env-thn (env+ *lexical-env* [fs+] flag+)
+ then-ret (with-lexical-env env-thn
+ (check thn))]
+ [(assoc thn
+ expr-type (expr-type then-ret))
+ env-thn])))
;TODO consider tests that failed to refine env
cdefault (check (:default expr))
case-result (let [type (apply Un (map (comp :t expr-type) (cons cdefault (map first cthens-and-envs))))
View
2  test/typed/test/array.clj
@@ -1,6 +1,6 @@
(ns typed.test.pomegranate
(:import (clojure.lang DynamicClassLoader Named Seqable IPersistentVector))
- (:require [typed.core :refer [ann check-ns override-method tc-pr-env ann-protocol
+ (:require [typed.core :refer [ann check-ns override-method ann-protocol
tc-ignore non-nil-return nilable-param]]
[clojure.repl :refer [pst]]))
View
7 test/typed/test/ckanren.clj
@@ -5,8 +5,9 @@
[typed.core :refer [ann def-alias declare-protocols ann-protocol
ann-pprotocol declare-datatypes
ann-form
- tc-ignore check-ns ann-datatype tc-pr-env cf
- parse-type ann-pdatatype fn> AnyInteger]]
+ tc-ignore check-ns ann-datatype cf
+ parse-type ann-pdatatype fn> AnyInteger
+ print-env]]
[clojure.repl :refer [pst]]
[analyze.core :refer [ast]])
(:import [java.io Writer]
@@ -490,7 +491,7 @@
(refinable? [_] true)
IRefine
(refine [this other]
- (tc-pr-env "refine:")
+ (print-env "refine:")
(intersection this other))
IFiniteDomain
(domain? [_] true)
View
4 test/typed/test/conduit.clj
@@ -1,7 +1,7 @@
(ns typed.test.conduit
(:import (clojure.lang Seqable IMeta IPersistentMap LazySeq ISeq))
(:require [typed.core :refer [check-ns ann fn> def-alias tc-ignore ann-form declare-names inst
- tc-pr-env inst-ctor cf Option declare-alias-kind AnyInteger]]
+ print-env inst-ctor cf Option declare-alias-kind AnyInteger]]
[clojure.repl :refer [pst]]
[arrows.core :refer [defarrow]]))
@@ -96,7 +96,7 @@
(nil? f) [nil abort-c] ;added - Ambrose
:else
(let [[new-f new-c] (f (nth xs n))
- _ (tc-pr-env "after new-f")
+ _ (print-env "after new-f")
next-c (ann-form
(fn [c]
(if (nil? c)
View
28 test/typed/test/core.clj
@@ -527,7 +527,7 @@
mapr)
maprl (clojure.core/get mapr :left)
- ;_ (tc-pr-env "maprl")
+ ;_ (print-env "maprl")
maprl
(if (clojure.core/seq? maprl)
(clojure.core/apply clojure.core/hash-map maprl)
@@ -599,11 +599,11 @@
(-FS -top -bot) -empty)))
; using filters derived by =
(is (= (tc-t (typed.core/fn> [[tmap :- typed.test.core/UnionName]]
- (if (typed.core/tc-pr-filters "the test"
+ (if (typed.core/print-env "the test"
(= :MapStruct1 (:type tmap)))
- (do (typed.core/tc-pr-env "follow then")
+ (do (typed.core/print-filterset "follow then")
(:a tmap))
- (do (typed.core/tc-pr-env "follow else")
+ (do (typed.core/print-env "follow else")
(:b tmap)))))
(ret (make-FnIntersection (->Function [(->Name 'typed.test.core/UnionName)]
(let [t (->Name 'typed.test.core/MyName)
@@ -616,20 +616,20 @@
(is (= (tc-t (typed.core/fn> [[tmap :- typed.test.core/UnionName]]
; (and (= :MapStruct1 (-> tmap :type))
; (= 1 1))
- (if (typed.core/tc-pr-filters "final filters"
- (let [and1 (typed.core/tc-pr-filters "first and1"
+ (if (typed.core/print-filterset "final filters"
+ (let [and1 (typed.core/print-filterset "first and1"
(= :MapStruct1 (-> tmap :type)))]
- (typed.core/tc-pr-env "first conjunct")
- (typed.core/tc-pr-filters "second and1"
- (if (typed.core/tc-pr-filters "second test"
+ (typed.core/print-env "first conjunct")
+ (typed.core/print-filterset "second and1"
+ (if (typed.core/print-filterset "second test"
and1)
- (do (typed.core/tc-pr-env "second conjunct")
- (typed.core/tc-pr-filters "third and1"
+ (do (typed.core/print-env "second conjunct")
+ (typed.core/print-filterset "third and1"
(= 1 1)))
- (do (typed.core/tc-pr-env "fail conjunct")
- (typed.core/tc-pr-filters "fail and1"
+ (do (typed.core/print-env "fail conjunct")
+ (typed.core/print-filterset "fail and1"
and1))))))
- (do (typed.core/tc-pr-env "follow then")
+ (do (typed.core/print-env "follow then")
(assoc tmap :c :d))
1)))
(ret (make-FnIntersection (->Function [(->Name 'typed.test.core/UnionName)]
View
2  test/typed/test/core_logic.clj
@@ -9,7 +9,7 @@
[typed.core :refer [ann-protocol ann tc-ignore def-alias
declare-protocols declare-datatypes
ann-datatype loop> check-ns non-nil-return
- tc-pr-env cf]]
+ cf]]
[analyze.core :refer [ast]]))
(ann *occurs-check* (U true false))
View
2  test/typed/test/monads.clj
@@ -26,7 +26,7 @@
:refer (with-symbol-macros defsymbolmacro name-with-attributes)]
[typed.core
:refer (tc-ignore check-ns ann ann-protocol def-alias unsafe-ann-form ann-form inst fn> pfn>
- AnyInteger tc-pr-env cf Option tc-pr-filters)]))
+ AnyInteger print-env cf Option print-filterset)]))
;; Monad Protocols
View
18 test/typed/test/rbt.clj
@@ -1,6 +1,6 @@
(ns typed.test.rbt
(:require [typed.core :refer [ann inst cf fn> pfn> def-alias declare-names
- tc-pr-env tc-pr-filters check-ns]]
+ print-env print-filterset check-ns]]
[clojure.repl :refer [pst]]
[analyze.core :refer [ast]]))
@@ -157,12 +157,12 @@
(Fn [badRight -> rbt]))
(defn restore-right [tmap]
(cond
- (tc-pr-filters "TEST1"
+ (print-filterset "TEST1"
(and (= :Black (-> tmap :tree))
(= :Red (-> tmap :left :tree))
(= :Red (-> tmap :right :tree))
(= :Red (-> tmap :right :left :tree))))
- (let [;_ (tc-pr-env "down first then")
+ (let [;_ (print-env "down first then")
{lt :left rt :right e :entry} tmap
;re-color
res {:tree :Red
@@ -171,10 +171,10 @@
:tree :Black)
:right (assoc rt
:tree :Black)}]
- ;(tc-pr-env "restore-right: output first branch (res)")
+ ;(print-env "restore-right: output first branch (res)")
res)
- (tc-pr-filters "TEST2"
+ (print-filterset "TEST2"
(and (= :Black (-> tmap :tree))
(= :Red (-> tmap :left :tree))
(= :Red (-> tmap :right :tree))
@@ -187,10 +187,10 @@
:tree :Black)
:right (assoc rt
:tree :Black)}]
- (tc-pr-env "restore-right: output second branch (res)")
+ (print-env "restore-right: output second branch (res)")
res)
- (tc-pr-filters "TEST3"
+ (print-filterset "TEST3"
(and (= :Black (-> tmap :tree))
(= :Red (-> tmap :right :tree))
(= :Red (-> tmap :right :left :tree))))
@@ -230,9 +230,9 @@
:right rl}
:right rr})
- (do (tc-pr-env "final else:")
+ (do (print-env "final else:")
:else)
- (do (tc-pr-env "follow final else:")
+ (do (print-env "follow final else:")
tmap)))
; Okasaki's simplified rotations for red-black trees
Please sign in to comment.
Something went wrong with that request. Please try again.