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

1178N/A{- |

1178N/AModule : ./Comorphisms/MonadicHasCASLTranslation.hs

1178N/ADescription : translating a HasCASL subset to Isabelle

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

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

1178N/A

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

1178N/AStability : provisional

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

1178N/A

1178N/AThe embedding comorphism from HasCASL without subtypes to

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

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

1178N/A-}

1178N/A

1178N/Amodule Comorphisms.MonadicHasCASLTranslation

2362N/A (MonadicHasCASL2IsabelleHOL (..)) where

2362N/A

2362N/Aimport Comorphisms.PPolyTyConsHOL2IsaUtils

1178N/Aimport Logic.Logic as Logic

4169N/Aimport Logic.Comorphism

1178N/A

1178N/Aimport HasCASL.Logic_HasCASL

4033N/Aimport HasCASL.Sublogic

4033N/Aimport HasCASL.As

0N/Aimport HasCASL.Le as Le

1178N/A

1178N/Aimport Isabelle.IsaSign as Isa

1178N/Aimport Isabelle.Logic_Isabelle

4033N/A

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

1178N/Adata MonadicHasCASL2IsabelleHOL = MonadicHasCASL2IsabelleHOL deriving Show

4033N/A

1178N/Ainstance Language MonadicHasCASL2IsabelleHOL where

1178N/A language_name MonadicHasCASL2IsabelleHOL = "MonadicTranslation"

4033N/A

1178N/Ainstance Comorphism MonadicHasCASL2IsabelleHOL

1178N/A HasCASL Sublogic

4033N/A BasicSpec Le.Sentence SymbItems SymbMapItems

1178N/A Env Morphism

1178N/A Symbol RawSymbol ()

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

4033N/A Isa.Sign

1178N/A IsabelleMorphism () () () where

1178N/A sourceLogic MonadicHasCASL2IsabelleHOL = HasCASL

1178N/A sourceSublogic MonadicHasCASL2IsabelleHOL = noSubtypes

1178N/A targetLogic MonadicHasCASL2IsabelleHOL = Isabelle

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

1178N/A then Just () else Nothing

1178N/A map_theory MonadicHasCASL2IsabelleHOL =

1178N/A mapTheory (Old NoSimpLift) simpForOption

1178N/A map_sentence MonadicHasCASL2IsabelleHOL sign =

1178N/A transSentence sign (typeToks sign) (Old NoSimpLift) simpForOption

0N/A isInclusionComorphism MonadicHasCASL2IsabelleHOL = True

1178N/A has_model_expansion MonadicHasCASL2IsabelleHOL = True

1178N/A