1d03ac3e808c2c653316d01713105e209914fc81Neil Madden{- |

1d03ac3e808c2c653316d01713105e209914fc81Neil MaddenModule : $Header$

1d03ac3e808c2c653316d01713105e209914fc81Neil MaddenCopyright : (c) Uni Bremen 2003

1d03ac3e808c2c653316d01713105e209914fc81Neil MaddenLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden

1d03ac3e808c2c653316d01713105e209914fc81Neil MaddenMaintainer : hets@tzi.de

1d03ac3e808c2c653316d01713105e209914fc81Neil MaddenStability : experimental

1d03ac3e808c2c653316d01713105e209914fc81Neil MaddenPortability : portable

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden Translation of the abstract syntax of HasCASL after the static analysis

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden to the abstract syntax of haskell.

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden todo: rename also vars when overloaded

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden-}

590e03a0114f53c994d970cfb356dadaaa57e39dJaco Jooste

1d03ac3e808c2c653316d01713105e209914fc81Neil Maddenmodule ToHaskell.TranslateAna (

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden -- * Translation of an environment

7bf512aea50c834dc9c3ef5a0a228059fcc753a5jenkins translateSig

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden -- * Translation of a map of assumptions

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateAssumps

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , distinctOpIds

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateTypeScheme

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateType

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateFunDef

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden -- ** Translation of terms

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateTerm

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden -- ** Translation of pattern

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translatePattern

4b8b489912a1b73758a1f72ef09b9ac7831731e6jenkins -- ** Translation of toplevel program equation

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateProgEq

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden -- * Translation of a map of types

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateTypeMap

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateTypeInfo

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateAltDefn

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateDt

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , translateSentence

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden , cleanSig

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden ) where

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil Madden

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil Maddenimport Common.Id

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil Maddenimport qualified Common.Lib.Map as Map

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil Maddenimport Common.AS_Annotation

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil Madden

b9e697e180c323785bf1cb8a29f5ec6288da8ec4Jaco Joosteimport HasCASL.As

b9e697e180c323785bf1cb8a29f5ec6288da8ec4Jaco Joosteimport HasCASL.Le

b9e697e180c323785bf1cb8a29f5ec6288da8ec4Jaco Jooste-- import HasCASL.OpDecl

b9e697e180c323785bf1cb8a29f5ec6288da8ec4Jaco Joosteimport HasCASL.ProgEq

b9e697e180c323785bf1cb8a29f5ec6288da8ec4Jaco Jooste

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Joosteimport Haskell.Hatchet.HsSyn

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Jooste

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Joosteimport ToHaskell.TranslateId

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Joosteimport ToHaskell.UniqueId

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Jooste

864e2a74d7dc5e572cd895466611cc57e3523083Andrew Forrest-------------------------------------------------------------------------

864e2a74d7dc5e572cd895466611cc57e3523083Andrew Forrest-- Translation of an HasCASL-Environement

864e2a74d7dc5e572cd895466611cc57e3523083Andrew Forrest-------------------------------------------------------------------------

864e2a74d7dc5e572cd895466611cc57e3523083Andrew Forrest

864e2a74d7dc5e572cd895466611cc57e3523083Andrew Forrest

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington-- | Converts an abstract syntax of HasCASL (after the static analysis)

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington-- to the top datatype of the abstract syntax of haskell.

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington-- Calls 'translateTypeMap' and 'translateAssumps'.

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington-- A True argument includes dummy types for data types.

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill CunningtontranslateSig :: Env -> [HsDecl]

f56a278c148b90f6c2a675e0c1fa8686ca5abed4Robert WapshotttranslateSig env = translateTypeMap (typeMap env) ++

971de91bce73bb05574a64c4304daf9f60e2b5b8Neil Madden translateAssumps (assumps env)

971de91bce73bb05574a64c4304daf9f60e2b5b8Neil Madden

f56a278c148b90f6c2a675e0c1fa8686ca5abed4Robert Wapshott-------------------------------------------------------------------------

f56a278c148b90f6c2a675e0c1fa8686ca5abed4Robert Wapshott-- Translation of types

f56a278c148b90f6c2a675e0c1fa8686ca5abed4Robert Wapshott-------------------------------------------------------------------------

