| Copyright | (c) J. von Schroeder, DFKI Bremen 2012 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | J. von Schroeder <jonathan.von_schroeder@dfki.de> |
| Stability | provisional |
| Portability | non-portable (imports Logic.Logic) |
| Safe Haskell | None |
Comorphisms.THFP2THF0
Description
The comorphism from THFP to THF0.
Documentation
trans_theory :: (SignTHF, [Named THFFormula]) -> Result (SignTHF, [Named THFFormula])
curryConstType :: Type -> Type
prodToMapType :: Type -> Type -> Type
rewriteSen :: TransMap -> [Named THFFormula] -> Result [Named THFFormula]
rewriteSen' :: TransMap -> Named THFFormula -> Result (Named THFFormula)
rewriteLogicFormula' :: (RewriteFuns TransMap, TransMap) -> THFLogicFormula -> Result THFLogicFormula
rewriteBinaryFormula' :: (RewriteFuns TransMap, TransMap) -> THFBinaryFormula -> Result (Either THFBinaryFormula THFUnitaryFormula)
rewriteBinaryTuple' :: (RewriteFuns TransMap, TransMap) -> THFBinaryTuple -> Result (Either THFBinaryFormula THFUnitaryFormula)
flattenTuples :: [THFUnitaryFormula] -> [THFUnitaryFormula]
rewriteVariableList' :: (RewriteFuns TransMap, TransMap) -> [THFVariable] -> Result [THFVariable]
transToken :: TransMap -> Token -> [Token]
rewriteConst' :: (RewriteFuns TransMap, TransMap) -> Constant -> Result THFUnitaryFormula
transConst' :: TransMap -> Constant -> [THFLogicFormula]
constMakeExplicitProduct :: Constant -> Type -> [(Constant, Type)]
makeExplicitProducts :: (TransMap, SignTHF) -> (TransMap, SignTHF)