{- |
Module      : ProofSyntax
Copyright   : (c) Leon Vatthauer, 2026
License     : GPL-3
Maintainer  : Leon Vatthauer <leon.vatthauer@fau.de>
Stability   : experimental
Portability : non-portable (GHC extensions)

QuickCheck property tests for the t'Proof'
manipulation functions defined in "Fitch.Proof".

The module defines various helpers for constructing t'Proof's,
generators for arbitrarily generating t'Proof' and their contents as well as t'NodeAddr' and t'ProofAddr'.

Finally, this module defined properties concerning t'Proof', t'NodeAddr' and t'ProofAddr'.
-}
module ProofSyntax where

import Fitch.Proof
import Specification.Types
import Test.Tasty
import Test.Tasty.HUnit
import Test.Tasty.QuickCheck as QC
import Text.Show qualified

------------------------------------------------------------------------------------------

-- * Pretty Printing

-- | A wrapper around t'Proof' that replaces the derived 'Show' with 'PrettyPrint'.
newtype PrettyProof = PrettyProof Proof deriving (PrettyProof -> PrettyProof -> Bool
(PrettyProof -> PrettyProof -> Bool)
-> (PrettyProof -> PrettyProof -> Bool) -> Eq PrettyProof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: PrettyProof -> PrettyProof -> Bool
== :: PrettyProof -> PrettyProof -> Bool
$c/= :: PrettyProof -> PrettyProof -> Bool
/= :: PrettyProof -> PrettyProof -> Bool
Eq)

-- | Unwraps a t'PrettyProof' back to the underlying t'Proof'.
fromPretty :: PrettyProof -> Proof
fromPretty :: PrettyProof -> Proof
fromPretty (PrettyProof Proof
p) = Proof
p

-- | Pretty Printing via 'prettyPrint'.
instance Show PrettyProof where
  show :: PrettyProof -> String
  show :: PrettyProof -> String
show (PrettyProof Proof
p) = Text -> String
forall a. ToString a => a -> String
toString (Text -> String) -> Text -> String
forall a b. (a -> b) -> a -> b
$ Proof -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Proof
p

-- * Constructing Proofs

-- This section introduces helpers for constructing t'Proof's with trivial data
-- where only the proof structure is relevant.

-- | Constructs a trivial t'Formula' consisting of an t'Int'.
formula :: Int -> Formula
formula :: Int -> Formula
formula Int
n = Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid (Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n) (RawFormula -> Formula) -> RawFormula -> Formula
forall a b. (a -> b) -> a -> b
$ Text -> [Term] -> RawFormula
Pred (Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n) []

-- | Constructs a trivial t'Assumption' consisting of an t'Int'.
assumption :: Int -> Assumption
assumption :: Int -> Assumption
assumption Int
n = Wrapper RawAssumption -> Assumption
mkAssumption (Wrapper RawAssumption -> Assumption)
-> Wrapper RawAssumption -> Assumption
forall a b. (a -> b) -> a -> b
$ Text -> RawAssumption -> Wrapper RawAssumption
forall a. Text -> a -> Wrapper a
ParsedValid (Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n) (RawAssumption -> Wrapper RawAssumption)
-> RawAssumption -> Wrapper RawAssumption
forall a b. (a -> b) -> a -> b
$ RawFormula -> RawAssumption
RawAssumption (RawFormula -> RawAssumption) -> RawFormula -> RawAssumption
forall a b. (a -> b) -> a -> b
$ Text -> [Term] -> RawFormula
Pred (Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n) []

-- | Constructs a trivial t'RuleApplication' consisting of an t'Int'.
rule :: Int -> [Reference] -> Wrapper RuleApplication
rule :: Int -> [Reference] -> Wrapper RuleApplication
rule Int
n [Reference]
ref = Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> a -> Wrapper a
ParsedValid (Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n) (Text -> [Reference] -> RuleApplication
RuleApplication (Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n) [Reference]
ref)

-- | Constructs a trivial t'Derivation' using 'formula' and 'rule'.
derivation :: Int -> Derivation
derivation :: Int -> Derivation
derivation Int
n = Formula -> Wrapper RuleApplication -> Derivation
Derivation (Int -> Formula
formula Int
n) (Int -> [Reference] -> Wrapper RuleApplication
rule Int
n [])

------------------------------------------------------------------------------------------

-- Generators

-- | Generates a t'RuleApplication' based on 'rule'.
instance Arbitrary (Wrapper RuleApplication) where
  arbitrary :: Gen (Wrapper RuleApplication)
  arbitrary :: Gen (Wrapper RuleApplication)
arbitrary = (Int -> [Reference] -> Wrapper RuleApplication)
-> Gen Int -> Gen [Reference] -> Gen (Wrapper RuleApplication)
forall a b c. (a -> b -> c) -> Gen a -> Gen b -> Gen c
forall (f :: * -> *) a b c.
Applicative f =>
(a -> b -> c) -> f a -> f b -> f c
liftA2 Int -> [Reference] -> Wrapper RuleApplication
rule Gen Int
forall a. Arbitrary a => Gen a
arbitrary ([Reference] -> Gen [Reference]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [])

