{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE RecordWildCards #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleContexts #-}

module Persistence.Reasoning.PremiseSelectionSInE ( G_SInEResult (..)
                                                  , SInEParameters (..)
                                                  , perform
                                                  , saveToDatabase
                                                  ) where

import PGIP.ReasoningParameters as ReasoningParameters

import Persistence.Database
import Persistence.Schema as DatabaseSchema
import Persistence.Utils

import Common.AS_Annotation
import Common.ExtSign
import qualified Common.OrderedMap as OMap
import Common.Timing (measureWallTime, timeOfDayToSeconds)
import Driver.Options
import Logic.Coerce
import Logic.Logic as Logic
import Logic.Prover (toNamed)
import Static.GTheory

import Control.Monad.IO.Class (MonadIO (..))
import qualified Control.Monad.Fail as Fail
import Data.List as List hiding (insert)
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Maybe
import Data.Set (Set)
import qualified Data.Set as Set
import Data.Typeable
import Database.Persist hiding ((==.))
import Database.Esqueleto hiding (insertBy)

data G_SInEResult =
  forall lid sublogics
    basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree .
  Logic.Logic lid sublogics
    basic_spec sentence symb_items symb_map_items
    sign morphism symbol raw_symbol proof_tree =>
  G_SInEResult { ()
gSineLogic :: lid
               , G_SInEResult -> SInEParameters
parameters :: SInEParameters
               , ()
symbolCommonnesses :: Map symbol Int
               , ()
premiseTriggers :: Map symbol [(Double, Named sentence)] -- this list is ordered by the Double
               , ()
leastCommonSymbols :: Map (Named sentence) (symbol, Int)
               , ()
selectedPremises :: Set (Named sentence)
               , G_SInEResult -> Set String
selectedPremiseNames :: Set String
               } deriving Typeable

data SInEParameters = SInEParameters { SInEParameters -> Maybe Int
depthLimit :: Maybe Int
                                     , SInEParameters -> Maybe Double
tolerance :: Maybe Double
                                     , SInEParameters -> Maybe Int
premiseNumberLimit :: Maybe Int
                                     } deriving Typeable

perform :: HetcatsOpts
        -> G_theory
        -> ReasoningParameters.PremiseSelection
        -> String
        -> IO (Maybe [String], Int, G_SInEResult)
perform :: HetcatsOpts
-> G_theory
-> PremiseSelection
-> String
-> IO (Maybe [String], Int, G_SInEResult)
perform opts :: HetcatsOpts
opts gTheory :: G_theory
gTheory@G_theory{gTheoryLogic :: ()
gTheoryLogic = lid
gTheoryLid, gTheorySign :: ()
gTheorySign = ExtSign sign symbol
extSign}
  premiseSelectionParameters :: PremiseSelection
premiseSelectionParameters goalName :: String
goalName = do
  let parameters_ :: SInEParameters
parameters_ = SInEParameters :: Maybe Int -> Maybe Double -> Maybe Int -> SInEParameters
SInEParameters
        { depthLimit :: Maybe Int
depthLimit = PremiseSelection -> Maybe Int
ReasoningParameters.sineDepthLimit PremiseSelection
premiseSelectionParameters
        , tolerance :: Maybe Double
tolerance = PremiseSelection -> Maybe Double
ReasoningParameters.sineTolerance PremiseSelection
premiseSelectionParameters
        , premiseNumberLimit :: Maybe Int
premiseNumberLimit = PremiseSelection -> Maybe Int
ReasoningParameters.sinePremiseNumberLimit PremiseSelection
premiseSelectionParameters
        }
  let sineResult0 :: G_SInEResult
sineResult0 = G_SInEResult :: forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
G_SInEResult
        { gSineLogic :: lid
gSineLogic = lid
gTheoryLid
        , parameters :: SInEParameters
parameters = SInEParameters
parameters_
        , symbolCommonnesses :: Map symbol Int
symbolCommonnesses = Map symbol Int
forall k a. Map k a
Map.empty
        , premiseTriggers :: Map symbol [(Double, Named sentence)]
premiseTriggers = Map symbol [(Double, Named sentence)]
forall k a. Map k a
Map.empty
        , leastCommonSymbols :: Map (Named sentence) (symbol, Int)
leastCommonSymbols = Map (Named sentence) (symbol, Int)
forall k a. Map k a
Map.empty
        , selectedPremises :: Set (Named sentence)
selectedPremises = Set (Named sentence)
forall a. Set a
Set.empty
        , selectedPremiseNames :: Set String
selectedPremiseNames = Set String
forall a. Set a
Set.empty
        }
  ((premisesM :: Maybe [String]
premisesM, sineResult :: G_SInEResult
sineResult), wallTimeOfDay :: TimeOfDay
wallTimeOfDay) <- IO (Maybe [String], G_SInEResult)
-> IO ((Maybe [String], G_SInEResult), TimeOfDay)
forall a. IO a -> IO (a, TimeOfDay)
measureWallTime (IO (Maybe [String], G_SInEResult)
 -> IO ((Maybe [String], G_SInEResult), TimeOfDay))
-> IO (Maybe [String], G_SInEResult)
-> IO ((Maybe [String], G_SInEResult), TimeOfDay)
forall a b. (a -> b) -> a -> b
$ do
    let (sineResult1 :: G_SInEResult
sineResult1, goal :: Named sentence
goal) =
          lid
-> G_theory
-> G_SInEResult
-> String
-> (G_SInEResult, Named sentence)
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> G_theory
-> G_SInEResult
-> String
-> (G_SInEResult, Named sentence)
preprocess lid
gTheoryLid G_theory
gTheory G_SInEResult
sineResult0 String
goalName
    let sineResult2 :: G_SInEResult
sineResult2 = HetcatsOpts
-> lid
-> ExtSign sign symbol
-> G_SInEResult
-> Named sentence
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
HetcatsOpts
-> lid
-> ExtSign sign symbol
-> G_SInEResult
-> Named sentence
-> G_SInEResult
selectPremises HetcatsOpts
opts lid
gTheoryLid ExtSign sign symbol
extSign G_SInEResult
sineResult1 Named sentence
goal
    let premisesM :: Maybe [String]
premisesM = case G_SInEResult
sineResult2 of
          G_SInEResult { selectedPremises :: ()
selectedPremises = Set (Named sentence)
premises } ->
            [String] -> Maybe [String]
forall a. a -> Maybe a
Just ([String] -> Maybe [String]) -> [String] -> Maybe [String]
forall a b. (a -> b) -> a -> b
$ Set String -> [String]
forall a. Set a -> [a]
Set.toList (Set String -> [String]) -> Set String -> [String]
forall a b. (a -> b) -> a -> b
$ (Named sentence -> String) -> Set (Named sentence) -> Set String
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Named sentence -> String
forall s a. SenAttr s a -> a
senAttr Set (Named sentence)
premises
    (Maybe [String], G_SInEResult) -> IO (Maybe [String], G_SInEResult)
forall (m :: * -> *) a. Monad m => a -> m a
return (Maybe [String]
premisesM, G_SInEResult
sineResult2)
  (Maybe [String], Int, G_SInEResult)
-> IO (Maybe [String], Int, G_SInEResult)
forall (m :: * -> *) a. Monad m => a -> m a
return ( Maybe [String]
premisesM
         , TimeOfDay -> Int
timeOfDayToSeconds TimeOfDay
wallTimeOfDay
         , G_SInEResult
sineResult
         )

preprocess :: Logic.Logic lid sublogics basic_spec sentence symb_items
              symb_map_items sign morphism symbol
              raw_symbol proof_tree
           => lid
           -> G_theory
           -> G_SInEResult
           -> String
           -> (G_SInEResult, Named sentence)
preprocess :: lid
-> G_theory
-> G_SInEResult
-> String
-> (G_SInEResult, Named sentence)
preprocess sentenceLid :: lid
sentenceLid
  G_theory{ gTheoryLogic :: ()
gTheoryLogic = lid
gTheoryLid, gTheorySens :: ()
gTheorySens = ThSens sentence (AnyComorphism, BasicProof)
sentences, gTheorySign :: ()
gTheorySign = ExtSign sign symbol
sign }
  sineResult0 :: G_SInEResult
sineResult0 goalName :: String
goalName =
  let namedSentences :: [Named sentence]
namedSentences = ((String, SenStatus sentence (AnyComorphism, BasicProof))
 -> Named sentence)
-> [(String, SenStatus sentence (AnyComorphism, BasicProof))]
-> [Named sentence]
forall a b. (a -> b) -> [a] -> [b]
map ((String
 -> SenStatus sentence (AnyComorphism, BasicProof)
 -> Named sentence)
-> (String, SenStatus sentence (AnyComorphism, BasicProof))
-> Named sentence
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String
-> SenStatus sentence (AnyComorphism, BasicProof) -> Named sentence
forall a b. String -> SenStatus a b -> Named a
toNamed) ([(String, SenStatus sentence (AnyComorphism, BasicProof))]
 -> [Named sentence])
-> [(String, SenStatus sentence (AnyComorphism, BasicProof))]
-> [Named sentence]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> [(String, SenStatus sentence (AnyComorphism, BasicProof))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens sentence (AnyComorphism, BasicProof)
sentences
      goal' :: Named sentence
goal' = Maybe (Named sentence) -> Named sentence
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (Named sentence) -> Named sentence)
-> Maybe (Named sentence) -> Named sentence
forall a b. (a -> b) -> a -> b
$ (Named sentence -> Bool)
-> [Named sentence] -> Maybe (Named sentence)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find ((String
goalName String -> String -> Bool
forall a. Eq a => a -> a -> Bool
==) (String -> Bool)
-> (Named sentence -> String) -> Named sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named sentence -> String
forall s a. SenAttr s a -> a
senAttr) [Named sentence]
namedSentences
      goal :: Named sentence
goal = String -> lid -> lid -> Named sentence -> Named sentence
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String -> lid1 -> lid2 -> Named sentence1 -> Named sentence2
coerceSen "preprocess" lid
gTheoryLid lid
sentenceLid Named sentence
goal'
      sineResult1 :: G_SInEResult
sineResult1 = lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
computeSymbolCommonnesses lid
gTheoryLid ExtSign sign symbol
sign G_SInEResult
sineResult0 [Named sentence]
namedSentences
      sineResult2 :: G_SInEResult
sineResult2 = lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
computeLeastCommonSymbols lid
gTheoryLid ExtSign sign symbol
sign G_SInEResult
sineResult1 [Named sentence]
namedSentences
      sineResult3 :: G_SInEResult
sineResult3 = lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
computePremiseTriggers lid
gTheoryLid ExtSign sign symbol
sign G_SInEResult
sineResult2 [Named sentence]
namedSentences
  in  (G_SInEResult
sineResult3, Named sentence
goal)

computeSymbolCommonnesses :: Logic.Logic lid sublogics basic_spec sentence
                                         symb_items symb_map_items sign
                                         morphism symbol raw_symbol proof_tree
                          => lid
                          -> ExtSign sign symbol
                          -> G_SInEResult
                          -> [Named sentence]
                          -> G_SInEResult
computeSymbolCommonnesses :: lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
computeSymbolCommonnesses gTheoryLid :: lid
gTheoryLid ExtSign{plainSign :: forall sign symbol. ExtSign sign symbol -> sign
plainSign = sign
sign}
  sineResult0 :: G_SInEResult
sineResult0@G_SInEResult{..} namedSentences :: [Named sentence]
namedSentences =
    let result :: Map symbol Int
result =
          (Named sentence -> Map symbol Int -> Map symbol Int)
-> Map symbol Int -> [Named sentence] -> Map symbol Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ namedSentence :: Named sentence
namedSentence symbolCommonnessesAcc :: Map symbol Int
symbolCommonnessesAcc ->
                  (symbol -> Map symbol Int -> Map symbol Int)
-> Map symbol Int -> [symbol] -> Map symbol Int
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ symbol :: symbol
symbol symbolCommonnessesAcc' :: Map symbol Int
symbolCommonnessesAcc' ->
                          (Int -> Int -> Int)
-> symbol -> Int -> Map symbol Int -> Map symbol Int
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith Int -> Int -> Int
forall a. Num a => a -> a -> a
(+) symbol
symbol 1 Map symbol Int
symbolCommonnessesAcc'
                        )
                        Map symbol Int