f56a278c148b90f6c2a675e0c1fa8686ca5abed4Robert Wapshott

7fba463e40b49ab852c67041dadb4ac02255bd93Neil Madden-- | Converts all HasCASL types to data or type declarations in haskell.

7fba463e40b49ab852c67041dadb4ac02255bd93Neil Madden-- Uses 'translateData'.

7fba463e40b49ab852c67041dadb4ac02255bd93Neil MaddentranslateTypeMap :: TypeMap -> [HsDecl]

7fba463e40b49ab852c67041dadb4ac02255bd93Neil MaddentranslateTypeMap m = concat $ map translateTypeInfo (Map.assocs m)

7fba463e40b49ab852c67041dadb4ac02255bd93Neil Madden

7fba463e40b49ab852c67041dadb4ac02255bd93Neil Madden-- | Converts one type to a data or type declaration in haskell.

f56a278c148b90f6c2a675e0c1fa8686ca5abed4Robert Wapshott-- Uses 'translateIdWithType'. True includes a dummy type for data types.

f56a278c148b90f6c2a675e0c1fa8686ca5abed4Robert WapshotttranslateTypeInfo :: (TypeId, TypeInfo) -> [HsDecl]

c44bbf5d2025d672efe11a37ea6e9c867e78b691Neil MaddentranslateTypeInfo (tid,info) =

c44bbf5d2025d672efe11a37ea6e9c867e78b691Neil Madden let hsname = (HsIdent (translateIdWithType UpperId tid))

c44bbf5d2025d672efe11a37ea6e9c867e78b691Neil Madden ddecl = HsDataDecl nullLoc

c44bbf5d2025d672efe11a37ea6e9c867e78b691Neil Madden [] -- empty HsContext

c44bbf5d2025d672efe11a37ea6e9c867e78b691Neil Madden hsname

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Jooste (kindToTypeArgs 1 $ typeKind info)

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Jooste [(HsConDecl nullLoc hsname [])]

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Jooste derives

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Jooste in case (typeDefn info) of

3088898b51fb95fdf66ceccd27949ec08465c62fPhill Cunnington NoTypeDefn -> case superTypes info of

3088898b51fb95fdf66ceccd27949ec08465c62fPhill Cunnington [] -> [ddecl]

3088898b51fb95fdf66ceccd27949ec08465c62fPhill Cunnington [si] -> if isSameId tid si then [ddecl] else

3088898b51fb95fdf66ceccd27949ec08465c62fPhill Cunnington [typeSynonym hsname si]

7197110fbdb6deb7868581c455516161cbcf7e0fJaco Jooste si : _ -> [typeSynonym hsname si]

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden Supertype _ ts _ ->

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden [HsTypeDecl nullLoc hsname (getAliasArgs ts) $ getAliasType ts]

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden AliasTypeDefn ts ->

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden [HsTypeDecl nullLoc hsname (getAliasArgs ts) $ getAliasType ts]

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden DatatypeDefn _ args alts ->

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden [HsDataDecl nullLoc [] hsname

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden (map getArg args) -- type arguments

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden (map translateAltDefn alts) derives]

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden _ -> [] -- ignore others

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil MaddenisSameId :: TypeId -> Type -> Bool

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil MaddenisSameId tid (TypeName tid2 _ _) = tid == tid2

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil MaddenisSameId _tid _ty = False

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil Madden

d45a839aef1439938b43cec508f1bbbd3c5c235eNeil MaddentypeSynonym :: HsName -> Type -> HsDecl

1d03ac3e808c2c653316d01713105e209914fc81Neil MaddentypeSynonym hsname ty =

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington HsTypeDecl nullLoc hsname [] (translateType ty)

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington

87e1cbcd02820f55e1816ee4efe9e9127be22a11James PhillpottskindToTypeArgs :: Int -> Kind -> [HsName]

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill CunningtonkindToTypeArgs i k = case k of

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington Universe _ -> []

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington MissingKind -> []

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington ClassKind _ rk -> kindToTypeArgs i rk

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington Downset _ _ rk _ -> kindToTypeArgs i rk

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington FunKind _ kr _ -> HsIdent ("a" ++ show i) : kindToTypeArgs (i+1) kr

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington Intersection l _ -> if null l then error "kindToTypeArgs"

