New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

manually type checked #3

Open
wants to merge 1 commit into
from
Jump to file or symbol
Failed to load files and symbols.
+46 −26
Diff settings

Always

Just for now

View
@@ -1,6 +1,6 @@
(ns mini-occ.core
{:lang :core.typed
:core.typed {:features #{:runtime-infer}}
;:core.typed {:features #{:runtime-infer}}
}
(:require [clojure.test :refer [deftest is]]
[clojure.core.typed :as t :refer [defalias ann U Vec Set Sym]]
@@ -12,7 +12,9 @@
(declare E NameTypeMap P T)
(defalias
E
(U
(U
'{:E ':add1}
'{:E ':n?}
'{:E ':app, :args (Vec E), :fun E}
'{:E ':false}
'{:E ':if, :else E, :test E, :then E}
@@ -30,26 +32,23 @@
(defalias
T
(U
'{:T ':not, :type T}
'{:T ':refine, :name t/Sym, :prop P}
'{:T ':union, :types (t/Set T)}
'{:T ':false}
'{:T ':fun, :params '[NameTypeMap], :return T}
'{:T ':fun, :params (t/Vec NameTypeMap), :return T}
'{:T ':intersection, :types (Set T)}
'{:T ':num}))
(ann check [(Set t/Nothing) E :-> T])
(ann id [(t/Map t/Any t/Any) :-> (t/Map t/Any t/Any)])
(ann id-test AnyFunction)
(ann ^:no-check check [(Set P) E :-> T]) ;; implementation of this function is WIP
(ann ^:no-check id [(t/Map t/Any t/Any) :-> (t/Map t/Any t/Any)]) ;;irrelevant
(ann parse-exp [t/Any :-> E])
(ann parse-exp-test AnyFunction)
(ann parse-prop [(t/Coll t/Any) :-> P])
(ann parse-prop-test AnyFunction)
(ann parse-prop [t/Any :-> P])
(ann parse-roundtrip [(t/Coll t/Any) :-> Boolean])
(ann parse-type [t/Any :-> T])
(ann parse-types-test AnyFunction)
(ann tc [(Vec t/Nothing) false :-> false])
(ann tc-test AnyFunction)
(ann tc [(Vec P) t/Any :-> t/Any])
(ann unparse-exp [E :-> t/Any])
(ann unparse-prop [P :-> (t/Coll t/Any)])
(ann unparse-prop-test AnyFunction)
(ann unparse-type [T :-> (U Sym false)])
(ann unparse-type [T :-> t/Any])
;; End: Generated by clojure.core.typed - DO NOT EDIT
;; e ::= x | (if e e e) | (lambda (x :- t) e) | (e e*) | #f | n? | add1
;; t ::= [x : t -> t] | (not t) | (or t t) | (and t t) | #f | N | Any
@@ -127,6 +126,7 @@
{:P :not
:p (parse-prop np)})))
(t/tc-ignore
(deftest parse-prop-test
(is (= (parse-prop '(is x Any))
{:P :is,
@@ -150,6 +150,7 @@
'{:P :not,
:p {:P :=, :exps #{{:name z, :E :var} {:args [{:name y, :E :var}], :fun {:name x, :E :var}, :E :app}}}}))
)
)
(declare unparse-exp unparse-type)
@@ -175,39 +176,48 @@
:exp {:E :var, :name x},
:type {:T :intersection, :types #{}}}})
(t/tc-ignore
(deftest unparse-prop-test
(is (parse-roundtrip '(is x Any)))
(is (parse-roundtrip '(= z (x y))))
(is (parse-roundtrip '(or (= (x y) z) (is x Any))))
(is (parse-roundtrip '(and (= (x y) z) (is x Any))))
(is (parse-roundtrip '(not (= (x y) z)))))
)
; Any -> T
(defn parse-type [t]
(cond
(vector? t) (let [[args [_ ret]] (split-at (- (count t) 2) t)
args (map (t/ann-form
(fn [[x _ t]]
{:pre [(symbol? x)]}
{:name x
:type (parse-type t)})
[(t/Coll (U Sym ':-)) :-> NameTypeMap])
[(t/ASeq t/Any) :-> NameTypeMap])
(partition 3 args))]
(assert (#{'->} (get t (- (count t) 2)))
(get t (- (count t) 2)))
{:T :fun
:params (vec args)
:return (parse-type ret)})
(seq? t) (case (first t)
not (let [[_ t1] t]
not (let [_ (assert (and (seqable? t) (sequential? t)))
[_ t1] t]
{:T :not
:type (parse-type t)})
or (let [[_ & ts] t]
or (let [_ (assert (and (seqable? t) (sequential? t)))
[_ & ts] t]
{:T :union
:types (set (map parse-type ts))})
and (let [[_ & ts] t]
and (let [_ (assert (and (seqable? t) (sequential? t)))
[_ & ts] t]
{:T :intersection
:types (set (map parse-type ts))})
refine (let [[_ [x] p] t]
refine (let [_ (assert (and (seqable? t) (sequential? t)))
[_ mid p] t
_ (assert (and (seqable? mid) (sequential? mid)))
[x] mid]
(assert (symbol? x))
{:T :refine
:name x
@@ -217,13 +227,15 @@
('#{Any} t) {:T :intersection :types #{}}
:else (assert false t)))
(t/tc-ignore
(deftest parse-types-test
(is (parse-type '(and false Num))))
)
(defn unparse-type [t]
{:pre [(contains? t :T)]}
(case (:T t)
:fun `[~@(mapcat (fn [{:keys [name type]}]
:fun `[~@(mapcat (t/fn [{:keys [name type]} :- NameTypeMap]
[name :- (unparse-type type)])
(:params t))
~'->
@@ -246,27 +258,31 @@
(= 'n? e) {:E :n?}
(= 'add1 e) {:E :add1}
(seq? e) (case (first e)
if (let [[_ e1 e2 e3] e]
if (let [[_ e1 e2 e3] (seq e)]
(assert (= 4 (count e)))
{:E :if
:test (parse-exp e1)
:then (parse-exp e2)
:else (parse-exp e3)})
lambda (let [[_ [x _ t :as param] b] e]
lambda (let [[_ param b] (seq e)
_ (assert (seqable? param))
[x _ t] (seq param)]
(assert (= 3 (count e)))
(assert (= 3 (count param)))
(assert (symbol? x))
{:E :lambda
:arg x
:arg-type (parse-type t)
:body (parse-exp b)})
(let [[f & args] e]
(let [_ (assert (seqable? e) (sequential? e))
[f & args] e]
(assert (<= 1 (count e)))
{:E :app
:fun (parse-exp f)
:args (mapv parse-exp args)}))
:else (assert false e)))
(t/tc-ignore
(deftest parse-exp-test
(is (= (parse-exp 'x)
'{:name x, :E :var}))
@@ -299,6 +315,7 @@
{:E :false}))
(is (= (parse-exp 'add1)
'{:name add1, :E :var})))
)
; E -> Any
(defn unparse-exp [e]
@@ -332,15 +349,16 @@
:false {:T :false}
:lambda {:T :fun
:params [{:name (:arg e), :type (:arg-type e)}]
:return (check (conj ps {:P :is, :exp (:arg e), :type (:arg-type e)})
:return (check (conj ps {:P :is, :exp {:E :var :name (:arg e)}, :type (:arg-type e)})
(:body e))}
:add1 (parse-type '[x :- Num -> Num])
:n? (parse-type '[x :- Any -> (refine [r]
(or (and (is r true)
(is x Num))
(and (is r false)
(is x (not Num)))))])
:app (let [[e1 e2] e
:app (let [_ (assert false "WIP")
[e1 e2] e
t1 (check ps e1)
t2 (check ps e2)]
(assert (#{:fun} (:T t1)) t1)
@@ -358,11 +376,13 @@
(parse-exp e))
unparse-type))
(t/tc-ignore
(deftest tc-test
(is (= false
(tc [] false)))
#_(is (= false
(tc [] '(lambda (x :- Num) (add1 x))))))
)
;; suprise identity function to mess up inference.
(defn id [x] x)
@@ -571,4 +591,4 @@ str/upper-case
(atom {x 1
y 2})
)
)