-- | Some propositional formulas to test, and functions to generate classes.
--
-- Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeSynonymInstances #-}

module Data.Logic.ATP.PropExamples
    ( Knows(K)
    , mk_knows, mk_knows2
    , prime
    , ramsey
    , testPropExamples
    ) where

import Data.Bits (Bits, shiftR)
import Data.List as List (map)
import Data.Logic.ATP.Formulas
import Data.Logic.ATP.Lib (allsets, timeMessage)
import Data.Logic.ATP.Lit ((.~.))
import Data.Logic.ATP.Pretty (HasFixity(precedence), Pretty(pPrint), prettyShow, text)
import Data.Logic.ATP.Prop
import Data.Set as Set
import Prelude hiding (sum)
import Test.HUnit

-- | Generate assertion equivalent to R(s,t) <= n for the Ramsey number R(s,t)
ramsey :: (IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) =>
          Integer -> Integer -> Integer -> pf
ramsey :: forall pf.
(IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) =>
Integer -> Integer -> Integer -> pf
ramsey Integer
s Integer
t Integer
n =
  let vertices :: Set Integer
vertices = [Integer] -> Set Integer
forall a. Ord a => [a] -> Set a
Set.fromList [Integer
1 .. Integer
n] in
  let yesgrps :: Set (Set (Set Integer))
yesgrps = (Set Integer -> Set (Set Integer))
-> Set (Set Integer) -> Set (Set (Set Integer))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Integer -> Set Integer -> Set (Set Integer)
forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsets (Integer
2 :: Integer)) (Integer -> Set Integer -> Set (Set Integer)
forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsets Integer
s Set Integer
vertices)
      nogrps :: Set (Set (Set Integer))
nogrps = (Set Integer -> Set (Set Integer))
-> Set (Set Integer) -> Set (Set (Set Integer))
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Integer -> Set Integer -> Set (Set Integer)
forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsets (Integer
2 :: Integer)) (Integer -> Set Integer -> Set (Set Integer)
forall a b. (Num a, Eq a, Ord b) => a -> Set b -> Set (Set b)
allsets Integer
t Set Integer
vertices) in
  let e :: Set a -> formula
e Set a
xs = let [a
a, a
b] = Set a -> [a]
forall a. Set a -> [a]
Set.toAscList Set a
xs in AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> a -> Maybe a -> Knows a
forall a. String -> a -> Maybe a -> Knows a
K String
"p" a
a (a -> Maybe a
forall a. a -> Maybe a
Just a
b)) in
  Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj ((Set (Set Integer) -> pf) -> Set (Set (Set Integer)) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj (Set pf -> pf)
-> (Set (Set Integer) -> Set pf) -> Set (Set Integer) -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Integer -> pf) -> Set (Set Integer) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Set Integer -> pf
forall {formula} {a}.
(AtomOf formula ~ Knows a, IsFormula formula, IsAtom (Knows a),
 Ord a, Show a, Num a) =>
Set a -> formula
e) Set (Set (Set Integer))
yesgrps) pf -> pf -> pf
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_disj ((Set (Set Integer) -> pf) -> Set (Set (Set Integer)) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Set pf -> pf
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj (Set pf -> pf)
-> (Set (Set Integer) -> Set pf) -> Set (Set Integer) -> pf
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Set Integer -> pf) -> Set (Set Integer) -> Set pf
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ Set Integer
p -> pf -> pf
forall formula. IsLiteral formula => formula -> formula
(.~.)(Set Integer -> pf
forall {formula} {a}.
(AtomOf formula ~ Knows a, IsFormula formula, IsAtom (Knows a),
 Ord a, Show a, Num a) =>
Set a -> formula
e Set Integer
p))) Set (Set (Set Integer))
nogrps)

