{- |
Module      : Fitch.Proof
Copyright   : (c) Leon Vatthauer, 2026
License     : GPL-3
Maintainer  : Leon Vatthauer <leon.vatthauer@fau.de>
Stability   : experimental
Portability : non-portable (ghc-wasm-meta)

This module defines data types for representing Fitch t'Proof's,
together with utilities for pretty-printing, indexing, querying, updating,
and reordering t'Proof's.
-}
module Fitch.Proof where

import Data.List (unsnoc)
import Data.Text qualified as T
import Relude.Extra.Map (toPairs, (!?))
import Relude.Extra.Newtype
import Util

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

-- * Pretty-printing

-- | Type class for pretty printing as t'Text'.
class PrettyPrint a where
  -- | Converts a value to its textual representation.
  prettyPrint :: a -> Text

instance (PrettyPrint a, PrettyPrint b) => PrettyPrint (a, b) where
  prettyPrint :: (PrettyPrint a, PrettyPrint b) => (a, b) -> Text
  prettyPrint :: (PrettyPrint a, PrettyPrint b) => (a, b) -> Text
prettyPrint (a
x, b
y) = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint a
x Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"," Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint b
y Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

instance PrettyPrint Text where
  prettyPrint :: Text -> Text
  prettyPrint :: Text -> Text
prettyPrint = Text -> Text
forall a. a -> a
id

instance (PrettyPrint a) => PrettyPrint [a] where
  prettyPrint :: [a] -> Text
  prettyPrint :: [a] -> Text
prettyPrint [a]
xs = [Text] -> Text
forall t. IsText t "unlines" => [t] -> t
unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ (a -> Text) -> [a] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map a -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint [a]
xs

instance (PrettyPrint a) => PrettyPrint (NonEmpty a) where
  prettyPrint :: NonEmpty a -> Text
  prettyPrint :: NonEmpty a -> Text
prettyPrint (a
x :| [a]
xs) = [a] -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint (a
x a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
xs)

instance (PrettyPrint a, PrettyPrint b) => PrettyPrint (Either a b) where
  prettyPrint :: Either a b -> Text
  prettyPrint :: Either a b -> Text
prettyPrint (Left a
x) = Text
"Left " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint a
x
  prettyPrint (Right b
x) = Text
"Right " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> b -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint b
x

instance (PrettyPrint a) => PrettyPrint (Maybe a) where
  prettyPrint :: Maybe a -> Text
  prettyPrint :: Maybe a -> Text
prettyPrint (Just a
x) = Text
"Just " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint a
x
  prettyPrint Maybe a
Nothing = Text
"Nothing"

instance (PrettyPrint a) => PrettyPrint (Map Name a) where
  prettyPrint :: Map Name a -> Text
  prettyPrint :: Map Text a -> Text
prettyPrint Map Text a
m = [Text] -> Text
forall t. IsText t "unlines" => [t] -> t
unlines ([Text] -> Text) -> [Text] -> Text
forall a b. (a -> b) -> a -> b
$ ((Text, a) -> Text) -> [(Text, a)] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\(Text
n, a
a) -> Text
n Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" |-> " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> a -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint a
a) (Map Text a -> [(Text, a)]
forall t a b. (IsList t, Item t ~ (a, b)) => t -> [(a, b)]
toPairs Map Text a
m)

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

-- * Parsed wrappers

-- | Wraps data with parsing and semantic information.
data Wrapper a where
  -- | Semantically valid parse success.
  ParsedValid :: Text -> a -> Wrapper a
  -- | Semantically invalid parse success.
  ParsedInvalid ::
    -- | User input.
    Text ->
    -- | Error message.
    Text ->
    -- | Inner value.
    a ->
    Wrapper a
  -- | Parse failure.
  Unparsed ::
    -- | User input.
    Text ->
    -- | Error message.
    Text ->
    Wrapper a
  deriving (Int -> Wrapper a -> ShowS
[Wrapper a] -> ShowS
Wrapper a -> String
(Int -> Wrapper a -> ShowS)
-> (Wrapper a -> String)
-> ([Wrapper a] -> ShowS)
-> Show (Wrapper a)
forall a. Show a => Int -> Wrapper a -> ShowS
forall a. Show a => [Wrapper a] -> ShowS
forall a. Show a => Wrapper a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall a. Show a => Int -> Wrapper a -> ShowS
showsPrec :: Int -> Wrapper a -> ShowS
$cshow :: forall a. Show a => Wrapper a -> String
show :: Wrapper a -> String
$cshowList :: forall a. Show a => [Wrapper a] -> ShowS
showList :: [Wrapper a] -> ShowS
Show, Wrapper a -> Wrapper a -> Bool
(Wrapper a -> Wrapper a -> Bool)
-> (Wrapper a -> Wrapper a -> Bool) -> Eq (Wrapper a)
forall a. Eq a => Wrapper a -> Wrapper a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall a. Eq a => Wrapper a -> Wrapper a -> Bool
== :: Wrapper a -> Wrapper a -> Bool
$c/= :: forall a. Eq a => Wrapper a -> Wrapper a -> Bool
/= :: Wrapper a -> Wrapper a -> Bool
Eq)

instance PrettyPrint (Wrapper a) where
  prettyPrint :: Wrapper a -> Text
  prettyPrint :: Wrapper a -> Text
prettyPrint = Wrapper a -> Text
forall a. Wrapper a -> Text
getText

-- | Returns whether a t'Wrapper' represents a parse failure.
isUnparsed :: Wrapper a -> Bool
isUnparsed :: forall a. Wrapper a -> Bool
isUnparsed (Unparsed{}) = Bool
True
isUnparsed Wrapper a
_ = Bool
False

-- | Returns whether a t'Wrapper' represents a semantically valid parse.
isParseValid :: Wrapper a -> Bool
isParseValid :: forall a. Wrapper a -> Bool
isParseValid (ParsedValid{}) = Bool
True
isParseValid Wrapper a
_ = Bool
False

instance Functor Wrapper where
  fmap :: (a -> b) -> Wrapper a -> Wrapper b
  fmap :: forall a b. (a -> b) -> Wrapper a -> Wrapper b
fmap a -> b
f (ParsedValid Text
txt a
x) = Text -> b -> Wrapper b
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt (a -> b
f a
x)
  fmap a -> b
f (ParsedInvalid Text
txt Text
err a
x) = Text -> Text -> b -> Wrapper b
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
err (a -> b
f a
x)
  fmap a -> b
_ (Unparsed Text
txt Text
err) = Text -> Text -> Wrapper b
forall a. Text -> Text -> Wrapper a
Unparsed Text
txt Text
err

-- | Extract data from a wrapper, returns v'Nothing' if no data is present.
fromWrapper :: Wrapper a -> Maybe a
fromWrapper :: forall a. Wrapper a -> Maybe a
fromWrapper (ParsedValid Text
_ a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
fromWrapper (ParsedInvalid Text
_ Text
_ a
x) = a -> Maybe a
forall a. a -> Maybe a
Just a
x
fromWrapper (Unparsed{}) = Maybe a
forall a. Maybe a
Nothing

-- | Extract text value from a wrapper, always succeeds.
getText :: Wrapper a -> Text
getText :: forall a. Wrapper a -> Text
getText (ParsedValid Text
txt a
_) = Text
txt
getText (ParsedInvalid Text
txt Text
_ a
_) = Text
txt
getText (Unparsed Text
txt Text
_) = Text
txt

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

-- | Renders a short preview of a t'Proof' as assumptions followed by its conclusion.
proofPreviewTex :: Proof -> Text
proofPreviewTex :: Proof -> Text
proofPreviewTex (SubProof [Assumption]
fs [Either Derivation Proof]
_ (Derivation Formula
f Wrapper RuleApplication
_)) =
  [Text] -> Text
T.concat [Text]
viewFs
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"⊢\n"
    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Formula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Formula
f
 where
  viewFs :: [Text]
viewFs = (Assumption -> Text) -> [Assumption] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\Assumption
a -> Assumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Assumption
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n") [Assumption]
fs

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

-- * Proof Types

-- | Type of symbolic names such as variables, predicates, rules, and operators.
type Name = Text

{- | A term in first-order logics consists either of a variable or
a function applied to terms.
-}
data Term
  = -- | A single variable in first-order logic
    Var Name
  | -- | A function applied to terms in first-order logic
    Fun Name [Term]
  deriving (Term -> Term -> Bool
(Term -> Term -> Bool) -> (Term -> Term -> Bool) -> Eq Term
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Term -> Term -> Bool
== :: Term -> Term -> Bool
$c/= :: Term -> Term -> Bool
/= :: Term -> Term -> Bool
Eq, Eq Term
Eq Term =>
(Term -> Term -> Ordering)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Bool)
-> (Term -> Term -> Term)
-> (Term -> Term -> Term)
-> Ord Term
Term -> Term -> Bool
Term -> Term -> Ordering
Term -> Term -> Term
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
$ccompare :: Term -> Term -> Ordering
compare :: Term -> Term -> Ordering
$c< :: Term -> Term -> Bool
< :: Term -> Term -> Bool
$c<= :: Term -> Term -> Bool
<= :: Term -> Term -> Bool
$c> :: Term -> Term -> Bool
> :: Term -> Term -> Bool
$c>= :: Term -> Term -> Bool
>= :: Term -> Term -> Bool
$cmax :: Term -> Term -> Term
max :: Term -> Term -> Term
$cmin :: Term -> Term -> Term
min :: Term -> Term -> Term
Ord, Int -> Term -> ShowS
[Term] -> ShowS
Term -> String
(Int -> Term -> ShowS)
-> (Term -> String) -> ([Term] -> ShowS) -> Show Term
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Term -> ShowS
showsPrec :: Int -> Term -> ShowS
$cshow :: Term -> String
show :: Term -> String
$cshowList :: [Term] -> ShowS
showList :: [Term] -> ShowS
Show)

-- | Returns whether a t'Term' is a function application.
isFun :: Term -> Bool
isFun :: Term -> Bool
isFun (Fun{}) = Bool
True
isFun Term
_ = Bool
False

instance PrettyPrint Term where
  prettyPrint :: Term -> Text
  prettyPrint :: Term -> Text
prettyPrint (Var Text
v) = Text
v
  prettyPrint (Fun Text
f []) = Text
f
  prettyPrint (Fun Text
f [Term]
ts) = Text
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
"," ((Term -> Text) -> [Term] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint [Term]
ts) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"

{- | A formula of first-order logic.
It can also represent propositional formulae by using v'Pred' without any t'Term's.
-}
data RawFormula
  = -- | A predicate applied to terms.
    Pred Name [Term]
  | -- | A predicate written in infix notation.
    InfixPred Name Term Term
  | -- | An n-ary operator, like @->@ for implication, or @~@ for negation.
    Opr Text [RawFormula]
  | -- | A quantifier, like @∀@ for universal quantification.
    Quantifier Name Name RawFormula
  deriving (RawFormula -> RawFormula -> Bool
(RawFormula -> RawFormula -> Bool)
-> (RawFormula -> RawFormula -> Bool) -> Eq RawFormula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RawFormula -> RawFormula -> Bool
== :: RawFormula -> RawFormula -> Bool
$c/= :: RawFormula -> RawFormula -> Bool
/= :: RawFormula -> RawFormula -> Bool
Eq, Eq RawFormula
Eq RawFormula =>
(RawFormula -> RawFormula -> Ordering)
-> (RawFormula -> RawFormula -> Bool)
-> (RawFormula -> RawFormula -> Bool)
-> (RawFormula -> RawFormula -> Bool)
-> (RawFormula -> RawFormula -> Bool)
-> (RawFormula -> RawFormula -> RawFormula)
-> (RawFormula -> RawFormula -> RawFormula)
-> Ord RawFormula
RawFormula -> RawFormula -> Bool
RawFormula -> RawFormula -> Ordering
RawFormula -> RawFormula -> RawFormula
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
$ccompare :: RawFormula -> RawFormula -> Ordering
compare :: RawFormula -> RawFormula -> Ordering
$c< :: RawFormula -> RawFormula -> Bool
< :: RawFormula -> RawFormula -> Bool
$c<= :: RawFormula -> RawFormula -> Bool
<= :: RawFormula -> RawFormula -> Bool
$c> :: RawFormula -> RawFormula -> Bool
> :: RawFormula -> RawFormula -> Bool
$c>= :: RawFormula -> RawFormula -> Bool
>= :: RawFormula -> RawFormula -> Bool
$cmax :: RawFormula -> RawFormula -> RawFormula
max :: RawFormula -> RawFormula -> RawFormula
$cmin :: RawFormula -> RawFormula -> RawFormula
min :: RawFormula -> RawFormula -> RawFormula
Ord, Int -> RawFormula -> ShowS
[RawFormula] -> ShowS
RawFormula -> String
(Int -> RawFormula -> ShowS)
-> (RawFormula -> String)
-> ([RawFormula] -> ShowS)
-> Show RawFormula
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RawFormula -> ShowS
showsPrec :: Int -> RawFormula -> ShowS
$cshow :: RawFormula -> String
show :: RawFormula -> String
$cshowList :: [RawFormula] -> ShowS
showList :: [RawFormula] -> ShowS
Show)

instance PrettyPrint RawFormula where
  prettyPrint :: RawFormula -> Text
  prettyPrint :: RawFormula -> Text
prettyPrint RawFormula
f = Bool -> RawFormula -> Text
go Bool
False RawFormula
f
   where
    go :: Bool -> RawFormula -> Text
    go :: Bool -> RawFormula -> Text
go Bool
_ (Pred Text
p []) = Text
p
    go Bool
_ (Pred Text
p [Term]
ts) = Text
p Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
"," ((Term -> Text) -> [Term] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Term -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint [Term]
ts) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
    go Bool
True RawFormula
f = Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Bool -> RawFormula -> Text
go Bool
False RawFormula
f Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
    go Bool
False (InfixPred Text
p Term
t1 Term
t2) = Term -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Term
t1 Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
p Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Term -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Term
t2
    go Bool
False (Opr Text
op [RawFormula]
fs)
      | [RawFormula] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [RawFormula]
fs = Text
op
      | [RawFormula] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [RawFormula]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
2 = Text -> [Text] -> Text
T.intercalate Text
op ((RawFormula -> Text) -> [RawFormula] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (Bool -> RawFormula -> Text
go Bool
True) [RawFormula]
fs)
      | Bool
otherwise = Text
op Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"(" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
"," ((RawFormula -> Text) -> [RawFormula] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint [RawFormula]
fs) Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
    go Bool
False (Quantifier Text
q Text
v RawFormula
f) = Text
q Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"." Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
f

-- | A reference to either a single line or a whole subproof.
data Reference where
  -- | Referencing a single line.
  LineReference :: Int -> Reference
  -- | Referencing a subproof by its line range.
  ProofReference :: Int -> Int -> Reference
  deriving (Int -> Reference -> ShowS
[Reference] -> ShowS
Reference -> String
(Int -> Reference -> ShowS)
-> (Reference -> String)
-> ([Reference] -> ShowS)
-> Show Reference
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Reference -> ShowS
showsPrec :: Int -> Reference -> ShowS
$cshow :: Reference -> String
show :: Reference -> String
$cshowList :: [Reference] -> ShowS
showList :: [Reference] -> ShowS
Show, Reference -> Reference -> Bool
(Reference -> Reference -> Bool)
-> (Reference -> Reference -> Bool) -> Eq Reference
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Reference -> Reference -> Bool
== :: Reference -> Reference -> Bool
$c/= :: Reference -> Reference -> Bool
/= :: Reference -> Reference -> Bool
Eq)

instance PrettyPrint Reference where
  prettyPrint :: Reference -> Text
  prettyPrint :: Reference -> Text
prettyPrint (LineReference Int
n) = Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n
  prettyPrint (ProofReference Int
start Int
end) = Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
start Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"-" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
end

-- | A formula with parsing and semantic information.
type Formula = Wrapper RawFormula

-- | The raw content of an t'Assumption'.
data RawAssumption
  = -- | A fresh variable of a t'Proof', written like @[c]@.
    FreshVar Name
  | -- | A regular t'RawFormula'.
    RawAssumption RawFormula
  deriving (RawAssumption -> RawAssumption -> Bool
(RawAssumption -> RawAssumption -> Bool)
-> (RawAssumption -> RawAssumption -> Bool) -> Eq RawAssumption
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RawAssumption -> RawAssumption -> Bool
== :: RawAssumption -> RawAssumption -> Bool
$c/= :: RawAssumption -> RawAssumption -> Bool
/= :: RawAssumption -> RawAssumption -> Bool
Eq, Int -> RawAssumption -> ShowS
[RawAssumption] -> ShowS
RawAssumption -> String
(Int -> RawAssumption -> ShowS)
-> (RawAssumption -> String)
-> ([RawAssumption] -> ShowS)
-> Show RawAssumption
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RawAssumption -> ShowS
showsPrec :: Int -> RawAssumption -> ShowS
$cshow :: RawAssumption -> String
show :: RawAssumption -> String
$cshowList :: [RawAssumption] -> ShowS
showList :: [RawAssumption] -> ShowS
Show)

{- | A wrapped assumption together with its attached t'RuleApplication'
for easily converting between t'Assumption' and t'Derivation'.
-}
type Assumption = (Wrapper RawAssumption, Wrapper RuleApplication)

-- | Constructs an t'Assumption' with the default rule @(⊤I)@.
mkAssumption :: Wrapper RawAssumption -> Assumption
mkAssumption :: Wrapper RawAssumption -> Assumption
mkAssumption Wrapper RawAssumption
w = (Wrapper RawAssumption
w, Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> a -> Wrapper a
ParsedValid Text
"(⊤I)" (Text -> [Reference] -> RuleApplication
RuleApplication Text
"⊤I" []))

