implementation of muKanren's search strategy in Agda with --guarded

GuardedKanren.agda

{-# OPTIONS --guarded #-}
module GuardedKanren where

open import Agda.Primitive using (Level)
private variable
  l : Level
  A B : Set l

data Bool : Set where true false : Bool
if_then_else_ : ∀{A : Set} → Bool → A → A → A
if true then x else y = x
if false then x else y = y

data _×_ (A B : Set) : Set where
  _,_ : A → B → A × B

data _≡_ {A : Set} : A → A → Set where
  refl : ∀{a} → a ≡ a

data _⊎_ (A B : Set) : Set where
  in₁ : A → A ⊎ B
  in₂ : B → A ⊎ B


-- Copied & modified from this example file:
-- https://github.com/agda/agda/blob/172366db528b28fb2eda03c5fc9804f2cdb1be18/test/Succeed/LaterPrims.agda

module Prims where primitive primLockUniv : Set₁
open Prims renaming (primLockUniv to LockU) public
postulate Tick : LockU

▹_ : ∀ {l} → Set l → Set l
▹_ A = (@tick x : Tick) -> A

▸_ : ∀ {l} → ▹ Set l → Set l
▸ A = (@tick x : Tick) → A x

-- does this actually *compute*? Can we make it compute instead of being a postulate?
postulate
  dfix : ∀ {l} {A : Set l} → (▹ A → A) → ▹ A

fix : ∀ {l} {A : Set l} → (▹ A → A) → A
fix f = f (dfix f)

-- If a type includes its own delayed version, we can do "fix" at that type directly.
delayfix : (▹ A → A) → (A → A) → A
delayfix delay f = fix (λ self → f (delay self))


-- Kanren search monad
data Stream (A : Set) : Set where
  nil : Stream A
  cons : A → Stream A → Stream A
  later : ▹ Stream A → Stream A

-- mukanren's mplus; simpler to prove correct?
union : Stream A → Stream A → Stream A
union nil ys = ys
union (cons x xs) ys = cons x (union ys xs)
union (later x) ys = later (λ t → union ys (x t))

-- -- The eager version I prefer; don't delay until you have no work left to do.
-- union : Stream A → Stream A → Stream A
-- union nil ys = ys
-- union xs nil = xs
-- union (cons x xs) ys = cons x (union xs ys)
-- union xs (cons y ys) = cons y (union xs ys)
-- union (later x) (later y) = later (λ t → union (x t) (y t))


bind : Stream A → (A → Stream B) → Stream B
bind nil f = nil
bind (cons x s) f = union (f x) (bind s f)
bind (later x) f = later λ t → bind (x t) f


-- Ok, let's do some proof search! NB. This is not a kanren yet since we don't have
-- existential variables or unification.
data Node : Set where node-x node-y node-z : Node
node-eq : Node → Node → Bool
node-eq node-x = λ { node-x → true ; _ → false }
node-eq node-y = λ { node-y → true ; _ → false }
node-eq node-z = λ { node-z → true ; _ → false }

edge : Stream (Node × Node)
edge = cons (node-x , node-y)
        (cons (node-y , node-z)
         (cons (node-x , node-z) nil))

trans : (A → A → Bool) → Stream (A × A) → Stream (A × A)
trans {A} eq edge = delayfix later f
  where f : Stream (A × A) → Stream (A × A)
        f self = union edge (bind self λ { (y₂ , z) →
                             bind edge λ { (x , y₁) →
                             if eq y₁ y₂ then cons (x , z) nil else nil } } )

reach : Stream (Node × Node)
reach = trans node-eq edge


-- Ok, can we prove something about this?
module Attempt1 where
  -- I want a type of "streams which completely enumerate some type".
  -- To do this I need the type of elements of a stream.
  data _∈_ {A : Set} (a : A) : Stream A → Set where
    ∈car   : ∀{as : Stream A} → a ∈ cons a as
    ∈cdr   : ∀{b bs} → a ∈ bs → a ∈ cons b bs
    ∈later : ∀{as : ▹ Stream A} → ▸ (λ t → a ∈ as t) → a ∈ later as

  -- OH NO, this definition of _∈_ is WRONG.
  -- It allows the stream `never` to contain EVERYTHING!
  -- I'm confident this can be proven using pfix (see the example file).
  -- So what I really need is a way to move back down to a clockless world.
  -- I should email Bob Atkey.
  never : ∀{A} → Stream A
  never = fix later
  ∈-never : ∀{a : A} → a ∈ never
  ∈-never = ∈later (λ t → {!!})

  -- Completeness of union: if it's in as or bs, it's in (union as bs).
  ∈union₁ : ∀{a : A} {as bs} → (a ∈ as) → a ∈ union as bs
  ∈union₂ : ∀{b : A} as → ∀{bs} → (b ∈ bs) → b ∈ union as bs

  ∈union₁ ∈car = ∈car
  ∈union₁ (∈cdr a∈as) = ∈cdr (∈union₂ _ a∈as)
  ∈union₁ (∈later ▸a∈as) = ∈later λ t → ∈union₂ _ (▸a∈as t)

  ∈union₂ nil b∈bs = b∈bs
  ∈union₂ (cons x as) b∈bs = ∈cdr (∈union₁ b∈bs)
  ∈union₂ (later x) b∈bs = ∈later λ t → ∈union₁ b∈bs

  -- Soundness of union: if it's in (union as bs), it's in as or bs.
  -- Except, shit! We can't decide this up front!
  -- We will need a number of steps depending on the size of the proof of containment!
  union∋ : ∀{a : A} as bs → a ∈ union as bs → (a ∈ as) ⊎ (a ∈ bs)
  union∋ nil bs a∈abs = in₂ a∈abs
  union∋ (cons a as) bs ∈car = in₁ ∈car
  union∋ (cons a as) bs (∈cdr a∈abs) with union∋ bs as a∈abs
  ... | in₁ x = in₂ x
  ... | in₂ x = in₁ (∈cdr x)
  union∋ (later as) bs (∈later a∈abs) = {!!} -- THE PROBLEM