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)
Safe Haskell	None

Comorphisms.MonadicHasCASLTranslation

Description

The embedding comorphism from HasCASL without subtypes to Isabelle-HOL. Partial functions yield an option or bool result in Isabelle. Case-terms and constructor classes are not supported yet.

Synopsis

data MonadicHasCASL2IsabelleHOL = MonadicHasCASL2IsabelleHOL

Documentation

data MonadicHasCASL2IsabelleHOL Source #

The identity of the comorphism

Constructors

MonadicHasCASL2IsabelleHOL

Instances

Instances details

Show MonadicHasCASL2IsabelleHOL Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods showsPrec :: Int -> MonadicHasCASL2IsabelleHOL -> ShowS show :: MonadicHasCASL2IsabelleHOL -> String showList :: [MonadicHasCASL2IsabelleHOL] -> ShowS
Language MonadicHasCASL2IsabelleHOL Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods language_name :: MonadicHasCASL2IsabelleHOL -> String Source # description :: MonadicHasCASL2IsabelleHOL -> String Source #
Comorphism MonadicHasCASL2IsabelleHOL HasCASL Sublogic BasicSpec Sentence SymbItems SymbMapItems Env Morphism Symbol RawSymbol () Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.MonadicHasCASLTranslation Methods sourceLogic :: MonadicHasCASL2IsabelleHOL -> HasCASL Source # sourceSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # sourceSublogicLossy :: MonadicHasCASL2IsabelleHOL -> Sublogic Source # minSourceTheory :: MonadicHasCASL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: MonadicHasCASL2IsabelleHOL -> Isabelle Source # mapSublogic :: MonadicHasCASL2IsabelleHOL -> Sublogic -> Maybe () Source # map_theory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: MonadicHasCASL2IsabelleHOL -> (Env, [Named Sentence0]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: MonadicHasCASL2IsabelleHOL -> Morphism -> Result IsabelleMorphism Source # map_sentence :: MonadicHasCASL2IsabelleHOL -> Env -> Sentence0 -> Result Sentence Source # map_symbol :: MonadicHasCASL2IsabelleHOL -> Env -> Symbol -> Set () Source # extractModel :: MonadicHasCASL2IsabelleHOL -> Env -> () -> Result (Env, [Named Sentence0]) Source # is_model_transportable :: MonadicHasCASL2IsabelleHOL -> Bool Source # has_model_expansion :: MonadicHasCASL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: MonadicHasCASL2IsabelleHOL -> Bool Source # constituents :: MonadicHasCASL2IsabelleHOL -> [String] Source # isInclusionComorphism :: MonadicHasCASL2IsabelleHOL -> Bool Source # rps :: MonadicHasCASL2IsabelleHOL -> Bool Source # eps :: MonadicHasCASL2IsabelleHOL -> Bool Source # isGTC :: MonadicHasCASL2IsabelleHOL -> Bool Source #