4751N/A{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

4751N/A{- |

4751N/AModule : ./Comorphisms/PCoClTyConsHOL2IsabelleHOL.hs

4751N/ADescription : translating a HasCASL subset to Isabelle

4751N/ACopyright : (c) C. Maeder, DFKI 2006

4751N/ALicense : GPLv2 or higher, see LICENSE.txt

4751N/A

4751N/AMaintainer : Christian.Maeder@dfki.de

4751N/AStability : provisional

4751N/APortability : non-portable (imports Logic.Logic)

4751N/A

4751N/AThe embedding comorphism from HasCASL without subtypes to

4751N/AIsabelle-HOL. Partial functions yield an option or bool result in

4751N/AIsabelle. Case-terms and constructor classes are not supported yet.

4751N/A-}

4751N/A

4751N/Amodule Comorphisms.PCoClTyConsHOL2IsabelleHOL

4751N/A (PCoClTyConsHOL2IsabelleHOL (..)) where

4751N/A

4751N/Aimport Comorphisms.PPolyTyConsHOL2IsaUtils

4751N/Aimport Logic.Logic as Logic

4751N/Aimport Logic.Comorphism

4751N/A

4751N/Aimport HasCASL.Logic_HasCASL

4751N/Aimport HasCASL.Sublogic

5061N/Aimport HasCASL.As

5821N/Aimport HasCASL.Le as Le

4751N/A

4751N/Aimport Isabelle.IsaSign as Isa

4751N/Aimport Isabelle.Logic_Isabelle

4751N/A

4751N/A-- | The identity of the comorphism

4751N/Adata PCoClTyConsHOL2IsabelleHOL = PCoClTyConsHOL2IsabelleHOL deriving Show

4751N/A

4751N/Ainstance Language PCoClTyConsHOL2IsabelleHOL where

4751N/A language_name PCoClTyConsHOL2IsabelleHOL = "HasCASL2IsabelleOption"

4751N/A

4751N/Ainstance Comorphism PCoClTyConsHOL2IsabelleHOL

4751N/A HasCASL Sublogic

4751N/A BasicSpec Le.Sentence SymbItems SymbMapItems

4751N/A Env Morphism

4751N/A Symbol RawSymbol ()

4751N/A Isabelle () () Isa.Sentence () ()

4751N/A Isa.Sign

4751N/A IsabelleMorphism () () () where

4751N/A sourceLogic PCoClTyConsHOL2IsabelleHOL = HasCASL

4751N/A sourceSublogic PCoClTyConsHOL2IsabelleHOL = noSubtypes

4751N/A targetLogic PCoClTyConsHOL2IsabelleHOL = Isabelle

4751N/A mapSublogic cid sl = if sl `isSubElem` sourceSublogic cid

4751N/A then Just () else Nothing

4751N/A map_theory PCoClTyConsHOL2IsabelleHOL =

4751N/A mapTheory (Old Lift2Case) simpForOption

4751N/A map_sentence PCoClTyConsHOL2IsabelleHOL sign =

4751N/A transSentence sign (typeToks sign) (Old Lift2Case) simpForOption

4751N/A isInclusionComorphism PCoClTyConsHOL2IsabelleHOL = True

4751N/A has_model_expansion PCoClTyConsHOL2IsabelleHOL = True

4751N/A