symbolCommonnessesAcc ([symbol] -> Map symbol Int) -> [symbol] -> Map symbol Int
forall a b. (a -> b) -> a -> b
$
                        [symbol] -> [symbol]
forall a. Eq a => [a] -> [a]
nub ([symbol] -> [symbol]) -> [symbol] -> [symbol]
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sentence -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> [symbol]
symsOfSen lid
gTheoryLid sign
sign (sentence -> [symbol]) -> sentence -> [symbol]
forall a b. (a -> b) -> a -> b
$ Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
namedSentence
                )
                (String -> lid -> lid -> Map symbol Int -> Map symbol Int
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String -> lid1 -> lid2 -> Map symbol1 Int -> Map symbol2 Int
coerceSymbolCommonnesses "computeSymbolCommonnesses 1" lid
gSineLogic lid
gTheoryLid Map symbol Int
symbolCommonnesses)
                [Named sentence]
namedSentences
    in  lid -> Map symbol Int -> G_SInEResult -> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Map symbol Int -> G_SInEResult -> G_SInEResult
withSymbolCommonnesses lid
gTheoryLid Map symbol Int
result G_SInEResult
sineResult0
  where
    withSymbolCommonnesses :: Logic.Logic lid sublogics basic_spec sentence
                                          symb_items symb_map_items sign
                                          morphism symbol raw_symbol proof_tree
                           => lid
                           -> Map symbol Int
                           -> G_SInEResult
                           -> G_SInEResult
    withSymbolCommonnesses :: lid -> Map symbol Int -> G_SInEResult -> G_SInEResult
withSymbolCommonnesses lid :: lid
lid symbolCommonnesses' :: Map symbol Int
symbolCommonnesses' _ =
      lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
G_SInEResult lid
gSineLogic SInEParameters
parameters
        (String -> lid -> lid -> Map symbol Int -> Map symbol Int
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String -> lid1 -> lid2 -> Map symbol1 Int -> Map symbol2 Int
coerceSymbolCommonnesses "withSymbolCommonnesses" lid
lid lid
gSineLogic Map symbol Int
symbolCommonnesses')
        Map symbol [(Double, Named sentence)]
premiseTriggers Map (Named sentence) (symbol, Int)
leastCommonSymbols Set (Named sentence)
selectedPremises Set String
selectedPremiseNames

computeLeastCommonSymbols :: Logic.Logic lid sublogics basic_spec sentence
                                         symb_items symb_map_items sign
                                         morphism symbol raw_symbol proof_tree
                          => lid
                          -> ExtSign sign symbol
                          -> G_SInEResult
                          -> [Named sentence]
                          -> G_SInEResult
computeLeastCommonSymbols :: lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
computeLeastCommonSymbols gTheoryLid :: lid
gTheoryLid ExtSign{plainSign :: forall sign symbol. ExtSign sign symbol -> sign
plainSign = sign
sign}
  sineResult0 :: G_SInEResult
sineResult0@G_SInEResult{..} namedSentences :: [Named sentence]
namedSentences =
  let symbolCommonnesses' :: Map symbol Int
symbolCommonnesses' =
        String -> lid -> lid -> Map symbol Int -> Map symbol Int
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String -> lid1 -> lid2 -> Map symbol1 Int -> Map symbol2 Int
coerceSymbolCommonnesses "computeLeastCommonSymbols 1" lid
gSineLogic lid
gTheoryLid Map symbol Int
symbolCommonnesses
      leastCommonSymbols' :: Map (Named sentence) (symbol, Int)
leastCommonSymbols' =
        String
-> lid
-> lid
-> Map (Named sentence) (symbol, Int)
-> Map (Named sentence) (symbol, Int)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1
-> lid2
-> Map (Named sentence1) (symbol1, Int)
-> Map (Named sentence2) (symbol2, Int)
coerceLeastCommonSymbols "computeLeastCommonSymbols 2" lid
gSineLogic lid
gTheoryLid Map (Named sentence) (symbol, Int)
leastCommonSymbols
      result :: Map (Named sentence) (symbol, Int)
result =
        (Named sentence
 -> Map (Named sentence) (symbol, Int)
 -> Map (Named sentence) (symbol, Int))
-> Map (Named sentence) (symbol, Int)
-> [Named sentence]
-> Map (Named sentence) (symbol, Int)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ namedSentence :: Named sentence
namedSentence leastCommonSymbolsAcc :: Map (Named sentence) (symbol, Int)
leastCommonSymbolsAcc ->
                (symbol
 -> Map (Named sentence) (symbol, Int)
 -> Map (Named sentence) (symbol, Int))
-> Map (Named sentence) (symbol, Int)
-> [symbol]
-> Map (Named sentence) (symbol, Int)
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ symbol :: symbol
symbol leastCommonSymbolsAcc' :: Map (Named sentence) (symbol, Int)
leastCommonSymbolsAcc' ->
                        let commonness :: Int
commonness =
                              Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ symbol -> Map symbol Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup symbol
symbol Map symbol Int
symbolCommonnesses'
                        in  ((symbol, Int) -> (symbol, Int) -> (symbol, Int))
-> Named sentence
-> (symbol, Int)
-> Map (Named sentence) (symbol, Int)
-> Map (Named sentence) (symbol, Int)
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith (\ new :: (symbol, Int)
new (oldSymbol :: symbol
oldSymbol, oldCommonness :: Int
oldCommonness) ->
                                             if Int
commonness Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
oldCommonness
                                             then (symbol, Int)
new
                                             else (symbol
oldSymbol, Int
oldCommonness)
                                           )
                                           Named sentence
namedSentence
                                           (symbol
symbol, Int
commonness)
                                           Map (Named sentence) (symbol, Int)
leastCommonSymbolsAcc'
                      )
                      Map (Named sentence) (symbol, Int)
leastCommonSymbolsAcc ([symbol] -> Map (Named sentence) (symbol, Int))
-> [symbol] -> Map (Named sentence) (symbol, Int)
forall a b. (a -> b) -> a -> b
$
                      [symbol] -> [symbol]
forall a. Eq a => [a] -> [a]
nub ([symbol] -> [symbol]) -> [symbol] -> [symbol]
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sentence -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> [symbol]
symsOfSen lid
gTheoryLid sign
sign (sentence -> [symbol]) -> sentence -> [symbol]
forall a b. (a -> b) -> a -> b
$ Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
namedSentence
              ) Map (Named sentence) (symbol, Int)
leastCommonSymbols' [Named sentence]
namedSentences
  in  lid
-> Map (Named sentence) (symbol, Int)
-> G_SInEResult
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Map (Named sentence) (symbol, Int)
-> G_SInEResult
-> G_SInEResult
withLeastCommonSymbols lid
gTheoryLid Map (Named sentence) (symbol, Int)
result G_SInEResult
sineResult0
  where
    withLeastCommonSymbols :: Logic.Logic lid sublogics basic_spec sentence symb_items
                                          symb_map_items sign morphism symbol
                                          raw_symbol proof_tree
                           => lid
                           -> Map (Named sentence) (symbol, Int)
                           -> G_SInEResult
                           -> G_SInEResult
    withLeastCommonSymbols :: lid
-> Map (Named sentence) (symbol, Int)
-> G_SInEResult
-> G_SInEResult
withLeastCommonSymbols lid :: lid
lid leastCommonSymbols' :: Map (Named sentence) (symbol, Int)
leastCommonSymbols' _ =
      lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
G_SInEResult lid
gSineLogic SInEParameters
parameters Map symbol Int
symbolCommonnesses Map symbol [(Double, Named sentence)]
premiseTriggers
        (String
-> lid
-> lid
-> Map (Named sentence) (symbol, Int)
-> Map (Named sentence) (symbol, Int)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1
-> lid2
-> Map (Named sentence1) (symbol1, Int)
-> Map (Named sentence2) (symbol2, Int)
coerceLeastCommonSymbols "withLeastCommonSymbols" lid
lid lid
gSineLogic Map (Named sentence) (symbol, Int)
leastCommonSymbols')
        Set (Named sentence)
selectedPremises Set String
selectedPremiseNames

computePremiseTriggers :: Logic.Logic lid sublogics basic_spec sentence symb_items
                                      symb_map_items sign morphism symbol
                                      raw_symbol proof_tree
                       => lid
                       -> ExtSign sign symbol
                       -> G_SInEResult
                       -> [Named sentence]
                       -> G_SInEResult
computePremiseTriggers :: lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
computePremiseTriggers gTheoryLid :: lid
gTheoryLid ExtSign{plainSign :: forall sign symbol. ExtSign sign symbol -> sign
plainSign = sign
sign}
  sineResult0 :: G_SInEResult
sineResult0@G_SInEResult{..} namedSentences :: [Named sentence]
namedSentences =
  let symbolCommonnesses' :: Map symbol Int
symbolCommonnesses' =
        String -> lid -> lid -> Map symbol Int -> Map symbol Int
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String -> lid1 -> lid2 -> Map symbol1 Int -> Map symbol2 Int
coerceSymbolCommonnesses "computePremiseTriggers 1" lid
gSineLogic lid
gTheoryLid Map symbol Int
symbolCommonnesses
      leastCommonnesses' :: Map (Named sentence) (symbol, Int)
leastCommonnesses' = String
-> lid
-> lid
-> Map (Named sentence) (symbol, Int)
-> Map (Named sentence) (symbol, Int)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1
-> lid2
-> Map (Named sentence1) (symbol1, Int)
-> Map (Named sentence2) (symbol2, Int)
coerceLeastCommonSymbols "computePremiseTriggers 2" lid
gSineLogic lid
gTheoryLid Map (Named sentence) (symbol, Int)
leastCommonSymbols
      premiseTriggers' :: Map symbol [(Double, Named sentence)]
premiseTriggers' =
        String
-> lid
-> lid
-> Map symbol [(Double, Named sentence)]
-> Map symbol [(Double, Named sentence)]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1
-> lid2
-> Map symbol1 [(Double, Named sentence1)]
-> Map symbol2 [(Double, Named sentence2)]
coercePremiseTriggers "computePremiseTriggers 3" lid
gSineLogic lid
gTheoryLid Map symbol [(Double, Named sentence)]
premiseTriggers
      result :: Map symbol [(Double, Named sentence)]
result =
        (Named sentence
 -> Map symbol [(Double, Named sentence)]
 -> Map symbol [(Double, Named sentence)])
-> Map symbol [(Double, Named sentence)]
-> [Named sentence]
-> Map symbol [(Double, Named sentence)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ namedSentence :: Named sentence
namedSentence premiseTriggersAcc :: Map symbol [(Double, Named sentence)]
premiseTriggersAcc ->
                let (_,leastCommonness :: Int
leastCommonness) = Maybe (symbol, Int) -> (symbol, Int)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (symbol, Int) -> (symbol, Int))
-> Maybe (symbol, Int) -> (symbol, Int)
forall a b. (a -> b) -> a -> b
$
                      Named sentence
-> Map (Named sentence) (symbol, Int) -> Maybe (symbol, Int)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Named sentence
namedSentence Map (Named sentence) (symbol, Int)
leastCommonnesses'
                in  (symbol
 -> Map symbol [(Double, Named sentence)]
 -> Map symbol [(Double, Named sentence)])
-> Map symbol [(Double, Named sentence)]
-> [symbol]
-> Map symbol [(Double, Named sentence)]
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ symbol :: symbol
symbol premiseTriggersAcc' :: Map symbol [(Double, Named sentence)]
premiseTriggersAcc' ->
                            let symbolCommonness :: Int
                                symbolCommonness :: Int
symbolCommonness = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$
                                  symbol -> Map symbol Int -> Maybe Int
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup symbol
symbol Map symbol Int
symbolCommonnesses'
                                minimalTolerance :: Double
minimalTolerance =
                                  ((Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
symbolCommonness Double -> Double -> Double
forall a. Fractional a => a -> a -> a
/
                                    Int -> Double
forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
leastCommonness) :: Double)
                            in  ([(Double, Named sentence)]
 -> [(Double, Named sentence)] -> [(Double, Named sentence)])
-> symbol
-> [(Double, Named sentence)]
-> Map symbol [(Double, Named sentence)]
-> Map symbol [(Double, Named sentence)]
forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
Map.insertWith
                                  (\ _ triggers :: [(Double, Named sentence)]
triggers ->
                                    ((Double, Named sentence) -> (Double, Named sentence) -> Ordering)
-> (Double, Named sentence)
-> [(Double, Named sentence)]
-> [(Double, Named sentence)]
forall a. (a -> a -> Ordering) -> a -> [a] -> [a]
List.insertBy
                                      (\ (a :: Double
a, _) (b :: Double
b, _) -> Double -> Double -> Ordering
forall a. Ord a => a -> a -> Ordering
compare Double
a Double
b)
                                      (Double
minimalTolerance, Named sentence
namedSentence)
                                      [(Double, Named sentence)]
triggers
                                  )
                                  symbol
symbol
                                  [(Double
minimalTolerance, Named sentence
namedSentence)]
                                  Map symbol [(Double, Named sentence)]
premiseTriggersAcc'
                          )
                          Map symbol [(Double, Named sentence)]
premiseTriggersAcc ([symbol] -> Map symbol [(Double, Named sentence)])
-> [symbol] -> Map symbol [(Double, Named sentence)]
forall a b. (a -> b) -> a -> b
$
                          [symbol] -> [symbol]
forall a. Eq a => [a] -> [a]
nub ([symbol] -> [symbol]) -> [symbol] -> [symbol]
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sentence -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> [symbol]
symsOfSen lid
gTheoryLid sign
sign (sentence -> [symbol]) -> sentence -> [symbol]
forall a b. (a -> b) -> a -> b
$ Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
namedSentence
              ) Map symbol [(Double, Named sentence)]
premiseTriggers' [Named sentence]
namedSentences
  in  lid
-> Map symbol [(Double, Named sentence)]
-> G_SInEResult
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> Map symbol [(Double, Named sentence)]
-> G_SInEResult
-> G_SInEResult
withPremiseTriggers lid
gTheoryLid Map symbol [(Double, Named sentence)]
result G_SInEResult
sineResult0
  where
    withPremiseTriggers :: Logic.Logic lid sublogics basic_spec sentence
                                       symb_items symb_map_items sign morphism
                                       symbol raw_symbol proof_tree
                        => lid
                        -> Map symbol [(Double, Named sentence)]
                        -> G_SInEResult
                        -> G_SInEResult
    withPremiseTriggers :: lid
-> Map symbol [(Double, Named sentence)]
-> G_SInEResult
-> G_SInEResult
withPremiseTriggers lid :: lid
lid premiseTriggers' :: Map symbol [(Double, Named sentence)]
premiseTriggers' _ =
      lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
G_SInEResult lid
gSineLogic SInEParameters
parameters Map symbol Int
symbolCommonnesses
        (String
-> lid
-> lid
-> Map symbol [(Double, Named sentence)]
-> Map symbol [(Double, Named sentence)]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1
-> lid2
-> Map symbol1 [(Double, Named sentence1)]
-> Map symbol2 [(Double, Named sentence2)]
coercePremiseTriggers "withPremiseTriggers" lid
lid lid
gSineLogic Map symbol [(Double, Named sentence)]
premiseTriggers')
        Map (Named sentence) (symbol, Int)
leastCommonSymbols Set (Named sentence)
selectedPremises Set String
selectedPremiseNames


selectPremises :: Logic.Logic lid sublogics basic_spec sentence
                              symb_items symb_map_items sign morphism
                              symbol raw_symbol proof_tree
               => HetcatsOpts
               -> lid
               -> ExtSign sign symbol
               -> G_SInEResult
               -> Named sentence
               -> G_SInEResult
selectPremises :: HetcatsOpts
-> lid
-> ExtSign sign symbol
-> G_SInEResult
-> Named sentence
-> G_SInEResult
selectPremises opts :: HetcatsOpts
opts gTheoryLid :: lid
gTheoryLid extSign :: ExtSign sign symbol
extSign sineResult0 :: G_SInEResult
sineResult0@G_SInEResult{..} goal :: Named sentence
goal =
  let premiseLimitM :: Maybe Int
premiseLimitM = SInEParameters -> Maybe Int
premiseNumberLimit SInEParameters
parameters
      depthLimitM :: Maybe Int
depthLimitM = SInEParameters -> Maybe Int
depthLimit SInEParameters
parameters
      tolerance_ :: Double
tolerance_ = Double -> Maybe Double -> Double
forall a. a -> Maybe a -> a
fromMaybe 1.0 (Maybe Double -> Double) -> Maybe Double -> Double
forall a b. (a -> b) -> a -> b
$ SInEParameters -> Maybe Double
tolerance SInEParameters
parameters
  in  HetcatsOpts
-> Double
-> Maybe Int
-> Maybe Int
-> Int
-> lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
HetcatsOpts
-> Double
-> Maybe Int
-> Maybe Int
-> Int
-> lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
selectPremises' HetcatsOpts
opts Double
tolerance_ Maybe Int
depthLimitM Maybe Int
premiseLimitM 0 lid
gTheoryLid
        ExtSign sign symbol
extSign G_SInEResult
sineResult0 [Named sentence
goal]


selectPremises' :: Logic.Logic lid sublogics basic_spec sentence symb_items
                               symb_map_items sign morphism symbol
                               raw_symbol proof_tree
                => HetcatsOpts
                -> Double
                -> Maybe Int
                -> Maybe Int
                -> Int
                -> lid
                -> ExtSign sign symbol
                -> G_SInEResult
                -> [Named sentence]
                -> G_SInEResult
selectPremises' :: HetcatsOpts
-> Double
-> Maybe Int
-> Maybe Int
-> Int
-> lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
selectPremises' opts :: HetcatsOpts
opts tolerance_ :: Double
tolerance_ depthLimitM :: Maybe Int
depthLimitM premiseLimitM :: Maybe Int
premiseLimitM currentDepth :: Int
currentDepth
  gTheoryLid :: lid
gTheoryLid extSign :: ExtSign sign symbol
extSign@ExtSign{plainSign :: forall sign symbol. ExtSign sign symbol -> sign
plainSign = sign
sign}
  sineResult :: G_SInEResult
sineResult@G_SInEResult {..} previouslySelectedNamedSentences :: [Named sentence]
previouslySelectedNamedSentences
  | Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
depthLimitM Bool -> Bool -> Bool
&& Int
currentDepth Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
depthLimitM = G_SInEResult
sineResult
  | Maybe Int -> Bool
forall a. Maybe a -> Bool
isJust Maybe Int
premiseLimitM Bool -> Bool -> Bool
&& Set (Named sentence) -> Int
forall a. Set a -> Int
Set.size Set (Named sentence)
selectedPremises Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust Maybe Int
premiseLimitM = G_SInEResult
sineResult
  | Bool
otherwise =
    (Named sentence -> G_SInEResult -> G_SInEResult)
-> G_SInEResult -> [Named sentence] -> G_SInEResult
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ previouslySelectedNamedSentence :: Named sentence
previouslySelectedNamedSentence sineResultAcc :: G_SInEResult
sineResultAcc ->
              (symbol -> G_SInEResult -> G_SInEResult)
-> G_SInEResult -> [symbol] -> G_SInEResult
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ symbol :: symbol
symbol sineResultAcc' :: G_SInEResult
sineResultAcc' ->
                      let possiblyTriggeredSentences :: [(Double, Named sentence)]
possiblyTriggeredSentences =
                            Maybe [(Double, Named sentence)] -> [(Double, Named sentence)]
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe [(Double, Named sentence)] -> [(Double, Named sentence)])
-> Maybe [(Double, Named sentence)] -> [(Double, Named sentence)]
forall a b. (a -> b) -> a -> b
$ symbol
-> Map symbol [(Double, Named sentence)]
-> Maybe [(Double, Named sentence)]
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup symbol
symbol Map symbol [(Double, Named sentence)]
premiseTriggers'
                          triggeredSentences :: [Named sentence]
triggeredSentences =
                            ((Double, Named sentence) -> Named sentence)
-> [(Double, Named sentence)] -> [Named sentence]
forall a b. (a -> b) -> [a] -> [b]
map (Double, Named sentence) -> Named sentence
forall a b. (a, b) -> b
snd ([(Double, Named sentence)] -> [Named sentence])
-> [(Double, Named sentence)] -> [Named sentence]
forall a b. (a -> b) -> a -> b
$ ((Double, Named sentence) -> Bool)
-> [(Double, Named sentence)] -> [(Double, Named sentence)]
forall a. (a -> Bool) -> [a] -> [a]
takeWhile ((Double -> Double -> Bool
forall a. Ord a => a -> a -> Bool
<= Double
tolerance_) (Double -> Bool)
-> ((Double, Named sentence) -> Double)
-> (Double, Named sentence)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Double, Named sentence) -> Double
forall a b. (a, b) -> a
fst)
                              [(Double, Named sentence)]
possiblyTriggeredSentences
                          nextSelectedSentences :: [Named sentence]
nextSelectedSentences =
                            (Named sentence -> Bool) -> [Named sentence] -> [Named sentence]
forall a. (a -> Bool) -> [a] -> [a]
filter (Bool -> Bool
not (Bool -> Bool)
-> (Named sentence -> Bool) -> Named sentence -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. G_SInEResult -> lid -> Named sentence -> Bool
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
G_SInEResult -> lid -> Named sentence -> Bool
isSelected G_SInEResult
sineResultAcc' lid
gTheoryLid)
                              [Named sentence]
triggeredSentences
                          sineResultAcc'' :: G_SInEResult
sineResultAcc'' =
                            (Named sentence -> G_SInEResult -> G_SInEResult)
-> G_SInEResult -> [Named sentence] -> G_SInEResult
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (lid -> Named sentence -> G_SInEResult -> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> Named sentence -> G_SInEResult -> G_SInEResult
selectPremise lid
gTheoryLid) G_SInEResult
sineResultAcc'
                              [Named sentence]
nextSelectedSentences
                      in  HetcatsOpts
-> Double
-> Maybe Int
-> Maybe Int
-> Int
-> lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
HetcatsOpts
-> Double
-> Maybe Int
-> Maybe Int
-> Int
-> lid
-> ExtSign sign symbol
-> G_SInEResult
-> [Named sentence]
-> G_SInEResult
selectPremises' HetcatsOpts
opts Double
tolerance_ Maybe Int
depthLimitM
                            Maybe Int
premiseLimitM (Int
currentDepth Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) lid
gTheoryLid
                            ExtSign sign symbol
extSign G_SInEResult
sineResultAcc'' [Named sentence]
nextSelectedSentences
                    )
                    G_SInEResult
sineResultAcc ([symbol] -> G_SInEResult) -> [symbol] -> G_SInEResult
forall a b. (a -> b) -> a -> b
$
                    [symbol] -> [symbol]
forall a. Eq a => [a] -> [a]
nub ([symbol] -> [symbol]) -> [symbol] -> [symbol]
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sentence -> [symbol]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> [symbol]
symsOfSen lid
gTheoryLid sign
sign (sentence -> [symbol]) -> sentence -> [symbol]
forall a b. (a -> b) -> a -> b
$
                    Named sentence -> sentence
