Copyright	(c) Till Mossakowski and Uni Bremen 2003-2005
License	GPLv2 or higher, see LICENSE.txt
Maintainer	Christian.Maeder@dfki.de
Stability	provisional
Portability	non-portable (imports Logic.Logic)
Safe Haskell	None

Comorphisms.CFOL2IsabelleHOL

Description

The embedding comorphism from CASL to Isabelle-HOL.

Synopsis

data CFOL2IsabelleHOL = CFOL2IsabelleHOL
transTheory :: FormExtension f => SignTranslator f e -> FormulaTranslator f e -> (Sign f e, [Named (FORMULA f)]) -> IsaTheory
transVar :: Set String -> VAR -> String
typeToks :: Sign f e -> Set String
mapSen :: FormulaTranslator f e -> Sign f e -> Set String -> FORMULA f -> Sentence
type IsaTheory = (Sign, [Named Sentence])
type SignTranslator f e = Sign f e -> e -> IsaTheory -> IsaTheory
type FormulaTranslator f e = Sign f e -> Set String -> f -> Term
getAssumpsToks :: Sign f e -> Set String
formTrCASL :: FormulaTranslator () ()
quantifyIsa :: String -> (String, Typ) -> Term -> Term
quantify :: Set String -> QUANTIFIER -> (VAR, SORT) -> Term -> Term
transFORMULA :: Sign f e -> Set String -> FormulaTranslator f e -> Set String -> FORMULA f -> Term
transSort :: SORT -> Typ
transRecord :: Sign f e -> Set String -> FormulaTranslator f e -> Set String -> Record f Term Term
transOpSymb :: Sign f e -> Set String -> OP_SYMB -> VName

Documentation

data CFOL2IsabelleHOL Source #

The identity of the comorphism

Constructors

CFOL2IsabelleHOL

Instances

Instances details

Show CFOL2IsabelleHOL Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods showsPrec :: Int -> CFOL2IsabelleHOL -> ShowS show :: CFOL2IsabelleHOL -> String showList :: [CFOL2IsabelleHOL] -> ShowS
Language CFOL2IsabelleHOL Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods language_name :: CFOL2IsabelleHOL -> String Source # description :: CFOL2IsabelleHOL -> String Source #
Comorphism CFOL2IsabelleHOL CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree Isabelle () () Sentence () () Sign IsabelleMorphism () () () Source #
Instance details Defined in Comorphisms.CFOL2IsabelleHOL Methods sourceLogic :: CFOL2IsabelleHOL -> CASL Source # sourceSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics Source # sourceSublogicLossy :: CFOL2IsabelleHOL -> CASL_Sublogics Source # minSourceTheory :: CFOL2IsabelleHOL -> Maybe (LibName, String) Source # targetLogic :: CFOL2IsabelleHOL -> Isabelle Source # mapSublogic :: CFOL2IsabelleHOL -> CASL_Sublogics -> Maybe () Source # map_theory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # mapMarkedTheory :: CFOL2IsabelleHOL -> (CASLSign, [Named CASLFORMULA]) -> Result (Sign, [Named Sentence]) Source # map_morphism :: CFOL2IsabelleHOL -> CASLMor -> Result IsabelleMorphism Source # map_sentence :: CFOL2IsabelleHOL -> CASLSign -> CASLFORMULA -> Result Sentence Source # map_symbol :: CFOL2IsabelleHOL -> CASLSign -> Symbol -> Set () Source # extractModel :: CFOL2IsabelleHOL -> CASLSign -> () -> Result (CASLSign, [Named CASLFORMULA]) Source # is_model_transportable :: CFOL2IsabelleHOL -> Bool Source # has_model_expansion :: CFOL2IsabelleHOL -> Bool Source # is_weakly_amalgamable :: CFOL2IsabelleHOL -> Bool Source # constituents :: CFOL2IsabelleHOL -> [String] Source # isInclusionComorphism :: CFOL2IsabelleHOL -> Bool Source # rps :: CFOL2IsabelleHOL -> Bool Source # eps :: CFOL2IsabelleHOL -> Bool Source # isGTC :: CFOL2IsabelleHOL -> Bool Source #

transTheory :: FormExtension f => SignTranslator f e -> FormulaTranslator f e -> (Sign f e, [Named (FORMULA f)]) -> IsaTheory Source #

transVar :: Set String -> VAR -> String Source #

typeToks :: Sign f e -> Set String Source #

mapSen :: FormulaTranslator f e -> Sign f e -> Set String -> FORMULA f -> Sentence Source #

type IsaTheory = (Sign, [Named Sentence]) Source #

type SignTranslator f e = Sign f e -> e -> IsaTheory -> IsaTheory Source #

type FormulaTranslator f e = Sign f e -> Set String -> f -> Term Source #

getAssumpsToks :: Sign f e -> Set String Source #

formTrCASL :: FormulaTranslator () () Source #

quantifyIsa :: String -> (String, Typ) -> Term -> Term Source #

quantify :: Set String -> QUANTIFIER -> (VAR, SORT) -> Term -> Term Source #

transFORMULA :: Sign f e -> Set String -> FormulaTranslator f e -> Set String -> FORMULA f -> Term Source #

transSort :: SORT -> Typ Source #

transRecord :: Sign f e -> Set String -> FormulaTranslator f e -> Set String -> Record f Term Term Source #

transOpSymb :: Sign f e -> Set String -> OP_SYMB -> VName Source #