rntz

module Kanren where

import Control.Applicative
import Control.Monad
import Data.Monoid
import Data.List (intercalate)

-- The microkanren search monad. The MonadPlus instance for this implements a
-- *complete* search strategy, even over infinite search spaces -- unlike eg the
-- List monad -- AS LONG AS you use `Later` to guard any potentially infinite

rntz

# a simple dependency tracking system
# pull-based, like Make


# ---------- INTERFACE ----------
class MakelikeInterface:
    # A graph is a dictionary mapping keys to (callback, dependencies...)
    # `callback` takes one argument per dependency and returns the computed
    # value.
    #

rntz

(define (treeo x)
  (conde
   ((== x 'n))
   ((fresh (a y z) (== x `(,y ,a ,z)) (into a) (treeo y) (treeo z)))
  ))

(define (lto x y)
  (conde
    ((== x 0) (== y 1))
    ((== x 0) (== y 2))

rntz

type var = string
type term = Var of var
          | Lam of var * term
          | App of term * term
          | Fix of var * term   (* only used for functions *)
          | Lit of int

type value = Int of int
           | Fun of (value -> value)

rntz

import System.Environment (getArgs)

import Control.Monad (guard, forM_)

import System.Random (RandomGen)
import qualified System.Random as Random

import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

rntz

module Main where

import Data.List (minimumBy)
import Data.Ord (comparing)
import Data.Maybe (fromJust)
import Data.Map.Strict (Map)
import qualified Data.Map.Strict as Map

-- Unknown: a list of ((x,y), options) for each cell (x,y).
type Unknown = [((Int, Int), [Int])]

rntz

import copy, random
n = 9
values = list(range(n))

def to_matrix(d):
    return [[d[(x,y)] for y in range(n)] for x in range(n)]

def sudoku():
    known = dict()
    unknown = {(x,y): set(values)

rntz

import copy, random
n = 4
values = list(range(n))

def to_matrix(d):
    return [[d[(x,y)] for y in range(n)] for x in range(n)]

def sudoku():
    known = dict()
    unknown = {(x,y): set(values)

rntz

-- see https://gist.github.com/rntz/c2996e06301d9ae95ee0c7a9b43f5e0d for comparison
module GuardedKanren where

import Control.Monad (liftM2, guard)
import Control.Applicative

data Stream a = Nil | Cons a (Stream a) | Later (Stream a)
                deriving (Show)

instance Functor Stream where

rntz

{-# 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