{- |
Module      :  ./CASL/CompositionTable/ComputeTable.hs
Description :  Compute the composition table of a relational algebra
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Compute the composition table of a relational algebra
  that isspecified in a particular way in a CASL theory.
-}

module CASL.CompositionTable.ComputeTable where

import CASL.CompositionTable.CompositionTable
import CASL.AS_Basic_CASL
import CASL.Sign

import Common.AS_Annotation
import Common.Id
import Common.IRI (IRI)
import Common.DocUtils
import Common.Result
import qualified Common.Lib.Rel as Rel
import qualified Control.Monad.Fail as Fail

import Data.Maybe
import qualified Data.Set as Set

-- | given a specfication (name and theory), compute the composition table
computeCompTable :: IRI -> (Sign f e, [Named (FORMULA f)])
                       -> Result Table
computeCompTable :: IRI -> (Sign f e, [Named (FORMULA f)]) -> Result Table
computeCompTable spName :: IRI
spName (sig :: Sign f e
sig, nsens :: [Named (FORMULA f)]
nsens) = do
  {- look for something isomorphic to
       sorts BaseRel < Rel
       ops
         id      : BaseRel;
         0,1     : Rel;
           inv__ : BaseRel -> BaseRel;
         __cmps__: BaseRel * BaseRel -> Rel;
          compl__: Rel -> Rel;
         __cup__ : Rel * Rel -> Rel, assoc, idem, comm, unit 1
     forall x:BaseRel
     . x cmps id = x
     . id cmps x = x
     . inv(id) = id
  -}
  let name :: String
name = IRI -> ShowS
forall a. Pretty a => a -> ShowS
showDoc IRI
spName ""
      errmsg :: String
errmsg = "cannot determine composition table of specification " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
name
      errSorts :: String
errSorts = String
errmsg
                   String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nneed exactly two sorts s,t, with s<t, but found:\n"
                   String -> ShowS
forall a. [a] -> [a] -> [a]
++ Sign () () -> ShowS
forall a. Pretty a => a -> ShowS
showDoc ((() -> Sign () ()
forall e f. e -> Sign f e
emptySign () :: Sign () ())
                                     { sortRel :: Rel SORT
sortRel = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig }) ""
      errOps :: a -> ShowS
errOps ops :: a
ops prof :: String
prof =
        String
errmsg String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nneed exactly one operation " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
prof String -> ShowS
forall a. [a] -> [a] -> [a]
++ ", but found:\n"
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ a -> ShowS
forall a. Pretty a => a -> ShowS
showDoc a
ops ""
  -- look for sorts
  (baseRel :: SORT
baseRel, rel :: SORT
rel) <-
     case (Set SORT -> [SORT]) -> [Set SORT] -> [[SORT]]
forall a b. (a -> b) -> [a] -> [b]
map Set SORT -> [SORT]
forall a. Set a -> [a]
Set.toList ([Set SORT] -> [[SORT]]) -> [Set SORT] -> [[SORT]]
forall a b. (a -> b) -> a -> b
$ Rel SORT -> [Set SORT]
forall a. Ord a => Rel a -> [Set a]
Rel.topSort (Rel SORT -> [Set SORT]) -> Rel SORT -> [Set SORT]
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sig of
       [[b :: SORT
b], [r :: SORT
r]] -> (SORT, SORT) -> Result (SORT, SORT)
forall (m :: * -> *) a. Monad m => a -> m a
return (SORT
b, SORT
r)
       _ -> String -> Result (SORT, SORT)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail String
errSorts
  -- types of operation symbols
  let opTypes :: [(SORT, OpType)]
opTypes = MapSet SORT OpType -> [(SORT, OpType)]
forall a b. MapSet a b -> [(a, b)]
mapSetToList (Sign f e -> MapSet SORT OpType
forall f e. Sign f e -> MapSet SORT OpType
opMap Sign f e
sig)
      invt :: OpType
invt = [SORT] -> SORT -> OpType
mkTotOpType [SORT
baseRel] SORT
baseRel
      cmpt :: OpType
cmpt = [SORT] -> SORT -> OpType
mkTotOpType [SORT
baseRel, SORT
baseRel] SORT
rel
      complt :: OpType
complt = [SORT] -> SORT -> OpType
mkTotOpType [SORT
rel] SORT
rel
      cupt :: OpType
cupt = [SORT] -> SORT -> OpType
mkTotOpType [SORT
rel, SORT
rel] SORT
rel
  -- look for operation symbols
  let mlookup :: OpType -> [SORT]
mlookup t :: OpType
t = ((SORT, OpType) -> SORT) -> [(SORT, OpType)] -> [SORT]
forall a b. (a -> b) -> [a] -> [b]
map (SORT, OpType) -> SORT
forall a b. (a, b) -> a
fst ([(SORT, OpType)] -> [SORT]) -> [(SORT, OpType)] -> [SORT]
forall a b. (a -> b) -> a -> b
$ ((SORT, OpType) -> Bool) -> [(SORT, OpType)] -> [(SORT, OpType)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((OpType -> OpType -> Bool
forall a. Eq a => a -> a -> Bool
== OpType
t) (OpType -> Bool)
-> ((SORT, OpType) -> OpType) -> (SORT, OpType) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SORT, OpType) -> OpType
forall a b. (a, b) -> b
snd) [(SORT, OpType)]
opTypes
  let oplookup :: OpType -> String -> m SORT
oplookup typ :: OpType
typ msg :: String
msg =
        case OpType -> [SORT]
mlookup OpType
typ of
               [op :: SORT
op] -> SORT -> m SORT
forall (m :: * -> *) a. Monad m => a -> m a
return SORT
op
               ops :: [SORT]
ops -> String -> m SORT
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail ([SORT] -> ShowS
forall a. Pretty a => a -> ShowS
errOps [SORT]
ops String
msg )
  SORT
cmps <- OpType -> String -> Result SORT
forall (m :: * -> *). MonadFail m => OpType -> String -> m SORT
oplookup OpType
cmpt "__cmps__: BaseRel * BaseRel -> Rel"
  SORT
_cmpl <- OpType -> String -> Result SORT
forall (m :: * -> *). MonadFail m => OpType -> String -> m SORT
oplookup OpType
complt "compl__: Rel -> Rel"
  SORT
inv <- OpType -> String -> Result SORT
forall (m :: * -> *). MonadFail m => OpType -> String -> m SORT
oplookup OpType
invt "inv__ : BaseRel -> BaseRel"
  SORT
cup <- OpType -> String -> Result SORT
forall (m :: * -> *). MonadFail m => OpType -> String -> m SORT
oplookup OpType
cupt "__cup__ : Rel * Rel -> Rel"
  {- look for
     forall x:BaseRel
     . x cmps id = x
     . id cmps x = x
     . inv(id) = id
  let idaxioms idt =
  [Quantification Universal [Var_decl [x] baseRel nullRange ....
  let ids = mlookup idt -}
  let sens :: [FORMULA f]
sens = (Named (FORMULA f) -> FORMULA f)
-> [Named (FORMULA f)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripQuant (FORMULA f -> FORMULA f)
-> (Named (FORMULA f) -> FORMULA f)
-> Named (FORMULA f)
-> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence) [Named (FORMULA f)]
nsens
  let cmpTab :: FORMULA f -> Maybe Cmptabentry
cmpTab sen :: FORMULA f
sen = case FORMULA f
sen of
       Equation (Application (Qual_op_name c :: SORT
c _ _)
                        [Application (Qual_op_name arg1 :: SORT
arg1 _ _) [] _,
                         Application (Qual_op_name arg2 :: SORT
arg2 _ _) [] _] _)
                       Strong res :: TERM f
res _ ->
         if SORT
c SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
cmps
           then
            Cmptabentry -> Maybe Cmptabentry
forall a. a -> Maybe a
Just (Cmptabentry -> Maybe Cmptabentry)
-> Cmptabentry -> Maybe Cmptabentry
forall a b. (a -> b) -> a -> b
$ Cmptabentry_Attrs -> [Baserel] -> Cmptabentry
Cmptabentry
                   Cmptabentry_Attrs :: Baserel -> Baserel -> Cmptabentry_Attrs
Cmptabentry_Attrs {
                      cmptabentryArgBaserel1 :: Baserel
cmptabentryArgBaserel1 = String -> Baserel
Baserel (SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
arg1 ""),
                      cmptabentryArgBaserel2 :: Baserel
cmptabentryArgBaserel2 = String -> Baserel
Baserel (SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
arg2 "") }
                   ([Baserel] -> Cmptabentry) -> [Baserel] -> Cmptabentry
forall a b. (a -> b) -> a -> b
$ SORT -> TERM f -> [Baserel]
forall f. SORT -> TERM f -> [Baserel]
extractRel SORT
cup TERM f
res
           else Maybe Cmptabentry
forall a. Maybe a
Nothing
       _ -> Maybe Cmptabentry
forall a. Maybe a
Nothing
  let invTab :: FORMULA f -> Maybe Contabentry
invTab sen :: FORMULA f
sen = case FORMULA f
sen of
       Equation (Application (Qual_op_name i :: SORT
i _ _)
                        [Application (Qual_op_name arg :: SORT
arg _ _) [] _] _)
                       Strong (Application (Qual_op_name res :: SORT
res _ _) [] _) _ ->
         if SORT
i SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
inv
           then
            Contabentry -> Maybe Contabentry
forall a. a -> Maybe a
Just Contabentry :: Baserel -> [Baserel] -> Contabentry
Contabentry {
                   contabentryArgBaseRel :: Baserel
contabentryArgBaseRel = String -> Baserel
Baserel (SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
arg ""),
                   contabentryConverseBaseRel :: [Baserel]
contabentryConverseBaseRel = [String -> Baserel
Baserel (SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
res "")] }
           else Maybe Contabentry
forall a. Maybe a
Nothing
       _ -> Maybe Contabentry
forall a. Maybe a
Nothing
  let attrs :: Table_Attrs
attrs = Table_Attrs :: String -> Baserel -> [Baserel] -> Table_Attrs
Table_Attrs
              { tableName :: String
tableName = String
name
              , tableIdentity :: Baserel
tableIdentity = String -> Baserel
Baserel "id"
              , baseRelations :: [Baserel]
baseRelations = []
              }
      compTable :: Compositiontable
compTable = [Cmptabentry] -> Compositiontable
Compositiontable ((FORMULA f -> Maybe Cmptabentry) -> [FORMULA f] -> [Cmptabentry]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe FORMULA f -> Maybe Cmptabentry
forall f. FORMULA f -> Maybe Cmptabentry
cmpTab [FORMULA f]
sens)
      convTable :: Conversetable
convTable = [Contabentry] -> Conversetable
Conversetable ((FORMULA f -> Maybe Contabentry) -> [FORMULA f] -> [Contabentry]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe FORMULA f -> Maybe Contabentry
forall f. FORMULA f -> Maybe Contabentry
invTab [FORMULA f]
sens)
      models :: Models
models = [Model] -> Models
Models []
  Table -> Result Table
forall (m :: * -> *) a. Monad m => a -> m a
return (Table -> Result Table) -> Table -> Result Table
forall a b. (a -> b) -> a -> b
$ Table_Attrs
-> Compositiontable
-> Conversetable
-> Reflectiontable
-> Models
-> Table
Table Table_Attrs
attrs Compositiontable
compTable Conversetable
convTable ([Reftabentry] -> Reflectiontable
Reflectiontable []) Models
models

stripQuant :: FORMULA f -> FORMULA f
stripQuant :: FORMULA f -> FORMULA f
stripQuant (Quantification _ _ f :: FORMULA f
f _) = FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripQuant FORMULA f
f
stripQuant f :: FORMULA f
f = FORMULA f
f

extractRel :: Id -> TERM f -> [Baserel]
extractRel :: SORT -> TERM f -> [Baserel]
extractRel cup :: SORT
cup (Application (Qual_op_name cup' :: SORT
cup' _ _) [arg1 :: TERM f
arg1, arg2 :: TERM f
arg2] _) =
  if SORT
cup SORT -> SORT -> Bool
forall a. Eq a => a -> a -> Bool
== SORT
cup'
    then SORT -> TERM f -> [Baserel]
forall f. SORT -> TERM f -> [Baserel]
extractRel SORT
cup TERM f
arg1 [Baserel] -> [Baserel] -> [Baserel]
forall a. [a] -> [a] -> [a]
++ SORT -> TERM f -> [Baserel]
forall f. SORT -> TERM f -> [Baserel]
extractRel SORT
cup TERM f
arg2
    else []
extractRel _ (Application (Qual_op_name b :: SORT
b _ _) [] _) =
  [String -> Baserel
Baserel (SORT -> ShowS
forall a. Pretty a => a -> ShowS
showDoc SORT
b "")]
extractRel _ _ = []