{-# 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
#ifdef PROGRAMATICA
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)