89c76a8c99f25ef6d24c3642f95dde19c5fd4d05Phill Cunnington else kindToTypeArgs i $ head l

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden ExtKind ek _ _ -> kindToTypeArgs i ek

1d03ac3e808c2c653316d01713105e209914fc81Neil Madden

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco Jooste-- | Translation of an alternative constructor for a datatype definition.

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco Jooste-- Uses 'translateRecord'.

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco JoostetranslateAltDefn :: AltDefn -> HsConDecl

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco JoostetranslateAltDefn (Construct uid ts _ _) =

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco Jooste HsConDecl nullLoc

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco Jooste (HsIdent (translateIdWithType UpperId uid))

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco Jooste (map getType ts)

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco Jooste

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco JoostegetType :: Type -> HsBangType

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostegetType t = HsBangedTy (translateType t)

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostegetAliasArgs :: TypeScheme -> [HsName]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostegetAliasArgs (TypeScheme arglist (_plist :=> _t) _poslist) =

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste map getArg arglist

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostegetArg :: TypeArg -> HsName

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostegetArg (TypeArg tid _ _ _) = (HsIdent (translateIdWithType LowerId tid))

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- ist UpperId oder LowerId hier richtig?

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostegetAliasType :: TypeScheme -> HsType

590e03a0114f53c994d970cfb356dadaaa57e39dJaco JoostegetAliasType (TypeScheme _arglist (_plist :=> t) _poslist) = translateType t

305fa812bf6619cb3436c8b1984210fd7f82fca7Jaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-------------------------------------------------------------------------

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- Translation of functions

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-------------------------------------------------------------------------

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- | Converts functions in HasCASL to the coresponding haskell declarations.

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostetranslateAssumps :: Assumps -> [HsDecl]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostetranslateAssumps as =

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste let distList = distinctOpIds 0 $ Map.toList as

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste in concatMap translateAssump distList

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- | Converts one distinct named function in HasCASL to the corresponding

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- haskell declaration.

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- Generates a definition (Prelude.undefined) for functions that are not

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- defined in HasCASL.

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostetranslateAssump :: (Id, OpInfo) -> [HsDecl]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostetranslateAssump (i, opinf) =

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste let fname = translateIdWithType LowerId i

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste res = HsTypeSig nullLoc

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste [(HsIdent fname)]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste (translateTypeScheme (opType opinf))

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste in case (opDefn opinf) of

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste VarDefn -> []

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste ConstructData _ -> [] -- wrong case!

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste _ -> [res, (functionUndef fname)]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- | Translation of the result type of a typescheme to a haskell type.

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- Uses 'translateType'.

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostetranslateTypeScheme :: TypeScheme -> HsQualType

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostetranslateTypeScheme (TypeScheme _arglist (_plist :=> t) _poslist) =

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste HsUnQualType (translateType t)

590e03a0114f53c994d970cfb356dadaaa57e39dJaco Jooste-- The context (in the _plist) is not yet used in HasCASL

305fa812bf6619cb3436c8b1984210fd7f82fca7Jaco Jooste-- arglist ??

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste-- | Translation of types (e.g. product type, type application ...).

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostetranslateType :: Type -> HsType

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco JoostetranslateType t =

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste case t of

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste FunType t1 _arr t2 _poslist -> HsTyFun (translateType t1) (translateType t2)

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste ProductType tlist _poslist -> if null tlist

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste then HsTyCon (UnQual (HsIdent "Bool"))

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste else HsTyTuple (map translateType tlist)

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste LazyType lt _poslist -> translateType lt

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste KindedType kt _kind _poslist -> translateType kt

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste TypeAppl t1 t2 -> HsTyApp (translateType t1) (translateType t2)

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste TypeName tid _kind n ->

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste if n > 0 then

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste HsTyVar (HsIdent (translateIdWithType LowerId tid))

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste else

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste HsTyCon (UnQual (HsIdent (translateIdWithType UpperId tid)))

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste _ -> error ("translateType: unexpected type: " ++ show t)

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste-- | Generates a type signature and a definition of a function in haskell

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste-- from the corresponding information in HasCASL.

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco JoostetranslateFunDef :: Assumps -> TypeMap -> Id -> TypeScheme -> Term -> [HsDecl]

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco JoostetranslateFunDef as tm i ts term =

