Copyright | (c) T. Mossakowski, C. Maeder, Uni Bremen 2005-2006 |
---|---|
License | GPLv2 or higher, see LICENSE.txt |
Maintainer | till@informatik.uni-bremen.de |
Stability | provisional |
Portability | non-portable (various -fglasgow-exts extensions) |
Safe Haskell | None |
Functions for coercion used in Grothendieck.hs and Analysis modules: These tell the typechecker that things dynamically belong to the same logic
Documentation
primCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2, Monad m) => lid1 -> lid2 -> String -> a -> m b
unsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2) => lid1 -> lid2 -> a -> b
coerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) => lid1 -> lid2 -> Range -> a -> Result b
coerceSublogic :: (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 -> sublogics1 -> m sublogics2
forceCoerceSublogic :: (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) => lid1 -> lid2 -> sublogics1 -> sublogics2
coercePlainSign :: (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 -> sign1 -> m sign2
coerceSign :: (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 -> ExtSign sign1 symbol1 -> m (ExtSign sign2 symbol2)
coerceBasicTheory :: (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 -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
coerceTheoryMorphism :: (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 -> TheoryMorphism sign1 sentence1 morphism1 proof_tree1 -> m (TheoryMorphism sign2 sentence2 morphism2 proof_tree2)
coerceSens :: (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 -> [Named sentence1] -> m [Named sentence2]
coerceMorphism :: (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 -> morphism1 -> m morphism2
coerceSymbol :: (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) => lid1 -> lid2 -> symbol1 -> symbol2
coerceSymbolmap :: (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, Typeable a) => lid1 -> lid2 -> Map symbol1 a -> Map symbol2 a
coerceMapofsymbol :: (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, Typeable a) => lid1 -> lid2 -> Map a symbol1 -> Map a symbol2
coerceSymbItemsList :: (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 -> [symb_items1] -> m [symb_items2]
coerceSymbMapItemsList :: (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 -> [symb_map_items1] -> m [symb_map_items2]
coerceProofStatus :: (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 -> ProofStatus proof_tree1 -> m (ProofStatus proof_tree2)
coerceSymbolSet :: (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 -> Set symbol1 -> m (Set symbol2)
coerceRawSymbolMap :: (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 -> EndoMap raw_symbol1 -> m (EndoMap raw_symbol2)
coerceFreeDefMorphism :: (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 -> FreeDefMorphism sentence1 morphism1 -> m (FreeDefMorphism sentence2 morphism2)