-- | Generates an t'Assumption' based on 'assumption'.
instance {-# OVERLAPPING #-} Arbitrary Assumption where
  arbitrary :: Gen Assumption
  arbitrary :: Gen Assumption
arbitrary = Int -> Assumption
assumption (Int -> Assumption) -> Gen Int -> Gen Assumption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary

-- | Generates a t'Derivation' based on 'derivation'.
instance Arbitrary Derivation where
  arbitrary :: Gen Derivation
  arbitrary :: Gen Derivation
arbitrary = Int -> Derivation
derivation (Int -> Derivation) -> Gen Int -> Gen Derivation
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int
forall a. Arbitrary a => Gen a
arbitrary

{- | Generates an arbitrary t'Proof' using 'sized'.

* At size @0@: a v'SubProof' consisting only of a conclusion.
* At size @n > 0@: a v'SubProof' with arbitrary assumptions, between 1 and
  8 body lines (to prevent huge t'Proof's.), and an arbitrary
  conclusion.
-}
instance Arbitrary Proof where
  arbitrary :: Gen Proof
  arbitrary :: Gen Proof
arbitrary = (Int -> Gen Proof) -> Gen Proof
forall a. (Int -> Gen a) -> Gen a
sized Int -> Gen Proof
proof'
   where
    proof' :: Int -> Gen Proof
    proof' :: Int -> Gen Proof
proof' Int
0 = ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Gen [Assumption]
-> Gen [Either Derivation Proof]
-> Gen Derivation
-> Gen Proof
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof ([Assumption] -> Gen [Assumption]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) ([Either Derivation Proof] -> Gen [Either Derivation Proof]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []) Gen Derivation
forall a. Arbitrary a => Gen a
arbitrary
    proof' Int
n | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Gen [Assumption]
-> Gen [Either Derivation Proof]
-> Gen Derivation
-> Gen Proof
forall (f :: * -> *) a b c d.
Applicative f =>
(a -> b -> c -> d) -> f a -> f b -> f c -> f d
liftA3 [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof Gen [Assumption]
forall a. Arbitrary a => Gen a
arbitrary Gen [Either Derivation Proof]
ps Gen Derivation
forall a. Arbitrary a => Gen a
arbitrary
     where
      ps :: Gen [Either Derivation Proof]
      ps :: Gen [Either Derivation Proof]
ps = do
        l <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
8)
        vectorOf l (resize (n `div` 2) arbitrary)

-- | Lifts 'Arbitrary' from t'Proof' to t'PrettyProof'.
instance Arbitrary PrettyProof where
  arbitrary :: Gen PrettyProof
  arbitrary :: Gen PrettyProof
arbitrary = (Proof -> PrettyProof) -> Gen Proof -> Gen PrettyProof
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proof -> PrettyProof
PrettyProof Gen Proof
forall a. Arbitrary a => Gen a
arbitrary

------------------------------------------------------------------------------------------

-- * Address Generators

{- | Used for specifying which kind of t'NodeAddr's 'arbitraryNodeAddrFor' should
produce.
-}
data AddrKind = AddrKind
  { AddrKind -> Bool
_assumptionKind :: Bool
  -- ^ a (possibly nested) 'NAAssumption'
  , AddrKind -> Bool
_lineKind :: Bool
  -- ^ a (possibly nested) 'NALine'
  , AddrKind -> Bool
_conclusionKind :: Bool
  -- ^  a (possibly nested) 'NAConclusion'
  , AddrKind -> Bool
_afterConclusionKind :: Bool
  -- ^ a (possibly nested) 'NAAfterConclusion'
  }

-- | Empty t'AddrKind' with all fields set to v'False'
instance Monoid AddrKind where
  mempty :: AddrKind
mempty =
    AddrKind
      { _assumptionKind :: Bool
_assumptionKind = Bool
False
      , _lineKind :: Bool
_lineKind = Bool
False
      , _conclusionKind :: Bool
_conclusionKind = Bool
False
      , _afterConclusionKind :: Bool
_afterConclusionKind = Bool
False
      }

-- | Combining t'AddrKind's, combines the fields with @||@.
instance Semigroup AddrKind where
  AddrKind Bool
ak1 Bool
lk1 Bool
ck1 Bool
ack1 <> :: AddrKind -> AddrKind -> AddrKind
<> AddrKind Bool
ak2 Bool
lk2 Bool
ck2 Bool
ack2 =
    Bool -> Bool -> Bool -> Bool -> AddrKind
AddrKind (Bool
ak1 Bool -> Bool -> Bool
|| Bool
ak2) (Bool
lk1 Bool -> Bool -> Bool
|| Bool
lk2) (Bool
ck1 Bool -> Bool -> Bool
|| Bool
ck2) (Bool
ack1 Bool -> Bool -> Bool
|| Bool
ack2)

-- | Constructor for setting '_assumptionKind'
assumptionKind :: AddrKind
assumptionKind :: AddrKind
assumptionKind = AddrKind
forall a. Monoid a => a
mempty{_assumptionKind = True}

-- | Constructor for setting '_lineKind'
lineKind :: AddrKind
lineKind :: AddrKind
lineKind = AddrKind
forall a. Monoid a => a
mempty{_lineKind = True}

-- | Constructor for setting '_conclusionKind'
conclusionKind :: AddrKind
conclusionKind :: AddrKind
conclusionKind = AddrKind
forall a. Monoid a => a
mempty{_conclusionKind = True}

-- | Constructor for setting '_afterConclusionKind'
afterConclusionKind :: AddrKind
afterConclusionKind :: AddrKind
afterConclusionKind = AddrKind
forall a. Monoid a => a
mempty{_afterConclusionKind = True}

-- | Constructor for setting all t'AddrKind's.
anyKind :: AddrKind
anyKind :: AddrKind
anyKind = AddrKind
assumptionKind AddrKind -> AddrKind -> AddrKind
forall a. Semigroup a => a -> a -> a
<> AddrKind
lineKind AddrKind -> AddrKind -> AddrKind
forall a. Semigroup a => a -> a -> a
<> AddrKind
conclusionKind AddrKind -> AddrKind -> AddrKind
forall a. Semigroup a => a -> a -> a
<> AddrKind
afterConclusionKind

{- | Constructor for setting all t'AddrKind's that are __inside__ of the t'Proof',
i.e. excluding 'afterConclusionKind'.
-}
anyInsideKind :: AddrKind
anyInsideKind :: AddrKind
anyInsideKind = AddrKind
assumptionKind AddrKind -> AddrKind -> AddrKind
forall a. Semigroup a => a -> a -> a
<> AddrKind
lineKind AddrKind -> AddrKind -> AddrKind
forall a. Semigroup a => a -> a -> a
<> AddrKind
conclusionKind

{- | Generates a valid t'NodeAddr' of the specified t'AddrKind'
for the given t'Proof'.
-}
arbitraryNodeAddrFor :: Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor :: Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
_) AddrKind
ak = do
  generators <- case [Maybe (Gen NodeAddr)] -> [Gen NodeAddr]