data Knows a = K String a (Maybe a) deriving (Knows a -> Knows a -> Bool
(Knows a -> Knows a -> Bool)
-> (Knows a -> Knows a -> Bool) -> Eq (Knows a)
forall a. Eq a => Knows a -> Knows a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Knows a -> Knows a -> Bool
== :: Knows a -> Knows a -> Bool
$c/= :: forall a. Eq a => Knows a -> Knows a -> Bool
/= :: Knows a -> Knows a -> Bool
Eq, Eq (Knows a)
Eq (Knows a) =>
(Knows a -> Knows a -> Ordering)
-> (Knows a -> Knows a -> Bool)
-> (Knows a -> Knows a -> Bool)
-> (Knows a -> Knows a -> Bool)
-> (Knows a -> Knows a -> Bool)
-> (Knows a -> Knows a -> Knows a)
-> (Knows a -> Knows a -> Knows a)
-> Ord (Knows a)
Knows a -> Knows a -> Bool
Knows a -> Knows a -> Ordering
Knows a -> Knows a -> Knows a
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall a. Ord a => Eq (Knows a)
forall a. Ord a => Knows a -> Knows a -> Bool
forall a. Ord a => Knows a -> Knows a -> Ordering
forall a. Ord a => Knows a -> Knows a -> Knows a
$ccompare :: forall a. Ord a => Knows a -> Knows a -> Ordering
compare :: Knows a -> Knows a -> Ordering
$c< :: forall a. Ord a => Knows a -> Knows a -> Bool
< :: Knows a -> Knows a -> Bool
$c<= :: forall a. Ord a => Knows a -> Knows a -> Bool
<= :: Knows a -> Knows a -> Bool
$c> :: forall a. Ord a => Knows a -> Knows a -> Bool
> :: Knows a -> Knows a -> Bool
$c>= :: forall a. Ord a => Knows a -> Knows a -> Bool
>= :: Knows a -> Knows a -> Bool
$cmax :: forall a. Ord a => Knows a -> Knows a -> Knows a
max :: Knows a -> Knows a -> Knows a
$cmin :: forall a. Ord a => Knows a -> Knows a -> Knows a
min :: Knows a -> Knows a -> Knows a
Ord, Int -> Knows a -> ShowS
[Knows a] -> ShowS
Knows a -> String
(Int -> Knows a -> ShowS)
-> (Knows a -> String) -> ([Knows a] -> ShowS) -> Show (Knows a)
forall a. Show a => Int -> Knows a -> ShowS
forall a. Show a => [Knows a] -> ShowS
forall a. Show a => Knows a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Knows a -> ShowS
showsPrec :: Int -> Knows a -> ShowS
$cshow :: forall a. Show a => Knows a -> String
show :: Knows a -> String
$cshowList :: forall a. Show a => [Knows a] -> ShowS
showList :: [Knows a] -> ShowS
Show)

instance (Num a, Show a) => Pretty (Knows a) where
    pPrint :: Knows a -> Doc
pPrint (K String
s a
n Maybe a
mm) = String -> Doc
text (String
s String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
n String -> ShowS
forall a. [a] -> [a] -> [a]
++ String -> (a -> String) -> Maybe a -> String
forall b a. b -> (a -> b) -> Maybe a -> b
maybe String
"" (\ a
m -> String
"." String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> String
forall a. Show a => a -> String
show a
m) Maybe a
mm)

instance Num a => HasFixity (Knows a) where
    precedence :: Knows a -> Precedence
precedence Knows a
_ = a
9

instance IsAtom (Knows Integer)

