{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeFamilies #-}

-- | This module implements binary numbers as described in the declarative pearl
-- “Pure, Declarative, and Constructive Arithmetic Relations” by O. Kiselyov
-- /et al/.
--
-- The paper is available at <https://okmij.org/ftp/Prolog/Arithm/arithm.pdf>
-- and the original implementation in Prolog is available at
-- <https://okmij.org/ftp/Prolog/Arithm/pure-bin-arithm.prl>.
module Kanren.Data.Binary (
  Bit (..),
  _O,
  _I,
  _O',
  _I',
  Binary,
  zeroo,
  poso,
  gtlo,
  binaryo,
  addo,
  subo,
  lesso,
  mulo,
  divo,
  logo,
  example,
) where

import Control.DeepSeq (NFData)
import Control.Lens.TH (makePrisms)
import Data.Bifunctor (bimap)
import Data.Function ((&))
import GHC.Generics (Generic)

import Kanren.Core
import Kanren.Goal
import Kanren.LogicalBase
import Kanren.Match
import Kanren.TH

data Bit = O | I deriving (Bit -> Bit -> Bool
(Bit -> Bit -> Bool) -> (Bit -> Bit -> Bool) -> Eq Bit
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Bit -> Bit -> Bool
== :: Bit -> Bit -> Bool
$c/= :: Bit -> Bit -> Bool
/= :: Bit -> Bit -> Bool
Eq, Int -> Bit -> ShowS
[Bit] -> ShowS
Bit -> String
(Int -> Bit -> ShowS)
-> (Bit -> String) -> ([Bit] -> ShowS) -> Show Bit
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Bit -> ShowS
showsPrec :: Int -> Bit -> ShowS
$cshow :: Bit -> String
show :: Bit -> String
$cshowList :: [Bit] -> ShowS
showList :: [Bit] -> ShowS
Show, (forall x. Bit -> Rep Bit x)
-> (forall x. Rep Bit x -> Bit) -> Generic Bit
forall x. Rep Bit x -> Bit
forall x. Bit -> Rep Bit x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. Bit -> Rep Bit x
from :: forall x. Bit -> Rep Bit x
$cto :: forall x. Rep Bit x -> Bit
to :: forall x. Rep Bit x -> Bit
Generic, Bit -> ()
(Bit -> ()) -> NFData Bit
forall a. (a -> ()) -> NFData a
$crnf :: Bit -> ()
rnf :: Bit -> ()
NFData)
instance Logical Bit
makePrisms ''Bit
makeExhaustivePrisms ''Bit

type Binary = [Bit]

instance Num Binary where
  fromInteger :: Integer -> [Bit]
fromInteger Integer
0 = []
  fromInteger Integer
1 = [Bit
I]
  fromInteger Integer
x | Integer
x Integer -> Integer -> Bool
forall a. Ord a => a -> a -> Bool
> Integer
1 = Bit
bit Bit -> [Bit] -> [Bit]
forall a. a -> [a] -> [a]
: Integer -> [Bit]
forall a. Num a => Integer -> a
fromInteger (Integer
x Integer -> Integer -> Integer
forall a. Integral a => a -> a -> a
`div` Integer
2)
   where
    bit :: Bit
bit
      | Integer -> Bool
forall a. Integral a => a -> Bool
even Integer
x = Bit
O
      | Bool
otherwise = Bit
I
  fromInteger Integer
_ = String -> [Bit]
forall a. HasCallStack => String -> a
error String
"Binary numbers cannot be negative"

  + :: [Bit] -> [Bit] -> [Bit]
(+) = [Bit] -> [Bit] -> [Bit]
forall a. HasCallStack => a
undefined
  * :: [Bit] -> [Bit] -> [Bit]
(*) = [Bit] -> [Bit] -> [Bit]
forall a. HasCallStack => a
undefined
  abs :: [Bit] -> [Bit]
abs = [Bit] -> [Bit]
forall a. a -> a
id
  signum :: [Bit] -> [Bit]
signum = [Bit] -> [Bit]
forall a. HasCallStack => a
undefined
  negate :: [Bit] -> [Bit]
negate = [Bit] -> [Bit]
forall a. HasCallStack => a
undefined

-- | Check that the number is zero.
zeroo :: Term Binary -> Goal ()
zeroo :: Term [Bit] -> Goal ()
zeroo Term [Bit]
n = Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0

-- | Check that the number is positive, i.e. greater than zero.
poso :: Term Binary -> Goal ()
poso :: Term [Bit] -> Goal ()
poso Term [Bit]
n = do
  (Term Bit
x, Term [Bit]
xs) <- Goal (Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
  Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
x Term [Bit]
xs)

-- | Check that the number is greater than one (i.e. at least two).
--
-- The naming comes from the paper.
gtlo :: Term Binary -> Goal ()
gtlo :: Term [Bit] -> Goal ()
gtlo Term [Bit]
n = do
  (Term Bit
x, Term Bit
y, Term [Bit]
ys) <- Goal (Term Bit, Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
  Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
x (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
y Term [Bit]
ys)))

{- FOURMOLU_DISABLE -}
-- | Generate valid binary numbers.
binaryo :: Term Binary -> Goal ()
binaryo :: Term [Bit] -> Goal ()
binaryo = Matched (Checked, Checked) [Bit] -> Goal ()
forall m a x. Exhausted m => Matched m a -> Goal x
matche'
  (Matched (Checked, Checked) [Bit] -> Goal ())
-> ((Matched (Checked, Checked) [Bit] -> Goal ())
    -> Matched (Remaining, Checked) [Bit] -> Goal ())
-> Matched (Remaining, Checked) [Bit]
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic [Bit])
  (Remaining, Checked)
  (Checked, Checked)
  ()
  Remaining
  Checked
-> (() -> Goal ())
-> (Matched (Checked, Checked) [Bit] -> Goal ())
-> Matched (Remaining, Checked) [Bit]
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, Checked) (Logic [Bit]))
     (f (Tagged (Checked, Checked) (Logic [Bit])))
p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, Checked) (LogicList Bit))
     (f (Tagged (Checked, Checked) (LogicList Bit)))
