content: {-# LANGUAGE CPP #-}
  {- |
  Module      :  ./Isabelle/CreateTheories.hs
  Description :  creating Isabelle thoeries via translations
  Copyright   :  (c) C. Maeder, Uni Bremen 2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable(Logic)
  
  dumping a LibEnv to Isabelle theory files
  -}
  
  module Isabelle.CreateTheories where
  
  import Common.Result
  import Common.AS_Annotation
  import Logic.Coerce
  import Logic.Comorphism
  
  import Static.GTheory
  import Logic.Prover
  
  import Common.ExtSign
  import Common.ProofUtils
  import Isabelle.IsaSign
  import Isabelle.Translate
  import Isabelle.Logic_Isabelle
  
  import CASL.Logic_CASL
  import HasCASL.Logic_HasCASL
  
  import Comorphisms.CASL2PCFOL
  import Comorphisms.CASL2HasCASL
  import Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
  import Comorphisms.HasCASL2PCoClTyConsHOL
  #ifdef PROGRAMATICA
  import Comorphisms.Haskell2IsabelleHOLCF
  import Haskell.Logic_Haskell
  #endif
  
  createIsaTheory :: G_theory -> Result (Sign, [Named Sentence])
  createIsaTheory (G_theory lid _ (ExtSign sign0 _) _ sens0 _) = do
      let th = (sign0, toNamedList sens0)
          r1 = coerceBasicTheory lid CASL "" th
          r1' = do
            th0 <- r1
            th1 <- wrapMapTheory CASL2PCFOL th0
            th2 <- wrapMapTheory CASL2HasCASL th1
            wrapMapTheory PCoClTyConsHOL2PairsInIsaHOL th2
  #ifdef PROGRAMATICA
          r2 = coerceBasicTheory lid Haskell "" th
          r2' = do
            th0 <- r2
            wrapMapTheory Haskell2IsabelleHOLCF th0
  #else
          r2 = r1
          r2' = r1'
  #endif
          r4 = coerceBasicTheory lid HasCASL "" th
          r4' = do
            th0 <- r4
            th1 <- wrapMapTheory HasCASL2PCoClTyConsHOL th0
            wrapMapTheory PCoClTyConsHOL2PairsInIsaHOL th1
          r5 = coerceBasicTheory lid Isabelle "" th
          r3 = case maybeResult r1 of
                 Nothing -> case maybeResult r2 of
                     Nothing -> case maybeResult r4 of
                         Nothing -> r5
                         _ -> r4'
                     _ -> r2'
                 _ -> r1'
      (sign, sens) <- r3
      return (sign, prepareSenNames transString $ toNamedList $ toThSens sens)
  