| 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.
- 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
transTheory :: FormExtension f => SignTranslator f e -> FormulaTranslator f e -> (Sign f e, [Named (FORMULA f)]) -> IsaTheory
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 () ()
transFORMULA :: Sign f e -> Set String -> FormulaTranslator f e -> Set String -> FORMULA f -> Term
transRecord :: Sign f e -> Set String -> FormulaTranslator f e -> Set String -> Record f Term Term