forall a logicNil logicCons logicNil' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicNil ()) (f (Tagged logicNil' ()))
-> p (Tagged (logicNil, logicCons) (LogicList a))
     (f (Tagged (logicNil', logicCons) (LogicList a)))
ExhaustivePrism
  (Logic [Bit])
  (Remaining, Checked)
  (Checked, Checked)
  ()
  Remaining
  Checked
_LogicNil' () -> Goal ()
forall a. a -> Goal a
forall (m :: * -> *) a. Monad m => a -> m a
return
  (Matched (Remaining, Checked) [Bit] -> Goal ())
-> ((Matched (Remaining, Checked) [Bit] -> Goal ())
    -> Matched (Remaining, Remaining) [Bit] -> Goal ())
-> Matched (Remaining, Remaining) [Bit]
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic [Bit])
  (Remaining, Remaining)
  (Remaining, Checked)
  (Term Bit, Term [Bit])
  Remaining
  Checked
-> ((Term Bit, Term [Bit]) -> Goal ())
-> (Matched (Remaining, Checked) [Bit] -> Goal ())
-> Matched (Remaining, Remaining) [Bit]
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' p (Tagged Remaining (Term Bit, Term [Bit]))
  (f (Tagged Checked (Term Bit, Term [Bit])))
-> p (Tagged (Remaining, Remaining) (Logic [Bit]))
     (f (Tagged (Remaining, Checked) (Logic [Bit])))
p (Tagged Remaining (Term Bit, Term [Bit]))
  (f (Tagged Checked (Term Bit, Term [Bit])))
-> p (Tagged (Remaining, Remaining) (LogicList Bit))
     (f (Tagged (Remaining, Checked) (LogicList Bit)))
forall a logicNil logicCons logicCons' (p :: * -> * -> *)
       (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged logicCons (Term a, Term [a]))
  (f (Tagged logicCons' (Term a, Term [a])))
-> p (Tagged (logicNil, logicCons) (LogicList a))
     (f (Tagged (logicNil, logicCons') (LogicList a)))
ExhaustivePrism
  (Logic [Bit])
  (Remaining, Remaining)
  (Remaining, Checked)
  (Term Bit, Term [Bit])
  Remaining
  Checked
_LogicCons' (\(Term Bit
b, Term [Bit]
bs) -> do
      Term Bit
b Term Bit -> (Term Bit -> Goal ()) -> Goal ()
forall a b. a -> (a -> b) -> b
& (Matched (Checked, Checked) Bit -> Goal ()
forall m a x. Exhausted m => Matched m a -> Goal x
matche'
        (Matched (Checked, Checked) Bit -> Goal ())
-> ((Matched (Checked, Checked) Bit -> Goal ())
    -> Matched (Checked, Remaining) Bit -> Goal ())
-> Matched (Checked, Remaining) Bit
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic Bit)
  (Checked, Remaining)
  (Checked, Checked)
  ()
  Remaining
  Checked
-> (() -> Goal ())
-> (Matched (Checked, Checked) Bit -> Goal ())
-> Matched (Checked, Remaining) Bit
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Checked, Remaining) (Logic Bit))
     (f (Tagged (Checked, Checked) (Logic Bit)))
p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Checked, Remaining) Bit)
     (f (Tagged (Checked, Checked) Bit))
forall o i i' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged i ()) (f (Tagged i' ()))
-> p (Tagged (o, i) Bit) (f (Tagged (o, i') Bit))
ExhaustivePrism
  (Logic Bit)
  (Checked, Remaining)
  (Checked, Checked)
  ()
  Remaining
  Checked
_I' () -> Goal ()
forall a. a -> Goal a
forall (m :: * -> *) a. Monad m => a -> m a
return
        (Matched (Checked, Remaining) Bit -> Goal ())
-> ((Matched (Checked, Remaining) Bit -> Goal ())
    -> Matched (Remaining, Remaining) Bit -> Goal ())
-> Matched (Remaining, Remaining) Bit
-> Goal ()
forall a b. a -> (a -> b) -> b
& ExhaustivePrism
  (Logic Bit)
  (Remaining, Remaining)
  (Checked, Remaining)
  ()
  Remaining
  Checked
-> (() -> Goal ())
-> (Matched (Checked, Remaining) Bit -> Goal ())
-> Matched (Remaining, Remaining) Bit
-> Goal ()
forall a v m m' x.
(Logical a, Fresh v) =>
ExhaustivePrism (Logic a) m m' v Remaining Checked
-> (v -> Goal x)
-> (Matched m' a -> Goal x)
-> Matched m a
-> Goal x
on' p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, Remaining) (Logic Bit))
     (f (Tagged (Checked, Remaining) (Logic Bit)))
p (Tagged Remaining ()) (f (Tagged Checked ()))
-> p (Tagged (Remaining, Remaining) Bit)
     (f (Tagged (Checked, Remaining) Bit))
forall o i o' (p :: * -> * -> *) (f :: * -> *).
(Choice p, Applicative f) =>
p (Tagged o ()) (f (Tagged o' ()))
-> p (Tagged (o, i) Bit) (f (Tagged (o', i) Bit))
ExhaustivePrism
  (Logic Bit)
  (Remaining, Remaining)
  (Checked, Remaining)
  ()
  Remaining
  Checked
_O' (\() -> Term [Bit] -> Goal ()
poso Term [Bit]
bs)
        (Matched (Remaining, Remaining) Bit -> Goal ())
-> ((Matched (Remaining, Remaining) Bit -> Goal ())
    -> Term Bit -> Goal ())
-> Term Bit
-> Goal ()
forall a b. a -> (a -> b) -> b
& (Matched (Remaining, Remaining) Bit -> Goal ())
-> Term Bit -> Goal ()
forall m a x. (Matched m a -> Goal x) -> Term a -> Goal x
enter')
      Term [Bit] -> Goal ()
binaryo Term [Bit]
bs)
  (Matched (Remaining, Remaining) [Bit] -> Goal ())
-> ((Matched (Remaining, Remaining) [Bit] -> Goal ())
    -> Term [Bit] -> Goal ())
-> Term [Bit]
-> Goal ()
forall a b. a -> (a -> b) -> b
& (Matched (Remaining, Remaining) [Bit] -> Goal ())
-> Term [Bit] -> Goal ()
forall m a x. (Matched m a -> Goal x) -> Term a -> Goal x
enter'
{- FOURMOLU_ENABLE -}

-- | Check that the first list is shorter than the second one.
lesslo :: Term Binary -> Term Binary -> Goal ()
lesslo :: Term [Bit] -> Term [Bit] -> Goal ()
lesslo Term [Bit]
n Term [Bit]
m =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit] -> Goal ()
zeroo Term [Bit]
n
        Term [Bit] -> Goal ()
poso Term [Bit]
m
    , do
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Goal ()
gtlo Term [Bit]
m
    , do
        (Term Bit
a, Term [Bit]
x, Term Bit
b, Term [Bit]
y) <- Goal (Term Bit, Term [Bit], Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a Term [Bit]
x)
        Term [Bit] -> Goal ()
poso Term [Bit]
x
        Term [Bit]
m Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
y)
        Term [Bit] -> Goal ()
poso Term [Bit]
y
        Term [Bit] -> Term [Bit] -> Goal ()
lesslo Term [Bit]
x Term [Bit]
y
    ]

-- | Check that the lists have the same length.
samelo :: Term Binary -> Term Binary -> Goal ()
samelo :: Term [Bit] -> Term [Bit] -> Goal ()
samelo Term [Bit]
n Term [Bit]
m =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit] -> Goal ()
zeroo Term [Bit]
n
        Term [Bit] -> Goal ()
zeroo Term [Bit]
m
    , do
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit]
m Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
    , do
        (Term Bit
a, Term [Bit]
x, Term Bit
b, Term [Bit]
y) <- Goal (Term Bit, Term [Bit], Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a Term [Bit]
x)
        Term [Bit] -> Goal ()
poso Term [Bit]
x
        Term [Bit]
m Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
y)
        Term [Bit] -> Goal ()
poso Term [Bit]
y
        Term [Bit] -> Term [Bit] -> Goal ()
samelo Term [Bit]
x Term [Bit]
y
    ]

