rntz

# based on "closed form formula" for the nth prime, defined by
# "On Formulae for the nth Prime Number", C. P. Willans
# (https://www.jstor.org/stable/3611701)
# 
# which I discovered through a stackexchange question at
# https://hsm.stackexchange.com/questions/13353/who-discovered-this-closed-form-formula-for-the-n-th-prime-number
from math import ceil, cos, factorial as fac, floor, pi, sqrt

# The direct definition. This produces incorrect answers because of floating
# point inaccuracy, and raises OverflowError for n>7. Let's fix this.

rntz

#!/usr/bin/env runhaskell
{-# OPTIONS -Wno-x-partial #-}
import Data.List (inits, transpose, intercalate)
import Data.Ratio
import System.Environment (getArgs)
import System.Exit (die)
import Text.Printf

main :: IO ()
main = do

rntz

import Debug.Trace
import Data.List

-- galloping search.
search :: (Int -> Bool) -> Int -> Int -> Int
search test lo hi | lo == hi = hi
                  | test lo  = lo
                  | otherwise = go True lo 1 where
    go accel i 0 = i + 1
    go accel i step

rntz

// ---------- SEEKABLE ITERATORS AND THEIR POSITIONS ----------
// Positions of an iterator:
// Yield(k, Some(v)) = we found a key-value pair (k, v)
// Yield(k, None)    = all remaining keys are >= k
// Empty             = there are no more key-value pairs
enum Position<S: Seek + ?Sized> {
    Yield(S::Key, Option<S::Value>),
    Empty,
}
use Position::*;

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))