HasCASL2Haskell.hs revision 13f6b64b022fac1179149bfacf9a2ad908f7038d
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder{- |
81d182b21020b815887e9057959228546cf61b6bChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederDescription : translating program equations to Haskell
a39175891082dc8a598e5630e5558cb08b84ac0aChristian MaederCopyright : (c) Christian Maeder, Uni Bremen 2004-2005
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederMaintainer : Christian.Maeder@dfki.de
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederStability : provisional
ffd01020a4f35f434b912844ad6e0d6918fadffdChristian MaederPortability : non-portable
66267bcb678a9c341272c323b299337bcfdb7cc5Christian Maeder
66267bcb678a9c341272c323b299337bcfdb7cc5Christian MaederThe embedding comorphism from HasCASL to Haskell.
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder-}
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maeder
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maedermodule Comorphisms.HasCASL2Haskell where
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederimport Logic.Logic
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport Logic.Comorphism
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maederimport Data.List((\\))
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maederimport Common.Id
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport Common.Result
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederimport Common.AS_Annotation
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederimport Common.GlobalAnnotations
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maederimport qualified Data.Map as Map
34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maederimport qualified Data.Set as Set
34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maederimport HasCASL.Logic_HasCASL
34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maederimport HasCASL.Sublogic
fb69cd512eab767747f109e40322df7cae2f7bdfChristian Maederimport HasCASL.As
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.AsUtils
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maederimport HasCASL.Builtin
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport HasCASL.Le as HC
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maederimport Haskell.Logic_Haskell as HS
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maederimport Haskell.HatParser hiding(TypeInfo, Kind)
05e2a3161e4589a717c6fe5c7306820273a473c5Christian Maederimport Haskell.HatAna
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maederimport Haskell.TranslateId
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5d7e4bf173534e7eb3fc84dce7bb0151079d3f8aChristian Maeder-- | The identity of the comorphism
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederdata HasCASL2Haskell = HasCASL2Haskell deriving Show
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder
ad270004874ce1d0697fb30d7309f180553bb315Christian Maederinstance Language HasCASL2Haskell -- default definition is okay
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maeder
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maederinstance Comorphism HasCASL2Haskell
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder HasCASL Sublogic
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder BasicSpec Sentence SymbItems SymbMapItems
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Env
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Morphism
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder HC.Symbol HC.RawSymbol ()
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Haskell ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder HsDecls (TiDecl PNT) () ()
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Sign
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder HaskellMorphism
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder HS.Symbol HS.RawSymbol () where
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder sourceLogic HasCASL2Haskell = HasCASL
e7ce154edb906685b3fa7f6c0a764e18a4658068Christian Maeder sourceSublogic HasCASL2Haskell = noSubtypes
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder targetLogic HasCASL2Haskell = Haskell
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder mapSublogic HasCASL2Haskell _ = Just ()
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder map_morphism = mapDefaultMorphism
024621f43239cfe9629e35d35a8669fad7acbba2Christian Maeder map_sentence HasCASL2Haskell = mapSingleSentence
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder map_theory HasCASL2Haskell = mapTheory
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder-- former FromHasCASL file
36c6cc568751e4235502cfee00ba7b597dae78dcChristian Maeder
27912d626bf179b82fcb337077e5cd9653bb71cfChristian MaedermapSingleSentence :: Env -> Sentence -> Result (TiDecl PNT)
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedermapSingleSentence sign sen = do
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (_, l) <- mapTheory (sign, [makeNamed "" sen])
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder case l of
5c933f3c61d2cfa7e76e4eb610a4b0bac988be47Christian Maeder [] -> fail "sentence was not translated"
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder [s] -> return $ sentence s
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder _ -> do (_, o) <- mapTheory (sign, [])
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case l \\ o of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [] -> fail "not a new sentence"
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder [s] -> return $ sentence s
51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder _ -> fail "several sentences resulted"
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder
51c65d5fb2d720dc77bc5cca15640cfa09711986Christian MaedermapTheory :: (Env, [Named Sentence]) -> Result (Sign, [Named (TiDecl PNT)])
51c65d5fb2d720dc77bc5cca15640cfa09711986Christian MaedermapTheory (sig, csens) = do
51c65d5fb2d720dc77bc5cca15640cfa09711986Christian Maeder let hs = translateSig sig
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder ps = concatMap (translateSentence sig) csens
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder cs = cleanSig hs ps
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (_, hsig, sens) <-
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder hatAna (HsDecls (cs ++ map sentence ps),
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder emptySign, emptyGlobalAnnos)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder return (diffSign hsig preludeSign,
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder filter (not . preludeEntity . getHsDecl . sentence) sens)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- former file UniqueId
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | Generates distinct names for overloaded function identifiers.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdistinctOpIds :: Int -> [(Id, [OpInfo])] -> [(Id, OpInfo)]
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaederdistinctOpIds n l = case l of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [] -> []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder (i, info) : idInfoList ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case info of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [] -> distinctOpIds 2 idInfoList
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [hd] -> (i, hd) : distinctOpIds 2 idInfoList
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder hd : tl -> (newName i n, hd) :
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder distinctOpIds (n + 1) ((i, tl) : idInfoList)
998747cb2ee575cccdd7d865c95d0ef07516a6a5Christian Maeder
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder-- | Adds a number to the name of an identifier.
07e579405f31fff7f9315685661b5a87cb99c41bChristian MaedernewName :: Id -> Int -> Id
07e579405f31fff7f9315685661b5a87cb99c41bChristian MaedernewName (Id tlist idlist poslist) n =
07e579405f31fff7f9315685661b5a87cb99c41bChristian Maeder Id (tlist ++ [mkSimpleId $ '0' : show n]) idlist poslist
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder-- | Searches for the real name of an overloaded identifier.
678e45c045799ce271c4719123ecd9cf4f456d4bChristian MaederfindUniqueId :: Env -> Id -> TypeScheme -> Maybe (Id, OpInfo)
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian MaederfindUniqueId env uid ts =
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder let l = Set.toList $ Map.findWithDefault Set.empty uid $ assumps env
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder fit :: Int -> [OpInfo] -> Maybe (Id, OpInfo)
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder fit n tl =
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder case tl of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder [] -> Nothing
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder oi:rt -> if ts == opType oi then
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder Just (if null rt then uid else newName uid n, oi)
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder else fit (n + 1) rt
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder in fit 2 l
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder-- former TranslateAna file
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder-------------------------------------------------------------------------
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder-- Translation of an HasCASL-Environement
fb8645096eb70aa243c146abe31d4173cfbe6e1aChristian Maeder-------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | Converts an abstract syntax of HasCASL (after the static analysis)
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder-- to the top datatype of the abstract syntax of haskell.
6b23467258cdc15e05f1845cd400d60ca6eba966Christian MaedertranslateSig :: Env -> [HsDecl]
6b23467258cdc15e05f1845cd400d60ca6eba966Christian MaedertranslateSig env =
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder (concat $ map (translateTypeInfo env) $ Map.toList $ typeMap env)
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder ++ (concatMap translateAssump $ distinctOpIds 2 $ Map.toList
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder $ Map.map Set.toList $ assumps env)
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder-------------------------------------------------------------------------
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder-- Translation of types
6b23467258cdc15e05f1845cd400d60ca6eba966Christian Maeder-------------------------------------------------------------------------
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-- | Converts one type to a data or type declaration in Haskell.
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertranslateTypeInfo :: Env -> (Id, TypeInfo) -> [HsDecl]
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian MaedertranslateTypeInfo env (tid,info) =
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder let hsname = mkHsIdent UpperId tid
e13ee09381f136f5eadaabdb9699773c0052cf3dChristian Maeder hsTyName = hsTyCon hsname
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mkTp l = foldl hsTyApp hsTyName l
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder k = typeKind info
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder loc = toProgPos $ posOfId tid
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ddecl = hsDataDecl loc
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder [] -- empty HsContext
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder (mkTp $ kindToTypeArgs 1 k)
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder [HsConDecl loc [] [] hsname []]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder derives
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder in case typeDefn info of
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder NoTypeDefn -> case Set.toList $ superTypes info of
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder [] -> [ddecl]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder j : _ -> [typeSynonym loc hsTyName $ TypeName j k 0]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder AliasTypeDefn ts ->
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder [hsTypeDecl loc (mkTp $ getAliasArgs ts) $ getAliasType ts]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder DatatypeDefn de -> [sentence $ translateDt env de]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder _ -> [] -- ignore others
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederisSameId :: Id -> Type -> Bool
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederisSameId tid (TypeName tid2 _ _) = tid == tid2
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederisSameId _tid _ty = False
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedertypeSynonym :: SrcLoc -> HsType -> Type -> HsDecl
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedertypeSynonym loc hsname ty =
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder hsTypeDecl loc hsname (translateType ty)
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederkindToTypeArgs :: Int -> RawKind -> [HsType]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaederkindToTypeArgs i k = case k of
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ClassKind _ -> []
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder FunKind _ _ kr ps -> (hsTyVar $ mkSName ("a" ++ show i)
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder $ toProgPos ps)
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder : kindToTypeArgs (i+1) kr
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedergetAliasArgs :: Type -> [HsType]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedergetAliasArgs ty = case ty of
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder TypeAbs v t _ -> getArg v : getAliasArgs t
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ExpandedType _ t -> getAliasArgs t
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder KindedType t _ _ -> getAliasArgs t
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder _ -> []
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedergetArg :: TypeArg -> HsType
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedergetArg ta = hsTyVar $ mkHsIdent LowerId $ getTypeVar ta
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedergetAliasType :: Type -> HsType
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedergetAliasType ty = case ty of
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder TypeAbs _ t _ -> getAliasType t
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder ExpandedType _ t -> getAliasType t
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder KindedType t _ _ -> getAliasType t
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder _ -> translateType ty
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder-- | Translation of an alternative constructor for a datatype definition.
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian MaedertranslateAltDefn :: Env -> Id -> [TypeArg] -> RawKind -> IdMap -> AltDefn
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder -> [HsConDecl HsType [HsType]]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedertranslateAltDefn env dt args rk im (Construct muid origTs p _) =
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder let ts = map (mapType im) origTs
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder in case muid of
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder Just uid -> let loc = toProgPos $ posOfId uid
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder sc = TypeScheme args
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder (getFunType (patToType dt args rk) p ts) nullRange
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -- resolve overloading
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder (c, ui) = translateId env uid sc
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder in case c of
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder UpperId -> -- no existentials, no context
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder [HsConDecl loc [] [] ui $
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder map (HsBangedType . translateType) ts]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder _ -> error "HasCASL2Haskell.translateAltDefn"
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder Nothing -> []
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaedertranslateDt :: Env -> DataEntry -> Named HsDecl
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian MaedertranslateDt env (DataEntry im i _ oargs rk alts) =
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder let j = Map.findWithDefault i i im
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder args = map inVarTypeArg oargs
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder loc = toProgPos $ posOfId i
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder hsname = mkHsIdent UpperId j
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder hsTyName = hsTyCon hsname
946f62de1b188898dde0c472f2a8a6fb86f4d2f5Christian Maeder tp = foldl hsTyApp hsTyName $ map getArg args
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder in
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder (makeNamed ("ga_" ++ showId j "") $ hsDataDecl loc
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder [] -- empty HsContext
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder tp (concatMap (translateAltDefn env j args rk im)
31a189d4cff554f78407cdc422480e84e99a6ec6Christian Maeder $ Set.toList alts)
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder derives) { isDef = True }
678e45c045799ce271c4719123ecd9cf4f456d4bChristian Maeder
6fe64923dcfd4b70bb863a56ad9ca2152faf8a0cChristian Maeder-------------------------------------------------------------------------
6cb518d88084543c13aa7e56db767c14ee97ab77Christian Maeder-- Translation of functions
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder-------------------------------------------------------------------------
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder-- | Converts one distinct named function in HasCASL to the corresponding
08b724e8dcbba5820d80f0974b9a5385140815baChristian Maeder-- haskell declaration.
34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maeder-- Generates a definition (Prelude.undefined) for functions that are not
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder-- defined in HasCASL.
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedertranslateAssump :: (Id, OpInfo) -> [HsDecl]
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedertranslateAssump (i, opinf) =
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder let fname = mkHsIdent LowerId i
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder loc = toProgPos $ posOfId i
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder res = hsTypeSig loc
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder [fname] []
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder $ translateTypeScheme $ opType opinf
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder in case opDefn opinf of
34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian Maeder ConstructData _ -> [] -- wrong case!
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder _ -> [res, functionUndef loc fname]
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder-- | Translation of the result type of a typescheme to a haskell type.
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder-- Uses 'translateType'.
34b55522ba6fe2601e4ee37a9ba1fc4b1a0bf50bChristian MaedertranslateTypeScheme :: TypeScheme -> HsType
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedertranslateTypeScheme (TypeScheme _ t _) =
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder translateType t
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder-- | Translation of types (e.g. product type, type application ...).
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedertranslateType :: Type -> HsType
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian MaedertranslateType t = case getTypeAppl t of
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder (TypeName tid _ n, tyArgs) -> let num = length tyArgs in
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder if n == 0 then
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder if tid == unitTypeId && null tyArgs then
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder hsTyCon $ mkSName "Bool" $ toProgPos $ getRange t
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder else if tid == lazyTypeId && num == 1 then
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder translateType $ head tyArgs
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder else if isArrow tid && num == 2 then
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let [t1, t2] = tyArgs in
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder hsTyFun (translateType t1) (translateType t2)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else if isProductId tid && num > 1 then
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder hsTyTuple loc0 $ map translateType tyArgs
a39175891082dc8a598e5630e5558cb08b84ac0aChristian Maeder else foldl hsTyApp (hsTyCon $ mkHsIdent UpperId tid)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ map translateType tyArgs
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder else foldl hsTyApp (hsTyVar $ mkHsIdent LowerId tid)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder $ map translateType tyArgs
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian Maeder _ -> error "translateType"
f9d358050e368eef1dcb45565b921a70bc68ef2dMihai Codescu
2e9985cd67e4f2414becb670ef33b8f16513e41dChristian MaedertoProgPos :: Range -> SrcLoc
d4146229cf85928342dfd25ec8b579a7feb0d381Christian MaedertoProgPos p = if isNullRange p then loc0
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder else let Range (SourcePos n l c:_) = p
a74f814d3b445eadad6f68737a98a7a303698affChristian Maeder in SrcLoc n (1000 + (l-1) * 80 + c) l c
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder
72b9099aeec0762bae4546db3bc4b48721027bf4Christian MaedermkSName :: String -> SrcLoc -> SN HsName
76647324ed70f33b95a881b536d883daccf9568dChristian MaedermkSName s p = SN (UnQual s) p
717686b54b9650402e2ebfbaadf433eab8ba5171Christian Maeder
405b95208385572f491e1e0207d8d14e31022fa6Christian MaedermkHsIdent :: IdCase -> Id -> SN HsName
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai CodescumkHsIdent c i = mkSName (translateIdWithType c i) $ toProgPos $ posOfId i
f2ee9fc53048ea92bad79e3f5d292d83efd7f8beMihai Codescu
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian MaedertranslateId :: Env -> Id -> TypeScheme -> (IdCase, SN HsName)
8c81b727b788d90ff3b8cbda7b0900c9009243bbChristian MaedertranslateId env uid sc =
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let oid = findUniqueId env uid sc
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mkUnQual :: IdCase -> Id -> (IdCase, SN HsName)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder mkUnQual c j = (c, mkHsIdent c j)
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder in case oid of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder Just (i, oi) -> if isConstructor oi then mkUnQual UpperId i
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder else mkUnQual LowerId i
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder _ -> mkUnQual LowerId uid -- variable
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder-- | Converts a term in HasCASL to an expression in haskell
599766906b25938d5b184febd19b8e0bbe623e7bChristian MaedertranslateTerm :: Env -> Term -> HsExp
599766906b25938d5b184febd19b8e0bbe623e7bChristian MaedertranslateTerm env t =
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder let loc = toProgPos $ getRange t
599766906b25938d5b184febd19b8e0bbe623e7bChristian Maeder in case t of
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder QualVar (VarDecl v ty _ _) ->
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder let (c, i) = translateId env v $ simpleTypeScheme ty in
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder case c of
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder LowerId -> rec $ HsId $ HsVar i
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder _ -> error "translateTerm: variable with UpperId"
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder QualOp _ (PolyId uid _ _) sc _ _ -> let
5a13581acc5a76d392c1dec01657bb3efd4dcf2dChristian Maeder -- The identifier 'uid' may have been renamed. To find its new name,
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder -- the typescheme 'ts' is tested for unifiability with the
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder -- typeschemes of the assumps. If an identifier is found, it is used
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder -- as HsVar or HsCon.
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder mkPHsVar s = rec $ HsPId $ HsVar $ mkSName s loc
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder mkHsVar s = rec $ HsId $ HsVar $ mkSName s loc
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder mkHsCon s = rec $ HsId $ HsCon $ mkSName s loc
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder mkUncurry s = rec $ HsApp (mkHsVar "uncurry") (mkHsVar s)
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder mkErr s = expUndef loc $ s ++ pp loc
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder hTrue = mkHsCon "True"
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder a = mkHsVar "a"
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder b = mkHsVar "b"
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder c = mkHsVar "c"
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder vs2 = [mkPHsVar "a", mkPHsVar "b"]
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder vs3 = vs2 ++ [mkPHsVar "c"]
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder pat2 = [rec $ HsPTuple loc vs2]
72b9099aeec0762bae4546db3bc4b48721027bf4Christian Maeder pat3 = [rec $ HsPTuple loc vs3]
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder mkLam2 x y = rec $ HsParen $ rec $ HsLambda pat2 $ rec $ HsIf x y hTrue
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder mkLam3 x y = rec $ HsParen $ rec $ HsLambda pat3 $ rec $ HsIf x y c
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder in if uid == botId then mkErr "bottom at "
d4146229cf85928342dfd25ec8b579a7feb0d381Christian Maeder else if uid == trueId then hTrue
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder else if uid == falseId then mkHsCon "False"
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder else if uid == notId || uid == negId then mkHsVar "not"
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if uid == defId then rec $ HsRightSection
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder (HsVar $ mkSName "seq" loc) hTrue
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if uid == orId then mkUncurry "||"
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if uid == andId then mkUncurry "&&"
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if uid == eqId || uid == eqvId || uid == exEq then
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder mkErr "equality at "
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if uid == implId then mkLam2 a b
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if uid == infixIf then mkLam2 b a
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if uid == whenElse then mkLam3 b a
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else if uid == ifThenElse then mkLam3 a b
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder else let (cs, ui) = translateId env uid sc
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder in rec $ HsId $ case cs of
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder UpperId -> HsCon ui
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder LowerId -> HsVar ui
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder ApplTerm t1 t2 _ ->
964d1dce6aa88a14e240a4f2fb81c539d2f834fcChristian Maeder rec $ HsApp (translateTerm env t1) $ translateTerm env t2
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder TupleTerm ts _ -> rec $ HsTuple (map (translateTerm env) ts)
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder TypedTerm t1 tqual _ty _ -> -- check for global types later
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder case tqual of
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder InType -> expUndef loc $ show tqual
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder _ -> translateTerm env t1
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder QuantifiedTerm qu _vars _t1 _ -> expUndef loc $ show qu
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder LambdaTerm pats _part t1 _ ->
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder rec $ HsLambda
f42bcc750a9a02cb4f753b70679f9aacf1b338d7Christian Maeder (map (translatePattern env) pats)
5553cf7e344c2b385a72e1244b419e9986042b8eChristian Maeder (translateTerm env t1)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder CaseTerm t1 progeqs _ ->
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder rec $ HsCase (translateTerm env t1)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder (map (translateCaseProgEq env) progeqs)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder LetTerm _ progeqs t1 _ ->
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder rec $ HsLet (map (translateLetProgEq env) progeqs)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder (translateTerm env t1)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder _ -> error ("translateTerm: unexpected term: " ++ show t)
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder
0a320bc4cdbf38f480b75ac15a54db1c4885b497Christian Maeder-- | Conversion of patterns form HasCASL to haskell.
167b6ed8639bce096380defb7311ded501ebb5daChristian MaedertranslatePattern :: Env -> Term -> HsPat
167b6ed8639bce096380defb7311ded501ebb5daChristian MaedertranslatePattern env pat = case pat of
59c301c268f79cfde0a4c30a2c572a368db98da5Christian Maeder QualVar (VarDecl v ty _ _) ->
167b6ed8639bce096380defb7311ded501ebb5daChristian Maeder 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 s = rec $ HsApp (rec $ HsId $ HsVar $ mkSName "error" loc)
$ rec $ HsLit loc $ HsString s
-- 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"]