{-# 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 -> Result (Sign, [Named Sentence])
createIsaTheory (G_theory lid :: lid
lid _ (ExtSign sign0 :: sign
sign0 _) _ sens0 :: ThSens sentence (AnyComorphism, BasicProof)
sens0 _) = do
    let th :: (sign, [Named sentence])
th = (sign
sign0, ThSens sentence (AnyComorphism, BasicProof) -> [Named sentence]
forall a b. ThSens a b -> [Named a]
toNamedList ThSens sentence (AnyComorphism, BasicProof)
sens0)
        r1 :: Result (CASLSign, [Named CASLFORMULA])
r1 = lid
-> CASL
-> String
-> (sign, [Named sentence])
-> Result (CASLSign, [Named CASLFORMULA])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid CASL
CASL "" (sign, [Named sentence])
th
        r1' :: Result (Sign, [Named Sentence])
r1' = do
          (CASLSign, [Named CASLFORMULA])
th0 <- Result (CASLSign, [Named CASLFORMULA])
r1
          (CASLSign, [Named CASLFORMULA])
th1 <- CASL2PCFOL
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CASL2PCFOL
CASL2PCFOL (CASLSign, [Named CASLFORMULA])
th0
          (Env, [Named Sentence])
th2 <- CASL2HasCASL
-> (CASLSign, [Named CASLFORMULA])
-> Result (Env, [Named Sentence])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory CASL2HasCASL
CASL2HasCASL (CASLSign, [Named CASLFORMULA])
th1
          PCoClTyConsHOL2PairsInIsaHOL
-> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory PCoClTyConsHOL2PairsInIsaHOL
PCoClTyConsHOL2PairsInIsaHOL (Env, [Named Sentence])
th2
#ifdef PROGRAMATICA
        r2 = coerceBasicTheory lid Haskell "" th
        r2' = do
          th0 <- r2
          wrapMapTheory Haskell2IsabelleHOLCF th0
#else
        r2 :: Result (CASLSign, [Named CASLFORMULA])
r2 = Result (CASLSign, [Named CASLFORMULA])
r1
        r2' :: Result (Sign, [Named Sentence])
r2' = Result (Sign, [Named Sentence])
r1'
#endif
        r4 :: Result (Env, [Named Sentence])
r4 = lid
-> HasCASL
-> String
-> (sign, [Named sentence])
-> Result (Env, [Named Sentence])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid HasCASL
HasCASL "" (sign, [Named sentence])
th
        r4' :: Result (Sign, [Named Sentence])
r4' = do
          (Env, [Named Sentence])
th0 <- Result (Env, [Named Sentence])
r4
          (Env, [Named Sentence])
th1 <- HasCASL2PCoClTyConsHOL
-> (Env, [Named Sentence]) -> Result (Env, [Named Sentence])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory HasCASL2PCoClTyConsHOL
HasCASL2PCoClTyConsHOL (Env, [Named Sentence])
th0
          PCoClTyConsHOL2PairsInIsaHOL
-> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2.
Comorphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  symbol1
  raw_symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  symbol2
  raw_symbol2
  proof_tree2 =>
cid
-> (sign1, [Named sentence1]) -> Result (sign2, [Named sentence2])
wrapMapTheory PCoClTyConsHOL2PairsInIsaHOL
PCoClTyConsHOL2PairsInIsaHOL (Env, [Named Sentence])
th1
        r5 :: Result (Sign, [Named Sentence])
r5 = lid
-> Isabelle
-> String
-> (sign, [Named sentence])
-> Result (Sign, [Named Sentence])
forall lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 symbol2 raw_symbol2 proof_tree2 (m :: * -> *).
(Logic
   lid1
   sublogics1
   basic_spec1
   sentence1
   symb_items1
   symb_map_items1
   sign1
   morphism1
   symbol1
   raw_symbol1
   proof_tree1,
 Logic
   lid2
   sublogics2
   basic_spec2
   sentence2
   symb_items2
   symb_map_items2
   sign2
   morphism2
   symbol2
   raw_symbol2
   proof_tree2,
 MonadFail m) =>
lid1
-> lid2
-> String
-> (sign1, [Named sentence1])
-> m (sign2, [Named sentence2])
coerceBasicTheory lid
lid Isabelle
Isabelle "" (sign, [Named sentence])
th
        r3 :: Result (Sign, [Named Sentence])
r3 = case Result (CASLSign, [Named CASLFORMULA])
-> Maybe (CASLSign, [Named CASLFORMULA])
forall a. Result a -> Maybe a
maybeResult Result (CASLSign, [Named CASLFORMULA])
r1 of
               Nothing -> case Result (CASLSign, [Named CASLFORMULA])
-> Maybe (CASLSign, [Named CASLFORMULA])
forall a. Result a -> Maybe a
maybeResult Result (CASLSign, [Named CASLFORMULA])
r2 of
                   Nothing -> case Result (Env, [Named Sentence]) -> Maybe (Env, [Named Sentence])
forall a. Result a -> Maybe a
maybeResult Result (Env, [Named Sentence])
r4 of
                       Nothing -> Result (Sign, [Named Sentence])
r5
                       _ -> Result (Sign, [Named Sentence])
r4'
                   _ -> Result (Sign, [Named Sentence])
r2'
               _ -> Result (Sign, [Named Sentence])
r1'
    (sign :: Sign
sign, sens :: [Named Sentence]
sens) <- Result (Sign, [Named Sentence])
r3
    (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sign, (String -> String) -> [Named Sentence] -> [Named Sentence]
forall a. (String -> String) -> [Named a] -> [Named a]
prepareSenNames String -> String
transString ([Named Sentence] -> [Named Sentence])
-> [Named Sentence] -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ ThSens Sentence Any -> [Named Sentence]
forall a b. ThSens a b -> [Named a]
toNamedList (ThSens Sentence Any -> [Named Sentence])
-> ThSens Sentence Any -> [Named Sentence]
forall a b. (a -> b) -> a -> b
$ [Named Sentence] -> ThSens Sentence Any
forall a b. Ord a => [Named a] -> ThSens a b
toThSens [Named Sentence]
sens)