Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Browse files

CLJS test ns, new analyze dep

  • Loading branch information...
commit e302b4f49321b689f6f8e595a0df5515a76c7e88 1 parent 48756cc
@frenchy64 authored
View
2  project.clj
@@ -1,6 +1,6 @@
(defproject typed "0.1.3-SNAPSHOT"
:description "Gradual typing for Clojure"
- :dependencies [[analyze "0.2"]
+ :dependencies [[analyze "0.3-SNAPSHOT"]
[net.intensivesystems/arrows "1.3.0"] ;for testing conduit, lein test wants it here?
[trammel "0.7.0"]
[org.clojure/math.combinatorics "0.0.2"]
View
16 src/typed/check.clj
@@ -1573,15 +1573,13 @@
(assert (:line env))
(binding [*current-env* env
*check-fn-method1-checkfn* check
- *check-fn-method1-checkfn* (fn [rest drest]
- {:pre [(some-fn #(when rest
- (Type? rest))
- #(when drest
- (DottedPretype? drest)))
- (not (and rest drest))]
- :post [(Type? %)]}
- (Un -nil (In (RClass-of Seqable [(or rest (.pre-type drest))])
- (make-CountRange 1))))]
+ *check-fn-method1-rest-type* (fn [rest drest]
+ {:pre [(or (Type? rest)
+ (DottedPretype? drest))
+ (not (and rest drest))]
+ :post [(Type? %)]}
+ (Un -nil (In (RClass-of Seqable [(or rest (.pre-type drest))])
+ (make-CountRange 1))))]
(assoc expr
expr-type (check-fn expr (or expected
(ret (make-FnIntersection
View
103 src/typed/check_cljs.clj
@@ -3,10 +3,22 @@
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Modify CLJS specials
-(def new-specials '#{defprotocol #_deftype typed.core/ann-form-cljs
- cljs.core/extend-type})
-
-(.doReset #'cljs.analyzer/specials (set/union cljs/specials new-specials))
+(assert cljs/specials)
+(def orig-specials cljs/specials)
+
+(def new-specials (set/union
+ orig-specials
+ '#{cljs.core/defprotocol deftype typed.core/ann-form-cljs
+ defprotocol
+ cljs.core/extend-type}))
+
+(defmacro with-altered-specials
+ [& body]
+ `(try
+ (alter-var-root #'cljs.analyzer/specials (constantly new-specials))
+ ~@body
+ (finally
+ (alter-var-root #'cljs.analyzer/specials (constantly orig-specials)))))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Special forms
@@ -14,8 +26,10 @@
(defmacro ann-form-cljs [form tsyn]
`form)
+(declare cljs-ann*)
+
(defmacro cljs-ann [vname tsyn]
- `(cljs-ann* '~vname '~tsyn))
+ `'~(cljs-ann* vname tsyn))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Envs
@@ -24,9 +38,14 @@
(set-validator! CLJS-VAR-ENV (hash-c? symbol? Type?))
(defn cljs-ann* [vname tsyn]
- (let [vtype (parse-type tsyn)]
- (swap! CLJS-VAR-ENV assoc vname vtype)
- [vname (unparse-type vtype)]))
+ (let [vtype (parse-type tsyn)
+ var (if (namespace vname)
+ (symbol vname)
+ (symbol (str cljs/*cljs-ns*) (str vname)))]
+ (swap! CLJS-VAR-ENV assoc var vtype)
+ [var (unparse-type vtype)]))
+
+(defonce CLJS-PROTOCOL-ENV (atom {}))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Types
@@ -80,6 +99,12 @@
*current-env*
(type-error s t)))
+(defmethod subtype* [Value BooleanCLJS ::clojurescript]
+ [{:keys [val] :as s} t]
+ (if ((some-fn true? false?) val)
+ *current-env*
+ (type-error s t)))
+
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Parsing new special forms
@@ -122,6 +147,11 @@
(defmulti check-cljs (fn [expr & [expected]] (:op expr)))
+(defmethod check-cljs :no-op
+ [expr & [expected]]
+ (assoc expr
+ expr-type (ret -any)))
+
(defmethod check-cljs :constant
[{:keys [form] :as expr} & [expected]]
(let [t (->Value form)
@@ -150,17 +180,18 @@
(map (comp ret-t expr-type) cvals)))))))
(defmethod check-cljs :def
- [{:keys [init] vname :name :as expr} & [expected]]
+ [{:keys [init env] vname :name :as expr} & [expected]]
(assert init "declare NYI")
(assert (not expected))
- (let [ann-type (binding [*var-annotations* CLJS-VAR-ENV]
+ (let [ann-type (binding [*var-annotations* CLJS-VAR-ENV
+ *current-env* env]
(type-of vname))
cinit (check-cljs init expected)
_ (assert (subtype? (-> cinit expr-type ret-t)
ann-type)
- (str "Var definition did not match annotation." \n
- " Expected: " (unparse-type ann-type) \n
- " Actual" (unparse-type ann-type)))]
+ (str "Var definition did not match annotation."
+ " Expected: " (unparse-type ann-type)
+ ", Actual: " (unparse-type (-> cinit expr-type ret-t))))]
(assoc expr
;FIXME should really be Var, change when protocols are implemented
expr-type (ret -any))))
@@ -194,14 +225,14 @@
expr-type actual)))
(defmethod check-cljs :var
- [{{vname :name} :info :as expr} & [expected]]
+ [{{vname :name} :info :keys [env] :as expr} & [expected]]
(assoc expr
- expr-type (ret (binding [*var-annotations* CLJS-VAR-ENV]
+ expr-type (ret (binding [*var-annotations* CLJS-VAR-ENV
+ *current-env* env]
(type-of vname)))))
(defmethod check-cljs :do
[{:keys [ret statements] :as expr} & [expected]]
- (prn ret)
(let [cstatements (mapv check-cljs statements)
cret (check-cljs ret expected)]
(assoc expr
@@ -272,12 +303,17 @@
(assert false) #_(check-let bindings body expr true expected)
(check-let bindings body expr false expected)))))
+(defmethod check-cljs :ns
+ [expr & [expected]]
+ (assoc expr
+ expr-type (ret -any)))
;; Debug
(defn ana-cljs [env form]
- (binding [cljs/*cljs-ns* (-> env :ns :name)]
- (cljs/analyze env form)))
+ (with-altered-specials
+ (binding [cljs/*cljs-ns* cljs/*cljs-ns*]
+ (cljs/analyze env form))))
(comment
;; TODO there's a bug in the docstring for cljs.analyzer/analyze: it says :ns is a symbol, when instead it's {:name nsym}
@@ -292,15 +328,17 @@
(cljs/analyze denv {:a 1})
(cf-cljs {:a 1})
-(cljs-ann cljs.user/a Any)
+(cljs/analyze denv (cljs-ann cljs.user/a Any))
(@CLJS-VAR-ENV 'cljs.user/a)
(cljs/analyze denv '(def a 1))
(cf-cljs (def a 1))
; defprotocol doesn't macroexpand because we've added 'defprotocol as a special
-(cljs/macroexpand-1 {} '(defprotocol A))
-(cljs/analyze denv '(defprotocol A))
+ (with-altered-specials
+ (prn cljs/specials)
+ (cljs/macroexpand-1 {} '(defprotocol A)))
+(cljs/analyze (cljs/empty-env) '(defprotocol A))
(cf-cljs (defprotocol A))
@@ -328,11 +366,18 @@
; deftype
(ana-cljs denv '(deftype A [b] cljs.core/ASeq))
-(cljs/macroexpand-1 denv '(deftype A [b]
- cljs.core/ASeq
- cljs.core/IFn
- (invoke [this a b] a)))
-(ana-cljs denv '(deftype A [b]
+ (cljs/macroexpand-1 (cljs/empty-env)
+ '(deftype A [b]
+ cljs.core/ASeq
+ cljs.core/IFn
+ (invoke [this a b] a)))
+ (cljs/macroexpand-1 (cljs/empty-env)
+ '(cljs.core/extend-type A
+ cljs.core/ASeq
+ cljs.core/ISeq
+ (first [this] this)
+ #_cljs.core/IFn #_(invoke ([this a b] a))))
+(cljs/analyze (cljs/empty-env) '(deftype A [b]
cljs.core/ASeq
cljs.core/IFn
(invoke [this a b] a)))
@@ -354,4 +399,10 @@
(ana-cljs denv '(let [a 2] a))
(cf-cljs (let [a 2] a))
+
+
+ ;ns
+ (cf-cljs (ns my-ns (:require [cljs.core :as s])))
+
+ (check-cljs-ns typed.test.logic)
)
View
45 src/typed/core.clj
@@ -14,6 +14,7 @@
[clojure.pprint :refer [pprint]]
[trammel.core :as contracts]
[clojure.math.combinatorics :as comb]
+ [clojure.java.io :as io]
[cljs
[compiler]
[analyzer :as cljs]]
@@ -566,11 +567,11 @@
([form]
`(do (ensure-clojurescript)
(tc-ignore
- (-> (ana-cljs {:locals {} :context :expr :ns {:name '~'cljs.user}} '~form) check-cljs expr-type unparse-TCResult))))
+ (-> (ana-cljs {:locals {} :context :expr :ns {:name cljs/*cljs-ns*}} '~form) check-cljs expr-type unparse-TCResult))))
([form expected]
- `(do (ensure-clojure)
+ `(do (ensure-clojurescript)
(tc-ignore
- (-> (ana-cljs {:locals {} :context :expr :ns {:name '~'cljs.user}}
+ (-> (ana-cljs {:locals {} :context :expr :ns {:name cljs/*cljs-ns*}}
'(typed.core/ann-form-cljs ~form ~expected))
(#(check-cljs % (ret (parse-type '~expected)))) expr-type unparse-TCResult)))))
@@ -585,11 +586,43 @@
(tc-ignore
(-> (ast (ann-form-cljs ~form ~expected)) (#(check % (ret (parse-type '~expected)))) expr-type unparse-TCResult)))))
+(defn analyze-file-asts
+ [^String f]
+ (let [res (if (re-find #"^file://" f) (java.net.URL. f) (io/resource f))]
+ (assert res (str "Can't find " f " in classpath"))
+ (with-altered-specials
+ (binding [cljs/*cljs-ns* 'cljs.user
+ cljs/*cljs-file* (.getPath ^java.net.URL res)
+ *ns* cljs/*reader-ns*]
+ (with-open [r (io/reader res)]
+ (let [env (cljs/empty-env)
+ pbr (clojure.lang.LineNumberingPushbackReader. r)
+ eof (Object.)]
+ (loop [r (read pbr false eof false)
+ asts []]
+ (let [env (assoc env :ns (cljs/get-namespace cljs/*cljs-ns*))]
+ (if-not (identical? eof r)
+ (let [ast1 (cljs/analyze env r)]
+ (recur (read pbr false eof false) (conj asts ast1)))
+ asts)))))))))
+
+(defn check-cljs-ns*
+ "Type check a CLJS namespace. If not provided default to current namespace"
+ ([] (check-cljs-ns* cljs/*cljs-ns*))
+ ([nsym]
+ (ensure-clojurescript)
+ (let [asts (analyze-file-asts (cljs/ns->relpath nsym))]
+ (doseq [ast asts]
+ (check-cljs ast)))))
+
+(defmacro check-cljs-ns
+ ([] (check-cljs-ns*))
+ ([nsym] (check-cljs-ns* nsym)))
+
(defn check-ns
"Type check a namespace. If not provided default to current namespace"
([] (check-ns (ns-name *ns*)))
([nsym]
- (require nsym)
(ensure-clojure)
(with-open [pbr (analyze/pb-reader-for-ns nsym)]
(let [[_ns-decl_ & asts] (analyze/analyze-ns pbr (analyze/uri-for-ns nsym) nsym)]
@@ -607,11 +640,15 @@
(comment
(check-ns 'typed.test.example)
+
; very slow because of update-composite
(check-ns 'typed.test.rbt)
+
(check-ns 'typed.test.macro)
(check-ns 'typed.test.conduit)
(check-ns 'typed.test.deftype)
(check-ns 'typed.test.core-logic)
(check-ns 'typed.test.ckanren)
+
+ (check-cljs-ns 'typed.test.logic)
)
View
1,003 test/typed/test/logic.cljs
@@ -0,0 +1,1003 @@
+(ns typed.test.logic
+ (:refer-clojure :exclude [==])
+ (:use-macros [typed.test.logic.macros :only
+ [defne defna defnu fresh == -inc]])
+ (:require-macros [typed.test.logic.macros :as m]
+ [typed.core :refer [cljs-ann check-cljs-ns]])
+ (:require [clojure.set :as set])
+ (:use [clojure.walk :only [postwalk]]))
+
+(cljs-ann *occurs-check* BooleanCLJS)
+(def ^{:dynamic true} *occurs-check* true)
+
+(defprotocol IUnifyTerms
+ (-unify-terms [u v s]))
+
+(defprotocol IUnifyWithNil
+ (-unify-with-nil [v u s]))
+
+(defprotocol IUnifyWithObject
+ (-unify-with-object [v u s]))
+
+(defprotocol IUnifyWithLVar
+ (-unify-with-lvar [v u s]))
+
+(defprotocol IUnifyWithLSeq
+ (-unify-with-lseq [v u s]))
+
+(defprotocol IUnifyWithSequential
+ (-unify-with-seq [v u s]))
+
+(defprotocol IUnifyWithMap
+ (-unify-with-map [v u s]))
+
+(defprotocol IUnifyWithSet
+ (-unify-with-set [v u s]))
+
+(defprotocol IReifyTerm
+ (-reify-term [v s]))
+
+(defprotocol IWalkTerm
+ (-walk-term [v s]))
+
+(defprotocol IOccursCheckTerm
+ (-occurs-check-term [v x s]))
+
+(defprotocol IBuildTerm
+ (-build-term [u s]))
+
+(defprotocol IBind
+ (-bind [this g]))
+
+(defprotocol IMPlus
+ (-mplus [a f]))
+
+(defprotocol ITake
+ (-take* [a]))
+
+;; =============================================================================
+;; Pair
+
+(defprotocol IPair
+ (-lhs [this])
+ (-rhs [this]))
+
+(deftype Pair [lhs rhs]
+ IEquiv
+ (-equiv [this other]
+ (and (= lhs (.-lhs other))
+ (= rhs (.-rhs other))))
+ ICounted
+ (-count [_] 2)
+ IIndexed
+ (-nth [_ i] (condp = i
+ 0 lhs
+ 1 rhs
+ (throw (js/Error. "Index out of bounds"))))
+ (-nth [_ i not-found] (condp = i
+ 0 lhs
+ 1 rhs
+ not-found))
+ IPair
+ (-lhs [_] lhs)
+ (-rhs [_] rhs)
+ IPrintWithWriter
+ (-pr-writer [coll writer opts]
+ (-write writer (str "(" lhs " . " rhs ")"))))
+
+(defn pair [lhs rhs]
+ (Pair. lhs rhs))
+
+;; =============================================================================
+;; Substitutions
+
+(defprotocol ISubstitutions
+ (-occurs-check [this u v])
+ (-ext [this u v])
+ (-ext-no-check [this u v])
+ (-walk [this v])
+ (-walk* [this v])
+ (-unify [this u v])
+ (-reify-lvar-name [_])
+ (-reify* [this v])
+ (-reify [this v]))
+
+(declare empty-s)
+(declare choice)
+(declare lvar)
+(declare lvar?)
+(declare pair)
+(declare lcons)
+
+(def not-found (js-obj))
+
+(defn assq
+ "Similar to Scheme assq, xs must be a List of Pairs"
+ [k ^cljs.core/List xs]
+ (loop [xs (-seq xs)]
+ (if (nil? xs)
+ not-found
+ (let [^cljs.core/List xs xs
+ x (-first xs)
+ lhs (.-lhs x)]
+ (if (identical? k lhs)
+ (.-rhs x)
+ (recur (-next xs)))))))
+
+(deftype Substitutions [s]
+ IEquiv
+ (-equiv [this o]
+ (or (identical? this o)
+ (and (instance? Substitutions o)
+ (= s (.-s o)))))
+
+ IPrintWithWriter
+ (-pr-writer [this writer opts]
+ (-pr-writer s writer opts))
+
+ ISubstitutions
+ (-occurs-check [this u v]
+ (let [v (-walk this v)]
+ (-occurs-check-term v u this)))
+
+ (-ext [this u v]
+ (if (and *occurs-check* (-occurs-check this u v))
+ nil
+ (-ext-no-check this u v)))
+
+ (-ext-no-check [this u v]
+ (Substitutions. (conj s (Pair. u v))))
+
+ (-walk [this v]
+ (cond
+ (lvar? v) (let [rhs (assq v s)
+ vp (-walk this rhs)]
+ (if (identical? not-found vp) v vp))
+ :else v))
+
+ (-walk* [this v]
+ (let [v (-walk this v)]
+ (-walk-term v this)))
+
+ (-unify [this u v]
+ (if (identical? u v)
+ this
+ (let [u (-walk this u)
+ v (-walk this v)]
+ (if (identical? u v)
+ this
+ (-unify-terms u v this)))))
+
+ (-reify-lvar-name [this]
+ (symbol (str "_." (count s))))
+
+ (-reify* [this v]
+ (let [v (-walk this v)]
+ (-reify-term v this)))
+
+ (-reify [this v]
+ (let [v (-walk* this v)]
+ (-walk* (-reify* empty-s v) v)))
+
+ IBind
+ (-bind [this g]
+ (g this))
+
+ IMPlus
+ (-mplus [this f]
+ (choice this f))
+
+ ITake
+ (-take* [this]
+ this))
+
+(defn make-s [s]
+ (Substitutions. s))
+
+(def empty-s (make-s '()))
+
+(defn ^boolean subst? [x]
+ (instance? Substitutions x))
+
+(defn to-s [v]
+ (let [s (reduce (fn [l [k v]]
+ (conj l (pair k v)))
+ () v)]
+ (make-s s)))
+
+;; =============================================================================
+;; Logic Variables
+
+(deftype LVar [name meta]
+ Object
+ (toString [this]
+ (pr-str this))
+ IHash
+ (-hash [this]
+ (-hash name))
+ IMeta
+ (-meta [this]
+ meta)
+ IWithMeta
+ (-with-meta [this new-meta]
+ (LVar. name meta))
+ IPrintWithWriter
+ (-pr-writer [_ writer opts]
+ (-write writer (str "<lvar:" name ">")))
+ IEquiv
+ (-equiv [this o]
+ (and (instance? LVar o)
+ (let [o o]
+ (identical? name (.-name o)))))
+ IUnifyTerms
+ (-unify-terms [u v s]
+ (-unify-with-lvar v u s))
+ IUnifyWithNil
+ (-unify-with-nil [v u s]
+ (-ext-no-check s v u))
+ IUnifyWithObject
+ (-unify-with-object [v u s]
+ (-ext s v u))
+ IUnifyWithLVar
+ (-unify-with-lvar [v u s]
+ (-ext-no-check s u v))
+ IUnifyWithLSeq
+ (-unify-with-lseq [v u s]
+ (-ext s v u))
+ IUnifyWithSequential
+ (-unify-with-seq [v u s]
+ (-ext s v u))
+ IUnifyWithMap
+ (-unify-with-map [v u s]
+ (-ext s v u))
+ IUnifyWithSet
+ (-unify-with-set [v u s]
+ (-ext s v u))
+ IReifyTerm
+ (-reify-term [v s]
+ (-ext s v (-reify-lvar-name s)))
+ IWalkTerm
+ (-walk-term [v s] v)
+ IOccursCheckTerm
+ (-occurs-check-term [v x s]
+ (= (-walk s v) x)))
+
+(def lvar-sym-counter (atom 0))
+
+(defn lvar
+ ([] (lvar 'gen))
+ ([name]
+ (let [name (js* "~{} + '_' + ~{}"
+ (.substring name 2 (.-length name))
+ (swap! lvar-sym-counter inc))]
+ (LVar. name nil))))
+
+(defn ^boolean lvar? [x]
+ (instance? LVar x))
+
+;; =============================================================================
+;; LCons
+
+(defprotocol LConsSeq
+ (-lfirst [this])
+ (-lnext [this]))
+
+(declare lcons?)
+
+(defn lcons-pr-seq [x]
+ (cond
+ (lcons? x) (lazy-seq
+ (cons (-lfirst x)
+ (lcons-pr-seq (-lnext x))))
+ :else (list '. x)))
+
+(deftype LCons [a d meta]
+ IMeta
+ (-meta [this]
+ meta)
+ IWithMeta
+ (-with-meta [this new-meta]
+ (LCons. a d new-meta))
+ LConsSeq
+ (-lfirst [_] a)
+ (-lnext [_] d)
+ IPrintWithWriter
+ (-pr-writer [this writer opts]
+ (pr-sequential-writer writer pr-writer "(" " " ")" opts (lcons-pr-seq this)))
+ IEquiv
+ (-equiv [this o]
+ (or (identical? this o)
+ (and (instance? LCons o)
+ (loop [me this
+ you o]
+ (cond
+ (nil? me) (nil? you)
+ (lvar? me) true
+ (lvar? you) true
+ (and (lcons? me) (lcons? you))
+ (let [mef (-lfirst me)
+ youf (-lfirst you)]
+ (and (or (= mef youf)
+ (lvar? mef)
+ (lvar? youf))
+ (recur (-lnext me) (-lnext you))))
+ :else (= me you))))))
+ IUnifyTerms
+ (-unify-terms [u v s]
+ (-unify-with-lseq v u s))
+ IUnifyWithNil
+ (-unify-with-nil [v u s] false)
+ IUnifyWithObject
+ (-unify-with-object [v u s] false)
+ IUnifyWithLSeq
+ (-unify-with-lseq [v u s]
+ (loop [u u v v s s]
+ (if (lvar? u)
+ (-unify s u v)
+ (cond
+ (lvar? v) (-unify s v u)
+ (and (lcons? u) (lcons? v))
+ (if-let [s (-unify s (-lfirst u) (-lfirst v))]
+ (recur (-lnext u) (-lnext v) s)
+ false)
+ :else (-unify s u v)))))
+ IUnifyWithSequential
+ (-unify-with-seq [v u s]
+ (-unify-with-lseq u v s))
+ IUnifyWithMap
+ (-unify-with-map [v u s] false)
+ IUnifyWithSet
+ (-unify-with-set [v u s] false)
+ IReifyTerm
+ (-reify-term [v s]
+ (loop [v v s s]
+ (if (lcons? v)
+ (recur (-lnext v) (-reify* s (-lfirst v)))
+ (-reify* s v))))
+ IWalkTerm
+ (-walk-term [v s]
+ (lcons (-walk* s (-lfirst v))
+ (-walk* s (-lnext v))))
+ IOccursCheckTerm
+ (-occurs-check-term [v x s]
+ (loop [v v x x s s]
+ (if (lcons? v)
+ (or (-occurs-check s x (-lfirst v))
+ (recur (-lnext v) x s))
+ (-occurs-check s x v)))))
+
+(defn lcons
+ "Constructs a sequence a with an improper tail d if d is a logic variable."
+ [a d]
+ (if (or (coll? d) (nil? d))
+ (cons a (seq d))
+ (LCons. a d nil)))
+
+(defn ^boolean lcons? [x]
+ (instance? LCons x))
+
+;; =============================================================================
+;; Unification
+
+(extend-protocol IUnifyTerms
+ nil
+ (-unify-terms [u v s]
+ (-unify-with-nil v u s))
+
+ default
+ (-unify-terms [u v s]
+ (if (sequential? u)
+ (-unify-with-seq v u s)
+ (-unify-with-object v u s)))
+
+ ObjMap
+ (-unify-terms [u v s]
+ (-unify-with-map v u s))
+
+ PersistentArrayMap
+ (-unify-terms [u v s]
+ (-unify-with-map v u s))
+
+ PersistentHashMap
+ (-unify-terms [u v s]
+ (-unify-with-map v u s))
+
+ PersistentHashSet
+ (-unify-terms [u v s]
+ (-unify-with-set v u s)))
+
+;; -----------------------------------------------------------------------------
+;; Unify nil with X
+
+(extend-protocol IUnifyWithNil
+ nil
+ (-unify-with-nil [v u s] s)
+
+ default
+ (-unify-with-nil [v u s] false))
+
+;; -----------------------------------------------------------------------------
+;; Unify Object with X
+
+(extend-protocol IUnifyWithObject
+ nil
+ (-unify-with-object [v u s] false)
+
+ default
+ (-unify-with-object [v u s]
+ (if (= u v) s false)))
+
+;; -----------------------------------------------------------------------------
+;; Unify LVar with X
+
+(extend-protocol IUnifyWithLVar
+ nil
+ (-unify-with-lvar [v u s] (-ext-no-check s u v))
+
+ default
+ (-unify-with-lvar [v u s]
+ (-ext s u v)))
+
+;; -----------------------------------------------------------------------------
+;; Unify LCons with X
+
+(extend-protocol IUnifyWithLSeq
+ nil
+ (-unify-with-lseq [v u s] false)
+
+ default
+ (-unify-with-lseq [v u s]
+ (if (sequential? v)
+ (loop [u u v v s s]
+ (if (seq v)
+ (if (lcons? u)
+ (if-let [s (-unify s (-lfirst u) (first v))]
+ (recur (-lnext u) (next v) s)
+ false)
+ (-unify s u v))
+ (if (lvar? u)
+ (-unify s u '())
+ false)))
+ false)))
+
+;; -----------------------------------------------------------------------------
+;; Unify Sequential with X
+
+(extend-protocol IUnifyWithSequential
+ nil
+ (-unify-with-seq [v u s] false)
+
+ default
+ (-unify-with-seq [v u s]
+ (if (sequential? v)
+ (loop [u u v v s s]
+ (if (seq u)
+ (if (seq v)
+ (if-let [s (-unify s (first u) (first v))]
+ (recur (next u) (next v) s)
+ false)
+ false)
+ (if (seq v) false s)))
+ false)))
+
+;; -----------------------------------------------------------------------------
+;; Unify IPersistentMap with X
+
+(def not-found (js-obj))
+
+(defn unify-with-map* [v u s]
+ (if-not (cljs.core/== (count v) (count u))
+ false
+ (loop [ks (seq (keys u)) s s]
+ (if ks
+ (let [kf (first ks)
+ vf (get v kf not-found)]
+ (if (identical? vf not-found)
+ false
+ (if-let [s (-unify s (get u kf) vf)]
+ (recur (next ks) s)
+ false)))
+ s))))
+
+(extend-protocol IUnifyWithMap
+ nil
+ (-unify-with-map [v u s] false)
+
+ default
+ (-unify-with-map [v u s] false)
+
+ ObjMap
+ (-unify-with-map [v u s]
+ (unify-with-map* v u s))
+
+ PersistentArrayMap
+ (-unify-with-map [v u s]
+ (unify-with-map* v u s))
+
+ PersistentHashMap
+ (-unify-with-map [v u s]
+ (unify-with-map* v u s)))
+
+;; -----------------------------------------------------------------------------
+;; Unify IPersistentSet with X
+
+(extend-protocol IUnifyWithSet
+ nil
+ (-unify-with-set [v u s] false)
+
+ default
+ (-unify-with-set [v u s] false)
+
+ PersistentHashSet
+ (-unify-with-set [v u s]
+ (loop [u u v v ulvars [] umissing []]
+ (if (seq u)
+ (if (seq v)
+ (let [uf (first u)]
+ (if (lvar? uf)
+ (recur (disj u uf) v (conj ulvars uf) umissing)
+ (if (contains? v uf)
+ (recur (disj u uf) (disj v uf) ulvars umissing)
+ (recur (disj u uf) v ulvars (conj umissing uf)))))
+ false)
+ (if (seq v)
+ (if (seq ulvars)
+ (loop [v v vlvars [] vmissing []]
+ (if (seq v)
+ (let [vf (first v)]
+ (if (lvar? vf)
+ (recur (disj v vf) (conj vlvars vf) vmissing)
+ (recur (disj v vf) vlvars (conj vmissing vf))))
+ (-unify s (concat ulvars umissing)
+ (concat vmissing vlvars))))
+ false)
+ s)))))
+
+;; =============================================================================
+;; Reification
+
+(extend-protocol IReifyTerm
+ nil
+ (-reify-term [v s] s)
+
+ default
+ (-reify-term [v s]
+ (if (sequential? v)
+ (loop [v v s s]
+ (if (seq v)
+ (recur (next v) (-reify* s (first v)))
+ s))
+ s)))
+
+;; =============================================================================
+;; Walk Term
+
+(defn walk-term-map* [v s]
+ (loop [v v r {}]
+ (if (seq v)
+ (let [[vfk vfv] (first v)]
+ (recur (next v) (assoc r vfk (-walk* s vfv))))
+ r)))
+
+(extend-protocol IWalkTerm
+ nil
+ (-walk-term [v s] nil)
+
+ default
+ (-walk-term [v s]
+ (if (sequential? v)
+ (map #(-walk* s %) v)
+ v))
+
+ PersistentVector
+ (-walk-term [v s]
+ (loop [v v r []]
+ (if (seq v)
+ (recur (next v) (conj r (-walk* s (first v))))
+ r)))
+
+ ObjMap
+ (-walk-term [v s] (walk-term-map* v s))
+
+ PersistentHashMap
+ (-walk-term [v s] (walk-term-map* v s))
+
+ PersistentHashSet
+ (-walk-term [v s]
+ (loop [v v r {}]
+ (if (seq v)
+ (recur (next v) (conj r (-walk* s (first v))))
+ r))))
+
+;; =============================================================================
+;; Occurs Check Term
+
+(extend-protocol IOccursCheckTerm
+ nil
+ (-occurs-check-term [v x s] false)
+
+ default
+ (-occurs-check-term [v x s]
+ (if (sequential? v)
+ (loop [v v x x s s]
+ (if (seq v)
+ (or (-occurs-check s x (first v))
+ (recur (next v) x s))
+ false))
+ false)))
+
+;; =============================================================================
+;; Goals and Goal Constructors
+
+(extend-type default
+ ITake
+ (-take* [this] this))
+
+;; TODO: Choice always holds a as a list, can we just remove that?
+
+(declare Inc)
+
+(deftype Choice [a f]
+ IBind
+ (-bind [this g]
+ (-mplus (g a) (-inc (-bind f g))))
+ IMPlus
+ (-mplus [this fp]
+ (Choice. a (-inc (-mplus (fp) f))))
+ ITake
+ (-take* [this]
+ (lazy-seq (cons (first a) (lazy-seq (-take* f))))))
+
+(defn choice [a f]
+ (Choice. a f))
+
+;; -----------------------------------------------------------------------------
+;; MZero
+
+(extend-protocol IBind
+ nil
+ (-bind [_ g] nil))
+
+(extend-protocol IMPlus
+ nil
+ (-mplus [_ b] b))
+
+(extend-protocol ITake
+ nil
+ (-take* [_] '()))
+
+;; -----------------------------------------------------------------------------
+;; Unit
+
+(extend-type default
+ IMPlus
+ (-mplus [this f]
+ (Choice. this f)))
+
+;; -----------------------------------------------------------------------------
+;; Inc
+
+(deftype Inc [f]
+ IFn
+ (-invoke [_] (f))
+ IBind
+ (-bind [this g]
+ (-inc (-bind (f) g)))
+ IMPlus
+ (-mplus [this fp]
+ (-inc (-mplus (fp) this)))
+ ITake
+ (-take* [this] (lazy-seq (-take* (f)))))
+
+;; =============================================================================
+;; Syntax
+
+(defn succeed
+ "A goal that always succeeds."
+ [a] a)
+
+(defn fail
+ "A goal that always fails."
+ [a] nil)
+
+(def s# succeed)
+
+(def u# fail)
+
+;; =============================================================================
+;; conda (soft-cut), condu (committed-choice)
+
+(defprotocol IIfA
+ (-ifa [b gs c]))
+
+(defprotocol IIfU
+ (-ifu [b gs c]))
+
+(extend-protocol IIfA
+ nil
+ (-ifa [b gs c]
+ (when c
+ (force c))))
+
+(extend-protocol IIfU
+ nil
+ (-ifu [b gs c]
+ (when c
+ (force c))))
+
+(extend-type Substitutions
+ IIfA
+ (-ifa [b gs c]
+ (loop [b b [g0 & gr] gs]
+ (if g0
+ (when-let [b (g0 b)]
+ (recur b gr))
+ b))))
+
+(extend-type Substitutions
+ IIfU
+ (-ifu [b gs c]
+ (loop [b b [g0 & gr] gs]
+ (if g0
+ (when-let [b (g0 b)]
+ (recur b gr))
+ b))))
+
+(extend-type Inc
+ IIfA
+ (-ifa [b gs c]
+ (-inc (-ifa (b) gs c)))
+ IIfU
+ (-ifu [b gs c]
+ (-inc (-ifu (b) gs c))))
+
+(extend-protocol IIfA
+ Choice
+ (-ifa [b gs c]
+ (reduce -bind b gs)))
+
+;; TODO: Choice always holds a as a list, can we just remove that?
+(extend-protocol IIfU
+ Choice
+ (-ifu [b gs c]
+ (reduce -bind (.-a b) gs)))
+
+;; =============================================================================
+;; Useful goals
+
+(defn nilo
+ "A relation where a is nil"
+ [a]
+ (m/== nil a))
+
+(defn emptyo
+ "A relation where a is the empty list"
+ [a]
+ (m/== '() a))
+
+(defn conso
+ "A relation where l is a collection, such that a is the first of l
+ and d is the rest of l"
+ [a d l]
+ (m/== (lcons a d) l))
+
+(defn firsto
+ "A relation where l is a collection, such that a is the first of l"
+ [l a]
+ (fresh [d]
+ (conso a d l)))
+
+(defn resto
+ "A relation where l is a collection, such that d is the rest of l"
+ [l d]
+ (fresh [a]
+ (m/== (lcons a d) l)))
+
+;; ==============================================================================
+;; More convenient goals
+
+(defne membero
+ "A relation where l is a collection, such that l contains x"
+ [x l]
+ ([_ [x . tail]])
+ ([_ [head . tail]]
+ (membero x tail)))
+
+(defne appendo
+ "A relation where x, y, and z are proper collections,
+ such that z is x appended to y"
+ [x y z]
+ ([() _ y])
+ ([[a . d] _ [a . r]] (appendo d y r)))
+
+;; TODO: change to lazy-seq
+(defn prefix [s <s]
+ (if (= s <s)
+ ()
+ (conj (prefix (rest s) <s) (first s))))
+
+;; ==============================================================================
+;; partial-maps
+
+(defprotocol IUnifyWithPMap
+ (unify-with-pmap [pmap u s]))
+
+(defrecord PMap []
+ IUnifyWithMap
+ (-unify-with-map [v u s]
+ (loop [ks (keys v) s s]
+ (if (seq ks)
+ (let [kf (first ks)
+ uf (get u kf ::not-found)]
+ (if (= uf ::not-found)
+ nil
+ (if-let [s (-unify s (get v kf) uf)]
+ (recur (next ks) s)
+ nil)))
+ s)))
+
+ IUnifyWithPMap
+ (unify-with-pmap [v u s]
+ (-unify-with-map v u s))
+
+ IUnifyTerms
+ (-unify-terms [u v s]
+ (unify-with-pmap v u s))
+
+ IUnifyWithLVar
+ (-unify-with-lvar [v u s]
+ (-ext-no-check s u v))
+
+ IWalkTerm
+ (-walk-term [v s]
+ (walk-term-map* v s)))
+
+(extend-protocol IUnifyWithPMap
+ nil
+ (unify-with-pmap [v u s] nil)
+
+ js/Object
+ (unify-with-pmap [v u s] nil)
+
+ cljs.core.logic.LVar
+ (unify-with-pmap [v u s]
+ (-ext s v u))
+
+ ObjMap
+ (unify-with-pmap [v u s]
+ (-unify-with-map u v s))
+
+ PersistentArrayMap
+ (unify-with-pmap [v u s]
+ (-unify-with-map u v s))
+
+ PersistentHashMap
+ (unify-with-pmap [v u s]
+ (-unify-with-map u v s)))
+
+(defn partial-map
+ "Given map m, returns partial map that unifies with maps even if it doesn't share all of the keys of that map.
+ Only the keys of the partial map will be unified:
+
+ (m/run* [q]
+ (m/fresh [pm x]
+ (m/== pm (partial-map {:a x}))
+ (m/== pm {:a 1 :b 2})
+ (m/== pm q)))
+ ;;=> ({:a 1})"
+ [m]
+ (map->PMap m))
+
+;; =============================================================================
+;; Easy Unification
+
+(defn- lvarq-sym? [s]
+ (and (symbol? s) (= (first (str s)) \?)))
+
+(defn- proc-lvar [lvar-expr store]
+ (let [v (if-let [u (@store lvar-expr)]
+ u
+ (lvar lvar-expr))]
+ (swap! store conj [lvar-expr v])
+ v))
+
+(defn- lcons-expr? [expr]
+ (and (seq? expr) (some '#{.} (set expr))))
+
+(declare prep*)
+
+(defn- replace-lvar [store]
+ (fn [expr]
+ (if (lvarq-sym? expr)
+ (proc-lvar expr store)
+ (if (lcons-expr? expr)
+ (prep* expr store)
+ expr))))
+
+(defn- prep*
+ ([expr store] (prep* expr store false false))
+ ([expr store lcons?] (prep* expr store lcons? false))
+ ([expr store lcons? last?]
+ (let [expr (if (and last? (seq expr))
+ (first expr)
+ expr)]
+ (cond
+ (lvarq-sym? expr) (proc-lvar expr store)
+ (seq? expr) (if (or lcons? (lcons-expr? expr))
+ (let [[f & n] expr
+ skip (= f '.)
+ tail (prep* n store lcons? skip)]
+ (if skip
+ tail
+ (lcons (prep* f store) tail)))
+ (postwalk (replace-lvar store) expr))
+ :else expr))))
+
+(defn prep
+ "Prep a quoted expression. All symbols preceded by ? will
+ be replaced with logic vars."
+ [expr]
+ (let [lvars (atom {})
+ prepped (if (lcons-expr? expr)
+ (prep* expr lvars true)
+ (postwalk (replace-lvar lvars) expr))]
+ (with-meta prepped {:lvars @lvars})))
+
+(defn unify [s u v]
+ (if (identical? u v)
+ s
+ (let [u (-walk s u)
+ v (-walk s v)]
+ (if (identical? u v)
+ s
+ (-unify-terms u v s)))))
+
+(defn unifier*
+ "Unify the terms u and w."
+ ([u w]
+ (first
+ (m/run* [q]
+ (== u w)
+ (== u q))))
+ ([u w & ts]
+ (apply unifier* (unifier* u w) ts)))
+
+(defn binding-map*
+ "Return the binding map that unifies terms u and w.
+ u and w should prepped terms."
+ ([u w]
+ (let [lvars (merge (-> u meta :lvars)
+ (-> w meta :lvars))
+ s (unify empty-s u w)]
+ (when s
+ (into {} (map (fn [[k v]]
+ [k (-reify s v)])
+ lvars)))))
+ ([u w & ts]
+ (apply binding-map* (binding-map* u w) ts)))
+
+(defn unifier
+ "Unify the terms u and w. Will prep the terms."
+ ([u w]
+ {:pre [(not (lcons? u))
+ (not (lcons? w))]}
+ (let [up (prep u)
+ wp (prep w)]
+ (unifier* up wp)))
+ ([u w & ts]
+ (apply unifier (unifier u w) ts)))
+
+(defn binding-map
+ "Return the binding map that unifies terms u and w.
+ Will prep the terms."
+ ([u w]
+ {:pre [(not (lcons? u))
+ (not (lcons? w))]}
+ (let [up (prep u)
+ wp (prep w)]
+ (binding-map* up wp)))
+ ([u w & ts]
+ (apply binding-map (binding-map u w) ts)))
+
+
+
View
415 test/typed/test/logic/macros.clj
@@ -0,0 +1,415 @@
+(ns typed.test.logic.macros
+ (:refer-clojure :exclude [==])
+ (:require [clojure.set :as set]))
+
+(def ^{:dynamic true} *locals*)
+
+(defmacro llist
+ "Constructs a sequence from 2 or more arguments, with the last argument as the tail.
+ The tail is improper if the last argument is a logic variable."
+ ([f s] `(cljs.core.logic/lcons ~f ~s))
+ ([f s & rest] `(cljs.core.logic/lcons ~f (llist ~s ~@rest))))
+
+(defn bind-conde-clause [a]
+ (fn [g-rest]
+ `(bind* ~a ~@g-rest)))
+
+(defn bind-conde-clauses [a clauses]
+ (map (bind-conde-clause a) clauses))
+
+(defn lvar-bind [sym]
+ ((juxt identity
+ (fn [s] `(cljs.core.logic/lvar '~s))) sym))
+
+(defn lvar-binds [syms]
+ (mapcat lvar-bind syms))
+
+(defmacro bind*
+ ([a g] `(cljs.core.logic/-bind ~a ~g))
+ ([a g & g-rest]
+ `(bind* (cljs.core.logic/-bind ~a ~g) ~@g-rest)))
+
+(defmacro mplus*
+ ([e] e)
+ ([e & e-rest]
+ `(cljs.core.logic/-mplus ~e (-inc (mplus* ~@e-rest)))))
+
+(defmacro -inc [& rest]
+ `(cljs.core.logic/Inc. (fn [] ~@rest)))
+
+(defmacro ==
+ "A goal that attempts to unify terms u and v."
+ [u v]
+ `(fn [a#]
+ (if-let [b# (cljs.core.logic/-unify a# ~u ~v)]
+ b# nil)))
+
+(defmacro conde
+ "Logical disjunction of the clauses. The first goal in
+ a clause is considered the head of that clause. Interleaves the
+ execution of the clauses."
+ [& clauses]
+ (let [a (gensym "a")]
+ `(fn [~a]
+ (-inc
+ (mplus* ~@(bind-conde-clauses a clauses))))))
+
+(defmacro fresh
+ "Creates fresh variables. Goals occuring within form a logical
+ conjunction."
+ [[& lvars] & goals]
+ `(fn [a#]
+ (-inc
+ (let [~@(lvar-binds lvars)]
+ (bind* a# ~@goals)))))
+
+(defmacro solve [& [n [x] & goals]]
+ `(let [xs# (cljs.core.logic/-take* (-inc
+ ((fresh [~x] ~@goals
+ (fn [a#]
+ (cons (cljs.core.logic/-reify a# ~x) '()))) ;; TODO: do we need this?
+ cljs.core.logic/empty-s)))]
+ (if ~n
+ (take ~n xs#)
+ xs#)))
+
+(defmacro run
+ "Executes goals until a maximum of n results are found."
+ [n & goals]
+ `(doall (solve ~n ~@goals)))
+
+(defmacro run*
+ "Executes goals until results are exhausted."
+ [& goals]
+ `(run false ~@goals))
+
+(defmacro run-nc
+ "Executes goals until a maximum of n results are found. Does not occurs-check."
+ [& [n & goals]]
+ `(binding [*occurs-check* false]
+ (run ~n ~@goals)))
+
+(defmacro run-nc*
+ "Executes goals until results are exhausted. Does not occurs-check."
+ [& goals]
+ `(run-nc false ~@goals))
+
+(defmacro lazy-run
+ "Lazily executes goals until a maximum of n results are found."
+ [& [n & goals]]
+ `(solve ~n ~@goals))
+
+(defmacro lazy-run*
+ "Lazily executes goals until results are exhausted."
+ [& goals]
+ `(solve false ~@goals))
+
+(defmacro all
+ "Like fresh but does does not create logic variables."
+ ([] `cljs.core.logic/s#)
+ ([& goals] `(fn [a#] (bind* a# ~@goals))))
+
+;; =============================================================================
+;; Debugging
+
+(defmacro log [& s]
+ "Goal for println"
+ `(fn [a#]
+ (println ~@s)
+ a#))
+
+(defmacro trace-s []
+ "Goal that prints the current substitution"
+ `(fn [a#]
+ (println (str a#))
+ a#))
+
+(defn trace-lvar [a lvar]
+ `(println (format "%5s = %s" (str '~lvar) (-reify ~a ~lvar))))
+
+(defmacro trace-lvars
+ "Goal for tracing the values of logic variables."
+ [title & lvars]
+ (let [a (gensym "a")]
+ `(fn [~a]
+ (println ~title)
+ ~@(map (partial trace-lvar a) lvars)
+ ~a)))
+
+;; =============================================================================
+;; Non-relational goals
+
+;; =============================================================================
+;; project
+
+(defn project-binding [s]
+ (fn [var]
+ `(~var (cljs.core.logic/-walk* ~s ~var))))
+
+(defn project-bindings [vars s]
+ (reduce concat (map (project-binding s) vars)))
+
+(defmacro project
+ "Extract the values bound to the specified logic vars. Non-relational."
+ [[& vars] & goals]
+ (let [a (gensym "a")]
+ `(fn [~a]
+ (let [~@(project-bindings vars a)]
+ ((fresh []
+ ~@goals) ~a)))))
+
+(defmacro pred
+ "Check a predicate against the value logic var. Non-relational."
+ [v f]
+ `(project [~v]
+ (== (~f ~v) true)))
+
+(defmacro is
+ "Set the value of a var to value of another var with the operation
+ applied. Non-relational."
+ [u v op]
+ `(project [~v]
+ (== ~u (~op ~v))))
+
+;; =============================================================================
+;; conda (soft-cut), condu (committed-choice)
+;;
+;; conda once a line succeeds no others are tried
+;; condu a line can succeed only one time
+
+;; TODO : if -> when
+
+(defmacro ifa*
+ ([])
+ ([[e & gs] & grest]
+ `(cljs.core.logic/-ifa ~e [~@gs]
+ ~(if (seq grest)
+ `(delay (ifa* ~@grest))
+ nil))))
+
+(defmacro ifu*
+ ([])
+ ([[e & gs] & grest]
+ `(cljs.core.logic/-ifu ~e [~@gs]
+ ~(if (seq grest)
+ `(delay (ifu* ~@grest))
+ nil))))
+
+(defn cond-clauses [a]
+ (fn [goals]
+ `((~(first goals) ~a) ~@(rest goals))))
+
+(defmacro conda
+ "Soft cut. Once the head of a clause has succeeded
+ all other clauses will be ignored. Non-relational."
+ [& clauses]
+ (let [a (gensym "a")]
+ `(fn [~a]
+ (ifa* ~@(map (cond-clauses a) clauses)))))
+
+(defmacro condu
+ "Committed choice. Once the head (first goal) of a clause
+ has succeeded, remaining goals of the clause will only
+ be run once. Non-relational."
+ [& clauses]
+ (let [a (gensym "a")]
+ `(fn [~a]
+ (ifu* ~@(map (cond-clauses a) clauses)))))
+
+;; =============================================================================
+;; lvar nonlvar
+
+;; =============================================================================
+;; Pattern matching
+
+(defn warn [& msg]
+ (binding [*out* *err*]
+ (apply println "WARNING:" msg)))
+
+(declare p->term)
+
+(defn lcons-p? [p]
+ (and (coll? p)
+ (not (nil? (some '#{.} p)))))
+
+(defn p->llist [p]
+ `(llist
+ ~@(map p->term
+ (remove #(contains? '#{.} %) p))))
+
+(defn- p->term [p]
+ (cond
+ (= p '_) `(cljs.core.logic/lvar)
+ (lcons-p? p) (p->llist p)
+ (and (coll? p) (not= (first p) 'quote))
+ (cond
+ ;; support simple expressions
+ (list? p) p
+ ;; preserve original collection type
+ :else (let [ps (map p->term p)]
+ (cond
+ (instance? clojure.lang.MapEntry p) (into [] ps)
+ :else (into (empty p) ps))))
+ :else p))
+
+(defn lvar-sym? [s]
+ (and (symbol? s)
+ (not= s '.)
+ (not (contains? *locals* s))))
+
+(defn extract-vars
+ ([p]
+ (set (cond
+ (lvar-sym? p) [p]
+ (coll? p) (let [p (if (seq? p) (rest p) p)]
+ (filter lvar-sym? (flatten p)))
+ :else nil)))
+ ([p seen]
+ (set/difference (extract-vars p) (set seen))))
+
+(defn fresh-expr? [cs]
+ (= (first cs) `fresh))
+
+(defn ex
+ ([vs t a]
+ `(fresh [~@vs]
+ (== ~t ~a)))
+ ([vs t a exprs]
+ (if (fresh-expr? exprs)
+ `(fresh [~@vs]
+ (== ~t ~a)
+ ~exprs)
+ `(fresh [~@vs]
+ (== ~t ~a)
+ ~@exprs))))
+
+(defn ex* [[[p a :as pa] & par] exprs seen]
+ (let [t (p->term p)
+ vs (extract-vars p seen)
+ seen (reduce conj seen vs)]
+ (cond
+ (nil? pa) exprs
+ (= p '_) (ex* par exprs seen)
+ (empty? par) (if exprs
+ (ex vs t a exprs)
+ (ex vs t a))
+ :else (let [r (ex* par exprs seen)]
+ (if r
+ (ex vs t a r)
+ (ex vs t a))))))
+
+(defn all-blank? [p]
+ (every? #(= % '_) p))
+
+(defn handle-clause [as]
+ (when-not (vector? as)
+ (throw (Exception. (str "Expecting vector of arguments, instead " as))))
+ (fn [[p & exprs]]
+ (when-not (vector? p)
+ (throw (Exception. (str "Expecting vector of matches, instead " p))))
+ (when-not (= (count p) (count as))
+ (warn "Differing number of matches. Matching" p "against" as))
+ (let [pas (partition 2 (interleave p as))
+ r (ex* pas exprs #{})]
+ (if (all-blank? p)
+ r
+ (list r)))))
+
+(defn handle-clauses [t as cs]
+ `(~t
+ ~@(doall (map (handle-clause as) cs))))
+
+;; name-with-attributes by Konrad Hinsen, from clojure.contrib.def
+(defn name-with-attributes
+ "To be used in macro definitions.
+ Handles optional docstrings and attribute maps for a name to be defined
+ in a list of macro arguments. If the first macro argument is a string
+ it is added as a docstring to name and removed from the macro argument
+ list. If afterwards the first macro argument is a map, its entries are
+ added to the name's metadata map and the map is removed from the
+ macro argument list. The return value is a vector containing the name
+ with its extended metadata map and the list of unprocessed macro
+ arguments."
+ [name macro-args]
+ (let [[docstring macro-args] (if (string? (first macro-args))
+ [(first macro-args) (next macro-args)]
+ [nil macro-args])
+ [attr macro-args] (if (map? (first macro-args))
+ [(first macro-args) (next macro-args)]
+ [{} macro-args])
+ attr (if docstring
+ (assoc attr :doc docstring)
+ attr)
+ attr (if (meta name)
+ (conj (meta name) attr)
+ attr)]
+ [(with-meta name attr) macro-args]))
+
+(defmacro lvaro
+ "Goal to test whether a logic var is ground. Non-relational."
+ [v]
+ `(fn [a#]
+ (if (cljs.core.logic/lvar? (cljs.core.logic/-walk a# ~v))
+ a# nil)))
+
+(defmacro nonlvaro
+ "Goal to test whether a logic var is ground. Non-relational."
+ [v]
+ `(fn [a#]
+ (if (not (cljs.core.logic/lvar? (cljs.core.logic/walk a# ~v)))
+ a# nil)))
+
+(defn env-locals [& syms]
+ (disj (set (apply concat syms)) '_))
+
+(defmacro defnm [t n & rest]
+ (let [[n [as & cs]] (name-with-attributes n rest)]
+ (binding [*locals* (env-locals as (-> &env :locals keys))]
+ (if-let [tabled? (-> n meta :tabled)]
+ `(def ~n (tabled [~@as] ~(handle-clauses t as cs)))
+ `(defn ~n [~@as] ~(handle-clauses t as cs))))))
+
+;; =============================================================================
+;; Goal sugar syntax
+
+(defmacro defne
+ "Define a goal fn. Supports pattern matching. All
+ patterns will be tried. See conde."
+ [& rest]
+ `(defnm conde ~@rest))
+
+(defmacro matche
+ "Pattern matching macro. All patterns will be tried.
+ See conde."
+ [xs & cs]
+ (binding [*locals* (env-locals xs (-> &env :locals keys))]
+ (handle-clauses `conde xs cs)))
+
+;; -----------------------------------------------------------------------------
+;; defnu, defna, matcha, matchu
+
+;; TODO: we need to rethink defna and defnu, the unification comes first
+;; the *question* should come first
+
+(defmacro defna
+ "Define a soft cut goal. See conda."
+ [& rest]
+ `(defnm conda ~@rest))
+
+(defmacro defnu
+ "Define a committed choice goal. See condu."
+ [& rest]
+ `(defnm condu ~@rest))
+
+(defmacro matcha
+ "Define a soft cut pattern match. See conda."
+ [xs & cs]
+ (binding [*locals* (env-locals xs (-> &env :locals keys))]
+ (handle-clauses `conda xs cs)))
+
+(defmacro matchu
+ "Define a committed choice goal. See condu."
+ [xs & cs]
+ (binding [*locals* (env-locals xs (-> &env :locals keys))]
+ (handle-clauses `condu xs cs)))
+
View
2  test/typed/test/monads.clj
@@ -1075,7 +1075,7 @@
(ann afun (All [x y] [(U x nil) [x -> (U nil y)] -> (U nil y)]))
(ann bfun [Symbol -> (U nil Symbol)])
(declare afun bfun)
-(tc-ignore (cf (afun 'a bfun)))
+#_(tc-ignore (cf (afun 'a bfun)))
;TODO these are test cases
;

0 comments on commit e302b4f

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