Grothendieck.hs revision 1d581e55c7ec020a445684310394c3a5fc056e96
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiModule : $Header$
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiDescription : Grothendieck logic (flattening of logic graph to a single logic)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiCopyright : (c) Till Mossakowski, and Uni Bremen 2002-2006
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiMaintainer : till@informatik.uni-bremen.de
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiStability : provisional
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiPortability : non-portable (overlapping instances, dynamics, existentials)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiGrothendieck logic (flattening of logic graph to a single logic)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiThe Grothendieck logic is defined to be the
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai heterogeneous logic over the logic graph.
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai This will be the logic over which the data
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai structures and algorithms for specification in-the-large
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai are built.
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai This module heavily works with existential types, see
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai <http://haskell.org/hawiki/ExistentialTypes> and chapter 7 of /Heterogeneous
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai specification and the heterogeneous tool set/
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (<http://www.informatik.uni-bremen.de/~till/papers/habil.ps>).
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai References:
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi R. Diaconescu:
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Grothendieck institutions
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai J. applied categorical structures 10, 2002, p. 383-402.
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai T. Mossakowski:
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Comorphism-based Grothendieck institutions.
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai In K. Diks, W. Rytter (Eds.), Mathematical foundations of computer science,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai LNCS 2420, pp. 593-604
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai T. Mossakowski:
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Heterogeneous specification and the heterogeneous tool set.
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Transportability for heterogeneous morphisms -solved
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi G_basic_spec (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_sign (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , isHomSubGsign
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , langNameSig
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_sign_list (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_ext_sign (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_symbol (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_symb_items_list (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_symb_map_items_list (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_diagram (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_sublogics (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , isProperSublogic
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_morphism (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , AnyComorphism (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , idComorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , isIdComorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , isInclComorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , isModelTransportable
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , hasModelExpansion
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , isWeaklyAmalgamable
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , compComorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , lessSublogicComor
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , AnyMorphism (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , AnyModification (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , idModification
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , vertCompModification
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , horCompModification
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , LogicGraph (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , emptyLogicGraph
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , HetSublogicGraph (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , emptyHetSublogicGraph
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , lookupLogic
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , lookupCompComorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , lookupComorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , lookupModification
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , GMorphism (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , isHomogeneous
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , Grothendieck (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , gEmbedComorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , homogeneousGsigUnion
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , gsigManyUnion
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , homogeneousMorManyUnion
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , logicInclusion
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , updateMorIndex
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , toG_morphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , compInclusion
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , compHomInclusion
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , findComorphismPaths
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , findComorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , isTransportable
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_prover (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , getProverName
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , coerceProver
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , G_cons_checker (..)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , coerceConsChecker
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , coerceG_sign
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiimport qualified Common.Lib.Graph as Tree
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiimport qualified Data.Map as Map
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiimport qualified Data.Set as Set
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiimport Data.Maybe (catMaybes)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiimport Control.Monad (foldM, unless)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiimport Text.ParserCombinators.Parsec (Parser, try, parse, eof, char, (<|>))
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- for looking up modifications
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- * \"Grothendieck\" versions of the various parts of type class Logic
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | Grothendieck basic specifications
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata G_basic_spec = forall lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree .
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Logic lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree =>
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi G_basic_spec lid basic_spec
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Show G_basic_spec where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi show (G_basic_spec _ s) = show s
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Pretty G_basic_spec where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi pretty (G_basic_spec _ s) = pretty s
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi{- | Grothendieck signatures with an lookup index. Zero indices
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi indicate unknown ones. It would be nice to have special (may be
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi negative) indices for empty signatures (one for every logic). -}
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata G_sign = forall lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree .
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Logic lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree => G_sign
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi { gSignLogic :: lid
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , gSign :: sign
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi , gSignSelfIdx :: Int -- ^ index to lookup this 'G_sign' in sign map
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchityconG_sign :: TyCon
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchityconG_sign = mkTyCon "Logic.Grothendieck.G_sign"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Typeable G_sign where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi typeOf _ = mkTyConApp tyconG_sign []
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Eq G_sign where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi G_sign l1 sigma1 i1 == G_sign l2 sigma2 i2 =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (i1 > 0 && i2 > 0 && i1 == i2) ||
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi coerceSign l1 l2 "Eq G_sign" sigma1 == Just sigma2
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | prefer a faster subsignature test if possible
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiisHomSubGsign :: G_sign -> G_sign -> Bool
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiisHomSubGsign (G_sign i1 sigma1 s1) (G_sign i2 sigma2 s2) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi if s1 == s2 then True else
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi maybe False (is_subsig i1 sigma1) $ coerceSign i2 i1 "is_subgsign" sigma2
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiisSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiisSubGsign lg (G_sign lid1 sigma1 _) (G_sign lid2 sigma2 _) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi do Comorphism cid <- resultToMaybe $
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi logicInclusion lg (Logic lid1) (Logic lid2)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sigma1' <- coerceSign lid1 (sourceLogic cid)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi "Grothendieck.isSubGsign: cannot happen" sigma1
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sigma2' <- coerceSign lid2 (targetLogic cid)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi "Grothendieck.isSubGsign: cannot happen" sigma2
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sigma1t <- resultToMaybe $ map_sign cid sigma1'
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return $ is_subsig (targetLogic cid) (fst sigma1t) sigma2'
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Show G_sign where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi show (G_sign _ s _) = show s
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Pretty G_sign where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi pretty (G_sign _ s _) = pretty s
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchilangNameSig :: G_sign -> String
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchilangNameSig (G_sign lid _ _) = language_name lid
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | Grothendieck signature lists
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata G_sign_list = forall lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree .
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Logic lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree =>
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi G_sign_list lid [sign]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | Grothendieck extended signatures
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata G_ext_sign = forall lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree .
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Logic lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree =>
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi G_ext_sign lid sign (Set.Set symbol)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | Grothendieck symbols
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata G_symbol = forall lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree .
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Logic lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree =>
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi G_symbol lid symbol
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Show G_symbol where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi show (G_symbol _ s) = show s
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Pretty G_symbol where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi pretty (G_symbol _ s) = pretty s
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Eq G_symbol where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (G_symbol i1 s1) == (G_symbol i2 s2) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi language_name i1 == language_name i2 && coerceSymbol i1 i2 s1 == s2
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | Grothendieck symbol lists
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata G_symb_items_list = forall lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree .
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Logic lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree =>
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi G_symb_items_list lid [symb_items]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Show G_symb_items_list where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi show (G_symb_items_list _ l) = show l
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Pretty G_symb_items_list where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi pretty (G_symb_items_list _ l) = ppWithCommas l
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Eq G_symb_items_list where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi coerceSymbItemsList i1 i2 "Eq G_symb_items_list" s1 == Just s2
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | Grothendieck symbol maps
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata G_symb_map_items_list = forall lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree .
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Logic lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree =>
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi G_symb_map_items_list lid [symb_map_items]
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Show G_symb_map_items_list where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi show (G_symb_map_items_list _ l) = show l
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Pretty G_symb_map_items_list where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi pretty (G_symb_map_items_list _ l) = ppWithCommas l
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiinstance Eq G_symb_map_items_list where
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi coerceSymbMapItemsList i1 i2 "Eq G_symb_map_items_list" s1 == Just s2
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | Grothendieck diagrams
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchidata G_diagram = forall lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sign morphism symbol raw_symbol proof_tree .
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi Logic lid sublogics
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi basic_spec sentence symb_items symb_map_items
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign morphism symbol raw_symbol proof_tree =>
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai G_diagram lid (Tree.Gr sign morphism)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Grothendieck sublogics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata G_sublogics = forall lid sublogics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec sentence symb_items symb_map_items
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign morphism symbol raw_symbol proof_tree .
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Logic lid sublogics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec sentence symb_items symb_map_items
aa59c4cb15a6ac5d4e585dadf7a055b580abf579rsb sign morphism symbol raw_symbol proof_tree =>
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai G_sublogics lid sublogics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaityconG_sublogics :: TyCon
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaityconG_sublogics = mkTyCon "Logic.Grothendieck.G_sublogics"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Typeable G_sublogics where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai typeOf _ = mkTyConApp tyconG_sublogics []
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Show G_sublogics where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai show (G_sublogics lid sub) = case sublogic_names sub of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai [] -> error "show G_sublogics"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai h : _ -> show lid ++ (if null h then "" else "." ++ h)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Eq G_sublogics where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai g1 == g2 = compare g1 g2 == EQ
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Ord G_sublogics where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai compare (G_sublogics lid1 l1) (G_sublogics lid2 l2) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai case compare (language_name lid1) $ language_name lid2 of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai EQ -> compare (forceCoerceSublogic lid1 lid2 l1) l2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisProperSublogic :: G_sublogics -> G_sublogics -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisProperSublogic a@(G_sublogics lid1 l1) b@(G_sublogics lid2 l2) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai isSubElem (forceCoerceSublogic lid1 lid2 l1) l2 && a /= b
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai{- | Homogeneous Grothendieck signature morphisms with indices. For
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaithe domain index it would be nice it showed also the emptiness. -}
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata G_morphism = forall lid sublogics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec sentence symb_items symb_map_items
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign morphism symbol raw_symbol proof_tree .
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Logic lid sublogics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec sentence symb_items symb_map_items
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign morphism symbol raw_symbol proof_tree => G_morphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai { gMorphismLogic :: lid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , gMorphismSelfIdx :: Int -- ^ lookup index in morphism map
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , gMorphism :: morphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , gMorphismDomIdx :: Int -- ^ 'G_sign' index of domain
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , gMorphismCodIdx :: Int -- ^ 'G_sign' index of codomain
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Show G_morphism where
681d9761e8516a7dc5ab6589e2dfe717777e1123Eric Taylor show (G_morphism _ _ l _ _) = show l
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- * Comorphisms and existential types for the logic graph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Existential type for comorphisms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata AnyComorphism = forall cid lid1 sublogics1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec1 sentence1 symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid2 sublogics2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec2 sentence2 symb_items2 symb_map_items2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Comorphism cid
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid1 sublogics1 basic_spec1 sentence1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid2 sublogics2 basic_spec2 sentence2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai symb_items2 symb_map_items2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Comorphism cid
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwinstance Eq AnyComorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Comorphism cid1 == Comorphism cid2 =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai constituents cid1 == constituents cid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -- need to be refined, using comorphism translations !!!
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Show AnyComorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai show (Comorphism cid) = language_name cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ++ " : " ++ language_name (sourceLogic cid)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ++ " -> " ++ language_name (targetLogic cid)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaityconAnyComorphism :: TyCon
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaityconAnyComorphism = mkTyCon "Logic.Grothendieck.AnyComorphism"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Typeable AnyComorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai typeOf _ = mkTyConApp tyconAnyComorphism []
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | compute the identity comorphism for a logic
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiidComorphism :: AnyLogic -> AnyComorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiidComorphism (Logic lid) = Comorphism (mkIdComorphism lid (top_sublogic lid))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Test whether a comporphism is the identity
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisIdComorphism :: AnyComorphism -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisIdComorphism (Comorphism cid) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai constituents cid == []
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Test wether a comorphism is an ad-hoc inclusion
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisInclComorphism :: AnyComorphism -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisInclComorphism (Comorphism cid) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Logic (sourceLogic cid) == Logic (targetLogic cid) &&
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (isProperSublogic (G_sublogics (sourceLogic cid) (sourceSublogic cid))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (G_sublogics (targetLogic cid) (targetSublogic cid)))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- * Properties of comorphisms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Test whether a comorphism is model-transportable
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisModelTransportable :: AnyComorphism -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisModelTransportable (Comorphism cid) = is_model_transportable cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Test whether a comorphism has model expansion
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaihasModelExpansion :: AnyComorphism -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaihasModelExpansion (Comorphism cid) = has_model_expansion cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Test whether a comorphism is weakly amalgamable
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwisWeaklyAmalgamable :: AnyComorphism -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisWeaklyAmalgamable (Comorphism cid) = is_weakly_amalgamable cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Compose comorphisms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicompComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicompComorphism (Comorphism cid1) (Comorphism cid2) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let l1 = targetLogic cid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai l2 = sourceLogic cid2 in
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if language_name l1 == language_name l2 then
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ sourceSublogic cid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai then {- case (isIdComorphism cm1,isIdComorphism cm2) of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (True,_) -> return cm2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (_,True) -> return cm1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> -} return $ Comorphism (CompComorphism cid1 cid2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else fail ("Sublogic mismatch in composition of "++language_name cid1++
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai " and "++language_name cid2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else fail ("Logic mismatch in composition of "++language_name cid1++
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai " and "++language_name cid2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | check if sublogic fits for comorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailessSublogicComor (G_sublogics lid1 sub1) (Comorphism cid) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let lid2 = sourceLogic cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai in language_name lid2 == language_name lid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai && isSubElem (forceCoerceSublogic lid1 lid2 sub1) (sourceSublogic cid)
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- * Morphisms
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- | Existential type for morphisms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata AnyMorphism = forall cid lid1 sublogics1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec1 sentence1 symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid2 sublogics2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec2 sentence2 symb_items2 symb_map_items2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Morphism cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid1 sublogics1 basic_spec1 sentence1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw lid2 sublogics2 basic_spec2 sentence2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai symb_items2 symb_map_items2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Morphism cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Eq AnyMorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Morphism cid1 == Morphism cid2 =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai constituents cid1 == constituents cid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -- need to be refined, using morphism translations !!!
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwinstance Show AnyMorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai show (Morphism cid) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai language_name cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ++" : "++language_name (morSourceLogic cid)
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw ++" -> "++language_name (morTargetLogic cid)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaityconAnyMorphism :: TyCon
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaityconAnyMorphism = mkTyCon "Logic.Grothendieck.AnyMorphism"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Typeable AnyMorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai typeOf _ = mkTyConApp tyconAnyMorphism []
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- * Modifications
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata AnyModification = forall
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid cid1 cid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign2 morphism2 symbol2 raw_symbol2 proof_tree2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign3 morphism3 symbol3 raw_symbol3 proof_tree3
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign4 morphism4 symbol4 raw_symbol4 proof_tree4.
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw Modification lid cid1 cid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign2 morphism2 symbol2 raw_symbol2 proof_tree2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign3 morphism3 symbol3 raw_symbol3 proof_tree3
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign4 morphism4 symbol4 raw_symbol4 proof_tree4 => Modification lid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Eq AnyModification where
cbcfaf83d8f1bf6aa00c793903a55685cac2c548jg find rules for equality
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Show AnyModification where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai show (Modification lid) = language_name lid ++
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ":" ++ language_name (sourceComorphism lid) ++
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai "=>" ++ language_name (targetComorphism lid)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiidModification :: AnyComorphism -> AnyModification
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwidModification (Comorphism cid) = Modification (IdModif cid)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaityconAnyModification :: TyCon
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaityconAnyModification = mkTyCon "Logic.Grothendieck.AnyModification"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Typeable AnyModification where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai typeOf _ = mkTyConApp tyconAnyModification []
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | vertical compositions of modifications
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaivertCompModification :: Monad m => AnyModification -> AnyModification
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> m AnyModification
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwvertCompModification (Modification lid1) (Modification lid2) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let cid1 = targetComorphism lid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai cid2 = sourceComorphism lid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if language_name cid1 == language_name cid2
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw then return $ Modification (VerCompModif lid1 lid2)
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw else fail $ "Comorphism mismatch in composition of" ++ language_name lid1
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw ++ "and" ++ language_name lid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | horizontal composition of modifications
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaihorCompModification :: Monad m => AnyModification -> AnyModification
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw -> m AnyModification
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaihorCompModification (Modification lid1) (Modification lid2) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let cid1 = sourceComorphism lid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai cid2 = sourceComorphism lid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai in if language_name (targetLogic cid1) == language_name (sourceLogic cid2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai then return $ Modification (HorCompModif lid1 lid2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else fail $ "Logic mismatch in composition of" ++ language_name lid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ++ "and" ++ language_name lid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Logic graph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata LogicGraph = LogicGraph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai { logics :: Map.Map String AnyLogic
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , comorphisms :: Map.Map String AnyComorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , inclusions :: Map.Map (String,String) AnyComorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , unions :: Map.Map (String, String) (AnyComorphism, AnyComorphism)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , morphisms :: Map.Map String AnyMorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , modifications :: Map.Map String AnyModification }
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiemptyLogicGraph :: LogicGraph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiemptyLogicGraph =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai LogicGraph Map.empty Map.empty Map.empty Map.empty Map.empty Map.empty
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Heterogenous Sublogic Graph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- this graph only contains interesting Sublogics plus comorphisms relating
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- these sublogics; a comorphism might be mentioned multiple times
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata HetSublogicGraph = HetSublogicGraph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai { sublogicNodes :: Map.Map String G_sublogics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , comorphismEdges :: Map.Map (String,String) [AnyComorphism]
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiemptyHetSublogicGraph :: HetSublogicGraph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiemptyHetSublogicGraph = HetSublogicGraph Map.empty Map.empty
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | find a logic in a logic graph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailookupLogic error_prefix logname logicGraph =
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw case Map.lookup logname $ logics logicGraph of
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw Nothing -> fail $ error_prefix ++" in LogicGraph logic \""
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw ++ logname ++ "\" unknown"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just lid -> return lid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | union to two logics
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert MustacchilogicUnion :: LogicGraph -> AnyLogic -> AnyLogic
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi -> Result (AnyComorphism, AnyComorphism)
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert MustacchilogicUnion lg l1@(Logic lid1) l2@(Logic lid2) =
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi case logicInclusion lg l1 l2 of
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi Result _ (Just c) -> return (c,idComorphism l2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> case logicInclusion lg l2 l1 of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Result _ (Just c) -> return (idComorphism l1,c)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> case Map.lookup (ln1,ln2) (unions lg) of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just u -> return u
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Nothing -> case Map.lookup (ln2,ln1) (unions lg) of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just (c2,c1) -> return (c1,c2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Nothing -> fail $ "Union of logics " ++ ln1 ++
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai " and " ++ ln2 ++ " does not exist"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai where ln1 = language_name lid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ln2 = language_name lid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | find a comorphism composition in a logic graph
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism
134a1f4e3289b54e0f980e9cf05352e419a60beeCasper H.S. DiklookupCompComorphism nameList logicGraph = do
134a1f4e3289b54e0f980e9cf05352e419a60beeCasper H.S. Dik cs <- sequence $ map lookupN nameList
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai case cs of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai c:cs1 -> foldM compComorphism c cs1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> fail "Illegal empty comorphism composition"
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw hasSublogic name (Logic lid) = elem name (sublogic_names $ top_sublogic lid)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lookupN name =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai 'i':'d':'_':logic -> do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let (mainLogic, subLogicD) = span (/= '.') logic
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai --subLogicD will begin with a . which has to be removed
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw l <- maybe (fail ("Cannot find Logic "++mainLogic)) return
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai $ Map.lookup mainLogic (logics logicGraph)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai case hasSublogic (tail subLogicD) l of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai True -> return $ idComorphism l
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai False -> fail ("Error in sublogic name"++logic)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> maybe (fail ("Cannot find logic comorphism "++name)) return
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi $ Map.lookup name (comorphisms logicGraph)
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi-- | find a comorphism in a logic graph
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert MustacchilookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert MustacchilookupComorphism coname = lookupCompComorphism $ splitOn ';' coname
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi-- | find a modification in a logic graph
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert MustacchilookupModification :: (Monad m) => String -> LogicGraph -> m AnyModification
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert MustacchilookupModification input lG
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi = case (parse (do r<- parseModif lG; eof; return r) "" input) of
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi Left err -> fail $ show err
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert MustacchiparseModif :: (Monad m) => LogicGraph -> Parser (m AnyModification)
368fc9412cc48af49761a1b8808d9c4079709391Robert MustacchiparseModif lG= do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (xs, _) <- separatedBy (vertcomp lG) (char '*')
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let r = do y <- sequence xs
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai m:ms -> return $ foldM horCompModification m ms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> Nothing
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Nothing -> fail "Illegal empty horizontal composition"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just m -> return m
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaivertcomp :: (Monad m) => LogicGraph -> Parser (m AnyModification)
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwvertcomp lG = do
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw (xs, _) <- separatedBy (pm lG) (char ';')
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let r = do
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg y <- sequence xs
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai m:ms -> return $ foldM vertCompModification m ms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> Nothing
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai --r has type Maybe (m AnyModification)
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg Nothing -> fail "Illegal empty vertical composition"
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw Just m -> return m
6b9384783302cfb5bb67d617114d5a4e1dc3d609jgpm :: (Monad m) => LogicGraph -> Parser (m AnyModification)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaipm lG = parseName lG <|> bracks lG
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaibracks :: (Monad m) => LogicGraph -> Parser (m AnyModification)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaibracks lG = do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai modif <- parseModif lG
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai return modif
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwparseIdentity :: (Monad m) => LogicGraph -> Parser (m AnyModification)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiparseIdentity lG = do {
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ; char 'd'
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ; char '_'
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ; tok <- simpleId
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ; let name = tokStr tok
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ; let y = Map.lookup name (comorphisms lG)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ; case y of
0bfaec6936a60046cf3a098fa731cb5e07377595llai Nothing -> fail $ "Cannot find comorphism"++name
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just x -> return$ return $ idModification x
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiparseName :: (Monad m) => LogicGraph -> Parser (m AnyModification)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiparseName lG = do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai try (parseIdentity lG)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai tok <- simpleId
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let name = tokStr tok
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let y = Map.lookup name (modifications lG)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Nothing -> fail $ "Cannot find modification"++name
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just x -> return $ return x
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- * The Grothendieck signature category
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Grothendieck signature morphisms with indices
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata GMorphism = forall cid lid1 sublogics1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec1 sentence1 symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg lid2 sublogics2
1c4bb543a73abbf7464757d5ba7d8b84899f2408Jerry Gilliam basic_spec2 sentence2 symb_items2 symb_map_items2
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg Comorphism cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid1 sublogics1 basic_spec1 sentence1
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw symb_items1 symb_map_items1
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign1 morphism1 symbol1 raw_symbol1 proof_tree1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid2 sublogics2 basic_spec2 sentence2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai symb_items2 symb_map_items2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => GMorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai { gMorphismComor :: cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , gMorphismSign :: sign1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , gMorphismSignIdx :: Int -- ^ 'G_sign' index of source signature
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , gMorphismMor :: morphism2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai , gMorphismMorIdx :: Int -- ^ `G_morphism index of target morphism
174e0b3da3fbbb8b4edc68dcf4726e5727d34df6jginstance Eq GMorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai GMorphism cid1 sigma1 in1 mor1 in1' == GMorphism cid2 sigma2 in2 mor2 in2'
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai = Comorphism cid1 == Comorphism cid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai && G_sign (sourceLogic cid1) sigma1 in1 ==
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai G_sign (sourceLogic cid2) sigma2 in2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai && (in1' > 0 && in2' > 0 && in1' == in2'
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai || coerceMorphism (targetLogic cid1) (targetLogic cid2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai "Eq GMorphism.coerceMorphism" mor1 == Just mor2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisHomogeneous :: GMorphism -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisHomogeneous (GMorphism cid _ _ _ _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai isIdComorphism (Comorphism cid)
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwdata Grothendieck = Grothendieck deriving Show
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Language Grothendieck
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Show GMorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai show (GMorphism cid s _ m _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai show (normalize (Comorphism cid)) ++ "(" ++ show s ++ ")" ++ show m
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Pretty GMorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai pretty (GMorphism cid s _ m _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai text (show (normalize (Comorphism cid)))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai parens (space <> pretty s <> space)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllainormalize :: AnyComorphism -> AnyComorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllainormalize = id
1c4bb543a73abbf7464757d5ba7d8b84899f2408Jerry Gilliam{- todo: somthing like the following...
1c4bb543a73abbf7464757d5ba7d8b84899f2408Jerry Gilliamnormalize (Comorphism cid) =
1c4bb543a73abbf7464757d5ba7d8b84899f2408Jerry Gilliam CompComorphism r1 r2 ->
1c4bb543a73abbf7464757d5ba7d8b84899f2408Jerry Gilliam case (normalize (Comorphism r1), normalize (Comorphism r2)) of
1c4bb543a73abbf7464757d5ba7d8b84899f2408Jerry Gilliam (Comorphism n1, Comorphism n2) ->
1c4bb543a73abbf7464757d5ba7d8b84899f2408Jerry Gilliam if isIdComorphism (Comorphism n1) then Comorphism n2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else if isIdComorphism (Comorphism n2) then Comorphism n1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else Comorphism (CompComorphism n1 n2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> Comorphism cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiinstance Category Grothendieck G_sign GMorphism where
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ide _ (G_sign lid sigma ind) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai GMorphism (mkIdComorphism lid (top_sublogic lid))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sigma ind (ide lid sigma) 0
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (GMorphism r1 sigma1 ind1 mor1 _)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (GMorphism r2 _sigma2 _ mor2 _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai do let lid1 = sourceLogic r1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid2 = targetLogic r1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid3 = sourceLogic r2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lid4 = targetLogic r2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai mor1' <- coerceMorphism lid2 lid3 "Grothendieck.comp" mor1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai mor1'' <- map_morphism r2 mor1'
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai mor <- comp lid4 mor1'' mor2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if isIdComorphism (Comorphism r1) &&
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai case coerceSublogic lid2 lid3 "Grothendieck.comp"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (targetSublogic r1) of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just sl1 -> maybe (error ("Logic.Grothendieck: Category "++
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai "instance.comp: no mapping for " ++
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai show sl1))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (isSubElem (targetSublogic r2))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (mapSublogic r2 sl1)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai _ -> False
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai then do sigma1' <- coerceSign lid1 lid3 "Grothendieck.comp" sigma1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai return (GMorphism r2 sigma1' ind1 mor 0)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else if isIdComorphism (Comorphism r2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai then do mor2' <- coerceMorphism lid4 lid2 "Grothendieck.comp" mor2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai mor' <- comp lid2 mor1 mor2'
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai return (GMorphism r1 sigma1 ind1 mor' 0)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai else return (GMorphism (CompComorphism r1 r2) sigma1 ind1 mor 0)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai dom _ (GMorphism r sigma ind _mor _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai G_sign (sourceLogic r) sigma ind
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai cod _ (GMorphism r _sigma _ mor _) =
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw G_sign lid2 (cod lid2 mor) 0
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw where lid2 = targetLogic r
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai legal_obj _ (G_sign lid sigma _) = legal_obj lid sigma
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai legal_mor _ (GMorphism r sigma _ mor _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai legal_mor lid2 mor &&
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai case maybeResult $ map_sign r sigma of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just (sigma',_) -> sigma' == cod lid2 mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Nothing -> False
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry Gilliam where lid2 = targetLogic r
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaigEmbed2 :: G_sign -> G_morphism -> GMorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaigEmbed2 (G_sign lid2 sig si) (G_morphism lid _ mor ind _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let cid = mkIdComorphism lid (top_sublogic lid)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just sig1 = coerceSign lid2 (sourceLogic cid) "gEmbed2" sig
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai in GMorphism cid sig1 si mor ind
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaigEmbed :: G_morphism -> GMorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaigEmbed (G_morphism lid s1 mor ind _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai GMorphism (mkIdComorphism lid (top_sublogic lid)) (dom lid mor) s1 mor ind
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Embedding of comorphisms as Grothendieck sig mors
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaigEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaigEmbedComorphism (Comorphism cid) (G_sign lid sig ind) = do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sig' <- coerceSign lid (sourceLogic cid) "gEmbedComorphism" sig
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (sigTar,_) <- map_sign cid sig'
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg let lidTar = targetLogic cid
de442498e34e37fe9b61cfe5beaacdecd06c6a1cRobert Mustacchi return (GMorphism cid sig' ind (ide lidTar sigTar) 0)
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg-- | heterogeneous union of two Grothendieck signatures
6b9384783302cfb5bb67d617114d5a4e1dc3d609jggsigUnion :: LogicGraph -> G_sign -> G_sign -> Result G_sign
6b9384783302cfb5bb67d617114d5a4e1dc3d609jggsigUnion lg gsig1@(G_sign lid1 sigma1 _) gsig2@(G_sign lid2 sigma2 _) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if language_name lid1 == language_name lid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai then homogeneousGsigUnion gsig1 gsig2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (Comorphism cid1, Comorphism cid2) <-
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai logicUnion lg (Logic lid1) (Logic lid2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let lidS1 = sourceLogic cid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lidS2 = sourceLogic cid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lidT1 = targetLogic cid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai lidT2 = targetLogic cid2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sigma1' <- coerceSign lid1 lidS1 "Union of signaturesa" sigma1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sigma2' <- coerceSign lid2 lidS2 "Union of signaturesb" sigma2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (sigma1'',_) <- map_sign cid1 sigma1' -- where to put axioms???
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (sigma2'',_) <- map_sign cid2 sigma2' -- where to put axioms???
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sigma2''' <- coerceSign lidT2 lidT1 "Union of signaturesc" sigma2''
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sigma3 <- signature_union lidT1 sigma1'' sigma2'''
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg return (G_sign lidT1 sigma3 0)
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg-- | homogeneous Union of two Grothendieck signatures
6b9384783302cfb5bb67d617114d5a4e1dc3d609jghomogeneousGsigUnion :: G_sign -> G_sign -> Result G_sign
6b9384783302cfb5bb67d617114d5a4e1dc3d609jghomogeneousGsigUnion (G_sign lid1 sigma1 _) (G_sign lid2 sigma2 _) = do
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg sigma2' <- coerceSign lid2 lid1 "Union of signaturesd" sigma2
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg sigma3 <- signature_union lid1 sigma1 sigma2'
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry Gilliam return (G_sign lid1 sigma3 0)
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry Gilliam-- | union of a list of Grothendieck signatures
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry GilliamgsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchigsigManyUnion _ [] =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi fail "union of emtpy list of signatures"
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchigsigManyUnion lg (gsigma : gsigmas) =
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi foldM (gsigUnion lg) gsigma gsigmas
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | homogeneous Union of a list of morphisms
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry GilliamhomogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry GilliamhomogeneousMorManyUnion [] =
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry Gilliam fail "homogeneous union of emtpy list of morphisms"
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry GilliamhomogeneousMorManyUnion (gmor : gmors) =
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry Gilliam foldM ( \ (G_morphism lid2 _ mor2 _ _) (G_morphism lid1 _ mor1 _ _) -> do
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry Gilliam mor1' <- coerceMorphism lid1 lid2 "homogeneousMorManyUnion" mor1
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry Gilliam mor <- morphism_union lid2 mor1' mor2
6c6a45620b26cdcc248b9dc54f23d045d8dd4588Jerry Gilliam return (G_morphism lid2 0 mor 0 0)) gmor gmors
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | inclusion between two logics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailogicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllailogicInclusion logicGraph l1@(Logic lid1) (Logic lid2) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let ln1 = language_name lid1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai ln2 = language_name lid2 in
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if ln1==ln2 then
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (idComorphism l1)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi else case Map.lookup (ln1,ln2) (inclusions logicGraph) of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just (Comorphism i) ->
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai return (Comorphism i)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi fail ("No inclusion from "++ln1++" to "++ln2++" found")
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiupdateMorIndex :: Int -> GMorphism -> GMorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchiupdateMorIndex i (GMorphism cid sign si mor _) = GMorphism cid sign si mor i
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert MustacchitoG_morphism :: GMorphism -> G_morphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaitoG_morphism (GMorphism cid _ _ mor i) = G_morphism (targetLogic cid) 0 mor i 0
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi-- | inclusion morphism between two Grothendieck signatures
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchiginclusion logicGraph (G_sign lid1 sigma1 ind) (G_sign lid2 sigma2 _) = do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Comorphism i <- logicInclusion logicGraph (Logic lid1) (Logic lid2)
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sigma1' <- coerceSign lid1 (sourceLogic i) "Inclusion of signatures" sigma1
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi (sigma1'',_) <- map_sign i sigma1'
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi sigma2' <- coerceSign lid2 (targetLogic i) "Inclusion of signatures" sigma2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai mor <- inclusion (targetLogic i) sigma1'' sigma2'
9e5aa9d8a21f8efa8ba9c9e4a0aa6edc66d07eb2Robert Mustacchi return (GMorphism i sigma1' ind mor 0)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Composition of two Grothendieck signature morphisms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | with itermediate inclusion
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicompInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicompInclusion lg mor1 mor2 = do
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let sigma1 = cod Grothendieck mor1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sigma2 = dom Grothendieck mor2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai unless (isSubGsign lg sigma1 sigma2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (fail "Logic.Grothendieck.compInclusion: not a subsignature")
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai incl <- ginclusion lg sigma1 sigma2
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw mor <- comp Grothendieck mor1 incl
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai comp Grothendieck mor mor2
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw-- | Composition of two Grothendieck signature morphisms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | with intermediate homogeneous inclusion
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicompHomInclusion :: GMorphism -> GMorphism -> Result GMorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicompHomInclusion mor1 mor2 = compInclusion emptyLogicGraph mor1 mor2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | Find all (composites of) comorphisms starting from a given logic
0bfaec6936a60046cf3a098fa731cb5e07377595llaifindComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaifindComorphismPaths lg (G_sublogics lid sub) =
0bfaec6936a60046cf3a098fa731cb5e07377595llai nub $ map fst $ iterateComp (0::Int) [(idc,[idc])]
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai idc = Comorphism (mkIdComorphism lid sub)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai coMors = Map.elems $ comorphisms lg
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -- compute possible compositions, but only up to depth 3
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai iterateComp n l = -- (l::[(AnyComorphism,[AnyComorphism])]) =
0bfaec6936a60046cf3a098fa731cb5e07377595llai if n>3 || l==newL then newL else iterateComp (n+1) newL
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai newL = nub (l ++ (concat (map extend l)))
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -- extend comorphism list in all directions, but no cylces
0bfaec6936a60046cf3a098fa731cb5e07377595llai extend (coMor, cmps) =
0bfaec6936a60046cf3a098fa731cb5e07377595llai let addCoMor c =
0bfaec6936a60046cf3a098fa731cb5e07377595llai case compComorphism coMor c of
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Nothing -> Nothing
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Just c1 -> Just (c1, c : cmps)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai in catMaybes $ map addCoMor $ filter (not . (`elem` cmps)) $ coMors
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | finds first comorphism with a matching sublogic
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaifindComorphism ::Monad m => G_sublogics -> [AnyComorphism] -> m AnyComorphism
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaifindComorphism _ [] = fail "No matching comorphism found"
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaifindComorphism gsl@(G_sublogics lid sub) ((Comorphism cid):rest) =
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai let l2 = sourceLogic cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai rec = findComorphism gsl rest in
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai if language_name lid == language_name l2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai then if isSubElem (forceCoerceSublogic lid l2 sub) $ sourceSublogic cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai then return $ Comorphism cid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | check transportability of Grothendieck signature morphisms
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | (currently returns false for heterogeneous morphisms)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisTransportable :: GMorphism -> Bool
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaiisTransportable (GMorphism cid _ ind1 mor ind2) = ind1 >0 && ind2 >0
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai && isModelTransportable(Comorphism cid)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai && is_transportable (targetLogic cid) mor
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- * Provers
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai-- | provers and consistency checkers for specific logics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata G_prover = forall lid sublogics
0bfaec6936a60046cf3a098fa731cb5e07377595llai basic_spec sentence symb_items symb_map_items
6b9384783302cfb5bb67d617114d5a4e1dc3d609jg sign morphism symbol raw_symbol proof_tree .
0bfaec6936a60046cf3a098fa731cb5e07377595llai Logic lid sublogics
0bfaec6936a60046cf3a098fa731cb5e07377595llai basic_spec sentence symb_items symb_map_items
0bfaec6936a60046cf3a098fa731cb5e07377595llai sign morphism symbol raw_symbol proof_tree =>
0bfaec6936a60046cf3a098fa731cb5e07377595llai G_prover lid (Prover sign sentence sublogics proof_tree)
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwgetProverName :: G_prover -> String
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amwgetProverName (G_prover _ p) = prover_name p
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicoerceProver ::
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
0bfaec6936a60046cf3a098fa731cb5e07377595llai Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Monad m) => lid1 -> lid2 -> String
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> Prover sign1 sentence1 sublogics1 proof_tree1
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw -> m (Prover sign2 sentence2 sublogics2 proof_tree2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicoerceProver l1 l2 msg m1 = primCoerce l1 l2 msg m1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaidata G_cons_checker = forall lid sublogics
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai basic_spec sentence symb_items symb_map_items
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign morphism symbol raw_symbol proof_tree .
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Logic lid sublogics
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw basic_spec sentence symb_items symb_map_items
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign morphism symbol raw_symbol proof_tree =>
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw G_cons_checker lid
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (ConsChecker sign sentence sublogics morphism proof_tree)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicoerceConsChecker ::
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
da6c28aaf62fa55f0fdb8004aa40f88f23bf53f0amw sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Monad m) => lid1 -> lid2 -> String
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> ConsChecker sign1 sentence1 sublogics1 morphism1 proof_tree1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai -> m (ConsChecker sign2 sentence2 sublogics2 morphism2 proof_tree2)
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicoerceConsChecker l1 l2 msg m1 = primCoerce l1 l2 msg m1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicoerceG_sign ::
0bfaec6936a60046cf3a098fa731cb5e07377595llai (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
0bfaec6936a60046cf3a098fa731cb5e07377595llai sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllai Monad m) => lid1 -> String -> G_sign -> m sign1
facf4a8d7b59fde89a8662b4f4c73a758e6c402cllaicoerceG_sign l1 msg (G_sign l2 sign2 _) = primCoerce l2 l1 msg sign2