public
Last active

type-inf.clj

  • Download Gist
gistfile1.clj
Clojure
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72
(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)
)

Please sign in to comment on this gist.

Something went wrong with that request. Please try again.