swannodette / gist:997140

Created May 28, 2011


    
    View gist:997140 
  
  
      gistfile1.clj
    
    
        Raw
      
    
    File suppressed. Click to show.
  
  
            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) 
  )