-- Some currently tractable examples. (p. 36)
test01 :: Test
test01 :: Test
test01 = [Test] -> Test
TestList [Assertion -> Test
TestCase (String -> String -> String -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"ramsey 3 3 4"
                                         String
"(p1.2∧p1.3∧p2.3)∨(p1.2∧p1.4∧p2.4)∨(p1.3∧p1.4∧p3.4)∨(p2.3∧p2.4∧p3.4)∨(¬p1.2∧¬p1.3∧¬p2.3)∨(¬p1.2∧¬p1.4∧¬p2.4)∨(¬p1.3∧¬p1.4∧¬p3.4)∨(¬p2.3∧¬p2.4∧¬p3.4)"
                                         -- "p1.2∧p1.3∧p2.3∨p1.2∧p1.4∧p2.4∨p1.3∧p1.4∧p3.4∨p2.3∧p2.4∧p3.4∨¬p1.2∧¬p1.3∧¬p2.3∨¬p1.2∧¬p1.4∧¬p2.4∨¬p1.3∧¬p1.4∧¬p3.4∨¬p2.3∧¬p2.4∧¬p3.4"
                                         (PFormula (Knows Integer) -> String
forall a. Pretty a => a -> String
prettyShow (Integer -> Integer -> Integer -> PFormula (Knows Integer)
forall pf.
(IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) =>
Integer -> Integer -> Integer -> pf
ramsey Integer
3 Integer
3 Integer
4 :: PFormula (Knows Integer)))),
                   Assertion -> Test
TestCase ((() -> NominalDiffTime -> String) -> Assertion -> Assertion
forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage (\()
_ NominalDiffTime
t -> String
"\nTime to compute (ramsey 3 3 5): " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
forall a. Show a => a -> String
show NominalDiffTime
t) (Assertion -> Assertion) -> Assertion -> Assertion
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology (ramsey 3 3 5)" Bool
False (PFormula (Knows Integer) -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (Integer -> Integer -> Integer -> PFormula (Knows Integer)
forall pf.
(IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) =>
Integer -> Integer -> Integer -> pf
ramsey Integer
3 Integer
3 Integer
5 :: PFormula (Knows Integer)))),
                   Assertion -> Test
TestCase ((() -> NominalDiffTime -> String) -> Assertion -> Assertion
forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage (\()
_ NominalDiffTime
t -> String
"\nTime to compute (ramsey 3 3 6): " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
forall a. Show a => a -> String
show NominalDiffTime
t) (Assertion -> Assertion) -> Assertion -> Assertion
forall a b. (a -> b) -> a -> b
$ String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology (ramsey 3 3 6)" Bool
True (PFormula (Knows Integer) -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (Integer -> Integer -> Integer -> PFormula (Knows Integer)
forall pf.
(IsPropositional pf, AtomOf pf ~ Knows Integer, Ord pf) =>
Integer -> Integer -> Integer -> pf
ramsey Integer
3 Integer
3 Integer
6 :: PFormula (Knows Integer))))]

-- | Half adder.  (p. 66)
halfsum :: forall formula. IsPropositional formula => formula -> formula -> formula
halfsum :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
halfsum formula
x formula
y = formula
x formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
y)

halfcarry :: forall formula. IsPropositional formula => formula -> formula -> formula
halfcarry :: forall formula.
IsPropositional formula =>
formula -> formula -> formula
halfcarry formula
x formula
y = formula
x formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
y

ha :: forall formula. IsPropositional formula => formula -> formula -> formula -> formula -> formula
ha :: forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula -> formula
ha formula
x formula
y formula
s formula
c = (formula
s formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
halfsum formula
x formula
y) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (formula
c formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
halfcarry formula
x formula
y)

-- | Full adder.
carry :: forall formula. IsPropositional formula => formula -> formula -> formula -> formula
carry :: forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula
carry formula
x formula
y formula
z = (formula
x formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
y) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. ((formula
x formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. formula
y) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
z)

sum :: forall formula. IsPropositional formula => formula -> formula -> formula -> formula
sum :: forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula
sum formula
x formula
y formula
z = formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
halfsum (formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
halfsum formula
x formula
y) formula
z

fa :: forall formula. IsPropositional formula => formula -> formula -> formula -> formula -> formula -> formula
fa :: forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula -> formula -> formula
fa formula
x formula
y formula
z formula
s formula
c = (formula
s formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. formula -> formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula
sum formula
x formula
y formula
z) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (formula
c formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. formula -> formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula
carry formula
x formula
y formula
z)

-- | Useful idiom.
conjoin :: (IsPropositional formula, Ord formula, Ord a) => (a -> formula) -> Set a -> formula
conjoin :: forall formula a.
(IsPropositional formula, Ord formula, Ord a) =>
(a -> formula) -> Set a -> formula
conjoin a -> formula
f Set a
l = Set formula -> formula
forall (t :: * -> *) formula.
(Foldable t, IsFormula formula, IsPropositional formula) =>
t formula -> formula
list_conj ((a -> formula) -> Set a -> Set formula
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map a -> formula
f Set a
l)

-- | n-bit ripple carry adder with carry c(0) propagated in and c(n) out.  (p. 67)
ripplecarry :: (IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
               (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> a -> formula
ripplecarry :: forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry a -> formula
x a -> formula
y a -> formula
c a -> formula
out a
n =
    (a -> formula) -> Set a -> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a) =>
(a -> formula) -> Set a -> formula
conjoin (\ a
i -> formula -> formula -> formula -> formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula -> formula -> formula
fa (a -> formula
x a
i) (a -> formula
y a
i) (a -> formula
c a
i) (a -> formula
out a
i) (a -> formula
c(a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
1))) ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
0 .. (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)])

-- Example.
mk_knows :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> formula
mk_knows :: forall formula a.
(IsPropositional formula, AtomOf formula ~ Knows a) =>
String -> a -> formula
mk_knows String
x a
i = AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> a -> Maybe a -> Knows a
forall a. String -> a -> Maybe a -> Knows a
K String
x a
i Maybe a
forall a. Maybe a
Nothing)
mk_knows2 :: (IsPropositional formula, AtomOf formula ~ Knows a) => String -> a -> a -> formula
mk_knows2 :: forall formula a.
(IsPropositional formula, AtomOf formula ~ Knows a) =>
String -> a -> a -> formula
mk_knows2 String
x a
i a
j = AtomOf formula -> formula
forall formula. IsFormula formula => AtomOf formula -> formula
atomic (String -> a -> Maybe a -> Knows a
forall a. String -> a -> Maybe a -> Knows a
K String
x a
i (a -> Maybe a
forall a. a -> Maybe a
Just a
j))

test02 :: Test
test02 :: Test
test02 =
    let [Integer -> PFormula (Knows Integer)
x, Integer -> PFormula (Knows Integer)
y, Integer -> PFormula (Knows Integer)
out, Integer -> PFormula (Knows Integer)
c] = (String -> Integer -> PFormula (Knows Integer))
-> [String] -> [Integer -> PFormula (Knows Integer)]
forall a b. (a -> b) -> [a] -> [b]
List.map String -> Integer -> PFormula (Knows Integer)
forall formula a.
(IsPropositional formula, AtomOf formula ~ Knows a) =>
String -> a -> formula
mk_knows [String
"X", String
"Y", String
"OUT", String
"C"] :: [Integer -> PFormula (Knows Integer)] in
    Assertion -> Test
TestCase (String
-> PFormula (Knows Integer)
-> PFormula (Knows Integer)
-> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"ripplecarry x y c out 2"
                          (((Integer -> PFormula (Knows Integer)
out Integer
0 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((Integer -> PFormula (Knows Integer)
x Integer
0 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula. IsLiteral formula => formula -> formula
(.~.) (Integer -> PFormula (Knows Integer)
y Integer
0))) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula. IsLiteral formula => formula -> formula
(.~.) (Integer -> PFormula (Knows Integer)
c Integer
0)))) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                            (Integer -> PFormula (Knows Integer)
c Integer
1 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((Integer -> PFormula (Knows Integer)
x Integer
0 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. Integer -> PFormula (Knows Integer)
y Integer
0) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. ((Integer -> PFormula (Knows Integer)
x Integer
0 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. Integer -> PFormula (Knows Integer)
y Integer
0) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. Integer -> PFormula (Knows Integer)
c Integer
0)))) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                           ((Integer -> PFormula (Knows Integer)
out Integer
1 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((Integer -> PFormula (Knows Integer)
x Integer
1 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula. IsLiteral formula => formula -> formula
(.~.) (Integer -> PFormula (Knows Integer)
y Integer
1))) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula. IsLiteral formula => formula -> formula
(.~.) (Integer -> PFormula (Knows Integer)
c Integer
1)))) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
                            (Integer -> PFormula (Knows Integer)
c Integer
2 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. ((Integer -> PFormula (Knows Integer)
x Integer
1 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. Integer -> PFormula (Knows Integer)
y Integer
1) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. ((Integer -> PFormula (Knows Integer)
x Integer
1 PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. Integer -> PFormula (Knows Integer)
y Integer
1) PFormula (Knows Integer)
-> PFormula (Knows Integer) -> PFormula (Knows Integer)
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. Integer -> PFormula (Knows Integer)
c Integer
1)))))
                          ((Integer -> PFormula (Knows Integer))
-> (Integer -> PFormula (Knows Integer))
-> (Integer -> PFormula (Knows Integer))
-> (Integer -> PFormula (Knows Integer))
-> Integer
-> PFormula (Knows Integer)
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry Integer -> PFormula (Knows Integer)
x Integer -> PFormula (Knows Integer)
y Integer -> PFormula (Knows Integer)
c Integer -> PFormula (Knows Integer)
out Integer
2 :: PFormula (Knows Integer)))

