content: {- |
  Module      :  ./Haskell/CreateModules.hs
  Description :  creating Haskell modules via translations
  Copyright   :  (c) C. Maeder, Uni Bremen 2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  dumping a LibEnv to a Haskell module
  -}
  
  module Haskell.CreateModules where
  
  import Common.Result
  import Common.ExtSign
  import Common.Doc
  
  import Logic.Coerce
  import Logic.Logic
  import Logic.Comorphism
  import Static.GTheory
  import Logic.Prover
  
  import CASL.Logic_CASL
  import HasCASL.Logic_HasCASL
  import Haskell.Logic_Haskell
  
  import Comorphisms.HasCASL2Haskell
  import Comorphisms.CASL2HasCASL
  import Comorphisms.HasCASL2HasCASL
  
  printModule :: G_theory -> Maybe Doc
  printModule (G_theory lid _ (ExtSign sign0 _) _ sens0 _) =
                  let th = (sign0, toNamedList sens0)
                      r1 = do
                        th0 <- coerceBasicTheory lid CASL "" th
                        th1 <- wrapMapTheory CASL2HasCASL th0
                        th2 <- wrapMapTheory HasCASL2HasCASL th1
                        wrapMapTheory HasCASL2Haskell th2
                      r2 = do
                        th0 <- coerceBasicTheory lid HasCASL "" th
                        th2 <- wrapMapTheory HasCASL2HasCASL th0
                        wrapMapTheory HasCASL2Haskell th2
                      r3 = case maybeResult r1 of
                           Nothing -> r2
                           _ -> r1
                  in case maybeResult r3 of
                     Nothing -> Nothing
                     Just (_, sens) -> Just $
                         vcat $ map (print_named Haskell) sens
  