590e03a0114f53c994d970cfb356dadaaa57e39dJaco Jooste let fname = translateIdWithType LowerId i

590e03a0114f53c994d970cfb356dadaaa57e39dJaco Jooste in [HsTypeSig nullLoc

590e03a0114f53c994d970cfb356dadaaa57e39dJaco Jooste [(HsIdent fname)]

590e03a0114f53c994d970cfb356dadaaa57e39dJaco Jooste (translateTypeScheme ts)] ++

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste [HsFunBind [HsMatch nullLoc

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste (UnQual (HsIdent fname)) --HsName

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste (getPattern term) -- [HsPat]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste (getRhs as tm term) -- HsRhs

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste [] -- {-where-} [HsDecl]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste ]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste ]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostegetPattern :: Term -> [HsPat]

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco JoostegetPattern _t = []

ece5a262d20a50d0abf584d0f7ec73929ede9cfdJaco Jooste

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco JoostegetRhs :: Assumps -> TypeMap -> Term -> HsRhs

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco JoostegetRhs as tm t = HsUnGuardedRhs (translateTerm as tm t)

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco Jooste

abffea1c30ac3b8508f7d708cdd90d9198b64e04Jaco JoosteisConstructId :: Id -> [(Id,OpInfos)] -> Bool

305fa812bf6619cb3436c8b1984210fd7f82fca7Jaco JoosteisConstructId _ [] = False

305fa812bf6619cb3436c8b1984210fd7f82fca7Jaco JoosteisConstructId i ((i1,info1):idInfoList) =

305fa812bf6619cb3436c8b1984210fd7f82fca7Jaco Jooste if i == i1 then

305fa812bf6619cb3436c8b1984210fd7f82fca7Jaco Jooste or $ map isConstructor $ opInfos info1

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste else isConstructId i idInfoList

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste-- | Converts a term in HasCASL to an expression in haskell

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco JoostetranslateTerm :: Assumps -> TypeMap -> Term -> HsExp

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco JoostetranslateTerm as tm t =

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste let undef = HsVar $ UnQual $ HsIdent "undefined" in

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste case t of

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste QualVar v _ty _pos -> HsVar $ UnQual $ HsIdent $

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste translateIdWithType LowerId v

4701cb94cccc5ef52c5333593fe9dd5a2376a9d9Jaco Jooste QualOp _ (InstOpId uid _types _) ts _pos ->

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

-- the typescheme 'ts' is tested for "Unifizierbarkeit" with the

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

-- as HsVar or HsCon.

let oid = findUniqueId uid ts tm as

in case oid of

Just i ->

if isConstructId i $ Map.toList as then

(HsCon (UnQual (HsIdent (translateIdWithType UpperId i))))

else (HsVar (UnQual (HsIdent (translateIdWithType LowerId i))))

_ -> error("translateTerm: non-unique id: " ++ show t)

ApplTerm t1 t2 _pos -> let at = translateTerm as tm t2 in

HsApp (translateTerm as tm t1) $ (case at of

HsTuple _ -> id

HsCon _ -> id

HsVar _ -> id

_ -> HsParen) at

TupleTerm ts _pos -> HsTuple (map (translateTerm as tm) ts)

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

let res = translateTerm as tm t1

in case tqual of

InType -> undef

_ -> res

QuantifiedTerm _quant _vars _t1 _pos -> undef

LambdaTerm pats _part t1 _pos ->

HsLambda nullLoc

(map (translatePattern as tm) pats)

(translateTerm as tm t1)

CaseTerm t1 progeqs _pos ->

HsCase (translateTerm as tm t1)

(map(translateCaseProgEq as tm)progeqs)

LetTerm _ progeqs t1 _pos ->

HsLet (map (translateLetProgEq as tm) progeqs)

(translateTerm as tm t1)

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

