27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech{- |

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechModule : $Header$

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechCopyright : (c) Till Mossakowski and Uni Bremen 2003

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechLicence : All rights reserved.

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechMaintainer : hets@tzi.de

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechStability : provisional

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechPortability : non-portable (imports Logic.Logic)

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech The embedding comorphism from CASL to HasCASL.

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-}

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechmodule Comorphisms.CASL2HasCASL where

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Logic.Logic

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Logic.Comorphism

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Common.Id

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport qualified Common.Lib.Map as Map

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Common.Lib.Set as Set

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport Data.Dynamic

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- CASL

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport CASL.Logic_CASL

dd285415d7a8d8376207960cfa3e977524c3b98cJakub Hrozekimport CASL.AS_Basic_CASL

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport CASL.Sublogic

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport CASL.StaticAna

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport CASL.Morphism

dd285415d7a8d8376207960cfa3e977524c3b98cJakub Hrozek

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport HasCASL.Logic_HasCASL

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport HasCASL.As

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport HasCASL.Le

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport HasCASL.Symbol

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechimport HasCASL.Morphism

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech-- | The identity of the comorphism

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechdata CASL2HasCASL = CASL2HasCASL deriving (Show)

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechinstance Language CASL2HasCASL -- default definition is okay

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechtycon_CASL2HasCASL :: TyCon

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechtycon_CASL2HasCASL = mkTyCon "G_sign"

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechinstance Typeable CASL2HasCASL where

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech typeOf _ = mkAppTy tycon_CASL2HasCASL []

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cechinstance Comorphism CASL2HasCASL

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech CASL CASL.Sublogic.CASL_Sublogics

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech BASIC_SPEC Sentence SYMB_ITEMS SYMB_MAP_ITEMS

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech Sign

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech CASL.Morphism.Morphism

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech CASL.Morphism.Symbol CASL.Morphism.RawSymbol ()

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech HasCASL HasCASL_Sublogics

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech BasicSpec Term SymbItems SymbMapItems

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech HasCASL.Le.Env

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech HasCASL.Morphism.Morphism

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech HasCASL.Morphism.Symbol HasCASL.Morphism.RawSymbol () where

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech sourceLogic _ = CASL

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech sourceSublogic _ = CASL_SL

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech { has_sub = False, -- no subsorting in HasCASL yet...

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech has_part = True,

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech has_cons = True,

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech has_eq = True,

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech has_pred = True,

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech which_logic = FOL

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech }

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech targetLogic _ = HasCASL

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech targetSublogic _ = ()

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech map_sign _ = mapSignature

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech --map_morphism _ morphism1 -> Maybe morphism2

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech --map_sentence _ sign1 -> sentence1 -> Maybe sentence2

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech --map_symbol :: cid -> symbol1 -> Set symbol2

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechsortTypeinfo :: TypeInfo

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechsortTypeinfo = TypeInfo { typeKind = star,

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech otherTypeKinds = [],

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech superTypes = [],

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech typeDefn = NoTypeDefn

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech }

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechmakeType :: Id -> HasCASL.As.Type

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechmakeType i = TypeName i star 0

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtrOpType :: CASL.StaticAna.OpType -> HasCASL.Le.OpInfo

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtrOpType ot = OpInfo { opType = simpleTypeScheme t,

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech opAttrs = [],

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech opDefn = NoOpDefn Op

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech }

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech where t = if null args then res

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech else FunType arg arrow res []

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech arrow = case opKind ot of

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech CASL.StaticAna.Total -> FunArr

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech CASL.StaticAna.Partial -> PFunArr

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech args = map makeType $ opArgs ot

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech arg = if isSingle args then head args else

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech ProductType args []

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech res = makeType $ opRes ot

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtrPredType :: CASL.StaticAna.PredType -> HasCASL.Le.OpInfo

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr CechtrPredType pt = OpInfo { opType = simpleTypeScheme t,

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech opAttrs = [],

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech opDefn = NoOpDefn Pred

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech }

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech where t = if null args then logicalType else

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech predType arg

27a7dedb0ee4d4b51ca4c196aa894ad30cb3e821Petr Cech args = map makeType $ predArgs pt

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech arg = if isSingle args then head args else

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech ProductType args []

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr ČechmapSignature :: CASL.StaticAna.Sign -> Maybe(HasCASL.Le.Env,[Term])

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr ČechmapSignature sign = Just (initialEnv {

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech classMap = Map.empty,

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech typeMap = Map.fromList $ map (\s -> (s,sortTypeinfo))

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech $ Set.toList $ sortSet sign,

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech assumps = Map.map OpInfos $ Map.unionWith (++) opmap predmap }, [])

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech where

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech opmap = Map.map (map trOpType . Set.toList) $ opMap sign

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech predmap = Map.map (map trPredType . Set.toList) $ predMap sign

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech

23637e2fd2b1fe42bdd2335893a11ac8016f56bcPetr Čech