4141N/A{- |

4141N/AModule : $Header$

4141N/ACopyright : (c) C. Maeder, Uni Bremen 2006

4141N/ALicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4141N/A

4141N/AMaintainer : maeder@tzi.de

4141N/AStability : provisional

4141N/APortability : non-portable(Logic)

4141N/A

4141N/Adumping a LibEnv to a Haskell module

4141N/A-}

4141N/A

4141N/Amodule Haskell.CreateModules where

4141N/A

4141N/Aimport Common.Result

4141N/Aimport Common.Doc

4141N/A

4141N/Aimport Logic.Coerce

4141N/Aimport Logic.Comorphism

4141N/A

4141N/Aimport Static.DevGraph

4141N/Aimport Logic.Prover

4141N/A

4141N/Aimport CASL.Logic_CASL

4141N/Aimport HasCASL.Logic_HasCASL

4141N/A

4141N/Aimport Comorphisms.HasCASL2Haskell

4141N/Aimport Comorphisms.CASL2HasCASL

4141N/Aimport Comorphisms.HasCASL2HasCASL

4141N/A

4141N/AprintModule :: G_theory -> Maybe Doc

4141N/AprintModule (G_theory lid sign0 sens0) =

4141N/A let th = (sign0, toNamedList sens0)

4141N/A r1 = do

4141N/A th0 <- coerceBasicTheory lid CASL "" th

4141N/A th1 <- map_theory CASL2HasCASL th0

4141N/A th2 <- map_theory HasCASL2HasCASL th1

4141N/A map_theory HasCASL2Haskell th2

4141N/A r2 = do

4141N/A th0 <- coerceBasicTheory lid HasCASL "" th

4141N/A th2 <- map_theory HasCASL2HasCASL th0

4141N/A map_theory HasCASL2Haskell th2

4141N/A r3 = case maybeResult r1 of

4141N/A Nothing -> r2

4141N/A _ -> r1

4141N/A in case maybeResult r3 of

4141N/A Nothing -> Nothing

4141N/A Just (_, sens) -> Just $

4141N/A vcat $ map pretty $ toNamedList $ toThSens sens

4141N/A

4141N/A