-- | Special case with 0 instead of c(0).
ripplecarry0 :: (IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
                (a -> formula)
             -> (a -> formula)
             -> (a -> formula)
             -> (a -> formula)
             -> a -> formula
ripplecarry0 :: forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry0 a -> formula
x a -> formula
y a -> formula
c a -> formula
out a
n =
  formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify
   ((a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry a -> formula
x a -> formula
y (\ a
i -> if a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 then formula
forall formula. IsFormula formula => formula
false else a -> formula
c a
i) a -> formula
out a
n)

-- | Carry-select adder
ripplecarry1 :: (IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
                (a -> formula)
             -> (a -> formula)
             -> (a -> formula)
             -> (a -> formula)
             -> a -> formula
ripplecarry1 :: forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry1 a -> formula
x a -> formula
y a -> formula
c a -> formula
out a
n =
  formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify
   ((a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry a -> formula
x a -> formula
y (\ a
i -> if a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 then formula
forall formula. IsFormula formula => formula
true else a -> formula
c a
i) a -> formula
out a
n)

mux :: forall formula. IsPropositional formula => formula -> formula -> formula -> formula
mux :: forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula
mux formula
sel formula
in0 formula
in1 = ((formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) formula
sel) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
in0) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.|. (formula
sel formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. formula
in1)

offset :: forall t a. Num a => a -> (a -> t) -> a -> t
offset :: forall t a. Num a => a -> (a -> t) -> a -> t
offset a
n a -> t
x a
i = a -> t
x (a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
i)

carryselect :: (IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
               (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> a -> a -> formula
carryselect :: forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> a
-> formula
carryselect a -> formula
x a -> formula
y a -> formula
c0 a -> formula
c1 a -> formula
s0 a -> formula
s1 a -> formula
c a -> formula
s a
n a
k =
  let k' :: a
k' = a -> a -> a
forall a. Ord a => a -> a -> a
min a
n a
k in
  let fm :: formula
fm = (((a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry0 a -> formula
x a -> formula
y a -> formula
c0 a -> formula
s0 a
k') formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry1 a -> formula
x a -> formula
y a -> formula
c1 a -> formula
s1 a
k')) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
           (((a -> formula
c a
k') formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (formula -> formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula
mux (a -> formula
c a
0) (a -> formula
c0 a
k') (a -> formula
c1 a
k'))) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
            ((a -> formula) -> Set a -> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a) =>
(a -> formula) -> Set a -> formula
conjoin (\ a
i -> (a -> formula
s a
i) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (formula -> formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula -> formula
mux (a -> formula
c a
0) (a -> formula
s0 a
i) (a -> formula
s1 a
i)))
                             ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
0 .. (a
k' a -> a -> a
forall a. Num a => a -> a -> a
- a
1)]))) in
  if a
k' a -> a -> Bool
forall a. Ord a => a -> a -> Bool
< a
k then formula
fm else
  formula
fm formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> a
-> formula
carryselect
          (a -> (a -> formula) -> a -> formula
forall t a. Num a => a -> (a -> t) -> a -> t
offset a
k a -> formula
x) (a -> (a -> formula) -> a -> formula
forall t a. Num a => a -> (a -> t) -> a -> t
offset a
k a -> formula
y) (a -> (a -> formula) -> a -> formula
forall t a. Num a => a -> (a -> t) -> a -> t
offset a
k a -> formula
c0) (a -> (a -> formula) -> a -> formula
forall t a. Num a => a -> (a -> t) -> a -> t
offset a
k a -> formula
c1)
          (a -> (a -> formula) -> a -> formula
forall t a. Num a => a -> (a -> t) -> a -> t
offset a
k a -> formula
s0) (a -> (a -> formula) -> a -> formula
forall t a. Num a => a -> (a -> t) -> a -> t
offset a
k a -> formula
s1) (a -> (a -> formula) -> a -> formula
forall t a. Num a => a -> (a -> t) -> a -> t
offset a
k a -> formula
c) (a -> (a -> formula) -> a -> formula
forall t a. Num a => a -> (a -> t) -> a -> t
offset a
k a -> formula
s)
          (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
k) a
k)

-- | Equivalence problems for carry-select vs ripple carry adders. (p. 69)
mk_adder_test :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows a, Ord a, Num a, Enum a, Show a) =>
                 a -> a -> formula
mk_adder_test :: forall formula a.
(IsPropositional formula, Ord formula, AtomOf formula ~ Knows a,
 Ord a, Num a, Enum a, Show a) =>
a -> a -> formula
mk_adder_test a
n a
k =
  let [a -> formula
x, a -> formula
y, a -> formula
c, a -> formula
s, a -> formula
c0, a -> formula
s0, a -> formula
c1, a -> formula
s1, a -> formula
c2, a -> formula
s2] =
          (String -> a -> formula) -> [String] -> [a -> formula]
forall a b. (a -> b) -> [a] -> [b]
List.map String -> a -> formula
forall formula a.
(IsPropositional formula, AtomOf formula ~ Knows a) =>
String -> a -> formula
mk_knows [String
"x", String
"y", String
"c", String
"s", String
"c0", String
"s0", String
"c1", String
"s1", String
"c2", String
"s2"] in
  ((((a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> a
-> formula
carryselect a -> formula
x a -> formula
y a -> formula
c0 a -> formula
c1 a -> formula
s0 a -> formula
s1 a -> formula
c a -> formula
s a
n a
k) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
    (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) (a -> formula
c a
0))) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
   ((a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry0 a -> formula
x a -> formula
y a -> formula
c2 a -> formula
s2 a
n)) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.=>.
  (((a -> formula
c a
n) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (a -> formula
c2 a
n)) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
   ((a -> formula) -> Set a -> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a) =>
(a -> formula) -> Set a -> formula
conjoin (\ a
i -> (a -> formula
s a
i) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (a -> formula
s2 a
i)) ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
0 .. (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)])))

-- | Ripple carry stage that separates off the final result.  (p. 70)
--
--       UUUUUUUUUUUUUUUUUUUU  (u)
--    +  VVVVVVVVVVVVVVVVVVVV  (v)
--
--    = WWWWWWWWWWWWWWWWWWWW   (w)
--    +                     Z  (z)

rippleshift :: (IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
               (a -> formula)
            -> (a -> formula)
            -> (a -> formula)
            -> formula
            -> (a -> formula)
            -> a -> formula
rippleshift :: forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> formula
-> (a -> formula)
-> a
-> formula
rippleshift a -> formula
u a -> formula
v a -> formula
c formula
z a -> formula
w a
n =
  (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> a
-> formula
ripplecarry0 a -> formula
u a -> formula
v (\ a
i -> if a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n then a -> formula
w(a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) else a -> formula
c(a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
1))
                   (\ a
i -> if a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 then formula
z else a -> formula
w(a
i a -> a -> a
forall a. Num a => a -> a -> a
- a
1)) a
n

-- | Naive multiplier based on repeated ripple carry.
multiplier :: (IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
              (a -> a -> formula)
           -> (a -> a -> formula)
           -> (a -> a -> formula)
           -> (a -> formula)
           -> a
           -> formula
multiplier :: forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> a -> formula)
-> (a -> a -> formula)
-> (a -> a -> formula)
-> (a -> formula)
-> a
-> formula
multiplier a -> a -> formula
x a -> a -> formula
u a -> a -> formula
v a -> formula
out a
n =
  if a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
1 then ((a -> formula
out a
0) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (a -> a -> formula
x a
0 a
0)) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(a -> formula
out a
1)) else
  formula -> formula
forall formula. IsPropositional formula => formula -> formula
psimplify (((a -> formula
out a
0) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (a -> a -> formula
x a
0 a
0)) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
             (((a -> formula)
-> (a -> formula)
-> (a -> formula)
-> formula
-> (a -> formula)
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> formula
-> (a -> formula)
-> a
-> formula
rippleshift
               (\ a
i -> if a
i a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1 then formula
forall formula. IsFormula formula => formula
false else a -> a -> formula
x a
0 (a
i a -> a -> a
forall a. Num a => a -> a -> a
+ a
1))
               (a -> a -> formula
x a
1) (a -> a -> formula
v a
2) (a -> formula
out a
1) (a -> a -> formula
u a
2) a
n) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&.
              (if a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
2 then ((a -> formula
out a
2) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (a -> a -> formula
u a
2 a
0)) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. ((a -> formula
out a
3) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.<=>. (a -> a -> formula
u a
2 a
1)) else
                   (a -> formula) -> Set a -> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a) =>
(a -> formula) -> Set a -> formula
conjoin (\ a
k -> (a -> formula)
-> (a -> formula)
-> (a -> formula)
-> formula
-> (a -> formula)
-> a
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> formula)
-> (a -> formula)
-> (a -> formula)
-> formula
-> (a -> formula)
-> a
-> formula
rippleshift (a -> a -> formula
u a
k) (a -> a -> formula
x a
k) (a -> a -> formula
v(a
k a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)) (a -> formula
out a
k)
                                   (if a
k a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1 then \ a
i -> a -> formula
out(a
n a -> a -> a
forall a. Num a => a -> a -> a
+ a
i)
                                    else a -> a -> formula
u(a
k a -> a -> a
forall a. Num a => a -> a -> a
+ a
1)) a
n) ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
2 .. (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)]))))

-- | Primality examples. (p. 71)
--
-- For large examples, should use 'Integer' instead of 'Int' in these functions.
bitlength :: forall b a. (Num a, Num b, Bits b) => b -> a
bitlength :: forall b a. (Num a, Num b, Bits b) => b -> a
bitlength b
x = if b
x b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
0 then a
0 else a
1 a -> a -> a
forall a. Num a => a -> a -> a
+ b -> a
forall b a. (Num a, Num b, Bits b) => b -> a
bitlength (b -> Int -> b
forall a. Bits a => a -> Int -> a
shiftR b
x Int
1);;

bit :: forall a b. (Num a, Eq a, Bits b, Integral b) => a -> b -> Bool
bit :: forall a b. (Num a, Eq a, Bits b, Integral b) => a -> b -> Bool
bit a
n b
x = if a
n a -> a -> Bool
forall a. Eq a => a -> a -> Bool
== a
0 then b
x b -> b -> b
forall a. Integral a => a -> a -> a
`mod` b
2 b -> b -> Bool
forall a. Eq a => a -> a -> Bool
== b
1 else a -> b -> Bool
forall a b. (Num a, Eq a, Bits b, Integral b) => a -> b -> Bool
bit (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1) (b -> Int -> b
forall a. Bits a => a -> Int -> a
shiftR b
x Int
1)

congruent_to :: (IsPropositional formula, Ord formula, Bits b, Ord a, Num a, Integral b, Enum a) =>
                (a -> formula) -> b -> a -> formula
congruent_to :: forall formula b a.
(IsPropositional formula, Ord formula, Bits b, Ord a, Num a,
 Integral b, Enum a) =>
(a -> formula) -> b -> a -> formula
congruent_to a -> formula
x b
m a
n =
  (a -> formula) -> Set a -> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a) =>