instance {-# OVERLAPPING #-} PrettyPrint Assumption where
  prettyPrint :: Assumption -> Text
  prettyPrint :: Assumption -> Text
prettyPrint = Wrapper RawAssumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint (Wrapper RawAssumption -> Text)
-> (Assumption -> Wrapper RawAssumption) -> Assumption -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assumption -> Wrapper RawAssumption
forall a b. (a, b) -> a
fst

{- | Converts a t'Derivation' into an t'Assumption' by wrapping its formula
as a t'RawAssumption'.
-}
toAssumption :: Derivation -> Assumption
toAssumption :: Derivation -> Assumption
toAssumption (Derivation (Unparsed Text
txt Text
err) Wrapper RuleApplication
ra) = (Text -> Text -> Wrapper RawAssumption
forall a. Text -> Text -> Wrapper a
Unparsed Text
txt Text
err, Wrapper RuleApplication
ra)
toAssumption (Derivation (ParsedInvalid Text
txt Text
err RawFormula
f) Wrapper RuleApplication
ra) =
  (Text -> Text -> RawAssumption -> Wrapper RawAssumption
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
err (RawFormula -> RawAssumption
RawAssumption RawFormula
f), Wrapper RuleApplication
ra)
toAssumption (Derivation (ParsedValid Text
txt RawFormula
f) Wrapper RuleApplication
ra) = (Text -> RawAssumption -> Wrapper RawAssumption
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt (RawFormula -> RawAssumption
RawAssumption RawFormula
f), Wrapper RuleApplication
ra)

{- | Converts an t'Assumption' into a t'Derivation'.
Fresh-variable assumptions cannot be converted to formulas and are therefore turned
into v'Unparsed'.
-}
toDerivation :: Assumption -> Derivation
toDerivation :: Assumption -> Derivation
toDerivation (Unparsed Text
txt Text
err, Wrapper RuleApplication
ra) = Formula -> Wrapper RuleApplication -> Derivation
Derivation (Text -> Text -> Formula
forall a. Text -> Text -> Wrapper a
Unparsed Text
txt Text
err) Wrapper RuleApplication
ra
toDerivation (ParsedInvalid Text
txt Text
err (RawAssumption RawFormula
f), Wrapper RuleApplication
ra) =
  Formula -> Wrapper RuleApplication -> Derivation
Derivation (Text -> Text -> RawFormula -> Formula
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
err RawFormula
f) Wrapper RuleApplication
ra
toDerivation (ParsedInvalid Text
txt Text
err a :: RawAssumption
a@(FreshVar Text
v), Wrapper RuleApplication
ra) =
  Formula -> Wrapper RuleApplication -> Derivation
Derivation (Text -> Text -> Formula
forall a. Text -> Text -> Wrapper a
Unparsed (RawAssumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawAssumption
a) (Text
"Could not parse " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawAssumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawAssumption
a)) Wrapper RuleApplication
ra
toDerivation (ParsedValid Text
txt (RawAssumption RawFormula
f), Wrapper RuleApplication
ra) =
  Formula -> Wrapper RuleApplication -> Derivation
Derivation (Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawFormula
f) Wrapper RuleApplication
ra
toDerivation (ParsedValid Text
txt a :: RawAssumption
a@(FreshVar Text
v), Wrapper RuleApplication
ra) =
  Formula -> Wrapper RuleApplication -> Derivation
Derivation (Text -> Text -> Formula
forall a. Text -> Text -> Wrapper a
Unparsed (RawAssumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawAssumption
a) (Text
"Could not parse " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawAssumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawAssumption
a)) Wrapper RuleApplication
ra

instance PrettyPrint RawAssumption where
  prettyPrint :: RawAssumption -> Text
  prettyPrint :: RawAssumption -> Text
prettyPrint (RawAssumption RawFormula
f) = RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
f
  prettyPrint (FreshVar Text
v) = Text
"[" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"]"

-- | Application of a rule.
data RuleApplication
  = -- | Application of a rule, consisting of the rule t'Name' and a list of t'Reference's.
    RuleApplication Name [Reference]
  deriving (Int -> RuleApplication -> ShowS
[RuleApplication] -> ShowS
RuleApplication -> String
(Int -> RuleApplication -> ShowS)
-> (RuleApplication -> String)
-> ([RuleApplication] -> ShowS)
-> Show RuleApplication
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> RuleApplication -> ShowS
showsPrec :: Int -> RuleApplication -> ShowS
$cshow :: RuleApplication -> String
show :: RuleApplication -> String
$cshowList :: [RuleApplication] -> ShowS
showList :: [RuleApplication] -> ShowS
Show, RuleApplication -> RuleApplication -> Bool
(RuleApplication -> RuleApplication -> Bool)
-> (RuleApplication -> RuleApplication -> Bool)
-> Eq RuleApplication
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: RuleApplication -> RuleApplication -> Bool
== :: RuleApplication -> RuleApplication -> Bool
$c/= :: RuleApplication -> RuleApplication -> Bool
/= :: RuleApplication -> RuleApplication -> Bool
Eq)

instance {-# OVERLAPPING #-} PrettyPrint (Wrapper RuleApplication) where
  prettyPrint :: Wrapper RuleApplication -> Text
  prettyPrint :: Wrapper RuleApplication -> Text
prettyPrint (Unparsed Text
"" Text
_) = Text
"()"
  prettyPrint Wrapper RuleApplication
w = Wrapper RuleApplication -> Text
forall a. Wrapper a -> Text
getText Wrapper RuleApplication
w

instance PrettyPrint RuleApplication where
  prettyPrint :: RuleApplication -> Text
  prettyPrint :: RuleApplication -> Text
prettyPrint (RuleApplication Text
n [Reference]
refs) =
    Text
"("
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")"
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" "
      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> [Text] -> Text
T.intercalate Text
"," ((Reference -> Text) -> [Reference] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Reference -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint [Reference]
refs)

-- | A derivation inside a t'Proof'.
data Derivation
  = {- | A single proof line consisting of a t'Formula'
    and the t'RuleApplication' that justifies it.
    -}
    Derivation Formula (Wrapper RuleApplication)
  deriving (Int -> Derivation -> ShowS
[Derivation] -> ShowS
Derivation -> String
(Int -> Derivation -> ShowS)
-> (Derivation -> String)
-> ([Derivation] -> ShowS)
-> Show Derivation
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Derivation -> ShowS
showsPrec :: Int -> Derivation -> ShowS
$cshow :: Derivation -> String
show :: Derivation -> String
$cshowList :: [Derivation] -> ShowS
showList :: [Derivation] -> ShowS
Show, Derivation -> Derivation -> Bool
(Derivation -> Derivation -> Bool)
-> (Derivation -> Derivation -> Bool) -> Eq Derivation
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Derivation -> Derivation -> Bool
== :: Derivation -> Derivation -> Bool
$c/= :: Derivation -> Derivation -> Bool
/= :: Derivation -> Derivation -> Bool
Eq)

instance PrettyPrint Derivation where
  prettyPrint :: Derivation -> Text
  prettyPrint :: Derivation -> Text
prettyPrint (Derivation Formula
a Wrapper RuleApplication
ra) = Formula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Formula
a Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Wrapper RuleApplication -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Wrapper RuleApplication
ra

-- | A datatype for representing Fitch-style proofs.
data Proof where
  {- | A sub proof consisting of t'Assumption's, t'Derivation's,
  nested t'Proof's, and a conclusion.
  -}
  SubProof :: [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
  deriving (Proof -> Proof -> Bool
(Proof -> Proof -> Bool) -> (Proof -> Proof -> Bool) -> Eq Proof
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Proof -> Proof -> Bool
== :: Proof -> Proof -> Bool
$c/= :: Proof -> Proof -> Bool
/= :: Proof -> Proof -> Bool
Eq, Int -> Proof -> ShowS
[Proof] -> ShowS
Proof -> String
(Int -> Proof -> ShowS)
-> (Proof -> String) -> ([Proof] -> ShowS) -> Show Proof
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Proof -> ShowS
showsPrec :: Int -> Proof -> ShowS
$cshow :: Proof -> String
show :: Proof -> String
$cshowList :: [Proof] -> ShowS
showList :: [Proof] -> ShowS
Show)

instance PrettyPrint Proof where
  prettyPrint :: Proof -> Text
  prettyPrint :: Proof -> Text
prettyPrint Proof
p = Int -> Int -> Proof -> Text
pretty' Int
1 Int
0 Proof
p
   where
    lineNoLen :: Int
    lineNoLen :: Int
lineNoLen = Text -> Int
T.length (Text -> Int) -> (Int -> Text) -> Int -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text
forall b a. (Show a, IsString b) => a -> b
show (Int -> Int) -> Int -> Int
forall a b. (a -> b) -> a -> b
$ Proof -> Int
pLength Proof
p
    withLevel :: Int -> Text -> Text
    withLevel :: Int -> Text -> Text
withLevel Int
level Text
t = Int -> Text -> Text
T.replicate Int
level Text
"|" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n"
    withLine :: Int -> Text -> Text
    withLine :: Int -> Text -> Text
withLine Int
line Text
t = Text
lineNo Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
padding Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
t
     where
      lineNo :: Text
lineNo = Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
line
      padding :: Text
padding = Int -> Text -> Text
T.replicate (Int
lineNoLen Int -> Int -> Int
forall a. Num a => a -> a -> a
- Text -> Int
T.length Text
lineNo) Text
" "
    withoutLine :: Text -> Text
    withoutLine :: Text -> Text
withoutLine = (Int -> Text -> Text
T.replicate (Int
lineNoLen Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Text
" " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>)
    pretty' :: Int -> Int -> Proof -> Text
    pretty' :: Int -> Int -> Proof -> Text
pretty' Int
line Int
level (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
      [Text] -> Text
T.concat [Text]
fsShow
        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
withoutLine (Int -> Text -> Text
withLevel (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Text
"---")
        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> [Text] -> Text
T.concat [Text]
psShow
        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
cShow
     where
      (Int
line', [Text]
fsShow) =
        (Int -> Assumption -> (Int, Text))
-> Int -> [Assumption] -> (Int, [Text])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
          (\Int
ln Assumption
f -> (Int
ln Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int -> Text -> Text
withLine Int
ln (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
withLevel (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Assumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Assumption
f))
          Int
line
          [Assumption]
fs
      (Int
line'', [Text]
psShow) =
        (Int -> Either Derivation Proof -> (Int, Text))
-> Int -> [Either Derivation Proof] -> (Int, [Text])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
          ( \Int
ln' Either Derivation Proof
e ->
              ( Int
ln' Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Derivation -> Int)
-> (Proof -> Int) -> Either Derivation Proof -> Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Int -> Derivation -> Int
forall a b. a -> b -> a
const Int
1) Proof -> Int
pLength Either Derivation Proof
e
              , (Derivation -> Text)
-> (Proof -> Text) -> Either Derivation Proof -> Text
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
                  (Int -> Text -> Text
withLine Int
ln' (Text -> Text) -> (Derivation -> Text) -> Derivation -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Text -> Text
withLevel (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Text -> Text) -> (Derivation -> Text) -> Derivation -> Text
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint)
                  (Int -> Int -> Proof -> Text
pretty' Int
ln' (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1))
                  Either Derivation Proof
e
              )
          )
          Int
line'
          [Either Derivation Proof]
ps
      cShow :: Text
cShow = Int -> Text -> Text
withLine Int
line'' (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Int -> Text -> Text
withLevel (Int
level Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Text -> Text) -> Text -> Text
forall a b. (a -> b) -> a -> b
$ Derivation -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Derivation
c

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

-- * Folds and Maps

{- | @'pFoldLines' af df s p@ folds the proof @p@ line-wise to a value
of type @a@ with starting value @s@.
-}
pFoldLines ::
  (a -> Assumption -> a) ->
  (a -> Derivation -> a) ->
  a ->
  Proof ->
  a
pFoldLines :: forall a.
(a -> Assumption -> a) -> (a -> Derivation -> a) -> a -> Proof -> a
pFoldLines a -> Assumption -> a
af a -> Derivation -> a
df a
s (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  a -> Derivation -> a
df
    ( (a -> Either Derivation Proof -> a)
-> a -> [Either Derivation Proof] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl'
        ( \a
s' ->
            (Derivation -> a) -> (Proof -> a) -> Either Derivation Proof -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              (a -> Derivation -> a
df a
s')
              ((a -> Assumption -> a) -> (a -> Derivation -> a) -> a -> Proof -> a
forall a.
(a -> Assumption -> a) -> (a -> Derivation -> a) -> a -> Proof -> a
pFoldLines a -> Assumption -> a
af a -> Derivation -> a
df a
s')
        )
        ((a -> Assumption -> a) -> a -> [Assumption] -> a
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' a -> Assumption -> a
af a
s [Assumption]
fs)
        [Either Derivation Proof]
ps
    )
    Derivation
c

-- | The 'pLength' of a t'Proof' is its total number of lines.
pLength :: Proof -> Int
pLength :: Proof -> Int
pLength = (Int -> Assumption -> Int)
-> (Int -> Derivation -> Int) -> Int -> Proof -> Int
forall a.
(a -> Assumption -> a) -> (a -> Derivation -> a) -> a -> Proof -> a
pFoldLines (\Int
n Assumption
_ -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (\Int
n Derivation
_ -> Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
0

-- | Monadic variant of 'pFoldLines'.
pFoldLinesM ::
  (Monad m) =>
  (a -> Assumption -> m a) ->
  (a -> Derivation -> m a) ->
  a ->
  Proof ->
  m a
pFoldLinesM :: forall (m :: * -> *) a.
Monad m =>
(a -> Assumption -> m a)
-> (a -> Derivation -> m a) -> a -> Proof -> m a
pFoldLinesM a -> Assumption -> m a
af a -> Derivation -> m a
df a
s (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) = do
  result1 <- (a -> Assumption -> m a) -> a -> [Assumption] -> m a
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM a -> Assumption -> m a
af a
s [Assumption]
fs
  result2 <- foldlM (\a
s' -> (Derivation -> m a)
-> (Proof -> m a) -> Either Derivation Proof -> m a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (a -> Derivation -> m a
df a
s') ((a -> Assumption -> m a)
-> (a -> Derivation -> m a) -> a -> Proof -> m a
forall (m :: * -> *) a.
Monad m =>
(a -> Assumption -> m a)
-> (a -> Derivation -> m a) -> a -> Proof -> m a
pFoldLinesM a -> Assumption -> m a
af a -> Derivation -> m a
df a
s')) result1 ps
  df result2 d

{- | Serializes a t'Proof' by mapping t'Assumption's, t'Derivation's, t'Proof's,
and conclusions.
Nested proofs are first serialized recursively
and then combined with the given proof function.
-}
pSerialize ::
  (Assumption -> a) ->
  (Derivation -> a) ->
  ([a] -> a) ->
  (Derivation -> a) ->
  Proof ->
  [a]
pSerialize :: forall a.
(Assumption -> a)
-> (Derivation -> a)
-> ([a] -> a)
-> (Derivation -> a)
-> Proof
-> [a]
pSerialize Assumption -> a
af Derivation -> a
df [a] -> a
pf Derivation -> a
cf (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (Assumption -> a) -> [Assumption] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Assumption -> a
af [Assumption]
fs
    [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> (Either Derivation Proof -> a) -> [Either Derivation Proof] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((Derivation -> a) -> (Proof -> a) -> Either Derivation Proof -> a
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Derivation -> a
df ([a] -> a
pf ([a] -> a) -> (Proof -> [a]) -> Proof -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assumption -> a)
-> (Derivation -> a)
-> ([a] -> a)
-> (Derivation -> a)
-> Proof
-> [a]
forall a.
(Assumption -> a)
-> (Derivation -> a)
-> ([a] -> a)
-> (Derivation -> a)
-> Proof
-> [a]
pSerialize Assumption -> a
af Derivation -> a
df [a] -> a
pf Derivation -> a
cf)) [Either Derivation Proof]
ps
    [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> OneItem [a] -> [a]
forall x. One x => OneItem x -> x
one (Derivation -> a
cf Derivation
c)

{- | 'pSerializeLines' @af@ @df@ @p@ serializes the t'Proof' @p@ line-by-line,
applying @af@ to each t'Assumption' and @df@ to each t'Derivation',
and collecting the results into a flat list.
-}
pSerializeLines :: (Assumption -> a) -> (Derivation -> a) -> Proof -> [a]
pSerializeLines :: forall a. (Assumption -> a) -> (Derivation -> a) -> Proof -> [a]
pSerializeLines Assumption -> a
af Derivation -> a
df (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) =
  (Assumption -> a) -> [Assumption] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map Assumption -> a
af [Assumption]
fs
    [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> (Either Derivation Proof -> [a])
-> [Either Derivation Proof] -> [a]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Derivation -> [a])
-> (Proof -> [a]) -> Either Derivation Proof -> [a]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (a -> [a]
OneItem [a] -> [a]
forall x. One x => OneItem x -> x
one (a -> [a]) -> (Derivation -> a) -> Derivation -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation -> a
df) ((Assumption -> a) -> (Derivation -> a) -> Proof -> [a]
forall a. (Assumption -> a) -> (Derivation -> a) -> Proof -> [a]
pSerializeLines Assumption -> a
af Derivation -> a
df)) [Either Derivation Proof]
ps
    [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> OneItem [a] -> [a]
forall x. One x => OneItem x -> x
one (Derivation -> a
df Derivation
d)

{- | Like 'pSerializeLines' but also passes the current t'NodeAddr'
to each mapping function.
-}
pSerializeLinesWithAddr ::
  (NodeAddr -> Assumption -> a) ->
  (NodeAddr -> Derivation -> a) ->
  Proof ->
  [a]
pSerializeLinesWithAddr :: forall a.
(NodeAddr -> Assumption -> a)
-> (NodeAddr -> Derivation -> a) -> Proof -> [a]
pSerializeLinesWithAddr = (NodeAddr -> NodeAddr)
-> (NodeAddr -> Assumption -> a)
-> (NodeAddr -> Derivation -> a)
-> Proof
-> [a]
forall a.
(NodeAddr -> NodeAddr)
-> (NodeAddr -> Assumption -> a)
-> (NodeAddr -> Derivation -> a)
-> Proof
-> [a]
go NodeAddr -> NodeAddr
forall a. a -> a
id
 where
  go ::
    (NodeAddr -> NodeAddr) ->
    (NodeAddr -> Assumption -> a) ->
    (NodeAddr -> Derivation -> a) ->
    Proof ->
    [a]
  go :: forall a.
(NodeAddr -> NodeAddr)
-> (NodeAddr -> Assumption -> a)
-> (NodeAddr -> Derivation -> a)
-> Proof
-> [a]
go NodeAddr -> NodeAddr
getNA NodeAddr -> Assumption -> a
af NodeAddr -> Derivation -> a
df (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) =
    [a]
mappedFs
      [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [[a]] -> [a]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[a]]
mappedPs
      [a] -> [a] -> [a]
forall a. Semigroup a => a -> a -> a
<> [NodeAddr -> Derivation -> a
df (NodeAddr -> NodeAddr
getNA NodeAddr
NAConclusion) Derivation
d]
   where
    (Int
_, [a]
mappedFs) = (Int -> Assumption -> (Int, a))
-> Int -> [Assumption] -> (Int, [a])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (\Int
m Assumption
frm -> (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, NodeAddr -> Assumption -> a
af (NodeAddr -> NodeAddr
getNA (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NAAssumption Int
m) Assumption
frm)) Int
0 [Assumption]
fs
    (Int
_, [[a]]
mappedPs) =
      (Int -> Either Derivation Proof -> (Int, [a]))
-> Int -> [Either Derivation Proof] -> (Int, [[a]])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
        ( \Int
m Either Derivation Proof
e ->
            ( Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
            , (Derivation -> [a])
-> (Proof -> [a]) -> Either Derivation Proof -> [a]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
                (a -> [a]
OneItem [a] -> [a]
forall x. One x => OneItem x -> x
one (a -> [a]) -> (Derivation -> a) -> Derivation -> [a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeAddr -> Derivation -> a
df (NodeAddr -> NodeAddr
getNA (Int -> NodeAddr
NALine Int
m)))
                ((NodeAddr -> NodeAddr)
-> (NodeAddr -> Assumption -> a)
-> (NodeAddr -> Derivation -> a)
-> Proof
-> [a]
forall a.
(NodeAddr -> NodeAddr)
-> (NodeAddr -> Assumption -> a)
-> (NodeAddr -> Derivation -> a)
-> Proof
-> [a]
go (NodeAddr -> NodeAddr
getNA (NodeAddr -> NodeAddr)
-> (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr -> NodeAddr
NAProof Int
m) NodeAddr -> Assumption -> a
af NodeAddr -> Derivation -> a
df)
                Either Derivation Proof
e
            )
        )
        Int
0
        [Either Derivation Proof]
ps

{- | @'pMapLines' af df p@ maps each line of the t'Proof' @p@,
applying @af@ to every t'Assumption' and @df@ to every t'Derivation'.
-}
pMapLines ::
  (Assumption -> Assumption) ->
  (Derivation -> Derivation) ->
  Proof ->
  Proof
pMapLines :: (Assumption -> Assumption)
-> (Derivation -> Derivation) -> Proof -> Proof
pMapLines Assumption -> Assumption
af Derivation -> Derivation
df (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) =
  [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof
    ((Assumption -> Assumption) -> [Assumption] -> [Assumption]
forall a b. (a -> b) -> [a] -> [b]
map Assumption -> Assumption
af [Assumption]
fs)
    ((Either Derivation Proof -> Either Derivation Proof)
-> [Either Derivation Proof] -> [Either Derivation Proof]
forall a b. (a -> b) -> [a] -> [b]
map ((Derivation -> Derivation)
-> (Proof -> Proof)
-> Either Derivation Proof
-> Either Derivation Proof
forall a b c d. (a -> b) -> (c -> d) -> Either a c -> Either b d
forall (p :: * -> * -> *) a b c d.
Bifunctor p =>
(a -> b) -> (c -> d) -> p a c -> p b d
bimap Derivation -> Derivation
df ((Assumption -> Assumption)
-> (Derivation -> Derivation) -> Proof -> Proof
pMapLines Assumption -> Assumption
af Derivation -> Derivation
df)) [Either Derivation Proof]
ps)
    (Derivation -> Derivation
df Derivation
d)

-- | Like 'pMapLines', but threads an accumulator from left to right.
pMapLinesAccumL ::
  (s -> Assumption -> (s, Assumption)) ->
  (s -> Derivation -> (s, Derivation)) ->
  s ->
  Proof ->
  (s, Proof)
pMapLinesAccumL :: forall s.
(s -> Assumption -> (s, Assumption))
-> (s -> Derivation -> (s, Derivation)) -> s -> Proof -> (s, Proof)
pMapLinesAccumL s -> Assumption -> (s, Assumption)
af s -> Derivation -> (s, Derivation)
df s
s (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) =
  let
    (s
s', [Assumption]
fs') = (s -> Assumption -> (s, Assumption))
-> s -> [Assumption] -> (s, [Assumption])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL s -> Assumption -> (s, Assumption)
af s
s [Assumption]
fs
    (s
s'', [Either Derivation Proof]
ps') =
      (s -> Either Derivation Proof -> (s, Either Derivation Proof))
-> s -> [Either Derivation Proof] -> (s, [Either Derivation Proof])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
        (\s
a Either Derivation Proof
e -> (Derivation -> (s, Either Derivation Proof))
-> (Proof -> (s, Either Derivation Proof))
-> Either Derivation Proof
-> (s, Either Derivation Proof)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((Derivation -> Either Derivation Proof)
-> (s, Derivation) -> (s, Either Derivation Proof)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left ((s, Derivation) -> (s, Either Derivation Proof))
-> (Derivation -> (s, Derivation))
-> Derivation
-> (s, Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> Derivation -> (s, Derivation)
df s
a) ((Proof -> Either Derivation Proof)
-> (s, Proof) -> (s, Either Derivation Proof)
forall b c a. (b -> c) -> (a, b) -> (a, c)
forall (p :: * -> * -> *) b c a.
Bifunctor p =>
(b -> c) -> p a b -> p a c
second Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right ((s, Proof) -> (s, Either Derivation Proof))
-> (Proof -> (s, Proof)) -> Proof -> (s, Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (s -> Assumption -> (s, Assumption))
-> (s -> Derivation -> (s, Derivation)) -> s -> Proof -> (s, Proof)
forall s.
(s -> Assumption -> (s, Assumption))
-> (s -> Derivation -> (s, Derivation)) -> s -> Proof -> (s, Proof)
pMapLinesAccumL s -> Assumption -> (s, Assumption)
af s -> Derivation -> (s, Derivation)
df s
a) Either Derivation Proof
e)
        s
s'
        [Either Derivation Proof]
ps
    (s
s''', Derivation
d') = s -> Derivation -> (s, Derivation)
df s
s'' Derivation
d
   in
    (s
s''', [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs' [Either Derivation Proof]
ps' Derivation
d')

-- | Like 'pMapLines', but also passes the current line number to the mapping functions.
pMapLinesWithLineNo ::
  (Int -> Assumption -> Assumption) ->
  (Int -> Derivation -> Derivation) ->
  Proof ->
  Proof
pMapLinesWithLineNo :: (Int -> Assumption -> Assumption)
-> (Int -> Derivation -> Derivation) -> Proof -> Proof
pMapLinesWithLineNo Int -> Assumption -> Assumption
af Int -> Derivation -> Derivation
df = (Int, Proof) -> Proof
forall a b. (a, b) -> b
snd ((Int, Proof) -> Proof)
-> (Proof -> (Int, Proof)) -> Proof -> Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> Assumption -> (Int, Assumption))
-> (Int -> Derivation -> (Int, Derivation))
-> Int
-> Proof
-> (Int, Proof)
forall s.
(s -> Assumption -> (s, Assumption))
-> (s -> Derivation -> (s, Derivation)) -> s -> Proof -> (s, Proof)
pMapLinesAccumL Int -> Assumption -> (Int, Assumption)
af' Int -> Derivation -> (Int, Derivation)
df' Int
1
 where
  af' :: Int -> Assumption -> (Int, Assumption)
  af' :: Int -> Assumption -> (Int, Assumption)
af' Int
n Assumption
a = (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int -> Assumption -> Assumption
af Int
n Assumption
a)
  df' :: Int -> Derivation -> (Int, Derivation)
  df' :: Int -> Derivation -> (Int, Derivation)
df' Int
n Derivation
d = (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Int -> Derivation -> Derivation
df Int
n Derivation
d)

-- | Like 'pMapLines', but also passes the current t'NodeAddr' to the mapping functions.
pMapLinesWithAddr ::
  (NodeAddr -> Assumption -> Assumption) ->
  (NodeAddr -> Derivation -> Derivation) ->
  Proof ->
  Proof
pMapLinesWithAddr :: (NodeAddr -> Assumption -> Assumption)
-> (NodeAddr -> Derivation -> Derivation) -> Proof -> Proof
pMapLinesWithAddr = (NodeAddr -> NodeAddr)
-> (NodeAddr -> Assumption -> Assumption)
-> (NodeAddr -> Derivation -> Derivation)
-> Proof
-> Proof
go NodeAddr -> NodeAddr
forall a. a -> a
id
 where
  go ::
    (NodeAddr -> NodeAddr) ->
    (NodeAddr -> Assumption -> Assumption) ->
    (NodeAddr -> Derivation -> Derivation) ->
    Proof ->
    Proof
  go :: (NodeAddr -> NodeAddr)
-> (NodeAddr -> Assumption -> Assumption)
-> (NodeAddr -> Derivation -> Derivation)
-> Proof
-> Proof
go NodeAddr -> NodeAddr
getNA NodeAddr -> Assumption -> Assumption
af NodeAddr -> Derivation -> Derivation
df (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) = [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs' [Either Derivation Proof]
ps' Derivation
d'
   where
    (Int
_, [Assumption]
fs') = (Int -> Assumption -> (Int, Assumption))
-> Int -> [Assumption] -> (Int, [Assumption])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL (\Int
m Assumption
frm -> (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, NodeAddr -> Assumption -> Assumption
af (NodeAddr -> NodeAddr
getNA (Int -> NodeAddr
NAAssumption Int
m)) Assumption
frm)) Int
0 [Assumption]
fs
    (Int
_, [Either Derivation Proof]
ps') =
      (Int -> Either Derivation Proof -> (Int, Either Derivation Proof))
-> Int
-> [Either Derivation Proof]
-> (Int, [Either Derivation Proof])
forall (t :: * -> *) s a b.
Traversable t =>
(s -> a -> (s, b)) -> s -> t a -> (s, t b)
mapAccumL
        ( \Int
m Either Derivation Proof
e ->
            ( Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
            , (Derivation -> Either Derivation Proof)
-> (Proof -> Either Derivation Proof)
-> Either Derivation Proof
-> Either Derivation Proof
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
                (Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left (Derivation -> Either Derivation Proof)
-> (Derivation -> Derivation)
-> Derivation
-> Either Derivation Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeAddr -> Derivation -> Derivation
df (NodeAddr -> NodeAddr
getNA (Int -> NodeAddr
NALine Int
m)))
                (Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right (Proof -> Either Derivation Proof)
-> (Proof -> Proof) -> Proof -> Either Derivation Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NodeAddr -> NodeAddr)
-> (NodeAddr -> Assumption -> Assumption)
-> (NodeAddr -> Derivation -> Derivation)
-> Proof
-> Proof
go (NodeAddr -> NodeAddr
getNA (NodeAddr -> NodeAddr)
-> (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr -> NodeAddr
NAProof Int
m) NodeAddr -> Assumption -> Assumption
af NodeAddr -> Derivation -> Derivation
df)
                Either Derivation Proof
e
            )
        )
        Int
0
        [Either Derivation Proof]
ps
    d' :: Derivation
d' = NodeAddr -> Derivation -> Derivation
df (NodeAddr -> NodeAddr
getNA NodeAddr
NAConclusion) Derivation
d

-- | Like 'pMapLines' but lifted to monadic results.
pMapLinesM ::
  (Monad m) =>
  (Assumption -> m Assumption) ->
  (Derivation -> m Derivation) ->
  Proof ->
  m Proof
pMapLinesM :: forall (m :: * -> *).
Monad m =>
(Assumption -> m Assumption)
-> (Derivation -> m Derivation) -> Proof -> m Proof
pMapLinesM Assumption -> m Assumption
af Derivation -> m Derivation
df (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> m [Assumption]
-> m [Either Derivation Proof]
-> m Derivation
-> m 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 -> m Assumption) -> [Assumption] -> m [Assumption]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM Assumption -> m Assumption
af [Assumption]
fs)
    ((Either Derivation Proof -> m (Either Derivation Proof))
-> [Either Derivation Proof] -> m [Either Derivation Proof]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((Derivation -> m (Either Derivation Proof))
-> (Proof -> m (Either Derivation Proof))
-> Either Derivation Proof
-> m (Either Derivation Proof)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either ((Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left (Derivation -> Either Derivation Proof)
-> m Derivation -> m (Either Derivation Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (m Derivation -> m (Either Derivation Proof))
-> (Derivation -> m Derivation)
-> Derivation
-> m (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Derivation -> m Derivation
df) ((Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right (Proof -> Either Derivation Proof)
-> m Proof -> m (Either Derivation Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (m Proof -> m (Either Derivation Proof))
-> (Proof -> m Proof) -> Proof -> m (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Assumption -> m Assumption)
-> (Derivation -> m Derivation) -> Proof -> m Proof
forall (m :: * -> *).
Monad m =>
(Assumption -> m Assumption)
-> (Derivation -> m Derivation) -> Proof -> m Proof
pMapLinesM Assumption -> m Assumption
af Derivation -> m Derivation
df)) [Either Derivation Proof]
ps)
    (Derivation -> m Derivation
df Derivation
d)

-- | Like 'pMapLinesM' but threads an accumulator from left to right.
pMapLinesMAccumL ::
  (Monad m) =>
  (s -> Assumption -> m (s, Assumption)) ->
  (s -> Derivation -> m (s, Derivation)) ->
  s ->
  Proof ->
  m (s, Proof)
pMapLinesMAccumL :: forall (m :: * -> *) s.
Monad m =>
(s -> Assumption -> m (s, Assumption))
-> (s -> Derivation -> m (s, Derivation))
-> s
-> Proof
-> m (s, Proof)
pMapLinesMAccumL s -> Assumption -> m (s, Assumption)
af s -> Derivation -> m (s, Derivation)
df s
s (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
d) = do
  (s', fs') <-
    ((s, [Assumption]) -> Assumption -> m (s, [Assumption]))
-> (s, [Assumption]) -> [Assumption] -> m (s, [Assumption])
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
      (\(s
t, [Assumption]
fs') -> s -> Assumption -> m (s, Assumption)
af s
t (Assumption -> m (s, Assumption))
-> ((s, Assumption) -> m (s, [Assumption]))
-> Assumption
-> m (s, [Assumption])
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (\(s
t', Assumption
f') -> (s, [Assumption]) -> m (s, [Assumption])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s
t', [Assumption]
fs' [Assumption] -> [Assumption] -> [Assumption]
forall a. [a] -> [a] -> [a]
++ [Assumption
Item [Assumption]
f'])))
      (s
s, [])
      [Assumption]
fs
  (s'', ps') <-
    foldlM
      ( \(s
t, [Either Derivation Proof]
ps') ->
          (Derivation -> m (s, [Either Derivation Proof]))
-> (Proof -> m (s, [Either Derivation Proof]))
-> Either Derivation Proof
-> m (s, [Either Derivation Proof])
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
            (s -> Derivation -> m (s, Derivation)
df s
t (Derivation -> m (s, Derivation))
-> ((s, Derivation) -> m (s, [Either Derivation Proof]))
-> Derivation
-> m (s, [Either Derivation Proof])
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (\(s
t', Derivation
d') -> (s, [Either Derivation Proof]) -> m (s, [Either Derivation Proof])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s
t', [Either Derivation Proof]
ps' [Either Derivation Proof]
-> [Either Derivation Proof] -> [Either Derivation Proof]
forall a. Semigroup a => a -> a -> a
<> [Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left Derivation
d'])))
            ((s -> Assumption -> m (s, Assumption))
-> (s -> Derivation -> m (s, Derivation))
-> s
-> Proof
-> m (s, Proof)
forall (m :: * -> *) s.
Monad m =>
(s -> Assumption -> m (s, Assumption))
-> (s -> Derivation -> m (s, Derivation))
-> s
-> Proof
-> m (s, Proof)
pMapLinesMAccumL s -> Assumption -> m (s, Assumption)
af s -> Derivation -> m (s, Derivation)
df s
t (Proof -> m (s, Proof))
-> ((s, Proof) -> m (s, [Either Derivation Proof]))
-> Proof
-> m (s, [Either Derivation Proof])
forall (m :: * -> *) a b c.
Monad m =>
(a -> m b) -> (b -> m c) -> a -> m c
>=> (\(s
t', Proof
p') -> (s, [Either Derivation Proof]) -> m (s, [Either Derivation Proof])
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (s
t', [Either Derivation Proof]
ps' [Either Derivation Proof]
-> [Either Derivation Proof] -> [Either Derivation Proof]
forall a. Semigroup a => a -> a -> a
<> [Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right Proof
p'])))
      )
      (s', [])
      ps
  (s''', d') <- df s'' d
  pure (s''', SubProof fs' ps' d')

{- | Maps every t'Reference' in a t'Proof', optionally removing references
by returning 'Nothing'.
-}
pMapRefs :: (Reference -> Maybe Reference) -> Proof -> Proof
pMapRefs :: (Reference -> Maybe Reference) -> Proof -> Proof
pMapRefs Reference -> Maybe Reference
goRef = (Assumption -> Assumption)
-> (Derivation -> Derivation) -> Proof -> Proof
pMapLines Assumption -> Assumption
goAssumption Derivation -> Derivation
goDerivation
 where
  goAssumption :: Assumption -> Assumption
  goAssumption :: Assumption -> Assumption
goAssumption (Wrapper RawAssumption
a, Wrapper RuleApplication
r) = (Wrapper RawAssumption
a, Wrapper RuleApplication -> Wrapper RuleApplication
goRule Wrapper RuleApplication
r)
  goDerivation :: Derivation -> Derivation
  goDerivation :: Derivation -> Derivation
goDerivation (Derivation Formula
f Wrapper RuleApplication
r) = Formula -> Wrapper RuleApplication -> Derivation
Derivation Formula
f (Wrapper RuleApplication -> Derivation)
-> Wrapper RuleApplication -> Derivation
forall a b. (a -> b) -> a -> b
$ Wrapper RuleApplication -> Wrapper RuleApplication
goRule Wrapper RuleApplication
r
  goRule :: Wrapper RuleApplication -> Wrapper RuleApplication
  goRule :: Wrapper RuleApplication -> Wrapper RuleApplication
goRule (Unparsed Text
txt Text
err) = Text -> Text -> Wrapper RuleApplication
forall a. Text -> Text -> Wrapper a
Unparsed Text
txt Text
err
  goRule w :: Wrapper RuleApplication
w@(ParsedInvalid Text
txt Text
err (RuleApplication Text
name [Reference]
refs)) =
    let
      newRefs :: [Reference]
newRefs = (Reference -> Maybe Reference) -> [Reference] -> [Reference]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Reference -> Maybe Reference
goRef [Reference]
refs
      ra :: RuleApplication
ra = Text -> [Reference] -> RuleApplication
RuleApplication Text
name [Reference]
newRefs
     in
      if [Reference]
newRefs [Reference] -> [Reference] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Reference]
refs
        then Text -> Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid (RuleApplication -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RuleApplication
ra) Text
err RuleApplication
ra
        else Wrapper RuleApplication
w
  goRule w :: Wrapper RuleApplication
w@(ParsedValid Text
txt (RuleApplication Text
name [Reference]
refs)) =
    let
      newRefs :: [Reference]
newRefs = (Reference -> Maybe Reference) -> [Reference] -> [Reference]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe Reference -> Maybe Reference
goRef [Reference]
refs
      ra :: RuleApplication
ra = Text -> [Reference] -> RuleApplication
RuleApplication Text
name [Reference]
newRefs
     in
      if [Reference]
newRefs [Reference] -> [Reference] -> Bool
forall a. Eq a => a -> a -> Bool
/= [Reference]
refs
        then Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> a -> Wrapper a
ParsedValid (RuleApplication -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RuleApplication
ra) RuleApplication
ra
        else Wrapper RuleApplication
w

-- * Indexing proofs

{- | This type is used for indexing lines in a proof.
  Its recursive structure makes defining functions that manipulate proofs more convenient

A t'NodeAddr' may either be a reference to

* a single t'Assumption': v'NAAssumption' @n@,
* the conclusion: 'NAConclusion' of the t'Proof'
* the spot after the conclusion: 'NAAfterConclusion'
* a single t'Derivation' inside the proof @v'NALine' n@
* a reference to a nested element inside the t'Proof' 'NAProof' @n@ ('Just' @a@)
-}
data NodeAddr
  = -- | The @n@-th assumption of the current proof.
    NAAssumption Int
  | -- | The conclusion of the current proof.
    NAConclusion
  | -- | The position directly after the conclusion of the current proof.
    NAAfterConclusion
  | -- | The @n@-th derivation line of the current proof.
    NALine Int
  | -- | A nested address inside the @n@-th subproof of the current proof.
    NAProof Int NodeAddr
  deriving (Int -> NodeAddr -> ShowS
[NodeAddr] -> ShowS
NodeAddr -> String
(Int -> NodeAddr -> ShowS)
-> (NodeAddr -> String) -> ([NodeAddr] -> ShowS) -> Show NodeAddr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> NodeAddr -> ShowS
showsPrec :: Int -> NodeAddr -> ShowS
$cshow :: NodeAddr -> String
show :: NodeAddr -> String
$cshowList :: [NodeAddr] -> ShowS
showList :: [NodeAddr] -> ShowS
Show, NodeAddr -> NodeAddr -> Bool
(NodeAddr -> NodeAddr -> Bool)
-> (NodeAddr -> NodeAddr -> Bool) -> Eq NodeAddr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: NodeAddr -> NodeAddr -> Bool
== :: NodeAddr -> NodeAddr -> Bool
$c/= :: NodeAddr -> NodeAddr -> Bool
/= :: NodeAddr -> NodeAddr -> Bool
Eq)

instance Ord NodeAddr where
  compare :: NodeAddr -> NodeAddr -> Ordering
  compare :: NodeAddr -> NodeAddr -> Ordering
compare (NAAssumption Int
n) (NAAssumption Int
m) = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m
  compare (NAAssumption Int
_) (NALine Int
_) = Ordering
LT
  compare (NALine Int
_) (NAAssumption Int
_) = Ordering
GT
  compare (NALine Int
n) (NALine Int
m) = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m
  compare (NALine Int
n) (NAProof Int
m NodeAddr
_) = case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m of
    Ordering
LT -> Ordering
LT
    Ordering
EQ -> Ordering
LT
    Ordering
GT -> Ordering
GT
  compare (NAProof Int
n NodeAddr
_) (NALine Int
m) = case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m of
    Ordering
LT -> Ordering
LT
    Ordering
EQ -> Ordering
GT
    Ordering
GT -> Ordering
GT
  compare (NAAssumption Int
_) (NAProof Int
_ NodeAddr
_) = Ordering
LT
  compare (NAProof Int
_ NodeAddr
_) (NAAssumption Int
_) = Ordering
GT
  compare (NAProof Int
n NodeAddr
addr1) (NAProof Int
m NodeAddr
addr2) | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m = NodeAddr -> NodeAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare NodeAddr
addr1 NodeAddr
addr2
  compare (NAProof Int
n NodeAddr
_) (NAProof Int
m NodeAddr
_) = Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n Int
m
  compare NodeAddr
NAConclusion NodeAddr
NAConclusion = Ordering
EQ
  compare NodeAddr
NAAfterConclusion NodeAddr
NAAfterConclusion = Ordering
EQ
  compare NodeAddr
NAConclusion NodeAddr
NAAfterConclusion = Ordering
LT
  compare NodeAddr
NAConclusion NodeAddr
a = Ordering
GT
  compare NodeAddr
NAAfterConclusion NodeAddr
a = Ordering
GT
  compare NodeAddr
a NodeAddr
NAConclusion = Ordering
LT
  compare NodeAddr
a NodeAddr
NAAfterConclusion = Ordering
LT

-- | Returns whether a t'NodeAddr' points to an assumption of the current proof level.
isNAAssumption :: NodeAddr -> Bool
isNAAssumption :: NodeAddr -> Bool
isNAAssumption NAAssumption{} = Bool
True
isNAAssumption NodeAddr
_ = Bool
False

-- | Returns whether a t'NodeAddr' points to a possibly nested t'Assumption'.
isNestedNAAssumption :: NodeAddr -> Bool
isNestedNAAssumption :: NodeAddr -> Bool
isNestedNAAssumption (NAProof Int
_ NodeAddr
na) = NodeAddr -> Bool
isNestedNAAssumption NodeAddr
na
isNestedNAAssumption NAAssumption{} = Bool
True
isNestedNAAssumption NodeAddr
_ = Bool
False

-- | Returns whether a t'NodeAddr' points to a possibly nested t'Assumption'.
isNestedNAConclusion :: NodeAddr -> Bool
isNestedNAConclusion :: NodeAddr -> Bool
isNestedNAConclusion (NAProof Int
_ NodeAddr
na) = NodeAddr -> Bool
isNestedNAConclusion NodeAddr
na
isNestedNAConclusion NodeAddr
NAConclusion = Bool
True
isNestedNAConclusion NodeAddr
_ = Bool
False

-- | Returns whether two t'NodeAddr's are on the same level in the same t'Proof'.
naInSameProof :: NodeAddr -> NodeAddr -> Bool
naInSameProof :: NodeAddr -> NodeAddr -> Bool
naInSameProof (NAProof Int
n NodeAddr
na1) (NAProof Int
m NodeAddr
na2) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& NodeAddr -> NodeAddr -> Bool
naInSameProof NodeAddr
na1 NodeAddr
na2
naInSameProof
  (NAAssumption{}; NALine{}; NodeAddr
NAConclusion; NodeAddr
NAAfterConclusion)
  (NAAssumption{}; NALine{}; NodeAddr
NAConclusion; NodeAddr
NAAfterConclusion) = Bool
True
naInSameProof NodeAddr
_ NodeAddr
_ = Bool
False

-- | Returns whether two t'ProofAddr's are on the same level in the same t'Proof'.
paInSameProof :: ProofAddr -> ProofAddr -> Bool
paInSameProof :: ProofAddr -> ProofAddr -> Bool
paInSameProof (PANested Int
n ProofAddr
pa1) (PANested Int
m ProofAddr
pa2) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& ProofAddr -> ProofAddr -> Bool
paInSameProof ProofAddr
pa1 ProofAddr
pa2
paInSameProof PAProof{} PAProof{} = Bool
True
paInSameProof ProofAddr
_ ProofAddr
_ = Bool
False

{- | Returns whether a t'NodeAddr' is the first line
in a t'Proof'. This could be because:

* it is the first assumption;
* there are no assumptions and it is the first line;
* there are no assumptions and it is the first line of the first subproof;
* there are no assumptions, no lines, no subproofs and it is the conclusion.
-}
isFirstLineIn :: Proof -> NodeAddr -> Bool
isFirstLineIn :: Proof -> NodeAddr -> Bool
isFirstLineIn (SubProof (Assumption
_ : [Assumption]
_) [Either Derivation Proof]
_ Derivation
_) (NAAssumption Int
0) = Bool
True
isFirstLineIn (SubProof [] (Left Derivation
_ : [Either Derivation Proof]
_) Derivation
_) (NALine Int
0) = Bool
True
isFirstLineIn (SubProof [] (Right Proof
p : [Either Derivation Proof]
_) Derivation
_) (NAProof Int
0 NodeAddr
na) = Proof -> NodeAddr -> Bool
isFirstLineIn Proof
p NodeAddr
na
isFirstLineIn (SubProof [] [] Derivation
_) NodeAddr
NAConclusion = Bool
True
isFirstLineIn Proof
_ NodeAddr
_ = Bool
False

-- | Address of a t'Proof' within a t'Proof'.
data ProofAddr
  = -- | A nested t'Proof'.
    PANested Int ProofAddr
  | -- | The current t'Proof'.
    PAProof
  deriving (Int -> ProofAddr -> ShowS
[ProofAddr] -> ShowS
ProofAddr -> String
(Int -> ProofAddr -> ShowS)
-> (ProofAddr -> String)
-> ([ProofAddr] -> ShowS)
-> Show ProofAddr
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProofAddr -> ShowS
showsPrec :: Int -> ProofAddr -> ShowS
$cshow :: ProofAddr -> String
show :: ProofAddr -> String
$cshowList :: [ProofAddr] -> ShowS
showList :: [ProofAddr] -> ShowS
Show, ProofAddr -> ProofAddr -> Bool
(ProofAddr -> ProofAddr -> Bool)
-> (ProofAddr -> ProofAddr -> Bool) -> Eq ProofAddr
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ProofAddr -> ProofAddr -> Bool
== :: ProofAddr -> ProofAddr -> Bool
$c/= :: ProofAddr -> ProofAddr -> Bool
/= :: ProofAddr -> ProofAddr -> Bool
Eq)

instance Ord ProofAddr where
  compare :: ProofAddr -> ProofAddr -> Ordering
  compare :: ProofAddr -> ProofAddr -> Ordering
compare ProofAddr
PAProof ProofAddr
PAProof = Ordering
EQ
  compare ProofAddr
PAProof PANested{} = Ordering
LT
  compare PANested{} ProofAddr
PAProof = Ordering
GT
  compare (PANested Int
n1 ProofAddr
pa1) (PANested Int
n2 ProofAddr
pa2) = case Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Int
n1 Int
n2 of
    Ordering
LT -> Ordering
LT
    Ordering
EQ -> ProofAddr -> ProofAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ProofAddr
pa1 ProofAddr
pa2
    Ordering
GT -> Ordering
GT

{- | Moves the given t'ProofAddr' one level higher,
returning a function that can be used to build t'ProofAddr's on the current level.
-}
paProofToNested :: ProofAddr -> (ProofAddr -> ProofAddr)
paProofToNested :: ProofAddr -> ProofAddr -> ProofAddr
paProofToNested ProofAddr
PAProof = ProofAddr -> ProofAddr
forall a. a -> a
id
paProofToNested (PANested Int
n ProofAddr
pa) = Int -> ProofAddr -> ProofAddr
PANested Int
n (ProofAddr -> ProofAddr)
-> (ProofAddr -> ProofAddr) -> ProofAddr -> ProofAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofAddr -> ProofAddr -> ProofAddr
paProofToNested ProofAddr
pa

-- | Returns the t'ProofAddr' that contains the t'NodeAddr'.
paContaining :: NodeAddr -> ProofAddr
paContaining :: NodeAddr -> ProofAddr
paContaining (NAAssumption{}; NALine{}; NodeAddr
NAConclusion; NodeAddr
NAAfterConclusion) = ProofAddr
PAProof
paContaining (NAProof Int
n NodeAddr
na) = Int -> ProofAddr -> ProofAddr
PANested Int
n (NodeAddr -> ProofAddr
paContaining NodeAddr
na)

-- ** Conversion between line numbers and t'NodeAddr'

{- | Takes a line number and returns the corresponding t'NodeAddr' for a given t'Proof'.
Returns v'Nothing' on error.

__Note:__ t'NodeAddr' indices start at @0@, but line numbers start at @1@.
-}
fromLineNo ::
  Int ->
  Proof ->
  Maybe NodeAddr
fromLineNo :: Int -> Proof -> Maybe NodeAddr
fromLineNo Int
n Proof
_ | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
1 = Maybe NodeAddr
forall a. Maybe a
Nothing
fromLineNo Int
n (SubProof [] [Either Derivation Proof]
ps Derivation
_) = Int -> Int -> [Either Derivation Proof] -> Maybe NodeAddr
helper Int
n Int
0 [Either Derivation Proof]
ps
 where
  helper :: Int -> Int -> [Either Derivation Proof] -> Maybe NodeAddr
  helper :: Int -> Int -> [Either Derivation Proof] -> Maybe NodeAddr
helper Int
1 Int
_ [] = NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just NodeAddr
NAConclusion
  helper Int
n Int
_ [] = Maybe NodeAddr
forall a. Maybe a
Nothing
  helper Int
1 Int
m (Left Derivation
d : [Either Derivation Proof]
ps) = NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> Maybe NodeAddr) -> NodeAddr -> Maybe NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NALine Int
m
  helper Int
n Int
m (Left Derivation
d : [Either Derivation Proof]
ps) = Int -> Int -> [Either Derivation Proof] -> Maybe NodeAddr
helper (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Either Derivation Proof]
ps
  helper Int
n Int
m (Right Proof
p : [Either Derivation Proof]
ps) | Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Proof -> Int
pLength Proof
p = do
    addr <- Int -> Proof -> Maybe NodeAddr
fromLineNo Int
n Proof
p
    pure $ NAProof m addr
  helper Int
n Int
m (Right Proof
p : [Either Derivation Proof]
ps) = Int -> Int -> [Either Derivation Proof] -> Maybe NodeAddr
helper (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Proof -> Int
pLength Proof
p) (Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [Either Derivation Proof]
ps
fromLineNo Int
n (SubProof [Assumption]
fs [Either Derivation Proof]
_ Derivation
_) | Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1 Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Assumption] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Assumption]
fs = NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> Maybe NodeAddr) -> NodeAddr -> Maybe NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NAAssumption (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
fromLineNo Int
n (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
l) = Int -> Proof -> Maybe NodeAddr
fromLineNo (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- [Assumption] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Assumption]
fs) ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [] [Either Derivation Proof]
ps Derivation
l)

{- | Takes a t'NodeAddr' and returns the corresponding line number for a given t'Proof'.

__Note:__ t'NodeAddr' indices start at @0@, but line numbers start at @1@.
-}
fromNodeAddr :: NodeAddr -> Proof -> Maybe Int
fromNodeAddr :: NodeAddr -> Proof -> Maybe Int
fromNodeAddr = Int -> NodeAddr -> Proof -> Maybe Int
go Int
1
 where
  go :: Int -> NodeAddr -> Proof -> Maybe Int
  go :: Int -> NodeAddr -> Proof -> Maybe Int
go Int
n (NAAssumption Int
m) (SubProof [Assumption]
fs [Either Derivation Proof]
_ Derivation
_) | Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< [Assumption] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Assumption]
fs = Int -> Maybe Int
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
m
  go Int
n (NAAssumption Int
m) (SubProof [Assumption]
fs [Either Derivation Proof]
_ Derivation
_) = Maybe Int
forall a. Maybe a
Nothing
  go Int
1 (NALine Int
0) (SubProof [] [] Derivation
_) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
1
  go Int
n (NALine Int
m) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
_)
    | (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 Int
m =
        Int -> Maybe Int
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$
          [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
n
            Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Either Derivation Proof -> Int -> Int)
-> Int -> [Either Derivation Proof] -> Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
              (\Either Derivation Proof
p Int
n -> (Derivation -> Int)
-> (Proof -> Int) -> Either Derivation Proof -> Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Int -> Derivation -> Int
forall a b. a -> b -> a
const (Int -> Derivation -> Int) -> Int -> Derivation -> Int
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+) (Int -> Int) -> (Proof -> Int) -> Proof -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof -> Int
pLength) Either Derivation Proof
p)
              Int
0
              (Int -> [Either Derivation Proof] -> [Either Derivation Proof]
forall a. Int -> [a] -> [a]
take Int
m [Either Derivation Proof]
ps)
  go Int
n NodeAddr
NAConclusion (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
_) =
    Int -> Maybe Int
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> Maybe Int) -> Int -> Maybe Int
forall a b. (a -> b) -> a -> b
$
      [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
n
        Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Either Derivation Proof -> Int -> Int)
-> Int -> [Either Derivation Proof] -> Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
          (\Either Derivation Proof
p Int
n -> (Derivation -> Int)
-> (Proof -> Int) -> Either Derivation Proof -> Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Int -> Derivation -> Int
forall a b. a -> b -> a
const (Int -> Derivation -> Int) -> Int -> Derivation -> Int
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+) (Int -> Int) -> (Proof -> Int) -> Proof -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof -> Int
pLength) Either Derivation Proof
p)
          Int
0
          [Either Derivation Proof]
ps
  go Int
n (NAProof Int
m NodeAddr
na) (SubProof [Assumption]
fs ps :: [Either Derivation Proof]
ps@(([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
m) -> Just (Right Proof
p)) Derivation
_) =
    Int -> NodeAddr -> Proof -> Maybe Int
go
      ( [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
n
          Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Either Derivation Proof -> Int -> Int)
-> Int -> [Either Derivation Proof] -> Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
            (\Either Derivation Proof
p Int
n -> (Derivation -> Int)
-> (Proof -> Int) -> Either Derivation Proof -> Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Int -> Derivation -> Int
forall a b. a -> b -> a
const (Int -> Derivation -> Int) -> Int -> Derivation -> Int
forall a b. (a -> b) -> a -> b
$ Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+) (Int -> Int) -> (Proof -> Int) -> Proof -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof -> Int
pLength) Either Derivation Proof
p)
            Int
0
            (Int -> [Either Derivation Proof] -> [Either Derivation Proof]
forall a. Int -> [a] -> [a]
take Int
m [Either Derivation Proof]
ps)
      )
      NodeAddr
na
      Proof
p
  go Int
_ NodeAddr
_ Proof
_ = Maybe Int
forall a. Maybe a
Nothing

{- | Like 'fromNodeAddr',
but falls back to line number @999@ if the t'NodeAddr' is invalid.
-}
lineNoOr999 :: NodeAddr -> Proof -> Int
lineNoOr999 :: NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
na Proof
p = Int -> Maybe Int -> Int
forall a. a -> Maybe a -> a
fromMaybe Int
999 (NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
na Proof
p)

{- | Returns the t'ProofAddr' of the t'Proof' spanning from the given start line
to the given end line, or v'Nothing' if no such t'Proof' exists.
-}
fromLineRange ::
  Int ->
  Int ->
  Proof ->
  Maybe ProofAddr
fromLineRange :: Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
start Int
end Proof
p = do
  -- get corresponding 'NodeAddr's
  lastLine <- Int -> Proof -> Maybe NodeAddr
fromLineNo Int
end Proof
p

  -- Get 'ProofAddr' of the conclusion
  pa <-
    if isNestedNAConclusion lastLine
      then Just $ paContaining lastLine
      else Nothing

  -- compare starting line of pa with firstLine
  (start', _) <- lineRangeFromProofAddr pa p
  if start' == start
    then Just pa
    else Nothing

{- | Returns the start and end line numbers of the t'Proof' addressed by a t'ProofAddr'.
Returns v'Nothing' if the t'ProofAddr' is invalid.
-}
lineRangeFromProofAddr :: ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr :: ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr ProofAddr
PAProof Proof
p = (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
1, Proof -> Int
pLength Proof
p)
lineRangeFromProofAddr (PANested Int
0 ProofAddr
pa) (SubProof [Assumption]
fs (Right Proof
p : [Either Derivation Proof]
ps) Derivation
_) =
  case ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr ProofAddr
pa Proof
p of
    Just (Int
start, Int
end) -> (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Assumption] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Assumption]
fs, Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Assumption] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Assumption]
fs)
    Maybe (Int, Int)
Nothing -> Maybe (Int, Int)
forall a. Maybe a
Nothing
lineRangeFromProofAddr (PANested Int
n ProofAddr
pa) (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 =
  case ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr (Int -> ProofAddr -> ProofAddr
PANested (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ProofAddr
pa) ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) of
    Just (Int
start, Int
end) ->
      (Int, Int) -> Maybe (Int, Int)
forall a. a -> Maybe a
Just
        ( Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Derivation -> Int)
-> (Proof -> Int) -> Either Derivation Proof -> Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Int -> Derivation -> Int
forall a b. a -> b -> a
const Int
1) Proof -> Int
pLength Either Derivation Proof
e
        , Int
end
            Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Derivation -> Int)
-> (Proof -> Int) -> Either Derivation Proof -> Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              (Int -> Derivation -> Int
forall a b. a -> b -> a
const Int
1)
              Proof -> Int
pLength
              Either Derivation Proof
e
        )
    Maybe (Int, Int)
Nothing -> Maybe (Int, Int)
forall a. Maybe a
Nothing
lineRangeFromProofAddr ProofAddr
_ Proof
_ = Maybe (Int, Int)
forall a. Maybe a
Nothing

-- ** Utilities for working with addresses

{- | Increments a t'NodeAddr' index by 1, keeping the nesting structure unchanged.
Returns v'Nothing' for addresses without a numeric index (e.g. v'NAConclusion').
-}
incrementNodeAddr :: NodeAddr -> Maybe NodeAddr
incrementNodeAddr :: NodeAddr -> Maybe NodeAddr
incrementNodeAddr (NAAssumption Int
n) = NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> Maybe NodeAddr) -> NodeAddr -> Maybe NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NAAssumption (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
incrementNodeAddr (NALine Int
n) = NodeAddr -> Maybe NodeAddr
forall a. a -> Maybe a
Just (NodeAddr -> Maybe NodeAddr) -> NodeAddr -> Maybe NodeAddr
forall a b. (a -> b) -> a -> b
$ Int -> NodeAddr
NALine (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
incrementNodeAddr (NAProof Int
n NodeAddr
na) = Int -> NodeAddr -> NodeAddr
NAProof Int
n (NodeAddr -> NodeAddr) -> Maybe NodeAddr -> Maybe NodeAddr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Maybe NodeAddr
incrementNodeAddr NodeAddr
na
incrementNodeAddr NodeAddr
_ = Maybe NodeAddr
forall a. Maybe a
Nothing

{- | Converts a t'NodeAddr' to a t'ProofAddr', by

* Converting @v'NALine' n@ to @v'PAProof' n@
* Converting @v'NAConclusion n' to @v'PAProof' (length ps)@
* Converting @v'NAProof' n@ to @v'PANested' n@ and recursing.

For other t'NodeAddr's, returns v'Nothing'.
-}
paFromNA :: NodeAddr -> Proof -> Maybe ProofAddr
paFromNA :: NodeAddr -> Proof -> Maybe ProofAddr
paFromNA (NALine Int
n) Proof
_ = ProofAddr -> Maybe ProofAddr
forall a. a -> Maybe a
Just (ProofAddr -> Maybe ProofAddr) -> ProofAddr -> Maybe ProofAddr
forall a b. (a -> b) -> a -> b
$ Int -> ProofAddr -> ProofAddr
PANested Int
n ProofAddr
PAProof
paFromNA NodeAddr
NAConclusion (SubProof [Assumption]
_ [Either Derivation Proof]
ps Derivation
_) = ProofAddr -> Maybe ProofAddr
forall a. a -> Maybe a
Just (ProofAddr -> Maybe ProofAddr) -> ProofAddr -> Maybe ProofAddr
forall a b. (a -> b) -> a -> b
$ Int -> ProofAddr -> ProofAddr
PANested ([Either Derivation Proof] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Derivation Proof]
ps) ProofAddr
PAProof
paFromNA (NAProof Int
n NodeAddr
na) (SubProof [Assumption]
_ (([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n) -> Just (Right Proof
p)) Derivation
_) =
  Int -> ProofAddr -> ProofAddr
PANested Int
n
    (ProofAddr -> ProofAddr) -> Maybe ProofAddr -> Maybe ProofAddr
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Proof -> Maybe ProofAddr
paFromNA NodeAddr
na Proof
p
paFromNA NodeAddr
_ Proof
_ = Maybe ProofAddr
forall a. Maybe a
Nothing

{- | Turns a t'ProofAddr' into a function for building a t'NodeAddr'
that is contained in the t'ProofAddr'.
-}
naFromPA :: ProofAddr -> (NodeAddr -> NodeAddr)
naFromPA :: ProofAddr -> NodeAddr -> NodeAddr
naFromPA ProofAddr
PAProof = NodeAddr -> NodeAddr
forall a. a -> a
id
naFromPA (PANested Int
n ProofAddr
pa) = Int -> NodeAddr -> NodeAddr
NAProof Int
n (NodeAddr -> NodeAddr)
-> (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofAddr -> NodeAddr -> NodeAddr
naFromPA ProofAddr
pa

-- | Returns a function that lifts a nested t'NodeAddr' by one proof level, if possible.
naLevelup2 :: NodeAddr -> Maybe (NodeAddr -> NodeAddr)
naLevelup2 :: NodeAddr -> Maybe (NodeAddr -> NodeAddr)
naLevelup2 = (NodeAddr -> NodeAddr) -> NodeAddr -> Maybe (NodeAddr -> NodeAddr)
go NodeAddr -> NodeAddr
forall a. a -> a
id
 where
  go :: (NodeAddr -> NodeAddr) -> NodeAddr -> Maybe (NodeAddr -> NodeAddr)
  go :: (NodeAddr -> NodeAddr) -> NodeAddr -> Maybe (NodeAddr -> NodeAddr)
go NodeAddr -> NodeAddr
na (NAProof Int
_ NodeAddr
NAConclusion) = (NodeAddr -> NodeAddr) -> Maybe (NodeAddr -> NodeAddr)
forall a. a -> Maybe a
Just NodeAddr -> NodeAddr
na
  go NodeAddr -> NodeAddr
na (NAProof Int
_ NodeAddr
NAAfterConclusion) = (NodeAddr -> NodeAddr) -> Maybe (NodeAddr -> NodeAddr)
forall a. a -> Maybe a
Just NodeAddr -> NodeAddr
na
  go NodeAddr -> NodeAddr
na (NAProof Int
_ (NAAssumption Int
_)) = (NodeAddr -> NodeAddr) -> Maybe (NodeAddr -> NodeAddr)
forall a. a -> Maybe a
Just NodeAddr -> NodeAddr
na
  go NodeAddr -> NodeAddr
na (NAProof Int
_ (NALine Int
_)) = (NodeAddr -> NodeAddr) -> Maybe (NodeAddr -> NodeAddr)
forall a. a -> Maybe a
Just NodeAddr -> NodeAddr
na
  go NodeAddr -> NodeAddr
na (NAProof Int
m NodeAddr
na') = (NodeAddr -> NodeAddr) -> NodeAddr -> Maybe (NodeAddr -> NodeAddr)
go (NodeAddr -> NodeAddr
na (NodeAddr -> NodeAddr)
-> (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> NodeAddr -> NodeAddr
NAProof Int
m) NodeAddr
na'
  go NodeAddr -> NodeAddr
_ NodeAddr
_ = Maybe (NodeAddr -> NodeAddr)
forall a. Maybe a
Nothing

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

-- * Querying proofs

-- | Counts the number of parse or validation errors occurring in a t'Proof'.
proofErrors :: Proof -> Int
proofErrors :: Proof -> Int
proofErrors (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (Either Derivation Proof -> Int -> Int)
-> Int -> [Either Derivation Proof] -> Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
    (\Either Derivation Proof
e Int
n -> (Derivation -> Int)
-> (Proof -> Int) -> Either Derivation Proof -> Int
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either Derivation -> Int
derivationErrors Proof -> Int
proofErrors Either Derivation Proof
e Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n)
    ((Assumption -> Int -> Int) -> Int -> [Assumption] -> Int
forall a b. (a -> b -> b) -> b -> [a] -> b
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\Assumption
a Int
n -> Assumption -> Int
assumptionErrors Assumption
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
n) Int
0 [Assumption]
fs)
    [Either Derivation Proof]
ps
    Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Derivation -> Int
derivationErrors Derivation
c
 where
  derivationErrors :: Derivation -> Int
  derivationErrors :: Derivation -> Int
derivationErrors (Derivation Formula
f Wrapper RuleApplication
r)
    | Formula -> Bool
forall a. Wrapper a -> Bool
isParseValid Formula
f Bool -> Bool -> Bool
&& Wrapper RuleApplication -> Bool
forall a. Wrapper a -> Bool
isParseValid Wrapper RuleApplication
r = Int
0
    | Bool -> Bool
not (Formula -> Bool
forall a. Wrapper a -> Bool
isParseValid Formula
f) Bool -> Bool -> Bool
&& Bool -> Bool
not (Wrapper RuleApplication -> Bool
forall a. Wrapper a -> Bool
isParseValid Wrapper RuleApplication
r) = Int
2
    | Bool
otherwise = Int
1
  assumptionErrors :: Assumption -> Int
  assumptionErrors :: Assumption -> Int
assumptionErrors (Wrapper RawAssumption
f, Wrapper RuleApplication
_)
    | Wrapper RawAssumption -> Bool
forall a. Wrapper a -> Bool
isParseValid Wrapper RawAssumption
f = Int
0
    | Bool
otherwise = Int
1

-- | Returns whether the element at the given index exists and satisfies a predicate.
holdsAt :: (a -> Bool) -> [a] -> Int -> Bool
holdsAt :: forall a. (a -> Bool) -> [a] -> Int -> Bool
holdsAt a -> Bool
f [a]
xs Int
n = Bool -> (a -> Bool) -> Maybe a -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False a -> Bool
f ([a]
xs [a] -> Int -> Maybe a
forall a. [a] -> Int -> Maybe a
!!? Int
n)

{- | Returns whether the element at the given t'NodeAddr' exists
 and satisfies a predicate.
-}
holdsAtNA :: (Either Assumption Derivation -> Bool) -> Proof -> NodeAddr -> Bool
holdsAtNA :: (Either Assumption Derivation -> Bool) -> Proof -> NodeAddr -> Bool
holdsAtNA Either Assumption Derivation -> Bool
f Proof
p NodeAddr
na = Bool
-> (Either Assumption Derivation -> Bool)
-> Maybe (Either Assumption Derivation)
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False Either Assumption Derivation -> Bool
f (NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
na Proof
p)

{- | Returns whether the t'NodeAddr' is a valid address for the given t'Proof'.
(Valid in the sense that 'naLookup' would return a valid result.)
-}
naValid :: NodeAddr -> Proof -> Bool
naValid :: NodeAddr -> Proof -> Bool
naValid NodeAddr
na Proof
p = Maybe (Either Assumption Derivation) -> Bool
forall a. Maybe a -> Bool
isJust (Maybe (Either Assumption Derivation) -> Bool)
-> Maybe (Either Assumption Derivation) -> Bool
forall a b. (a -> b) -> a -> b
$ NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
na Proof
p

{- | Returns the line at a given t'NodeAddr'.
Returns v'Nothing' if the t'NodeAddr' does not correspond to any line in the t'Proof'.
-}
naLookup :: NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup :: NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup (NAAssumption Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
_ Derivation
_) = Assumption -> Either Assumption Derivation
forall a b. a -> Either a b
Left (Assumption -> Either Assumption Derivation)
-> Maybe Assumption -> Maybe (Either Assumption Derivation)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Assumption]
fs [Assumption] -> Int -> Maybe Assumption
forall a. [a] -> Int -> Maybe a
!!? Int
n
naLookup (NALine Int
n) (SubProof [Assumption]
_ (([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n) -> Just (Left Derivation
d)) Derivation
_) = 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 (Either Assumption Derivation))
-> Derivation -> Maybe (Either Assumption Derivation)
forall a b. (a -> b) -> a -> b
$ Derivation
d
naLookup NodeAddr
NAConclusion (SubProof [Assumption]
_ [Either Derivation Proof]
_ Derivation
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 (Either Assumption Derivation))
-> Derivation -> Maybe (Either Assumption Derivation)
forall a b. (a -> b) -> a -> b
$ Derivation
c
naLookup (NAProof Int
n NodeAddr
na) (SubProof [Assumption]
_ (([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n) -> Just (Right Proof
p)) Derivation
_) = NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
na Proof
p
naLookup NodeAddr
_ Proof
_ = Maybe (Either Assumption Derivation)
forall a. Maybe a
Nothing

-- | Returns the t'Proof' at a given t'ProofAddr' if it exists.
paLookup :: ProofAddr -> Proof -> Maybe Proof
paLookup :: ProofAddr -> Proof -> Maybe Proof
paLookup (PANested Int
n ProofAddr
pa) (SubProof [Assumption]
_ (([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n) -> Just (Right Proof
p)) Derivation
_) = ProofAddr -> Proof -> Maybe Proof
paLookup ProofAddr
pa Proof
p
paLookup ProofAddr
PAProof Proof
p = Proof -> Maybe Proof
forall a. a -> Maybe a
Just Proof
p
paLookup ProofAddr
_ Proof
_ = Maybe Proof
forall a. Maybe a
Nothing

-- | Returns the t'Assumption' or t'Derivation' at the given line number if it exists.
pIndex :: Int -> Proof -> Maybe (Either Assumption Derivation)
pIndex :: Int -> Proof -> Maybe (Either Assumption Derivation)
pIndex Int
n Proof
p = case Int -> Proof -> Maybe NodeAddr
fromLineNo Int
n Proof
p of
  Maybe NodeAddr
Nothing -> Maybe (Either Assumption Derivation)
forall a. Maybe a
Nothing
  Just NodeAddr
addr -> case NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
addr Proof
p of
    Maybe (Either Assumption Derivation)
Nothing -> Maybe (Either Assumption Derivation)
forall a. Maybe a
Nothing
    Just (Left Assumption
a) -> Either Assumption Derivation
-> Maybe (Either Assumption Derivation)
forall a. a -> Maybe a
Just (Assumption -> Either Assumption Derivation
forall a b. a -> Either a b
Left Assumption
a)
    Just (Right Derivation
d) -> 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 (Either Assumption Derivation))
-> Derivation -> Maybe (Either Assumption Derivation)
forall a b. (a -> b) -> a -> b
$ Derivation
d

-- | Returns the t'Proof' spanning the given start and end line numbers if it exists.
pIndexProof :: Int -> Int -> Proof -> Maybe Proof
pIndexProof :: Int -> Int -> Proof -> Maybe Proof
pIndexProof Int
start Int
end Proof
p = Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
start Int
end Proof
p Maybe ProofAddr -> (ProofAddr -> 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
>>= (ProofAddr -> Proof -> Maybe Proof
`paLookup` Proof
p)

{- | Returns whether the second t'NodeAddr' is relevant
when checking freshness for the first t'NodeAddr'.

I.e., whether the second t'NodeAddr' appears before the first one,
or appears on the same level.
-}
naAffectsFreshness :: NodeAddr -> NodeAddr -> Bool
naAffectsFreshness :: NodeAddr -> NodeAddr -> Bool
naAffectsFreshness (NAProof Int
n NodeAddr
na1) (NAProof Int
m NodeAddr
na2)
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
m = Bool
True
  | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m = NodeAddr -> NodeAddr -> Bool
naAffectsFreshness NodeAddr
na1 NodeAddr
na2
  | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
m = Bool
False
naAffectsFreshness
  (NAProof Int
_ (NAAssumption{}; NALine{}; NodeAddr
NAConclusion))
  (NAAssumption{}; NALine{}; NodeAddr
NAConclusion) = Bool
True
naAffectsFreshness (NAProof{}) (NAAssumption{}) = Bool
False
naAffectsFreshness (NAProof Int
n NodeAddr
_) (NALine Int
m) = Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n
naAffectsFreshness (NAProof{}) NodeAddr
_ = Bool
False
naAffectsFreshness (NAAssumption Int
n) (NAAssumption Int
m) = Int
m Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n
naAffectsFreshness (NAAssumption Int
_) (NALine{}; NodeAddr
NAConclusion) = Bool
False
naAffectsFreshness NodeAddr
_ NodeAddr
_ = Bool
False

-- | Collects all lines relevant for freshness checking of the given t'NodeAddr'.
pCollectFreshnessNodes ::
  Proof -> NodeAddr -> [(NodeAddr, Either Assumption Derivation)]
pCollectFreshnessNodes :: Proof -> NodeAddr -> [(NodeAddr, Either Assumption Derivation)]
pCollectFreshnessNodes Proof
p NodeAddr
na =
  [Maybe (NodeAddr, Either Assumption Derivation)]
-> [(NodeAddr, Either Assumption Derivation)]
forall a. [Maybe a] -> [a]
catMaybes ([Maybe (NodeAddr, Either Assumption Derivation)]
 -> [(NodeAddr, Either Assumption Derivation)])
-> [Maybe (NodeAddr, Either Assumption Derivation)]
-> [(NodeAddr, Either Assumption Derivation)]
forall a b. (a -> b) -> a -> b
$
    (NodeAddr
 -> Assumption -> Maybe (NodeAddr, Either Assumption Derivation))
-> (NodeAddr
    -> Derivation -> Maybe (NodeAddr, Either Assumption Derivation))
-> Proof
-> [Maybe (NodeAddr, Either Assumption Derivation)]
forall a.
(NodeAddr -> Assumption -> a)
-> (NodeAddr -> Derivation -> a) -> Proof -> [a]
pSerializeLinesWithAddr
      (\NodeAddr
na' Assumption
a -> if NodeAddr -> NodeAddr -> Bool
naAffectsFreshness NodeAddr
na NodeAddr
na' then (NodeAddr, Either Assumption Derivation)
-> Maybe (NodeAddr, Either Assumption Derivation)
forall a. a -> Maybe a
Just (NodeAddr
na', Assumption -> Either Assumption Derivation
forall a b. a -> Either a b
Left Assumption
a) else Maybe (NodeAddr, Either Assumption Derivation)
forall a. Maybe a
Nothing)
      (\NodeAddr
na' Derivation
d -> if NodeAddr -> NodeAddr -> Bool
naAffectsFreshness NodeAddr
na NodeAddr
na' then (NodeAddr, Either Assumption Derivation)
-> Maybe (NodeAddr, Either Assumption Derivation)
forall a. a -> Maybe a
Just (NodeAddr
na', Derivation -> Either Assumption Derivation
forall a b. b -> Either a b
Right Derivation
d) else Maybe (NodeAddr, Either Assumption Derivation)
forall a. Maybe a
Nothing)
      Proof
p

-- * Updating proof contents

{- | 'naUpdateFormula' @f@ @addr@ @proof@ replaces the t'Assumption' or
t'Formula' at @addr@ in @proof@ using @f@.
Pass 'Left' to update an t'Assumption', or 'Right'
to update the t'Formula' of a t'Derivation'.
Returns v'Nothing' if the address does not exist or is incompatible
with the chosen update function.
-}
naUpdateFormula ::
  Either (Assumption -> Assumption) (Formula -> Formula) ->
  NodeAddr ->
  Proof ->
  Maybe Proof
naUpdateFormula :: Either (Assumption -> Assumption) (Formula -> Formula)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateFormula (Left Assumption -> Assumption
f) (NAAssumption Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
l) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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
    (Int
-> (Assumption -> Maybe Assumption)
-> [Assumption]
-> Maybe [Assumption]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM Int
n (Assumption -> Maybe Assumption
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Assumption -> Maybe Assumption)
-> (Assumption -> Assumption) -> Assumption -> Maybe Assumption
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Assumption -> Assumption
f) [Assumption]
fs)
    ([Either Derivation Proof] -> Maybe [Either Derivation Proof]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Either Derivation Proof]
ps)
    (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
l)
naUpdateFormula (Right Formula -> Formula
f) (NALine Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
l) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
    ( Int
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM
        Int
n
        ( Either Derivation Proof -> Maybe (Either Derivation Proof)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> (Either Derivation Proof -> Either Derivation Proof)
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Derivation -> Either Derivation Proof)
-> (Proof -> Either Derivation Proof)
-> Either Derivation Proof
-> Either Derivation Proof
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              ( Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left (Derivation -> Either Derivation Proof)
-> (Derivation -> Derivation)
-> Derivation
-> Either Derivation Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \(Derivation Formula
formula Wrapper RuleApplication
rule) ->
                  Formula -> Wrapper RuleApplication -> Derivation
Derivation (Formula -> Formula
f Formula
formula) Wrapper RuleApplication
rule
              )
              Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right
        )
        [Either Derivation Proof]
ps
    )
    (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
l)
naUpdateFormula (Right Formula -> Formula
f) NodeAddr
NAConclusion (SubProof [Assumption]
fs [Either Derivation Proof]
ps (Derivation Formula
formula Wrapper RuleApplication
rule)) =
  Proof -> Maybe Proof
forall a. a -> Maybe a
Just (Proof -> Maybe Proof) -> Proof -> Maybe Proof
forall a b. (a -> b) -> a -> b
$ [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs [Either Derivation Proof]
ps (Formula -> Wrapper RuleApplication -> Derivation
Derivation (Formula -> Formula
f Formula
formula) Wrapper RuleApplication
rule)
naUpdateFormula Either (Assumption -> Assumption) (Formula -> Formula)
f (NAProof Int
n NodeAddr
na) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
l) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
    (Int
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM Int
n ((Derivation -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Either Derivation Proof)
-> Derivation -> Maybe (Either Derivation Proof)
forall a b. a -> b -> a
const Maybe (Either Derivation Proof)
forall a. Maybe a
Nothing) ((Proof -> Either Derivation Proof)
-> Maybe Proof -> Maybe (Either Derivation Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right (Maybe Proof -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe Proof)
-> Proof
-> Maybe (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either (Assumption -> Assumption) (Formula -> Formula)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateFormula Either (Assumption -> Assumption) (Formula -> Formula)
f NodeAddr
na)) [Either Derivation Proof]
ps)
    (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
l)
naUpdateFormula Either (Assumption -> Assumption) (Formula -> Formula)
_ NodeAddr
_ Proof
_ = Maybe Proof
forall a. Maybe a
Nothing

{- | 'naUpdateRule' @f@ @addr@ @proof@ updates the t'RuleApplication'
at @addr@ in @proof@ using @f@.
Returns v'Nothing' if the address does not exist
or points to an t'Assumption' (which has no editable t'RuleApplication').
-}
naUpdateRule ::
  (Wrapper RuleApplication -> Wrapper RuleApplication) ->
  NodeAddr ->
  Proof ->
  Maybe Proof
naUpdateRule :: (Wrapper RuleApplication -> Wrapper RuleApplication)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateRule Wrapper RuleApplication -> Wrapper RuleApplication
f (NALine Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
l) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
    ( Int
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM
        Int
n
        ( Either Derivation Proof -> Maybe (Either Derivation Proof)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure
            (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> (Either Derivation Proof -> Either Derivation Proof)
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Derivation -> Either Derivation Proof)
-> (Proof -> Either Derivation Proof)
-> Either Derivation Proof
-> Either Derivation Proof
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
              ( Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left (Derivation -> Either Derivation Proof)
-> (Derivation -> Derivation)
-> Derivation
-> Either Derivation Proof
forall b c a. (b -> c) -> (a -> b) -> a -> c
. \(Derivation Formula
formula Wrapper RuleApplication
rule) ->
                  Formula -> Wrapper RuleApplication -> Derivation
Derivation Formula
formula (Wrapper RuleApplication -> Wrapper RuleApplication
f Wrapper RuleApplication
rule)
              )
              Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right
        )
        [Either Derivation Proof]
ps
    )
    (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
l)
naUpdateRule Wrapper RuleApplication -> Wrapper RuleApplication
f NodeAddr
NAConclusion (SubProof [Assumption]
fs [Either Derivation Proof]
ps (Derivation Formula
formula Wrapper RuleApplication
rule)) =
  Proof -> Maybe Proof
forall a. a -> Maybe a
Just (Proof -> Maybe Proof) -> Proof -> Maybe Proof
forall a b. (a -> b) -> a -> b
$ [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs [Either Derivation Proof]
ps (Formula -> Wrapper RuleApplication -> Derivation
Derivation Formula
formula (Wrapper RuleApplication -> Wrapper RuleApplication
f Wrapper RuleApplication
rule))
naUpdateRule Wrapper RuleApplication -> Wrapper RuleApplication
f (NAProof Int
n NodeAddr
na) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
l) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
    (Int
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM Int
n ((Derivation -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Either Derivation Proof)
-> Derivation -> Maybe (Either Derivation Proof)
forall a b. a -> b -> a
const Maybe (Either Derivation Proof)
forall a. Maybe a
Nothing) ((Proof -> Either Derivation Proof)
-> Maybe Proof -> Maybe (Either Derivation Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right (Maybe Proof -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe Proof)
-> Proof
-> Maybe (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Wrapper RuleApplication -> Wrapper RuleApplication)
-> NodeAddr -> Proof -> Maybe Proof
naUpdateRule Wrapper RuleApplication -> Wrapper RuleApplication
f NodeAddr
na)) [Either Derivation Proof]
ps)
    (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
l)
naUpdateRule Wrapper RuleApplication -> Wrapper RuleApplication
_ NodeAddr
_ Proof
p = Maybe Proof
forall a. Maybe a
Nothing

-- * (Re-)moving inside a proof

{- | @'naRemoveRaw' addr proof@ removes the element at a valid @addr@ from @proof@
without updating any t'Reference's.

For the v'NAConclusion' case: if the last element of @ps@ is a t'Derivation',
it is promoted to become the new conclusion. Otherwise v'Nothing' is returned.

__Note:__ Use 'naRemove' if references must stay consistent.
-}
naRemoveRaw :: NodeAddr -> Proof -> Maybe Proof
naRemoveRaw :: NodeAddr -> Proof -> Maybe Proof
naRemoveRaw (NAAssumption Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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
    (Int -> [Assumption] -> Maybe [Assumption]
forall a. Int -> [a] -> Maybe [a]
removeAt Int
n [Assumption]
fs)
    ([Either Derivation Proof] -> Maybe [Either Derivation Proof]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Either Derivation Proof]
ps)
    (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c)
naRemoveRaw (NALine Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c)
  | (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 Int
n =
      ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
        (Int -> [Either Derivation Proof] -> Maybe [Either Derivation Proof]
forall a. Int -> [a] -> Maybe [a]
removeAt Int
n [Either Derivation Proof]
ps)
        (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c)
naRemoveRaw NodeAddr
NAConclusion p :: Proof
p@(SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) = case [Either Derivation Proof]
-> Maybe ([Either Derivation Proof], Either Derivation Proof)
forall a. [a] -> Maybe ([a], a)
unsnoc [Either Derivation Proof]
ps of
  Just ([Either Derivation Proof]
ps', Left Derivation
d) -> Proof -> Maybe Proof
forall a. a -> Maybe a
Just (Proof -> Maybe Proof) -> Proof -> Maybe Proof
forall a b. (a -> b) -> a -> b
$ [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs [Either Derivation Proof]
ps' Derivation
d
  Maybe ([Either Derivation Proof], Either Derivation Proof)
_ -> Maybe Proof
forall a. Maybe a
Nothing
naRemoveRaw (NAProof Int
n NodeAddr
na) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
    ( Int
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM
        Int
n
        ( (Derivation -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
            (Maybe (Either Derivation Proof)
-> Derivation -> Maybe (Either Derivation Proof)
forall a b. a -> b -> a
const Maybe (Either Derivation Proof)
forall a. Maybe a
Nothing)
            ((Proof -> Either Derivation Proof)
-> Maybe Proof -> Maybe (Either Derivation Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right (Maybe Proof -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe Proof)
-> Proof
-> Maybe (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NodeAddr -> Proof -> Maybe Proof
naRemoveRaw NodeAddr
na)
        )
        [Either Derivation Proof]
ps
    )
    (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c)
naRemoveRaw NodeAddr
_ Proof
_ = Maybe Proof
forall a. Maybe a
Nothing

{- | Removes the t'Proof' at a valid t'ProofAddr' without updating references.

__Note:__ Use 'paRemove' if references must stay consistent.
-}
paRemoveRaw :: ProofAddr -> Proof -> Maybe Proof
paRemoveRaw :: ProofAddr -> Proof -> Maybe Proof
paRemoveRaw ProofAddr
PAProof Proof
_ = Maybe Proof
forall a. Maybe a
Nothing
paRemoveRaw (PANested Int
n ProofAddr
PAProof) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c)
  | (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 Int
n =
      ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
        (Int -> [Either Derivation Proof] -> Maybe [Either Derivation Proof]
forall a. Int -> [a] -> Maybe [a]
removeAt Int
n [Either Derivation Proof]
ps)
        (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c)
  | Bool
otherwise = Maybe Proof
forall a. Maybe a
Nothing
paRemoveRaw (PANested Int
n ProofAddr
pa) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
    (Int
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM Int
n ((Derivation -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Either Derivation Proof)
-> Derivation -> Maybe (Either Derivation Proof)
forall a b. a -> b -> a
const Maybe (Either Derivation Proof)
forall a. Maybe a
Nothing) ((Proof -> Either Derivation Proof)
-> Maybe Proof -> Maybe (Either Derivation Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right (Maybe Proof -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe Proof)
-> Proof
-> Maybe (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ProofAddr -> Proof -> Maybe Proof
paRemoveRaw ProofAddr
pa)) [Either Derivation Proof]
ps)
    (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c)

-- | Removes the line at a valid t'NodeAddr' and updates all affected references.
naRemove :: NodeAddr -> Proof -> Maybe Proof
naRemove :: NodeAddr -> Proof -> Maybe Proof
naRemove NodeAddr
na (NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
na -> Maybe Int
Nothing) = Maybe Proof
forall a. Maybe a
Nothing
naRemove NodeAddr
na p :: Proof
p@(NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
na -> Just Int
lineNo) = (Reference -> Maybe Reference) -> Proof -> Proof
pMapRefs Reference -> Maybe Reference
goRef (Proof -> Proof) -> Maybe Proof -> Maybe Proof
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Proof -> Maybe Proof
naRemoveRaw NodeAddr
na Proof
p
 where
  goRef :: Reference -> Maybe Reference
  goRef :: Reference -> Maybe Reference
goRef (LineReference Int
line)
    | Int
lineNo Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
line = Maybe Reference
forall a. Maybe a
Nothing
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
line = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Reference
LineReference Int
line
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
line = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Reference
LineReference (Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
  goRef (ProofReference Int
start Int
end)
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
start = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
start Bool -> Bool -> Bool
&& Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
end = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Reference
ProofReference Int
start (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
start Bool -> Bool -> Bool
&& Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
end = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Reference
ProofReference Int
start Int
end

-- | Removes the t'Proof' at a valid t'ProofAddr' and updates all affected references.
paRemove :: ProofAddr -> Proof -> Maybe Proof
paRemove :: ProofAddr -> Proof -> Maybe Proof
paRemove ProofAddr
pa (ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr ProofAddr
pa -> Maybe (Int, Int)
Nothing) = Maybe Proof
forall a. Maybe a
Nothing
paRemove ProofAddr
pa p :: Proof
p@(ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr ProofAddr
pa -> Just (Int
start, Int
end)) =
  (Reference -> Maybe Reference) -> Proof -> Proof
pMapRefs Reference -> Maybe Reference
goRef
    (Proof -> Proof) -> Maybe Proof -> Maybe Proof
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofAddr -> Proof -> Maybe Proof
paRemoveRaw ProofAddr
pa Proof
p
 where
  pLen :: Int
pLen = Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  goRef :: Reference -> Maybe Reference
  goRef :: Reference -> Maybe Reference
goRef (LineReference Int
line)
    | Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
line Bool -> Bool -> Bool
&& Int
line Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
end = Maybe Reference
forall a. Maybe a
Nothing
    | Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
line Bool -> Bool -> Bool
&& Int
line Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
end = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Reference
LineReference (Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
pLen)
    | Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
line = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Reference
LineReference Int
line
  goRef (ProofReference Int
start' Int
end')
    | Int
start Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
start' = Maybe Reference
forall a. Maybe a
Nothing
    | Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
start' = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Reference
ProofReference (Int
start' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
pLen) (Int
end' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
pLen)
    | Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
start' Bool -> Bool -> Bool
&& Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
end' = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Reference
ProofReference Int
start' (Int
end' Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
pLen)
    | Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
start' Bool -> Bool -> Bool
&& Int
start Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
end' = Reference -> Maybe Reference
forall a. a -> Maybe a
Just (Reference -> Maybe Reference) -> Reference -> Maybe Reference
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Reference
ProofReference Int
start' Int
end'

{- | Inserts a line before the given t'NodeAddr' in the t'Proof',
without updating t'Reference's.

* 'naInsertBeforeRaw' ('Left' @a@) @addr@ @proof@
inserts the t'Assumption' @a@ before @addr@.
* 'naInsertBeforeRaw' ('Right' @d@) @addr@ @proof@
inserts the t'Derivation' @d@ before @addr@.

Returns the t'NodeAddr' of the inserted line together with the updated t'Proof'.
Returns v'Nothing' if line could not be inserted.

__Note:__ Use 'naInsertBefore' if references must stay consistent.
-}
naInsertBeforeRaw ::
  Either Assumption Derivation ->
  NodeAddr ->
  Proof ->
  Maybe (NodeAddr, Proof)
-- Inserting before NAAssumption
naInsertBeforeRaw :: Either Assumption Derivation
-> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naInsertBeforeRaw (Left Assumption
a) (NAAssumption Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (Proof -> (NodeAddr, Proof))
-> Maybe Proof -> Maybe (NodeAddr, Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> NodeAddr
NAAssumption Int
n,) (([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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 -> Int -> [Assumption] -> Maybe [Assumption]
forall a. a -> Int -> [a] -> Maybe [a]
insertAt Assumption
a Int
n [Assumption]
fs) ([Either Derivation Proof] -> Maybe [Either Derivation Proof]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Either Derivation Proof]
ps) (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c))
naInsertBeforeRaw (Right Derivation
d) (NAAssumption Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (Proof -> (NodeAddr, Proof))
-> Maybe Proof -> Maybe (NodeAddr, Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
    (Int -> NodeAddr
NAAssumption Int
n,)
    (([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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 -> Int -> [Assumption] -> Maybe [Assumption]
forall a. a -> Int -> [a] -> Maybe [a]
insertAt (Derivation -> Assumption
toAssumption Derivation
d) Int
n [Assumption]
fs) ([Either Derivation Proof] -> Maybe [Either Derivation Proof]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Either Derivation Proof]
ps) (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c))
-- Inserting before NALine
naInsertBeforeRaw (Left Assumption
a) (NALine Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (Proof -> (NodeAddr, Proof))
-> Maybe Proof -> Maybe (NodeAddr, Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
    (Int -> NodeAddr
NALine Int
n,)
    (([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs) (Either Derivation Proof
-> Int
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall a. a -> Int -> [a] -> Maybe [a]
insertAt (Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left (Derivation -> Either Derivation Proof)
-> Derivation -> Either Derivation Proof
forall a b. (a -> b) -> a -> b
$ Assumption -> Derivation
toDerivation Assumption
a) Int
n [Either Derivation Proof]
ps) (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c))
naInsertBeforeRaw (Right Derivation
d) (NALine Int
n) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (Proof -> (NodeAddr, Proof))
-> Maybe Proof -> Maybe (NodeAddr, Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int -> NodeAddr
NALine Int
n,) (([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs) (Either Derivation Proof
-> Int
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall a. a -> Int -> [a] -> Maybe [a]
insertAt (Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left Derivation
d) Int
n [Either Derivation Proof]
ps) (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c))
-- Inserting before NAConclusion
naInsertBeforeRaw (Left Assumption
a) NodeAddr
NAConclusion (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (NodeAddr, Proof) -> Maybe (NodeAddr, Proof)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> NodeAddr
NALine ([Either Derivation Proof] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Derivation Proof]
ps), [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs ([Either Derivation Proof]
ps [Either Derivation Proof]
-> [Either Derivation Proof] -> [Either Derivation Proof]
forall a. Semigroup a => a -> a -> a
<> OneItem [Either Derivation Proof] -> [Either Derivation Proof]
forall x. One x => OneItem x -> x
one (Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left (Derivation -> Either Derivation Proof)
-> Derivation -> Either Derivation Proof
forall a b. (a -> b) -> a -> b
$ Assumption -> Derivation
toDerivation Assumption
a)) Derivation
c)
naInsertBeforeRaw (Right Derivation
d) NodeAddr
NAConclusion (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (NodeAddr, Proof) -> Maybe (NodeAddr, Proof)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> NodeAddr
NALine ([Either Derivation Proof] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Either Derivation Proof]
ps), [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs ([Either Derivation Proof]
ps [Either Derivation Proof]
-> [Either Derivation Proof] -> [Either Derivation Proof]
forall a. Semigroup a => a -> a -> a
<> OneItem [Either Derivation Proof] -> [Either Derivation Proof]
forall x. One x => OneItem x -> x
one (Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left Derivation
d)) Derivation
c)
-- Inserting before NAAfterConclusion
naInsertBeforeRaw (Left Assumption
a) NodeAddr
NAAfterConclusion (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (NodeAddr, Proof) -> Maybe (NodeAddr, Proof)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NodeAddr
NAConclusion, [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs ([Either Derivation Proof]
ps [Either Derivation Proof]
-> [Either Derivation Proof] -> [Either Derivation Proof]
forall a. Semigroup a => a -> a -> a
<> OneItem [Either Derivation Proof] -> [Either Derivation Proof]
forall x. One x => OneItem x -> x
one (Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left Derivation
c)) (Assumption -> Derivation
toDerivation Assumption
a))
naInsertBeforeRaw (Right Derivation
d) NodeAddr
NAAfterConclusion (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (NodeAddr, Proof) -> Maybe (NodeAddr, Proof)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (NodeAddr
NAConclusion, [Assumption] -> [Either Derivation Proof] -> Derivation -> Proof
SubProof [Assumption]
fs ([Either Derivation Proof]
ps [Either Derivation Proof]
-> [Either Derivation Proof] -> [Either Derivation Proof]
forall a. Semigroup a => a -> a -> a
<> OneItem [Either Derivation Proof] -> [Either Derivation Proof]
forall x. One x => OneItem x -> x
one (Derivation -> Either Derivation Proof
forall a b. a -> Either a b
Left Derivation
c)) Derivation
d)
-- Descent
naInsertBeforeRaw Either Assumption Derivation
e (NAProof Int
n NodeAddr
na) (SubProof [Assumption]
fs ps :: [Either Derivation Proof]
ps@(([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n) -> Just (Right Proof
p)) Derivation
c) =
  Either Assumption Derivation
-> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naInsertBeforeRaw Either Assumption Derivation
e NodeAddr
na Proof
p
    Maybe (NodeAddr, Proof)
-> ((NodeAddr, Proof) -> Maybe (NodeAddr, Proof))
-> Maybe (NodeAddr, 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
addr, Proof
p') ->
      (Proof -> (NodeAddr, Proof))
-> Maybe Proof -> Maybe (NodeAddr, Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
        (Int -> NodeAddr -> NodeAddr
NAProof Int
n NodeAddr
addr,)
        ( ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
            (Int
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM Int
n ((Derivation -> Maybe (Either Derivation Proof))
-> (Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (Maybe (Either Derivation Proof)
-> Derivation -> Maybe (Either Derivation Proof)
forall a b. a -> b -> a
const Maybe (Either Derivation Proof)
forall a. Maybe a
Nothing) (Maybe (Either Derivation Proof)
-> Proof -> Maybe (Either Derivation Proof)
forall a b. a -> b -> a
const (Maybe (Either Derivation Proof)
 -> Proof -> Maybe (Either Derivation Proof))
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Proof
-> Maybe (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Derivation Proof -> Maybe (Either Derivation Proof)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Derivation Proof
 -> Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Proof
-> Maybe (Either Derivation Proof)
forall a b. (a -> b) -> a -> b
$ Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right Proof
p')) [Either Derivation Proof]
ps)
            (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c)
        )
naInsertBeforeRaw Either Assumption Derivation
_ NodeAddr
_ Proof
_ = Maybe (NodeAddr, Proof)
forall a. Maybe a
Nothing

{- | Like 'naInsertBeforeRaw', but also updates references affected by the insertion.

Returns the t'NodeAddr' of the inserted line together with the updated t'Proof'.
-}
naInsertBefore ::
  Either Assumption Derivation ->
  NodeAddr ->
  Proof ->
  Maybe (NodeAddr, Proof)
naInsertBefore :: Either Assumption Derivation
-> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naInsertBefore Either Assumption Derivation
e NodeAddr
na Proof
prf = case Either Assumption Derivation
-> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naInsertBeforeRaw Either Assumption Derivation
e NodeAddr
na Proof
prf of
  Just (NodeAddr
na', p :: Proof
p@(NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
na' -> Just Int
lineNo)) ->
    (NodeAddr, Proof) -> Maybe (NodeAddr, Proof)
forall a. a -> Maybe a
Just (NodeAddr
na', (Reference -> Maybe Reference) -> Proof -> Proof
pMapRefs (Reference -> Maybe Reference
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reference -> Maybe Reference)
-> (Reference -> Reference) -> Reference -> Maybe Reference
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof -> NodeAddr -> Int -> Reference -> Reference
goRef Proof
prf NodeAddr
na' Int
lineNo) Proof
p)
  Maybe (NodeAddr, Proof)
_ -> Maybe (NodeAddr, Proof)
forall a. Maybe a
Nothing
 where
  goRef :: Proof -> NodeAddr -> Int -> Reference -> Reference
  goRef :: Proof -> NodeAddr -> Int -> Reference -> Reference
goRef Proof
p NodeAddr
_ Int
lineNo (LineReference Int
line)
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
line = Int -> Reference
LineReference Int
line
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
line = Int -> Reference
LineReference (Int -> Reference) -> Int -> Reference
forall a b. (a -> b) -> a -> b
$ Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  goRef Proof
p NodeAddr
na Int
lineNo (ProofReference Int
start Int
end) = case Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
start Int
end Proof
p of
    Just ProofAddr
pa
      | NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
na ProofAddr
pa -> Int -> Int -> Reference
ProofReference Int
start (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
end -> Int -> Int -> Reference
ProofReference Int
start Int
end
      | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
start -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    Maybe ProofAddr
_ -> Int -> Int -> Reference
ProofReference Int
start Int
end

{- | Inserts a t'Proof' before the t'Proof' at the given t'ProofAddr'
without updating references.
Returns v'Nothing' if t'Proof' could not be inserted.

__Note:__ Use 'paInsertBefore' if references must stay consistent.
-}
paInsertBeforeRaw ::
  Proof ->
  ProofAddr ->
  Proof ->
  Maybe (ProofAddr, Proof)
paInsertBeforeRaw :: Proof -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paInsertBeforeRaw Proof
p (PANested Int
n ProofAddr
PAProof) (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) =
  (Proof -> (ProofAddr, Proof))
-> Maybe Proof -> Maybe (ProofAddr, Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
    (Int -> ProofAddr -> ProofAddr
PANested Int
n ProofAddr
PAProof,)
    ( ([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs)
        (Either Derivation Proof
-> Int
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall a. a -> Int -> [a] -> Maybe [a]
insertAt (Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right Proof
p) Int
n [Either Derivation Proof]
ps)
        (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c)
    )
paInsertBeforeRaw Proof
p (PANested Int
n ProofAddr
pa) (SubProof [Assumption]
fs ps :: [Either Derivation Proof]
ps@(([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n) -> Just (Right Proof
prf)) Derivation
c) =
  Proof -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paInsertBeforeRaw Proof
p ProofAddr
pa Proof
prf
    Maybe (ProofAddr, Proof)
-> ((ProofAddr, Proof) -> Maybe (ProofAddr, Proof))
-> Maybe (ProofAddr, Proof)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(ProofAddr
pa, Proof
p') ->
      (Proof -> (ProofAddr, Proof))
-> Maybe Proof -> Maybe (ProofAddr, Proof)
forall a b. (a -> b) -> Maybe a -> Maybe b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap
        (Int -> ProofAddr -> ProofAddr
PANested Int
n ProofAddr
pa,)
        (([Assumption] -> [Either Derivation Proof] -> Derivation -> Proof)
-> Maybe [Assumption]
-> Maybe [Either Derivation Proof]
-> Maybe Derivation
-> Maybe 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] -> Maybe [Assumption]
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Assumption]
fs) (Int
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> [Either Derivation Proof]
-> Maybe [Either Derivation Proof]
forall (m :: * -> *) a.
MonadFail m =>
Int -> (a -> m a) -> [a] -> m [a]
updateAtM Int
n (Maybe (Either Derivation Proof)
-> Either Derivation Proof -> Maybe (Either Derivation Proof)
forall a b. a -> b -> a
const (Maybe (Either Derivation Proof)
 -> Either Derivation Proof -> Maybe (Either Derivation Proof))
-> (Either Derivation Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Either Derivation Proof -> Maybe (Either Derivation Proof)
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either Derivation Proof
 -> Either Derivation Proof -> Maybe (Either Derivation Proof))
-> Either Derivation Proof
-> Either Derivation Proof
-> Maybe (Either Derivation Proof)
forall a b. (a -> b) -> a -> b
$ Proof -> Either Derivation Proof
forall a b. b -> Either a b
Right Proof
p') [Either Derivation Proof]
ps) (Derivation -> Maybe Derivation
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Derivation
c))
paInsertBeforeRaw Proof
_ ProofAddr
_ Proof
_ = Maybe (ProofAddr, Proof)
forall a. Maybe a
Nothing

{- | Like 'paInsertBeforeRaw', but also updates references affected by the insertion.
Returns the t'ProofAddr' of the inserted t'Proof' together with the updated t'Proof'.
-}
paInsertBefore ::
  Proof ->
  ProofAddr ->
  Proof ->
  Maybe (ProofAddr, Proof)
paInsertBefore :: Proof -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paInsertBefore Proof
p ProofAddr
pa Proof
prf = case Proof -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paInsertBeforeRaw Proof
p ProofAddr
pa Proof
prf of
  Just (ProofAddr
pa, p :: Proof
p@(ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr ProofAddr
pa -> Just (Int
targetStart, Int
targetEnd))) ->
    (ProofAddr, Proof) -> Maybe (ProofAddr, Proof)
forall a. a -> Maybe a
Just (ProofAddr
pa, (Reference -> Maybe Reference) -> Proof -> Proof
pMapRefs (Reference -> Maybe Reference
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reference -> Maybe Reference)
-> (Reference -> Reference) -> Reference -> Maybe Reference
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Proof -> ProofAddr -> Int -> Int -> Reference -> Reference
goRef Proof
prf ProofAddr
pa (Int
targetEnd Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
targetStart Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
targetStart) Proof
p)
  Maybe (ProofAddr, Proof)
_ -> Maybe (ProofAddr, Proof)
forall a. Maybe a
Nothing
 where
  goRef :: Proof -> ProofAddr -> Int -> Int -> Reference -> Reference
  goRef :: Proof -> ProofAddr -> Int -> Int -> Reference -> Reference
goRef Proof
_ ProofAddr
_ Int
offset Int
lineNo (LineReference Int
line)
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
line = Int -> Reference
LineReference Int
line
    | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
line = Int -> Reference
LineReference (Int -> Reference) -> Int -> Reference
forall a b. (a -> b) -> a -> b
$ Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
offset
  goRef Proof
p ProofAddr
pa Int
offset Int
lineNo (ProofReference Int
start Int
end) = case Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
start Int
end Proof
p of
    Just ProofAddr
pa'
      | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
end -> Int -> Int -> Reference
ProofReference Int
start Int
end
      | ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
pa ProofAddr
pa' -> Int -> Int -> Reference
ProofReference Int
start (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
offset)
      | Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
start -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
offset) (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
offset)
    Maybe ProofAddr
_ -> Int -> Int -> Reference
ProofReference Int
start Int
end

{- | Moves the line at @source@ before the line at @target@ in t'Proof' @p@,
without updating any t'Reference's.
Returns the updated target t'NodeAddr' together with the modified t'Proof'
or v'Nothing' on failure.

__Note:__ Use 'naMoveBefore' if references must stay consistent.
-}
naMoveBeforeRaw :: NodeAddr -> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naMoveBeforeRaw :: NodeAddr -> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naMoveBeforeRaw NodeAddr
targetAddr NodeAddr
sourceAddr Proof
p =
  if Bool -> Bool
not (Proof -> NodeAddr -> NodeAddr -> Bool
naCanMoveBefore Proof
p NodeAddr
sourceAddr NodeAddr
targetAddr)
    then Maybe (NodeAddr, Proof)
forall a. Maybe a
Nothing
    else case (NodeAddr -> NodeAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare NodeAddr
targetAddr NodeAddr
sourceAddr, NodeAddr -> Proof -> Maybe (Either Assumption Derivation)
naLookup NodeAddr
sourceAddr Proof
p) of
      (Ordering
LT, Just Either Assumption Derivation
node) -> do
        p' <- NodeAddr -> Proof -> Maybe Proof
naRemoveRaw NodeAddr
sourceAddr Proof
p
        naInsertBeforeRaw node targetAddr p'
      (Ordering
GT, Just Either Assumption Derivation
node) -> do
        -- since 'na' is fixed here already
        (na, p') <- Either Assumption Derivation
-> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naInsertBeforeRaw Either Assumption Derivation
node NodeAddr
targetAddr Proof
p
        p'' <- naRemoveRaw sourceAddr p'
        -- we might need to decrement 'na' by one, if sourceAddr is in the same proof.
        let
          naDecrementWhenOnSameLevel :: NodeAddr -> NodeAddr -> NodeAddr
          naDecrementWhenOnSameLevel (NAAssumption Int
n) NAAssumption{}
            | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 =
                Int -> NodeAddr
NAAssumption (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          naDecrementWhenOnSameLevel (NALine Int
n) NALine{} | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Int -> NodeAddr
NALine (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
          naDecrementWhenOnSameLevel (NAProof Int
n NodeAddr
na) NALine{} | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Int -> NodeAddr -> NodeAddr
NAProof (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) NodeAddr
na
          naDecrementWhenOnSameLevel (NAProof Int
n NodeAddr
na1) (NAProof Int
m NodeAddr
na2)
            | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m =
                Int -> NodeAddr -> NodeAddr
NAProof Int
n (NodeAddr -> NodeAddr) -> NodeAddr -> NodeAddr
forall a b. (a -> b) -> a -> b
$ NodeAddr -> NodeAddr -> NodeAddr
naDecrementWhenOnSameLevel NodeAddr
na1 NodeAddr
na2
          naDecrementWhenOnSameLevel NodeAddr
na NodeAddr
_ = NodeAddr
na
        pure (naDecrementWhenOnSameLevel na sourceAddr, p'')
      (Ordering, Maybe (Either Assumption Derivation))
_ -> Maybe (NodeAddr, Proof)
forall a. Maybe a
Nothing

{- | Returns whether @lineNo@ falls within the given line range,
accounting for same-proof boundary rules.
-}
targetInRange :: Int -> (Int, Int) -> Proof -> Bool
targetInRange :: Int -> (Int, Int) -> Proof -> Bool
targetInRange Int
lineNo (Int
start, Int
end) Proof
p =
  Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
start Bool -> Bool -> Bool
&& Int
lineNo Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
end
    Bool -> Bool -> Bool
|| Int
lineNo Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
start
      Bool -> Bool -> Bool
&& Bool -> (NodeAddr -> Bool) -> Maybe NodeAddr -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe
        Bool
False
        ((NodeAddr -> Bool)
-> (NodeAddr -> NodeAddr -> Bool)
-> Maybe NodeAddr
-> NodeAddr
-> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe (Bool -> NodeAddr -> Bool
forall a b. a -> b -> a
const Bool
False) NodeAddr -> NodeAddr -> Bool
naInSameProof (Int -> Proof -> Maybe NodeAddr
fromLineNo Int
start Proof
p))
        (Int -> Proof -> Maybe NodeAddr
fromLineNo Int
end Proof
p)

{- | Moves the line at @source@ before the line at @target@ in t'Proof' @p@,
and updates all t'Reference's affected by the move.
Returns v'Nothing' if the move is rejected by 'naCanMoveBefore'.
-}
naMoveBefore :: NodeAddr -> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naMoveBefore :: NodeAddr -> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naMoveBefore NodeAddr
targetAddr NodeAddr
sourceAddr Proof
p =
  case NodeAddr -> NodeAddr -> Proof -> Maybe (NodeAddr, Proof)
naMoveBeforeRaw NodeAddr
targetAddr NodeAddr
sourceAddr Proof
p of
    Maybe (NodeAddr, Proof)
Nothing -> Maybe (NodeAddr, Proof)
forall a. Maybe a
Nothing
    Just (NodeAddr
targetAddr', Proof
p') -> (NodeAddr
targetAddr',) (Proof -> (NodeAddr, Proof))
-> Maybe Proof -> Maybe (NodeAddr, Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> NodeAddr -> Proof -> Maybe Proof
go NodeAddr
targetAddr' Proof
p'
 where
  go :: NodeAddr -> Proof -> Maybe Proof
  go :: NodeAddr -> Proof -> Maybe Proof
go NodeAddr
targetAddr' Proof
p' =
    case (NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
targetAddr' Proof
p', NodeAddr -> Proof -> Maybe Int
fromNodeAddr NodeAddr
sourceAddr Proof
p) of
      (Just Int
target, Just Int
source) -> Proof -> Maybe Proof
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof) -> Proof -> Maybe Proof
forall a b. (a -> b) -> a -> b
$ (Reference -> Maybe Reference) -> Proof -> Proof
pMapRefs (Reference -> Maybe Reference
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reference -> Maybe Reference)
-> (Reference -> Reference) -> Reference -> Maybe Reference
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> Int -> Reference -> Reference
goRef Int
target Int
source) Proof
p'
      (Maybe Int, Maybe Int)
_ -> Maybe Proof
forall a. Maybe a
Nothing
  goRef :: Int -> Int -> Reference -> Reference
  goRef :: Int -> Int -> Reference -> Reference
goRef Int
target Int
source (LineReference Int
line)
    | Int
line Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
source = Int -> Reference
LineReference Int
target
    | Int
line Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
source Bool -> Bool -> Bool
&& Int
line Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
target = Int -> Reference
LineReference (Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
    | Int
line Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
source Bool -> Bool -> Bool
&& Int
line Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
target = Int -> Reference
LineReference (Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
    | Bool
otherwise = Int -> Reference
LineReference Int
line
  goRef Int
target Int
source (ProofReference Int
start Int
end) = case Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
start Int
end Proof
p of
    Maybe ProofAddr
Nothing -> Int -> Int -> Reference
ProofReference Int
start Int
end
    Just ProofAddr
pa
      | NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
targetAddr ProofAddr
pa Bool -> Bool -> Bool
&& Int
source Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
start -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) Int
end
      | NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
targetAddr ProofAddr
pa Bool -> Bool -> Bool
&& Int
source Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
end -> Int -> Int -> Reference
ProofReference Int
start (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      | NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
targetAddr ProofAddr
pa -> Int -> Int -> Reference
ProofReference Int
start Int
end
      | Int
target Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
start Bool -> Bool -> Bool
&& NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
sourceAddr ProofAddr
pa -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) Int
end
      | Int
target Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
start Bool -> Bool -> Bool
&& Int
source Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
end -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
      | Int
target Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
end Bool -> Bool -> Bool
&& NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
sourceAddr ProofAddr
pa -> Int -> Int -> Reference
ProofReference Int
start (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      | Int
target Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
end Bool -> Bool -> Bool
&& Int
source Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
start -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1)
      | Bool
otherwise -> Int -> Int -> Reference
ProofReference Int
start Int
end

{- | Returns whether a t'NodeAddr' is contained in the t'Proof'
designated by a t'ProofAddr'.

__Note:__ does not check if the t'NodeAddr' is valid!
-}
naContainedIn :: NodeAddr -> ProofAddr -> Bool
naContainedIn :: NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
_ ProofAddr
PAProof = Bool
True
naContainedIn (NAProof Int
n NodeAddr
na) (PANested Int
m ProofAddr
pa) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
na ProofAddr
pa
naContainedIn NodeAddr
_ ProofAddr
_ = Bool
False

{- | Returns whether a t'ProofAddr' is contained in another t'ProofAddr'.

__Note:__ does not check if either t'ProofAddr' is valid!
-}
paContainedIn :: ProofAddr -> ProofAddr -> Bool
paContainedIn :: ProofAddr -> ProofAddr -> Bool
paContainedIn PANested{} ProofAddr
PAProof = Bool
True
paContainedIn (PANested Int
n ProofAddr
pa1) (PANested Int
m ProofAddr
pa2) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
&& ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
pa1 ProofAddr
pa2
paContainedIn ProofAddr
_ ProofAddr
_ = Bool
False

-- | Returns whether the target address is identical to, or immediately after, the source.
naSameOrNext :: NodeAddr -> NodeAddr -> Proof -> Bool
naSameOrNext :: NodeAddr -> NodeAddr -> Proof -> Bool
naSameOrNext
  (NAProof Int
n NodeAddr
na)
  (NAProof ((Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n) -> Bool
True) NodeAddr
na')
  (SubProof [Assumption]
_ (([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n) -> Just (Right Proof
p)) Derivation
_) =
    NodeAddr -> NodeAddr -> Proof -> Bool
naSameOrNext NodeAddr
na NodeAddr
na' Proof
p
naSameOrNext (NAAssumption Int
n) (NAAssumption Int
m) Proof
_ = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
naSameOrNext (NALine Int
n) (NALine Int
m) Proof
_ = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
naSameOrNext NodeAddr
NAAfterConclusion NodeAddr
NAConclusion Proof
_ = Bool
True
naSameOrNext NodeAddr
NAConclusion NodeAddr
NAConclusion Proof
_ = Bool
True
naSameOrNext NodeAddr
NAConclusion (NALine Int
n) (SubProof [Assumption]
_ [Either Derivation Proof]
ps Derivation
_) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [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
naSameOrNext NodeAddr
_ NodeAddr
_ Proof
_ = Bool
False

-- | Returns whether the target address is identical to, or immediately after, the source.
paSameOrNext :: ProofAddr -> ProofAddr -> Bool
paSameOrNext :: ProofAddr -> ProofAddr -> Bool
paSameOrNext (PANested Int
n ProofAddr
PAProof) (PANested Int
m ProofAddr
PAProof) = Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Bool -> Bool -> Bool
|| Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
paSameOrNext (PANested Int
n ProofAddr
pa1) (PANested Int
m ProofAddr
pa2) | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m = ProofAddr -> ProofAddr -> Bool
paSameOrNext ProofAddr
pa1 ProofAddr
pa2
paSameOrNext ProofAddr
_ ProofAddr
_ = Bool
False

{- | Helper for deciding whether a t'NodeAddr' may be moved to the target position
defaulting to v'True' and only does a real check for v'NAConclusion' where it
checks whether the conclusion has a t'Derivation' that can take its place, when it moves.
-}
naCanMoveConclusion :: NodeAddr -> Proof -> Bool
naCanMoveConclusion :: NodeAddr -> Proof -> Bool
naCanMoveConclusion NodeAddr
NAConclusion (SubProof [Assumption]
fs [Either Derivation Proof]
ps Derivation
c) = case [Either Derivation Proof]
-> Maybe ([Either Derivation Proof], Either Derivation Proof)
forall a. [a] -> Maybe ([a], a)
unsnoc [Either Derivation Proof]
ps of
  Just ([Either Derivation Proof]
_, Left Derivation
_) -> Bool
True
  Maybe ([Either Derivation Proof], Either Derivation Proof)
_ -> Bool
False
naCanMoveConclusion (NAProof Int
n NodeAddr
na) (SubProof [Assumption]
_ (([Either Derivation Proof] -> Int -> Maybe (Either Derivation Proof)
forall a. [a] -> Int -> Maybe a
!!? Int
n) -> Just (Right Proof
p)) Derivation
_) =
  NodeAddr -> Proof -> Bool
naCanMoveConclusion NodeAddr
na Proof
p
naCanMoveConclusion NodeAddr
_ Proof
_ = Bool
True

-- | Returns whether a t'NodeAddr' can be moved before the given target t'NodeAddr'.
naCanMoveBefore :: Proof -> NodeAddr -> NodeAddr -> Bool
naCanMoveBefore :: Proof -> NodeAddr -> NodeAddr -> Bool
naCanMoveBefore Proof
p NodeAddr
source NodeAddr
target =
  NodeAddr -> Proof -> Bool
naCanMoveConclusion NodeAddr
source Proof
p
    Bool -> Bool -> Bool
&& Bool -> Bool
not (NodeAddr -> NodeAddr -> Proof -> Bool
naSameOrNext NodeAddr
target NodeAddr
source Proof
p)

-- | Returns whether a t'ProofAddr' can be moved before the given target t'ProofAddr'.
paCanMoveBefore :: ProofAddr -> ProofAddr -> Bool
paCanMoveBefore :: ProofAddr -> ProofAddr -> Bool
paCanMoveBefore ProofAddr
source ProofAddr
target =
  Bool -> Bool
not (ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
target ProofAddr
source)
    Bool -> Bool -> Bool
&& Bool -> Bool
not (ProofAddr -> ProofAddr -> Bool
paSameOrNext ProofAddr
target ProofAddr
source)

{- | Moves a t'Proof' before another t'Proof' without updating references.

__Note:__ Use 'paMoveBefore' if references must stay consistent.
-}
paMoveBeforeRaw :: ProofAddr -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paMoveBeforeRaw :: ProofAddr -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paMoveBeforeRaw ProofAddr
targetAddr ProofAddr
sourceAddr Proof
p =
  if Bool -> Bool
not (ProofAddr -> ProofAddr -> Bool
paCanMoveBefore ProofAddr
sourceAddr ProofAddr
targetAddr)
    then Maybe (ProofAddr, Proof)
forall a. Maybe a
Nothing
    else case (ProofAddr -> ProofAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ProofAddr
targetAddr ProofAddr
sourceAddr, ProofAddr -> Proof -> Maybe Proof
paLookup ProofAddr
sourceAddr Proof
p) of
      (Ordering
LT, Just Proof
prf) -> do
        p' <- ProofAddr -> Proof -> Maybe Proof
paRemoveRaw ProofAddr
sourceAddr Proof
p
        paInsertBeforeRaw prf targetAddr p'
      (Ordering
GT, Just Proof
prf) -> do
        (pa, p') <- Proof -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paInsertBeforeRaw Proof
prf ProofAddr
targetAddr Proof
p
        p'' <- paRemoveRaw sourceAddr p'
        let
          -- Decrements the new targetAddr by one, on the same level
          -- that sourceAddr lives.
          -- This is needed, because removal happens after insertion, so
          -- paInsertBeforeRaw returns a 'ProofAddr' that is not valid for p''.
          paDecrementWhenOnSameLevel :: ProofAddr -> ProofAddr -> ProofAddr
          paDecrementWhenOnSameLevel
            (PANested Int
n ProofAddr
pa)
            (PANested Int
_ ProofAddr
PAProof; ProofAddr
PAProof) | Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0 = Int -> ProofAddr -> ProofAddr
PANested (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ProofAddr
pa
          paDecrementWhenOnSameLevel pa :: ProofAddr
pa@(PANested Int
n ProofAddr
pa1) (PANested Int
m ProofAddr
pa2)
            | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m = Int -> ProofAddr -> ProofAddr
PANested Int
n (ProofAddr -> ProofAddr) -> ProofAddr -> ProofAddr
forall a b. (a -> b) -> a -> b
$ ProofAddr -> ProofAddr -> ProofAddr
paDecrementWhenOnSameLevel ProofAddr
pa1 ProofAddr
pa2
            | Bool
otherwise = ProofAddr
pa
          paDecrementWhenOnSameLevel ProofAddr
pa ProofAddr
_ = ProofAddr
pa
        pure (paDecrementWhenOnSameLevel pa sourceAddr, p'')
      (Ordering, Maybe Proof)
_ -> Maybe (ProofAddr, Proof)
forall a. Maybe a
Nothing

-- | Moves a t'Proof' before another t'Proof' and updates all affected references.
paMoveBefore :: ProofAddr -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paMoveBefore :: ProofAddr -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paMoveBefore ProofAddr
targetAddr ProofAddr
sourceAddr Proof
p = case ProofAddr -> ProofAddr -> Proof -> Maybe (ProofAddr, Proof)
paMoveBeforeRaw ProofAddr
targetAddr ProofAddr
sourceAddr Proof
p of
  Maybe (ProofAddr, Proof)
Nothing -> Maybe (ProofAddr, Proof)
forall a. Maybe a
Nothing
  Just (ProofAddr
targetAddr', Proof
p') -> (ProofAddr
targetAddr',) (Proof -> (ProofAddr, Proof))
-> Maybe Proof -> Maybe (ProofAddr, Proof)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ProofAddr -> Proof -> Maybe Proof
go ProofAddr
targetAddr' Proof
p'
 where
  go :: ProofAddr -> Proof -> Maybe Proof
  go :: ProofAddr -> Proof -> Maybe Proof
go ProofAddr
targetAddr' Proof
p' =
    case (ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr ProofAddr
targetAddr' Proof
p', ProofAddr -> Proof -> Maybe (Int, Int)
lineRangeFromProofAddr ProofAddr
sourceAddr Proof
p) of
      (Just (Int, Int)
targetRange, Just (Int, Int)
sourceRange) ->
        Proof -> Maybe Proof
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Proof -> Maybe Proof) -> Proof -> Maybe Proof
forall a b. (a -> b) -> a -> b
$ (Reference -> Maybe Reference) -> Proof -> Proof
pMapRefs (Reference -> Maybe Reference
forall a. a -> Maybe a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Reference -> Maybe Reference)
-> (Reference -> Reference) -> Reference -> Maybe Reference
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, Int) -> (Int, Int) -> Reference -> Reference
goRef (Int, Int)
targetRange (Int, Int)
sourceRange) Proof
p'
      (Maybe (Int, Int), Maybe (Int, Int))
_ -> Maybe Proof
forall a. Maybe a
Nothing
  goRef :: (Int, Int) -> (Int, Int) -> Reference -> Reference
  goRef :: (Int, Int) -> (Int, Int) -> Reference -> Reference
goRef (Int
targetStart, Int
targetEnd) (Int
sourceStart, Int
sourceEnd) (LineReference Int
line)
    | (Int, Int) -> Int -> Bool
inRange (Int
sourceStart, Int
sourceEnd) Int
line = Int -> Reference
LineReference (Int
targetStart Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
proofOffset)
    | Int
line Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
sourceStart Bool -> Bool -> Bool
&& Int
targetStart Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
line = Int -> Reference
LineReference (Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
proofLen)
    | Int
line Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
sourceEnd Bool -> Bool -> Bool
&& Int
targetEnd Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
line = Int -> Reference
LineReference (Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
proofLen)
    | Bool
otherwise = Int -> Reference
LineReference Int
line
   where
    proofOffset :: Int
proofOffset = Int
line Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sourceStart
    proofLen :: Int
proofLen = Int
sourceEnd Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sourceStart Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
  goRef (Int
targetStart, Int
targetEnd) (Int
sourceStart, Int
sourceEnd) (ProofReference Int
start Int
end) =
    case Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
start Int
end Proof
p of
      Maybe ProofAddr
Nothing -> Int -> Int -> Reference
ProofReference Int
start Int
end
      Just ProofAddr
pa
        | Int
start Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
sourceStart Bool -> Bool -> Bool
&& Int
end Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
sourceEnd ->
            Int -> Int -> Reference
ProofReference
              Int
targetStart
              Int
targetEnd
        | ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
pa ProofAddr
sourceAddr ->
            Int -> Int -> Reference
ProofReference
              (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
targetStart Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sourceStart))
              (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int
targetEnd Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sourceEnd))
        | ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
sourceAddr ProofAddr
pa Bool -> Bool -> Bool
&& Bool -> Bool
not (ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
targetAddr ProofAddr
pa) ->
            case ProofAddr -> ProofAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ProofAddr
targetAddr ProofAddr
pa of
              Ordering
LT; Ordering
EQ -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
proofLen) Int
end
              Ordering
GT -> Int -> Int -> Reference
ProofReference Int
start (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
proofLen)
        | ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
targetAddr ProofAddr
pa Bool -> Bool -> Bool
&& Bool -> Bool
not (ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
sourceAddr ProofAddr
pa) ->
            case ProofAddr -> ProofAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ProofAddr
sourceAddr ProofAddr
pa of
              Ordering
LT; Ordering
EQ -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
proofLen) Int
end
              Ordering
GT -> Int -> Int -> Reference
ProofReference Int
start (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
proofLen)
        | Bool -> Bool
not (ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
targetAddr ProofAddr
pa) Bool -> Bool -> Bool
&& Bool -> Bool
not (ProofAddr -> ProofAddr -> Bool
paContainedIn ProofAddr
sourceAddr ProofAddr
pa) ->
            case (ProofAddr -> ProofAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ProofAddr
sourceAddr ProofAddr
pa, ProofAddr -> ProofAddr -> Ordering
forall a. Ord a => a -> a -> Ordering
compare ProofAddr
targetAddr ProofAddr
pa) of
              ((,) (Ordering
LT; Ordering
EQ) Ordering
GT) -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
proofLen) (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
proofLen)
              ((,) Ordering
GT (Ordering
LT; Ordering
EQ)) -> Int -> Int -> Reference
ProofReference (Int
start Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
proofLen) (Int
end Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
proofLen)
              (Ordering, Ordering)
_ -> Int -> Int -> Reference
ProofReference Int
start Int
end
        | Bool
otherwise -> Int -> Int -> Reference
ProofReference Int
start Int
end
   where
    proofLen :: Int
proofLen = Int
sourceEnd Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
sourceStart Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1