-- | Conversion of patterns form HasCASL to haskell.

translatePattern :: Assumps -> TypeMap -> Pattern -> HsPat

translatePattern as tm pat = case pat of

QualVar v _ty _pos

-> HsPVar $ HsIdent $ translateIdWithType LowerId v

QualOp _ (InstOpId uid _t _p) ts _pos ->

let oid = findUniqueId uid ts tm as

in case oid of

Just i ->

HsPApp (UnQual $ HsIdent $ translateIdWithType UpperId i) []

_ -> error ("translatePattern: non-unique id: " ++ show pat)

ApplTerm p1 p2 _pos ->

let tp = translatePattern as tm p1

a = translatePattern as tm p2

in case tp of

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

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

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

TupleTerm pats _pos ->

HsPTuple $ map (translatePattern as tm) pats

TypedTerm p OfType _ty _pos -> translatePattern as tm p

--the type is implicit

--AsPattern pattern pattern pos -> HsPAsPat name pattern ??

AsPattern _p1 _p2 _pos -> error "AsPattern nyi"

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

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

translateCaseProgEq :: Assumps -> TypeMap -> ProgEq -> HsAlt

translateCaseProgEq as tm (ProgEq pat t _pos) =

HsAlt nullLoc

(translatePattern as tm pat)

(HsUnGuardedAlt (translateTerm as tm t))

[]

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

translateLetProgEq ::Assumps -> TypeMap -> ProgEq -> HsDecl

translateLetProgEq as tm (ProgEq pat t _pos) =

HsPatBind nullLoc

(translatePattern as tm pat)

(HsUnGuardedRhs (translateTerm as tm t))

[]

-- | Translation of a toplevel program equation

translateProgEq ::Assumps -> TypeMap -> ProgEq -> HsDecl

translateProgEq as tm (ProgEq pat t _) =

case getAppl pat of

Just (uid, ts, args) ->

let oid = findUniqueId uid ts tm as

in case oid of

Just i -> HsFunBind [HsMatch nullLoc

(UnQual $ HsIdent $ translateIdWithType LowerId i)

(map (translatePattern as tm) args) -- [HsPat]

(HsUnGuardedRhs $ translateTerm as tm t) -- HsRhs

[]]

_ -> error ("translateLetProgEq: non-unique id: " ++ show pat)

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

translateDt :: DatatypeDefn -> Named HsDecl

translateDt (DatatypeConstr i _ _ args alts) =

let hsname = HsIdent $ translateIdWithType UpperId i in

NamedSen ("ga_" ++ showId i "") $

HsDataDecl nullLoc

[] -- empty HsContext

hsname

(map getArg args) -- type arguments

(map translateAltDefn alts) -- [HsConDecl]

derives

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

translateSentence env sen =

let as = assumps env

tm = typeMap env

in case sentence sen of

DatatypeSen dt -> map translateDt dt

ProgEqSen _ _ pe -> [NamedSen (senName sen)

$ translateProgEq as tm pe]

_ -> []

-------------------------------------------------------------------------

-- some stuff

-------------------------------------------------------------------------

-- The positions in the source code are not necessary during the translation,

-- therefore the same SrcLoc is used everywhere.

nullLoc :: SrcLoc

nullLoc = SrcLoc 1 0

-- For the definition of an undefined function.

-- Takes the name of the function as argument.

functionUndef :: String -> HsDecl

functionUndef s =

HsPatBind nullLoc

(HsPVar (HsIdent s))

(HsUnGuardedRhs (HsVar (UnQual (HsIdent "undefined"))))

[]

-- | remove dummy decls given by sentences

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

cleanSig ds sens =

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

HsDataDecl _ _ n _ _ _ -> n : l

_ -> l) [] sens

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

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

_ -> l) [] sens

in filter ( \ hs -> case hs of

HsDataDecl _ _ n _ _ _ -> n `notElem` dds

HsTypeDecl _ n _ _ -> n `notElem` dds

HsPatBind _ (HsPVar n) _ _ -> UnQual n `notElem` funs

_ -> True)

ds

derives :: [HsQName]

derives = [(UnQual $ HsIdent "Show"), (UnQual $ HsIdent "Eq"),

(UnQual $ HsIdent "Ord")]