ComputeTable.hs revision 94e112d16f89130a688db8b03ad3224903f5e97e
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederModule : $Header$
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederDescription : Compute the composition table of a relational algebra
75a6279dbae159d018ef812185416cf6df386c10Till MossakowskiCopyright : (c) Till Mossakowski, Uni Bremen 2002-2005
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederLicense : GPLv2 or higher, see LICENSE.txt
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederMaintainer : till@informatik.uni-bremen.de
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederStability : provisional
7abd0c58a5ce51db13f93de82407b2188d55d298Christian MaederPortability : portable
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian MaederCompute the composition table of a relational algebra
c00adad2e9459b422dee09e3a2bddba66b433bb7Christian Maeder that isspecified in a particular way in a CASL theory.
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maedermodule CASL.CompositionTable.ComputeTable where
e8ffec0fa3d3061061bdc16e44247b9cf96b050fChristian Maederimport CASL.CompositionTable.CompositionTable
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maederimport qualified Common.Lib.Rel as Rel
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maederimport qualified Data.Set as Set
c18e9c3c6d5039618f1f2c05526ece84c7794ea3Christian Maeder-- | given a specfication (name and theory), compute the composition table
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaedercomputeCompTable :: IRI -> (Sign f e, [Named (FORMULA f)])
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -> Result Table
64f7c2188d578b920d8e5513a423449af633e9bcChristian MaedercomputeCompTable spName (sig, nsens) = do
64f7c2188d578b920d8e5513a423449af633e9bcChristian Maeder {- look for something isomorphic to
64f7c2188d578b920d8e5513a423449af633e9bcChristian Maeder sorts BaseRel < Rel
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder id : BaseRel;
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder inv__ : BaseRel -> BaseRel;
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder __cmps__: BaseRel * BaseRel -> Rel;
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder compl__: Rel -> Rel;
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder __cup__ : Rel * Rel -> Rel, assoc, idem, comm, unit 1
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder forall x:BaseRel
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder . x cmps id = x
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder . id cmps x = x
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder . inv(id) = id
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder let name = showDoc spName ""
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder errmsg = "cannot determine composition table of specification " ++ name
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder errSorts = errmsg
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder ++ "\nneed exactly two sorts s,t, with s<t, but found:\n"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder ++ showDoc ((emptySign () :: Sign () ())
bbae6e6ca0de7f2ffbb44d2c8da179f2b717237fChristian Maeder { sortRel = sortRel sig }) ""
e289294500ad68fa0706b09521af340bbb356a69Christian Maeder errOps ops prof =
e289294500ad68fa0706b09521af340bbb356a69Christian Maeder errmsg ++ "\nneed exactly one operation " ++ prof ++ ", but found:\n"
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder ++ showDoc ops ""
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- look for sorts
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder (baseRel, rel) <-
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder case map Set.toList $ Rel.topSort $ sortRel sig of
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder [[b], [r]] -> return (b, r)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder _ -> fail errSorts
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- types of operation symbols
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder let opTypes = mapSetToList (opMap sig)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder invt = mkTotOpType [baseRel] baseRel
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder cmpt = mkTotOpType [baseRel, baseRel] rel
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder complt = mkTotOpType [rel] rel
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder cupt = mkTotOpType [rel, rel] rel
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder -- look for operation symbols
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder let mlookup t = map fst $ filter ((== t) . snd) opTypes
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder let oplookup typ msg =
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder case mlookup typ of
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder [op] -> return op
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder ops -> fail (errOps ops msg )
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder cmps <- oplookup cmpt "__cmps__: BaseRel * BaseRel -> Rel"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder _cmpl <- oplookup complt "compl__: Rel -> Rel"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder inv <- oplookup invt "inv__ : BaseRel -> BaseRel"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder cup <- oplookup cupt "__cup__ : Rel * Rel -> Rel"
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder forall x:BaseRel
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder . x cmps id = x
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder . id cmps x = x
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder . inv(id) = id
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let idaxioms idt =
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder [Quantification Universal [Var_decl [x] baseRel nullRange ....
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let ids = mlookup idt -}
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder let sens = map (stripQuant . sentence) nsens
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder let cmpTab sen = case sen of
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Equation (Application (Qual_op_name c _ _)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder [Application (Qual_op_name arg1 _ _) [] _,
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Application (Qual_op_name arg2 _ _) [] _] _)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Strong res _ ->
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Just $ Cmptabentry
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Cmptabentry_Attrs {
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder cmptabentryArgBaserel1 = Baserel (showDoc arg1 ""),
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder cmptabentryArgBaserel2 = Baserel (showDoc arg2 "") }
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder $ extractRel cup res
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder let invTab sen = case sen of
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Equation (Application (Qual_op_name i _ _)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder [Application (Qual_op_name arg _ _) [] _] _)
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder Strong (Application (Qual_op_name res _ _) [] _) _ ->
0f67ca7b0c738a28f6688ba6e96d44d7c14af611Christian Maeder Just Contabentry {
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder contabentryArgBaseRel = Baserel (showDoc arg ""),
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder contabentryConverseBaseRel = Baserel (showDoc res "") }
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder let attrs = Table_Attrs
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder { tableName = name
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder , tableIdentity = Baserel "id"
9b3bf7c6cf82dc11478bbac3414fe657b9bca327Christian Maeder , baseRelations = []
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder compTable = Compositiontable (mapMaybe cmpTab sens)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder convTable = Conversetable (mapMaybe invTab sens)
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder models = Models []
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian Maeder return $ Table attrs compTable convTable (Reflectiontable []) models
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederstripQuant :: FORMULA f -> FORMULA f
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederstripQuant (Quantification _ _ f _) = stripQuant f
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederstripQuant f = f
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederextractRel :: Id -> TERM f -> [Baserel]
aff01ee50b66032469c232e00c945d1fd4f57d1bChristian MaederextractRel cup (Application (Qual_op_name cup' _ _) [arg1, arg2] _) =
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder if cup == cup'
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder then extractRel cup arg1 ++ extractRel cup arg2
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederextractRel _ (Application (Qual_op_name b _ _) [] _) =
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian Maeder [Baserel (showDoc b "")]
c1124c6303c288db3fcb40518d38169cd7baaa4cChristian MaederextractRel _ _ = []