(ns logic.y | |
(:refer-clojure :exclude [== reify inc]) | |
(:use [clojure.core.logic minikanren prelude | |
nonrel match])) | |
(defna findo [x l o] | |
([_ [[?y :- o] . _] _] | |
(project [x ?y] (== (= x ?y) true))) | |
([_ [_ . ?c] _] (findo x ?c o))) | |
(defn typedo [c x t] | |
(conda | |
((lvaro x) (findo x c t)) | |
((matche [c x t] | |
([_ [[?x] :>> ?a] [?s :> ?t]] | |
(exist [l] | |
(conso [?x :- ?s] c l) | |
(typedo l ?a ?t))) | |
([_ [:apply ?a ?b] _] | |
(exist [s o] | |
(typedo c ?a [s :> t]) | |
(typedo c ?b s))))))) | |
(comment | |
;; ([_.0 :> _.1]) | |
(run* [q] | |
(exist [f g a b t] | |
(typedo [[f :- a] [g :- b]] [:apply f g] t) | |
(== q a))) | |
;; ([:int :> _.0]) | |
(run* [q] | |
(exist [f g a t] | |
(typedo [[f :- a] [g :- :int]] [:apply f g] t) | |
(== q a))) | |
;; (:int) | |
(run* [q] | |
(exist [f g a t] | |
(typedo [[f :- [:int :> :float]] [g :- a]] | |
[:apply f g] t) | |
(== q a))) | |
;; () | |
(run* [t] | |
(exist [f a b] | |
(typedo [f :- a] [:apply f f] t))) | |
;; ([_.0 :> [[_.0 :> _.1] :> _.1]]) | |
(run* [t] | |
(exist [x y] | |
(typedo [] | |
[[x] :>> [[y] :>> [:apply y x]]] t))) | |
;; Prolog taken from here http://bit.ly/dC0xJm | |
;; find(X,[Y-S|_],S) :- X==Y, !. | |
;; find(X,[_|C],S) :- find(X,C,S). | |
;; typed(C,X,T) :- var(X), !, find(X,C,S), | |
;; unify_with_occurs_check(S,T). | |
;; typed(C,[X]>>A,S>T) :- typed([X-S|C],A,T). | |
;; typed(C,apply(A,B),R) :- typed(C,A,S>R), typed(C,B,T), | |
;; unify_with_occurs_check(S,T). | |
;; ?- typed([F-A,G-B],apply(F,G),C). | |
;; A = B > C | |
;; ?- typed([F-A],apply(F,F),B). | |
;; No | |
;; ?- typed([],[X]>>([Y]>>apply(Y,X)),T). | |
;; T = _T > ((_T > _Q) > _Q) | |
) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment