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.PCoClTyConsHOL2IsabelleHOL

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 PCoClTyConsHOL2IsabelleHOL = PCoClTyConsHOL2IsabelleHOL

Documentation

data PCoClTyConsHOL2IsabelleHOL Source #

The identity of the comorphism

Constructors

PCoClTyConsHOL2IsabelleHOL

Instances

Instances details

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