2665d7759e63acff0bcd4135678f2cc6f2041d46Christian Maeder{-# LANGUAGE CPP #-}
b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder{- |
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerModule : ./Isabelle/CreateTheories.hs
e1f395fef7ea8b00a675a330e5461fad35158ca5Christian MaederDescription : creating Isabelle thoeries via translations
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian MaederCopyright : (c) C. Maeder, Uni Bremen 2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maeder
6c3404f178e77b7951d20c2d51de765c63dc1912Christian MaederMaintainer : Christian.Maeder@dfki.de
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian MaederStability : provisional
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian MaederPortability : non-portable(Logic)
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maeder
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maederdumping a LibEnv to Isabelle theory files
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maeder-}
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maeder
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maedermodule Isabelle.CreateTheories where
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maeder
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maederimport Common.Result
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport Common.AS_Annotation
7bf4436b6f9987b070033a323757b206c898c1beChristian Maederimport Logic.Coerce
028b461babeae0507b583c6f3021bf763d22f92bChristian Maederimport Logic.Comorphism
028b461babeae0507b583c6f3021bf763d22f92bChristian Maeder
1842453990fed8a1bd7a5ac792d7982c1d2bfcd5Christian Maederimport Static.GTheory
9603ad7198b72e812688ad7970e4eac4b553837aKlaus Luettichimport Logic.Prover
028b461babeae0507b583c6f3021bf763d22f92bChristian Maeder
f9e0b18852b238ddb649d341194e05d7200d1bbeChristian Maederimport Common.ExtSign
b6a54d7292d7a3713000847334de4316d105f40fChristian Maederimport Common.ProofUtils
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maederimport Isabelle.IsaSign
b6a54d7292d7a3713000847334de4316d105f40fChristian Maederimport Isabelle.Translate
1b3be21e14d65a0c22f35b6f2c540b9a12e55909Christian Maederimport Isabelle.Logic_Isabelle
028b461babeae0507b583c6f3021bf763d22f92bChristian Maeder
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maederimport CASL.Logic_CASL
0c6c67747ce3bf27f438537ccd7732483e68e1c9Christian Maederimport HasCASL.Logic_HasCASL
84d0842e67266a0f7c96ea4caddb6b8e8ac6d2baChristian Maeder
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maederimport Comorphisms.CASL2PCFOL
447d46e1d013a01d2be3e3a6a72c6b8dddd1dc89Christian Maederimport Comorphisms.CASL2HasCASL
5f5dfe16ad4651001fbc45d36ebf1e1f8be00c0eChristian Maederimport Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
b4429078c8295c7d5bf7734a4f72ae7d92d06d7eChristian Maederimport Comorphisms.HasCASL2PCoClTyConsHOL
84d0842e67266a0f7c96ea4caddb6b8e8ac6d2baChristian Maeder#ifdef PROGRAMATICA
33cf9048c095bd1bc7d85dbe07b937812a1319c2Paolo Torriniimport Comorphisms.Haskell2IsabelleHOLCF
84d0842e67266a0f7c96ea4caddb6b8e8ac6d2baChristian Maederimport Haskell.Logic_Haskell
84d0842e67266a0f7c96ea4caddb6b8e8ac6d2baChristian Maeder#endif
a1e0b7d38a38c77086142f736addbd40cc92de0fChristian Maeder
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian MaedercreateIsaTheory :: G_theory -> Result (Sign, [Named Sentence])
c1d06b3018b34ede2b3fb6c7fe2ad28cd5ce5b68Christian MaedercreateIsaTheory (G_theory lid _ (ExtSign sign0 _) _ sens0 _) = do
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder let th = (sign0, toNamedList sens0)
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r1 = coerceBasicTheory lid CASL "" th
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r1' = do
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder th0 <- r1
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder th1 <- wrapMapTheory CASL2PCFOL th0
447d46e1d013a01d2be3e3a6a72c6b8dddd1dc89Christian Maeder th2 <- wrapMapTheory CASL2HasCASL th1
5f5dfe16ad4651001fbc45d36ebf1e1f8be00c0eChristian Maeder wrapMapTheory PCoClTyConsHOL2PairsInIsaHOL th2
b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder#ifdef PROGRAMATICA
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r2 = coerceBasicTheory lid Haskell "" th
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r2' = do
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder th0 <- r2
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder wrapMapTheory Haskell2IsabelleHOLCF th0
b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder#else
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r2 = r1
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r2' = r1'
84d0842e67266a0f7c96ea4caddb6b8e8ac6d2baChristian Maeder#endif
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r4 = coerceBasicTheory lid HasCASL "" th
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r4' = do
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder th0 <- r4
b4429078c8295c7d5bf7734a4f72ae7d92d06d7eChristian Maeder th1 <- wrapMapTheory HasCASL2PCoClTyConsHOL th0
5f5dfe16ad4651001fbc45d36ebf1e1f8be00c0eChristian Maeder wrapMapTheory PCoClTyConsHOL2PairsInIsaHOL th1
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r5 = coerceBasicTheory lid Isabelle "" th
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder r3 = case maybeResult r1 of
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder Nothing -> case maybeResult r2 of
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder Nothing -> case maybeResult r4 of
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder Nothing -> r5
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder _ -> r4'
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder _ -> r2'
4cd978f7cad8579ed812ebb7a089dd5d5e6b525bChristian Maeder _ -> r1'
447d46e1d013a01d2be3e3a6a72c6b8dddd1dc89Christian Maeder (sign, sens) <- r3
ab9b86500ed66416e1a7c01be54491ed72c7d633Christian Maeder return (sign, prepareSenNames transString $ toNamedList $ toThSens sens)