Coerce.hs revision acabd9ab36e1870f6f02c513bcfbfd10ffd118e0
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceModule : $Header$
5d801400993c9671010d244646936d8fd435638cChristian MaederCopyright : (c) Till Mossakowski, C.Maeder and Uni Bremen 2005
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceMaintainer : till@tzi.de
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceStability : provisional
5d801400993c9671010d244646936d8fd435638cChristian MaederPortability : non-portable (various -fglasgow-exts extensions)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance-- for coercion used in Grothendieck.hs and Analysis modules
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Manceimport qualified Common.Lib.Set as Set
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance-- coercion using the language name
b1162cc13e8371724e3382ae6d1cfdeb43891fbbChristian MaederprimCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Monad m) => lid1 -> lid2 -> String -> a -> m b
ab72ebade3d901d3857bf76626216456b83ebdc6Felix Gabriel ManceprimCoerce i1 i2 err a =
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance if language_name i1 == language_name i2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance then return $ fromDyn (toDyn a) $ error "mcoerce"
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance else fail (err1++"Logic "++ language_name i1 ++ " expected, but "
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance ++ language_name i2 ++ " found")
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance where err1 = if err=="" then "" else err++": "
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceunsafeCoerce :: (Typeable a, Typeable b, Language lid1, Language lid2)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance => lid1 -> lid2 -> a -> b
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel ManceunsafeCoerce i1 i2 a = maybe (error "unsafeCoerce") id $ primCoerce i1 i2 "" a
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecoerceToResult :: (Typeable a, Typeable b, Language lid1, Language lid2) =>
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance lid1 -> lid2 -> Range -> a -> Result b
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel MancecoerceToResult i1 i2 pos a = adjustPos pos $ primCoerce i1 i2 "" a
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecoerceSublogic ::
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
968930c7674ae3b63d308bf4fa651400aa263054Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance => lid1 -> lid2 -> sublogics1 -> sublogics2
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancecoerceSublogic l1 l2 s1 = unsafeCoerce l1 l2 s1
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian Maeder Monad m) => lid1 -> lid2 -> String -> sign1 -> m sign2
fc7bd98aabe1bc26058660085e8c77d60a97bcecChristian MaedercoerceSign l1 l2 msg s1 = primCoerce l1 l2 msg s1
3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel MancecoerceBasicTheory ::
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Monad m) => lid1 -> lid2 -> String
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance -> (sign1, [Named sentence1]) -> m (sign2, [Named sentence2])
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecoerceBasicTheory l1 l2 msg t1 = primCoerce l1 l2 msg t1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecoerceMorphism ::
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Monad m) => lid1 -> lid2 -> String -> morphism1 -> m morphism2
852bd6145634dc2832b61c44678fe539bc1682d5Christian MaedercoerceMorphism l1 l2 msg m1 = primCoerce l1 l2 msg m1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecoerceSymbol ::
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder sign2 morphism2 symbol2 raw_symbol2 proof_tree2)
852bd6145634dc2832b61c44678fe539bc1682d5Christian Maeder => lid1 -> lid2 -> symbol1 -> symbol2
852bd6145634dc2832b61c44678fe539bc1682d5Christian MaedercoerceSymbol l1 l2 s1 = unsafeCoerce l1 l2 s1
ea3f858eb531d981df3ed00beeadd99cf025adecChristian MaedercoerceSymbItemsList ::
ea3f858eb531d981df3ed00beeadd99cf025adecChristian Maeder (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance Monad m) => lid1 -> lid2 -> String -> [symb_items1] -> m [symb_items2]
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel MancecoerceSymbItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel MancecoerceSymbMapItemsList ::
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Monad m) => lid1 -> lid2 -> String
3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel Mance -> [symb_map_items1] -> m [symb_map_items2]
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel MancecoerceSymbMapItemsList l1 l2 msg m1 = primCoerce l1 l2 msg m1
3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel MancecoerceBasicProof ::
3c6b4f79cea11dd2acc2060bf1502b6ba9e905f2Felix Gabriel Mance (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
75aaf82c430ad2a5cf159962b1c5c09255010fb4Felix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance Monad m) => lid1 -> lid2 -> String
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel Mance -> Proof_status proof_tree1 -> m (Proof_status proof_tree2)
ffa6044b04fa0e31242141ff56a5d80c4233b676Felix Gabriel MancecoerceBasicProof l1 l2 msg m1 = primCoerce l1 l2 msg m1
4c684d7a2343be7350eba088f8be42888f86a495Felix Gabriel MancecoerceSymbolSet ::
1b1144abf7f95a4b23405b8d5604813cfe7b036aFelix Gabriel Mance (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
5a3ae0a9224276de25e709ef8788c1b9716cd206Christian Maeder sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
668c9c725a11c0f77057152148570af853a1bc0dFelix Gabriel Mance Monad m) => lid1 -> lid2 -> String -> Set.Set symbol1 -> m (Set.Set symbol2)
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecoerceSymbolSet l1 l2 msg m1 = primCoerce l1 l2 msg m1
c298a419605037f5352b5ad0f67b3e06db094051Felix Gabriel MancecoerceRawSymbolMap ::
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance (Logic lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance Logic lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance sign2 morphism2 symbol2 raw_symbol2 proof_tree2,
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance Monad m) => lid1 -> lid2 -> String -> EndoMap raw_symbol1
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel Mance -> m (EndoMap raw_symbol2)
1b90322eaf59ded3de24fc891bd67bbd73ec2bfaFelix Gabriel MancecoerceRawSymbolMap l1 l2 msg m1 = primCoerce l1 l2 msg m1