-- | Check that the first list is shorter than the second one and at least of
-- the same length as the third list combined with the forth one.
--
-- Meaningfully, the part @[a]@ must be shorter than the whole @[b]@ and must
-- fit the result of multiplying @[c]@ with @[d]@, but here we're just concerned
-- with the lengths of the lists.
lessl3o :: Term Binary -> Term Binary -> Term Binary -> Term Binary -> Goal ()
lessl3o :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
lessl3o Term [Bit]
q Term [Bit]
c Term [Bit]
a Term [Bit]
b =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit] -> Goal ()
zeroo Term [Bit]
q
        Term [Bit] -> Goal ()
poso Term [Bit]
c
    , do
        (Term Bit
a0, Term Bit
a1, Term Bit
a2, Term Bit
a3, Term [Bit]
x, (Term [Bit]
y, Term [Bit]
z)) <- Goal
  (Term Bit, Term Bit, Term Bit, Term Bit, Term [Bit],
   (Term [Bit], Term [Bit]))
forall v. Fresh v => Goal v
fresh
        Term [Bit]
q Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a0 Term [Bit]
x)
        Term [Bit]
c Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a1 Term [Bit]
y)
        [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
          [ do
              Term [Bit] -> Goal ()
zeroo Term [Bit]
a
              Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a2 Term [Bit]
z)
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
lessl3o Term [Bit]
x Term [Bit]
y Term [Bit]
z ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0)
          , do
              Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a3 Term [Bit]
z)
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
lessl3o Term [Bit]
x Term [Bit]
y Term [Bit]
z Term [Bit]
b
          ]
    ]

appendo :: (Logical a) => Term [a] -> Term [a] -> Term [a] -> Goal ()
appendo :: forall a. Logical a => Term [a] -> Term [a] -> Term [a] -> Goal ()
appendo Term [a]
xs Term [a]
ys Term [a]
zs =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [a]
xs Term [a] -> Term [a] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [a] -> Term [a]
forall a. Logical a => a -> Term a
inject' []
        Term [a]
ys Term [a] -> Term [a] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [a]
zs
    , do
        (Term a
x, Term [a]
xs', Term [a]
zs') <- Goal (Term a, Term [a], Term [a])
forall v. Fresh v => Goal v
fresh
        Term [a]
xs Term [a] -> Term [a] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [a] -> Term [a]
forall a. Logic a -> Term a
Value (Term a -> Term [a] -> LogicList a
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term a
x Term [a]
xs')
        Term [a]
zs Term [a] -> Term [a] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [a] -> Term [a]
forall a. Logic a -> Term a
Value (Term a -> Term [a] -> LogicList a
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term a
x Term [a]
zs')
        Term [a] -> Term [a] -> Term [a] -> Goal ()
forall a. Logical a => Term [a] -> Term [a] -> Term [a] -> Goal ()
appendo Term [a]
xs' Term [a]
ys Term [a]
zs'
    ]

-- | A one-bit full adder.
full1Addero :: Term Bit -> Term Bit -> Term Bit -> Term Bit -> Term Bit -> Goal ()
full1Addero :: Term Bit -> Term Bit -> Term Bit -> Term Bit -> Term Bit -> Goal ()
full1Addero Term Bit
carryIn Term Bit
a Term Bit
b Term Bit
s Term Bit
carryOut =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term Bit
carryIn Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O
        [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
          [ do
              Term Bit
a Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O
              [[Goal ()]] -> Goal ()
conde
                [ [Term Bit
b Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O, Term Bit
s Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O, Term Bit
carryOut Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O]
                , [Term Bit
b Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I, Term Bit
s Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I, Term Bit
carryOut Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O]
                ]
          , do
              Term Bit
a Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I
              [[Goal ()]] -> Goal ()
conde
                [ [Term Bit
b Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O, Term Bit
s Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I, Term Bit
carryOut Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O]
                , [Term Bit
b Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I, Term Bit
s Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O, Term Bit
carryOut Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I]
                ]
          ]
    , do
        Term Bit
carryIn Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I
        [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
          [ do
              Term Bit
a Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O
              [[Goal ()]] -> Goal ()
conde
                [ [Term Bit
b Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O, Term Bit
s Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I, Term Bit
carryOut Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O]
                , [Term Bit
b Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I, Term Bit
s Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O, Term Bit
carryOut Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I]
                ]
          , do
              Term Bit
a Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I
              [[Goal ()]] -> Goal ()
conde
                [ [Term Bit
b Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O, Term Bit
s Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O, Term Bit
carryOut Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I]
                , [Term Bit
b Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I, Term Bit
s Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I, Term Bit
carryOut Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I]
                ]
          ]
    ]

-- | A full adder for numbers of arbitrary lengths.
fullNAddero :: Term Bit -> Term Binary -> Term Binary -> Term Binary -> Goal ()
fullNAddero :: Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
fullNAddero Term Bit
carryIn Term [Bit]
a Term [Bit]
b Term [Bit]
r =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term Bit
carryIn Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O
        Term [Bit] -> Goal ()
zeroo Term [Bit]
b
        Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
r
    , do
        Term Bit
carryIn Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O
        Term [Bit] -> Goal ()
zeroo Term [Bit]
a
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
r
        Term [Bit] -> Goal ()
poso Term [Bit]
b
    , do
        Term Bit
carryIn Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I
        Term [Bit] -> Goal ()
zeroo Term [Bit]
b
        Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
fullNAddero (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) Term [Bit]
a ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
r
    , do
        Term Bit
carryIn Term Bit -> Term Bit -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I
        Term [Bit] -> Goal ()
zeroo Term [Bit]
a
        Term [Bit] -> Goal ()
poso Term [Bit]
b
        Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
fullNAddero (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
b Term [Bit]
r
    , do
        Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        (Term Bit
d, Term Bit
c) <- Goal (Term Bit, Term Bit)
forall v. Fresh v => Goal v
fresh
        Term [Bit]
r Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
d (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
c (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value Logic [Bit]
LogicList Bit
forall a. LogicList a
LogicNil))))
        Term Bit -> Term Bit -> Term Bit -> Term Bit -> Term Bit -> Goal ()
full1Addero Term Bit
carryIn (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term Bit
d Term Bit
c
    , do
        Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
genFullNAddero Term Bit
carryIn Term [Bit]
a Term [Bit]
b Term [Bit]
r
    , do
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Goal ()
gtlo Term [Bit]
a
        Term [Bit] -> Goal ()
gtlo Term [Bit]
r
        Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
fullNAddero Term Bit
carryIn ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
a Term [Bit]
r
    , do
        Term [Bit] -> Goal ()
gtlo Term [Bit]
a
        Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
genFullNAddero Term Bit
carryIn Term [Bit]
a Term [Bit]
b Term [Bit]
r
    ]

genFullNAddero :: Term Bit -> Term Binary -> Term Binary -> Term Binary -> Goal ()
genFullNAddero :: Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
genFullNAddero Term Bit
carryIn Term [Bit]
n Term [Bit]
m Term [Bit]
r = do
  (Term Bit
a, Term Bit
b, Term Bit
c, Term Bit
e, Term [Bit]
x, (Term [Bit]
y, Term [Bit]
z)) <- Goal
  (Term Bit, Term Bit, Term Bit, Term Bit, Term [Bit],
   (Term [Bit], Term [Bit]))
forall v. Fresh v => Goal v
fresh
  Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a Term [Bit]
x)
  Term [Bit]
m Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
y)
  Term [Bit] -> Goal ()
poso Term [Bit]
y
  Term [Bit]
r Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
c Term [Bit]
z)
  Term [Bit] -> Goal ()
poso Term [Bit]
z
  Term Bit -> Term Bit -> Term Bit -> Term Bit -> Term Bit -> Goal ()
full1Addero Term Bit
carryIn Term Bit
a Term Bit
b Term Bit
c Term Bit
e
  Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
fullNAddero Term Bit
e Term [Bit]
x Term [Bit]
y Term [Bit]
z

-- | Calculate the sum @c@ of two numbers @a@ and @b@.
--
-- >>> extract' <$> run (addo (inject' 3) (inject' 5))
-- [Just [O,O,O,I]]
--
-- One can turn it around to subtract from a number:
--
-- >>> extract' <$> run (\b -> addo (inject' 2) b (inject' 8))
-- [Just [O,I,I]]
--
-- When both summands are unknown, every possible pair will be enumerated.
--
-- >>> bimap extract' extract' <$> run (\(a, b) -> addo a b (inject' 2))
-- [(Just [O,I],Just []),(Just [],Just [O,I]),(Just [I],Just [I])]
--
-- If one of the summands is greater than the sum, the relation will produce no
-- results.
--
-- >>> run (\a -> addo a (inject' 10) (inject' 3))
-- []
--
-- The implementation of @add@ is discussed in section 4 of the paper.
addo
  :: Term Binary
  -- ^ @a@, the first summand
  -> Term Binary
  -- ^ @b@, the second summand
  -> Term Binary
  -- ^ @c@, the sum
  -> Goal ()
addo :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo = Term Bit -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
fullNAddero (Bit -> Term Bit
forall a. Logical a => a -> Term a
inject' Bit
O)

-- | Calculate the difference @c@ of two numbers @a@ and @b@. This is just
-- 'addo', but with parameters in different order.
subo
  :: Term Binary
  -- ^ @a@, the minuend
  -> Term Binary
  -- ^ @b@, the subtrahend
  -> Term Binary
  -- ^ @c@, the difference
  -> Goal ()
subo :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
subo Term [Bit]
a Term [Bit]
b Term [Bit]
c = Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
b Term [Bit]
c Term [Bit]
a

-- | Check that @a@ is strictly less than @b@. Otherwise, the goal fails.
--
-- >>> run (\() -> lesso (inject' 3) (inject' 4))
-- [()]
-- >>> run (\() -> lesso (inject' 3) (inject' 2))
-- []
--
-- One can turn this relation around to generate numbers less or greater than a
-- given one.
--
-- >>> extract' <$> run (\x -> lesso x (inject' 4))
-- [Just [],Just [I],Just [I,I],Just [O,I]]
-- >>> take 5 $ extract' <$> run (\x -> lesso (inject' 4) x)
-- [Just [I,O,I],Just [O,I,I],Just [I,I,I],Just [O,O,O,I],Just [I,O,O,I]]
lesso
  :: Term Binary
  -- ^ @a@, the lesser number
  -> Term Binary
  -- ^ @b@, the greater number
  -> Goal ()
