Qualify.hs revision 9ecf13b5fd914bc7272f1fc17348d7f4a8c77061
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel ManceModule : $Header$
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel ManceDescription : Code out overloading and qualify all names
e9458b1a7a19a63aa4c179f9ab20f4d50681c168Jens ElknerCopyright : (c) Christian Maeder, DFKI GmbH 2008
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel ManceLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel ManceMaintainer : Christian.Maeder@dfki.de
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel ManceStability : provisional
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel MancePortability : portable
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel ManceCode out overloading and qualify all names
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mancemodule CASL.Qualify (qualifySig, inverseMorphism) where
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport qualified Common.Lib.Rel as Rel
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Manceimport qualified Data.Map as Map
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Manceimport qualified Data.Set as Set
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel MancemkOverloadedId :: Int -> Id -> Id
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel MancemkOverloadedId n i =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Id [genToken "Over"] (i : map (stringToId . (: [])) (show n)) $ posOfId i
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel MancemkOrReuseQualSortName :: Sort_map -> SIMPLE_ID -> LIB_ID -> Id -> Id
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel MancemkOrReuseQualSortName sm nodeId libId i =
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance Just j | isQualName j -> j
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance _ -> mkQualName nodeId libId i
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel MancequalifySig :: SIMPLE_ID -> LIB_ID -> Morphism f e () -> Sign f e
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance -> Result (Morphism f e (), [Named (FORMULA f)])
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel MancequalifySig nodeId libId m sig = do
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance let ps = predMap sig
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance os = opMap sig
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance ss = sortSet sig
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance $ mkOrReuseQualSortName (sort_map m) nodeId libId s)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance om = createOpMorMap $ qualOverloaded (Map.map fst $ op_map m)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance nodeId libId (mapOpType sm) (\ o -> o { opKind = Partial }) os
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance $ qualOverloaded (pred_map m) nodeId libId (mapPredType sm) id ps
12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance { sortSet = Set.map (mapSort sm) ss
12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance , sortRel = Rel.map (mapSort sm) $ sortRel sig
12078a24d49ba36b83cda9d07c8e8a480c493fe8Felix Gabriel Mance , emptySortSet = Set.map (mapSort sm) $ emptySortSet sig
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance , opMap = inducedOpMap sm om os
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance , assocOps = inducedOpMap sm om $ assocOps sig
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance , predMap = inducedPredMap sm pm ps }
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder return ((embedMorphism () sig tar)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance { sort_map = sm
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , pred_map = pm }, monotonicities sig)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel MancequalOverloaded :: Ord a => Map.Map (Id, a) Id -> SIMPLE_ID -> LIB_ID
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance -> (a -> a) -> (a -> a) -> Map.Map Id (Set.Set a)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance -> Map.Map (Id, a) (Id, a)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel MancequalOverloaded rn nodeId libId f g =
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Map.foldWithKey (\ i s m -> case Set.toList s of
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance [] -> error "CASL.Qualify.qualOverloaded"
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance m1 = Map.insert (i, gt) (case Map.lookup (i, gt) rn of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just j | isQualName j -> j
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance _ -> mkQualName nodeId libId i, f t) m
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance in foldr (\ (e, n) -> let ge = g e in Map.insert (i, ge)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance (case Map.lookup (i, ge) rn of
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder Just j | isQualName j -> j
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance _ -> mkQualName nodeId libId $ mkOverloadedId n i, f e)) m1
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance $ zip r [2 ..]) Map.empty
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel MancecreateOpMorMap :: Map.Map (Id, OpType) (Id, OpType)
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder -> Map.Map (Id, OpType) (Id, OpKind)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel MancecreateOpMorMap = Map.map (\ (i, t) -> (i, opKind t))
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederinverseMorphism :: (m -> Result m) -> Morphism f e m -> Result (Morphism f e m)
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel ManceinverseMorphism invExt m = do
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance iExt <- invExt $ extended_map m
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance let src = msource m
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance ss = sortSet src
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance os = opMap src
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance ps = predMap src
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance tar = mtarget m
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder sm = sort_map m
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance nss = Set.map (mapSort sm) ss
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance nos = inducedOpMap sm fm os
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance nps = inducedPredMap sm pm ps
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance pm = pred_map m
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance { sortSet = nss
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance , sortRel = Rel.map (mapSort sm) $ sortRel src
3b15ba1ffa9a23ca14f3882d1390abddfc494009Felix Gabriel Mance , emptySortSet = Set.map (mapSort sm) $ emptySortSet src
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder , assocOps = inducedOpMap sm fm $ assocOps src
1f9274bb2aa44ea236327814dce99946be52e348Felix Gabriel Mance , predMap = nps }
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance ism = Map.fromList $ map (\ (s1, s2) -> (s2, s1)) $ Map.toList sm
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance ifm = Map.fromList $ map (\ ((i, t), (j, k)) ->
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance ((j, mapOpType sm t), (i, k))) $ Map.toList fm
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance ipm = Map.fromList $ map (\ ((i, t), j) ->
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance ((j, mapPredType sm t), i)) $ Map.toList pm
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance unless (ss == Set.map (mapSort ism) nss)
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance $ fail "no injective CASL sort mapping"
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance unless (os == inducedOpMap ism ifm nos)
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance $ fail "no injective CASL op mapping"
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance unless (ps == inducedPredMap ism ipm nps)
15d62726781e67fe6458fbcf0a8c46832a7bb8daFelix Gabriel Mance $ fail "no injective CASL pred mapping"
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance return (embedMorphism iExt ntar src)
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance { sort_map = ism
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance , op_map = ifm
8dd62da91d8ac7cfa80cfaff34dc87bb4c2c855bFelix Gabriel Mance , pred_map = ipm }