Hets - the Heterogeneous Tool Set
Copyright(c) J. von Schroeder DFKI Bremen 2012
LicenseGPLv2 or higher, see LICENSE.txt
MaintainerJ. von Schroeder <jonathan.von_schroeder@dfki.de>
Stabilityprovisional
Portabilitynon-portable (imports Logic.Logic)
Safe HaskellNone

Comorphisms.THFP2THF0

Description

The comorphism from THFP to THF0.

Documentation

data THFP2THF0 Source #

Constructors

THFP2THF0 

Instances

Instances details
Show THFP2THF0 Source # 
Instance details

Defined in Comorphisms.THFP2THF0

Methods

showsPrec :: Int -> THFP2THF0 -> ShowS

show :: THFP2THF0 -> String

showList :: [THFP2THF0] -> ShowS

Language THFP2THF0 Source # 
Instance details

Defined in Comorphisms.THFP2THF0

Methods

language_name :: THFP2THF0 -> String Source #

description :: THFP2THF0 -> String Source #

Comorphism THFP2THF0 THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree THF THFSl BasicSpecTHF THFFormula () () SignTHF MorphismTHF SymbolTHF () ProofTree Source # 
Instance details

Defined in Comorphisms.THFP2THF0

Methods

sourceLogic :: THFP2THF0 -> THF Source #

sourceSublogic :: THFP2THF0 -> THFSl Source #

sourceSublogicLossy :: THFP2THF0 -> THFSl Source #

minSourceTheory :: THFP2THF0 -> Maybe (LibName, String) Source #

targetLogic :: THFP2THF0 -> THF Source #

mapSublogic :: THFP2THF0 -> THFSl -> Maybe THFSl Source #

map_theory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

mapMarkedTheory :: THFP2THF0 -> (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

map_morphism :: THFP2THF0 -> MorphismTHF -> Result MorphismTHF Source #

map_sentence :: THFP2THF0 -> SignTHF -> THFFormula -> Result THFFormula Source #

map_symbol :: THFP2THF0 -> SignTHF -> SymbolTHF -> Set SymbolTHF Source #

extractModel :: THFP2THF0 -> SignTHF -> ProofTree -> Result (SignTHF, [Named THFFormula]) Source #

is_model_transportable :: THFP2THF0 -> Bool Source #

has_model_expansion :: THFP2THF0 -> Bool Source #

is_weakly_amalgamable :: THFP2THF0 -> Bool Source #

constituents :: THFP2THF0 -> [String] Source #

isInclusionComorphism :: THFP2THF0 -> Bool Source #

rps :: THFP2THF0 -> Bool Source #

eps :: THFP2THF0 -> Bool Source #

isGTC :: THFP2THF0 -> Bool Source #

trans_theory :: (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula]) Source #

type TransMap = Map Constant [Constant] Source #

curryConstType :: Type -> Type Source #

prodToMapType :: Type -> Type -> Type Source #

rewriteSen :: TransMap -> [Named THFFormula] -> Result [Named THFFormula] Source #

rewriteFns :: RewriteFuns TransMap Source #

rewriteSen' :: TransMap -> Named THFFormula -> Result (Named THFFormula) Source #

rewriteLogicFormula' :: (RewriteFuns TransMap, TransMap) -> THFLogicFormula -> Result THFLogicFormula Source #

rewriteBinaryFormula' :: (RewriteFuns TransMap, TransMap) -> THFBinaryFormula -> Result (Either THFBinaryFormula THFUnitaryFormula) Source #

toTuple :: THFUnitaryFormula -> Maybe THFUnitaryFormula Source #

logicFormula2UnitaryFormula :: THFLogicFormula -> THFUnitaryFormula Source #

rewriteBinaryTuple' :: (RewriteFuns TransMap, TransMap) -> THFBinaryTuple -> Result (Either THFBinaryFormula THFUnitaryFormula) Source #

flattenTuples :: [THFUnitaryFormula] -> [THFUnitaryFormula] Source #

flattenTuple :: THFUnitaryFormula -> [THFUnitaryFormula] Source #

unpack_tuple :: THFUnitaryFormula -> Int -> Result (Either THFBinaryFormula THFUnitaryFormula) Source #

removeParensUnitaryFormula :: THFUnitaryFormula -> THFUnitaryFormula Source #

rewriteVariableList' :: (RewriteFuns TransMap, TransMap) -> [THFVariable] -> Result [THFVariable] Source #

transToken :: TransMap -> Token -> [Token] Source #

rewriteConst' :: (RewriteFuns TransMap, TransMap) -> Constant -> Result THFUnitaryFormula Source #

transConst' :: TransMap -> Constant -> [THFLogicFormula] Source #

constMakeExplicitProduct :: Constant -> Type -> [(Constant, Type)] Source #

makeExplicitProducts :: (TransMap, SignTHF) -> (TransMap, SignTHF) Source #

mkExplicitProductsT :: TransMap -> Map Constant ConstInfo -> (TransMap, Map Constant ConstInfo) Source #

prodTToTuple :: TransMap -> Map Constant ConstInfo -> Constant -> Name -> Type -> (TransMap, Map Constant ConstInfo) Source #

hasProdT :: TransMap -> ConstInfo -> Bool Source #

isProdT :: TransMap -> Type -> Bool Source #