{- |
Module      :  $Id$
Description :  various encodings
Copyright   :  (c) Uni Bremen 2005-2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  non-portable (existential types)

This folder contains various comorphisms (implemented using
the type class 'Logic.Comorphism.Comorphism'), which are then
collected to a logic graph in "Comorphisms.LogicGraph".
The latter is based on the list of logics collected in
"Comorphisms.LogicList".

The individual comorphisms are on the one hand trivial embeddings:

"Comorphisms.CASL2CoCASL"

"Comorphisms.CASL2CspCASL"

"Comorphisms.CASL2HasCASL"

"Comorphisms.CASL2Modal"

"Comorphisms.Prop2CASL"


On the other hand, there are a number of real encodings:

"Comorphisms.CASL2PCFOL", "Comorphisms.CASL2TopSort"  encodings of subsorting

"Comorphisms.CASL2SubCFOL" encoding of partiality

"Comorphisms.Sule2SoftFOL" translating a CASL subset to SoftFOL

"Comorphisms.Modal2CASL" encoding of Kripke worlds


"Comorphisms.HasCASL2Haskell"
  translation of executable HasCASL subset to Haskell

"Comorphisms.CspCASL2Modal"
  unfinished coding of CSP-CASL LTS semantics as Kripke models

"Comorphisms.CspCASL2IsabelleHOL"
  unfinished coding of CSP-CASL in IsabelleHOL

"Comorphisms.HasCASL2HasCASL"
  unfinished mapping of HasCASL subset to HasCASL program blocks


Finally, encodings to the theorem prover Isabelle:

"Comorphisms.CFOL2IsabelleHOL"

"Comorphisms.CoCFOL2IsabelleHOL"

"Comorphisms.PCoClTyCons2IsabelleHOL"
 unfinished translation of HasCASL subset to Isabelle

"Comorphisms.Haskell2IsabelleHOLCF"
-}

module Comorphisms where