ComputeTable.hs revision b87efd3db0d2dc41615ea28669faf80fc1b48d56
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederModule : $Header$
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederDescription : Compute the composition table of a relational algebra
cd7372fc7e6e43c389619f63daa6eb872d9d5b16Christian MaederCopyright : (c) Till Mossakowski, Uni Bremen 2002-2005
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederLicense : GPLv2 or higher
c3d42e13d2a7c3749229498658aec34e7e4fd0a0Christian MaederMaintainer : till@informatik.uni-bremen.de
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederStability : provisional
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian MaederPortability : portable
99c923311eab71a85f1dcc4785d349609c828da4Christian MaederCompute the composition table of a relational algebra
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maeder that isspecified in a particular way in a CASL theory.
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maedermodule CASL.CompositionTable.ComputeTable where
d5ef5a29a89fa5548f81fcd49fcf0ffda69d45b0Christian Maederimport CASL.CompositionTable.CompositionTable
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport qualified Data.Map as Map
ce31795240d8fb340bc984b8b35147c955e29afaChristian Maederimport qualified Data.Set as Set
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torriniimport qualified Common.Lib.Rel as Rel
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder-- | given a specfication (name and theory), compute the composition table
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicomputeCompTable :: SIMPLE_ID -> (Sign f e, [Named (FORMULA f)])
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -> Result Table
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinicomputeCompTable spName (sig,nsens) = do
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder {- look for something isomorphic to
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sorts BaseRel < Rel
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini id : BaseRel;
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini inv__ : BaseRel -> BaseRel;
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini __cmps__: BaseRel * BaseRel -> Rel;
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini compl__: Rel -> Rel;
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini __cup__ : Rel * Rel -> Rel, assoc, idem, comm, unit 1
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini forall x:BaseRel
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini . x cmps id = x
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini . id cmps x = x
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini . inv(id) = id
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let name = showDoc spName ""
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini errmsg = "cannot determine composition table of specification "++name
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini errSorts = errmsg
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ "\nneed exactly two sorts s,t, with s<t, but found:\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ showDoc ((emptySign ()::Sign () ())
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini { sortSet = sortSet sig,
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini sortRel = sortRel sig }) ""
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini errOps ops prof =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini errmsg ++ "\nneed exactly one operation "++prof++", but found:\n"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini ++ showDoc ops ""
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- look for sorts
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini (baseRel,rel) <-
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini case map Set.toList $ Rel.topSort $ sortRel sig of
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini [[b],[r]] -> return (b,r)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini _ -> fail errSorts
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- types of operation symbols
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let opTypes = concatMap (\ (o, ts) ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini map ( \ ty -> (ty, o) ) $ Set.toList ts)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- idt = OpType {opKind = Total, opArgs = [], opRes = baseRel}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- zerot = OpType {opKind = Total, opArgs = [], opRes = rel}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini invt = OpType {opKind = Total, opArgs = [baseRel], opRes = baseRel}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini cmpt = OpType {opKind = Total, opArgs = [baseRel,baseRel],
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini complt = OpType {opKind = Total, opArgs = [rel], opRes = rel}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini cupt = OpType {opKind = Total, opArgs = [rel,rel], opRes = rel}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- look for operation symbols
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let mlookup t = map snd $ filter (\(t',_) -> t==t') opTypes
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let oplookup typ msg =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini case mlookup typ of
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini [op] -> return op
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini ops -> fail (errOps ops msg )
38f8320f50c5f63965ba42e4e48f38be07c823cfChristian Maeder cmps <- oplookup cmpt "__cmps__: BaseRel * BaseRel -> Rel"
aa436590b8c7f5035f5cf657d6de163046bc23eaPaolo Torrini _cmpl <- oplookup complt "compl__: Rel -> Rel"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini inv <- oplookup invt "inv__ : BaseRel -> BaseRel"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini cup <- oplookup cupt "__cup__ : Rel * Rel -> Rel"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini forall x:BaseRel
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini . x cmps id = x
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini . id cmps x = x
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini . inv(id) = id -}
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini -- let idaxioms idt =
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly -- [Quantification Universal [Var_decl [x] baseRel nullRange ....
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly -- let ids = mlookup idt
226d4df216d0d67423d139ead4744eb66fb62ac1Liam O'Reilly let sens = map (stripQuant . sentence) nsens
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly let cmpTab sen = case sen of
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly Strong_equation (Application (Qual_op_name c _ _)
d9c1248c7972dfdafbacb1b73b2eb965eac9ef42Liam O'Reilly [Application (Qual_op_name arg1 _ _) [] _,
33bdce26495121cdbce30331ef90a1969126a840Liam O'Reilly Application (Qual_op_name arg2 _ _) [] _] _)
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly Just (Cmptabentry
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (Cmptabentry_Attrs {
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly cmptabentryArgBaserel1 = Baserel (showDoc arg1 ""),
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly cmptabentryArgBaserel2 = Baserel (showDoc arg2 "") })
d3b4ad111a281d125659e12d6641943f29d6b3dfLiam O'Reilly (extractRel cup res) )
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let invTab sen = case sen of
120c9bff9059626735fc12b0399dcc9e5a62c345Christian Maeder Strong_equation (Application (Qual_op_name i _ _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder [Application (Qual_op_name arg _ _) [] _] _)
99c923311eab71a85f1dcc4785d349609c828da4Christian Maeder (Application (Qual_op_name res _ _) [] _) _ ->
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini Just (Contabentry {
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini contabentryArgBaseRel = Baserel (showDoc arg ""),
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini contabentryConverseBaseRel = Baserel (showDoc res "") } )
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini let attrs = Table_Attrs
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini { tableName = name
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , tableIdentity = Baserel "id"
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini , baseRelations = []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini compTable = Compositiontable (mapMaybe cmpTab sens)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini convTable = Conversetable (mapMaybe invTab sens)
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini models = Models []
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini return $ Table attrs compTable convTable (Reflectiontable []) models
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinistripQuant :: FORMULA f -> FORMULA f
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinistripQuant (Quantification _ _ f _) = stripQuant f
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorrinistripQuant f = f
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniextractRel :: Id -> TERM f -> [Baserel]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniextractRel cup (Application (Qual_op_name cup' _ _) [arg1,arg2] _) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini then extractRel cup arg1 ++ extractRel cup arg2
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniextractRel _ (Application (Qual_op_name b _ _) [] _) =
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo Torrini [Baserel (showDoc b "")]
1b0778e21d9b3e71a684ad6e901e8a0e7d57ee1cPaolo TorriniextractRel _ _ = []