lesso :: Term [Bit] -> Term [Bit] -> Goal ()
lesso Term [Bit]
a Term [Bit]
b =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit] -> Term [Bit] -> Goal ()
lesslo Term [Bit]
a Term [Bit]
b
    , do
        Term [Bit] -> Term [Bit] -> Goal ()
samelo Term [Bit]
a Term [Bit]
b
        Term [Bit]
x <- Goal (Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Goal ()
poso Term [Bit]
x
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
a Term [Bit]
x Term [Bit]
b
    ]

-- | Calculate the product @c@ of two numbers @a@ and @b@.
--
-- >>> extract' <$> run (mulo (inject' 3) (inject' 4))
-- [Just [O,O,I,I]]
--
-- One can turn this around to factor a given number.
--
-- >>> extract' <$> run (\a -> mulo a (inject' 2) (inject' 12))
-- [Just [O,I,I]]
-- >>> bimap extract' extract' <$> run (\(a, b) -> mulo a b (inject' 4))
-- [(Just [I],Just [O,O,I]),(Just [O,I],Just [O,I]),(Just [O,O,I],Just [I])]
--
-- The goal will fail if any multiplier is not a factor of the product.
--
-- >>> run (\a -> mulo a (inject' 5) (inject' 7))
-- []
--
-- The implementation of @mul@ is discussed in section 5 of the paper.
mulo
  :: Term Binary
  -- ^ @a@, the first multiplier
  -> Term Binary
  -- ^ @b@, the second multiplier
  -> Term Binary
  -- ^ @c@, the product
  -> Goal ()
mulo :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
a Term [Bit]
b Term [Bit]
c =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit] -> Goal ()
zeroo Term [Bit]
a
        Term [Bit] -> Goal ()
zeroo Term [Bit]
c
    , do
        Term [Bit] -> Goal ()
poso Term [Bit]
a
        Term [Bit] -> Goal ()
zeroo Term [Bit]
b
        Term [Bit] -> Goal ()
zeroo Term [Bit]
c
    , do
        Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Goal ()
poso Term [Bit]
b
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
c
    , do
        Term [Bit] -> Goal ()
gtlo Term [Bit]
a
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
c
    , do
        (Term [Bit]
x, Term [Bit]
z) <- Goal (Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) Term [Bit]
x)
        Term [Bit] -> Goal ()
poso Term [Bit]
x
        Term [Bit]
c Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) Term [Bit]
z)
        Term [Bit] -> Goal ()
poso Term [Bit]
z
        Term [Bit] -> Goal ()
gtlo Term [Bit]
b
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
x Term [Bit]
b Term [Bit]
z
    , do
        (Term [Bit]
x, Term [Bit]
y) <- Goal (Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term [Bit]
x)
        Term [Bit] -> Goal ()
poso Term [Bit]
x
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) Term [Bit]
y)
        Term [Bit] -> Goal ()
poso Term [Bit]
y
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
b Term [Bit]
a Term [Bit]
c
    , do
        (Term [Bit]
x, Term [Bit]
y) <- Goal (Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
a Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term [Bit]
x)
        Term [Bit] -> Goal ()
poso Term [Bit]
x
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term [Bit]
y)
        Term [Bit] -> Goal ()
poso Term [Bit]
y

        Term [Bit]
q <- Goal (Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
lessl3o Term [Bit]
q Term [Bit]
c Term [Bit]
a Term [Bit]
b
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
x Term [Bit]
b Term [Bit]
q
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) Term [Bit]
q)) Term [Bit]
b Term [Bit]
c
    ]

-- | Calculate the quotient @q@ and remainder @r@ of dividing @n@ by @m@.
--
-- >>> bimap extract' extract' <$> run (\(q, r) -> divo (inject' 17) (inject' 5) q r)
-- [(Just [I,I],Just [O,I])]
--
-- One can turn this around to find divisors of a number.
--
-- >>> extract' <$> run (\m -> fresh >>= \q -> divo (inject' 12) m q (inject' 0))
-- [Just [O,O,I,I],Just [I],Just [I,I],Just [O,I,I],Just [O,I],Just [O,O,I]]
--
-- The implementation of @div@ is discussed in section 6 of the paper.
divo
  :: Term Binary
  -- ^ @n@, the dividend
  -> Term Binary
  -- ^ @m@, the divisor
  -> Term Binary
  -- ^ @q@, the quotient
  -> Term Binary
  -- ^ @r@, the remainder
  -> Goal ()
divo :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
divo Term [Bit]
n Term [Bit]
m Term [Bit]
q Term [Bit]
r =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
r
        Term [Bit] -> Goal ()
zeroo Term [Bit]
q
        Term [Bit] -> Term [Bit] -> Goal ()
lesso Term [Bit]
n Term [Bit]
m
    , do
        Term [Bit]
q Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Term [Bit] -> Goal ()
samelo Term [Bit]
n Term [Bit]
m
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
r Term [Bit]
m Term [Bit]
n
        Term [Bit] -> Term [Bit] -> Goal ()
lesso Term [Bit]
r Term [Bit]
m
    , do
        Term [Bit] -> Term [Bit] -> Goal ()
lesslo Term [Bit]
m Term [Bit]
n
        Term [Bit] -> Term [Bit] -> Goal ()
lesso Term [Bit]
r Term [Bit]
m
        Term [Bit] -> Goal ()
poso Term [Bit]
q

        (Term [Bit]
n1, Term [Bit]
n2, Term [Bit]
q1, Term [Bit]
q2, Term [Bit]
q2m, (Term [Bit]
q2mr, Term [Bit]
rr, Term [Bit]
r1)) <- Goal
  (Term [Bit], Term [Bit], Term [Bit], Term [Bit], Term [Bit],
   (Term [Bit], Term [Bit], Term [Bit]))
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
n Term [Bit]
r Term [Bit]
n1 Term [Bit]
n2
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
q Term [Bit]
r Term [Bit]
q1 Term [Bit]
q2
        [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
          [ do
              Term [Bit] -> Goal ()
zeroo Term [Bit]
n1
              Term [Bit] -> Goal ()
zeroo Term [Bit]
q1
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
subo Term [Bit]
n2 Term [Bit]
r Term [Bit]
q2m
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
q2 Term [Bit]
m Term [Bit]
q2m
          , do
              Term [Bit] -> Goal ()
poso Term [Bit]
n1
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
q2 Term [Bit]
m Term [Bit]
q2m
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
q2m Term [Bit]
r Term [Bit]
q2mr
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
subo Term [Bit]
q2mr Term [Bit]
n2 Term [Bit]
rr
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
rr Term [Bit]
r Term [Bit]
r1 ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0)
              Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
divo Term [Bit]
n1 Term [Bit]
m Term [Bit]
q1 Term [Bit]
r1
          ]
    ]

