{-# 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 Int -> PCoClTyConsHOL2PairsInIsaHOL -> ShowS
[PCoClTyConsHOL2PairsInIsaHOL] -> ShowS
PCoClTyConsHOL2PairsInIsaHOL -> String
(Int -> PCoClTyConsHOL2PairsInIsaHOL -> ShowS)
-> (PCoClTyConsHOL2PairsInIsaHOL -> String)
-> ([PCoClTyConsHOL2PairsInIsaHOL] -> ShowS)
-> Show PCoClTyConsHOL2PairsInIsaHOL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [PCoClTyConsHOL2PairsInIsaHOL] -> ShowS
$cshowList :: [PCoClTyConsHOL2PairsInIsaHOL] -> ShowS
show :: PCoClTyConsHOL2PairsInIsaHOL -> String
$cshow :: PCoClTyConsHOL2PairsInIsaHOL -> String
showsPrec :: Int -> PCoClTyConsHOL2PairsInIsaHOL -> ShowS
$cshowsPrec :: Int -> PCoClTyConsHOL2PairsInIsaHOL -> ShowS
Show

instance Language PCoClTyConsHOL2PairsInIsaHOL where
  language_name :: PCoClTyConsHOL2PairsInIsaHOL -> String
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
sourceLogic PCoClTyConsHOL2PairsInIsaHOL = HasCASL
HasCASL
    sourceSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic
sourceSublogic PCoClTyConsHOL2PairsInIsaHOL = Sublogic
noSubtypes
    targetLogic :: PCoClTyConsHOL2PairsInIsaHOL -> Isabelle
targetLogic PCoClTyConsHOL2PairsInIsaHOL = Isabelle
Isabelle
    mapSublogic :: PCoClTyConsHOL2PairsInIsaHOL -> Sublogic -> Maybe ()
mapSublogic cid :: PCoClTyConsHOL2PairsInIsaHOL
cid sl :: Sublogic
sl = if Sublogic
sl Sublogic -> Sublogic -> Bool
forall l. SemiLatticeWithTop l => l -> l -> Bool
`isSubElem` PCoClTyConsHOL2PairsInIsaHOL -> Sublogic
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 -> sublogics1
sourceSublogic PCoClTyConsHOL2PairsInIsaHOL
cid
                       then () -> Maybe ()
forall a. a -> Maybe a
Just () else Maybe ()
forall a. Maybe a
Nothing
    map_theory :: PCoClTyConsHOL2PairsInIsaHOL
-> (Env, [Named Sentence]) -> Result (Sign, [Named Sentence])
map_theory PCoClTyConsHOL2PairsInIsaHOL th :: (Env, [Named Sentence])
th = do
      (sig :: Sign
sig, sens :: [Named Sentence]
sens) <- SimpKind
-> Simplifier
-> (Env, [Named Sentence])
-> Result (Sign, [Named Sentence])
mapTheory SimpKind
New Simplifier
simpForOption (Env, [Named Sentence])
th
      (Sign, [Named Sentence]) -> Result (Sign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
sig { baseSig :: BaseSig
baseSig = BaseSig
MainHC_thy }, [Named Sentence]
sens)
    map_sentence :: PCoClTyConsHOL2PairsInIsaHOL -> Env -> Sentence -> Result Sentence
map_sentence PCoClTyConsHOL2PairsInIsaHOL sign :: Env
sign =
       Env
-> Set String
-> SimpKind
-> Simplifier
-> Sentence
-> Result Sentence
transSentence Env
sign (Env -> Set String
typeToks Env
sign) SimpKind
New Simplifier
simpForOption
    isInclusionComorphism :: PCoClTyConsHOL2PairsInIsaHOL -> Bool
isInclusionComorphism PCoClTyConsHOL2PairsInIsaHOL = Bool
True
    has_model_expansion :: PCoClTyConsHOL2PairsInIsaHOL -> Bool
has_model_expansion PCoClTyConsHOL2PairsInIsaHOL = Bool
True