{- |
Module      : Fitch.Verification
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 implements the proof verification algorithm for Fitch-style
natural deduction t'Proof's. Given a map of t'RuleSpec's, it checks each
line by verifying that its t'RuleApplication' is applied correctly.

Phases of proof verification:

  1. Check that the rule exists
  2. Check that the formula matches the rules' conclusion.
  3. Match references to lines/proof, concretely:
    - check that references are parsed and valid line numbers
    - line references should only refer to lines
    - proof references should refer to proofs,
      i.e. first number is the first line and second number the conclusion
    - referenced line needs to be visible for the referer,
      i.e. not in a subproof or later in the proof.
    - unify referenced lines with expected formula/proof.
  4. Collect name->term mappings.
  5. Verify name->term mappings, the datastructure should be `Map Name [(Int, Term)]`
     to give better error messages. The `Int` is the corresponding line number.
  6. Collect name->formula mappings, using the name->term mappings
     to resolve substitutions.
     The datastructure for name->formula mappings should be
     `Map Name [Either RawFormula [RawFormula]]`, where
     `Name` is e.g. φ, `RawFormula` is a formula that has been identified as φ,
     and `[RawFormula]` is a list of possible formulae that
     can be identified as φ (yielded by backwards-substitution).
  7. Now check that for every φ all its mappings can be made equal by
     choosing from the lists.

It also provides 'checkFreshness' for validating fresh-variable
t'Assumption's, and 'regenerateSymbols' for collecting and validating
function- and predicate-symbol arities across the whole t'Proof'.
-}
module Fitch.Verification where

import App.Model
import Data.Map qualified as M
import Data.Text qualified as T
import Data.Traversable (mapAccumM)
import Fitch.Proof
import Fitch.Unification
import Relude.Extra.Map
import Relude.Extra.Newtype
import Specification.Types
import Util (allCombinations)

{- | Runs the full proof-verification pipeline on a t'Proof',
adding error messages to erroneous t'RuleApplication's

__Note:__ This does not check freshness assumptions or check if arities are consistent.
Use 'checkFreshness' and 'regenerateSymbols' for that.
-}
verifyProof :: [(Name, RuleSpec)] -> Proof -> Proof
verifyProof :: [(Text, RuleSpec)] -> Proof -> Proof
verifyProof [(Text, RuleSpec)]
rules Proof
p = (Int -> Assumption -> Assumption)
-> (Int -> Derivation -> Derivation) -> Proof -> Proof
pMapLinesWithLineNo ((Assumption -> Assumption) -> Int -> Assumption -> Assumption
forall a b. a -> b -> a
const Assumption -> Assumption
forall a. a -> a
id) Int -> Derivation -> Derivation
verifyRule Proof
p
 where
  verifyRule :: Int -> Derivation -> Derivation
  verifyRule :: Int -> Derivation -> Derivation
verifyRule Int
_ d :: Derivation
d@(Derivation Formula
_ (Unparsed{})) = Derivation
d
  verifyRule Int
lineNo d :: Derivation
d@(Derivation f :: Formula
f@(Unparsed{}) Wrapper RuleApplication
wr) =
    let (Text
ruleText, RuleApplication
ra) = case Wrapper RuleApplication
wr of
          (ParsedInvalid Text
ruleText Text
_ RuleApplication
ra) -> (Text
ruleText, RuleApplication
ra)
          (ParsedValid Text
ruleText RuleApplication
ra) -> (Text
ruleText, RuleApplication
ra)
     in Formula -> Wrapper RuleApplication -> Derivation
Derivation Formula
f (Wrapper RuleApplication -> Derivation)
-> Wrapper RuleApplication -> Derivation
forall a b. (a -> b) -> a -> b
$
          Text -> Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
ruleText (Text
"Error:\ninvalid formula at line " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
lineNo) RuleApplication
ra
  verifyRule Int
ruleLine (Derivation Formula
wf Wrapper RuleApplication
wr) = Formula -> Wrapper RuleApplication -> Derivation
Derivation Formula
wf
    (Wrapper RuleApplication -> Derivation)
-> Wrapper RuleApplication -> Derivation
forall a b. (a -> b) -> a -> b
$ (Text -> Wrapper RuleApplication)
-> (() -> Wrapper RuleApplication)
-> Either Text ()
-> Wrapper RuleApplication
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either
      (\Text
err -> Text -> Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
ruleText Text
err RuleApplication
ra)
      (Wrapper RuleApplication -> () -> Wrapper RuleApplication
forall a b. a -> b -> a
const (Wrapper RuleApplication -> () -> Wrapper RuleApplication)
-> Wrapper RuleApplication -> () -> Wrapper RuleApplication
forall a b. (a -> b) -> a -> b
$ Text -> RuleApplication -> Wrapper RuleApplication
forall a. Text -> a -> Wrapper a
ParsedValid Text
ruleText RuleApplication
ra)
    (Either Text () -> Wrapper RuleApplication)
-> Either Text () -> Wrapper RuleApplication
forall a b. (a -> b) -> a -> b
$ do
      spec <- [(Text, RuleSpec)] -> Either Text RuleSpec
checkExistence [(Text, RuleSpec)]
rules
      (conclusion, conclusionSpec) <- checkConclusion spec formula
      formulaSpecs <- unifyReferences 0 spec refs
      termMap <-
        verifyTerms
          ( collectTermsFormula
              ((ruleLine, Right (conclusion, conclusionSpec)) : formulaSpecs)
          )
      formMap <-
        verifyFormulae
          termMap
          ((ruleLine, Right (conclusion, conclusionSpec)) : formulaSpecs)
      pass
   where
    (Text
formulaText, RawFormula
formula, Text
ruleText, ra :: RuleApplication
ra@(RuleApplication Text
ruleName [Reference]
refs)) =
      case (Formula
wf, Wrapper RuleApplication
wr) of
        (ParsedInvalid Text
formulaText Text
_ RawFormula
f, ParsedInvalid Text
ruleText Text
_ RuleApplication
ra) ->
          (Text
formulaText, RawFormula
f, Text
ruleText, RuleApplication
ra)
        (ParsedValid Text
formulaText RawFormula
f, ParsedInvalid Text
ruleText Text
_ RuleApplication
ra) ->
          (Text
formulaText, RawFormula
f, Text
ruleText, RuleApplication
ra)
        (ParsedInvalid Text
formulaText Text
_ RawFormula
f, ParsedValid Text
ruleText RuleApplication
ra) ->
          (Text
formulaText, RawFormula
f, Text
ruleText, RuleApplication
ra)
        (ParsedValid Text
formulaText RawFormula
f, ParsedValid Text
ruleText RuleApplication
ra) ->
          (Text
formulaText, RawFormula
f, Text
ruleText, RuleApplication
ra)
    ---------------------------------------------------
    -- 1. Check that the rule exists.
    checkExistence :: [(Name, RuleSpec)] -> Either Text RuleSpec
    checkExistence :: [(Text, RuleSpec)] -> Either Text RuleSpec
checkExistence [(Text, RuleSpec)]
rules = case ([Item (Map Text RuleSpec)] -> Map Text RuleSpec
forall l. IsList l => [Item l] -> l
fromList [(Text, RuleSpec)]
[Item (Map Text RuleSpec)]
rules :: Map Name RuleSpec) Map Text RuleSpec
-> Key (Map Text RuleSpec) -> Maybe (Val (Map Text RuleSpec))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? Text
Key (Map Text RuleSpec)
ruleName of
      Maybe (Val (Map Text RuleSpec))
Nothing -> Text -> Either Text RuleSpec
forall a b. a -> Either a b
Left (Text
"Error:\nrule (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") does not exist")
      Just Val (Map Text RuleSpec)
spec -> RuleSpec -> Either Text RuleSpec
forall a b. b -> Either a b
Right Val (Map Text RuleSpec)
RuleSpec
spec
    ---------------------------------------------------

    ---------------------------------------------------
    -- 2. Unify conclusion.
    checkConclusion :: RuleSpec -> RawFormula -> Either Text (RawFormula, FormulaSpec)
    checkConclusion :: RuleSpec -> RawFormula -> Either Text (RawFormula, FormulaSpec)
checkConclusion (RuleSpec [FormulaSpec]
_ [ProofSpec]
_ FormulaSpec
expected) RawFormula
actual =
      if RawFormula -> FormulaSpec -> Bool