(a -> formula) -> Set a -> formula
conjoin (\ a
i -> if a -> b -> Bool
forall a b. (Num a, Eq a, Bits b, Integral b) => a -> b -> Bool
bit a
i b
m then a -> formula
x a
i else formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.)(a -> formula
x a
i))
          ([a] -> Set a
forall a. Ord a => [a] -> Set a
Set.fromList [a
0 .. (a
n a -> a -> a
forall a. Num a => a -> a -> a
- a
1)])

prime :: (IsPropositional formula, Ord formula, AtomOf formula ~ Knows Integer) => Integer -> formula
prime :: forall formula.
(IsPropositional formula, Ord formula,
 AtomOf formula ~ Knows Integer) =>
Integer -> formula
prime Integer
p =
  let [Integer -> formula
x, Integer -> formula
y, Integer -> formula
out] = (String -> Integer -> formula) -> [String] -> [Integer -> formula]
forall a b. (a -> b) -> [a] -> [b]
List.map String -> Integer -> formula
forall formula a.
(IsPropositional formula, AtomOf formula ~ Knows a) =>
String -> a -> formula
mk_knows [String
"x", String
"y", String
"out"] in
  let m :: Integer -> Integer -> formula
m Integer
i Integer
j = (Integer -> formula
x Integer
i) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (Integer -> formula
y Integer
j)
      [Integer -> Integer -> formula
u, Integer -> Integer -> formula
v] = (String -> Integer -> Integer -> formula)
-> [String] -> [Integer -> Integer -> formula]
forall a b. (a -> b) -> [a] -> [b]
List.map String -> Integer -> Integer -> formula
forall formula a.
(IsPropositional formula, AtomOf formula ~ Knows a) =>
String -> a -> a -> formula
mk_knows2 [String
"u", String
"v"] in
  let (Integer
n :: Integer) = Integer -> Integer
forall b a. (Num a, Num b, Bits b) => b -> a
bitlength Integer
p in
  formula -> formula