forall s a. SenAttr s a -> s
sentence Named sentence
previouslySelectedNamedSentence
           ) G_SInEResult
sineResult [Named sentence]
previouslySelectedNamedSentences
  where
    premiseTriggers' :: Map symbol [(Double, Named sentence)]
premiseTriggers' =
      String
-> lid
-> lid
-> Map symbol [(Double, Named sentence)]
-> Map symbol [(Double, Named sentence)]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1
-> lid2
-> Map symbol1 [(Double, Named sentence1)]
-> Map symbol2 [(Double, Named sentence2)]
coercePremiseTriggers "selectPremises' 1" lid
gSineLogic lid
gTheoryLid Map symbol [(Double, Named sentence)]
premiseTriggers

isSelected :: Logic.Logic lid sublogics basic_spec sentence symb_items
                          symb_map_items sign morphism symbol
                          raw_symbol proof_tree
           => G_SInEResult
           -> lid
           -> Named sentence
           -> Bool
isSelected :: G_SInEResult -> lid -> Named sentence -> Bool
isSelected G_SInEResult{..} _ namedSentence :: Named sentence
namedSentence =
  String -> Set String -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (Named sentence -> String
forall s a. SenAttr s a -> a
senAttr Named sentence
namedSentence) Set String
selectedPremiseNames

selectPremise :: Logic.Logic lid sublogics basic_spec sentence symb_items
                             symb_map_items sign morphism symbol
                             raw_symbol proof_tree
              => lid
              -> Named sentence
              -> G_SInEResult
              -> G_SInEResult
selectPremise :: lid -> Named sentence -> G_SInEResult -> G_SInEResult
selectPremise gTheoryLid :: lid
gTheoryLid triggeredSentence :: Named sentence
triggeredSentence G_SInEResult{..} =
  let symbolCommonnesses' :: Map symbol Int
symbolCommonnesses' =
        String -> lid -> lid -> Map symbol Int -> Map symbol Int
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String -> lid1 -> lid2 -> Map symbol1 Int -> Map symbol2 Int
coerceSymbolCommonnesses "selectPremise 1" lid
gSineLogic lid
gTheoryLid Map symbol Int
symbolCommonnesses
      premiseTriggers' :: Map symbol [(Double, Named sentence)]
premiseTriggers' =
        String
-> lid
-> lid
-> Map symbol [(Double, Named sentence)]
-> Map symbol [(Double, Named sentence)]
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1
-> lid2
-> Map symbol1 [(Double, Named sentence1)]
-> Map symbol2 [(Double, Named sentence2)]
coercePremiseTriggers "selectPremise 2" lid
gSineLogic lid
gTheoryLid Map symbol [(Double, Named sentence)]
premiseTriggers
      leastCommonSymbols' :: Map (Named sentence) (symbol, Int)
leastCommonSymbols' =
        String
-> lid
-> lid
-> Map (Named sentence) (symbol, Int)
-> Map (Named sentence) (symbol, Int)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1
-> lid2
-> Map (Named sentence1) (symbol1, Int)
-> Map (Named sentence2) (symbol2, Int)
coerceLeastCommonSymbols "selectPremise 3" lid
gSineLogic lid
gTheoryLid Map (Named sentence) (symbol, Int)
leastCommonSymbols
      selectedPremises' :: Set (Named sentence)
selectedPremises' = Named sentence -> Set (Named sentence) -> Set (Named sentence)
forall a. Ord a => a -> Set a -> Set a
Set.insert Named sentence
triggeredSentence (Set (Named sentence) -> Set (Named sentence))
-> Set (Named sentence) -> Set (Named sentence)
forall a b. (a -> b) -> a -> b
$
        String
-> lid -> lid -> Set (Named sentence) -> Set (Named sentence)
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2) =>
String
-> lid1 -> lid2 -> Set (Named sentence1) -> Set (Named sentence2)
coerceSelectedPremises "selectPremise 4" lid
gSineLogic lid
gTheoryLid Set (Named sentence)
selectedPremises
      selectedPremiseNames' :: Set String
selectedPremiseNames' = String -> Set String -> Set String
forall a. Ord a => a -> Set a -> Set a
Set.insert (Named sentence -> String
forall s a. SenAttr s a -> a
senAttr Named sentence
triggeredSentence) Set String
selectedPremiseNames
  in  lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid
-> SInEParameters
-> Map symbol Int
-> Map symbol [(Double, Named sentence)]
-> Map (Named sentence) (symbol, Int)
-> Set (Named sentence)
-> Set String
-> G_SInEResult
G_SInEResult lid
gTheoryLid SInEParameters
parameters Map symbol Int
symbolCommonnesses' Map symbol [(Double, Named sentence)]
premiseTriggers'
        Map (Named sentence) (symbol, Int)
leastCommonSymbols' Set (Named sentence)
selectedPremises' Set String
selectedPremiseNames'

saveToDatabase :: (MonadIO m, Fail.MonadFail m)
               => HetcatsOpts
               -> G_SInEResult
               -> Entity LocIdBase
               -> SinePremiseSelectionId
               -> DBMonad m ()
saveToDatabase :: HetcatsOpts
-> G_SInEResult
-> Entity LocIdBase
-> SinePremiseSelectionId
-> DBMonad m ()
saveToDatabase _ G_SInEResult{..} omsEntity :: Entity LocIdBase
omsEntity sinePremiseSelectionKey :: SinePremiseSelectionId
sinePremiseSelectionKey = do
  DBMonad m ()
saveSymbolPremiseTriggers
  DBMonad m ()
saveSymbolCommonnesses
  () -> DBMonad m ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  where
    saveSymbolPremiseTriggers :: DBMonad m ()
saveSymbolPremiseTriggers =
      ((symbol, [(Double, Named sentence)]) -> DBMonad m ())
-> [(symbol, [(Double, Named sentence)])] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (symbol :: symbol
symbol, triggers :: [(Double, Named sentence)]
triggers) -> do
              Key LocIdBase
symbolKey <- symbol -> ReaderT SqlBackend m (Key LocIdBase)
fetchSymbolId symbol
symbol
              ((Double, Named sentence)
 -> ReaderT SqlBackend m (Key SineSymbolPremiseTrigger))
-> [(Double, Named sentence)] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (minimalTolerance :: Double
minimalTolerance, namedSentence :: Named sentence
namedSentence) -> do
                      Key LocIdBase
premiseKey <- Named sentence -> ReaderT SqlBackend m (Key LocIdBase)
fetchSentenceId Named sentence
namedSentence
                      SineSymbolPremiseTrigger
