rntz

import bisect
from dataclasses import dataclass

class Bound:
    def to_bound(self): return self
    def __lt__(self, other):
        return self <= other and self != other
    def __le__(self, other):
        if isinstance(self, Init) or isinstance(other, Done): return True
        if isinstance(self, Done) or isinstance(other, Init): return False

rntz

-- A lower bound in a totally ordered key-space k; corresponds to some part of an
-- ordered sequence we can seek forward to.
data Bound k = Init | Atleast !k | Greater !k | Done deriving (Show, Eq)
instance Ord k => Ord (Bound k) where
  Init      <= _         = True
  _         <= Done      = True
  _         <= Init      = False
  Done      <= _         = False
  Atleast x <= Atleast y = x <= y
  Atleast x <= Greater y = x <= y

rntz

-- Sorted, seekable iterators as a coinductive type.
data Seek k v = Seek
  { lagging :: !k
  , leading :: !k
  -- invariant: lagging <= leading
  , value :: v
  -- value must only be accessed when lagging == leading.
  , search :: k -> k -> Maybe (Seek k v)
  -- Let t' = search t lo hi. The pre/post conditions are:
  -- PRE:  lagging t <= lo               && leading t <= hi

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)