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