formulaMatchesSpec RawFormula
actual FormulaSpec
expected
        then (RawFormula, FormulaSpec) -> Either Text (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right (RawFormula
actual, FormulaSpec
expected)
        else
          Text -> Either Text (RawFormula, FormulaSpec)
forall a b. a -> Either a b
Left (Text -> Either Text (RawFormula, FormulaSpec))
-> Text -> Either Text (RawFormula, FormulaSpec)
forall a b. (a -> b) -> a -> b
$
            Text
"Error:\nrule ("
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") can only derive formulae of the form\n"
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FormulaSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint FormulaSpec
expected
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
",\nbut found\n"
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
actual
    ---------------------------------------------------

    ---------------------------------------------------
    -- 3. Unify references
    handleFormula ::
      Int ->
      Formula ->
      FormulaSpec ->
      Either Text (RawFormula, FormulaSpec)
    handleFormula :: Int
-> Formula -> FormulaSpec -> Either Text (RawFormula, FormulaSpec)
handleFormula Int
line Formula
f FormulaSpec
fSpec = case Formula
f of
      Unparsed{} -> Text -> Either Text (RawFormula, FormulaSpec)
forall a b. a -> Either a b
Left (Text -> Either Text (RawFormula, FormulaSpec))
-> Text -> Either Text (RawFormula, FormulaSpec)
forall a b. (a -> b) -> a -> b
$ Text
"Error:\ninvalid formula at line " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
line
      ParsedInvalid Text
txt Text
err RawFormula
rf -> RawFormula -> Either Text (RawFormula, FormulaSpec)
handleRawFormula RawFormula
rf
      ParsedValid Text
txt RawFormula
rf -> RawFormula -> Either Text (RawFormula, FormulaSpec)
handleRawFormula RawFormula
rf
     where
      handleRawFormula :: RawFormula -> Either Text (RawFormula, FormulaSpec)
      handleRawFormula :: RawFormula -> Either Text (RawFormula, FormulaSpec)
handleRawFormula RawFormula
rf =
        if RawFormula -> FormulaSpec -> Bool
formulaMatchesSpec RawFormula
rf FormulaSpec
fSpec
          then (RawFormula, FormulaSpec) -> Either Text (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right (RawFormula
rf, FormulaSpec
fSpec)
          else
            Text -> Either Text (RawFormula, FormulaSpec)
forall a b. a -> Either a b
Left (Text -> Either Text (RawFormula, FormulaSpec))
-> Text -> Either Text (RawFormula, FormulaSpec)
forall a b. (a -> b) -> a -> b
$
              Text
"Error:\nfound "
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
rf
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nat line "
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
line
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
",\nbut expected a formula of the form\n"
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> FormulaSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint FormulaSpec
fSpec
    handleAssumption ::
      Int -> Assumption -> AssumptionSpec -> Either Text (RawAssumption, AssumptionSpec)
    handleAssumption :: Int
-> Assumption
-> AssumptionSpec
-> Either Text (RawAssumption, AssumptionSpec)
handleAssumption Int
line (Wrapper RawAssumption
a, Wrapper RuleApplication
_) AssumptionSpec
aSpec = case Wrapper RawAssumption
a of
      Unparsed{} -> Text -> Either Text (RawAssumption, AssumptionSpec)
forall a b. a -> Either a b
Left (Text -> Either Text (RawAssumption, AssumptionSpec))
-> Text -> Either Text (RawAssumption, AssumptionSpec)
forall a b. (a -> b) -> a -> b
$ Text
"Error:\ninvalid formula at line " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
line
      (ParsedInvalid Text
txt Text
err RawAssumption
ra) -> RawAssumption -> Either Text (RawAssumption, AssumptionSpec)
handleRawAssumption RawAssumption
ra
      (ParsedValid Text
txt RawAssumption
ra) -> RawAssumption -> Either Text (RawAssumption, AssumptionSpec)
handleRawAssumption RawAssumption
ra
     where
      handleRawAssumption :: RawAssumption -> Either Text (RawAssumption, AssumptionSpec)
      handleRawAssumption :: RawAssumption -> Either Text (RawAssumption, AssumptionSpec)
handleRawAssumption RawAssumption
ra =
        if RawAssumption -> AssumptionSpec -> Bool
assumptionMatchesSpec RawAssumption
ra AssumptionSpec
aSpec
          then (RawAssumption, AssumptionSpec)
-> Either Text (RawAssumption, AssumptionSpec)
forall a b. b -> Either a b
Right (RawAssumption
ra, AssumptionSpec
aSpec)
          else
            Text -> Either Text (RawAssumption, AssumptionSpec)
forall a b. a -> Either a b
Left (Text -> Either Text (RawAssumption, AssumptionSpec))
-> Text -> Either Text (RawAssumption, AssumptionSpec)
forall a b. (a -> b) -> a -> b
$
              Text
"Error:\nfound formula\n"
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawAssumption -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawAssumption
ra
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nat line "
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
line
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
",\nbut expected a formula of the form\n"
                Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> AssumptionSpec -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint AssumptionSpec
aSpec
    unifyReferences ::
      Int ->
      RuleSpec ->
      [Reference] ->
      Either Text [(Pos, Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
    unifyReferences :: Int
-> RuleSpec
-> [Reference]
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
unifyReferences
      Int
n
      (RuleSpec (FormulaSpec
fSpec : [FormulaSpec]
fSpecs) [ProofSpec]
pSpecs FormulaSpec
cSpec)
      (LineReference Int
refLine : [Reference]
refs) = do
        f <- Int -> Proof -> Either Text (Either Assumption Formula)
lookupLineReference Int
refLine Proof
p
        f' <- case f of
          Left Assumption
a -> (RawAssumption, AssumptionSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. a -> Either a b
Left ((RawAssumption, AssumptionSpec)
 -> Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
-> Either Text (RawAssumption, AssumptionSpec)
-> Either
     Text
     (Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Assumption
-> AssumptionSpec
-> Either Text (RawAssumption, AssumptionSpec)
handleAssumption Int
refLine Assumption
a (FormulaSpec -> AssumptionSpec
AssumptionSpec FormulaSpec
fSpec)
          Right Formula
f -> (RawFormula, FormulaSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right ((RawFormula, FormulaSpec)
 -> Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
-> Either Text (RawFormula, FormulaSpec)
-> Either
     Text
     (Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Formula -> FormulaSpec -> Either Text (RawFormula, FormulaSpec)
handleFormula Int
refLine Formula
f FormulaSpec
fSpec
        fs <- unifyReferences (n + 1) (RuleSpec fSpecs pSpecs cSpec) refs
        pure ((refLine, f') : fs)
    unifyReferences
      Int
n
      (RuleSpec [] (ProofSpec
pSpec : [ProofSpec]
pSpecs) FormulaSpec
cSpec)
      (ProofReference Int
start Int
end : [Reference]
refs) = do
        prf <- Int -> Int -> Proof -> Either Text Proof
lookupProofReference Int
start Int
end Proof
p
        fs <- handleProof (start, end) prf pSpec
        fs' <- unifyReferences (n + 1) (RuleSpec [] pSpecs cSpec) refs
        pure (fs <> fs')
       where
        handleProof ::
          (Int, Int) ->
          Proof ->
          ProofSpec ->
          Either Text [(Pos, Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
        handleProof :: (Int, Int)
-> Proof
-> ProofSpec
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
handleProof (Int
start, Int
end) (SubProof [Assumption]
fs [Either Derivation Proof]
ps (Derivation Formula
c Wrapper RuleApplication
r)) ([AssumptionSpec]
fSpecs, FormulaSpec
cSpec)
          | [Assumption] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Assumption]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= [AssumptionSpec] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AssumptionSpec]
fSpecs =
              Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      [(Int,
        Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))])
-> Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. (a -> b) -> a -> b
$
                Text
"Error:\nsubproof at range "
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> 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
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nshould have "
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show ([AssumptionSpec] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AssumptionSpec]
fSpecs)
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" assumptions, but found "
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show ([Assumption] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Assumption]
fs)
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" assumptions"
          | Bool
otherwise = do
              (_, fs'') <-
                (Int
 -> (Assumption, AssumptionSpec)
 -> Either Text (Int, (Int, RawAssumption, AssumptionSpec)))
-> Int
-> [(Assumption, AssumptionSpec)]
-> Either Text (Int, [(Int, RawAssumption, AssumptionSpec)])
forall (m :: * -> *) (t :: * -> *) s a b.
(Monad m, Traversable t) =>
(s -> a -> m (s, b)) -> s -> t a -> m (s, t b)
mapAccumM
                  ( \Int
s (Assumption
a, AssumptionSpec
fSpec) -> do
                      (a', fSpec') <- Int
-> Assumption
-> AssumptionSpec
-> Either Text (RawAssumption, AssumptionSpec)
handleAssumption Int
s Assumption
a AssumptionSpec
fSpec
                      pure (s + 1, (s, a', fSpec'))
                  )
                  Int
start
                  ([Assumption] -> [AssumptionSpec] -> [(Assumption, AssumptionSpec)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Assumption]
fs [AssumptionSpec]
fSpecs)
              (c', cSpec') <- handleFormula end c cSpec
              pure $
                map (\(Int
ln, RawAssumption
f, AssumptionSpec
fspec) -> (Int
ln, (RawAssumption, AssumptionSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. a -> Either a b
Left (RawAssumption
f, AssumptionSpec
fspec))) fs'' <> [(end, Right (c', cSpec'))]
    unifyReferences Int
n (RuleSpec (FormulaSpec
_ : [FormulaSpec]
_) [ProofSpec]
_ FormulaSpec
_) (ProofReference Int
start Int
end : [Reference]
refs) =
      Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      [(Int,
        Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))])
-> Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. (a -> b) -> a -> b
$
        Text
"Error:\nrule ("
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") expects a single line at position "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
",\nbut found the range "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> 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
    unifyReferences Int
n (RuleSpec [FormulaSpec]
_ (ProofSpec
_ : [ProofSpec]
_) FormulaSpec
_) (LineReference Int
line : [Reference]
refs) =
      Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      [(Int,
        Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))])
-> Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. (a -> b) -> a -> b
$
        Text
"Error:\nrule ("
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") expects a line range at position "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
",\nbut found the single line "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
line
    unifyReferences Int
n (RuleSpec (FormulaSpec
_ : [FormulaSpec]
fs) [ProofSpec]
ps FormulaSpec
_) [] =
      Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      [(Int,
        Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))])
-> Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. (a -> b) -> a -> b
$
        Text
"Error:\nrule ("
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") expects "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [FormulaSpec] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [FormulaSpec]
fs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [ProofSpec] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ProofSpec]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" references,\nbut found "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" references"
    unifyReferences Int
n (RuleSpec [] (ProofSpec
_ : [ProofSpec]
ps) FormulaSpec
_) [] =
      Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      [(Int,
        Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))])
-> Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. (a -> b) -> a -> b
$
        Text
"Error:\nrule ("
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") expects "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [ProofSpec] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [ProofSpec]
ps Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" references,\nbut found "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" references"
    unifyReferences Int
n (RuleSpec [] [] FormulaSpec
_) (Reference
_ : [Reference]
refs) =
      Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      [(Int,
        Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))])
-> Text
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. (a -> b) -> a -> b
$
        Text
"Error:\nrule ("
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") expects "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
n
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" references,\nbut found "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Reference] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Reference]
refs Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" references"
    unifyReferences Int
