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

rntz

#lang racket

(require racket/hash) ;; hash-union

;; UNIFICATION VAR
;; symbol beginning with ?
(define (var? x) (and (symbol? x) (string-prefix? (symbol->string x) "?")))
(define/contract (var x) (-> symbol? var?)
  (string->symbol (format "?~a" x)))
(define/contract (var-name x) (-> var? symbol?)

rntz

#lang racket

(struct rig (zero? sum product) #:prefab)
(define the-rig (make-parameter #f))
(define (the-rig-zero? x) ((rig-zero? (the-rig)) x))
(define (the-rig-sum args) ((rig-sum (the-rig)) args))
(define (the-rig-product args) ((rig-product (the-rig)) args))
(define (the-rig-+ . args) (the-rig-sum args))
(define (the-rig-* . args) (the-rig-product args))
(define (the-rig-zero) (the-rig-+))

rntz

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
module IncrementalStreams where

import Prelude hiding (init)
import Data.Foldable (toList)
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.Map as Map
import Data.Map (Map)

rntz

{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE ScopedTypeVariables #-}
module IncrementalStreams where

import Prelude hiding (init)
import qualified Data.Set as Set
import Data.Set (Set)
import qualified Data.Map as Map
import Data.Map (Map)

rntz

record Preorder (A : Set) : Set1 where
  _≤_   : A → A → Set
  refl  : {a} → a ≤ a
  trans : {a b c} → a ≤ b → b ≤ c → a ≤ c

record is-lub {A} (P : Preorder A) {I} (a : I → A) (⋁a : A) : Set where
  bound : (i : I) → a i ≤ ⋁a
  least : (b : A) → ((i : I) → a i ≤ b) → ⋁a ≤ b

module _ {A B} (P : Preorder A) (Q : Preorder B) (f : A → B) where