aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowski{-# OPTIONS_GHC -fno-glasgow-exts #-}

e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens Elkner{-# LANGUAGE TypeSynonymInstances, FlexibleInstances, MultiParamTypeClasses #-}

e1f395fef7ea8b00a675a330e5461fad35158ca5Christian Maeder{- |

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill MossakowskiModule : $Header$

1ac0c4de66a297fd7e345d9275f723fd83bb7bd1Christian MaederDescription : translating program equations to Haskell

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuCopyright : (c) Christian Maeder, Uni Bremen 2004-2005

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill MossakowskiLicense : GPLv2 or higher

3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill MossakowskiMaintainer : Christian.Maeder@dfki.de

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill MossakowskiStability : provisional

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill MossakowskiPortability : non-portable

f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder

87b7a494f805b2b2f3311564f3dfcc4352f803fcTill MossakowskiThe embedding comorphism from HasCASL to Haskell.

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder-}

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maedermodule Comorphisms.HasCASL2Haskell where

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder

1f084d62dbf8ae72357697c226cacd1973f0c03fTill Mossakowskiimport Logic.Logic

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowskiimport Logic.Comorphism

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaederimport Data.List((\\))

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaederimport Common.Id

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaederimport Common.Result

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaederimport Common.AS_Annotation

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaederimport Common.GlobalAnnotations

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowskiimport Common.ExtSign

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowskiimport qualified Data.Map as Map

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowskiimport qualified Data.Set as Set

1ac0c4de66a297fd7e345d9275f723fd83bb7bd1Christian Maeder

b6a54d7292d7a3713000847334de4316d105f40fChristian Maederimport HasCASL.As

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maederimport HasCASL.AsUtils

e79472ac9f45b44b205357ff33965c36bfe6f765Christian Maederimport HasCASL.Builtin

a7dc6e2f1ca4f1b9164b496af09228b44c8dd4b0Christian Maederimport HasCASL.DataAna

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowskiimport HasCASL.Le as HC

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowskiimport HasCASL.Logic_HasCASL

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maederimport HasCASL.Sublogic

fa941cafef82113297227345cbb21e523f962cbePaolo Torrini

92303a4d15dffd2c571d32311dcae866bd449d86Klaus Luettichimport Haskell.Logic_Haskell as HS

b161fda9df774b071a907cc9b18f0e7aee244129cmaederimport Haskell.HatParser hiding(TypeInfo, Kind)

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaederimport Haskell.HatAna

ad270004874ce1d0697fb30d7309f180553bb315Christian Maederimport Haskell.TranslateId

ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowski-- | The identity of the comorphism

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maederdata HasCASL2Haskell = HasCASL2Haskell deriving Show

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder

b161fda9df774b071a907cc9b18f0e7aee244129cmaederinstance Language HasCASL2Haskell -- default definition is okay

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder

b161fda9df774b071a907cc9b18f0e7aee244129cmaederinstance Comorphism HasCASL2Haskell

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder HasCASL Sublogic

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder BasicSpec Sentence SymbItems SymbMapItems

9f84560989b06003d74d125ed8b8ca99a94bd165Christian Maeder Env

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder Morphism

74fc328292d911eff0baa47a247005cf33d2bdd2Sonja Gröning HC.Symbol HC.RawSymbol ()

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder Haskell ()

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder HsDecls (TiDecl PNT) () ()

0db76fa4de562d31f829d0113500e70771f0852dcmaeder Sign

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowski HaskellMorphism

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder HS.Symbol HS.RawSymbol () where

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder sourceLogic HasCASL2Haskell = HasCASL

840ad39a5a571d5170e7bc4796058208502fa73fSonja Gröning sourceSublogic HasCASL2Haskell = noSubtypes

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder targetLogic HasCASL2Haskell = Haskell

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder mapSublogic HasCASL2Haskell _ = Just ()

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder map_morphism = mapDefaultMorphism

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder map_sentence HasCASL2Haskell = mapSingleSentence

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder map_theory HasCASL2Haskell = mapTheory

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder isInclusionComorphism HasCASL2Haskell = True

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder

2857cf346f2387af92b04a43c41e829c00664ed1cmaedermapSingleSentence :: Env -> Sentence -> Result (TiDecl PNT)

2857cf346f2387af92b04a43c41e829c00664ed1cmaedermapSingleSentence sign sen = do

2857cf346f2387af92b04a43c41e829c00664ed1cmaeder (_, l) <- mapTheory (sign, [makeNamed "" sen])

3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder case l of

3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder [] -> fail "sentence was not translated"

f04d7c1dac7b1dc835e63c671027455f8db17837Christian Maeder [s] -> return $ sentence s

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder _ -> do (_, o) <- mapTheory (sign, [])

9b557297a9b3b1f44044b8d80a00264715b9f9d6cmaeder case l \\ o of

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder [] -> fail "not a new sentence"

aa0ef8adb2833838c1954e6f93c61d85d2cb226aTill Mossakowski [s] -> return $ sentence s

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder _ -> fail "several sentences resulted"

9b557297a9b3b1f44044b8d80a00264715b9f9d6cmaeder

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaedermapTheory :: (Env, [Named Sentence]) -> Result (Sign, [Named (TiDecl PNT)])

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaedermapTheory (sig, csens) = do

cd6e5706893519bfcf24539afa252fcbed5097ddKlaus Luettich let hs = translateSig sig

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder ps = concatMap (translateSentence sig) csens

e24ad3f655daa60ddabe690e4b11de3187996c16cmaeder cs = cleanSig hs ps

90fbaf1cd73486129e26e1ac94a413550832e4d6Thiemo Wiedemeyer (_, ExtSign hsig _, sens) <-

90fbaf1cd73486129e26e1ac94a413550832e4d6Thiemo Wiedemeyer hatAna (HsDecls (cs ++ map sentence ps),

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder emptySign, emptyGlobalAnnos)

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder return (diffSign hsig preludeSign,

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder filter (not . preludeEntity . getHsDecl . sentence) sens)

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder-- former file UniqueId

1d3635d5ca4cfbe47c3f1add3790f68b6c76c57dChristian Maeder

1d3635d5ca4cfbe47c3f1add3790f68b6c76c57dChristian Maeder-- | Generates distinct names for overloaded function identifiers.

1d3635d5ca4cfbe47c3f1add3790f68b6c76c57dChristian MaederdistinctOpIds :: Int -> [(Id, [OpInfo])] -> [(Id, OpInfo)]

1d3635d5ca4cfbe47c3f1add3790f68b6c76c57dChristian MaederdistinctOpIds n l = case l of

1d3635d5ca4cfbe47c3f1add3790f68b6c76c57dChristian Maeder [] -> []

1d3635d5ca4cfbe47c3f1add3790f68b6c76c57dChristian Maeder (i, info) : idInfoList ->

1d3635d5ca4cfbe47c3f1add3790f68b6c76c57dChristian Maeder case info of

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder [] -> distinctOpIds 2 idInfoList

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder [hd] -> (i, hd) : distinctOpIds 2 idInfoList

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder hd : tl -> (newName i n, hd) :

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder distinctOpIds (n + 1) ((i, tl) : idInfoList)

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder-- | Adds a number to the name of an identifier.

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaedernewName :: Id -> Int -> Id

f094a7999dfa79cad2eb34ce15f1939c0d6b9e39Till MossakowskinewName (Id tlist idlist poslist) n =

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder Id (tlist ++ [mkSimpleId $ '0' : show n]) idlist poslist

c44c23429c72f3a709e22a18f2ed6f05fc8cc765Christian Maeder

1d3635d5ca4cfbe47c3f1add3790f68b6c76c57dChristian Maeder-- | Searches for the real name of an overloaded identifier.

f094a7999dfa79cad2eb34ce15f1939c0d6b9e39Till MossakowskifindUniqueId :: Env -> Id -> TypeScheme -> Maybe (Id, OpInfo)

f094a7999dfa79cad2eb34ce15f1939c0d6b9e39Till MossakowskifindUniqueId env uid ts =

2eb18519bf2f61e04ffbe68ab06ec1e32eee07d7Christian Maeder let l = Set.toList $ Map.findWithDefault Set.empty uid $ assumps env

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder fit :: Int -> [OpInfo] -> Maybe (Id, OpInfo)

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder fit n tl =

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder case tl of

b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder [] -> Nothing

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder oi:rt -> if ts == opType oi then

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder Just (if null rt then uid else newName uid n, oi)

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder else fit (n + 1) rt

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder in fit 2 l

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder

b205bc86685958085af2b816c277faef3ebed52aChristian Maeder-- former TranslateAna file

135bcb7f65991146c103e5e7599adbc49fe7359dChristian Maeder

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder-------------------------------------------------------------------------

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder-- Translation of an HasCASL-Environement

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder-------------------------------------------------------------------------

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder-- | Converts an abstract syntax of HasCASL (after the static analysis)

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder-- to the top datatype of the abstract syntax of haskell.

4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedertranslateSig :: Env -> [HsDecl]

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian MaedertranslateSig env =

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder concatMap (translateTypeInfo env) (Map.toList $ typeMap env)

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder ++ concatMap translateAssump (distinctOpIds 2 $ Map.toList

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder $ Map.map Set.toList $ assumps env)

b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder

3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder-------------------------------------------------------------------------

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder-- Translation of types

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder-------------------------------------------------------------------------

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder

b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder-- | Converts one type to a data or type declaration in Haskell.

0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian MaedertranslateTypeInfo :: Env -> (Id, TypeInfo) -> [HsDecl]

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian MaedertranslateTypeInfo env (tid,info) =

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder let hsname = mkHsIdent UpperId tid

3fe4d4988c6d17ce5df9b413af03944114dc5d63Christian Maeder hsTyName = hsTyCon hsname

3fe4d4988c6d17ce5df9b413af03944114dc5d63Christian Maeder mkTp = foldl hsTyApp hsTyName

3fe4d4988c6d17ce5df9b413af03944114dc5d63Christian Maeder k = typeKind info

3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian Maeder loc = toProgPos $ posOfId tid

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder ddecl = hsDataDecl loc

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder [] -- empty HsContext

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder (mkTp $ kindToTypeArgs 1 k)

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder [HsConDecl loc [] [] hsname []]

b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder derives

b418a0262aa84ea68de72623793361bebed51f9eChristian Maeder in case typeDefn info of

b418a0262aa84ea68de72623793361bebed51f9eChristian Maeder NoTypeDefn -> case Set.toList $ superTypes info of

177b47384142a17a086bf08966097e9c624d7891Christian Maeder [] -> [ddecl]

177b47384142a17a086bf08966097e9c624d7891Christian Maeder j : _ -> [typeSynonym loc hsTyName $ TypeName j k 0]

177b47384142a17a086bf08966097e9c624d7891Christian Maeder AliasTypeDefn ts ->

177b47384142a17a086bf08966097e9c624d7891Christian Maeder [hsTypeDecl loc (mkTp $ getAliasArgs ts) $ getAliasType ts]

16076938607b9401efc432359077252dd0ed0d63Christian Maeder DatatypeDefn de -> [sentence $ translateDt env de]

177b47384142a17a086bf08966097e9c624d7891Christian Maeder _ -> [] -- ignore others

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder

177b47384142a17a086bf08966097e9c624d7891Christian MaederisSameId :: Id -> Type -> Bool

c97ea41501cc68e04648fbed17812eee014a89a0Christian MaederisSameId tid (TypeName tid2 _ _) = tid == tid2

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian MaederisSameId _tid _ty = False

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder

3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian MaedertypeSynonym :: SrcLoc -> HsType -> Type -> HsDecl

3a6decfd748f532d5cb03fbcb7a42fa37b0faab3Christian MaedertypeSynonym loc hsname = hsTypeDecl loc hsname . translateType

2f1781ab0a0a58328ef9d1ad8bda1984fd80259dChristian Maeder

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian MaederkindToTypeArgs :: Int -> RawKind -> [HsType]

2f1781ab0a0a58328ef9d1ad8bda1984fd80259dChristian MaederkindToTypeArgs i k = case k of

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder ClassKind _ -> []

177b47384142a17a086bf08966097e9c624d7891Christian Maeder FunKind _ _ kr ps -> (hsTyVar $ mkSName ('a' : show i)

177b47384142a17a086bf08966097e9c624d7891Christian Maeder $ toProgPos ps)

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder : kindToTypeArgs (i + 1) kr

0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian Maeder

0a64bfd28dff15bc93e1f7a86e0a8052e879636dChristian MaedergetAliasArgs :: Type -> [HsType]

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian MaedergetAliasArgs ty = case ty of

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder TypeAbs v t _ -> getArg v : getAliasArgs t

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder ExpandedType _ t -> getAliasArgs t

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder KindedType t _ _ -> getAliasArgs t

b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder _ -> []

4ef05f4edeb290beb89845f57156baa5298af7c4Christian Maeder

177b47384142a17a086bf08966097e9c624d7891Christian MaedergetArg :: TypeArg -> HsType

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian MaedergetArg = hsTyVar . mkHsIdent LowerId . getTypeVar

177b47384142a17a086bf08966097e9c624d7891Christian Maeder

177b47384142a17a086bf08966097e9c624d7891Christian MaedergetAliasType :: Type -> HsType

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian MaedergetAliasType ty = case ty of

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder TypeAbs _ t _ -> getAliasType t

b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder ExpandedType _ t -> getAliasType t

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder KindedType t _ _ -> getAliasType t

46b8ba7474c61b90ceb0d3a1c7fe6f4cfe9c7028Till Mossakowski _ -> translateType ty

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder-- | Translation of an alternative constructor for a datatype definition.

4ef05f4edeb290beb89845f57156baa5298af7c4Christian MaedertranslateAltDefn :: Env -> DataPat-> AltDefn

b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder -> [HsConDecl HsType [HsType]]

b6a54d7292d7a3713000847334de4316d105f40fChristian MaedertranslateAltDefn env dp (Construct muid ts p _) = case muid of

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder Just uid -> let loc = toProgPos $ posOfId uid

177b47384142a17a086bf08966097e9c624d7891Christian Maeder sc = getConstrScheme dp p ts

177b47384142a17a086bf08966097e9c624d7891Christian Maeder -- resolve overloading

177b47384142a17a086bf08966097e9c624d7891Christian Maeder (c, ui) = translateId env uid sc

177b47384142a17a086bf08966097e9c624d7891Christian Maeder in case c of

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder UpperId -> -- no existentials, no context

c438c79d00fc438f99627e612498744bdc0d0c89Christian Maeder [HsConDecl loc [] [] ui $

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder map (HsBangedType . translateType) ts]

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder _ -> error "HasCASL2Haskell.translateAltDefn"

177b47384142a17a086bf08966097e9c624d7891Christian Maeder Nothing -> []

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder

c97ea41501cc68e04648fbed17812eee014a89a0Christian MaedertranslateDt :: Env -> DataEntry -> Named HsDecl

c97ea41501cc68e04648fbed17812eee014a89a0Christian MaedertranslateDt env de@(DataEntry _ i _ args _ alts) =

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder let dp@(DataPat _ j _ _ _) = toDataPat de

177b47384142a17a086bf08966097e9c624d7891Christian Maeder loc = toProgPos $ posOfId i

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder hsname = mkHsIdent UpperId j

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder hsTyName = hsTyCon hsname

c97ea41501cc68e04648fbed17812eee014a89a0Christian Maeder tp = foldl hsTyApp hsTyName $ map getArg args

b6a54d7292d7a3713000847334de4316d105f40fChristian Maeder in

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder (makeNamed ("ga_" ++ showId j "") $ hsDataDecl loc

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder [] -- empty HsContext

5308ef83ee1b668f4cf6c8278bc645e7e0f8b4edTill Mossakowski tp (concatMap (translateAltDefn env dp)

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder $ Set.toList alts)

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder derives) { isDef = True }

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder-------------------------------------------------------------------------

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder-- Translation of functions

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder-------------------------------------------------------------------------

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder

ef7cdc5bb04f4c0d1a14cbd3008959edd2d6336cChristian Maeder-- | Converts one distinct named function in HasCASL to the corresponding

135bcb7f65991146c103e5e7599adbc49fe7359dChristian Maeder-- haskell declaration.

807d5fddaa5dd8924321c73400fcf875a9ed9a9cChristian Maeder-- Generates a definition (Prelude.undefined) for functions that are not

9f84560989b06003d74d125ed8b8ca99a94bd165Christian Maeder-- defined in HasCASL.

9f84560989b06003d74d125ed8b8ca99a94bd165Christian MaedertranslateAssump :: (Id, OpInfo) -> [HsDecl]

9f84560989b06003d74d125ed8b8ca99a94bd165Christian MaedertranslateAssump (i, opinf) =

c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder let fname = mkHsIdent LowerId i

c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder loc = toProgPos $ posOfId i

c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder res = hsTypeSig loc

c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder [fname] []

42f38bd450a260a4494113dc89041ef9b1c5f87cChristian Maeder $ translateTypeScheme $ opType opinf

eee01977bc7ead7e5dba08912ff15beb33604882Christian Maeder in case opDefn opinf of

42f38bd450a260a4494113dc89041ef9b1c5f87cChristian Maeder ConstructData _ -> [] -- wrong case!

c4ba3e20a432419afff01558e425e00be42871d8Christian Maeder _ -> [res, functionUndef loc fname]

16076938607b9401efc432359077252dd0ed0d63Christian Maeder

177b47384142a17a086bf08966097e9c624d7891Christian Maeder-- | Translation of the result type of a typescheme to a haskell type.

177b47384142a17a086bf08966097e9c624d7891Christian Maeder-- Uses 'translateType'.

177b47384142a17a086bf08966097e9c624d7891Christian MaedertranslateTypeScheme :: TypeScheme -> HsType

16076938607b9401efc432359077252dd0ed0d63Christian MaedertranslateTypeScheme (TypeScheme _ t _) =

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder translateType t

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder

2857cf346f2387af92b04a43c41e829c00664ed1cmaeder

074fa38abe1cef6132877a888b080d26d96697d2cmaeder-- | Translation of types (e.g. product type, type application ...).

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaedertranslateType :: Type -> HsType

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaedertranslateType t = case getTypeAppl t of

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder (TypeName tid _ n, tyArgs) -> let num = length tyArgs in

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder if n == 0 then

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder if tid == unitTypeId && null tyArgs then

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder hsTyCon $ mkSName "Bool" $ toProgPos $ getRange t

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder else if tid == lazyTypeId && num == 1 then

d9b1a9c8fce2e68aaf4a8b415ab40ab461a1b488cmaeder translateType $ head tyArgs

b418a0262aa84ea68de72623793361bebed51f9eChristian Maeder else if isArrow tid && num == 2 then

16076938607b9401efc432359077252dd0ed0d63Christian Maeder let [t1, t2] = tyArgs in

177b47384142a17a086bf08966097e9c624d7891Christian Maeder hsTyFun (translateType t1) (translateType t2)

177b47384142a17a086bf08966097e9c624d7891Christian Maeder else if isProductId tid && num > 1 then

80c2d23821d095b55d9a547f48fc3fcdc27df405Christian Maeder hsTyTuple loc0 $ map translateType tyArgs

177b47384142a17a086bf08966097e9c624d7891Christian Maeder else foldl hsTyApp (hsTyCon $ mkHsIdent UpperId tid)

177b47384142a17a086bf08966097e9c624d7891Christian Maeder $ map translateType tyArgs

177b47384142a17a086bf08966097e9c624d7891Christian Maeder else foldl hsTyApp (hsTyVar $ mkHsIdent LowerId tid)

177b47384142a17a086bf08966097e9c624d7891Christian Maeder $ map translateType tyArgs

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder _ -> error "translateType"

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder

b161fda9df774b071a907cc9b18f0e7aee244129cmaedertoProgPos :: Range -> SrcLoc

b161fda9df774b071a907cc9b18f0e7aee244129cmaedertoProgPos p = if isNullRange p then loc0

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder else let Range (SourcePos n l c:_) = p

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder in SrcLoc n (1000 + (l-1) * 80 + c) l c

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder

b161fda9df774b071a907cc9b18f0e7aee244129cmaedermkSName :: String -> SrcLoc -> SN HsName

b161fda9df774b071a907cc9b18f0e7aee244129cmaedermkSName = SN . UnQual

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder

b161fda9df774b071a907cc9b18f0e7aee244129cmaedermkHsIdent :: IdCase -> Id -> SN HsName

b161fda9df774b071a907cc9b18f0e7aee244129cmaedermkHsIdent c i = mkSName (translateIdWithType c i) $ toProgPos $ posOfId i

eb9c04f9cff47a81f6d362ca03fbf4cb7ab97e7ccmaeder

b161fda9df774b071a907cc9b18f0e7aee244129cmaedertranslateId :: Env -> Id -> TypeScheme -> (IdCase, SN HsName)

b161fda9df774b071a907cc9b18f0e7aee244129cmaedertranslateId env uid sc =

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder let oid = findUniqueId env uid sc

b161fda9df774b071a907cc9b18f0e7aee244129cmaeder mkUnQual :: IdCase -> Id -> (IdCase, SN HsName)

mkUnQual c j = (c, mkHsIdent c j)

in case oid of

Just (i, oi) -> if isConstructor oi then mkUnQual UpperId i

else mkUnQual LowerId i

_ -> mkUnQual LowerId uid -- variable

-- | Converts a term in HasCASL to an expression in haskell

translateTerm :: Env -> Term -> HsExp

translateTerm env t =

let loc = toProgPos $ getRange t

in case t of

QualVar (VarDecl v ty _ _) ->

let (c, i) = translateId env v $ simpleTypeScheme ty in

case c of

LowerId -> rec $ HsId $ HsVar i

_ -> error "translateTerm: variable with UpperId"

QualOp _ (PolyId uid _ _) sc _ _ _ -> let

-- The identifier 'uid' may have been renamed. To find its new name,

-- the typescheme 'ts' is tested for unifiability with the

-- typeschemes of the assumps. If an identifier is found, it is used

-- as HsVar or HsCon.

mkPHsVar s = rec $ HsPId $ HsVar $ mkSName s loc

mkHsVar s = rec $ HsId $ HsVar $ mkSName s loc

mkHsCon s = rec $ HsId $ HsCon $ mkSName s loc

mkUncurry s = rec $ HsApp (mkHsVar "uncurry") (mkHsVar s)

mkErr s = expUndef loc $ s ++ pp loc

hTrue = mkHsCon "True"

a = mkHsVar "a"

b = mkHsVar "b"

c = mkHsVar "c"

vs2 = [mkPHsVar "a", mkPHsVar "b"]

vs3 = vs2 ++ [mkPHsVar "c"]

pat2 = [rec $ HsPTuple loc vs2]

pat3 = [rec $ HsPTuple loc vs3]

mkLam2 x y = rec $ HsParen $ rec $ HsLambda pat2 $ rec $ HsIf x y hTrue

mkLam3 x y = rec $ HsParen $ rec $ HsLambda pat3 $ rec $ HsIf x y c

in if uid == botId then mkErr "bottom at "

else if uid == trueId then hTrue

else if uid == falseId then mkHsCon "False"

else if uid == notId || uid == negId then mkHsVar "not"

else if uid == defId then rec $ HsRightSection

(HsVar $ mkSName "seq" loc) hTrue

else if uid == orId then mkUncurry "||"

else if uid == andId then mkUncurry "&&"

else if uid == eqId || uid == eqvId || uid == exEq then

mkErr "equality at "

else if uid == implId then mkLam2 a b

else if uid == infixIf then mkLam2 b a

else if uid == whenElse then mkLam3 b a

else if uid == ifThenElse then mkLam3 a b

else let (cs, ui) = translateId env uid sc

in rec $ HsId $ case cs of

UpperId -> HsCon ui

LowerId -> HsVar ui

ApplTerm t1 t2 _ ->

rec $ HsApp (translateTerm env t1) $ translateTerm env t2

TupleTerm ts _ -> rec $ HsTuple (map (translateTerm env) ts)

TypedTerm t1 tqual _ty _ -> -- check for global types later

case tqual of

InType -> expUndef loc $ show tqual

_ -> translateTerm env t1

QuantifiedTerm qu _vars _t1 _ -> expUndef loc $ show qu

LambdaTerm pats _part t1 _ ->

rec $ HsLambda

(map (translatePattern env) pats)

(translateTerm env t1)

CaseTerm t1 progeqs _ ->

rec $ HsCase (translateTerm env t1)

(map (translateCaseProgEq env) progeqs)

LetTerm _ progeqs t1 _ ->

rec $ HsLet (map (translateLetProgEq env) progeqs)

(translateTerm env t1)

_ -> error ("translateTerm: unexpected term: " ++ show t)

-- | Conversion of patterns form HasCASL to haskell.

translatePattern :: Env -> Term -> HsPat

translatePattern env pat = case pat of

QualVar (VarDecl v ty _ _) ->

if show v == "_" then rec HsPWildCard else

let (c, i) = translateId env v $ simpleTypeScheme ty

in case c of

LowerId -> rec $ HsPId $ HsVar i

_ -> error ("unexpected constructor as variable: " ++ show v)

QualOp _ (PolyId uid _ _) sc _ _ _ ->

let (_, ui) = translateId env uid sc

in rec $ HsPApp ui []

ApplTerm p1 p2 _ ->

let tp = translatePattern env p1

a = translatePattern env p2

in case struct tp of

HsPApp u os -> rec $ HsPParen $ rec $ HsPApp u (os ++ [a])

HsPParen (Pat (HsPApp u os)) ->

rec $ HsPParen $ rec $ HsPApp u (os ++ [a])

_ -> error ("problematic application pattern " ++ show pat)

TupleTerm pats _ ->

rec $ HsPTuple (toProgPos $ getRange pat)

$ map (translatePattern env) pats

TypedTerm _ InType _ _ -> error "translatePattern InType"

TypedTerm p _ _ty _ -> translatePattern env p

--the type is implicit

AsPattern (VarDecl v ty _ _) p _ ->

let (c, i) = translateId env v $ simpleTypeScheme ty

hp = translatePattern env p

in case c of

LowerId -> rec $ HsPAsPat i hp

_ -> error ("unexpected constructor as @-variable: " ++ show v)

_ -> error ("translatePattern: unexpected pattern: " ++ show pat)

-- | Translation of a program equation of a case term in HasCASL

translateCaseProgEq :: Env -> ProgEq -> HsAlt HsExp HsPat [HsDecl]

translateCaseProgEq env (ProgEq pat t ps) =

HsAlt (toProgPos ps)

(translatePattern env pat)

(HsBody (translateTerm env t))

[]

-- | Translation of a program equation of a let term in HasCASL

translateLetProgEq :: Env -> ProgEq -> HsDecl

translateLetProgEq env (ProgEq pat t ps) =

hsPatBind (toProgPos ps)

(translatePattern env pat)

(HsBody (translateTerm env t))

[]

-- | Translation of a toplevel program equation

translateProgEq :: Env -> ProgEq -> HsDecl

translateProgEq env (ProgEq pat t _) =

let loc = toProgPos $ getRange pat in case getAppl pat of

Just (uid, sc, args) ->

let (_, ui) = translateId env uid sc

in hsFunBind loc [HsMatch loc ui

(map (translatePattern env) args) -- [HsPat]

(HsBody $ translateTerm env t) -- HsRhs

[]]

Nothing -> error ("translateLetProgEq: no toplevel id: " ++ show pat)

-- | remove dummy decls given by sentences

cleanSig :: [HsDecl] -> [Named HsDecl] -> [HsDecl]

cleanSig ds sens =

let dds = foldr ( \ nd l -> case basestruct $ sentence nd of

Just (HsDataDecl _ _ n _ _) -> n : l

_ -> l) [] sens

funs = foldr ( \ nd l -> case basestruct $ sentence nd of

Just (HsFunBind _ (HsMatch _ n _ _ _ : _)) -> n : l

_ -> l) [] sens

in filter ( \ hs -> case basestruct hs of

Just (HsDataDecl _ _ n _ _) -> n `notElem` dds

Just (HsTypeDecl _ n _) -> n `notElem` dds

Just (HsFunBind _ (HsMatch _ n _ _ _ : _)) -> n `notElem` funs

_ -> True)

ds

expUndef :: SrcLoc -> String -> HsExp

expUndef loc = rec . HsApp (rec $ HsId $ HsVar $ mkSName "error" loc)

. rec . HsLit loc . HsString

-- For the definition of an undefined function.

-- Takes the name of the function as argument.

functionUndef :: SrcLoc -> SN HsName -> HsDecl

functionUndef loc s =

hsFunBind loc [HsMatch loc s [] -- hsPatBind loc (rec $ HsPId $ HsVar s)

(HsBody $ expUndef loc $ pp s)

[]]

translateSentence :: Env -> Named Sentence -> [Named HsDecl]

translateSentence env sen = case sentence sen of

DatatypeSen dt -> map (translateDt env) dt

ProgEqSen _ _ pe -> [sen { sentence = translateProgEq env pe }]

_ -> []

derives :: [SN HsName]

derives = [] -- map (fakeSN . UnQual) ["Show", "Eq", "Ord"]