------------------------------------------------------------------
--"Grothendieck" versions of the various parts of type class Logic
------------------------------------------------------------------
-- | Grothendieck basic specifications
data G_basic_spec = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_basic_spec lid basic_spec
instance Show G_basic_spec where
show (G_basic_spec _ s) = show s
instance Pretty G_basic_spec where
pretty (G_basic_spec _ s) = pretty s
-- | Grothendieck signatures
data G_sign = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
instance Typeable G_sign where
typeOf _ = mkTyConApp tyconG_sign []
G_sign l1 sigma1 i1 == G_sign l2 sigma2 i2 =
(i1 > 0 && i2 > 0 && i1 == i2) ||
coerceSign l1 l2 "Eq G_sign" sigma1 == Just sigma2
-- | prefer a faster subsignature test if possible
isHomSubGsign :: G_sign -> G_sign -> Bool
isHomSubGsign (G_sign i1 sigma1 s1) (G_sign i2 sigma2 s2) =
if s1 == s2 then True else
maybe False (is_subsig i1 sigma1) $ coerceSign i2 i1 "is_subgsign" sigma2
isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
isSubGsign lg (G_sign lid1 sigma1 _) (G_sign lid2 sigma2 _) =
do Comorphism cid <- resultToMaybe $
logicInclusion lg (Logic lid1) (Logic lid2)
sigma1' <- coerceSign lid1 (sourceLogic cid)
sigma2' <- coerceSign lid2 (targetLogic cid)
sigma1t <- resultToMaybe $ map_sign cid sigma1'
return $ is_subsig (targetLogic cid) (fst sigma1t) sigma2'
instance Show G_sign where
show (G_sign _ s _) = show s
instance Pretty G_sign where
pretty (G_sign _ s _) = pretty s
langNameSig :: G_sign -> String
langNameSig (G_sign lid _ _) = language_name lid
-- | Grothendieck signature lists
data G_sign_list = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
-- | Grothendieck extended signatures
data G_ext_sign = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_ext_sign lid sign (
Set.Set symbol)
-- | Grothendieck symbols
data G_symbol = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
instance Show G_symbol where
show (G_symbol _ s) = show s
instance Pretty G_symbol where
pretty (G_symbol _ s) = pretty s
instance Eq G_symbol where
(G_symbol i1 s1) == (G_symbol i2 s2) =
language_name i1 == language_name i2 && coerceSymbol i1 i2 s1 == s2
-- | Grothendieck symbol lists
data G_symb_items_list = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_symb_items_list lid [symb_items]
instance Show G_symb_items_list where
show (G_symb_items_list _ l) = show l
instance Pretty G_symb_items_list where
pretty (G_symb_items_list _ l) = ppWithCommas l
instance Eq G_symb_items_list where
(G_symb_items_list i1 s1) == (G_symb_items_list i2 s2) =
coerceSymbItemsList i1 i2 "Eq G_symb_items_list" s1 == Just s2
-- | Grothendieck symbol maps
data G_symb_map_items_list = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_symb_map_items_list lid [symb_map_items]
instance Show G_symb_map_items_list where
show (G_symb_map_items_list _ l) = show l
instance Pretty G_symb_map_items_list where
pretty (G_symb_map_items_list _ l) = ppWithCommas l
instance Eq G_symb_map_items_list where
(G_symb_map_items_list i1 s1) == (G_symb_map_items_list i2 s2) =
coerceSymbMapItemsList i1 i2 "Eq G_symb_map_items_list" s1 == Just s2
-- | Grothendieck diagrams
data G_diagram = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_diagram lid (
Tree.Gr sign morphism)
-- | Grothendieck sublogics
data G_sublogics = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_sublogics lid sublogics
tyconG_sublogics :: TyCon
instance Typeable G_sublogics where
typeOf _ = mkTyConApp tyconG_sublogics []
instance Show G_sublogics where
show (G_sublogics lid sub) = case sublogic_names sub of
[] -> error "show G_sublogics"
h : _ -> show lid ++ "." ++ h
instance Eq G_sublogics where
(G_sublogics lid1 l1) == (G_sublogics lid2 l2) =
language_name lid1 == language_name lid2
&& forceCoerceSublogic lid1 lid2 l1 == l2
isProperSublogic :: G_sublogics -> G_sublogics -> Bool
isProperSublogic a@(G_sublogics lid1 l1) b@(G_sublogics lid2 l2) =
isSubElem (forceCoerceSublogic lid1 lid2 l1) l2 && a /= b
-- | Homogeneous Grothendieck signature morphisms
data G_morphism = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_morphism lid morphism Int
instance Show G_morphism where
show (G_morphism _ l _) = show l
----------------------------------------------------------------
-- Existential types for the logic graph
----------------------------------------------------------------
-- | Existential type for comorphisms
data AnyComorphism = forall cid lid1 sublogics1
basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
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 =>
instance Eq AnyComorphism where
Comorphism cid1 == Comorphism cid2 =
constituents cid1 == constituents cid2
-- need to be refined, using comorphism translations !!!
instance Show AnyComorphism where
++" : "++language_name (sourceLogic cid)
++" -> "++language_name (targetLogic cid)
tyconAnyComorphism :: TyCon
instance Typeable AnyComorphism where
typeOf _ = mkTyConApp tyconAnyComorphism []
-- | compute the identity comorphism for a logic
idComorphism :: AnyLogic -> AnyComorphism
idComorphism (Logic lid) = Comorphism (IdComorphism lid (top_sublogic lid))
-- | Test whether a comporphism is the identity
isIdComorphism :: AnyComorphism -> Bool
isIdComorphism (Comorphism cid) =
compComorphism :: Monad m => AnyComorphism -> AnyComorphism -> m AnyComorphism
compComorphism (Comorphism cid1) (Comorphism cid2) =
let l1 = targetLogic cid1
if language_name l1 == language_name l2 then
if isSubElem (forceCoerceSublogic l1 l2 $ targetSublogic cid1)
then {- case (isIdComorphism cm1,isIdComorphism cm2) of
_ -> -} return $ Comorphism (CompComorphism cid1 cid2)
else fail ("Sublogic mismatch in composition of "++language_name cid1++
" and "++language_name cid2)
else fail ("Logic mismatch in composition of "++language_name cid1++
" and "++language_name cid2)
-- | check if sublogic fits for comorphism
lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
lessSublogicComor (G_sublogics lid1 sub1) (Comorphism cid) =
let lid2 = sourceLogic cid
in language_name lid2 == language_name lid1
&& isSubElem (forceCoerceSublogic lid1 lid2 sub1) (sourceSublogic cid)
-- | Existential type for morphisms
data AnyMorphism = forall cid lid1 sublogics1
basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
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 =>
instance Eq AnyMorphism where
Morphism cid1 == Morphism cid2 =
constituents cid1 == constituents cid2
-- need to be refined, using morphism translations !!!
instance Show AnyMorphism where
++" : "++language_name (morSourceLogic cid)
++" -> "++language_name (morTargetLogic cid)
tyconAnyMorphism :: TyCon
instance Typeable AnyMorphism where
typeOf _ = mkTyConApp tyconAnyMorphism []
data LogicGraph = LogicGraph
{ logics ::
Map.Map String AnyLogic
, comorphisms ::
Map.Map String AnyComorphism
, inclusions ::
Map.Map (String,String) AnyComorphism
, unions ::
Map.Map (String, String) (AnyComorphism, AnyComorphism)
emptyLogicGraph :: LogicGraph
-- | find a logic in a logic graph
lookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic
lookupLogic error_prefix logname logicGraph =
Nothing -> fail (error_prefix++" in LogicGraph logic \""
logicUnion :: LogicGraph -> AnyLogic -> AnyLogic
-> Result (AnyComorphism, AnyComorphism)
logicUnion lg l1@(Logic lid1) l2@(Logic lid2) =
case logicInclusion lg l1 l2 of
Result _ (Just c) -> return (c,idComorphism l2)
_ -> case logicInclusion lg l2 l1 of
Result _ (Just c) -> return (idComorphism l1,c)
Nothing -> case
Map.lookup (ln2,ln1) (unions lg) of
Just (c2,c1) -> return (c1,c2)
Nothing -> fail $ "Union of logics " ++ ln1 ++
" and " ++ ln2 ++ " does not exist"
where ln1 = language_name lid1
-- | find a comorphism composition in a logic graph
lookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism
lookupCompComorphism nameList logicGraph = do
cs <- sequence $ map lookupN nameList
c:cs1 -> foldM compComorphism c cs1
_ -> fail "Illegal empty comorphism composition"
let mainLogic = takeWhile (/= '.') logic
l <- maybe (fail ("Cannot find Logic "++mainLogic)) return
_ -> maybe (fail ("Cannot find logic comorphism "++name)) return
-- | find a comorphism in a logic graph
lookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism
lookupComorphism coname = lookupCompComorphism $ splitOn ';' coname
------------------------------------------------------------------
-- The Grothendieck signature category
------------------------------------------------------------------
-- | Grothendieck signature morphisms
data GMorphism = forall cid lid1 sublogics1
basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1
basic_spec2 sentence2 symb_items2 symb_map_items2
sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
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 =>
GMorphism cid sign1 Int morphism2 Int
instance Eq GMorphism where
GMorphism cid1 sigma1 in1 mor1 in1' == GMorphism cid2 sigma2 in2 mor2 in2'
= Comorphism cid1 == Comorphism cid2
&& G_sign (sourceLogic cid1) sigma1 in1 ==
G_sign (sourceLogic cid2) sigma2 in2
&& (in1' > 0 && in2' > 0 && in1' == in2'
|| coerceMorphism (targetLogic cid1) (targetLogic cid2)
isHomogeneous :: GMorphism -> Bool
isHomogeneous (GMorphism cid _ _ _ _) =
isIdComorphism (Comorphism cid)
data Grothendieck = Grothendieck deriving Show
instance Language Grothendieck
instance Show GMorphism where
show (GMorphism cid s _ m _) =
show (normalize (Comorphism cid)) ++ "(" ++ show s ++ ")" ++ show m
instance Pretty GMorphism where
pretty (GMorphism cid s _ m _) =
text (show (normalize (Comorphism cid)))
parens (space <> pretty s <> space)
normalize :: AnyComorphism -> AnyComorphism
{- todo: somthing like the following...
normalize (Comorphism cid) =
case (normalize (Comorphism r1), normalize (Comorphism r2)) of
(Comorphism n1, Comorphism n2) ->
if isIdComorphism (Comorphism n1) then Comorphism n2
else if isIdComorphism (Comorphism n2) then Comorphism n1
else Comorphism (CompComorphism n1 n2)
instance Category Grothendieck G_sign GMorphism where
ide _ (G_sign lid sigma ind) =
GMorphism (IdComorphism lid (top_sublogic lid)) sigma ind (ide lid sigma) 0
(GMorphism r1 sigma1 ind1 mor1 _)
(GMorphism r2 _sigma2 _ mor2 _) =
do let lid1 = sourceLogic r1
mor1'' <- map_morphism r2 mor1'
mor <- comp lid4 mor1'' mor2
if isIdComorphism (Comorphism r1) &&
Just sl1 -> isSubElem (targetSublogic r2) (mapSublogic r2 sl1)
return (GMorphism r2 sigma1' ind1 mor 0)
else if isIdComorphism (Comorphism r2)
mor' <- comp lid2 mor1 mor2'
return (GMorphism r1 sigma1 ind1 mor' 0)
else return (GMorphism (CompComorphism r1 r2) sigma1 ind1 mor 0)
dom _ (GMorphism r sigma ind _mor _) =
G_sign (sourceLogic r) sigma ind
cod _ (GMorphism r _sigma _ mor _) =
G_sign lid2 (cod lid2 mor) 0
where lid2 = targetLogic r
legal_obj _ (G_sign lid sigma _) = legal_obj lid sigma
legal_mor _ (GMorphism r sigma _ mor _) =
case maybeResult $ map_sign r sigma of
Just (sigma',_) -> sigma' == cod lid2 mor
where lid2 = targetLogic r
-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
gEmbed2 :: G_sign -> G_morphism -> GMorphism
gEmbed2 (G_sign lid2 sig si) (G_morphism lid mor ind) =
let cid = IdComorphism lid (top_sublogic lid)
Just sig1 = coerceSign lid2 (sourceLogic cid) "gEmbed2" sig
in GMorphism cid sig1 si mor ind
-- | Embedding of homogeneous signature morphisms as Grothendieck sig mors
gEmbed :: G_morphism -> GMorphism
gEmbed (G_morphism lid mor ind) =
GMorphism (IdComorphism lid (top_sublogic lid)) (dom lid mor) 0 mor ind
-- | Embedding of comorphisms as Grothendieck sig mors
gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
gEmbedComorphism (Comorphism cid) (G_sign lid sig ind) = do
sig' <- coerceSign lid (sourceLogic cid) "gEmbedComorphism" sig
(sigTar,_) <- map_sign cid sig'
let lidTar = targetLogic cid
return (GMorphism cid sig' ind (ide lidTar sigTar) 0)
-- | heterogeneous union of two Grothendieck signatures
gsigUnion :: LogicGraph -> G_sign -> G_sign -> Result G_sign
gsigUnion lg gsig1@(G_sign lid1 sigma1 _) gsig2@(G_sign lid2 sigma2 _) =
if language_name lid1 == language_name lid2
then homogeneousGsigUnion gsig1 gsig2
(Comorphism cid1, Comorphism cid2) <-
logicUnion lg (Logic lid1) (Logic lid2)
let lidS1 = sourceLogic cid1
sigma1' <- coerceSign lid1 lidS1 "Union of signaturesa" sigma1
sigma2' <- coerceSign lid2 lidS2 "Union of signaturesb" sigma2
(sigma1'',_) <- map_sign cid1 sigma1' -- where to put axioms???
(sigma2'',_) <- map_sign cid2 sigma2' -- where to put axioms???
sigma2''' <- coerceSign lidT2 lidT1 "Union of signaturesc" sigma2''
sigma3 <- signature_union lidT1 sigma1'' sigma2'''
return (G_sign lidT1 sigma3 0)
-- | homogeneous Union of two Grothendieck signatures
homogeneousGsigUnion :: G_sign -> G_sign -> Result G_sign
homogeneousGsigUnion (G_sign lid1 sigma1 _) (G_sign lid2 sigma2 _) = do
sigma2' <- coerceSign lid2 lid1 "Union of signaturesd" sigma2
sigma3 <- signature_union lid1 sigma1 sigma2'
return (G_sign lid1 sigma3 0)
-- | union of a list of Grothendieck signatures
gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
fail "union of emtpy list of signatures"
gsigManyUnion lg (gsigma : gsigmas) =
foldM (gsigUnion lg) gsigma gsigmas
-- | homogeneous Union of a list of morphisms
homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
homogeneousMorManyUnion [] =
fail "homogeneous union of emtpy list of morphisms"
homogeneousMorManyUnion (gmor : gmors) =
foldM ( \ (G_morphism lid2 mor2 _) (G_morphism lid1 mor1 _) -> do
mor1' <- coerceMorphism lid1 lid2 "homogeneousMorManyUnion" mor1
mor <- morphism_union lid2 mor1' mor2
return (G_morphism lid2 mor 0)) gmor gmors
-- | inclusion between two logics
logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicInclusion logicGraph l1@(Logic lid1) (Logic lid2) =
let ln1 = language_name lid1
ln2 = language_name lid2 in
else case
Map.lookup (ln1,ln2) (inclusions logicGraph) of
fail ("No inclusion from "++ln1++" to "++ln2++" found")
updateMorIndex :: Int -> GMorphism -> GMorphism
updateMorIndex i (GMorphism cid sign si mor _) = GMorphism cid sign si mor i
toG_morphism :: GMorphism -> G_morphism
toG_morphism (GMorphism cid _ _ mor i) = G_morphism (targetLogic cid) mor i
-- | inclusion morphism between two Grothendieck signatures
ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
ginclusion logicGraph (G_sign lid1 sigma1 ind) (G_sign lid2 sigma2 _) = do
Comorphism i <- logicInclusion logicGraph (Logic lid1) (Logic lid2)
sigma1' <- coerceSign lid1 (sourceLogic i) "Inclusion of signatures" sigma1
(sigma1'',_) <- map_sign i sigma1'
sigma2' <- coerceSign lid2 (targetLogic i) "Inclusion of signatures" sigma2
mor <- inclusion (targetLogic i) sigma1'' sigma2'
return (GMorphism i sigma1' ind mor 0)
-- | Composition of two Grothendieck signature morphisms
-- | with itermediate inclusion
compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
compInclusion lg mor1 mor2 = do
let sigma1 = cod Grothendieck mor1
sigma2 = dom Grothendieck mor2
unless (isSubGsign lg sigma1 sigma2)
incl <- ginclusion lg sigma1 sigma2
mor <- comp Grothendieck mor1 incl
comp Grothendieck mor mor2
-- | Composition of two Grothendieck signature morphisms
-- | with intermediate homogeneous inclusion
compHomInclusion :: GMorphism -> GMorphism -> Result GMorphism
compHomInclusion mor1 mor2 = compInclusion emptyLogicGraph mor1 mor2
-- | Find all (composites of) comorphisms starting from a given logic
findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
findComorphismPaths lg (G_sublogics lid sub) =
nub $ map fst $ iterateComp (0::Int) [(idc,[idc])]
idc = Comorphism (IdComorphism lid sub)
-- compute possible compositions, but only up to depth 3
iterateComp n l = -- (l::[(AnyComorphism,[AnyComorphism])]) =
if n>3 || l==newL then newL else iterateComp (n+1) newL
newL = nub (l ++ (concat (map extend l)))
-- extend comorphism list in all directions, but no cylces
case compComorphism coMor c of
Just c1 -> Just (c1,c:comps)
in catMaybes $ map addCoMor $ filter (not . (`elem` comps)) $ coMors
-- | finds first comorphism with a matching sublogic
findComorphism ::Monad m => G_sublogics -> [AnyComorphism] -> m AnyComorphism
findComorphism _ [] = fail "No matching comorphism found"
findComorphism gsl@(G_sublogics lid sub) ((Comorphism cid):rest) =
rec = findComorphism gsl rest in
if language_name lid == language_name l2
then if isSubElem (forceCoerceSublogic lid l2 sub) $ sourceSublogic cid
then return $ Comorphism cid
-- | check transpotability of Grothendieck signature morphisms
-- | (currently returns false for heterogeneous morphisms)
isTransportable :: GMorphism -> Bool
isTransportable (GMorphism cid _ ind1 mor ind2) =ind1 > 0 && ind2 > 0 &&
isIdComorphism (Comorphism cid) && is_transportable (targetLogic cid) mor
------------------------------------------------------------------
------------------------------------------------------------------
-- | provers and consistency checkers for specific logics
data G_prover = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_prover lid (Prover sign sentence proof_tree)
(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,
Monad m) => lid1 -> lid2 -> String -> Prover sign1 sentence1 proof_tree1
-> m (Prover sign2 sentence2 proof_tree2)
coerceProver l1 l2 msg m1 = primCoerce l1 l2 msg m1
data G_cons_checker = forall lid sublogics
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree .
basic_spec sentence symb_items symb_map_items
sign morphism symbol raw_symbol proof_tree =>
G_cons_checker lid (ConsChecker sign sentence morphism proof_tree)
(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,
Monad m) => lid1 -> lid2 -> String
-> ConsChecker sign1 sentence1 morphism1 proof_tree1
-> m (ConsChecker sign2 sentence2 morphism2 proof_tree2)
coerceConsChecker l1 l2 msg m1 = primCoerce l1 l2 msg m1
(Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
Monad m) => lid1 -> String -> G_sign -> m sign1
coerceG_sign l1 msg (G_sign l2 sign2 _) = primCoerce l2 l1 msg sign2