Implementation of µKanren in Idris

mukanren.idr

data Value = Null
           | Var Nat
           | Pair Value Value
           | Num Int

data Substitution = Nil
                  | (::) (Nat, Value) Substitution

State : Type
State = (Substitution, Nat)

data Stream = MZero 
            | Cons State Stream
            | Zzz (Lazy Stream)

unit : State -> Stream
unit st = Cons st MZero

Goal : Type
Goal = State -> Stream

lookup : Nat -> Substitution -> Maybe Value
lookup _ Nil = Nothing
lookup x ((y, v) :: ss) = if x == y then (Just v) else lookup x ss

walk : Value -> Substitution -> Value
walk (Var v) s = case (lookup v s) of
                   Nothing => (Var v)
                   Just p => walk p s
walk u s = u

ext_s : Nat -> Value -> Substitution -> Substitution
ext_s c v = (::) (c, v)

mutual
    unify : Value -> Value -> Substitution -> Maybe Substitution
    unify u v s = let u = (walk u s)
                      v = (walk v s)
                  in unify' u v s

    unify' : Value -> Value -> Substitution -> Maybe Substitution
    unify' Null Null s = Just s
    unify' (Num a) (Num b) s = if a == b then Just s else Nothing
    unify' (Var c) (Var d) s = if c == d then Just s else Just (ext_s c (Var d) s)
    unify' (Var c) v s = Just (ext_s c v s)
    unify' u (Var d) s = Just (ext_s d u s)
    unify' (Pair u1 u2) (Pair v1 v2) s = case (unify u1 v1 s) of
                                        Nothing => Nothing
                                        Just s' => unify u2 v2 s'
    unify' _ _ _ = Nothing

eql : Value -> Value -> Goal
eql u v (s,c) = case (unify u v s) of
                  Nothing => MZero
                  Just s' => unit (s',c)

call_fresh  : (Value -> Goal) -> Goal
call_fresh f (s, c)= f (Var c) (s, S(c))

mplus : Stream -> Stream -> Stream
mplus MZero ys = ys
mplus (Cons x xs) ys = Cons x (mplus xs ys)
mplus (Zzz xs) ys = Zzz (mplus ys xs)

bind : Stream -> Goal -> Stream
bind MZero _ = MZero
bind (Cons x xs) g = mplus (g x) (bind xs g)
bind (Zzz xs) g = Zzz (bind xs g)
                  
disj : Goal -> Goal -> Goal
disj g1 g2 st = mplus (g1 st) (g2 st)

conj : Goal -> Goal -> Goal
conj g1 g2 st = bind (g1 st) g2



-------------------

fives : Value -> Goal
fives x = disj (eql x (Num 5)) (\sc => Zzz ((fives x) sc))