forall a. [Maybe a] -> [a]
catMaybes
    [ Gen NodeAddr -> Bool -> Maybe (Gen NodeAddr)
forall a. a -> Bool -> Maybe a
boolToMaybe Gen NodeAddr
naAssumption ([Assumption]
fs [Assumption] -> [Assumption] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] Bool -> Bool -> Bool
&& AddrKind -> Bool
_assumptionKind AddrKind
ak)
    , Gen NodeAddr -> Bool -> Maybe (Gen NodeAddr)
forall a. a -> Bool -> Maybe a
boolToMaybe Gen NodeAddr
naLine ([Either Derivation Proof]
ps [Either Derivation Proof] -> [Either Derivation Proof] -> Bool
forall a. Eq a => a -> a -> Bool
/= [] Bool -> Bool -> Bool
&& AddrKind -> Bool
_lineKind AddrKind
ak)
    , Gen NodeAddr -> Bool -> Maybe (Gen NodeAddr)
forall a. a -> Bool -> Maybe a
boolToMaybe Gen NodeAddr
naSubProof ([Either Derivation Proof]
ps [Either Derivation Proof] -> [Either Derivation Proof] -> Bool
forall a. Eq a => a -> a -> Bool
/= [])
    , Gen NodeAddr -> Bool -> Maybe (Gen NodeAddr)
forall a. a -> Bool -> Maybe a
boolToMaybe (NodeAddr -> Gen NodeAddr
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NodeAddr
NAConclusion) (AddrKind -> Bool
_conclusionKind AddrKind
ak)
    , Gen NodeAddr -> Bool -> Maybe (Gen NodeAddr)
forall a. a -> Bool -> Maybe a
boolToMaybe (NodeAddr -> Gen NodeAddr
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure NodeAddr
NAAfterConclusion) (AddrKind -> Bool
_afterConclusionKind AddrKind
ak)
    ] of
    [] -> Gen [Gen NodeAddr]
forall a. a
discard
    [Gen NodeAddr]
l -> [Gen NodeAddr] -> Gen [Gen NodeAddr]
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Gen NodeAddr]
l
  oneof generators
 where
  boolToMaybe :: a -> Bool -> Maybe a
  boolToMaybe :: forall a. a -> Bool -> Maybe a
boolToMaybe a
x Bool
True = a -> Maybe a
forall a. a -> Maybe a
Just a
x
  boolToMaybe a
_ Bool
False = Maybe a
forall a. Maybe a
Nothing
  naLine :: Gen NodeAddr
naLine =
    NodeAddr -> (Int -> NodeAddr) -> Maybe Int -> NodeAddr
forall b a. b -> (a -> b) -> Maybe a -> b
maybe NodeAddr
forall a. a
discard Int -> NodeAddr
NALine (Maybe Int -> NodeAddr) -> Gen (Maybe Int) -> Gen NodeAddr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen Int -> (Int -> Bool) -> Gen (Maybe Int)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
suchThatMaybe ((Int, Int) -> Gen Int
chooseInt (Int
0, [Either Derivation Proof] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Derivation Proof]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)) ((Either Derivation Proof -> Bool)
-> [Either Derivation Proof] -> Int -> Bool
forall a. (a -> Bool) -> [a] -> Int -> Bool
holdsAt Either Derivation Proof -> Bool
forall a b. Either a b -> Bool
isLeft [Either Derivation Proof]
ps)
  naAssumption :: Gen NodeAddr