forall formula. IsLiteral formula => formula -> formula
(.~.) ((Integer -> Integer -> formula)
-> (Integer -> Integer -> formula)
-> (Integer -> Integer -> formula)
-> (Integer -> formula)
-> Integer
-> formula
forall formula a.
(IsPropositional formula, Ord formula, Ord a, Num a, Enum a) =>
(a -> a -> formula)
-> (a -> a -> formula)
-> (a -> a -> formula)
-> (a -> formula)
-> a
-> formula
multiplier Integer -> Integer -> formula
m Integer -> Integer -> formula
u Integer -> Integer -> formula
v Integer -> formula
out (Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
1) formula -> formula -> formula
forall formula.
IsPropositional formula =>
formula -> formula -> formula
.&. (Integer -> formula) -> Integer -> Integer -> formula
forall formula b a.
(IsPropositional formula, Ord formula, Bits b, Ord a, Num a,
 Integral b, Enum a) =>
(a -> formula) -> b -> a -> formula
congruent_to Integer -> formula
out Integer
p (Integer -> Integer -> Integer
forall a. Ord a => a -> a -> a
max Integer
n (Integer
2 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* Integer
n Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
- Integer
2)))

-- Examples. (p. 72)

type F = PFormula (Knows Integer)

test03 :: Test
test03 :: Test
test03 =
    [Test] -> Test