-- | Split @n@ into @n1@ and @n2@ such that @n = 2^(length r + 1) * n1 + n2@.
splito :: Term Binary -> Term Binary -> Term Binary -> Term Binary -> Goal ()
splito :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
n Term [Bit]
r Term [Bit]
n1 Term [Bit]
n2 =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit] -> Goal ()
zeroo Term [Bit]
n
        Term [Bit] -> Goal ()
zeroo Term [Bit]
n1
        Term [Bit] -> Goal ()
zeroo Term [Bit]
n2
    , do
        (Term Bit
b, Term [Bit]
n') <- Goal (Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
n')))
        Term [Bit] -> Goal ()
zeroo Term [Bit]
r
        Term [Bit]
n1 Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
n')
        Term [Bit] -> Goal ()
zeroo Term [Bit]
n2
    , do
        Term [Bit]
n' <- Goal (Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term [Bit]
n')
        Term [Bit] -> Goal ()
zeroo Term [Bit]
r
        Term [Bit]
n1 Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
n'
        Term [Bit]
n2 Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
    , do
        (Term Bit
b, Term [Bit]
n', Term Bit
a, Term [Bit]
r') <- Goal (Term Bit, Term [Bit], Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
n')))
        Term [Bit]
r Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a Term [Bit]
r')
        Term [Bit] -> Goal ()
zeroo Term [Bit]
n2
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
n')) Term [Bit]
r' Term [Bit]
n1 ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0)
    , do
        (Term [Bit]
n', Term Bit
a, Term [Bit]
r') <- Goal (Term [Bit], Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term [Bit]
n')
        Term [Bit]
r Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a Term [Bit]
r')
        Term [Bit]
n2 Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
n' Term [Bit]
r' Term [Bit]
n1 ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0)
    , do
        (Term Bit
b, Term [Bit]
n', Term Bit
a, Term [Bit]
r', Term [Bit]
n2') <- Goal (Term Bit, Term [Bit], Term Bit, Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
n')
        Term [Bit]
r Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
a Term [Bit]
r')
        Term [Bit]
n2 Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b Term [Bit]
n2')
        Term [Bit] -> Goal ()
poso Term [Bit]
n2'
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
n' Term [Bit]
r' Term [Bit]
n1 Term [Bit]
n2'
    ]

-- | Calculate @n = (b + 1)^q@, where @b + 1@ is a power of two.
exp2o :: Term Binary -> Term Binary -> Term Binary -> Goal ()
exp2o :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
exp2o Term [Bit]
n Term [Bit]
b Term [Bit]
q =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Goal ()
zeroo Term [Bit]
q
    , do
        Term [Bit] -> Goal ()
gtlo Term [Bit]
n
        Term [Bit]
q Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit]
_n2 <- Goal (Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
n Term [Bit]
b ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
_n2
    , do
        (Term [Bit]
q1, Term [Bit]
b2) <- Goal (Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
q Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
O) Term [Bit]
q1)
        Term [Bit] -> Goal ()
poso Term [Bit]
q1
        Term [Bit] -> Term [Bit] -> Goal ()
lesslo Term [Bit]
b Term [Bit]
n
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term [a] -> Term [a] -> Term [a] -> Goal ()
appendo Term [Bit]
b (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term [Bit]
b)) Term [Bit]
b2
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
exp2o Term [Bit]
n Term [Bit]
b2 Term [Bit]
q1
    , do
        (Term [Bit]
q1, Term [Bit]
n1, Term [Bit]
b2, Term [Bit]
_n2) <- Goal (Term [Bit], Term [Bit], Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit]
q Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term [Bit]
q1)
        Term [Bit] -> Goal ()
poso Term [Bit]
q1
        Term [Bit] -> Goal ()
poso Term [Bit]
n1
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
n Term [Bit]
b Term [Bit]
n1 Term [Bit]
_n2
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term [a] -> Term [a] -> Term [a] -> Goal ()
appendo Term [Bit]
b (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons (Logic Bit -> Term Bit
forall a. Logic a -> Term a
Value Logic Bit
Bit
I) Term [Bit]
b)) Term [Bit]
b2
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
exp2o Term [Bit]
n1 Term [Bit]
b2 Term [Bit]
q1
    ]

-- | Calculate @nq = n ^ q@.
repeatedMulo :: Term Binary -> Term Binary -> Term Binary -> Goal ()
repeatedMulo :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
repeatedMulo Term [Bit]
n Term [Bit]
q Term [Bit]
nq =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        Term [Bit] -> Goal ()
poso Term [Bit]
n
        Term [Bit] -> Goal ()
zeroo Term [Bit]
q
        Term [Bit]
nq Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
    , do
        Term [Bit]
q Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
nq
    , do
        Term [Bit] -> Goal ()
gtlo Term [Bit]
q
        (Term [Bit]
q1, Term [Bit]
nq1) <- Goal (Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
q1 ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
q
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
repeatedMulo Term [Bit]
n Term [Bit]
q1 Term [Bit]
nq1
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
nq1 Term [Bit]
n Term [Bit]
nq
    ]