naAssumption = (Int -> NodeAddr) -> Gen Int -> Gen NodeAddr
forall a b. (a -> b) -> Gen a -> Gen b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> NodeAddr
NAAssumption ((Int, Int) -> Gen Int
chooseInt (Int
0, [Assumption] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Assumption]
fs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
  naSubProof :: Gen NodeAddr
naSubProof = do
    mn <- (Int, Int) -> Gen Int
chooseInt (Int
0, [Either Derivation Proof] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Derivation Proof]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Gen Int -> (Int -> Bool) -> Gen (Maybe Int)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
`suchThatMaybe` (Either Derivation Proof -> Bool)
-> [Either Derivation Proof] -> Int -> Bool
forall a. (a -> Bool) -> [a] -> Int -> Bool
holdsAt Either Derivation Proof -> Bool
forall a b. Either a b -> Bool
isRight [Either Derivation Proof]
ps
    case mn of
      Just Int
n -> case [Either Derivation Proof]
ps [Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n of
        Just (Right Proof
p) -> Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
ak Gen NodeAddr -> (NodeAddr -> NodeAddr) -> Gen NodeAddr
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Int -> NodeAddr -> NodeAddr
NAProof Int
n
        Maybe (Either Derivation Proof)
_ -> Gen NodeAddr
forall a. a
discard
      Maybe Int
_ -> Gen NodeAddr
forall a. a
discard

-- | Generates a valid t'ProofAddr' for the given t'Proof'.
arbitraryProofAddrFor :: Proof -> Gen ProofAddr
arbitraryProofAddrFor :: Proof -> Gen ProofAddr
arbitraryProofAddrFor (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) = [Gen ProofAddr] -> Gen ProofAddr
forall a. HasCallStack => [Gen a] -> Gen a
oneof [Gen ProofAddr
paProof, Gen ProofAddr
paNested]
 where
  paProof :: Gen ProofAddr
paProof = ProofAddr -> Gen ProofAddr
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ProofAddr
PAProof
  paNested :: Gen ProofAddr
paNested = do
    mn <- (Int, Int) -> Gen Int
chooseInt (Int
0, [Either Derivation Proof] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Derivation Proof]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Gen Int -> (Int -> Bool) -> Gen (Maybe Int)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
`suchThatMaybe` (Either Derivation Proof -> Bool)
-> [Either Derivation Proof] -> Int -> Bool
forall a. (a -> Bool) -> [a] -> Int -> Bool
holdsAt Either Derivation Proof -> Bool
forall a b. Either a b -> Bool
isRight [Either Derivation Proof]
ps
    case mn of
      Just Int
n -> case [Either Derivation Proof]
ps [Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n of
        Just (Right Proof
p) -> Proof -> Gen ProofAddr
arbitraryProofAddrFor Proof
p Gen ProofAddr -> (ProofAddr -> ProofAddr) -> Gen ProofAddr
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Int -> ProofAddr -> ProofAddr
PANested Int
n
        Maybe (Either Derivation Proof)
_ -> Gen ProofAddr
forall a. a
discard
      Maybe Int
_ -> Gen ProofAddr
forall a. a
discard

{- | Generates a valid @(start, end)@ line-number range within the given
t'Proof'.
-}
arbitraryLineRangeFor :: Proof -> Gen (Int, Int)
arbitraryLineRangeFor :: Proof -> Gen (Int, Int)
arbitraryLineRangeFor p :: Proof
p@(SubProof [Assumption]
_ [Either Derivation Proof]
ps Derivation
_) = [Gen (Int, Int)] -> Gen (Int, Int)
forall a. HasCallStack => [Gen a] -> Gen a
oneof [Gen (Int, Int)
thisRange, Gen (Int, Int)
nestedRange]
 where
  thisRange :: Gen (Int, Int)
thisRange = (Int, Int) -> Gen (Int, Int)
forall a. a -> Gen a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int
1, Proof -> Int
pLength Proof
p)
  nestedRange :: Gen (Int, Int)
nestedRange = do
    mn <- (Int, Int) -> Gen Int
chooseInt (Int
0, [Either Derivation Proof] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Derivation Proof]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Gen Int -> (Int -> Bool) -> Gen (Maybe Int)
forall a. Gen a -> (a -> Bool) -> Gen (Maybe a)
`suchThatMaybe` (Either Derivation Proof -> Bool)
-> [Either Derivation Proof] -> Int -> Bool
forall a. (a -> Bool) -> [a] -> Int -> Bool
holdsAt Either Derivation Proof -> Bool
forall a b. Either a b -> Bool
isRight [Either Derivation Proof]
ps
    case mn of
      Just Int
n -> Int -> Proof -> Gen (Int, Int)
go Int
n Proof
p
      Maybe Int
Nothing -> Gen (Int, Int)
forall a. a
discard
  go :: Int -> Proof -> Gen (Int, Int)
  go :: Int -> Proof -> Gen (Int, Int)
go Int
0 (SubProof [Assumption]
fs (Right Proof
p : [Either Derivation Proof]
ps) Derivation
c) = do
    (start, end) <- Proof -> Gen (Int, Int)
arbitraryLineRangeFor Proof
p
    pure (start + length fs, end + length fs)
  go Int
n (SubProof [Assumption]
fs (Either Derivation Proof
e : [Either Derivation Proof]
ps) Derivation
c) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = do
    (start, end) <- Int -> Proof -> Gen (Int, Int)
go (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c)
    pure (start + either (const 1) pLength e, end + either (const 1) pLength e)
  go Int
_ Proof
_ = Gen (Int, Int)
forall a. a
discard

------------------------------------------------------------------------------------------

-- * Properties: naRemove

{- | Removing a 'lineKind' or 'assumptionKind' decreases 'pLength' by exactly 1.

> pLength <$> naRemove a p  ===  Just (pLength p - 1)
-}
prop_naRemoveMinus1 :: PrettyProof -> Property
prop_naRemoveMinus1 :: PrettyProof -> Property
prop_naRemoveMinus1 (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p (AddrKind
assumptionKind AddrKind -> AddrKind -> AddrKind
forall a. Semigroup a => a -> a -> a
<> AddrKind
lineKind)) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
a ->
    (Proof -> Int
pLength (Proof -> Int) -> Maybe Proof -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Proof -> Maybe Proof
naRemove NodeAddr
a Proof
p) Maybe Int -> Maybe Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Int -> Maybe Int
forall a. a -> Maybe a
Just (Proof -> Int
pLength Proof
p Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)

{- | After removing the t'Derivation' at address @a@, the entry that was immediately
after @a@ (at @'incrementNodeAddr' a@) is now reachable at address @a@.

> naLookup a <$> naRemove a p === Just ((`naLookup` p) =<< incrementNodeAddr a)
-}
prop_naRemoveShiftLine :: PrettyProof -> Property
prop_naRemoveShiftLine :: PrettyProof -> Property
prop_naRemoveShiftLine (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
lineKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
a ->
    case (Either Assumption Derivation -> Bool) -> Proof -> NodeAddr -> Bool
holdsAtNA Either Assumption Derivation -> Bool
forall a b. Either a b -> Bool
isRight Proof
p (NodeAddr -> Bool) -> Maybe NodeAddr -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Maybe NodeAddr
incrementNodeAddr NodeAddr
a of
      Maybe Bool
Nothing -> Maybe (Maybe (Either Assumption Derivation))
forall a. a
discard
      Just Bool
a' ->
        NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
a (Proof -> Maybe (Either Assumption Derivation))
-> Maybe Proof -> Maybe (Maybe (Either Assumption Derivation))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Proof -> Maybe Proof
naRemove NodeAddr
a Proof
p
      Maybe (Maybe (Either Assumption Derivation))
-> Maybe (Maybe (Either Assumption Derivation)) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe (Either Assumption Derivation)
-> Maybe (Maybe (Either Assumption Derivation))
forall a. a -> Maybe a
Just ((NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
`naLookup` Proof
p) (NodeAddr -> Maybe (Either Assumption Derivation))
-> Maybe NodeAddr -> Maybe (Either Assumption Derivation)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NodeAddr -> Maybe NodeAddr
incrementNodeAddr NodeAddr
a)

{- | After removing the t'Assumption' at address @a@, the entry that was immediately
after @a@ (at @'incrementNodeAddr' a@) is now reachable at address @a@.

> naLookup a <$> naRemove a p === Just ((`naLookup` p) =<< incrementNodeAddr a)
-}
prop_naRemoveShiftAssumption :: PrettyProof -> Property
prop_naRemoveShiftAssumption :: PrettyProof -> Property
prop_naRemoveShiftAssumption (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
assumptionKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
a ->
    case (Either Assumption Derivation -> Bool) -> Proof -> NodeAddr -> Bool
holdsAtNA Either Assumption Derivation -> Bool
forall a b. Either a b -> Bool
isLeft Proof
p (NodeAddr -> Bool) -> Maybe NodeAddr -> Maybe Bool
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Maybe NodeAddr
incrementNodeAddr NodeAddr
a of
      Maybe Bool
Nothing -> Maybe (Maybe (Either Assumption Derivation))
forall a. a
discard
      Just Bool
a' ->
        NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
a (Proof -> Maybe (Either Assumption Derivation))
-> Maybe Proof -> Maybe (Maybe (Either Assumption Derivation))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Proof -> Maybe Proof
naRemove NodeAddr
a Proof
p
      Maybe (Maybe (Either Assumption Derivation))
-> Maybe (Maybe (Either Assumption Derivation)) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe (Either Assumption Derivation)
-> Maybe (Maybe (Either Assumption Derivation))
forall a. a -> Maybe a
Just ((NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
`naLookup` Proof
p) (NodeAddr -> Maybe (Either Assumption Derivation))
-> Maybe NodeAddr -> Maybe (Either Assumption Derivation)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< NodeAddr -> Maybe NodeAddr
incrementNodeAddr NodeAddr
a)

------------------------------------------------------------------------------------------

-- * Properties: naInsertBefore

{- | A wrapper around 'naInsertBefore' that discards the
returned t'NodeAddr' and returns only the modified t'Proof'.
-}
naInsertBefore' ::
  Either Assumption Derivation ->
  NodeAddr ->
  Proof ->
  Maybe Proof
naInsertBefore' :: Either Assumption Derivation -> NodeAddr -> Proof -> Maybe Proof
naInsertBefore' Either Assumption Derivation
e NodeAddr
na Proof
p = case Either Assumption Derivation
-> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naInsertBefore Either Assumption Derivation
e NodeAddr
na Proof
p of
  Just (NodeAddr
_, Proof
p) -> Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
p
  Maybe (NodeAddr, Proof)
Nothing -> Maybe Proof
forall a. Maybe a
Nothing

{- | Inserting an t'Assumption' before an 'anyInsideKind' address increases
'pLength' by exactly 1.

> pLength <$> naInsertBefore' (Left (assumption 0)) a p  ===  Just (pLength p + 1)
-}
prop_naInsertBeforeAssumptionPlus1 :: PrettyProof -> Property
prop_naInsertBeforeAssumptionPlus1 :: PrettyProof -> Property
prop_naInsertBeforeAssumptionPlus1 (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
anyInsideKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
a ->
    (Proof -> Int
pLength (Proof -> Int) -> Maybe Proof -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Assumption Derivation -> NodeAddr -> Proof -> Maybe Proof
naInsertBefore' (Assumption -> Either Assumption Derivation
forall a b. a -> Either a b
Left (Assumption -> Either Assumption Derivation)
-> Assumption -> Either Assumption Derivation
forall a b. (a -> b) -> a -> b
$ Int -> Assumption
assumption Int
0) NodeAddr
a Proof
p) Maybe Int -> Maybe Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Int -> Maybe Int
forall a. a -> Maybe a
Just (Proof -> Int
pLength Proof
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

{- | Inserting a t'Derivation' before an 'anyInsideKind' address increases
'pLength' by exactly 1.

> pLength <$> naInsertBefore' (Right (derivation 0)) a p  ===  Just (pLength p + 1)
-}
prop_naInsertBeforeDerivationPlus1 :: PrettyProof -> Property
prop_naInsertBeforeDerivationPlus1 :: PrettyProof -> Property
prop_naInsertBeforeDerivationPlus1 (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
lineKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
a ->
    (Proof -> Int
pLength (Proof -> Int) -> Maybe Proof -> Maybe Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Assumption Derivation -> NodeAddr -> Proof -> Maybe Proof
naInsertBefore' (Derivation -> Either Assumption Derivation
forall a b. b -> Either a b
Right (Derivation -> Either Assumption Derivation)
-> Derivation -> Either Assumption Derivation
forall a b. (a -> b) -> a -> b
$ Int -> Derivation
derivation Int
0) NodeAddr
a Proof
p) Maybe Int -> Maybe Int -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Int -> Maybe Int
forall a. a -> Maybe a
Just (Proof -> Int
pLength Proof
p Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)

{- | After inserting @assumption 0@ before an 'assumptionKind' address,
'naLookup' returns @assumption 0@.


> naLookup a <$> naInsertBefore' (Left (assumption 0)) a p ===  Just (Just (Left (assumption 0)))
-}
prop_naInsertBeforeNaLookupAssumption :: PrettyProof -> Property
prop_naInsertBeforeNaLookupAssumption :: PrettyProof -> Property
prop_naInsertBeforeNaLookupAssumption (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
assumptionKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
na ->
    (NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
na (Proof -> Maybe (Either Assumption Derivation))
-> Maybe Proof -> Maybe (Maybe (Either Assumption Derivation))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Assumption Derivation -> NodeAddr -> Proof -> Maybe Proof
naInsertBefore' (Assumption -> Either Assumption Derivation
forall a b. a -> Either a b
Left (Assumption -> Either Assumption Derivation)
-> Assumption -> Either Assumption Derivation
forall a b. (a -> b) -> a -> b
$ Int -> Assumption
assumption Int
0) NodeAddr
na Proof
p)
      Maybe (Maybe (Either Assumption Derivation))
-> Maybe (Maybe (Either Assumption Derivation)) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (Maybe (Either Assumption Derivation)
-> Maybe (Maybe (Either Assumption Derivation))
forall a. a -> Maybe a
Just (Maybe (Either Assumption Derivation)
 -> Maybe (Maybe (Either Assumption Derivation)))
-> (Assumption -> Maybe (Either Assumption Derivation))
-> Assumption
-> Maybe (Maybe (Either Assumption Derivation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Assumption Derivation
-> Maybe (Either Assumption Derivation)
forall a. a -> Maybe a
Just (Either Assumption Derivation
 -> Maybe (Either Assumption Derivation))
-> (Assumption -> Either Assumption Derivation)
-> Assumption
-> Maybe (Either Assumption Derivation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assumption -> Either Assumption Derivation
forall a b. a -> Either a b
Left (Assumption -> Maybe (Maybe (Either Assumption Derivation)))
-> Assumption -> Maybe (Maybe (Either Assumption Derivation))
forall a b. (a -> b) -> a -> b
$ Int -> Assumption
assumption Int
0)

{- | After inserting @derivation 0@ before a 'lineKind' address,
'naLookup' returns @derivation 0@.

> naLookup a <$> naInsertBefore' (Right (derivation 0)) a p ===  Just (Just (Right (derivation 0)))
-}
prop_naInsertBeforeNaLookupDerivation :: PrettyProof -> Property
prop_naInsertBeforeNaLookupDerivation :: PrettyProof -> Property
prop_naInsertBeforeNaLookupDerivation (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
lineKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
na ->
    (NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
na (Proof -> Maybe (Either Assumption Derivation))
-> Maybe Proof -> Maybe (Maybe (Either Assumption Derivation))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Either Assumption Derivation -> NodeAddr -> Proof -> Maybe Proof
naInsertBefore' (Derivation -> Either Assumption Derivation
forall a b. b -> Either a b
Right (Derivation -> Either Assumption Derivation)
-> Derivation -> Either Assumption Derivation
forall a b. (a -> b) -> a -> b
$ Int -> Derivation
derivation Int
0) NodeAddr
na Proof
p)
      Maybe (Maybe (Either Assumption Derivation))
-> Maybe (Maybe (Either Assumption Derivation)) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (Maybe (Either Assumption Derivation)
-> Maybe (Maybe (Either Assumption Derivation))
forall a. a -> Maybe a
Just (Maybe (Either Assumption Derivation)
 -> Maybe (Maybe (Either Assumption Derivation)))
-> (Derivation -> Maybe (Either Assumption Derivation))
-> Derivation
-> Maybe (Maybe (Either Assumption Derivation))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Assumption Derivation
-> Maybe (Either Assumption Derivation)
forall a. a -> Maybe a
Just (Either Assumption Derivation
 -> Maybe (Either Assumption Derivation))
-> (Derivation -> Either Assumption Derivation)
-> Derivation
-> Maybe (Either Assumption Derivation)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation -> Either Assumption Derivation
forall a b. b -> Either a b
Right (Derivation -> Maybe (Maybe (Either Assumption Derivation)))
-> Derivation -> Maybe (Maybe (Either Assumption Derivation))
forall a b. (a -> b) -> a -> b
$ Int -> Derivation
derivation Int
0)

-- | Inserting an element and then removing it should return the original proof.
prop_naInsertBeforeRemove :: PrettyProof -> Property
prop_naInsertBeforeRemove :: PrettyProof -> Property
prop_naInsertBeforeRemove (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
anyKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
na ->
    (Either Assumption Derivation
-> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naInsertBefore (Derivation -> Either Assumption Derivation
forall a b. b -> Either a b
Right (Derivation -> Either Assumption Derivation)
-> Derivation -> Either Assumption Derivation
forall a b. (a -> b) -> a -> b
$ Int -> Derivation
derivation Int
0) NodeAddr
na Proof
p Maybe (NodeAddr, Proof)
-> ((NodeAddr, Proof) -> Maybe Proof) -> Maybe Proof
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= (NodeAddr -> Proof -> Maybe Proof)
-> (NodeAddr, Proof) -> Maybe Proof
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry NodeAddr -> Proof -> Maybe Proof
naRemove)
      Maybe Proof -> Maybe Proof -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
p

------------------------------------------------------------------------------------------

-- * Properties: paMoveBefore

{- | Moving a t'Proof' to a new position with 'paMoveBeforeRaw' preserves
its content, i.e. looking up the source address in the original t'Proof' yields the
same t'Proof' as looking up the destination address in the modified t'Proof.

> paLookup paTarget' p'  ===  paLookup paSource p
-}
prop_paMoveBeforeRawSameProof :: PrettyProof -> Property
prop_paMoveBeforeRawSameProof :: PrettyProof -> Property
prop_paMoveBeforeRawSameProof (PrettyProof Proof
p) =
  Gen ProofAddr -> (ProofAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> Gen ProofAddr
arbitraryProofAddrFor Proof
p) ((ProofAddr -> Property) -> Property)
-> (ProofAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ProofAddr
paSource ->
    Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
lineKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
naTarget -> case NodeAddr -> Proof -> Maybe ProofAddr
paFromNA NodeAddr
naTarget Proof
p of
      Maybe ProofAddr
Nothing -> Property
forall a. a
discard
      Just ProofAddr
paTarget ->
        if ProofAddr
paTarget ProofAddr -> ProofAddr -> Bool
forall a. Eq a => a -> a -> Bool
== ProofAddr
paSource Bool -> Bool -> Bool
|| ProofAddr
paTarget ProofAddr -> ProofAddr -> Bool
forall a. Eq a => a -> a -> Bool
== ProofAddr
PAProof Bool -> Bool -> Bool
|| ProofAddr
paSource ProofAddr -> ProofAddr -> Bool
forall a. Eq a => a -> a -> Bool
== ProofAddr
PAProof
          then Property
forall a. a
discard
          else case ProofAddr -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paMoveBeforeRaw ProofAddr
paTarget ProofAddr
paSource Proof
p of
            Maybe (ProofAddr, Proof)
Nothing -> Property
forall a. a
discard
            Just (ProofAddr
paTarget', Proof
p') ->
              String -> Property -> Property
forall prop. Testable prop => String -> prop -> Property
counterexample
                ( String
"paTarget="
                    String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofAddr -> String
forall b a. (Show a, IsString b) => a -> b
show ProofAddr
paTarget
                    String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\npaTarget'="
                    String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ProofAddr -> String
forall b a. (Show a, IsString b) => a -> b
show ProofAddr
paTarget'
                    String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"\np'=\n"
                    String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Text -> String
forall a. ToString a => a -> String
toString (Proof -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Proof
p')
                )
                (Property -> Property) -> Property -> Property
forall a b. (a -> b) -> a -> b
$ (Proof -> PrettyProof
PrettyProof (Proof -> PrettyProof) -> Maybe Proof -> Maybe PrettyProof
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofAddr -> Proof -> Maybe Proof
paLookup ProofAddr
paTarget' Proof
p') Maybe PrettyProof -> Maybe PrettyProof -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (Proof -> PrettyProof
PrettyProof (Proof -> PrettyProof) -> Maybe Proof -> Maybe PrettyProof
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofAddr -> Proof -> Maybe Proof
paLookup ProofAddr
paSource Proof
p)

------------------------------------------------------------------------------------------

-- * Properties: Line Number Conversion

{- | 'fromLineNo' followed by 'fromNodeAddr' is the identity on valid line
numbers.

> (fromNodeAddr addr p =<< fromLineNo n p)  ===  Just (Just n)
-}
prop_fromLineNoInverse :: PrettyProof -> Property
prop_fromLineNoInverse :: PrettyProof -> Property
prop_fromLineNoInverse (PrettyProof Proof
p) = Gen Int -> (Int -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll ((Int, Int) -> Gen Int
chooseInt (Int
1, Proof -> Int
pLength Proof
p)) ((Int -> Property) -> Property) -> (Int -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \Int
n ->
  ((NodeAddr -> Proof -> Maybe Int
`fromNodeAddr` Proof
p) (NodeAddr -> Maybe Int) -> Maybe NodeAddr -> Maybe (Maybe Int)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Proof -> Maybe NodeAddr
fromLineNo Int
n Proof
p)
    Maybe (Maybe Int) -> Maybe (Maybe Int) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe Int -> Maybe (Maybe Int)
forall a. a -> Maybe a
Just (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
n)

{- | 'fromNodeAddr' followed by 'fromLineNo' is the identity on valid
t'NodeAddr' values.

> (fromLineNo n p =<< fromNodeAddr a p)  ===  Just (Just a)
-}
prop_fromNodeAddrInverse :: PrettyProof -> Property
prop_fromNodeAddrInverse :: PrettyProof -> Property
prop_fromNodeAddrInverse (PrettyProof Proof
p) = Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
anyInsideKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
a ->
  ((Int -> Proof -> Maybe NodeAddr
`fromLineNo` Proof
p) (Int -> Maybe NodeAddr) -> Maybe Int -> Maybe (Maybe NodeAddr)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
a Proof
p)
    Maybe (Maybe NodeAddr) -> Maybe (Maybe NodeAddr) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe NodeAddr -> Maybe (Maybe NodeAddr)
forall a. a -> Maybe a
Just (NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
a)

------------------------------------------------------------------------------------------

-- * Properties: Ordering on Addresses

{- | The 'Ord' instance for t'NodeAddr' is consistent with line-number
ordering: for any two addresses @a@ and @b@,

@
compare a b  ===  compare (fromNodeAddr a p) (fromNodeAddr b p)
@
-}
prop_compareLineNo :: PrettyProof -> Property
prop_compareLineNo :: PrettyProof -> Property
prop_compareLineNo (PrettyProof Proof
p) =
  Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
anyInsideKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
a ->
    Gen NodeAddr -> (NodeAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> AddrKind -> Gen NodeAddr
arbitraryNodeAddrFor Proof
p AddrKind
anyInsideKind) ((NodeAddr -> Property) -> Property)
-> (NodeAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \NodeAddr
b ->
      NodeAddr -> NodeAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare NodeAddr
a NodeAddr
b
        Ordering -> Ordering -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== Maybe Int -> Maybe Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
a Proof
p) (NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
b Proof
p)

------------------------------------------------------------------------------------------

-- * Properties: Line Range Conversion

{- | 'lineRangeFromProofAddr' followed by 'fromLineRange' is the identity
on valid t'ProofAddr' values.

> (fromLineRange s e p =<< lineRangeFromProofAddr pa p)  ===  Just pa
-}
prop_fromLineRangeInverse :: PrettyProof -> Property
prop_fromLineRangeInverse :: PrettyProof -> Property
prop_fromLineRangeInverse (PrettyProof Proof
p) = Gen ProofAddr -> (ProofAddr -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> Gen ProofAddr
arbitraryProofAddrFor Proof
p) ((ProofAddr -> Property) -> Property)
-> (ProofAddr -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \ProofAddr
pa ->
  ((\(Int
s, Int
e) -> Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
s Int
e Proof
p) ((Int, Int) -> Maybe ProofAddr)
-> Maybe (Int, Int) -> Maybe ProofAddr
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr ProofAddr
pa Proof
p) Maybe ProofAddr -> Maybe ProofAddr -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== ProofAddr -> Maybe ProofAddr
forall a. a -> Maybe a
Just ProofAddr
pa

{- | 'fromLineRange' followed by 'lineRangeFromProofAddr' is the identity
on valid @(start, end)@ line ranges.

> (lineRangeFromProofAddr pa p =<< fromLineRange start end p) ===  Just (start, end)
-}
prop_lineRangeFromProofAddrInverse :: PrettyProof -> Property
prop_lineRangeFromProofAddrInverse :: PrettyProof -> Property
prop_lineRangeFromProofAddrInverse (PrettyProof Proof
p) =
  Gen (Int, Int) -> ((Int, Int) -> Property) -> Property
forall a prop.
(Show a, Testable prop) =>
Gen a -> (a -> prop) -> Property
forAll (Proof -> Gen (Int, Int)
arbitraryLineRangeFor Proof
p) (((Int, Int) -> Property) -> Property)
-> ((Int, Int) -> Property) -> Property
forall a b. (a -> b) -> a -> b
$ \(Int
start, Int
end) ->
    ((ProofAddr -> Proof -> Maybe (Int, Int)
`lineRangeFromProofAddr` Proof
p) (ProofAddr -> Maybe (Int, Int))
-> Maybe ProofAddr -> Maybe (Int, Int)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
start Int
end Proof
p) Maybe (Int, Int) -> Maybe (Int, Int) -> Property
forall a. (Eq a, Show a) => a -> a -> Property
=== (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
start, Int
end)

------------------------------------------------------------------------------------------

-- * Tests

-- | Tests for 'naRemove'
naRemoveQCTests :: TestTree
naRemoveQCTests :: TestTree
naRemoveQCTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"Testing naRemove"
    [ String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_naRemoveMinus1" PrettyProof -> Property
prop_naRemoveMinus1
    , String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_naRemoveShiftLine" PrettyProof -> Property
prop_naRemoveShiftLine
    , String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_naRemoveShiftAssumption" PrettyProof -> Property
prop_naRemoveShiftAssumption
    ]

-- | Tests for 'naInsertBefore'
naInsertBeforeQCTests :: TestTree
naInsertBeforeQCTests :: TestTree
naInsertBeforeQCTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"Testing naInsertBefore"
    [ String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_naInsertBeforeFormulaPlus1" PrettyProof -> Property
prop_naInsertBeforeAssumptionPlus1
    , String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_naInsertBeforeDerivationPlus1" PrettyProof -> Property
prop_naInsertBeforeDerivationPlus1
    , String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty
        String
"prop_naInsertBeforeNaLookupAssumption"
        PrettyProof -> Property
prop_naInsertBeforeNaLookupAssumption
    , String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty
        String
"prop_naInsertBeforeNaLookupDerivation"
        PrettyProof -> Property
prop_naInsertBeforeNaLookupDerivation
    , String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty
        String
"prop_naInsertBeforeRemove"
        PrettyProof -> Property
prop_naInsertBeforeRemove
    ]

-- | Tests for 'paMoveBefore'
paMoveBeforeQCTests :: TestTree
paMoveBeforeQCTests :: TestTree
paMoveBeforeQCTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"Testing paMoveBefore"
    [ String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_paMoveBeforeRawSameProof" PrettyProof -> Property
prop_paMoveBeforeRawSameProof
    ]

-- | Tests regarding the conversion of line numbers and t'NodeAddr's.
lineNoQCTests :: TestTree
lineNoQCTests :: TestTree
lineNoQCTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"Testing conversion of line numbers and NodeAddr"
    [ String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_fromLineNoInverse" PrettyProof -> Property
prop_fromLineNoInverse
    , String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_fromNodeAddrInverse" PrettyProof -> Property
prop_fromNodeAddrInverse
    ]

-- | Tests for compare instances of address types like t'NodeAddr' and t'ProofAddr.
compareQCTests :: TestTree
compareQCTests :: TestTree
compareQCTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"Testing Ord instances"
    [ String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_compareLineNo" PrettyProof -> Property
prop_compareLineNo
    ]

-- | Tests regarding the conversion of line ranges and t'ProofAddr's.
lineRangeQCTests :: TestTree
lineRangeQCTests :: TestTree
lineRangeQCTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"Testing conversion of line ranges and ProofAddr"
    [ String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_fromLineRangeInverse" PrettyProof -> Property
prop_fromLineRangeInverse
    , String -> (PrettyProof -> Property) -> TestTree
forall a. Testable a => String -> a -> TestTree
QC.testProperty String
"prop_lineRangeFromProofAddrInverse" PrettyProof -> Property
prop_lineRangeFromProofAddrInverse
    ]

-- | Groups all tests in this module.
proofTests :: TestTree
proofTests :: TestTree
proofTests =
  String -> [TestTree] -> TestTree
testGroup
    String
"QuickCheck tests for Fitch.Proof"
    [ TestTree
naRemoveQCTests
    , TestTree
naInsertBeforeQCTests
    , TestTree
paMoveBeforeQCTests
    , TestTree
lineNoQCTests
    , TestTree
compareQCTests
    , TestTree
lineRangeQCTests
    ]