Qualify.hs revision d0c66a832d7b556e20ea4af4852cdc27a5463d51
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeModule : $Header$
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerDescription : Code out overloading and qualify all names
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederCopyright : (c) Christian Maeder, DFKI GmbH 2008
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeMaintainer : Christian.Maeder@dfki.de
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeStability : provisional
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkePortability : portable
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeCode out overloading and qualify all names
501e4e6b8288a5b73d7d4b8d8b80817f9bf8e60fJonathan von Schroedermodule CASL.Qualify (qualifySig, inverseMorphism) where
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartkeimport qualified Common.Lib.Rel as Rel
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport qualified Data.Map as Map
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maederimport qualified Data.Set as Set
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedermkOverloadedId :: Int -> Id -> Id
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaedermkOverloadedId n i =
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder Id [genToken "Over"] (i : map (stringToId . (: [])) (show n)) $ posOfId i
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkemkOrReuseQualSortName :: Sort_map -> SIMPLE_ID -> LIB_ID -> Id -> Id
1a38107941725211e7c3f051f7a8f5e12199f03acmaedermkOrReuseQualSortName sm nodeId libId i =
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Just j | isQualName j -> j
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder _ -> mkQualName nodeId libId i
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkequalifySig :: SIMPLE_ID -> LIB_ID -> Morphism f e () -> Sign f e
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder -> Result (Morphism f e (), [Named (FORMULA f)])
1a38107941725211e7c3f051f7a8f5e12199f03acmaederqualifySig nodeId libId m sig = do
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke let ps = predMap sig
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder os = opMap sig
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke ss = sortSet sig
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder $ mkOrReuseQualSortName (sort_map m) nodeId libId s)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke om = createFunMap $ qualOverloaded (Map.map fst $ fun_map m)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nodeId libId (mapOpType sm) (\ o -> o { opKind = Partial }) os
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke $ qualOverloaded (pred_map m) nodeId libId (mapPredType sm) id ps
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder { sortSet = Set.map (mapSort sm) ss
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , sortRel = Rel.map (mapSort sm) $ sortRel sig
1a38107941725211e7c3f051f7a8f5e12199f03acmaeder , emptySortSet = Set.map (mapSort sm) $ emptySortSet sig
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke , opMap = inducedOpMap sm om os
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke , assocOps = inducedOpMap sm om $ assocOps sig
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke , predMap = inducedPredMap sm pm ps }
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke return ((embedMorphism () sig tar)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder { sort_map = sm
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke , fun_map = om
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , pred_map = pm }, monotonicities sig)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkequalOverloaded :: Ord a => Map.Map (Id, a) Id -> SIMPLE_ID -> LIB_ID
656f17ae9b7610ff2de1b6eedeeadea0c3bcdc8dChristian Maeder -> (a -> a) -> (a -> a) -> Map.Map Id (Set.Set a)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke -> Map.Map (Id, a) (Id, a)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederqualOverloaded rn nodeId libId f g =
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Map.foldWithKey (\ i s m -> case Set.toList s of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder [] -> error "CASL.Qualify.qualOverloaded"
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder m1 = Map.insert (i, gt) (case Map.lookup (i, gt) rn of
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Just j | isQualName j -> j
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke _ -> mkQualName nodeId libId i, f t) m
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke in foldr (\ (e, n) -> let ge = g e in Map.insert (i, ge)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke (case Map.lookup (i, ge) rn of
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke Just j | isQualName j -> j
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke _ -> mkQualName nodeId libId $ mkOverloadedId n i, f e)) m1
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke $ zip r [2 ..]) Map.empty
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkecreateFunMap :: Map.Map (Id, OpType) (Id, OpType)
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder -> Map.Map (Id, OpType) (Id, FunKind)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkecreateFunMap = Map.map (\ (i, t) -> (i, opKind t))
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian MaederinverseMorphism :: (m -> Result m) -> Morphism f e m -> Result (Morphism f e m)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus HartkeinverseMorphism invExt m = do
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder iExt <- invExt $ extended_map m
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let src = msource m
a23e572c8f957cc051a1b0831abd6fe9380d45c7Christian Maeder ss = sortSet src
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder os = opMap src
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ps = predMap src
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder tar = mtarget m
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder sm = sort_map m
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder nss = Set.map (mapSort sm) ss
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder nos = inducedOpMap sm fm os
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke nps = inducedPredMap sm pm ps
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke fm = fun_map m
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke pm = pred_map m
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke { sortSet = nss
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke , sortRel = Rel.map (mapSort sm) $ sortRel src
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke , emptySortSet = Set.map (mapSort sm) $ emptySortSet src
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke , opMap = nos
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , assocOps = inducedOpMap sm fm $ assocOps src
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder , predMap = nps }
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ism = Map.fromList $ map (\ (s1, s2) -> (s2, s1)) $ Map.toList sm
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ifm = Map.fromList $ map (\ ((i, t), (j, k)) ->
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder ((j, mapOpType sm t), (i, k))) $ Map.toList fm
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke ipm = Map.fromList $ map (\ ((i, t), j) ->
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ((j, mapPredType sm t), i)) $ Map.toList pm
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder unless (ss == Set.map (mapSort ism) nss)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke $ fail "no injective CASL sort mapping"
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder unless (os == inducedOpMap ism ifm nos)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke $ fail "no injective CASL op mapping"
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke unless (ps == inducedPredMap ism ipm nps)
9f93539f2fa4f5b9d935c7baa22fcd750806def9Klaus Hartke $ fail "no injective CASL pred mapping"