-- | Calculate discrete logarithm @q@ of a number @n@ in base @b@, perhaps with
-- some remainder @r@.
--
-- >>> bimap extract' extract' <$> run (\(q, r) -> logo (inject' 9) (inject' 3) q r)
-- [(Just [O,I],Just [])]
-- >>> bimap extract' extract' <$> run (\(q, r) -> logo (inject' 15) (inject' 3) q r)
-- [(Just [O,I],Just [0,I,I])]
--
-- One can turn this around to find the number @b@ raised to some power @q@:
--
-- >>> extract' <$> run (\n -> logo n (inject' 5) (inject' 2) (inject' 0))
-- [Just [I,O,O,I,I]]
--
-- or to find the @q@-th root of @n@:
--
-- >>> extract' <$> run (\b -> logo (inject' 8) b (inject' 3) (inject' 0))
-- [Just [O,I]]
--
-- If you want to enumerate solutions to @logo n b q r@, you probably shouldn't
-- go beyond the first 16 solutions without an OOM killer.
--
-- The original implementation of this relation in Prolog can be found at
-- <https://okmij.org/ftp/Prolog/Arithm/pure-bin-arithm.prl>. Although the paper
-- mentions this relation in section 6, it does not discuss its implementation
-- in detail.
logo
  :: Term Binary
  -- ^ @n@, of which to calculate the logarithm
  -> Term Binary
  -- ^ @b@, the base
  -> Term Binary
  -- ^ @q@, the logarithm
  -> Term Binary
  -- ^ @r@, the remainder
  -> Goal ()
logo :: Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
logo Term [Bit]
n Term [Bit]
b Term [Bit]
q Term [Bit]
r =
  [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
    [ do
        -- n = b^0 + 0, b > 0
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Goal ()
poso Term [Bit]
b
        Term [Bit] -> Goal ()
zeroo Term [Bit]
q
        Term [Bit] -> Goal ()
zeroo Term [Bit]
r
    , do
        -- n = b^0 + r, r > 0
        Term [Bit] -> Goal ()
zeroo Term [Bit]
q
        Term [Bit] -> Term [Bit] -> Goal ()
lesso Term [Bit]
n Term [Bit]
b
        Term [Bit] -> Goal ()
poso Term [Bit]
r
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
r ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
n
    , do
        -- n = b^1 + r, b >= 2
        Term [Bit]
q Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Goal ()
gtlo Term [Bit]
b
        Term [Bit] -> Term [Bit] -> Goal ()
samelo Term [Bit]
n Term [Bit]
b
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
r Term [Bit]
b Term [Bit]
n
    , do
        -- n = 1^q + r, q > 0
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1
        Term [Bit] -> Goal ()
poso Term [Bit]
q
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
r ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
n
    , do
        -- n = 0^q + r, q > 0
        Term [Bit] -> Goal ()
zeroo Term [Bit]
b
        Term [Bit] -> Goal ()
poso Term [Bit]
q
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
r
    , do
        -- n = 2^q + r, n >= 4
        Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
2
        (Term Bit
_b1, Term Bit
_b2, Term [Bit]
n1) <- Goal (Term Bit, Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Goal ()
poso Term [Bit]
n1
        Term [Bit]
n Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
_b1 (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
_b2 Term [Bit]
n1)))
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
exp2o Term [Bit]
n ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0) Term [Bit]
q
        Term [Bit]
_r1 <- Goal (Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
splito Term [Bit]
n Term [Bit]
n1 Term [Bit]
_r1 Term [Bit]
r
    , do
        -- n = b^q + r, b >= 3
        (Term Bit
b1, Term Bit
b2, Term Bit
b3, Term [Bit]
br) <- Goal (Term Bit, Term Bit, Term Bit, Term [Bit])
forall v. Fresh v => Goal v
fresh
        [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany
          [ Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== [Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
3
          , Term [Bit]
b Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b1 (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b2 (Logic [Bit] -> Term [Bit]
forall a. Logic a -> Term a
Value (Term Bit -> Term [Bit] -> LogicList Bit
forall a. Term a -> Term [a] -> LogicList a
LogicCons Term Bit
b3 Term [Bit]
br)))))
          ]
        Term [Bit] -> Term [Bit] -> Goal ()
lesslo Term [Bit]
b Term [Bit]
n

        (Term [Bit]
bw1, Term [Bit]
bw, Term [Bit]
nw1, Term [Bit]
nw, Term [Bit]
ql, (Term [Bit]
ql1, Term [Bit]
_r)) <- Goal
  (Term [Bit], Term [Bit], Term [Bit], Term [Bit], Term [Bit],
   (Term [Bit], Term [Bit]))
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
exp2o Term [Bit]
b ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0) Term [Bit]
bw1
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
bw1 ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
bw
        Term [Bit] -> Term [Bit] -> Goal ()