-> ReaderT SqlBackend m (Key SineSymbolPremiseTrigger)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WSineSymbolPremiseTrigger :: SinePremiseSelectionId
-> Key LocIdBase
-> Key LocIdBase
-> Double
-> SineSymbolPremiseTrigger
SineSymbolPremiseTrigger
                        { sineSymbolPremiseTriggerSinePremiseSelectionId :: SinePremiseSelectionId
sineSymbolPremiseTriggerSinePremiseSelectionId = SinePremiseSelectionId
sinePremiseSelectionKey
                        , sineSymbolPremiseTriggerPremiseId :: Key LocIdBase
sineSymbolPremiseTriggerPremiseId = Key LocIdBase
premiseKey
                        , sineSymbolPremiseTriggerSymbolId :: Key LocIdBase
sineSymbolPremiseTriggerSymbolId = Key LocIdBase
symbolKey
                        , sineSymbolPremiseTriggerMinTolerance :: Double
sineSymbolPremiseTriggerMinTolerance = Double
minimalTolerance
                        }
                    ) [(Double, Named sentence)]
triggers
            ) ([(symbol, [(Double, Named sentence)])] -> DBMonad m ())
-> [(symbol, [(Double, Named sentence)])] -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ Map symbol [(Double, Named sentence)]
-> [(symbol, [(Double, Named sentence)])]
forall k a. Map k a -> [(k, a)]
Map.toList Map symbol [(Double, Named sentence)]
premiseTriggers

    saveSymbolCommonnesses :: DBMonad m ()
saveSymbolCommonnesses =
      ((symbol, Int) -> ReaderT SqlBackend m (Key SineSymbolCommonness))
-> [(symbol, Int)] -> DBMonad m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (\ (symbol :: symbol
symbol, commonness :: Int
commonness) -> do
              Key LocIdBase
symbolKey <- symbol -> ReaderT SqlBackend m (Key LocIdBase)
fetchSymbolId symbol
symbol
              SineSymbolCommonness
-> ReaderT SqlBackend m (Key SineSymbolCommonness)
forall backend (m :: * -> *) record.
(PersistStoreWrite backend, MonadIO m,
 PersistRecordBackend record backend) =>
record -> ReaderT backend m (Key record)
insert $WSineSymbolCommonness :: SinePremiseSelectionId
-> Key LocIdBase -> Int -> SineSymbolCommonness
SineSymbolCommonness
                { sineSymbolCommonnessSinePremiseSelectionId :: SinePremiseSelectionId
sineSymbolCommonnessSinePremiseSelectionId = SinePremiseSelectionId
sinePremiseSelectionKey
                , sineSymbolCommonnessSymbolId :: Key LocIdBase
sineSymbolCommonnessSymbolId = Key LocIdBase
symbolKey
                , sineSymbolCommonnessCommonness :: Int
sineSymbolCommonnessCommonness = Int
commonness
                }
            ) ([(symbol, Int)] -> DBMonad m ())
-> [(symbol, Int)] -> DBMonad m ()
forall a b. (a -> b) -> a -> b
$ Map symbol Int -> [(symbol, Int)]
forall k a. Map k a -> [(k, a)]
Map.toList Map symbol Int
symbolCommonnesses

    fetchSymbolId :: symbol -> ReaderT SqlBackend m (Key LocIdBase)
fetchSymbolId symbol :: symbol
symbol =
      let (locId :: String
locId, _, _, _) = Entity LocIdBase
-> lid -> symbol -> (String, String, String, String)
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
Entity LocIdBase
-> lid -> symbol -> (String, String, String, String)
symbolDetails Entity LocIdBase
omsEntity lid
gSineLogic symbol
symbol
      in  String -> String -> ReaderT SqlBackend m (Key LocIdBase)
forall (m :: * -> *) backend.
(MonadIO m, BackendCompatible SqlBackend backend,
 PersistQueryRead backend, PersistUniqueRead backend,
 MonadFail m) =>
String -> String -> ReaderT backend m (Key LocIdBase)
fetchLocId String
locId "Symbol"

    fetchSentenceId :: Named sentence -> ReaderT SqlBackend m (Key LocIdBase)
fetchSentenceId namedSentence :: Named sentence
namedSentence =
      let name :: String
name = Named sentence -> String
forall s a. SenAttr s a -> a
senAttr Named sentence
namedSentence
          locId :: String
locId = Entity LocIdBase -> String -> String
locIdOfSentence Entity LocIdBase
omsEntity String
name
      in  String -> String -> ReaderT SqlBackend m (Key LocIdBase)
forall (m :: * -> *) backend.
(MonadIO m, BackendCompatible SqlBackend backend,
 PersistQueryRead backend, PersistUniqueRead backend,
 MonadFail m) =>
String -> String -> ReaderT backend m (Key LocIdBase)
fetchLocId String
locId "Sentence"

    fetchLocId :: String -> String -> ReaderT backend m (Key LocIdBase)
fetchLocId locId :: String
locId kind :: String
kind = do
      [Entity LocIdBase]
sentenceL <- SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT backend m [Entity LocIdBase]
forall a r (m :: * -> *).
(SqlSelect a r, MonadIO m) =>
SqlQuery a -> SqlReadT m [r]
select (SqlQuery (SqlExpr (Entity LocIdBase))
 -> ReaderT backend m [Entity LocIdBase])
