43b4c41fbb07705c9df321221ab9cb9832460407Christian Maeder{-# OPTIONS -cpp #-}

c63ebf815c8a874525cf18670ad74847f7fc7b26Christian Maeder{- |

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian MaederModule : $Header$

25cc5fbba63f84b47e389af749f55abbbde71c8cChristian MaederDescription : creating Isabelle thoeries via translations

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederCopyright : (c) C. Maeder, Uni Bremen 2005

43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederMaintainer : Christian.Maeder@dfki.de

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian MaederStability : provisional

43b4c41fbb07705c9df321221ab9cb9832460407Christian MaederPortability : non-portable(Logic)

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maederdumping a LibEnv to Isabelle theory files

f2f9df2e17e70674f0bf426ed1763c973ee4cde0Christian Maeder-}

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maedermodule Isabelle.CreateTheories where

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder

68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maederimport Common.Result

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Common.AS_Annotation

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Logic.Coerce

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Logic.Comorphism

a53841f6d6e86ac751c12a33dc8aadf53f59d977Klaus Luettichimport Logic.ExtSign

a737caf82de97c1907027c03e4b4509eb492b4b8Christian Maeder

68d10d143f29fcff3c637ba24f90e983995ceae6Christian Maederimport Static.GTheory

96646aed2ae087b942ae23f15bbe729a8f7c43d3Christian Maederimport Logic.Prover

01e383014b555bbcf639c0ca60c5810b3eff83c0Christian Maeder

3b06e23643a9f65390cb8c1caabe83fa7e87a708Till Mossakowskiimport Common.ProofUtils

9dac90ec2be2a72e03893095461960d483fe2fc2Christian Maederimport Isabelle.IsaSign

5e5d3e82af3bc2834f8718a52d9f45da80220273Dominik Lueckeimport Isabelle.Translate

7bdc9c0783f9c8c830346e6baeac9306eee1a622Christian Maederimport Isabelle.Logic_Isabelle

ce8b15da31cd181b7e90593cbbca98f47eda29d6Till Mossakowski

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport CASL.Logic_CASL

e7757995211bd395dc79d26fe017d99375f7d2a6Christian Maederimport HasCASL.Logic_HasCASL

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Comorphisms.CASL2PCFOL

a1ed34933c266ce85066acb0d7b20c90cb8eb213Christian Maederimport Comorphisms.CASL2HasCASL

c0c2380bced8159ff0297ece14eba948bd236471Christian Maederimport Comorphisms.PCoClTyConsHOL2IsabelleHOL

8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport Comorphisms.HasCASL2PCoClTyConsHOL

6a79849bed67264c396dddb3e9c184bdfc1a1bc9Christian Maeder#ifdef PROGRAMATICA

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maederimport Comorphisms.Haskell2IsabelleHOLCF

8410667510a76409aca9bb24ff0eda0420088274Christian Maederimport Haskell.Logic_Haskell

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich#endif

b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder

ad270004874ce1d0697fb30d7309f180553bb315Christian MaedercreateIsaTheory :: G_theory -> Result (Sign, [Named Sentence])

4d56f2fa72e4aec20eb827c11ed49c8cbb7014bdChristian MaedercreateIsaTheory (G_theory lid (ExtSign sign0 _) _ sens0 _) = do

4cb215739e9ab13447fa21162482ebe485b47455Christian Maeder let th = (sign0, toNamedList sens0)

8ef75f1cc0437656bf622cec5ac9e8ea221da8f2Christian Maeder r1 = coerceBasicTheory lid CASL "" th

404166b9366552e9ec5abb87a37c76ec8a815fb7Klaus Luettich r1' = do

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder th0 <- r1

356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder th1 <- wrapMapTheory CASL2PCFOL th0

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder th2 <- wrapMapTheory CASL2HasCASL th1

55adfe57a4de1f36adc3e3bfc16f342e44a7d444Christian Maeder wrapMapTheory PCoClTyConsHOL2IsabelleHOL th2

d23b0cc79c0d204e6ec758dff8d0ba71c9f693f7Christian Maeder#ifdef PROGRAMATICA

8d97ef4f234681b11bb5924bd4d03adef858d2d2Christian Maeder r2 = coerceBasicTheory lid Haskell "" th

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder r2' = do

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder th0 <- r2

e593b89bfd4952698dc37feced21cefe869d87a2Christian Maeder wrapMapTheory Haskell2IsabelleHOLCF th0

63f0e65a37b95621334db9ee4ba0cd9d826f5c0fChristian Maeder#else

5191fa24c532d1f67e7a642e9aece65efb8a0975Christian Maeder r2 = r1

7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder r2' = r1'

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder#endif

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder r4 = coerceBasicTheory lid HasCASL "" th

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder r4' = do

f041c9a6bda23de33a38490e35b831ae18d96b45Christian Maeder th0 <- r4

7cc09dd93962a2155c34d209d1d4cd7d7b838264Christian Maeder th1 <- wrapMapTheory HasCASL2PCoClTyConsHOL th0

51d769d55d88dfa88bdf54bee78d8fa85a2deba8Christian Maeder wrapMapTheory PCoClTyConsHOL2IsabelleHOL th1

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder r5 = coerceBasicTheory lid Isabelle "" th

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder r3 = case maybeResult r1 of

c3053d57f642ca507cdf79512e604437c4546cb9Christian Maeder Nothing -> case maybeResult r2 of

dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder Nothing -> case maybeResult r4 of

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder Nothing -> r5

f4a2a20e49f41b2afa657e5e64d9e349c7faa091Christian Maeder _ -> r4'

dcbd32289a7bdf1e6edd06c6ab0698c6a9dbf37aChristian Maeder _ -> r2'

d0279930f87bf39843e0bd2992a4789322662144Christian Maeder _ -> r1'

c2fcc35abb03cf0b4ca4b050efeb10827f38c322Christian Maeder (sign, sens) <- r3

1aee4aaddde105264c1faf394d88e302c05094ffChristian Maeder return (sign, prepareSenNames transString $ toNamedList $ toThSens sens)

356fa49fe3e6a8398f92d13e9f920d0f093697ecChristian Maeder