lesslo Term [Bit]
q Term [Bit]
n

        (Term [Bit]
q1, Term [Bit]
bwq1) <- Goal (Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
q ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
q1
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
bw Term [Bit]
q1 Term [Bit]
bwq1
        Term [Bit] -> Term [Bit] -> Goal ()
lesso Term [Bit]
nw1 Term [Bit]
bwq1

        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
exp2o Term [Bit]
n ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0) Term [Bit]
nw1
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
nw1 ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
nw
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
divo Term [Bit]
nw Term [Bit]
bw Term [Bit]
ql1 Term [Bit]
_r
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
ql ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
1) Term [Bit]
ql1
        [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany [Term [Bit] -> Term [Bit] -> Goal ()
samelo Term [Bit]
q Term [Bit]
ql, Term [Bit] -> Term [Bit] -> Goal ()
lesslo Term [Bit]
ql Term [Bit]
q]

        (Term [Bit]
bql, Term [Bit]
qh, Term [Bit]
_r', Term [Bit]
qdh, Term [Bit]
qd) <- Goal (Term [Bit], Term [Bit], Term [Bit], Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
repeatedMulo Term [Bit]
b Term [Bit]
ql Term [Bit]
bql
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
divo Term [Bit]
nw Term [Bit]
bw1 Term [Bit]
qh Term [Bit]
_r'
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
ql Term [Bit]
qdh Term [Bit]
qh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
ql Term [Bit]
qd Term [Bit]
q
        [Goal ()] -> Goal ()
forall x. [Goal x] -> Goal x
disjMany [Term [Bit]
qd Term [Bit] -> Term [Bit] -> Goal ()
forall a. Logical a => Term a -> Term a -> Goal ()
=== Term [Bit]
qdh, Term [Bit] -> Term [Bit] -> Goal ()
lesso Term [Bit]
qd Term [Bit]
qdh]

        (Term [Bit]
bqd, Term [Bit]
bq, Term [Bit]
bq1) <- Goal (Term [Bit], Term [Bit], Term [Bit])
forall v. Fresh v => Goal v
fresh
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
repeatedMulo Term [Bit]
b Term [Bit]
qd Term [Bit]
bqd
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
bql Term [Bit]
bqd Term [Bit]
bq
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo Term [Bit]
b Term [Bit]
bq Term [Bit]
bq1
        Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo Term [Bit]
bq Term [Bit]
r Term [Bit]
n
        Term [Bit] -> Term [Bit] -> Goal ()
lesso Term [Bit]
n Term [Bit]
bq1
    ]

example :: IO ()
example :: IO ()
example = do
  String -> IO ()
putStrLn String
"addo 3 5 x:"
  (Maybe [Bit] -> IO ()) -> [Maybe [Bit]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Maybe [Bit] -> IO ()
forall a. Show a => a -> IO ()
print ([Maybe [Bit]] -> IO ()) -> [Maybe [Bit]] -> IO ()
forall a b. (a -> b) -> a -> b
$ Term [Bit] -> Maybe [Bit]
forall a. Logical a => Term a -> Maybe a
extract' (Term [Bit] -> Maybe [Bit]) -> [Term [Bit]] -> [Maybe [Bit]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term [Bit] -> Goal ()) -> [Term [Bit]]
forall v. Fresh v => (v -> Goal ()) -> [v]
run (Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
addo ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
3) ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
5))

  String -> IO ()
putStrLn String
"\nmulo 3 4 x:"
  (Maybe [Bit] -> IO ()) -> [Maybe [Bit]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Maybe [Bit] -> IO ()
forall a. Show a => a -> IO ()
print ([Maybe [Bit]] -> IO ()) -> [Maybe [Bit]] -> IO ()
forall a b. (a -> b) -> a -> b
$ Term [Bit] -> Maybe [Bit]
forall a. Logical a => Term a -> Maybe a
extract' (Term [Bit] -> Maybe [Bit]) -> [Term [Bit]] -> [Maybe [Bit]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (Term [Bit] -> Goal ()) -> [Term [Bit]]
forall v. Fresh v => (v -> Goal ()) -> [v]
run (Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
mulo ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
3) ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
4))

  String -> IO ()
putStrLn String
"\ndivo 15 4 q r:"
  ((Maybe [Bit], Maybe [Bit]) -> IO ())
-> [(Maybe [Bit], Maybe [Bit])] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Maybe [Bit], Maybe [Bit]) -> IO ()
forall a. Show a => a -> IO ()
print ([(Maybe [Bit], Maybe [Bit])] -> IO ())
-> [(Maybe [Bit], Maybe [Bit])] -> IO ()
forall a b. (a -> b) -> a -> b
$ (Term [Bit] -> Maybe [Bit])
-> (Term [Bit] -> Maybe [Bit])
-> (Term [Bit], Term [Bit])
-> (Maybe [Bit], Maybe [Bit])
forall a b c d. (a -> b) -> (c -> d) -> (a, c) -> (b, d)
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Term [Bit] -> Maybe [Bit]
forall a. Logical a => Term a -> Maybe a
extract' Term [Bit] -> Maybe [Bit]
forall a. Logical a => Term a -> Maybe a
extract' ((Term [Bit], Term [Bit]) -> (Maybe [Bit], Maybe [Bit]))
-> [(Term [Bit], Term [Bit])] -> [(Maybe [Bit], Maybe [Bit])]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Term [Bit], Term [Bit]) -> Goal ()) -> [(Term [Bit], Term [Bit])]
forall v. Fresh v => (v -> Goal ()) -> [v]
run ((Term [Bit] -> Term [Bit] -> Goal ())
-> (Term [Bit], Term [Bit]) -> Goal ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
divo ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
15) ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
4)))

  let exps :: [(Integer, Integer, [Term [Bit]])]
exps =
        [ (Integer
b, Integer
p, (Term [Bit] -> Goal ()) -> [Term [Bit]]
forall v. Fresh v => (v -> Goal ()) -> [v]
run (\Term [Bit]
n -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Term [Bit] -> Goal ()
logo Term [Bit]
n ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' (Integer -> [Bit]
forall a. Num a => Integer -> a
fromInteger Integer
b)) ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' (Integer -> [Bit]
forall a. Num a => Integer -> a
fromInteger Integer
p)) ([Bit] -> Term [Bit]
forall a. Logical a => a -> Term a
inject' [Bit]
0)))
        | Integer
b <- [Integer
1 .. Integer
3]
        , Integer
p <- [Integer
1 .. Integer
6]
        ]
  ((Integer, Integer, [Term [Bit]]) -> IO ())
-> [(Integer, Integer, [Term [Bit]])] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_
    ( \(Integer
b, Integer
p, [Term [Bit]]
bp) -> do
        String -> IO ()
putStrLn (String
"\nlogo n " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
b String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Integer -> String
forall a. Show a => a -> String
show Integer
p String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" 0:")
        (Maybe [Bit] -> IO ()) -> [Maybe [Bit]] -> IO ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ Maybe [Bit] -> IO ()
forall a. Show a => a -> IO ()
print (Term [Bit] -> Maybe [Bit]
forall a. Logical a => Term a -> Maybe a
extract' (Term [Bit] -> Maybe [Bit]) -> [Term [Bit]] -> [Maybe [Bit]]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Term [Bit]]
bp)
    )
    [(Integer, Integer, [Term [Bit]])]
exps