05bf9cbe382548c2665dd01a6a402640c9ec3813Christian Maeder{- |

eceb9606af609acfa431c3203484317c55ce8b35Ewaryst SchulzModule : $Header$

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) C. Maeder, Uni Bremen 2006

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuMaintainer : maeder@tzi.de

26db4a742376d513cdba128780ee8ca60eeb927eTill MossakowskiStability : provisional

f1edf379717f0ddb7607585a027cf6f03a6fce68Christian MaederPortability : non-portable(Logic)

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskidumping a LibEnv to a Haskell module

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski-}

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskimodule Haskell.CreateModules where

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowski

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Common.Result

316fe96124dce26bfbc374b2f82c23fadcf2fa8bChristian Maederimport Common.Doc

26db4a742376d513cdba128780ee8ca60eeb927eTill Mossakowskiimport Common.DocUtils

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maeder

e16b3696b2c173aac14200321868ed81b8f7dc69Christian Maederimport Logic.Coerce

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Logic.Comorphism

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Static.DevGraph

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Logic.Prover

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport CASL.Logic_CASL

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport HasCASL.Logic_HasCASL

d54cd08a4cfa26256c38d8ed12c343adbfe1a0e3Christian Maeder

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Comorphisms.HasCASL2Haskell

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Comorphisms.CASL2HasCASL

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport Comorphisms.HasCASL2HasCASL

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeprintModule :: G_theory -> Maybe Doc

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeprintModule (G_theory lid sign0 sens0) =

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke let th = (sign0, toNamedList sens0)

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke r1 = do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke th0 <- coerceBasicTheory lid CASL "" th

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke th1 <- map_theory CASL2HasCASL th0

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke th2 <- map_theory HasCASL2HasCASL th1

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke map_theory HasCASL2Haskell th2

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke r2 = do

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke th0 <- coerceBasicTheory lid HasCASL "" th

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke th2 <- map_theory HasCASL2HasCASL th0

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke map_theory HasCASL2Haskell th2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder r3 = case maybeResult r1 of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> r2

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder _ -> r1

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in case maybeResult r3 of

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Nothing -> Nothing

a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder Just (_, sens) -> Just $

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke vcat $ map pretty $ toNamedList $ toThSens sens

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke

9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke