content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  ./Comorphisms/PCoClTyConsHOL2PairsInIsaHOL.hs
  Description :  normalising translation of a HasCASL subset to Isabelle
  Copyright   :  (c) C. Maeder, DFKI 2006
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  An embedding comorphism from HasCASL without subtypes to
  Isabelle-HOL.
  -}
  
  module Comorphisms.PCoClTyConsHOL2PairsInIsaHOL
      (PCoClTyConsHOL2PairsInIsaHOL (..)) where
  
  import Comorphisms.PPolyTyConsHOL2IsaUtils
  import Logic.Logic as Logic
  import Logic.Comorphism
  
  import HasCASL.Logic_HasCASL
  import HasCASL.Sublogic
  import HasCASL.As
  import HasCASL.Le as Le
  
  import Isabelle.IsaSign as Isa
  import Isabelle.Logic_Isabelle
  
  -- | The identity of the comorphism
  data PCoClTyConsHOL2PairsInIsaHOL = PCoClTyConsHOL2PairsInIsaHOL deriving Show
  
  instance Language PCoClTyConsHOL2PairsInIsaHOL where
    language_name PCoClTyConsHOL2PairsInIsaHOL = "NormalisingTranslation"
  
  instance Comorphism PCoClTyConsHOL2PairsInIsaHOL
                 HasCASL Sublogic
                 BasicSpec Le.Sentence SymbItems SymbMapItems
                 Env Morphism
                 Symbol RawSymbol ()
                 Isabelle () () Isa.Sentence () ()
                 Isa.Sign
                 IsabelleMorphism () () () where
      sourceLogic PCoClTyConsHOL2PairsInIsaHOL = HasCASL
      sourceSublogic PCoClTyConsHOL2PairsInIsaHOL = noSubtypes
      targetLogic PCoClTyConsHOL2PairsInIsaHOL = Isabelle
      mapSublogic cid sl = if sl `isSubElem` sourceSublogic cid
                         then Just () else Nothing
      map_theory PCoClTyConsHOL2PairsInIsaHOL th = do
        (sig, sens) <- mapTheory New simpForOption th
        return (sig { baseSig = MainHC_thy }, sens)
      map_sentence PCoClTyConsHOL2PairsInIsaHOL sign =
         transSentence sign (typeToks sign) New simpForOption
      isInclusionComorphism PCoClTyConsHOL2PairsInIsaHOL = True
      has_model_expansion PCoClTyConsHOL2PairsInIsaHOL = True
  