-> SqlQuery (SqlExpr (Entity LocIdBase))
-> ReaderT backend m [Entity LocIdBase]
forall a b. (a -> b) -> a -> b
$ (SqlExpr (Entity LocIdBase)
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. From a => (a -> SqlQuery b) -> SqlQuery b
from ((SqlExpr (Entity LocIdBase)
  -> SqlQuery (SqlExpr (Entity LocIdBase)))
 -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> (SqlExpr (Entity LocIdBase)
    -> SqlQuery (SqlExpr (Entity LocIdBase)))
-> SqlQuery (SqlExpr (Entity LocIdBase))
forall a b. (a -> b) -> a -> b
$ \ loc_id_bases :: SqlExpr (Entity LocIdBase)
loc_id_bases -> do
        SqlExpr (Value Bool) -> SqlQuery ()
where_ (SqlExpr (Entity LocIdBase)
loc_id_bases SqlExpr (Entity LocIdBase)
-> EntityField LocIdBase String -> SqlExpr (Value String)
forall typ val.
(PersistEntity val, PersistField typ) =>
SqlExpr (Entity val) -> EntityField val typ -> SqlExpr (Value typ)
^. EntityField LocIdBase String
forall typ. (typ ~ String) => EntityField LocIdBase typ
LocIdBaseLocId SqlExpr (Value String)
-> SqlExpr (Value String) -> SqlExpr (Value Bool)
forall typ.
PersistField typ =>
SqlExpr (Value typ) -> SqlExpr (Value typ) -> SqlExpr (Value Bool)
==. String -> SqlExpr (Value String)
forall typ. PersistField typ => typ -> SqlExpr (Value typ)
val String
locId)
        Int64 -> SqlQuery ()
limit 1
        SqlExpr (Entity LocIdBase) -> SqlQuery (SqlExpr (Entity LocIdBase))
forall (m :: * -> *) a. Monad m => a -> m a
return SqlExpr (Entity LocIdBase)
loc_id_bases
      case [Entity LocIdBase]
sentenceL of
        [] -> String -> ReaderT backend m (Key LocIdBase)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ("Persistence.Reasoning.saveToDatabase: Could not find " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
kind String -> String -> String
forall a. [a] -> [a] -> [a]
++ " " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
locId)
        Entity key :: Key LocIdBase
key _ : _ -> Key LocIdBase -> ReaderT backend m (Key LocIdBase)
forall (m :: * -> *) a. Monad m => a -> m a
return Key LocIdBase
key


coerceSymbolCommonnesses ::
   (Logic.Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
   Logic.Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
   => String -> lid1 -> lid2 -> Map symbol1 Int -> Map symbol2 Int
coerceSymbolCommonnesses :: String -> lid1 -> lid2 -> Map symbol1 Int -> Map symbol2 Int
coerceSymbolCommonnesses errorMessage :: String
errorMessage lid1 :: lid1
lid1 lid2 :: lid2
lid2 a :: Map symbol1 Int
a =
  let errorMessage' :: String
errorMessage' =
        "PremiseSelectionSInE." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
errorMessage String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": Coercion failed."
  in  Map symbol2 Int -> Maybe (Map symbol2 Int) -> Map symbol2 Int
forall a. a -> Maybe a -> a
fromMaybe (String -> Map symbol2 Int
forall a. HasCallStack => String -> a
error String
errorMessage') (Maybe (Map symbol2 Int) -> Map symbol2 Int)
-> Maybe (Map symbol2 Int) -> Map symbol2 Int
forall a b. (a -> b) -> a -> b
$ lid1
-> lid2 -> String -> Map symbol1 Int -> Maybe (Map symbol2 Int)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce lid1
lid1 lid2
lid2 String
errorMessage' Map symbol1 Int
a

coerceLeastCommonSymbols ::
   (Logic.Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
   Logic.Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
   => String -> lid1 -> lid2 
         -> Map (Named sentence1) (symbol1, Int)
         -> Map (Named sentence2) (symbol2, Int)
coerceLeastCommonSymbols :: String
-> lid1
-> lid2
-> Map (Named sentence1) (symbol1, Int)
-> Map (Named sentence2) (symbol2, Int)
coerceLeastCommonSymbols errorMessage :: String
errorMessage lid1 :: lid1
lid1 lid2 :: lid2
lid2 a :: Map (Named sentence1) (symbol1, Int)
a =
  let errorMessage' :: String
errorMessage' =
        "PremiseSelectionSInE." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
errorMessage String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": Coercion failed."
  in  Map (Named sentence2) (symbol2, Int)
-> Maybe (Map (Named sentence2) (symbol2, Int))
-> Map (Named sentence2) (symbol2, Int)
forall a. a -> Maybe a -> a
fromMaybe (String -> Map (Named sentence2) (symbol2, Int)
forall a. HasCallStack => String -> a
error String
errorMessage') (Maybe (Map (Named sentence2) (symbol2, Int))
 -> Map (Named sentence2) (symbol2, Int))
-> Maybe (Map (Named sentence2) (symbol2, Int))
-> Map (Named sentence2) (symbol2, Int)
forall a b. (a -> b) -> a -> b
$ lid1
-> lid2
-> String
-> Map (Named sentence1) (symbol1, Int)
-> Maybe (Map (Named sentence2) (symbol2, Int))
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce lid1
lid1 lid2
lid2 String
errorMessage' Map (Named sentence1) (symbol1, Int)
a

coercePremiseTriggers ::
   (Logic.Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
   Logic.Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
   => String -> lid1 -> lid2 
         -> Map symbol1 [(Double, Named sentence1)]
         -> Map symbol2 [(Double, Named sentence2)]
coercePremiseTriggers :: String
-> lid1
-> lid2
-> Map symbol1 [(Double, Named sentence1)]
-> Map symbol2 [(Double, Named sentence2)]
coercePremiseTriggers errorMessage :: String
errorMessage lid1 :: lid1
lid1 lid2 :: lid2
lid2 a :: Map symbol1 [(Double, Named sentence1)]
a =
  let errorMessage' :: String
errorMessage' =
        "PremiseSelectionSInE." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
errorMessage String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": Coercion failed."
  in  Map symbol2 [(Double, Named sentence2)]
-> Maybe (Map symbol2 [(Double, Named sentence2)])
-> Map symbol2 [(Double, Named sentence2)]
forall a. a -> Maybe a -> a
fromMaybe (String -> Map symbol2 [(Double, Named sentence2)]
forall a. HasCallStack => String -> a
error String
errorMessage') (Maybe (Map symbol2 [(Double, Named sentence2)])
 -> Map symbol2 [(Double, Named sentence2)])
-> Maybe (Map symbol2 [(Double, Named sentence2)])
-> Map symbol2 [(Double, Named sentence2)]
forall a b. (a -> b) -> a -> b
$ lid1
-> lid2
-> String
-> Map symbol1 [(Double, Named sentence1)]
-> Maybe (Map symbol2 [(Double, Named sentence2)])
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce lid1
lid1 lid2
lid2 String
errorMessage' Map symbol1 [(Double, Named sentence1)]
a

coerceSelectedPremises ::
   (Logic.Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
   Logic.Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
   => String -> lid1 -> lid2 -> Set (Named sentence1) -> Set (Named sentence2)
coerceSelectedPremises :: String
-> lid1 -> lid2 -> Set (Named sentence1) -> Set (Named sentence2)
coerceSelectedPremises errorMessage :: String
errorMessage lid1 :: lid1
lid1 lid2 :: lid2
lid2 a :: Set (Named sentence1)
a =
  let errorMessage' :: String
errorMessage' =
        "PremiseSelectionSInE." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
errorMessage String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": Coercion failed."
  in  Set (Named sentence2)
-> Maybe (Set (Named sentence2)) -> Set (Named sentence2)
forall a. a -> Maybe a -> a
fromMaybe (String -> Set (Named sentence2)
forall a. HasCallStack => String -> a
error String
errorMessage') (Maybe (Set (Named sentence2)) -> Set (Named sentence2))
-> Maybe (Set (Named sentence2)) -> Set (Named sentence2)
forall a b. (a -> b) -> a -> b
$ lid1
-> lid2
-> String
-> Set (Named sentence1)
-> Maybe (Set (Named sentence2))
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce lid1
lid1 lid2
lid2 String
errorMessage' Set (Named sentence1)
a

coerceSen ::
   (Logic.Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
   Logic.Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
   => String -> lid1 -> lid2 -> Named sentence1 -> Named sentence2
coerceSen :: String -> lid1 -> lid2 -> Named sentence1 -> Named sentence2
coerceSen errorMessage :: String
errorMessage lid1 :: lid1
lid1 lid2 :: lid2
lid2 a :: Named sentence1
a =
  let errorMessage' :: String
errorMessage' =
        "PremiseSelectionSInE." String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
errorMessage String -> String -> String
forall a. [a] -> [a] -> [a]
++ ": Coercion failed."
  in  Named sentence2 -> Maybe (Named sentence2) -> Named sentence2
forall a. a -> Maybe a -> a
fromMaybe (String -> Named sentence2
forall a. HasCallStack => String -> a
error String
errorMessage') (Maybe (Named sentence2) -> Named sentence2)
-> Maybe (Named sentence2) -> Named sentence2
forall a b. (a -> b) -> a -> b
$ lid1
-> lid2 -> String -> Named sentence1 -> Maybe (Named sentence2)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce lid1
lid1 lid2
lid2 String
errorMessage' Named sentence1
a