{-# LANGUAGE ExistentialQuantification, DeriveDataTypeable
  , GeneralizedNewtypeDeriving #-}
{- |
Module      :  ./Static/GTheory.hs
Description :  theory datastructure for development graphs
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

theory datastructure for development graphs
-}

module Static.GTheory where

import Logic.Prover
import Logic.Logic
import Logic.ExtSign
import Logic.Grothendieck
import Logic.Comorphism
import Logic.Coerce

import qualified Common.OrderedMap as OMap

import ATerm.Lib
import Common.Lib.Graph as Tree
import Common.Amalgamate -- for now
import Common.Keywords
import Common.AS_Annotation
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.IRI
import Common.Result

import Data.Graph.Inductive.Graph as Graph

import Data.List
import qualified Data.Map as Map

import Data.Typeable

import Control.Monad (foldM)
import qualified Control.Monad.Fail as Fail
import Control.Exception

-- a theory index describing a set of sentences
newtype ThId = ThId Int
  deriving (Typeable, Int -> ThId -> ShowS
[ThId] -> ShowS
ThId -> String
(Int -> ThId -> ShowS)
-> (ThId -> String) -> ([ThId] -> ShowS) -> Show ThId
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ThId] -> ShowS
$cshowList :: [ThId] -> ShowS
show :: ThId -> String
$cshow :: ThId -> String
showsPrec :: Int -> ThId -> ShowS
$cshowsPrec :: Int -> ThId -> ShowS
Show, ThId -> ThId -> Bool
(ThId -> ThId -> Bool) -> (ThId -> ThId -> Bool) -> Eq ThId
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: ThId -> ThId -> Bool
$c/= :: ThId -> ThId -> Bool
== :: ThId -> ThId -> Bool
$c== :: ThId -> ThId -> Bool
Eq, Eq ThId
Eq ThId =>
(ThId -> ThId -> Ordering)
-> (ThId -> ThId -> Bool)
-> (ThId -> ThId -> Bool)
-> (ThId -> ThId -> Bool)
-> (ThId -> ThId -> Bool)
-> (ThId -> ThId -> ThId)
-> (ThId -> ThId -> ThId)
-> Ord ThId
ThId -> ThId -> Bool
ThId -> ThId -> Ordering
ThId -> ThId -> ThId
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: ThId -> ThId -> ThId
$cmin :: ThId -> ThId -> ThId
max :: ThId -> ThId -> ThId
$cmax :: ThId -> ThId -> ThId
>= :: ThId -> ThId -> Bool
$c>= :: ThId -> ThId -> Bool
> :: ThId -> ThId -> Bool
$c> :: ThId -> ThId -> Bool
<= :: ThId -> ThId -> Bool
$c<= :: ThId -> ThId -> Bool
< :: ThId -> ThId -> Bool
$c< :: ThId -> ThId -> Bool
compare :: ThId -> ThId -> Ordering
$ccompare :: ThId -> ThId -> Ordering
$cp1Ord :: Eq ThId
Ord, Int -> ThId
ThId -> Int
ThId -> [ThId]
ThId -> ThId
ThId -> ThId -> [ThId]
ThId -> ThId -> ThId -> [ThId]
(ThId -> ThId)
-> (ThId -> ThId)
-> (Int -> ThId)
-> (ThId -> Int)
-> (ThId -> [ThId])
-> (ThId -> ThId -> [ThId])
-> (ThId -> ThId -> [ThId])
-> (ThId -> ThId -> ThId -> [ThId])
-> Enum ThId
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: ThId -> ThId -> ThId -> [ThId]
$cenumFromThenTo :: ThId -> ThId -> ThId -> [ThId]
enumFromTo :: ThId -> ThId -> [ThId]
$cenumFromTo :: ThId -> ThId -> [ThId]
enumFromThen :: ThId -> ThId -> [ThId]
$cenumFromThen :: ThId -> ThId -> [ThId]
enumFrom :: ThId -> [ThId]
$cenumFrom :: ThId -> [ThId]
fromEnum :: ThId -> Int
$cfromEnum :: ThId -> Int
toEnum :: Int -> ThId
$ctoEnum :: Int -> ThId
pred :: ThId -> ThId
$cpred :: ThId -> ThId
succ :: ThId -> ThId
$csucc :: ThId -> ThId
Enum, Typeable ThId
Typeable ThId =>
(ATermTable -> ThId -> IO (ATermTable, Int))
-> (ATermTable -> [ThId] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, ThId))
-> (Int -> ATermTable -> (ATermTable, [ThId]))
-> ShATermConvertible ThId
Int -> ATermTable -> (ATermTable, [ThId])
Int -> ATermTable -> (ATermTable, ThId)
ATermTable -> [ThId] -> IO (ATermTable, Int)
ATermTable -> ThId -> IO (ATermTable, Int)
forall t.
Typeable t =>
(ATermTable -> t -> IO (ATermTable, Int))
-> (ATermTable -> [t] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, t))
-> (Int -> ATermTable -> (ATermTable, [t]))
-> ShATermConvertible t
fromShATermList' :: Int -> ATermTable -> (ATermTable, [ThId])
$cfromShATermList' :: Int -> ATermTable -> (ATermTable, [ThId])
fromShATermAux :: Int -> ATermTable -> (ATermTable, ThId)
$cfromShATermAux :: Int -> ATermTable -> (ATermTable, ThId)
toShATermList' :: ATermTable -> [ThId] -> IO (ATermTable, Int)
$ctoShATermList' :: ATermTable -> [ThId] -> IO (ATermTable, Int)
toShATermAux :: ATermTable -> ThId -> IO (ATermTable, Int)
$ctoShATermAux :: ATermTable -> ThId -> IO (ATermTable, Int)
$cp1ShATermConvertible :: Typeable ThId
ShATermConvertible)

startThId :: ThId
startThId :: ThId
startThId = Int -> ThId
ThId 0

-- | Grothendieck theories with lookup indices
data G_theory = 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_theory
    { ()
gTheoryLogic :: lid
    , G_theory -> Maybe IRI
gTheorySyntax :: Maybe IRI
    , ()
gTheorySign :: ExtSign sign symbol
    , G_theory -> SigId
gTheorySignIdx :: SigId -- ^ index to lookup 'G_sign' (using 'signOf')
    , ()
gTheorySens :: ThSens sentence (AnyComorphism, BasicProof)
    , G_theory -> ThId
gTheorySelfIdx :: ThId -- ^ index to lookup this 'G_theory' in theory map
    } deriving Typeable

createGThWith :: G_theory -> SigId -> ThId -> G_theory
createGThWith :: G_theory -> SigId -> ThId -> G_theory
createGThWith (G_theory gtl :: lid
gtl gsub :: Maybe IRI
gsub gts :: ExtSign sign symbol
gts _ _ _) si :: SigId
si =
  lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
gtl Maybe IRI
gsub ExtSign sign symbol
gts SigId
si ThSens sentence (AnyComorphism, BasicProof)
forall a b. ThSens a b
noSens

coerceThSens ::
   ( 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
   , Fail.MonadFail m, Typeable b)
   => lid1 -> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens :: lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens = lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce

instance Eq G_theory where
  G_theory l1 :: lid
l1 ser1 :: Maybe IRI
ser1 sig1 :: ExtSign sign symbol
sig1 ind1 :: SigId
ind1 sens1 :: ThSens sentence (AnyComorphism, BasicProof)
sens1 ind1' :: ThId
ind1'
    == :: G_theory -> G_theory -> Bool
== G_theory l2 :: lid
l2 ser2 :: Maybe IRI
ser2 sig2 :: ExtSign sign symbol
sig2 ind2 :: SigId
ind2 sens2 :: ThSens sentence (AnyComorphism, BasicProof)
sens2 ind2' :: ThId
ind2' = Maybe IRI
ser1 Maybe IRI -> Maybe IRI -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe IRI
ser2
     Bool -> Bool -> Bool
&& lid -> ExtSign sign symbol -> SigId -> G_sign
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 -> SigId -> G_sign
G_sign lid
l1 ExtSign sign symbol
sig1 SigId
ind1 G_sign -> G_sign -> Bool
forall a. Eq a => a -> a -> Bool
== lid -> ExtSign sign symbol -> SigId -> G_sign
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 -> SigId -> G_sign
G_sign lid
l2 ExtSign sign symbol
sig2 SigId
ind2
     Bool -> Bool -> Bool
&& (ThId
ind1' ThId -> ThId -> Bool
forall a. Ord a => a -> a -> Bool
> ThId
startThId Bool -> Bool -> Bool
&& ThId
ind2' ThId -> ThId -> Bool
forall a. Ord a => a -> a -> Bool
> ThId
startThId Bool -> Bool -> Bool
&& ThId
ind1' ThId -> ThId -> Bool
forall a. Eq a => a -> a -> Bool
== ThId
ind2'
         Bool -> Bool -> Bool
|| lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
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 (m :: * -> *) b.
(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,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
l1 lid
l2 "" ThSens sentence (AnyComorphism, BasicProof)
sens1 Maybe (ThSens sentence (AnyComorphism, BasicProof))
-> Maybe (ThSens sentence (AnyComorphism, BasicProof)) -> Bool
forall a. Eq a => a -> a -> Bool
== ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
forall a. a -> Maybe a
Just ThSens sentence (AnyComorphism, BasicProof)
sens2)

instance Show G_theory where
  show :: G_theory -> String
show (G_theory _ _ sign :: ExtSign sign symbol
sign _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) =
     ExtSign sign symbol -> ShowS
forall a. Show a => a -> ShowS
shows ExtSign sign symbol
sign ShowS -> ShowS
forall a b. (a -> b) -> a -> b
$ '\n' Char -> ShowS
forall a. a -> [a] -> [a]
: ThSens sentence (AnyComorphism, BasicProof) -> String
forall a. Show a => a -> String
show ThSens sentence (AnyComorphism, BasicProof)
sens

instance Pretty G_theory where
  pretty :: G_theory -> Doc
pretty g :: G_theory
g = Maybe IRI -> G_theory -> Doc
prettyFullGTheory (G_theory -> Maybe IRI
gTheorySyntax G_theory
g) G_theory
g

prettyFullGTheory :: Maybe IRI -> G_theory -> Doc
prettyFullGTheory :: Maybe IRI -> G_theory -> Doc
prettyFullGTheory sm :: Maybe IRI
sm g :: G_theory
g = G_theory -> Doc
prettyGTheorySL G_theory
g Doc -> Doc -> Doc
$++$ Maybe IRI -> G_theory -> Doc
prettyGTheory Maybe IRI
sm G_theory
g

prettyGTheorySL :: G_theory -> Doc
prettyGTheorySL :: G_theory -> Doc
prettyGTheorySL g :: G_theory
g = String -> Doc
keyword String
logicS Doc -> Doc -> Doc
<+> String -> Doc
structId (G_sublogics -> String
forall a. Show a => a -> String
show (G_sublogics -> String) -> G_sublogics -> String
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sublogics
sublogicOfTh G_theory
g)

prettyGTheory :: Maybe IRI -> G_theory -> Doc
prettyGTheory :: Maybe IRI -> G_theory -> Doc
prettyGTheory sm :: Maybe IRI
sm g :: G_theory
g = case G_theory -> G_theory
simplifyTh G_theory
g of
     G_theory lid :: lid
lid _ sign :: ExtSign sign symbol
sign@(ExtSign s :: sign
s _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _ -> let l :: [Named sentence]
l = ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens in
         if [Named sentence] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Named sentence]
l Bool -> Bool -> Bool
&& lid -> ExtSign sign symbol -> ExtSign sign symbol -> 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 =>
lid -> ExtSign sign symbol -> ExtSign sign symbol -> Bool
ext_is_subsig lid
lid ExtSign sign symbol
sign (lid -> ExtSign sign symbol
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
ext_empty_signature lid
lid) then
             Doc -> Doc
specBraces Doc
Common.Doc.empty else Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
Maybe IRI -> lid -> (sign, [Named sentence]) -> Doc
printTheory Maybe IRI
sm lid
lid (sign
s, [Named sentence]
l)

-- | compute sublogic of a theory
sublogicOfTh :: G_theory -> G_sublogics
sublogicOfTh :: G_theory -> G_sublogics
sublogicOfTh (G_theory lid :: lid
lid _ (ExtSign sigma :: sign
sigma _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) =
  let sub :: sublogics
sub = lid -> (sign, [sentence]) -> sublogics
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 -> (sign, [sentence]) -> sublogics
sublogicOfTheo lid
lid (sign
sigma, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> sentence)
-> ((String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
    -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> (String,
    SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall a b. (a, b) -> b
snd ((String, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> sentence)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [sentence]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ThSens sentence (AnyComorphism, BasicProof)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens sentence (AnyComorphism, BasicProof)
sens)
   in lid -> sublogics -> G_sublogics
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 -> sublogics -> G_sublogics
G_sublogics lid
lid sublogics
sub

-- | get theorem names with their best proof results
getThGoals :: G_theory -> [(String, Maybe BasicProof)]
getThGoals :: G_theory -> [(String, Maybe BasicProof)]
getThGoals (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = ((String, SenStatus sentence (AnyComorphism, BasicProof))
 -> (String, Maybe BasicProof))
-> [(String, SenStatus sentence (AnyComorphism, BasicProof))]
-> [(String, Maybe BasicProof)]
forall a b. (a -> b) -> [a] -> [b]
map (String, SenStatus sentence (AnyComorphism, BasicProof))
-> (String, Maybe BasicProof)
forall a a a a. Ord a => (a, SenStatus a (a, a)) -> (a, Maybe a)
toGoal ([(String, SenStatus sentence (AnyComorphism, BasicProof))]
 -> [(String, Maybe BasicProof)])
-> (ThSens sentence (AnyComorphism, BasicProof)
    -> [(String, SenStatus sentence (AnyComorphism, BasicProof))])
-> ThSens sentence (AnyComorphism, BasicProof)
-> [(String, Maybe BasicProof)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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)
 -> [(String, Maybe BasicProof)])
-> ThSens sentence (AnyComorphism, BasicProof)
-> [(String, Maybe BasicProof)]
forall a b. (a -> b) -> a -> b
$ (SenStatus sentence (AnyComorphism, BasicProof) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter (Bool -> Bool
not (Bool -> Bool)
-> (SenStatus sentence (AnyComorphism, BasicProof) -> Bool)
-> SenStatus sentence (AnyComorphism, BasicProof)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenStatus sentence (AnyComorphism, BasicProof) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom) ThSens sentence (AnyComorphism, BasicProof)
sens
  where toGoal :: (a, SenStatus a (a, a)) -> (a, Maybe a)
toGoal (n :: a
n, st :: SenStatus a (a, a)
st) = let ts :: [(a, a)]
ts = SenStatus a (a, a) -> [(a, a)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenStatus a (a, a)
st in
               (a
n, if [(a, a)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(a, a)]
ts then Maybe a
forall a. Maybe a
Nothing else a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
maximum ([a] -> a) -> [a] -> a
forall a b. (a -> b) -> a -> b
$ ((a, a) -> a) -> [(a, a)] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map (a, a) -> a
forall a b. (a, b) -> b
snd [(a, a)]
ts)

-- | get axiom names plus True for former theorem
getThAxioms :: G_theory -> [(String, Bool)]
getThAxioms :: G_theory -> [(String, Bool)]
getThAxioms (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = ((String, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> (String, Bool))
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [(String, Bool)]
forall a b. (a -> b) -> [a] -> [b]
map
    (\ (k :: String
k, s :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s) -> (String
k, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
wasTheorem SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s))
    ([(String,
   SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
 -> [(String, Bool)])
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [(String, Bool)]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList (ThSens sentence (AnyComorphism, BasicProof)
 -> [(String,
      SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))])
-> ThSens sentence (AnyComorphism, BasicProof)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall a b. (a -> b) -> a -> b
$ (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom ThSens sentence (AnyComorphism, BasicProof)
sens

-- | get sentence names
getThSens :: G_theory -> [String]
getThSens :: G_theory -> [String]
getThSens (G_theory _ _ _ _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = ((String, SenStatus sentence (AnyComorphism, BasicProof))
 -> String)
-> [(String, SenStatus sentence (AnyComorphism, BasicProof))]
-> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, SenStatus sentence (AnyComorphism, BasicProof)) -> String
forall a b. (a, b) -> a
fst ([(String, SenStatus sentence (AnyComorphism, BasicProof))]
 -> [String])
-> [(String, SenStatus sentence (AnyComorphism, BasicProof))]
-> [String]
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)
sens

-- | simplify a theory (throw away qualifications)
simplifyTh :: G_theory -> G_theory
simplifyTh :: G_theory -> G_theory
simplifyTh (G_theory lid :: lid
lid gsyn :: Maybe IRI
gsyn sigma :: ExtSign sign symbol
sigma@(ExtSign s :: sign
s _) ind1 :: SigId
ind1 sens :: ThSens sentence (AnyComorphism, BasicProof)
sens ind2 :: ThId
ind2) =
    lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
gsyn ExtSign sign symbol
sigma SigId
ind1
      ((SenStatus sentence (AnyComorphism, BasicProof)
 -> SenStatus sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map ((sentence -> sentence)
-> SenStatus sentence (AnyComorphism, BasicProof)
-> SenStatus sentence (AnyComorphism, BasicProof)
forall a b c. (a -> b) -> SenStatus a c -> SenStatus b c
mapValue ((sentence -> sentence)
 -> SenStatus sentence (AnyComorphism, BasicProof)
 -> SenStatus sentence (AnyComorphism, BasicProof))
-> (sentence -> sentence)
-> SenStatus sentence (AnyComorphism, BasicProof)
-> SenStatus sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ lid -> sign -> sentence -> sentence
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen lid
lid sign
s) ThSens sentence (AnyComorphism, BasicProof)
sens) ThId
ind2

-- | apply a comorphism to a theory
mapG_theory :: Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory :: Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory lossy :: Bool
lossy (Comorphism cid :: cid
cid) (G_theory lid :: lid
lid _ (ExtSign sign :: sign
sign _)
            ind1 :: SigId
ind1 sens :: ThSens sentence (AnyComorphism, BasicProof)
sens ind2 :: ThId
ind2) =
  do
  (sign1, [Named sentence1])
bTh <- lid
-> lid1
-> String
-> (sign, [Named sentence])
-> Result (sign1, [Named sentence1])
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid (cid -> lid1
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid1
sourceLogic cid
cid)
    ("unapplicable comorphism '" String -> ShowS
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid String -> ShowS
forall a. [a] -> [a] -> [a]
++ "'\n")
    (sign
sign, ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens)
  (sign' :: sign2
sign', sens' :: [Named sentence2]
sens') <- Bool
-> cid
-> (sign1, [Named sentence1])
-> Result (sign2, [Named sentence2])
forall cid 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.
Comorphism
  cid
  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 =>
Bool
-> cid
-> (sign1, [Named sentence1])
-> Result (sign2, [Named sentence2])
wrapMapTheoryPossiblyLossy Bool
lossy cid
cid (sign1, [Named sentence1])
bTh
  G_theory -> Result G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> Result G_theory) -> G_theory -> Result G_theory
forall a b. (a -> b) -> a -> b
$ lid2
-> Maybe IRI
-> ExtSign sign2 symbol2
-> SigId
-> ThSens sentence2 (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory (cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid) Maybe IRI
forall a. Maybe a
Nothing (sign2 -> ExtSign sign2 symbol2
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign sign2
sign')
         SigId
ind1 ([Named sentence2] -> ThSens sentence2 (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence2]
sens') ThId
ind2

-- | Embedding of GTCs as Grothendieck sig mors
gEmbedGTC :: AnyComorphism -> G_theory -> Result GMorphism
gEmbedGTC :: AnyComorphism -> G_theory -> Result GMorphism
gEmbedGTC (Comorphism cid :: cid
cid) gth :: G_theory
gth@(G_theory lid :: lid
lid _ ssig :: ExtSign sign symbol
ssig _ _ _) = do 
  (G_theory lid' :: lid
lid' _ tsig :: ExtSign sign symbol
tsig ind :: SigId
ind _ _) <- Bool -> AnyComorphism -> G_theory -> Result G_theory
mapG_theory Bool
False (cid -> AnyComorphism
forall cid 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.
Comorphism
  cid
  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 =>
cid -> AnyComorphism
Comorphism cid
cid) G_theory
gth
  ExtSign sign1 symbol1
ssig' <- lid
-> lid1
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign1 symbol1)
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid (cid -> lid1
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid1
sourceLogic cid
cid) "can't convert sigs" ExtSign sign symbol
ssig
  (ExtSign s :: sign2
s _) <- lid
-> lid2
-> String
-> ExtSign sign symbol
-> Result (ExtSign sign2 symbol2)
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid' (cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid) "can't convert sigs" ExtSign sign symbol
tsig
  GMorphism -> Result GMorphism
forall (m :: * -> *) a. Monad m => a -> m a
return (GMorphism -> Result GMorphism) -> GMorphism -> Result GMorphism
forall a b. (a -> b) -> a -> b
$ cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
forall cid 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.
Comorphism
  cid
  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 =>
cid
-> ExtSign sign1 symbol1
-> SigId
-> morphism2
-> MorId
-> GMorphism
GMorphism cid
cid ExtSign sign1 symbol1
ssig' SigId
ind (sign2 -> morphism2
forall object morphism.
Category object morphism =>
object -> morphism
ide sign2
s) MorId
startMorId

-- | Translation of a G_theory along a GMorphism
translateG_theory :: GMorphism -> G_theory -> Result G_theory
translateG_theory :: GMorphism -> G_theory -> Result G_theory
translateG_theory (GMorphism cid :: cid
cid _ _ morphism2 :: morphism2
morphism2 _)
                      (G_theory lid :: lid
lid _ (ExtSign sign :: sign
sign _) _ sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) = do
  let tlid :: lid2
tlid = cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid
  (sign1, [Named sentence1])
bTh <- lid
-> lid1
-> String
-> (sign, [Named sentence])
-> Result (sign1, [Named sentence1])
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid (cid -> lid1
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid1
sourceLogic cid
cid)
                    "translateG_theory" (sign
sign, ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens)
  (_, sens'' :: [Named sentence2]
sens'') <- cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
forall cid 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.
Comorphism
  cid
  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 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory cid
cid (sign1, [Named sentence1])
bTh
  [Named sentence2]
sens''' <- (Named sentence2 -> Result (Named sentence2))
-> [Named sentence2] -> Result [Named sentence2]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM ((sentence2 -> Result sentence2)
-> Named sentence2 -> Result (Named sentence2)
forall (m :: * -> *) s t.
Monad m =>
(s -> m t) -> Named s -> m (Named t)
mapNamedM ((sentence2 -> Result sentence2)
 -> Named sentence2 -> Result (Named sentence2))
-> (sentence2 -> Result sentence2)
-> Named sentence2
-> Result (Named sentence2)
forall a b. (a -> b) -> a -> b
$ lid2 -> morphism2 -> sentence2 -> Result sentence2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> sentence -> Result sentence
map_sen lid2
tlid morphism2
morphism2) [Named sentence2]
sens''
  G_theory -> Result G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> Result G_theory) -> G_theory -> Result G_theory
forall a b. (a -> b) -> a -> b
$ lid2
-> Maybe IRI
-> ExtSign sign2 symbol2
-> SigId
-> ThSens sentence2 (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid2
tlid Maybe IRI
forall a. Maybe a
Nothing (sign2 -> ExtSign sign2 symbol2
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign (sign2 -> ExtSign sign2 symbol2) -> sign2 -> ExtSign sign2 symbol2
forall a b. (a -> b) -> a -> b
$ morphism2 -> sign2
forall object morphism.
Category object morphism =>
morphism -> object
cod morphism2
morphism2)
             SigId
startSigId ([Named sentence2] -> ThSens sentence2 (AnyComorphism, BasicProof)
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named sentence2]
sens''') ThId
startThId

-- | Join the sentences of two G_theories
joinG_sentences :: Fail.MonadFail m => G_theory -> G_theory -> m G_theory
joinG_sentences :: G_theory -> G_theory -> m G_theory
joinG_sentences (G_theory lid1 :: lid
lid1 syn :: Maybe IRI
syn sig1 :: ExtSign sign symbol
sig1 ind :: SigId
ind sens1 :: ThSens sentence (AnyComorphism, BasicProof)
sens1 _)
                    (G_theory lid2 :: lid
lid2 _ sig2 :: ExtSign sign symbol
sig2 _ sens2 :: ThSens sentence (AnyComorphism, BasicProof)
sens2 _) = do
  ThSens sentence (AnyComorphism, BasicProof)
sens2' <- lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> m (ThSens sentence (AnyComorphism, BasicProof))
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 (m :: * -> *) b.
(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,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lid2 lid
lid1 "joinG_sentences" ThSens sentence (AnyComorphism, BasicProof)
sens2
  ExtSign sign symbol
sig2' <- lid
-> lid -> String -> ExtSign sign symbol -> m (ExtSign sign symbol)
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
lid2 lid
lid1 "joinG_sentences" ExtSign sign symbol
sig2
  G_theory -> m G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> m G_theory) -> G_theory -> m G_theory
forall a b. (a -> b) -> a -> b
$ Bool -> G_theory -> G_theory
forall a. (?callStack::CallStack) => Bool -> a -> a
assert (ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sig1 sign -> sign -> Bool
forall a. Eq a => a -> a -> Bool
== ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign sign symbol
sig2')
             (G_theory -> G_theory) -> G_theory -> G_theory
forall a b. (a -> b) -> a -> b
$ lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid1 Maybe IRI
syn ExtSign sign symbol
sig1 SigId
ind (ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
joinSens ThSens sentence (AnyComorphism, BasicProof)
sens1 ThSens sentence (AnyComorphism, BasicProof)
sens2') ThId
startThId

-- | Intersect the sentences of two G_theories, G_sign is the intersection of their signatures
intersectG_sentences :: Fail.MonadFail m => G_sign -> G_theory -> G_theory -> m G_theory
intersectG_sentences :: G_sign -> G_theory -> G_theory -> m G_theory
intersectG_sentences (G_sign lidS :: lid
lidS signS :: ExtSign sign symbol
signS indS :: SigId
indS)
                    (G_theory lid1 :: lid
lid1 _ _ _ sens1 :: ThSens sentence (AnyComorphism, BasicProof)
sens1 _)
                    (G_theory lid2 :: lid
lid2 _ _ _ sens2 :: ThSens sentence (AnyComorphism, BasicProof)
sens2 _) = do
  ThSens sentence (AnyComorphism, BasicProof)
sens1' <- lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> m (ThSens sentence (AnyComorphism, BasicProof))
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 (m :: * -> *) b.
(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,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lid1 lid
lidS "intersectG_sentences1" ThSens sentence (AnyComorphism, BasicProof)
sens1
  ThSens sentence (AnyComorphism, BasicProof)
sens2' <- lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> m (ThSens sentence (AnyComorphism, BasicProof))
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 (m :: * -> *) b.
(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,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lid2 lid
lidS "intersectG_sentences2" ThSens sentence (AnyComorphism, BasicProof)
sens2
  G_theory -> m G_theory
forall (m :: * -> *) a. Monad m => a -> m a
return (G_theory -> m G_theory) -> G_theory -> m G_theory
forall a b. (a -> b) -> a -> b
$ lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lidS Maybe IRI
forall a. Maybe a
Nothing ExtSign sign symbol
signS SigId
indS (ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (Ord a, Eq b) => ThSens a b -> ThSens a b -> ThSens a b
intersectSens ThSens sentence (AnyComorphism, BasicProof)
sens1' ThSens sentence (AnyComorphism, BasicProof)
sens2') ThId
startThId


-- | flattening the sentences form a list of G_theories
flatG_sentences :: Fail.MonadFail m => G_theory -> [G_theory] -> m G_theory
flatG_sentences :: G_theory -> [G_theory] -> m G_theory
flatG_sentences = (G_theory -> G_theory -> m G_theory)
-> G_theory -> [G_theory] -> m G_theory
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM G_theory -> G_theory -> m G_theory
forall (m :: * -> *).
MonadFail m =>
G_theory -> G_theory -> m G_theory
joinG_sentences

-- | Get signature of a theory
signOf :: G_theory -> G_sign
signOf :: G_theory -> G_sign
signOf (G_theory lid :: lid
lid _ sign :: ExtSign sign symbol
sign ind :: SigId
ind _ _) = lid -> ExtSign sign symbol -> SigId -> G_sign
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 -> SigId -> G_sign
G_sign lid
lid ExtSign sign symbol
sign SigId
ind

-- | create theory without sentences
noSensGTheory :: Logic lid sublogics basic_spec sentence symb_items
    symb_map_items sign morphism symbol raw_symbol proof_tree
    => lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory :: lid -> ExtSign sign symbol -> SigId -> G_theory
noSensGTheory lid :: lid
lid sig :: ExtSign sign symbol
sig si :: SigId
si = lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
forall a. Maybe a
Nothing ExtSign sign symbol
sig SigId
si ThSens sentence (AnyComorphism, BasicProof)
forall a b. ThSens a b
noSens ThId
startThId

data BasicProof =
  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 =>
        BasicProof lid (ProofStatus proof_tree)
     | Guessed
     | Conjectured
     | Handwritten
     deriving Typeable

instance Eq BasicProof where
  Guessed == :: BasicProof -> BasicProof -> Bool
== Guessed = Bool
True
  Conjectured == Conjectured = Bool
True
  Handwritten == Handwritten = Bool
True
  BasicProof lid1 :: lid
lid1 p1 :: ProofStatus proof_tree
p1 == BasicProof lid2 :: lid
lid2 p2 :: ProofStatus proof_tree
p2 =
    lid
-> lid
-> String
-> ProofStatus proof_tree
-> Maybe (ProofStatus proof_tree)
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ProofStatus proof_tree1
-> m (ProofStatus proof_tree2)
coerceProofStatus lid
lid1 lid
lid2 "Eq BasicProof" ProofStatus proof_tree
p1 Maybe (ProofStatus proof_tree)
-> Maybe (ProofStatus proof_tree) -> Bool
forall a. Eq a => a -> a -> Bool
== ProofStatus proof_tree -> Maybe (ProofStatus proof_tree)
forall a. a -> Maybe a
Just ProofStatus proof_tree
p2
  _ == _ = Bool
False

instance Ord BasicProof where
    Guessed <= :: BasicProof -> BasicProof -> Bool
<= _ = Bool
True
    Conjectured <= x :: BasicProof
x = case BasicProof
x of
                       Guessed -> Bool
False
                       _ -> Bool
True
    Handwritten <= x :: BasicProof
x = case BasicProof
x of
                       Guessed -> Bool
False
                       Conjectured -> Bool
False
                       _ -> Bool
True
    BasicProof lid1 :: lid
lid1 pst1 :: ProofStatus proof_tree
pst1 <= x :: BasicProof
x =
        case BasicProof
x of
        BasicProof lid2 :: lid
lid2 pst2 :: ProofStatus proof_tree
pst2
            | ProofStatus proof_tree -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
isProvedStat ProofStatus proof_tree
pst1 Bool -> Bool -> Bool
&& Bool -> Bool
not (ProofStatus proof_tree -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
isProvedStat ProofStatus proof_tree
pst2) -> Bool
False
            | Bool -> Bool
not (ProofStatus proof_tree -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
isProvedStat ProofStatus proof_tree
pst1) Bool -> Bool -> Bool
&& ProofStatus proof_tree -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
isProvedStat ProofStatus proof_tree
pst2 -> Bool
True
            | Bool
otherwise -> case lid
-> lid
-> String
-> ProofStatus proof_tree
-> Maybe (ProofStatus proof_tree)
forall a b lid1 lid2 (m :: * -> *).
(Typeable a, Typeable b, Language lid1, Language lid2,
 MonadFail m) =>
lid1 -> lid2 -> String -> a -> m b
primCoerce lid
lid1 lid
lid2 "" ProofStatus proof_tree
pst1 of
                           Nothing -> Bool
False
                           Just pst1' :: ProofStatus proof_tree
pst1' -> ProofStatus proof_tree
pst1' ProofStatus proof_tree -> ProofStatus proof_tree -> Bool
forall a. Ord a => a -> a -> Bool
<= ProofStatus proof_tree
pst2
        _ -> Bool
False

instance Show BasicProof where
  show :: BasicProof -> String
show (BasicProof _ p1 :: ProofStatus proof_tree
p1) = ProofStatus proof_tree -> String
forall a. Show a => a -> String
show ProofStatus proof_tree
p1
  show Guessed = "Guessed"
  show Conjectured = "Conjectured"
  show Handwritten = "Handwritten"

-- | test a theory sentence
isProvenSenStatus :: SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus :: SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus = ((AnyComorphism, BasicProof) -> Bool)
-> [(AnyComorphism, BasicProof)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (BasicProof -> Bool
isProvedBasically (BasicProof -> Bool)
-> ((AnyComorphism, BasicProof) -> BasicProof)
-> (AnyComorphism, BasicProof)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (AnyComorphism, BasicProof) -> BasicProof
forall a b. (a, b) -> b
snd) ([(AnyComorphism, BasicProof)] -> Bool)
-> (SenStatus a (AnyComorphism, BasicProof)
    -> [(AnyComorphism, BasicProof)])
-> SenStatus a (AnyComorphism, BasicProof)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SenStatus a (AnyComorphism, BasicProof)
-> [(AnyComorphism, BasicProof)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus

isProvedBasically :: BasicProof -> Bool
isProvedBasically :: BasicProof -> Bool
isProvedBasically b :: BasicProof
b = case BasicProof
b of
  BasicProof _ pst :: ProofStatus proof_tree
pst -> ProofStatus proof_tree -> Bool
forall proof_tree. ProofStatus proof_tree -> Bool
isProvedStat ProofStatus proof_tree
pst
  _ -> Bool
False

getValidAxioms
  :: G_theory -- ^ old global theory
  -> G_theory -- ^ new global theory
  -> [String] -- ^ unchanged axioms
getValidAxioms :: G_theory -> G_theory -> [String]
getValidAxioms
  (G_theory lid1 :: lid
lid1 _ _ _ sens1 :: ThSens sentence (AnyComorphism, BasicProof)
sens1 _)
  (G_theory lid2 :: lid
lid2 _ _ _ sens2 :: ThSens sentence (AnyComorphism, BasicProof)
sens2 _) =
  case lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
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 (m :: * -> *) b.
(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,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lid1 lid
lid2 "" ThSens sentence (AnyComorphism, BasicProof)
sens1 of
    Nothing -> []
    Just sens :: ThSens sentence (AnyComorphism, BasicProof)
sens -> ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall k a. Ord k => OMap k a -> [k]
OMap.keys (ThSens sentence (AnyComorphism, BasicProof) -> [String])
-> ThSens sentence (AnyComorphism, BasicProof) -> [String]
forall a b. (a -> b) -> a -> b
$ (String
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (k -> a -> Bool) -> OMap k a -> OMap k a
OMap.filterWithKey (\ k :: String
k s :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s ->
      case String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
forall (m :: * -> *) k a.
(MonadFail m, Ord k) =>
k -> OMap k a -> m a
OMap.lookup String
k ThSens sentence (AnyComorphism, BasicProof)
sens of
        Just s2 :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s2 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s Bool -> Bool -> Bool
&& SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s2 Bool -> Bool -> Bool
&& SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s sentence -> sentence -> Bool
forall a. Eq a => a -> a -> Bool
== SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s2
        _ -> Bool
False) ThSens sentence (AnyComorphism, BasicProof)
sens2

invalidateProofs
  :: G_theory -- ^ old global theory
  -> G_theory -- ^ new global theory
  -> G_theory -- ^ local theory with proven goals
  -> (Bool, G_theory) -- ^ no changes and new local theory with deleted proofs
invalidateProofs :: G_theory -> G_theory -> G_theory -> (Bool, G_theory)
invalidateProofs oTh :: G_theory
oTh nTh :: G_theory
nTh (G_theory lid :: lid
lid syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig si :: SigId
si sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) =
  let vAxs :: [String]
vAxs = G_theory -> G_theory -> [String]
getValidAxioms G_theory
oTh G_theory
nTh
      oAxs :: [String]
oAxs = ((String, Bool) -> String) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (String, Bool) -> String
forall a b. (a, b) -> a
fst ([(String, Bool)] -> [String]) -> [(String, Bool)] -> [String]
forall a b. (a -> b) -> a -> b
$ G_theory -> [(String, Bool)]
getThAxioms G_theory
oTh
      iValAxs :: [String]
iValAxs = [String]
vAxs [String] -> [String] -> [String]
forall a. Eq a => [a] -> [a] -> [a]
\\ [String]
oAxs
      validProofs :: (a, BasicProof) -> Bool
validProofs (_, bp :: BasicProof
bp) = case BasicProof
bp of
        BasicProof _ pst :: ProofStatus proof_tree
pst -> Bool -> Bool
not (Bool -> Bool) -> ([String] -> Bool) -> [String] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String -> Bool) -> [String] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (String -> [String] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [String]
iValAxs) ([String] -> Bool) -> [String] -> Bool
forall a b. (a -> b) -> a -> b
$ ProofStatus proof_tree -> [String]
forall proof_tree. ProofStatus proof_tree -> [String]
usedAxioms ProofStatus proof_tree
pst
        _ -> Bool
True
      newSens :: OMap
  String
  (Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
newSens = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
 -> (Bool,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))
-> ThSens sentence (AnyComorphism, BasicProof)
-> OMap
     String
     (Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map
        (\ s :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s -> if SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s then (Bool
True, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s) else
             let (ps :: [(AnyComorphism, BasicProof)]
ps, ups :: [(AnyComorphism, BasicProof)]
ups) = ((AnyComorphism, BasicProof) -> Bool)
-> [(AnyComorphism, BasicProof)]
-> ([(AnyComorphism, BasicProof)], [(AnyComorphism, BasicProof)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (AnyComorphism, BasicProof) -> Bool
forall a. (a, BasicProof) -> Bool
validProofs ([(AnyComorphism, BasicProof)]
 -> ([(AnyComorphism, BasicProof)], [(AnyComorphism, BasicProof)]))
-> [(AnyComorphism, BasicProof)]
-> ([(AnyComorphism, BasicProof)], [(AnyComorphism, BasicProof)])
forall a b. (a -> b) -> a -> b
$ SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s
             in ([(AnyComorphism, BasicProof)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(AnyComorphism, BasicProof)]
ups, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s { senAttr :: ThmStatus (AnyComorphism, BasicProof)
senAttr = [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a. [a] -> ThmStatus a
ThmStatus [(AnyComorphism, BasicProof)]
ps })) ThSens sentence (AnyComorphism, BasicProof)
sens
  in ( ((Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> Bool)
-> [(Bool,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> Bool
forall a b. (a, b) -> a
fst ([(Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
 -> Bool)
-> [(Bool,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> Bool
forall a b. (a -> b) -> a -> b
$ OMap
  String
  (Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> [(Bool,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall k a. Ord k => OMap k a -> [a]
OMap.elems OMap
  String
  (Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
newSens
     , lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
syn ExtSign sign symbol
sig SigId
si (((Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> OMap
     String
     (Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a b. Ord k => (a -> b) -> OMap k a -> OMap k b
OMap.map (Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall a b. (a, b) -> b
snd OMap
  String
  (Bool, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
newSens) ThId
startThId)

{- | mark sentences as proven if an identical axiom or other proven sentence
     is part of the same theory. -}
proveSens :: Logic lid sublogics basic_spec sentence symb_items
    symb_map_items sign morphism symbol raw_symbol proof_tree
    => lid -> ThSens sentence (AnyComorphism, BasicProof)
           -> ThSens sentence (AnyComorphism, BasicProof)
proveSens :: lid
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
proveSens lid :: lid
lid sens :: ThSens sentence (AnyComorphism, BasicProof)
sens = let
  (axs :: ThSens sentence (AnyComorphism, BasicProof)
axs, ths :: ThSens sentence (AnyComorphism, BasicProof)
ths) = (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> (ThSens sentence (AnyComorphism, BasicProof),
    ThSens sentence (AnyComorphism, BasicProof))
forall k a.
Ord k =>
(a -> Bool) -> OMap k a -> (OMap k a, OMap k a)
OMap.partition (\ s :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s Bool -> Bool -> Bool
|| SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s) ThSens sentence (AnyComorphism, BasicProof)
sens
  in ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union ThSens sentence (AnyComorphism, BasicProof)
axs (ThSens sentence (AnyComorphism, BasicProof)
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ lid
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
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
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
proveSensAux lid
lid ThSens sentence (AnyComorphism, BasicProof)
axs ThSens sentence (AnyComorphism, BasicProof)
ths

proveLocalSens :: G_theory -> G_theory -> G_theory
proveLocalSens :: G_theory -> G_theory -> G_theory
proveLocalSens (G_theory glid :: lid
glid _ _ _ gsens :: ThSens sentence (AnyComorphism, BasicProof)
gsens _)
  lth :: G_theory
lth@(G_theory lid :: lid
lid syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig ind :: SigId
ind sens :: ThSens sentence (AnyComorphism, BasicProof)
sens _) =
  case lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
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 (m :: * -> *) b.
(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,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
glid lid
lid "proveLocalSens" ThSens sentence (AnyComorphism, BasicProof)
gsens of
    Just lsens :: ThSens sentence (AnyComorphism, BasicProof)
lsens -> lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid Maybe IRI
syn ExtSign sign symbol
sig SigId
ind
      (lid
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
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
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
proveSensAux lid
lid ((SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => (a -> Bool) -> OMap k a -> OMap k a
OMap.filter (\ s :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s -> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall s a. SenAttr s a -> Bool
isAxiom SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s Bool -> Bool -> Bool
|| SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)) -> Bool
forall a. SenStatus a (AnyComorphism, BasicProof) -> Bool
isProvenSenStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s)
       ThSens sentence (AnyComorphism, BasicProof)
lsens) ThSens sentence (AnyComorphism, BasicProof)
sens) ThId
startThId
    Nothing -> G_theory
lth

{- | mark sentences as proven if an identical axiom or other proven sentence
     is part of a given global theory. -}
proveSensAux :: Logic lid sublogics basic_spec sentence symb_items
    symb_map_items sign morphism symbol raw_symbol proof_tree
    => lid -> ThSens sentence (AnyComorphism, BasicProof)
           -> ThSens sentence (AnyComorphism, BasicProof)
           -> ThSens sentence (AnyComorphism, BasicProof)
proveSensAux :: lid
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
proveSensAux lid :: lid
lid axs :: ThSens sentence (AnyComorphism, BasicProof)
axs ths :: ThSens sentence (AnyComorphism, BasicProof)
ths = let
  axSet :: Map sentence String
axSet = [(sentence, String)] -> Map sentence String
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(sentence, String)] -> Map sentence String)
-> [(sentence, String)] -> Map sentence String
forall a b. (a -> b) -> a -> b
$ ((String, SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> (sentence, String))
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [(sentence, String)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: String
n, s :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s) -> (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
s, String
n)) ([(String,
   SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
 -> [(sentence, String)])
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
-> [(sentence, String)]
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> [(String,
     SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))]
forall k a. Ord k => OMap k a -> [(k, a)]
OMap.toList ThSens sentence (AnyComorphism, BasicProof)
axs
  in (String
 -> ElemWOrd
      (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
 -> ElemWOrd
      (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a b. (k -> a -> b) -> Map k a -> Map k b
Map.mapWithKey (\ i :: String
i e :: ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
e -> let sen :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen = ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
-> SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
forall a. ElemWOrd a -> a
OMap.ele ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
e in
         case sentence -> Map sentence String -> Maybe String
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> sentence
forall s a. SenAttr s a -> s
sentence SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen) Map sentence String
axSet of
           Just ax :: String
ax ->
             ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
e { ele :: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
OMap.ele = SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen { senAttr :: ThmStatus (AnyComorphism, BasicProof)
senAttr = [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a. [a] -> ThmStatus a
ThmStatus ([(AnyComorphism, BasicProof)]
 -> ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
-> ThmStatus (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$
                   ( InclComorphism lid sublogics -> AnyComorphism
forall cid 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.
Comorphism
  cid
  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 =>
cid -> AnyComorphism
Comorphism (InclComorphism lid sublogics -> AnyComorphism)
-> InclComorphism lid sublogics -> AnyComorphism
forall a b. (a -> b) -> a -> b
$ lid -> sublogics -> InclComorphism lid sublogics
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 -> sublogics -> InclComorphism lid sublogics
mkIdComorphism lid
lid (sublogics -> InclComorphism lid sublogics)
-> sublogics -> InclComorphism lid sublogics
forall a b. (a -> b) -> a -> b
$ lid -> sublogics
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 -> sublogics
top_sublogic lid
lid
                   , lid -> ProofStatus proof_tree -> BasicProof
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 -> ProofStatus proof_tree -> BasicProof
BasicProof lid
lid
                     (String -> String -> proof_tree -> ProofStatus proof_tree
forall pt. Ord pt => String -> String -> pt -> ProofStatus pt
openProofStatus String
i "hets" (proof_tree -> ProofStatus proof_tree)
-> proof_tree -> ProofStatus proof_tree
forall a b. (a -> b) -> a -> b
$ lid -> proof_tree
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 -> proof_tree
empty_proof_tree lid
lid)
                     { usedAxioms :: [String]
usedAxioms = [String
ax]
                     , goalStatus :: GoalStatus
goalStatus = Bool -> GoalStatus
Proved Bool
True }) (AnyComorphism, BasicProof)
-> [(AnyComorphism, BasicProof)] -> [(AnyComorphism, BasicProof)]
forall a. a -> [a] -> [a]
: SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
-> [(AnyComorphism, BasicProof)]
forall a tStatus. SenStatus a tStatus -> [tStatus]
thmStatus SenAttr sentence (ThmStatus (AnyComorphism, BasicProof))
sen } }
           _ -> ElemWOrd (SenAttr sentence (ThmStatus (AnyComorphism, BasicProof)))
e) ThSens sentence (AnyComorphism, BasicProof)
ths

{- | mark all sentences of a local theory that have been proven via a prover
over a global theory (with the same signature) as proven.  Also mark
duplicates of proven sentences as proven.  Assume that the sentence names of
the local theory are identical to the global theory. -}
propagateProofs :: G_theory -> G_theory -> G_theory
propagateProofs :: G_theory -> G_theory -> G_theory
propagateProofs locTh :: G_theory
locTh@(G_theory lid1 :: lid
lid1 syn :: Maybe IRI
syn sig :: ExtSign sign symbol
sig ind :: SigId
ind lsens :: ThSens sentence (AnyComorphism, BasicProof)
lsens _)
  (G_theory lid2 :: lid
lid2 _ _ _ gsens :: ThSens sentence (AnyComorphism, BasicProof)
gsens _) =
  case lid
-> lid
-> String
-> ThSens sentence (AnyComorphism, BasicProof)
-> Maybe (ThSens sentence (AnyComorphism, BasicProof))
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 (m :: * -> *) b.
(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,
 MonadFail m, Typeable b) =>
lid1
-> lid2 -> String -> ThSens sentence1 b -> m (ThSens sentence2 b)
coerceThSens lid
lid2 lid
lid1 "" ThSens sentence (AnyComorphism, BasicProof)
gsens of
    Just ps :: ThSens sentence (AnyComorphism, BasicProof)
ps ->
      if ThSens sentence (AnyComorphism, BasicProof) -> Bool
forall k a. Map k a -> Bool
Map.null ThSens sentence (AnyComorphism, BasicProof)
ps then G_theory
locTh else
          lid
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
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
-> Maybe IRI
-> ExtSign sign symbol
-> SigId
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThId
-> G_theory
G_theory lid
lid1 Maybe IRI
syn ExtSign sign symbol
sig SigId
ind
            (lid
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
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
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
proveSens lid
lid1 (ThSens sentence (AnyComorphism, BasicProof)
 -> ThSens sentence (AnyComorphism, BasicProof))
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall a b. (a -> b) -> a -> b
$ ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union (ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
-> ThSens sentence (AnyComorphism, BasicProof)
forall k a b. Ord k => Map k a -> Map k b -> Map k a
Map.intersection ThSens sentence (AnyComorphism, BasicProof)
ps ThSens sentence (AnyComorphism, BasicProof)
lsens) ThSens sentence (AnyComorphism, BasicProof)
lsens)
            ThId
startThId
    Nothing -> String -> G_theory
forall a. (?callStack::CallStack) => String -> a
error "propagateProofs"

-- | Grothendieck diagrams
type GDiagram = Gr G_theory (Int, GMorphism)

-- | checks whether a connected GDiagram is homogeneous

isHomogeneousGDiagram :: GDiagram -> Bool
isHomogeneousGDiagram :: GDiagram -> Bool
isHomogeneousGDiagram = ((Int, Int, (Int, GMorphism)) -> Bool)
-> [(Int, Int, (Int, GMorphism))] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (\ (_, _, (_, phi :: GMorphism
phi)) -> GMorphism -> Bool
isHomogeneous GMorphism
phi) ([(Int, Int, (Int, GMorphism))] -> Bool)
-> (GDiagram -> [(Int, Int, (Int, GMorphism))]) -> GDiagram -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GDiagram -> [(Int, Int, (Int, GMorphism))]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges

-- | homogenise a GDiagram to a targeted logic

homogeniseGDiagram :: Logic lid sublogics
                           basic_spec sentence symb_items symb_map_items
                           sign morphism symbol raw_symbol proof_tree
                  => lid     -- ^ the target logic to be coerced to
                  -> GDiagram    -- ^ the GDiagram to be homogenised
                  -> Result (Gr sign (Int, morphism))

homogeniseGDiagram :: lid -> GDiagram -> Result (Gr sign (Int, morphism))
homogeniseGDiagram targetLid :: lid
targetLid diag :: GDiagram
diag = do
  let convertNode :: (a, G_theory) -> m (a, b)
convertNode (n :: a
n, gth :: G_theory
gth) = do
       G_sign srcLid :: lid
srcLid extSig :: ExtSign sign symbol
extSig _ <- G_sign -> m G_sign
forall (m :: * -> *) a. Monad m => a -> m a
return (G_sign -> m G_sign) -> G_sign -> m G_sign
forall a b. (a -> b) -> a -> b
$ G_theory -> G_sign
signOf G_theory
gth
       ExtSign b symbol
extSig' <- lid -> lid -> String -> ExtSign sign symbol -> m (ExtSign b symbol)
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1
-> lid2
-> String
-> ExtSign sign1 symbol1
-> m (ExtSign sign2 symbol2)
coerceSign lid
srcLid lid
targetLid "" ExtSign sign symbol
extSig
       (a, b) -> m (a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n, ExtSign b symbol -> b
forall sign symbol. ExtSign sign symbol -> sign
plainSign ExtSign b symbol
extSig')
      convertEdge :: (a, b, (a, GMorphism)) -> m (a, b, (a, b))
convertEdge (n1 :: a
n1, n2 :: b
n2, (nr :: a
nr, GMorphism cid :: cid
cid _ _ mor :: morphism2
mor _ ))
        = if AnyComorphism -> Bool
isIdComorphism (cid -> AnyComorphism
forall cid 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.
Comorphism
  cid
  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 =>
cid -> AnyComorphism
Comorphism cid
cid) then
            do b
mor' <- lid2 -> lid -> String -> morphism2 -> m b
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1 -> lid2 -> String -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid) lid
targetLid "" morphism2
mor
               (a, b, (a, b)) -> m (a, b, (a, b))
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n1, b
n2, (a
nr, b
mor'))
          else String -> m (a, b, (a, b))
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (a, b, (a, b))) -> String -> m (a, b, (a, b))
forall a b. (a -> b) -> a -> b
$
               "Trying to coerce a morphism between different logics.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
               "Heterogeneous specifications are not fully supported yet."
      convertNodes :: gr b b -> [(Int, G_theory)] -> m (gr b b)
convertNodes cDiag :: gr b b
cDiag [] = gr b b -> m (gr b b)
forall (m :: * -> *) a. Monad m => a -> m a
return gr b b
cDiag
      convertNodes cDiag :: gr b b
cDiag (lNode :: (Int, G_theory)
lNode : lNodes :: [(Int, G_theory)]
lNodes) = do
                  (Int, b)
convNode <- (Int, G_theory) -> m (Int, b)
forall (m :: * -> *) sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 b morphism2 symbol raw_symbol2 proof_tree2 a.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   b
   morphism2
   symbol
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
(a, G_theory) -> m (a, b)
convertNode (Int, G_theory)
lNode
                  let cDiag' :: gr b b
cDiag' = (Int, b) -> gr b b -> gr b b
forall (gr :: * -> * -> *) a b.
DynGraph gr =>
LNode a -> gr a b -> gr a b
insNode (Int, b)
convNode gr b b
cDiag
                  gr b b -> [(Int, G_theory)] -> m (gr b b)
convertNodes gr b b
cDiag' [(Int, G_theory)]
lNodes
      convertEdges :: gr a (a, b) -> [(Int, Int, (a, GMorphism))] -> m (gr a (a, b))
convertEdges cDiag :: gr a (a, b)
cDiag [] = gr a (a, b) -> m (gr a (a, b))
forall (m :: * -> *) a. Monad m => a -> m a
return gr a (a, b)
cDiag
      convertEdges cDiag :: gr a (a, b)
cDiag (lEdge :: (Int, Int, (a, GMorphism))
lEdge : lEdges :: [(Int, Int, (a, GMorphism))]
lEdges) = do
                  (Int, Int, (a, b))
convEdge <- (Int, Int, (a, GMorphism)) -> m (Int, Int, (a, b))
forall sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 b symbol2 raw_symbol2 proof_tree2 (m :: * -> *) a b a.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   b
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
(a, b, (a, GMorphism)) -> m (a, b, (a, b))
convertEdge (Int, Int, (a, GMorphism))
lEdge
                  let cDiag' :: gr a (a, b)
cDiag' = (Int, Int, (a, b)) -> gr a (a, b) -> gr a (a, b)
forall (gr :: * -> * -> *) b a.
DynGraph gr =>
LEdge b -> gr a b -> gr a b
insEdge (Int, Int, (a, b))
convEdge gr a (a, b)
cDiag
                  gr a (a, b) -> [(Int, Int, (a, GMorphism))] -> m (gr a (a, b))
convertEdges gr a (a, b)
cDiag' [(Int, Int, (a, GMorphism))]
lEdges
      dNodes :: [(Int, G_theory)]
dNodes = GDiagram -> [(Int, G_theory)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GDiagram
diag
      dEdges :: [(Int, Int, (Int, GMorphism))]
dEdges = GDiagram -> [(Int, Int, (Int, GMorphism))]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
labEdges GDiagram
diag
       -- insert converted nodes to an empty diagram
  Gr sign (Int, morphism)
cDiag <- Gr sign (Int, morphism)
-> [(Int, G_theory)] -> Result (Gr sign (Int, morphism))
forall (m :: * -> *) sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 b morphism2 symbol raw_symbol2 proof_tree2
       (gr :: * -> * -> *) b.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   b
   morphism2
   symbol
   raw_symbol2
   proof_tree2,
 MonadFail m, DynGraph gr) =>
gr b b -> [(Int, G_theory)] -> m (gr b b)
convertNodes Gr sign (Int, morphism)
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
Graph.empty [(Int, G_theory)]
dNodes
       -- insert converted edges to the diagram containing only nodes
  Gr sign (Int, morphism)
-> [(Int, Int, (Int, GMorphism))]
-> Result (Gr sign (Int, morphism))
forall (m :: * -> *) sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 b symbol2 raw_symbol2 proof_tree2
       (gr :: * -> * -> *) a a.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   b
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m, DynGraph gr) =>
gr a (a, b) -> [(Int, Int, (a, GMorphism))] -> m (gr a (a, b))
convertEdges Gr sign (Int, morphism)
cDiag [(Int, Int, (Int, GMorphism))]
dEdges

{- | Coerce GMorphisms in the list of (diagram node, GMorphism) pairs
to morphisms in given logic -}
homogeniseSink :: Logic lid sublogics
                         basic_spec sentence symb_items symb_map_items
                         sign morphism symbol raw_symbol proof_tree
                => lid -- ^ the target logic to which morphisms will be coerced
                -> [(Node, GMorphism)] -- ^ the list of edges to be homogenised
                -> Result [(Node, morphism)]
homogeniseSink :: lid -> [(Int, GMorphism)] -> Result [(Int, morphism)]
homogeniseSink targetLid :: lid
targetLid dEdges :: [(Int, GMorphism)]
dEdges =
     -- See homogeniseDiagram for comments on implementation.
       let convertMorphism :: (a, GMorphism) -> m (a, b)
convertMorphism (n :: a
n, GMorphism cid :: cid
cid _ _ mor :: morphism2
mor _) =
               if AnyComorphism -> Bool
isIdComorphism (cid -> AnyComorphism
forall cid 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.
Comorphism
  cid
  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 =>
cid -> AnyComorphism
Comorphism cid
cid) then
                  do b
mor' <- lid2 -> lid -> String -> morphism2 -> m b
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 (m :: * -> *).
(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,
 MonadFail m) =>
lid1 -> lid2 -> String -> morphism1 -> m morphism2
coerceMorphism (cid -> lid2
forall cid 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.
Comorphism
  cid
  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 =>
cid -> lid2
targetLogic cid
cid) lid
targetLid "" morphism2
mor
                     (a, b) -> m (a, b)
forall (m :: * -> *) a. Monad m => a -> m a
return (a
n, b
mor')
               else String -> m (a, b)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> m (a, b)) -> String -> m (a, b)
forall a b. (a -> b) -> a -> b
$
               "Trying to coerce a morphism between different logics.\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                "Heterogeneous specifications are not fully supported yet."
           convEdges :: [(a, GMorphism)] -> m [(a, b)]
convEdges [] = [(a, b)] -> m [(a, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return []
           convEdges (e :: (a, GMorphism)
e : es :: [(a, GMorphism)]
es) = do
             (a, b)
ce <- (a, GMorphism) -> m (a, b)
forall sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 b symbol2 raw_symbol2 proof_tree2 (m :: * -> *) a.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   b
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
(a, GMorphism) -> m (a, b)
convertMorphism (a, GMorphism)
e
             [(a, b)]
ces <- [(a, GMorphism)] -> m [(a, b)]
convEdges [(a, GMorphism)]
es
             [(a, b)] -> m [(a, b)]
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, b)
ce (a, b) -> [(a, b)] -> [(a, b)]
forall a. a -> [a] -> [a]
: [(a, b)]
ces)
       in [(Int, GMorphism)] -> Result [(Int, morphism)]
forall (m :: * -> *) sublogics2 basic_spec2 sentence2 symb_items2
       symb_map_items2 sign2 b symbol2 raw_symbol2 proof_tree2 a.
(Logic
   lid
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   b
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
[(a, GMorphism)] -> m [(a, b)]
convEdges [(Int, GMorphism)]
dEdges


{- amalgamabilty check for heterogeneous diagrams
currently only checks whether the diagram is
homogeneous and if so, calls amalgamability check
for the specific logic -}

gEnsuresAmalgamability :: [CASLAmalgOpt] -- the options
                       -> GDiagram -- the diagram
                       -> [(Int, GMorphism)] -- the sink
                       -> Result Amalgamates
gEnsuresAmalgamability :: [CASLAmalgOpt]
-> GDiagram -> [(Int, GMorphism)] -> Result Amalgamates
gEnsuresAmalgamability options :: [CASLAmalgOpt]
options gd :: GDiagram
gd sink :: [(Int, GMorphism)]
sink =
  if GDiagram -> Bool
isHomogeneousGDiagram GDiagram
gd Bool -> Bool -> Bool
&& ((Int, GMorphism) -> Bool) -> [(Int, GMorphism)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all (GMorphism -> Bool
isHomogeneous (GMorphism -> Bool)
-> ((Int, GMorphism) -> GMorphism) -> (Int, GMorphism) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, GMorphism) -> GMorphism
forall a b. (a, b) -> b
snd) [(Int, GMorphism)]
sink then
      case GDiagram -> [(Int, G_theory)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
labNodes GDiagram
gd of
       (_, G_theory lid :: lid
lid _ _ _ _ _) : _ -> do
          Gr sign (Int, morphism)
diag <- lid -> GDiagram -> Result (Gr sign (Int, morphism))
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 -> GDiagram -> Result (Gr sign (Int, morphism))
homogeniseGDiagram lid
lid GDiagram
gd
          [(Int, morphism)]
sink' <- lid -> [(Int, GMorphism)] -> Result [(Int, morphism)]
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 -> [(Int, GMorphism)] -> Result [(Int, morphism)]
homogeniseSink lid
lid [(Int, GMorphism)]
sink
          lid
-> ([CASLAmalgOpt], Gr sign (Int, morphism), [(Int, morphism)],
    Gr String String)
-> Result Amalgamates
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> ([CASLAmalgOpt], Gr sign (Int, morphism), [(Int, morphism)],
    Gr String String)
-> Result Amalgamates
ensures_amalgamability lid
lid ([CASLAmalgOpt]
options, Gr sign (Int, morphism)
diag, [(Int, morphism)]
sink', Gr String String
forall (gr :: * -> * -> *) a b. Graph gr => gr a b
Graph.empty)
       _ -> String -> Result Amalgamates
forall a. (?callStack::CallStack) => String -> a
error "heterogeneous amalgability check: no nodes"
    else String -> Result Amalgamates
forall a. (?callStack::CallStack) => String -> a
error "heterogeneous amalgability check not yet implemented"