_ (RuleSpec [] [] FormulaSpec
_) [] = [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Either
     Text
     [(Int,
       Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b. b -> Either a b
Right []
    ---------------------------------------------------

    ---------------------------------------------------
    -- 4. Collect terms
    collectTermsTerm :: [(Pos, Term, TermSpec)] -> Map Name (NonEmpty (Pos, Term))
    collectTermsTerm :: [(Int, Term, TermSpec)] -> Map Text (NonEmpty (Int, Term))
collectTermsTerm [] = Map Text (NonEmpty (Int, Term))
forall a. Monoid a => a
mempty
    collectTermsTerm ((Int
line, Fun Text
_ [Term]
ts, TFun Text
_ [TermSpec]
ss) : [(Int, Term, TermSpec)]
rest) =
      [(Int, Term, TermSpec)] -> Map Text (NonEmpty (Int, Term))
collectTermsTerm ((Term -> TermSpec -> (Int, Term, TermSpec))
-> [Term] -> [TermSpec] -> [(Int, Term, TermSpec)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Term
t TermSpec
s -> (Int
line, Term
t, TermSpec
s)) [Term]
ts [TermSpec]
ss [(Int, Term, TermSpec)]
-> [(Int, Term, TermSpec)] -> [(Int, Term, TermSpec)]
forall a. Semigroup a => a -> a -> a
<> [(Int, Term, TermSpec)]
rest)
    collectTermsTerm ((Int
line, Term
t, TPlaceholder Text
n) : [(Int, Term, TermSpec)]
rest) =
      (Val (Map Text (NonEmpty (Int, Term)))
 -> Val (Map Text (NonEmpty (Int, Term)))
 -> Val (Map Text (NonEmpty (Int, Term))))
-> Key (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
-> Map Text (NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
forall t.
DynamicMap t =>
(Val t -> Val t -> Val t) -> Key t -> Val t -> t -> t
insertWith
        NonEmpty (Int, Term)
-> NonEmpty (Int, Term) -> NonEmpty (Int, Term)
Val (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
forall a. Semigroup a => a -> a -> a
(<>)
        Text
Key (Map Text (NonEmpty (Int, Term)))
n
        [(Int
line, Term
t)]
        ([(Int, Term, TermSpec)] -> Map Text (NonEmpty (Int, Term))
collectTermsTerm [(Int, Term, TermSpec)]
rest)
    collectTermsTerm ((Int, Term, TermSpec)
_ : [(Int, Term, TermSpec)]
rest) = [(Int, Term, TermSpec)] -> Map Text (NonEmpty (Int, Term))
collectTermsTerm [(Int, Term, TermSpec)]
rest

    collectTermsFormula ::
      [(Pos, Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))] ->
      Map Name (NonEmpty (Pos, Term))
    collectTermsFormula :: [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Map Text (NonEmpty (Int, Term))
collectTermsFormula ((Int
line, Right (InfixPred Text
_ Term
p1 Term
p2, FInfixPred Text
_ TermSpec
q1 TermSpec
q2)) : [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest) =
      (NonEmpty (Int, Term)
 -> NonEmpty (Int, Term) -> NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith
        NonEmpty (Int, Term)
-> NonEmpty (Int, Term) -> NonEmpty (Int, Term)
forall a. Semigroup a => a -> a -> a
(<>)
        ([(Int, Term, TermSpec)] -> Map Text (NonEmpty (Int, Term))
collectTermsTerm [(Int
line, Term
p1, TermSpec
q1), (Int
line, Term
p2, TermSpec
q2)])
        ([(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Map Text (NonEmpty (Int, Term))
collectTermsFormula [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest)
    collectTermsFormula ((Int
line, Right (Pred Text
_ [Term]
ps, FPred Text
_ [TermSpec]
qs)) : [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest) =
      (NonEmpty (Int, Term)
 -> NonEmpty (Int, Term) -> NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith
        NonEmpty (Int, Term)
-> NonEmpty (Int, Term) -> NonEmpty (Int, Term)
forall a. Semigroup a => a -> a -> a
(<>)
        ([(Int, Term, TermSpec)] -> Map Text (NonEmpty (Int, Term))
collectTermsTerm ((Term -> TermSpec -> (Int, Term, TermSpec))
-> [Term] -> [TermSpec] -> [(Int, Term, TermSpec)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\Term
p TermSpec
q -> (Int
line, Term
p, TermSpec
q)) [Term]
ps [TermSpec]
qs))
        ([(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Map Text (NonEmpty (Int, Term))
collectTermsFormula [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest)
    collectTermsFormula ((Int
line, Right (Opr Text
_ [RawFormula]
fs, FOpr Text
_ [FormulaSpec]
fs')) : [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest) =
      [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Map Text (NonEmpty (Int, Term))
collectTermsFormula ((RawFormula
 -> FormulaSpec
 -> (Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)))
-> [RawFormula]
-> [FormulaSpec]
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (\RawFormula
f FormulaSpec
f' -> (Int
line, (RawFormula, FormulaSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right (RawFormula
f, FormulaSpec
f'))) [RawFormula]
fs [FormulaSpec]
fs' [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a. Semigroup a => a -> a -> a
<> [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest)
    collectTermsFormula ((Int
line, Right (Quantifier Text
_ Text
v RawFormula
f, FQuantifier Text
_ Text
v' FormulaSpec
f')) : [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest) =
      (Val (Map Text (NonEmpty (Int, Term)))
 -> Val (Map Text (NonEmpty (Int, Term)))
 -> Val (Map Text (NonEmpty (Int, Term))))
-> Key (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
-> Map Text (NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
forall t.
DynamicMap t =>
(Val t -> Val t -> Val t) -> Key t -> Val t -> t -> t
insertWith
        NonEmpty (Int, Term)
-> NonEmpty (Int, Term) -> NonEmpty (Int, Term)
Val (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
forall a. Semigroup a => a -> a -> a
(<>)
        Text
Key (Map Text (NonEmpty (Int, Term)))
v'
        [(Int
line, Text -> Term
Var Text
v)]
        ([(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Map Text (NonEmpty (Int, Term))
collectTermsFormula ((Int
line, (RawFormula, FormulaSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right (RawFormula
f, FormulaSpec
f')) (Int,
 Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a. a -> [a] -> [a]
: [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest))
    collectTermsFormula ((Int
line, Left (FreshVar Text
m, FFreshVar Text
n)) : [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest) =
      (Val (Map Text (NonEmpty (Int, Term)))
 -> Val (Map Text (NonEmpty (Int, Term)))
 -> Val (Map Text (NonEmpty (Int, Term))))
-> Key (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
-> Map Text (NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
forall t.
DynamicMap t =>
(Val t -> Val t -> Val t) -> Key t -> Val t -> t -> t
insertWith NonEmpty (Int, Term)
-> NonEmpty (Int, Term) -> NonEmpty (Int, Term)
Val (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
-> Val (Map Text (NonEmpty (Int, Term)))
forall a. Semigroup a => a -> a -> a
(<>) Text
Key (Map Text (NonEmpty (Int, Term)))
n [(Int
line, Text -> Term
Var Text
m)] (Map Text (NonEmpty (Int, Term))
 -> Map Text (NonEmpty (Int, Term)))
-> Map Text (NonEmpty (Int, Term))
-> Map Text (NonEmpty (Int, Term))
forall a b. (a -> b) -> a -> b
$ [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Map Text (NonEmpty (Int, Term))
collectTermsFormula [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest
    collectTermsFormula ((Int
line, Left (RawAssumption RawFormula
f, AssumptionSpec FormulaSpec
fSpec)) : [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest) =
      [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Map Text (NonEmpty (Int, Term))
collectTermsFormula ((Int
line, (RawFormula, FormulaSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right (RawFormula
f, FormulaSpec
fSpec)) (Int,
 Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
forall a. a -> [a] -> [a]
: [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest)
    collectTermsFormula ((Int,
 Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
_ : [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest) = [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Map Text (NonEmpty (Int, Term))
collectTermsFormula [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
rest
    collectTermsFormula [] = Map Text (NonEmpty (Int, Term))
forall a. Monoid a => a
mempty
    ---------------------------------------------------

    ---------------------------------------------------
    -- 5. Verify term mappings
    verifyTerms :: Map Name (NonEmpty (Pos, Term)) -> Either Text (Map Name (Pos, Term))
    verifyTerms :: Map Text (NonEmpty (Int, Term))
-> Either Text (Map Text (Int, Term))
verifyTerms Map Text (NonEmpty (Int, Term))
m = [(Text, (Int, Term))] -> Map Text (Int, Term)
[Item (Map Text (Int, Term))] -> Map Text (Int, Term)
forall l. IsList l => [Item l] -> l
fromList ([(Text, (Int, Term))] -> Map Text (Int, Term))
-> Either Text [(Text, (Int, Term))]
-> Either Text (Map Text (Int, Term))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((Text, NonEmpty (Int, Term)) -> Either Text (Text, (Int, Term)))
-> [(Text, NonEmpty (Int, Term))]
-> Either Text [(Text, (Int, Term))]
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 (Text, NonEmpty (Int, Term)) -> Either Text (Text, (Int, Term))
makeUnique (Map Text (NonEmpty (Int, Term)) -> [(Text, NonEmpty (Int, Term))]
forall t a b. (IsList t, Item t ~ (a, b)) => t -> [(a, b)]
toPairs Map Text (NonEmpty (Int, Term))
m)
     where
      makeUnique :: (Name, NonEmpty (Pos, Term)) -> Either Text (Name, (Pos, Term))
      makeUnique :: (Text, NonEmpty (Int, Term)) -> Either Text (Text, (Int, Term))
makeUnique (Text
v, (Int, Term)
t :| [(Int, Term)]
ts) = do
        ((Int, Term) -> (Int, Term) -> Either Text (Int, Term))
-> (Int, Term) -> [(Int, Term)] -> Either Text (Int, Term)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
          ( \(Int
_, Term
lastTerm) (Int
currTermLine, Term
currTerm) ->
              if Term
lastTerm Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
currTerm
                then (Int, Term) -> Either Text (Int, Term)
forall a b. b -> Either a b
Right (Int
currTermLine, Term
currTerm)
                else
                  Text -> Either Text (Int, Term)
forall a b. a -> Either a b
Left (Text -> Either Text (Int, Term))
-> Text -> Either Text (Int, Term)
forall a b. (a -> b) -> a -> b
$
                    Text
"Error:\ntrying to verify that all assignments\nof placeholder "
                      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v
                      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" in rule ("
                      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
                      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") are the same, but found\n"
                      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
<> Term -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Term
lastTerm
                      Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nand\n"
                      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
<> Term -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Term
currTerm
          )
          (Int, Term)
t
          [(Int, Term)]
ts
        (Text, (Int, Term)) -> Either Text (Text, (Int, Term))
forall a. a -> Either Text a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Text
v, (Int, Term)
t)
    ---------------------------------------------------

    ---------------------------------------------------
    -- 6. Collect formula mappings using backward substitution
    verifyFormulae ::
      Map Name (Pos, Term) ->
      [(Pos, Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))] ->
      Either Text (Map Name RawFormula)
    verifyFormulae :: Map Text (Int, Term)
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> Either Text (Map Text RawFormula)
verifyFormulae Map Text (Int, Term)
termMap [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
formsAndSpecs = do
      formMap <-
        Map
  Text
  (NonEmpty
     (Either
        RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Either Text (Map Text RawFormula)
reduceFormulae (Map
   Text
   (NonEmpty
      (Either
         RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
 -> Either Text (Map Text RawFormula))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Either Text (Map Text RawFormula)
forall a b. (a -> b) -> a -> b
$ (NonEmpty RawFormula
 -> NonEmpty
      (Either
         RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Map Text (NonEmpty RawFormula)
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (RawFormula
-> Either
     RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
forall a b. a -> Either a b
Left (RawFormula
 -> Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty RawFormula
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Map Text (NonEmpty RawFormula)
 -> Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Map Text (NonEmpty RawFormula)
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
forall a b. (a -> b) -> a -> b
$ [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae ((Int,
 Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. (a, b) -> b
snd ((Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
 -> Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
-> [(Int,
     Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [(Int,
  Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))]
formsAndSpecs)
      formMap' <- collectMoreFormulae formMap (snd <$> formsAndSpecs)
      reduceFormulae formMap'
     where
      collectSimpleFormulae ::
        [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)] ->
        Map Name (NonEmpty RawFormula)
      collectSimpleFormulae :: [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae [] = Map Text (NonEmpty RawFormula)
forall a. Monoid a => a
mempty
      collectSimpleFormulae (Right ((Pred{}; InfixPred{}), (FPred{}; FInfixPred{})) : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) =
        [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
      collectSimpleFormulae (Right (Opr Text
_ [RawFormula]
fs, FOpr Text
_ [FormulaSpec]
fSpecs) : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) =
        [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae ([Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
 -> Map Text (NonEmpty RawFormula))
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
forall a b. (a -> b) -> a -> b
$ (RawFormula
 -> FormulaSpec
 -> Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
-> [RawFormula]
-> [FormulaSpec]
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (((RawFormula, FormulaSpec)
 -> Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec))
-> RawFormula
-> FormulaSpec
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (RawFormula, FormulaSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right) [RawFormula]
fs [FormulaSpec]
fSpecs [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
forall a. Semigroup a => a -> a -> a
<> [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
      collectSimpleFormulae (Right (Quantifier Text
_ Text
_ RawFormula
f, FQuantifier Text
_ Text
_ FormulaSpec
fSpec) : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) =
        [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae ([Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
 -> Map Text (NonEmpty RawFormula))
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
forall a b. (a -> b) -> a -> b
$ (RawFormula, FormulaSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right (RawFormula
f, FormulaSpec
fSpec) Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
forall a. a -> [a] -> [a]
: [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
      collectSimpleFormulae (Left (FreshVar Text
n, FFreshVar Text
m) : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) =
        [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
      collectSimpleFormulae (Left (RawAssumption RawFormula
f, AssumptionSpec FormulaSpec
fSpec) : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) =
        [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae ((RawFormula, FormulaSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right (RawFormula
f, FormulaSpec
fSpec) Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
forall a. a -> [a] -> [a]
: [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest)
      collectSimpleFormulae (Right (RawFormula
f, FPlaceholder Text
n) : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) =
        (Val (Map Text (NonEmpty RawFormula))
 -> Val (Map Text (NonEmpty RawFormula))
 -> Val (Map Text (NonEmpty RawFormula)))
-> Key (Map Text (NonEmpty RawFormula))
-> Val (Map Text (NonEmpty RawFormula))
-> Map Text (NonEmpty RawFormula)
-> Map Text (NonEmpty RawFormula)
forall t.
DynamicMap t =>
(Val t -> Val t -> Val t) -> Key t -> Val t -> t -> t
insertWith
          NonEmpty RawFormula -> NonEmpty RawFormula -> NonEmpty RawFormula
Val (Map Text (NonEmpty RawFormula))
-> Val (Map Text (NonEmpty RawFormula))
-> Val (Map Text (NonEmpty RawFormula))
forall a. Semigroup a => a -> a -> a
(<>)
          Text
Key (Map Text (NonEmpty RawFormula))
n
          (RawFormula
f RawFormula -> [RawFormula] -> NonEmpty RawFormula
forall a. a -> [a] -> NonEmpty a
:| [])
          (Map Text (NonEmpty RawFormula) -> Map Text (NonEmpty RawFormula))
-> Map Text (NonEmpty RawFormula) -> Map Text (NonEmpty RawFormula)
forall a b. (a -> b) -> a -> b
$ [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
      collectSimpleFormulae (Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
_ : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) = [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Map Text (NonEmpty RawFormula)
collectSimpleFormulae [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
      reduceFormulae ::
        Map Name (NonEmpty (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))) ->
        Either Text (Map Name RawFormula)
      reduceFormulae :: Map
  Text
  (NonEmpty
     (Either
        RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Either Text (Map Text RawFormula)
reduceFormulae = (Text
 -> NonEmpty
      (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
 -> Either Text RawFormula)
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Either Text (Map Text RawFormula)
forall (t :: * -> *) k a b.
Applicative t =>
(k -> a -> t b) -> Map k a -> t (Map k b)
M.traverseWithKey Text
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> Either Text RawFormula
reduceHelper
       where
        reduceHelper ::
          Name ->
          NonEmpty (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)) ->
          Either Text RawFormula
        reduceHelper :: Text
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> Either Text RawFormula
reduceHelper Text
n (Left RawFormula
f :| [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest) = Text
-> RawFormula
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> Either Text RawFormula
go Text
n RawFormula
f [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest
        reduceHelper Text
n (Right ((RawFormula, Subst Term)
fOrig, RawFormula
f :| []) :| [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest) = Text
-> RawFormula
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> Either Text RawFormula
go Text
n RawFormula
f [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest
        reduceHelper Text
n (Right ((RawFormula, Subst Term)
fOrig, RawFormula
f :| (RawFormula
f' : [RawFormula]
fs)) :| [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest) = case Text
-> RawFormula
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> Either Text RawFormula
go Text
n RawFormula
f [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest of
          Left Text
err -> Text
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> Either Text RawFormula
reduceHelper Text
n (((RawFormula, Subst Term), NonEmpty RawFormula)
-> Either
     RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
forall a b. b -> Either a b
Right ((RawFormula, Subst Term)
fOrig, RawFormula
f' RawFormula -> [RawFormula] -> NonEmpty RawFormula
forall a. a -> [a] -> NonEmpty a
:| [RawFormula]
fs) Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
forall a. a -> [a] -> NonEmpty a
:| [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest)
          Right RawFormula
f -> RawFormula -> Either Text RawFormula
forall a b. b -> Either a b
Right RawFormula
f
        go ::
          Name ->
          RawFormula ->
          [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)] ->
          Either Text RawFormula
        go :: Text
-> RawFormula
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> Either Text RawFormula
go Text
n RawFormula
f [] = RawFormula -> Either Text RawFormula
forall a b. b -> Either a b
Right RawFormula
f
        go Text
n RawFormula
f (Left RawFormula
f' : [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest) =
          if RawFormula
f RawFormula -> RawFormula -> Bool
forall a. Eq a => a -> a -> Bool
== RawFormula
f'
            then
              Text
-> RawFormula
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> Either Text RawFormula
go Text
n RawFormula
f' [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest
            else
              Text -> Either Text RawFormula
forall a b. a -> Either a b
Left (Text -> Either Text RawFormula) -> Text -> Either Text RawFormula
forall a b. (a -> b) -> a -> b
$
                Text
"Error:\ntrying to verify that all assignments\nof placeholder "
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" in rule ("
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") are the same, but found\n"
                  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
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
f
                  Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nand\n"
                  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
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
f'
        go Text
n RawFormula
f (Right ((RawFormula, Subst Term), NonEmpty RawFormula)
fs' : [Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
rest) = ((RawFormula, Subst Term), NonEmpty RawFormula)
-> NonEmpty RawFormula -> Either Text RawFormula
mapFs ((RawFormula, Subst Term), NonEmpty RawFormula)
fs' (((RawFormula, Subst Term), NonEmpty RawFormula)
-> NonEmpty RawFormula
forall a b. (a, b) -> b
snd ((RawFormula, Subst Term), NonEmpty RawFormula)
fs')
         where
          mapFs ::
            ((RawFormula, Subst Term), NonEmpty RawFormula) ->
            NonEmpty RawFormula ->
            Either Text RawFormula
          mapFs :: ((RawFormula, Subst Term), NonEmpty RawFormula)
-> NonEmpty RawFormula -> Either Text RawFormula
mapFs ((RawFormula
fOrig, Subst Term
sub), RawFormula
f' :| []) NonEmpty RawFormula
allFs =
            if RawFormula
f RawFormula -> RawFormula -> Bool
forall a. Eq a => a -> a -> Bool
/= RawFormula
f'
              then
                Text -> Either Text RawFormula
forall a b. a -> Either a b
Left (Text -> Either Text RawFormula) -> Text -> Either Text RawFormula
forall a b. (a -> b) -> a -> b
$
                  Text
"Error:\ntrying to find an assignment to placeholder "
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nin rule ("
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
ruleName
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
") such that the equations\n"
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Subst Term -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Subst Term
sub
                    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
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\n"
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
n
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Subst Term -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Subst Term
sub
                    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
fOrig
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nhold, but none found"
              else RawFormula -> Either Text RawFormula
forall a b. b -> Either a b
Right RawFormula
f'
          mapFs ((RawFormula, Subst Term)
fOrig, RawFormula
f' :| (RawFormula
f'' : [RawFormula]
fs)) NonEmpty RawFormula
allFs = if RawFormula
f RawFormula -> RawFormula -> Bool
forall a. Eq a => a -> a -> Bool
/= RawFormula
f' then ((RawFormula, Subst Term), NonEmpty RawFormula)
-> NonEmpty RawFormula -> Either Text RawFormula
mapFs ((RawFormula, Subst Term)
fOrig, RawFormula
f'' RawFormula -> [RawFormula] -> NonEmpty RawFormula
forall a. a -> [a] -> NonEmpty a
:| [RawFormula]
fs) NonEmpty RawFormula
allFs else RawFormula -> Either Text RawFormula
forall a b. b -> Either a b
Right RawFormula
f'

      collectMoreFormulae ::
        Map Name RawFormula ->
        [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)] ->
        Either
          Text
          (Map Name (NonEmpty (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
      collectMoreFormulae :: Map Text RawFormula
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
collectMoreFormulae Map Text RawFormula
formMap [] = Map
  Text
  (NonEmpty
     (Either
        RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a b. b -> Either a b
Right (Map
   Text
   (NonEmpty
      (Either
         RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
 -> Either
      Text
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> (Map Text RawFormula
    -> Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Map Text RawFormula
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RawFormula
 -> NonEmpty
      (Either
         RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Map Text RawFormula
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
forall a b k. (a -> b) -> Map k a -> Map k b
M.map (\RawFormula
f -> RawFormula
-> Either
     RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
forall a b. a -> Either a b
Left RawFormula
f Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
forall a. a -> [a] -> NonEmpty a
:| []) (Map Text RawFormula
 -> Either
      Text
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> Map Text RawFormula
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a b. (a -> b) -> a -> b
$ Map Text RawFormula
formMap
      collectMoreFormulae Map Text RawFormula
formMap (Left (RawAssumption RawFormula
f, AssumptionSpec FormulaSpec
fSpec) : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) =
        Map Text RawFormula
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
collectMoreFormulae Map Text RawFormula
formMap ((RawFormula, FormulaSpec)
-> Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
forall a b. b -> Either a b
Right (RawFormula
f, FormulaSpec
fSpec) Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
forall a. a -> [a] -> [a]
: [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest)
      collectMoreFormulae Map Text RawFormula
formMap (Right (RawFormula
f, FSubst Text
phi (Subst Text
x Text
t)) : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) =
        case Map Text RawFormula
formMap Map Text RawFormula
-> Key (Map Text RawFormula) -> Maybe (Val (Map Text RawFormula))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? Text
Key (Map Text RawFormula)
phi of
          -- unify fs
          Just Val (Map Text RawFormula)
phiF ->
            let x' :: Text
x' = case Map Text (Int, Term)
termMap Map Text (Int, Term)
-> Key (Map Text (Int, Term)) -> Maybe (Val (Map Text (Int, Term)))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? Text
Key (Map Text (Int, Term))
x of
                  Just (Int
_, Var Text
x') -> Text
x'
                  Maybe (Val (Map Text (Int, Term)))
_ -> Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x
             in case Text -> [(RawFormula, RawFormula)] -> Maybe (Map Text Term)
unifyFormulaeOnVariable Text
x' [(Val (Map Text RawFormula)
RawFormula
phiF, RawFormula
f)] of
                  Maybe (Map Text Term)
Nothing ->
                    Text
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> Text
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a b. (a -> b) -> a -> b
$
                      Text
"Error:\nunable to unify\n"
                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Val (Map Text RawFormula)
RawFormula
phiF
                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nwith\n"
                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
f
                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\non variable "
                        Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x'
                  -- compare assignment of E
                  Just Map Text Term
mgu -> case (Map Text Term
mgu Map Text Term -> Key (Map Text Term) -> Maybe (Val (Map Text Term))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? Text
Key (Map Text Term)
x', Map Text (Int, Term)
termMap Map Text (Int, Term)
-> Key (Map Text (Int, Term)) -> Maybe (Val (Map Text (Int, Term)))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? Text
Key (Map Text (Int, Term))
t) of
                    (Maybe Term, Maybe (Int, Term))
_
                      | Map Text Term -> Int
forall t. StaticMap t => t -> Int
size Map Text Term
mgu Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1 ->
                          Text
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> Text
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a b. (a -> b) -> a -> b
$
                            Text
"Error:\nunable to unify\n"
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Val (Map Text RawFormula)
RawFormula
phiF
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nwith\n"
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
f
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\non variable "
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x'
                    ((Maybe Term
Nothing, Maybe (Int, Term)
_); (Maybe Term
_, Maybe (Int, Term)
Nothing)) ->
                      (Val
   (Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
 -> Val
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
 -> Val
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> Key
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
forall t.
DynamicMap t =>
(Val t -> Val t -> Val t) -> Key t -> Val t -> t -> t
insertWith
                        NonEmpty
  (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
Val
  (Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a. Semigroup a => a -> a -> a
(<>)
                        Text
Key
  (Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
phi
                        (RawFormula
-> Either
     RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
forall a b. a -> Either a b
Left Val (Map Text RawFormula)
RawFormula
phiF Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
forall a. a -> [a] -> NonEmpty a
:| [])
                        (Map
   Text
   (NonEmpty
      (Either
         RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
 -> Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text RawFormula
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
collectMoreFormulae Map Text RawFormula
formMap [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
                    (Just Term
e, Just (Int
line', Term
e')) ->
                      if Term
e Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
e'
                        then
                          (Val
   (Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
 -> Val
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
 -> Val
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> Key
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
forall t.
DynamicMap t =>
(Val t -> Val t -> Val t) -> Key t -> Val t -> t -> t
insertWith NonEmpty
  (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
Val
  (Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a. Semigroup a => a -> a -> a
(<>) Text
Key
  (Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
phi (RawFormula
-> Either
     RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
forall a b. a -> Either a b
Left Val (Map Text RawFormula)
RawFormula
phiF Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
forall a. a -> [a] -> NonEmpty a
:| [])
                            (Map
   Text
   (NonEmpty
      (Either
         RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
 -> Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text RawFormula
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
collectMoreFormulae Map Text RawFormula
formMap [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
                        else
                          Text
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a b. a -> Either a b
Left (Text
 -> Either
      Text
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> Text
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a b. (a -> b) -> a -> b
$
                            Text
"Error:\nwhile unifying\n"
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Val (Map Text RawFormula)
RawFormula
phiF
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nwith\n"
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint RawFormula
f
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\non variable "
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x'
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nfound the assignment\n"
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x'
                              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
e
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
",\nbut in line "
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
line'
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nfound\n"
                              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x'
                              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
e'
          Maybe (Val (Map Text RawFormula))
Nothing -> case Map Text (Int, Term)
termMap Map Text (Int, Term)
-> Key (Map Text (Int, Term)) -> Maybe (Val (Map Text (Int, Term)))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? Text
Key (Map Text (Int, Term))
t of
            Maybe (Val (Map Text (Int, Term)))
Nothing -> Map Text RawFormula
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
collectMoreFormulae Map Text RawFormula
formMap [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
            -- backwards
            Just (Int
_, Term
t') ->
              let x' :: Text
x' = case Map Text (Int, Term)
termMap Map Text (Int, Term)
-> Key (Map Text (Int, Term)) -> Maybe (Val (Map Text (Int, Term)))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? Text
Key (Map Text (Int, Term))
x of
                    Just (Int
_, Var Text
x') -> Text
x'
                    Maybe (Val (Map Text (Int, Term)))
_ -> Text
"_" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
x
               in -- NOTE: we use ('_' <> x) because it can not clash with a var name.
                  case Subst Term -> RawFormula -> NonEmpty RawFormula
substBackwardsForm (Text -> Term -> Subst Term
forall a. Text -> a -> Subst a
Subst Text
x' Term
t') RawFormula
f of
                    RawFormula
f' :| [] ->
                      (Val
   (Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
 -> Val
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
 -> Val
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> Key
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
forall t.
DynamicMap t =>
(Val t -> Val t -> Val t) -> Key t -> Val t -> t -> t
insertWith
                        NonEmpty
  (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
Val
  (Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a. Semigroup a => a -> a -> a
(<>)
                        Text
Key
  (Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
phi
                        (RawFormula
-> Either
     RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
forall a b. a -> Either a b
Left RawFormula
f' Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
forall a. a -> [a] -> NonEmpty a
:| [])
                        (Map
   Text
   (NonEmpty
      (Either
         RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
 -> Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text RawFormula
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
collectMoreFormulae Map Text RawFormula
formMap [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
                    l :: NonEmpty RawFormula
l@(RawFormula
_ :| RawFormula
_ : [RawFormula]
_) ->
                      (Val
   (Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
 -> Val
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
 -> Val
      (Map
         Text
         (NonEmpty
            (Either
               RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))))
-> Key
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
-> Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
forall t.
DynamicMap t =>
(Val t -> Val t -> Val t) -> Key t -> Val t -> t -> t
insertWith
                        NonEmpty
  (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
Val
  (Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Val
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall a. Semigroup a => a -> a -> a
(<>)
                        Text
Key
  (Map
     Text
     (NonEmpty
        (Either
           RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
phi
                        (((RawFormula, Subst Term), NonEmpty RawFormula)
-> Either
     RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
forall a b. b -> Either a b
Right ((RawFormula
f, Text -> Term -> Subst Term
forall a. Text -> a -> Subst a
Subst Text
x' Term
t'), NonEmpty RawFormula
l) Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)
-> [Either
      RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)]
-> NonEmpty
     (Either RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))
forall a. a -> [a] -> NonEmpty a
:| [])
                        (Map
   Text
   (NonEmpty
      (Either
         RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula)))
 -> Map
      Text
      (NonEmpty
         (Either
            RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Map Text RawFormula
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
collectMoreFormulae Map Text RawFormula
formMap [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
      collectMoreFormulae Map Text RawFormula
formMap (Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)
_ : [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest) = Map Text RawFormula
-> [Either
      (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
-> Either
     Text
     (Map
        Text
        (NonEmpty
           (Either
              RawFormula ((RawFormula, Subst Term), NonEmpty RawFormula))))
collectMoreFormulae Map Text RawFormula
formMap [Either (RawAssumption, AssumptionSpec) (RawFormula, FormulaSpec)]
rest
      substBackwardsForm :: Subst Term -> RawFormula -> NonEmpty RawFormula
      substBackwardsForm :: Subst Term -> RawFormula -> NonEmpty RawFormula
substBackwardsForm Subst Term
s (InfixPred Text
p Term
t1 Term
t2) =
        ([Term] -> RawFormula) -> NonEmpty [Term] -> NonEmpty RawFormula
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\[Item [Term]
t1', Item [Term]
t2'] -> Text -> Term -> Term -> RawFormula
InfixPred Text
p Item [Term]
Term
t1' Item [Term]
Term
t2') (NonEmpty [Term] -> NonEmpty RawFormula)
-> ([NonEmpty Term] -> NonEmpty [Term])
-> [NonEmpty Term]
-> NonEmpty RawFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NonEmpty Term] -> NonEmpty [Term]
forall a. [NonEmpty a] -> NonEmpty [a]
allCombinations ([NonEmpty Term] -> NonEmpty RawFormula)
-> [NonEmpty Term] -> NonEmpty RawFormula
forall a b. (a -> b) -> a -> b
$
          (Term -> NonEmpty Term) -> [Term] -> [NonEmpty Term]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst Term -> Term -> NonEmpty Term
substBackwardsTerm Subst Term
s) [Item [Term]
Term
t1, Item [Term]
Term
t2]
      substBackwardsForm Subst Term
s (Pred Text
p [Term]
ts) =
        ([Term] -> RawFormula) -> NonEmpty [Term] -> NonEmpty RawFormula
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> [Term] -> RawFormula
Pred Text
p) (NonEmpty [Term] -> NonEmpty RawFormula)
-> ([NonEmpty Term] -> NonEmpty [Term])
-> [NonEmpty Term]
-> NonEmpty RawFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NonEmpty Term] -> NonEmpty [Term]
forall a. [NonEmpty a] -> NonEmpty [a]
allCombinations ([NonEmpty Term] -> NonEmpty RawFormula)
-> [NonEmpty Term] -> NonEmpty RawFormula
forall a b. (a -> b) -> a -> b
$ (Term -> NonEmpty Term) -> [Term] -> [NonEmpty Term]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst Term -> Term -> NonEmpty Term
substBackwardsTerm Subst Term
s) [Term]
ts
      substBackwardsForm Subst Term
s (Opr Text
o [RawFormula]
fs) =
        ([RawFormula] -> RawFormula)
-> NonEmpty [RawFormula] -> NonEmpty RawFormula
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> [RawFormula] -> RawFormula
Opr Text
o) (NonEmpty [RawFormula] -> NonEmpty RawFormula)
-> ([NonEmpty RawFormula] -> NonEmpty [RawFormula])
-> [NonEmpty RawFormula]
-> NonEmpty RawFormula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NonEmpty RawFormula] -> NonEmpty [RawFormula]
forall a. [NonEmpty a] -> NonEmpty [a]
allCombinations ([NonEmpty RawFormula] -> NonEmpty RawFormula)
-> [NonEmpty RawFormula] -> NonEmpty RawFormula
forall a b. (a -> b) -> a -> b
$ (RawFormula -> NonEmpty RawFormula)
-> [RawFormula] -> [NonEmpty RawFormula]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst Term -> RawFormula -> NonEmpty RawFormula
substBackwardsForm Subst Term
s) [RawFormula]
fs
      -- NOTE: @x == v@ is not possible, because we only backwardsubst if @E@
      -- is assigned and in this case there is no rule where @x@ is assigned.
      -- Thus @v@ here will be something like '_x' that does not occur naturally,
      -- i.e. not in Subst!
      substBackwardsForm s :: Subst Term
s@(Subst Text
x Term
t) (Quantifier Text
q Text
v RawFormula
f) =
        (RawFormula -> RawFormula)
-> NonEmpty RawFormula -> NonEmpty RawFormula
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> Text -> RawFormula -> RawFormula
Quantifier Text
q Text
v) (Subst Term -> RawFormula -> NonEmpty RawFormula
substBackwardsForm Subst Term
s RawFormula
f)
      substBackwardsTerm :: Subst Term -> Term -> NonEmpty Term
      substBackwardsTerm :: Subst Term -> Term -> NonEmpty Term
substBackwardsTerm s :: Subst Term
s@(Subst Text
n Term
e) Term
t | Term
t Term -> Term -> Bool
forall a. Eq a => a -> a -> Bool
== Term
e = [Text -> Term
Var Text
n, Item (NonEmpty Term)
Term
t]
      substBackwardsTerm Subst Term
s (Var Text
x) = OneItem (NonEmpty Term) -> NonEmpty Term
forall x. One x => OneItem x -> x
one (OneItem (NonEmpty Term) -> NonEmpty Term)
-> OneItem (NonEmpty Term) -> NonEmpty Term
forall a b. (a -> b) -> a -> b
$ Text -> Term
Var Text
x
      substBackwardsTerm Subst Term
s (Fun Text
f [Term]
ts) =
        ([Term] -> Term) -> NonEmpty [Term] -> NonEmpty Term
forall a b. (a -> b) -> NonEmpty a -> NonEmpty b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Text -> [Term] -> Term
Fun Text
f) (NonEmpty [Term] -> NonEmpty Term)
-> ([NonEmpty Term] -> NonEmpty [Term])
-> [NonEmpty Term]
-> NonEmpty Term
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NonEmpty Term] -> NonEmpty [Term]
forall a. [NonEmpty a] -> NonEmpty [a]
allCombinations ([NonEmpty Term] -> NonEmpty [Term])
-> ([NonEmpty Term] -> [NonEmpty Term])
-> [NonEmpty Term]
-> NonEmpty [Term]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [NonEmpty Term] -> [NonEmpty Term]
forall a. [a] -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList ([NonEmpty Term] -> NonEmpty Term)
-> [NonEmpty Term] -> NonEmpty Term
forall a b. (a -> b) -> a -> b
$ (Term -> NonEmpty Term) -> [Term] -> [NonEmpty Term]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Subst Term -> Term -> NonEmpty Term
substBackwardsTerm Subst Term
s) [Term]
ts
    ---------------------------------------------------

    -- helpers

    -- Checks if given reference is visible for the current rule.
    refIsVisible ::
      (Int, NodeAddr) -> Either (Int, NodeAddr) ((Int, Int), ProofAddr) -> Maybe Text
    refIsVisible :: (Int, NodeAddr)
-> Either (Int, NodeAddr) ((Int, Int), ProofAddr) -> Maybe Text
refIsVisible (Int
ruleLine, NodeAddr
ruleAddr) (Left (Int
refLine, NodeAddr
refAddr))
      | Int
ruleLine Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
refLine =
          Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$
            Text
"Error:\nline "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
refLine
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" can not be referenced,\nbecause it does not appear before line "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
ruleLine
    refIsVisible (Int
ruleLine, NodeAddr
ruleAddr) (Right ((Int
start, Int
end), ProofAddr
refAddr))
      | Int
ruleLine Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
start =
          Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$
            Text
"Error:\nline range "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> 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
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" can not be referenced,\nbecause it does not appear before line "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
ruleLine
    refIsVisible (Int
ruleLine, NAProof Int
n NodeAddr
na1) (Left (Int
line, NAProof Int
m NodeAddr
na2))
      | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m = (Int, NodeAddr)
-> Either (Int, NodeAddr) ((Int, Int), ProofAddr) -> Maybe Text
refIsVisible (Int
ruleLine, NodeAddr
na1) ((Int, NodeAddr) -> Either (Int, NodeAddr) ((Int, Int), ProofAddr)
forall a b. a -> Either a b
Left (Int
line, NodeAddr
na2))
    refIsVisible (Int
ruleLine, NAProof Int
n NodeAddr
na1) (Right ((Int
start, Int
end), PANested Int
m ProofAddr
pa2))
      | Int
n Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
m = (Int, NodeAddr)
-> Either (Int, NodeAddr) ((Int, Int), ProofAddr) -> Maybe Text
refIsVisible (Int
ruleLine, NodeAddr
na1) (((Int, Int), ProofAddr)
-> Either (Int, NodeAddr) ((Int, Int), ProofAddr)
forall a b. b -> Either a b
Right ((Int
start, Int
end), ProofAddr
pa2))
    refIsVisible (Int, NodeAddr)
_ (Left (Int
line, NAProof Int
_ NodeAddr
_)) =
      Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$
        Text
"Error:\nline "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
line
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" cannot be referenced,\nbecause it is located inside of a different subproof"
    refIsVisible
      (Int
ruleLine, NodeAddr
ruleAddr)
      (Right ((Int
start, Int
end), NodeAddr -> ProofAddr -> Bool
naContainedIn NodeAddr
ruleAddr -> Bool
True)) =
        Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$
          Text
"Error:\nline range "
            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> 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
            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" can not be referenced,\nbecause it contains line "
            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
ruleLine
    refIsVisible (Int, NodeAddr)
_ (Right ((Int
start, Int
end), PANested Int
_ PANested{})) =
      Text -> Maybe Text
forall a. a -> Maybe a
Just (Text -> Maybe Text) -> Text -> Maybe Text
forall a b. (a -> b) -> a -> b
$
        Text
"Error:\nline range "
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> 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
          Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" can not be referenced,\nbecause it is located inside of a different subproof"
    refIsVisible (Int, NodeAddr)
_ Either (Int, NodeAddr) ((Int, Int), ProofAddr)
_ = Maybe Text
forall a. Maybe a
Nothing

    -- tries to look up a 'ProofReference'
    lookupProofReference :: Int -> Int -> Proof -> Either Text Proof
    lookupProofReference :: Int -> Int -> Proof -> Either Text Proof
lookupProofReference Int
start Int
end Proof
p =
      case (Int -> Int -> Proof -> Maybe Proof
pIndexProof Int
start Int
end Proof
p, Int -> Int -> Proof -> Maybe ProofAddr
fromLineRange Int
start Int
end Proof
p, Int -> Proof -> Maybe NodeAddr
fromLineNo Int
ruleLine Proof
p) of
        (Maybe Proof
_, Maybe ProofAddr
_, Maybe NodeAddr
Nothing) ->
          Text -> Either Text Proof
forall a b. a -> Either a b
Left
            Text
"Internal error on lookupProofReference: should not happen!"
        ((Maybe Proof
Nothing, Maybe ProofAddr
_, Maybe NodeAddr
_); (Maybe Proof
_, Maybe ProofAddr
Nothing, Maybe NodeAddr
_)) ->
          Text -> Either Text Proof
forall a b. a -> Either a b
Left (Text -> Either Text Proof) -> Text -> Either Text Proof
forall a b. (a -> b) -> a -> b
$
            Text
"Error:\nline range "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> 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
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" does not correspond to a subproof.\nline "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> 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
" should mark the start of a subproof and line "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
end
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" should be its conclusion"
        (Just Proof
prf, Just ProofAddr
refAddr, Just NodeAddr
ruleAddr) -> case (Int, NodeAddr)
-> Either (Int, NodeAddr) ((Int, Int), ProofAddr) -> Maybe Text
refIsVisible
          (Int
ruleLine, NodeAddr
ruleAddr)
          (((Int, Int), ProofAddr)
-> Either (Int, NodeAddr) ((Int, Int), ProofAddr)
forall a b. b -> Either a b
Right ((Int
start, Int
end), ProofAddr
refAddr)) of
          Maybe Text
Nothing -> Proof -> Either Text Proof
forall a b. b -> Either a b
Right Proof
prf
          Just Text
err -> Text -> Either Text Proof
forall a b. a -> Either a b
Left Text
err

    -- tries to look up a 'LineReference'
    lookupLineReference :: Int -> Proof -> Either Text (Either Assumption Formula)
    lookupLineReference :: Int -> Proof -> Either Text (Either Assumption Formula)
lookupLineReference Int
refLine Proof
p =
      case (Int -> Proof -> Maybe (Either Assumption Derivation)
pIndex Int
refLine Proof
p, Int -> Proof -> Maybe NodeAddr
fromLineNo Int
refLine Proof
p, Int -> Proof -> Maybe NodeAddr
fromLineNo Int
ruleLine Proof
p) of
        (Maybe (Either Assumption Derivation)
_, Maybe NodeAddr
_, Maybe NodeAddr
Nothing) ->
          Text -> Either Text (Either Assumption Formula)
forall a b. a -> Either a b
Left
            Text
"Internal error on lookupLineReference: should not happen!"
        ((Maybe (Either Assumption Derivation)
Nothing, Maybe NodeAddr
_, Maybe NodeAddr
_); (Maybe (Either Assumption Derivation)
_, Maybe NodeAddr
Nothing, Maybe NodeAddr
_)) ->
          Text -> Either Text (Either Assumption Formula)
forall a b. a -> Either a b
Left (Text -> Either Text (Either Assumption Formula))
-> Text -> Either Text (Either Assumption Formula)
forall a b. (a -> b) -> a -> b
$
            Text
"Error:\ncan not reference line "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
refLine
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" because it does not exist"
        (Just (Left Assumption
a), Just NodeAddr
refAddr, Just NodeAddr
ruleAddr) ->
          Either Assumption Formula
-> Maybe Text -> Either Text (Either Assumption Formula)
forall r l. r -> Maybe l -> Either l r
maybeToLeft
            (Assumption -> Either Assumption Formula
forall a b. a -> Either a b
Left Assumption
a)
            ((Int, NodeAddr)
-> Either (Int, NodeAddr) ((Int, Int), ProofAddr) -> Maybe Text
refIsVisible (Int
ruleLine, NodeAddr
ruleAddr) ((Int, NodeAddr) -> Either (Int, NodeAddr) ((Int, Int), ProofAddr)
forall a b. a -> Either a b
Left (Int
refLine, NodeAddr
refAddr)))
        (Just (Right (Derivation Formula
f Wrapper RuleApplication
_)), Just NodeAddr
refAddr, Just NodeAddr
ruleAddr) ->
          Either Assumption Formula
-> Maybe Text -> Either Text (Either Assumption Formula)
forall r l. r -> Maybe l -> Either l r
maybeToLeft
            (Formula -> Either Assumption Formula
forall a b. b -> Either a b
Right Formula
f)
            ((Int, NodeAddr)
-> Either (Int, NodeAddr) ((Int, Int), ProofAddr) -> Maybe Text
refIsVisible (Int
ruleLine, NodeAddr
ruleAddr) ((Int, NodeAddr) -> Either (Int, NodeAddr) ((Int, Int), ProofAddr)
forall a b. a -> Either a b
Left (Int
refLine, NodeAddr
refAddr)))

-- * Semantic checking

{- | Validates every fresh-variable t'Assumption' @[c]@ in a t'Proof'.

For each such t'Assumption', it collects all lines that are in scope and
checks that @c@ does not appear free in any of their t'Formula'e.
-}
checkFreshness :: Proof -> Proof
checkFreshness :: Proof -> Proof
checkFreshness Proof
p = (NodeAddr -> Assumption -> Assumption)
-> (NodeAddr -> Derivation -> Derivation) -> Proof -> Proof
pMapLinesWithAddr (Proof -> NodeAddr -> Assumption -> Assumption
goAssumption Proof
p) ((Derivation -> Derivation) -> NodeAddr -> Derivation -> Derivation
forall a b. a -> b -> a
const Derivation -> Derivation
forall a. a -> a
id) Proof
p
 where
  goAssumption :: Proof -> NodeAddr -> Assumption -> Assumption
  goAssumption :: Proof -> NodeAddr -> Assumption -> Assumption
goAssumption Proof
_ NodeAddr
_ a :: Assumption
a@(Unparsed{}, Wrapper RuleApplication
_) = Assumption
a
  goAssumption Proof
p NodeAddr
na a :: Assumption
a@(ParsedInvalid Text
txt Text
_ RawAssumption
ra, Wrapper RuleApplication
r) = (Proof -> NodeAddr -> Text -> RawAssumption -> Wrapper RawAssumption
goRawAssumption Proof
p NodeAddr
na Text
txt RawAssumption
ra, Wrapper RuleApplication
r)
  goAssumption Proof
p NodeAddr
na a :: Assumption
a@(ParsedValid Text
txt RawAssumption
ra, Wrapper RuleApplication
r) = (Proof -> NodeAddr -> Text -> RawAssumption -> Wrapper RawAssumption
goRawAssumption Proof
p NodeAddr
na Text
txt RawAssumption
ra, Wrapper RuleApplication
r)
  goRawAssumption :: Proof -> NodeAddr -> Text -> RawAssumption -> Wrapper RawAssumption
  goRawAssumption :: Proof -> NodeAddr -> Text -> RawAssumption -> Wrapper RawAssumption
goRawAssumption Proof
p (Proof -> NodeAddr -> [(NodeAddr, Either Assumption Derivation)]
pCollectFreshnessNodes Proof
p -> [(NodeAddr, Either Assumption Derivation)]
nodes) Text
txt ra :: RawAssumption
ra@(FreshVar Text
v) =
    case Text
-> [(NodeAddr, Either Assumption Derivation)]
-> Maybe (NodeAddr, Either RawAssumption RawFormula)
isFreshList Text
v [(NodeAddr, Either Assumption Derivation)]
nodes of
      Maybe (NodeAddr, Either RawAssumption RawFormula)
Nothing -> Text -> RawAssumption -> Wrapper RawAssumption
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawAssumption
ra
      Just (NodeAddr
naf', Either RawAssumption RawFormula
f') ->
        Text -> Text -> RawAssumption -> Wrapper RawAssumption
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid
          Text
txt
          ( Text
"Error:\ncould not verify freshness of "
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
v
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"\nit appears in formula:\n"
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show (NodeAddr -> Proof -> Int
lineNoOr999 NodeAddr
naf' Proof
p)
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
"|"
              Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Either RawAssumption RawFormula -> Text
forall a. PrettyPrint a => a -> Text
prettyPrint Either RawAssumption RawFormula
f'
          )
          RawAssumption
ra
  goRawAssumption Proof
_ NodeAddr
_ Text
txt RawAssumption
ra = Text -> RawAssumption -> Wrapper RawAssumption
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawAssumption
ra
  isFreshList ::
    Name ->
    [(NodeAddr, Either Assumption Derivation)] ->
    Maybe (NodeAddr, Either RawAssumption RawFormula)
  isFreshList :: Text
-> [(NodeAddr, Either Assumption Derivation)]
-> Maybe (NodeAddr, Either RawAssumption RawFormula)
isFreshList Text
v [] = Maybe (NodeAddr, Either RawAssumption RawFormula)
forall a. Maybe a
Nothing
  isFreshList Text
v ((NodeAddr
na, Left (Wrapper RawAssumption -> Maybe RawAssumption
forall a. Wrapper a -> Maybe a
fromWrapper -> Maybe RawAssumption
Nothing, Wrapper RuleApplication
_)) : [(NodeAddr, Either Assumption Derivation)]
rest) =
    Text
-> [(NodeAddr, Either Assumption Derivation)]
-> Maybe (NodeAddr, Either RawAssumption RawFormula)
isFreshList Text
v [(NodeAddr, Either Assumption Derivation)]
rest
  isFreshList Text
v ((NodeAddr
na, Left (Wrapper RawAssumption -> Maybe RawAssumption
forall a. Wrapper a -> Maybe a
fromWrapper -> Just RawAssumption
a, Wrapper RuleApplication
_)) : [(NodeAddr, Either Assumption Derivation)]
rest) =
    if Text -> RawAssumption -> Bool
forall a. AllVars a => Text -> a -> Bool
isFresh Text
v RawAssumption
a then Text
-> [(NodeAddr, Either Assumption Derivation)]
-> Maybe (NodeAddr, Either RawAssumption RawFormula)
isFreshList Text
v [(NodeAddr, Either Assumption Derivation)]
rest else (NodeAddr, Either RawAssumption RawFormula)
-> Maybe (NodeAddr, Either RawAssumption RawFormula)
forall a. a -> Maybe a
Just (NodeAddr
na, RawAssumption -> Either RawAssumption RawFormula
forall a b. a -> Either a b
Left RawAssumption
a)
  isFreshList Text
v ((NodeAddr
na, Right (Derivation (Formula -> Maybe RawFormula
forall a. Wrapper a -> Maybe a
fromWrapper -> Maybe RawFormula
Nothing) Wrapper RuleApplication
_)) : [(NodeAddr, Either Assumption Derivation)]
rest) =
    Text
-> [(NodeAddr, Either Assumption Derivation)]
-> Maybe (NodeAddr, Either RawAssumption RawFormula)
isFreshList Text
v [(NodeAddr, Either Assumption Derivation)]
rest
  isFreshList Text
v ((NodeAddr
na, Right (Derivation (Formula -> Maybe RawFormula
forall a. Wrapper a -> Maybe a
fromWrapper -> Just RawFormula
f) Wrapper RuleApplication
_)) : [(NodeAddr, Either Assumption Derivation)]
rest) =
    if Text -> RawFormula -> Bool
forall a. AllVars a => Text -> a -> Bool
isFresh Text
v RawFormula
f then Text
-> [(NodeAddr, Either Assumption Derivation)]
-> Maybe (NodeAddr, Either RawAssumption RawFormula)
isFreshList Text
v [(NodeAddr, Either Assumption Derivation)]
rest else (NodeAddr, Either RawAssumption RawFormula)
-> Maybe (NodeAddr, Either RawAssumption RawFormula)
forall a. a -> Maybe a
Just (NodeAddr
na, RawFormula -> Either RawAssumption RawFormula
forall a b. b -> Either a b
Right RawFormula
f)

{- | State used in 'regenerateSymbols',
contains list of functionSymbols and predicateSymbols
-}
type RegenState = (Int, Map Text (Int, Pos), Map Text (Int, Pos))

{- | Recalculates the list of functionsymbols and predicatesymbols in the model.

This is done by iterating over the proof and collecting all symbols.
The first occurence of a symbol fixes its arity, and all following symbols with the
same t'Name' are compared to this arity.
-}
regenerateSymbols :: Proof -> (Map Text (Int, Pos), Map Text (Int, Pos), Proof)
regenerateSymbols :: Proof -> (Map Text (Int, Int), Map Text (Int, Int), Proof)
regenerateSymbols Proof
p =
  let
    ((Int
_, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs), Proof
p') = (RegenState -> Assumption -> (RegenState, Assumption))
-> (RegenState -> Derivation -> (RegenState, Derivation))
-> RegenState
-> Proof
-> (RegenState, Proof)
forall s.
(s -> Assumption -> (s, Assumption))
-> (s -> Derivation -> (s, Derivation)) -> s -> Proof -> (s, Proof)
pMapLinesAccumL RegenState -> Assumption -> (RegenState, Assumption)
goAssumption RegenState -> Derivation -> (RegenState, Derivation)
goLine (Int
1, Map Text (Int, Int)
forall a. Monoid a => a
mempty, Map Text (Int, Int)
forall a. Monoid a => a
mempty) Proof
p
   in
    (Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs, Proof
p')
 where
  goAssumption :: RegenState -> Assumption -> (RegenState, Assumption)
  goAssumption :: RegenState -> Assumption -> (RegenState, Assumption)
goAssumption (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) a :: Assumption
a@(Unparsed{}, Wrapper RuleApplication
_) =
    ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs), Assumption
a)
  goAssumption (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) a :: Assumption
a@(ParsedInvalid Text
txt Text
err (RawAssumption RawFormula
f), Wrapper RuleApplication
r) =
    let ((Int
n', Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs'), Formula
f') =
          RegenState -> Formula -> (RegenState, Formula)
goFormula (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) (Text -> Text -> RawFormula -> Formula
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
err RawFormula
f)
     in ((Int
n', Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs'), (RawFormula -> RawAssumption
RawAssumption (RawFormula -> RawAssumption) -> Formula -> Wrapper RawAssumption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula
f', Wrapper RuleApplication
r))
  goAssumption (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) a :: Assumption
a@(ParsedValid Text
txt (RawAssumption RawFormula
f), Wrapper RuleApplication
r) =
    let ((Int
n', Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs'), Formula
f') = RegenState -> Formula -> (RegenState, Formula)
goFormula (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) (Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawFormula
f)
     in ((Int
n', Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs'), (RawFormula -> RawAssumption
RawAssumption (RawFormula -> RawAssumption) -> Formula -> Wrapper RawAssumption
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Formula
f', Wrapper RuleApplication
r))
  goAssumption (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) a :: Assumption
a@(ParsedInvalid Text
_ Text
_ (FreshVar{}), Wrapper RuleApplication
_) =
    ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs), Assumption
a)
  goAssumption (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) a :: Assumption
a@(ParsedValid Text
_ (FreshVar{}), Wrapper RuleApplication
_) =
    ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs), Assumption
a)

  -- collect symbols inside a formula
  goFormula :: RegenState -> Formula -> (RegenState, Formula)
  -- skip unparsed formulae
  goFormula :: RegenState -> Formula -> (RegenState, Formula)
goFormula (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) a :: Formula
a@(Unparsed{}) = ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs), Formula
a)
  goFormula (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) Formula
a =
    let
      (RawFormula
formula, Text
txt) = case Formula
a of
        (ParsedInvalid Text
txt Text
_ RawFormula
f) -> (RawFormula
f, Text
txt)
        (ParsedValid Text
txt RawFormula
f) -> (RawFormula
f, Text
txt)
      (Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs', Formula
a') = Int
-> Map Text (Int, Int)
-> Map Text (Int, Int)
-> Text
-> RawFormula
-> (Map Text (Int, Int), Map Text (Int, Int), Formula)
go Int
n Map Text (Int, Int)
fsymbs Map Text (Int, Int)
psymbs Text
txt RawFormula
formula
     in
      ((Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs'), Formula
a')
   where
    goArgs :: Int -> Map Text (Int, Pos) -> [Term] -> Either Text (Map Text (Int, Pos))
    goArgs :: Int
-> Map Text (Int, Int)
-> [Term]
-> Either Text (Map Text (Int, Int))
goArgs Int
n = (Map Text (Int, Int) -> Term -> Either Text (Map Text (Int, Int)))
-> Map Text (Int, Int)
-> [Term]
-> Either Text (Map Text (Int, Int))
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM (Int
-> Map Text (Int, Int) -> Term -> Either Text (Map Text (Int, Int))
goTerm Int
n)
     where
      goTerm :: Int -> Map Text (Int, Pos) -> Term -> Either Text (Map Text (Int, Pos))
      goTerm :: Int
-> Map Text (Int, Int) -> Term -> Either Text (Map Text (Int, Int))
goTerm Int
_ Map Text (Int, Int)
fsymbs (Var{}) = Map Text (Int, Int) -> Either Text (Map Text (Int, Int))
forall a b. b -> Either a b
Right Map Text (Int, Int)
fsymbs
      goTerm Int
n Map Text (Int, Int)
fsymbs (Fun Text
name [Term]
args) = do
        -- first check inner symbols
        fsymbs' <- Int
-> Map Text (Int, Int)
-> [Term]
-> Either Text (Map Text (Int, Int))
goArgs Int
n Map Text (Int, Int)
fsymbs [Term]
args
        -- then check the function symbol
        case fsymbs' !? name of
          Maybe (Val (Map Text (Int, Int)))
Nothing -> Map Text (Int, Int) -> Either Text (Map Text (Int, Int))
forall a b. b -> Either a b
Right (Map Text (Int, Int) -> Either Text (Map Text (Int, Int)))
-> Map Text (Int, Int) -> Either Text (Map Text (Int, Int))
forall a b. (a -> b) -> a -> b
$ Key (Map Text (Int, Int))
-> Val (Map Text (Int, Int))
-> Map Text (Int, Int)
-> Map Text (Int, Int)
forall t. DynamicMap t => Key t -> Val t -> t -> t
insert Text
Key (Map Text (Int, Int))
name ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args, Int
n) Map Text (Int, Int)
fsymbs'
          Just (Int
expLen, Int
pos) ->
            if Int
expLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args
              then Map Text (Int, Int) -> Either Text (Map Text (Int, Int))
forall a b. b -> Either a b
Right Map Text (Int, Int)
fsymbs'
              else
                Text -> Either Text (Map Text (Int, Int))
forall a b. a -> Either a b
Left (Text -> Either Text (Map Text (Int, Int)))
-> Text -> Either Text (Map Text (Int, Int))
forall a b. (a -> b) -> a -> b
$
                  Text
"Error:\nfunction symbol "
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text -> Text
forall b a. (Show a, IsString b) => a -> b
show Text
name
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" has "
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args)
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" argument"
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (if [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then Text
"" else Text
"s")
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
",\nbut in line "
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
pos
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" it appears with "
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
expLen
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" argument"
                    Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (if Int
expLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then Text
"" else Text
"s")
    -- proccesses a single formula.
    go ::
      Int ->
      Map Text (Int, Pos) ->
      Map Text (Int, Pos) ->
      Text ->
      RawFormula ->
      (Map Text (Int, Pos), Map Text (Int, Pos), Formula)
    go :: Int
-> Map Text (Int, Int)
-> Map Text (Int, Int)
-> Text
-> RawFormula
-> (Map Text (Int, Int), Map Text (Int, Int), Formula)
go Int
n Map Text (Int, Int)
fsymbs Map Text (Int, Int)
psymbs Text
txt formula :: RawFormula
formula@(InfixPred Text
name Term
a1 Term
a2) =
      let
        -- first check function symbols
        mTermError :: Either Text (Map Text (Int, Int))
mTermError = Int
-> Map Text (Int, Int)
-> [Term]
-> Either Text (Map Text (Int, Int))
goArgs Int
n Map Text (Int, Int)
fsymbs [Item [Term]
Term
a1, Item [Term]
Term
a2]
       in
        case Either Text (Map Text (Int, Int))
mTermError of
          Left Text
termError -> (Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs, Text -> Text -> RawFormula -> Formula
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
termError RawFormula
formula)
          Right Map Text (Int, Int)
fsymbs' -> (Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs, Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawFormula
formula)
    go Int
n Map Text (Int, Int)
fsymbs Map Text (Int, Int)
psymbs Text
txt formula :: RawFormula
formula@(Pred Text
name [Term]
args) =
      let
        -- first check function symbols
        mTermError :: Either Text (Map Text (Int, Int))
mTermError = Int
-> Map Text (Int, Int)
-> [Term]
-> Either Text (Map Text (Int, Int))
goArgs Int
n Map Text (Int, Int)
fsymbs [Term]
args
       in
        case Either Text (Map Text (Int, Int))
mTermError of
          Left Text
termError -> (Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs, Text -> Text -> RawFormula -> Formula
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
termError RawFormula
formula)
          -- then check the predicate symbol
          Right Map Text (Int, Int)
fsymbs' ->
            case Map Text (Int, Int)
psymbs Map Text (Int, Int)
-> Key (Map Text (Int, Int)) -> Maybe (Val (Map Text (Int, Int)))
forall t. StaticMap t => t -> Key t -> Maybe (Val t)
!? Text
Key (Map Text (Int, Int))
name of
              Maybe (Val (Map Text (Int, Int)))
Nothing ->
                let
                  psymbs' :: Map Text (Int, Int)
psymbs' = Key (Map Text (Int, Int))
-> Val (Map Text (Int, Int))
-> Map Text (Int, Int)
-> Map Text (Int, Int)
forall t. DynamicMap t => Key t -> Val t -> t -> t
insert Text
Key (Map Text (Int, Int))
name ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args, Int
n) Map Text (Int, Int)
psymbs
                 in
                  (Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs', Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawFormula
formula)
              Just (Int
expLen, Int
pos) ->
                if Int
expLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args
                  then (Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs, Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawFormula
formula)
                  else
                    ( Map Text (Int, Int)
fsymbs'
                    , Map Text (Int, Int)
psymbs
                    , Text -> Text -> RawFormula -> Formula
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid
                        Text
txt
                        ( Text
"Error:\npredicate symbol "
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
name
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" has "
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show ([Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args)
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" argument"
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (if [Term] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Term]
args Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then Text
"" else Text
"s")
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
",\nbut in line "
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
pos
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" it appears with "
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Int -> Text
forall b a. (Show a, IsString b) => a -> b
show Int
expLen
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" argument"
                            Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> (if Int
expLen Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 then Text
"" else Text
"s")
                        )
                        RawFormula
formula
                    )
    go Int
n Map Text (Int, Int)
fsymbs Map Text (Int, Int)
psymbs Text
txt form :: RawFormula
form@(Opr Text
name [RawFormula]
fs) =
      (Formula
 -> RawFormula
 -> (Map Text (Int, Int), Map Text (Int, Int), Formula))
-> Formula
-> [RawFormula]
-> (Map Text (Int, Int), Map Text (Int, Int), Formula)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldlM
        (\Formula
r RawFormula
f -> Int
-> Map Text (Int, Int)
-> Map Text (Int, Int)
-> Text
-> RawFormula
-> (Map Text (Int, Int), Map Text (Int, Int), Formula)
go Int
n Map Text (Int, Int)
fsymbs Map Text (Int, Int)
psymbs Text
txt RawFormula
f (Map Text (Int, Int), Map Text (Int, Int), Formula)
-> (Formula -> Formula)
-> (Map Text (Int, Int), Map Text (Int, Int), Formula)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> Formula -> Formula -> Formula
combineWrappers Formula
r)
        (Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawFormula
form)
        [RawFormula]
fs
     where
      combineWrappers :: Wrapper RawFormula -> Wrapper RawFormula -> Wrapper RawFormula
      combineWrappers :: Formula -> Formula -> Formula
combineWrappers (Unparsed Text
_ Text
err) Formula
_ =
        Text -> Text -> Formula
forall a. Text -> Text -> Wrapper a
Unparsed Text
txt Text
err
      combineWrappers (ParsedInvalid{}) (Unparsed Text
_ Text
err) =
        Text -> Text -> Formula
forall a. Text -> Text -> Wrapper a
Unparsed Text
txt Text
err
      combineWrappers (ParsedInvalid Text
_ Text
err RawFormula
_) (ParsedInvalid{}) =
        Text -> Text -> RawFormula -> Formula
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
err RawFormula
form
      combineWrappers (ParsedInvalid Text
_ Text
err RawFormula
_) (ParsedValid{}) =
        Text -> Text -> RawFormula -> Formula
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
err RawFormula
form
      combineWrappers (ParsedValid{}) (Unparsed Text
_ Text
err) =
        Text -> Text -> Formula
forall a. Text -> Text -> Wrapper a
Unparsed Text
txt Text
err
      combineWrappers (ParsedValid{}) (ParsedInvalid Text
_ Text
err RawFormula
_) =
        Text -> Text -> RawFormula -> Formula
forall a. Text -> Text -> a -> Wrapper a
ParsedInvalid Text
txt Text
err RawFormula
form
      combineWrappers (ParsedValid{}) (ParsedValid{}) =
        Text -> RawFormula -> Formula
forall a. Text -> a -> Wrapper a
ParsedValid Text
txt RawFormula
form
    go Int
n Map Text (Int, Int)
fsymbs Map Text (Int, Int)
psymbs Text
txt (Quantifier Text
name Text
variable RawFormula
formula) =
      Int
-> Map Text (Int, Int)
-> Map Text (Int, Int)
-> Text
-> RawFormula
-> (Map Text (Int, Int), Map Text (Int, Int), Formula)
go Int
n Map Text (Int, Int)
fsymbs Map Text (Int, Int)
psymbs Text
txt RawFormula
formula (Map Text (Int, Int), Map Text (Int, Int), Formula)
-> (Formula -> Formula)
-> (Map Text (Int, Int), Map Text (Int, Int), Formula)
forall (f :: * -> *) a b. Functor f => f a -> (a -> b) -> f b
<&> (Text -> Text -> RawFormula -> RawFormula
Quantifier Text
name Text
variable (RawFormula -> RawFormula) -> Formula -> Formula
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>)
  -- proccesses a single line, by proccessing its formula.
  goLine :: RegenState -> Derivation -> (RegenState, Derivation)
  goLine :: RegenState -> Derivation -> (RegenState, Derivation)
goLine (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) (Derivation Formula
f Wrapper RuleApplication
r) =
    let
      ((Int
n', Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs'), Formula
f') = RegenState -> Formula -> (RegenState, Formula)
goFormula (Int
n, Map Text (Int, Int)
fsymbs, Map Text (Int, Int)
psymbs) Formula
f
     in
      ((Int
n', Map Text (Int, Int)
fsymbs', Map Text (Int, Int)
psymbs'), Formula -> Wrapper RuleApplication -> Derivation
Derivation Formula
f' Wrapper RuleApplication
r)