Permalink
Browse files

Occurrence typing for CLJS

  • Loading branch information...
1 parent c44f890 commit 0bd50e6f69d72e480e57173d7c7de5a3ffebeafb @frenchy64 committed Nov 25, 2012
Showing with 70 additions and 31 deletions.
  1. +6 −8 src/typed/check.clj
  2. +47 −11 src/typed/check_cljs.clj
  3. +14 −11 src/typed/core.clj
  4. +3 −1 src/typed/subtype.clj
View
@@ -2477,8 +2477,8 @@
;; in particular, it might be (void)
(and expected reachable?)
(-> (*check-if-checkfn* expr (-> expected
- (update-in [:fl] #(map (constantly (->NoFilter)) %))
- (update-in [:o] #(map (constantly (->NoObject)) %))))
+ (update-in [:fl] (constantly (-FS -top -top)))
+ (update-in [:o] (constantly -empty))))
expr-type)
;; this code is reachable, but we have no expected type
reachable? (-> (*check-if-checkfn* expr) expr-type)
@@ -2487,12 +2487,10 @@
:else (do (prn (error-msg "Not checking unreachable code"))
(ret (Un)))))]
(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)
- flag- (atom true)
- _ (set-validator! flag+ boolean?)
- _ (set-validator! flag- boolean?)
+; _ (prn "check-if: fs+" (unparse-filter fs+))
+; _ (prn "check-if: fs-" (unparse-filter fs-))
+ flag+ (atom true :validator boolean?)
+ flag- (atom true :validator boolean?)
;_ (print-env)
idsym (gensym)
View
@@ -27,7 +27,8 @@
(declare cljs-ann*)
(defmacro cljs-ann [vname tsyn]
- `'~(cljs-ann* vname tsyn))
+ (let [r (cljs-ann* vname tsyn)]
+ `'~r))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Envs
@@ -119,13 +120,13 @@
(defmethod subtype* [Value SymbolCLJS ::clojurescript]
[{:keys [val] :as s} t]
(if (symbol? val)
- *current-env*
+ *sub-current-seen*
(type-error s t)))
(defmethod subtype* [Value BooleanCLJS ::clojurescript]
[{:keys [val] :as s} t]
(if ((some-fn true? false?) val)
- *current-env*
+ *sub-current-seen*
(type-error s t)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
@@ -200,7 +201,7 @@
(let [ann-type (binding [*var-annotations* CLJS-VAR-ENV
*current-env* env]
(type-of vname))
- cinit (check-cljs init expected)
+ cinit (check-cljs init (ret ann-type))
_ (assert (subtype? (-> cinit expr-type ret-t)
ann-type)
(str "Var definition did not match annotation."
@@ -222,15 +223,24 @@
(defmethod invoke-cljs-special :default [& _] ::not-special)
+; copied from Clojure impl
+(defmethod invoke-cljs-special 'typed.internal/print-env
+ [{[{debug-string :form :as texpr} :as args] :args :as expr} & [expected]]
+ (assert (= 1 (count args)))
+ (assert (string? debug-string))
+ ;DO NOT REMOVE
+ (pr debug-string)
+ (print-env)
+ ;DO NOT REMOVE
+ (assoc expr
+ expr-type (ret -any)))
+
(defmethod invoke-cljs-special 'typed.internal/ann-form-cljs*
[{[the-expr {typ-syn :form :as texpr} :as args] :args :as expr} & [expected]]
(assert (= (count args) 2))
(assert (= (:op texpr) :constant))
- (let [_ (prn 'type-syn typ-syn)
- given-type (parse-type typ-syn)
- _ (prn 'given-type (unparse-type given-type))
+ (let [given-type (parse-type typ-syn)
cform (check-cljs the-expr (ret given-type))
- _ (prn 'cform cform)
_ (assert (subtype? (-> cform expr-type ret-t) given-type)
(str "Annotation does not match actual type:\n"
"Expected: " (unparse-type given-type)"\n"
@@ -242,7 +252,6 @@
(defmethod check-cljs :invoke
[{fexpr :f :keys [args] :as expr} & [expected]]
- (prn "invoke" expr)
(let [e (invoke-cljs-special expr)]
(cond
(not= e ::not-special) e
@@ -260,7 +269,15 @@
(assoc expr
expr-type (ret (binding [*var-annotations* CLJS-VAR-ENV
*current-env* env]
- (type-of vname)))))
+ (type-of vname))
+ ;only local bindings are immutable, vars do not partipate in occurrence typing
+ (if-not (namespace vname)
+ (-FS (-not-filter (Un -nil -false) vname)
+ (-filter (Un -nil -false) vname))
+ (-FS -top -top))
+ (if-not (namespace vname)
+ (->Path nil vname)
+ -empty))))
(defmethod check-cljs :do
[{:keys [ret statements] :as expr} & [expected]]
@@ -272,6 +289,7 @@
(defmethod check-cljs :fn
[{:keys [name max-fixed-arity methods variadic] :as expr} & [expected]]
+ (when expected (prn 'fn-expected (unparse-type (ret-t expected))))
(binding [*check-fn-method1-checkfn* check-cljs]
(assoc expr
expr-type
@@ -318,9 +336,10 @@
(defmethod check-cljs :if
[{:keys [test then else] :as expr} & [expected]]
(let [ctest (check-cljs test)]
+ (prn "check-cljs :if" (expr-type ctest))
(assoc expr
expr-type (binding [*check-if-checkfn* check-cljs]
- (check-if (expr-type ctest) then else)))))
+ (check-if (expr-type ctest) then else expected)))))
(defmethod check-cljs :let
[{:keys [loop bindings statements ret env] :as expr} & [expected]]
@@ -394,6 +413,9 @@
(cf-cljs (fn [a] (if a (a) true)) [(U nil [-> BooleanCLJS]) -> BooleanCLJS])
+ (ana-cljs {:locals {} :context :expr :ns {:name cljs/*cljs-ns*}}
+ (list `ann-form-cljs 1 'Any))
+
(ana-cljs denv '(fn [a] a))
(cf-cljs (fn [a b c] a) [BooleanCLJS BooleanCLJS Any -> BooleanCLJS])
@@ -438,4 +460,18 @@
(cf-cljs (ns my-ns (:require [cljs.core :as s])))
(check-cljs-ns typed.test.logic)
+
+ (cljs/analyze (cljs/empty-env) '(typed.internal/print-env "start"))
+ (cf-cljs (typed.internal/print-env "start"))
+
+ (cljs-ann foo [(U nil [-> BooleanCLJS]) -> BooleanCLJS])
+ (cf-cljs
+ (defn foo [x]
+ (typed.internal/print-env "top-of-foo")
+ (if x
+ (x)
+ false)))
+
+
+
)
View
@@ -562,18 +562,21 @@
(load "check")
(load "check_cljs")
+;emit something that CLJS can display ie. a quoted unparsed typed
(defmacro cf-cljs
"Type check a Clojurescript form and return its type"
([form]
- (do (ensure-clojurescript)
- (-> (ana-cljs {:locals {} :context :expr :ns {:name cljs/*cljs-ns*}} form) check-cljs expr-type unparse-TCResult)))
+ (let [t
+ (do (ensure-clojurescript)
+ (-> (ana-cljs {:locals {} :context :expr :ns {:name cljs/*cljs-ns*}} form) check-cljs expr-type unparse-TCResult))]
+ `'~t))
([form expected]
- (prn 'expected expected)
- (prn 'prse (parse-type expected))
- (do (ensure-clojurescript)
- (-> (ana-cljs {:locals {} :context :expr :ns {:name cljs/*cljs-ns*}}
- (list 'typed.core/ann-form-cljs form expected))
- (#(check-cljs % (ret (parse-type expected)))) expr-type unparse-TCResult))))
+ (let [t
+ (do (ensure-clojurescript)
+ (-> (ana-cljs {:locals {} :context :expr :ns {:name cljs/*cljs-ns*}}
+ (list `ann-form-cljs form expected))
+ (#(check-cljs % (ret (parse-type expected)))) expr-type unparse-TCResult))]
+ `'~t)))
(defmacro cf
"Type check a Clojure form and return its type"
@@ -584,7 +587,7 @@
([form expected]
`(do (ensure-clojure)
(tc-ignore
- (-> (ast (ann-form-cljs ~form ~expected)) (#(check % (ret (parse-type '~expected)))) expr-type unparse-TCResult)))))
+ (-> (ast (ann-form ~form ~expected)) (#(check % (ret (parse-type '~expected)))) expr-type unparse-TCResult)))))
(defn analyze-file-asts
[^String f]
@@ -616,8 +619,8 @@
(check-cljs ast)))))
(defmacro check-cljs-ns
- ([] (check-cljs-ns*))
- ([nsym] (check-cljs-ns* nsym)))
+ ([] (check-cljs-ns*) `'~'success)
+ ([nsym] (check-cljs-ns* nsym) `'~'success))
(defn check-ns
"Type check a namespace. If not provided default to current namespace"
View
@@ -70,6 +70,7 @@
(infer X {} S T -any))
(defn subtypeA* [A s t]
+ {:post [(set? %)]}
(if (or (contains? A [s t])
(= s t)
(Top? t)
@@ -120,7 +121,7 @@
(subtypeA* *sub-current-seen* s (resolve-App t))
(Union? s)
- (if (every? #(subtypeA* *sub-current-seen* % t) (:types s))
+ (if (every? #(subtypeA*? *sub-current-seen* % t) (:types s))
*sub-current-seen*
(type-error s t))
@@ -168,6 +169,7 @@
:else (subtype* s t)))))
(defn subtype [s t]
+ {:post [(set? %)]}
(subtypeA* *sub-current-seen* s t))
(defn subtypes*-varargs [A0 argtys dom rst]

0 comments on commit 0bd50e6

Please sign in to comment.