TestList [Assertion -> Test
TestCase ((() -> NominalDiffTime -> String) -> Assertion -> Assertion
forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage (\()
_ NominalDiffTime
t -> String
"\nTime to prove (prime 7): " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
forall a. Show a => a -> String
show NominalDiffTime
t)  (String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology(prime 7)" Bool
True (PFormula (Knows Integer) -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (Integer -> PFormula (Knows Integer)
forall formula.
(IsPropositional formula, Ord formula,
 AtomOf formula ~ Knows Integer) =>
Integer -> formula
prime Integer
7 :: F)))),
              Assertion -> Test
TestCase ((() -> NominalDiffTime -> String) -> Assertion -> Assertion
forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage (\()
_ NominalDiffTime
t -> String
"\nTime to prove (prime 9): " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
forall a. Show a => a -> String
show NominalDiffTime
t)  (String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology(prime 9)" Bool
False (PFormula (Knows Integer) -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (Integer -> PFormula (Knows Integer)
forall formula.
(IsPropositional formula, Ord formula,
 AtomOf formula ~ Knows Integer) =>
Integer -> formula
prime Integer
9 :: F)))),
              Assertion -> Test
TestCase ((() -> NominalDiffTime -> String) -> Assertion -> Assertion
forall r. (r -> NominalDiffTime -> String) -> IO r -> IO r
timeMessage (\()
_ NominalDiffTime
t -> String
"\nTime to prove (prime 11): " String -> ShowS
forall a. [a] -> [a] -> [a]
++ NominalDiffTime -> String
forall a. Show a => a -> String
show NominalDiffTime
t) (String -> Bool -> Bool -> Assertion
forall a.
(HasCallStack, Eq a, Show a) =>
String -> a -> a -> Assertion
assertEqual String
"tautology(prime 11)" Bool
True (PFormula (Knows Integer) -> Bool
forall pf. JustPropositional pf => pf -> Bool
tautology (Integer -> PFormula (Knows Integer)
forall formula.
(IsPropositional formula, Ord formula,
 AtomOf formula ~ Knows Integer) =>
Integer -> formula
prime Integer
11 :: F))))]

testPropExamples :: Test
testPropExamples :: Test
testPropExamples = String -> Test -> Test
TestLabel String
"PropExamples" ([Test] -> Test
TestList [Test
test01, Test
test02, Test
test03])