Builtin.hs revision e76e6a43f51438215737d6fc176c89da05bb86da
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederModule : $Header$
81d182b21020b815887e9057959228546cf61b6bChristian MaederCopyright : (c) Christian Maeder and Uni Bremen 2003
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederLicence : similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederMaintainer : hets@tzi.de
3f69b6948966979163bdfe8331c38833d5d90ecdChristian MaederStability : experimental
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederPortability : portable
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder HasCASL's builtin types and functions
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maederimport qualified Common.Lib.Map as Map
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maederimport qualified Common.Lib.Set as Set
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian Maederimport qualified Common.Lib.Rel as Rel
ad270004874ce1d0697fb30d7309f180553bb315Christian MaedertrueId = mkId [mkSimpleId trueS]
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaederfalseId = mkId [mkSimpleId falseS]
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederifThenElse :: Id
ee9eddfa6953868fd6fbaff0d9ff68675a13675aChristian MaederifThenElse = mkId (map mkSimpleId [ifS, place, thenS, place, elseS, place])
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederwhenElse :: Id
33a5d53a412ba0a4e5847f7538d6da2e22bd116cChristian MaederwhenElse = mkId (map mkSimpleId [place, whenS, place, elseS, place])
e774ab5733a1d673b123b0e63b14dd533e6fd4fcChristian MaedermkInfix :: String -> Id
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian MaedermkInfix s = mkId $ map mkSimpleId [place, s, place]
62ecb1e7f8fd9573eea8369657de12c7bf9f4f25Christian MaederinfixIf = mkInfix ifS
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederexEq = mkInfix exEqual
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedereqId = mkInfix equalS
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederandId = mkInfix lAnd
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederorId = mkInfix lOr
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaederimplId = mkInfix implS
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedereqvId = mkInfix equivS
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaederdefId = mkId $ map mkSimpleId [defS, place]
66b0bf1e3102c83f5728cf6cfecbd07444276a5fChristian MaedernotId = mkId $ map mkSimpleId [notS, place]
715ffaf874309df081d1e1cd8e05073fc1227729Christian MaedernegId = mkId $ map mkSimpleId [negS, place]
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaederbuiltinRelIds :: Set.Set Id
ccf3de3d66b521a260e5c22d335c64a48e3f0195Christian MaederbuiltinRelIds = Set.fromDistinctAscList [typeId, eqId, exEq, defId]
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaederbuiltinLogIds :: Set.Set Id
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder [andId, eqvId, implId, orId, infixIf, notId]
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian MaederaddBuiltins :: GlobalAnnos -> GlobalAnnos
60303deac79adb97a71e55a4d66f95f26688f05aChristian MaederaddBuiltins ga =
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder let ass = assoc_annos ga
2a598ff0c1b7b51c33aee7029b43bc5cfcbea6b8Christian Maeder [(applId, ALeft), (andId, ALeft), (orId, ALeft),
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder (implId, ARight), (infixIf, ALeft),
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder (whenElse, ARight)]
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder precs = prec_annos ga
60303deac79adb97a71e55a4d66f95f26688f05aChristian Maeder opIds = Set.unions (Set.fromDistinctAscList (Map.keys pMap)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder opIs = Set.toList ((((Set.filter isInfix opIds)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder Set.\\ builtinRelIds) Set.\\ builtinLogIds)
961fc5d08256957f68f245f2723085ced14a0a1fChristian Maeder Set.\\ Set.fromDistinctAscList [applId, whenElse])
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder logs = [(eqvId, implId), (implId, andId), (implId, orId),
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder (eqvId, infixIf), (infixIf, andId), (infixIf, orId),
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder (andId, notId), (orId, notId),
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder (andId, negId), (orId, negId)]
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder rels1 = map ( \ i -> (notId, i)) $ Set.toList builtinRelIds
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder rels1b = map ( \ i -> (negId, i)) $ Set.toList builtinRelIds
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder rels2 = map ( \ i -> (i, whenElse)) $ Set.toList builtinRelIds
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder ops1 = map ( \ i -> (whenElse, i)) (applId : opIs)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder ops2 = map ( \ i -> (i, applId)) (whenElse : opIs)
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder newPrecs = foldr (\ (a, b) p -> if Rel.member b a p then p else
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder concat [logs, rels1, rels1b, rels2, ops1, ops2]
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder in ga { assoc_annos = newAss
df2a122c5ecd7d995323c3f0754e1a2a4e3dc0a8Christian Maeder , prec_annos = Rel.transClosure newPrecs }
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian MaedermkPrecIntMap :: Rel.Rel Id -> PrecMap
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian MaedermkPrecIntMap r =
715ffaf874309df081d1e1cd8e05073fc1227729Christian Maeder m = foldr ( \ (n, s) m1 ->
0ea85310d2beb8aa03cac481ad2a6564e6b8ddbcChristian Maeder Set.fold ( \ i m2 ->Map.insert i n m2) m1 s)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder in (m, Map.find eqId m, l)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederaVar = simpleIdToId $ mkSimpleId "a"
836e72a3c413366ba9801726f3b249c7791cb9caChristian MaederaType = TypeName aVar star (-1)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederbindA :: Type -> TypeScheme
2bf209888545860dc77b9c3f2198d00eeab30d20Christian MaederbindA ty = TypeScheme [TypeArg aVar star Other []] ([] :=> ty) []
36c6cc568751e4235502cfee00ba7b597dae78dcChristian MaedereqType, logType, defType, notType, ifType, whenType, unitType :: TypeScheme
5964438458028e61fdabfa74ca3b4210206cdba6Christian MaedereqType = bindA $
5964438458028e61fdabfa74ca3b4210206cdba6Christian Maeder FunType (ProductType [aType, aType] [])
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder PFunArr logicalType []
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederlogType = simpleTypeScheme $
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian Maeder FunType (ProductType [logicalType, logicalType] [])
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder PFunArr logicalType []
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederdefType = bindA $ FunType aType PFunArr logicalType []
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaedernotType = simpleTypeScheme $ FunType logicalType PFunArr logicalType []
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederifType = bindA $
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder FunType (ProductType [logicalType, aType, aType] [])
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder PFunArr aType []
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederwhenType = bindA $
d48085f765fca838c1d972d2123601997174583dChristian Maeder FunType (ProductType [aType, logicalType, aType] [])
797f811e57952d59e73b8cd03b667eef276db972Christian Maeder PFunArr aType []
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaederunitType = simpleTypeScheme logicalType
f6fc70956d64365527d77a521a96f54a1cc18f91Christian MaederbotId = mkId [mkSimpleId "bottom"]
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederbotType :: TypeScheme
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederbotType = bindA aType
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederbList :: [(Id, TypeScheme)]
3daa82a175c7cfabf22455aa77c4beda327404e4Christian MaederbList = (botId, botType) : (defId, defType) : (notId, notType) :
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder (negId, notType) : (whenElse, whenType) :
f6fc70956d64365527d77a521a96f54a1cc18f91Christian Maeder (trueId, unitType) : (falseId, unitType) :
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder (eqId, eqType) : (exEq, eqType) :
3daa82a175c7cfabf22455aa77c4beda327404e4Christian Maeder map ( \ o -> (o, logType)) [andId, orId, eqvId, implId, infixIf]
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederaddUnit :: TypeMap -> TypeMap
5e26bfc8d7b18cf3a3fa7b919b4450fb669f37a5Christian MaederaddUnit tm = foldr ( \ (i, k, d) m ->
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder Map.insertWith ( \ _ old -> old) i
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (TypeInfo k [k] [] d) m) tm $
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder (simpleIdToId $ mkSimpleId "Unit",
149e43c4a2705a86a0e5fa301ba849fdf19db32eChristian Maeder star, AliasTypeDefn $ simpleTypeScheme logicalType)
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder : (simpleIdToId $ mkSimpleId "Pred",
1738d16957389457347bee85075d3d33d002158fChristian Maeder FunKind star star [],
bdce0d5f7e435df37670d3720929d97ab0043b6bChristian Maeder AliasTypeDefn defType)
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder : (simpleIdToId $ mkSimpleId "Logical",
6e39bfd041946fce4982ac89834be73fd1bfb39aChristian Maeder star, AliasTypeDefn $ simpleTypeScheme $
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder FunType logicalType PFunArr logicalType [])
89dc77946055c0e4cb4671c4a74c3dcd55ed41a1Christian Maeder : (productId, prodKind, NoTypeDefn)
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder : map ( \ a -> (arrowId a, funKind, NoTypeDefn))
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder [FunArr, PFunArr, ContFunArr, PContFunArr]
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaederaddOps :: Assumps -> Assumps
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian MaederaddOps as = foldr ( \ (i, sc) m ->
304c84f22dd78f7979efd81b8fc38c8d2197ed39Christian Maeder Map.insertWith ( \ _ old -> old) i
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian Maeder (OpInfos [OpInfo sc [] (NoOpDefn Fun)]) m) as bList
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaedermkQualOp :: Id -> TypeScheme -> [Pos] -> Term
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaedermkQualOp i sc ps = QualOp Fun (InstOpId i [] ps) sc ps
e215ca0377dc79c9bcfb105157ecc4b958bec67bChristian MaedermkTerm :: Id -> TypeScheme -> [Pos] -> Term -> Term
1d589334ba6b4a4cbfb35307a7a732261e77b0cdChristian MaedermkTerm i sc ps t = ApplTerm (mkQualOp i sc ps) t ps
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedermkBinTerm :: Id -> TypeScheme -> [Pos] -> Term -> Term -> Term
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedermkBinTerm i sc ps t1 t2 = mkTerm i sc ps $ TupleTerm [t1, t2] ps
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedermkLogTerm :: Id -> [Pos] -> Term -> Term -> Term
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedermkLogTerm i ps = mkBinTerm i logType ps
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedermkEqTerm :: Id -> [Pos] -> Term -> Term -> Term
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedermkEqTerm i ps = mkBinTerm i eqType ps
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederunitTerm :: Id -> [Pos] -> Term
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaederunitTerm i ps = mkQualOp i unitType ps
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedertoBinJunctor :: Id -> [Term] -> [Pos] -> Term
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian MaedertoBinJunctor i ts ps = case ts of
d4be42ac0e0c969e95f93bd858e3d14de35cc6aaChristian Maeder [] -> error "toBinJunctor"
2bf209888545860dc77b9c3f2198d00eeab30d20Christian Maeder t:rs -> mkLogTerm i [headPos ps] t
88ece6e49930670e8fd3ee79c89a2e918d2fbd0cChristian Maeder (toBinJunctor i rs (if null ps then [] else tail ps))