Skip to content

Instantly share code, notes, and snippets.

@SRechenberger
Last active March 27, 2024 10:57
Show Gist options
  • Save SRechenberger/d5e1eb875ae72ce5cafe6ea1c5b3ee38 to your computer and use it in GitHub Desktop.
Save SRechenberger/d5e1eb875ae72ce5cafe6ea1c5b3ee38 to your computer and use it in GitHub Desktop.
FreeCHR instances
import Data.List hiding (nub)
import Prelude hiding (gcd)
-- FreeCHR Instance
newtype SolverStep c = SolverStep { runSolverStep :: [c] -> [c] }
match :: [a -> Bool] -> [a] -> [[a]]
match ps as = [ as''
| as' <- subsequences as, length as' == length ps
, as'' <- permutations as'
, and (zipWith ($) ps as'')
]
rule :: Eq c => [c -> Bool] -> [c -> Bool] -> ([c] -> Bool) -> ([c] -> [c])
-> SolverStep c
rule kept removed guard body = SolverStep
{ runSolverStep = \state ->
let matching = find guard (match (kept ++ removed) state)
in case matching of
Just ms -> (state \\ drop (length kept) ms) ++ body ms
_ -> state
}
instance Eq c => Semigroup (SolverStep c) where
(<>) :: Eq c => SolverStep c -> SolverStep c -> SolverStep c
solver <> solver' = SolverStep
{ runSolverStep = \state ->
let state' = runSolverStep solver state
in if state == state'
then runSolverStep solver' state
else state'
}
run :: Eq c => SolverStep c -> [c] -> [c]
run solver query
| result == query = result
| otherwise = run solver result
where
result = runSolverStep solver query
-- Example Programs
gcd :: Integral a => SolverStep a
gcd = rule [] [(<= 0)]
(const True)
(const []) <>
rule [(> 0)] [(> 0)]
(\[n, m] -> n <= m)
(\[n, m] -> [m - n])
fib :: SolverStep (Int, Int, Int)
fib = rule [] [\(n, _, _) -> n > 0] (const True) (\[(n, a, b)] -> [(n-1, b, a+b)])
nub :: Eq a => SolverStep a
nub = rule [const True] [const True] (\[a, b] -> a == b) (const [])
alldifferent :: Eq a => SolverStep a
alldifferent = rule [const True, const True] []
(\[x, y] -> x == y) (const $ error "False")
from itertools import permutations
## FreeCHR instance
def match(pattern, cs):
return (perm
for perm in permutations(cs, len(pattern))
if all(p(c) for p, c in zip(pattern, perm))
)
def rule(k, r, g, b):
def solver(state):
matching = next(
(matching for matching in match(k+r, state) if g(*matching)),
None)
if not matching:
return state
state_copy = state.copy()
for c in matching[len(k):]:
state_copy.remove(c)
return b(*matching) + state_copy
return solver
def compose(*solvers):
def solver(constraints):
result = constraints
for s in solvers:
result = s(constraints)
if result != constraints:
break
return result
return solver
def run(solver):
def solve(*query):
state = list(query)
result = solver(state)
while True:
if result == state:
break
state = result
result = solver(result)
return result
return solve
## Example Programs
gcd = compose(
rule([], [lambda n: isinstance(n, int)],
lambda n: n <= 0,
lambda _: []),
rule([lambda n: isinstance(n, int)], [lambda m: isinstance(m, int)],
lambda n, m: 0 < n <= m,
lambda n, m: [m-n])
)
fib = rule([], [lambda t: isinstance(t, tuple) and len(t) == 3 and all(isinstance(i, int) for i in t)],
lambda t: t[0] > 0,
lambda t: [(t[0]-1, t[2], t[1]+t[2])]
)
nub = rule([lambda a: True], [lambda b: True], lambda a, b: a == b, lambda a, b: [])
def false(*args):
raise Exception(False)
all_different = rule(
[lambda a: True, lambda b: True], [],
lambda a, b: a == b,
false
)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment