{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/RelScheme2CASL.hs
Description :  Comorphism from RelScheme to CASL
Copyright   :  (c) Dominik Luecke and Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

The translating comorphism from DL to CASL_DL basically this is an
identity comorphism from SROIQ(D) to SROIQ(D)
-}

module Comorphisms.RelScheme2CASL
    (
     RelScheme2CASL (..)
    )
    where

import Logic.Logic
import Logic.Comorphism

import Common.AS_Annotation
import Common.Id
import Common.ProofTree
import Common.Result
import Common.Utils (number)
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import qualified Data.Set as Set
import qualified Data.Map as Map

-- RelScheme
import RelationalScheme.Logic_Rel as LRel
import RelationalScheme.AS as ARel
import qualified RelationalScheme.Sign as SRel

-- CASL = codomain
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.Morphism

data RelScheme2CASL = RelScheme2CASL deriving (Int -> RelScheme2CASL -> ShowS
[RelScheme2CASL] -> ShowS
RelScheme2CASL -> String
(Int -> RelScheme2CASL -> ShowS)
-> (RelScheme2CASL -> String)
-> ([RelScheme2CASL] -> ShowS)
-> Show RelScheme2CASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [RelScheme2CASL] -> ShowS
$cshowList :: [RelScheme2CASL] -> ShowS
show :: RelScheme2CASL -> String
$cshow :: RelScheme2CASL -> String
showsPrec :: Int -> RelScheme2CASL -> ShowS
$cshowsPrec :: Int -> RelScheme2CASL -> ShowS
Show)

instance Language RelScheme2CASL

instance Comorphism
    RelScheme2CASL      -- comorphism
    RelScheme              -- lid domain
    ()              -- sublogics domain
    RSScheme         -- Basic spec domain
    Sentence     -- sentence domain
    ()              -- symbol items domain
    ()              -- symbol map items domain
    SRel.Sign        -- signature domain
    SRel.RSMorphism  -- morphism domain
    SRel.RSSymbol    -- symbol domain
    SRel.RSRawSymbol -- rawsymbol domain
    ()              -- proof tree codomain
    CASL         -- lid codomain
    CASL_Sublogics              -- sublogics codomain
    CASLBasicSpec   -- Basic spec codomain
    CASLFORMULA       -- sentence codomain
    SYMB_ITEMS      -- symbol items codomain
    SYMB_MAP_ITEMS  -- symbol map items codomain
    CASLSign          -- signature codomain
    CASLMor           -- morphism codomain
    Symbol          -- symbol codomain
    RawSymbol       -- rawsymbol codomain
    ProofTree              -- proof tree domain
        where
          sourceLogic :: RelScheme2CASL -> RelScheme
sourceLogic RelScheme2CASL = RelScheme
RelScheme
          sourceSublogic :: RelScheme2CASL -> ()
sourceSublogic RelScheme2CASL = ()
          targetLogic :: RelScheme2CASL -> CASL
targetLogic RelScheme2CASL = CASL
CASL
          mapSublogic :: RelScheme2CASL -> () -> Maybe CASL_Sublogics
mapSublogic RelScheme2CASL _ = CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
          map_theory :: RelScheme2CASL
-> (Sign, [Named Sentence])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory RelScheme2CASL = (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA])
map_RelScheme_theory
          map_morphism :: RelScheme2CASL -> RSMorphism -> Result CASLMor
map_morphism RelScheme2CASL = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLMor -> Result CASLMor)
-> (RSMorphism -> CASLMor) -> RSMorphism -> Result CASLMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSMorphism -> CASLMor
mapMorphism
          map_sentence :: RelScheme2CASL -> Sign -> Sentence -> Result CASLFORMULA
map_sentence RelScheme2CASL = Sign -> Sentence -> Result CASLFORMULA
mapSen
          isInclusionComorphism :: RelScheme2CASL -> Bool
isInclusionComorphism RelScheme2CASL = Bool
True

map_RelScheme_theory :: (SRel.Sign, [Named Sentence])
                     -> Result (CASLSign, [Named CASLFORMULA])
map_RelScheme_theory :: (Sign, [Named Sentence]) -> Result (CASLSign, [Named CASLFORMULA])
map_RelScheme_theory (sig :: Sign
sig, n_sens :: [Named Sentence]
n_sens) = do
     let tsign :: CASLSign
tsign = Sign -> CASLSign
mapSign Sign
sig
     [[Named CASLFORMULA]]
tax <- (RSTable -> Result [Named CASLFORMULA])
-> [RSTable] -> Result [[Named CASLFORMULA]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM RSTable -> Result [Named CASLFORMULA]
genAxioms ([RSTable] -> Result [[Named CASLFORMULA]])
-> [RSTable] -> Result [[Named CASLFORMULA]]
forall a b. (a -> b) -> a -> b
$ Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList (Set RSTable -> [RSTable]) -> Set RSTable -> [RSTable]
forall a b. (a -> b) -> a -> b
$ Sign -> Set RSTable
SRel.tables Sign
sig
     [Named CASLFORMULA]
tsens <- (Named Sentence -> Result (Named CASLFORMULA))
-> [Named Sentence] -> Result [Named CASLFORMULA]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM (Sign -> Named Sentence -> Result (Named CASLFORMULA)
mapNamedSen Sign
sig) [Named Sentence]
n_sens
     (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
tsign, [[Named CASLFORMULA]] -> [Named CASLFORMULA]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([Named CASLFORMULA]
tsens [Named CASLFORMULA]
-> [[Named CASLFORMULA]] -> [[Named CASLFORMULA]]
forall a. a -> [a] -> [a]
: [[Named CASLFORMULA]]
tax))

mapSign :: SRel.Sign -> CASLSign
mapSign :: Sign -> CASLSign
mapSign sig :: Sign
sig = let
 (sorts :: Set RSRawSymbol
sorts, ops :: OpMap
ops, preds :: PredMap
preds) = [RSTable]
-> Set RSRawSymbol
-> OpMap
-> PredMap
-> (Set RSRawSymbol, OpMap, PredMap)
genCASLSig (Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList (Set RSTable -> [RSTable]) -> Set RSTable -> [RSTable]
forall a b. (a -> b) -> a -> b
$ Sign -> Set RSTable
SRel.tables Sign
sig)
                                Set RSRawSymbol
forall a. Set a
Set.empty OpMap
forall a b. MapSet a b
MapSet.empty PredMap
forall a b. MapSet a b
MapSet.empty
              in (() -> CASLSign
forall e f. e -> Sign f e
emptySign ()) {
                  sortRel :: Rel RSRawSymbol
sortRel = Set RSRawSymbol -> Rel RSRawSymbol
forall a. Ord a => Set a -> Rel a
Rel.fromKeysSet Set RSRawSymbol
sorts,
                  opMap :: OpMap
opMap = OpMap
ops,
                  predMap :: PredMap
predMap = PredMap
preds
                 }

mapMorphism :: SRel.RSMorphism -> CASLMor
mapMorphism :: RSMorphism -> CASLMor
mapMorphism phi :: RSMorphism
phi = let
  ssign :: CASLSign
ssign = Sign -> CASLSign
mapSign (Sign -> CASLSign) -> Sign -> CASLSign
forall a b. (a -> b) -> a -> b
$ RSMorphism -> Sign
SRel.domain RSMorphism
phi
                  in
  Morphism :: forall f e m.
Sign f e
-> Sign f e
-> Sort_map
-> Op_map
-> Pred_map
-> m
-> Morphism f e m
Morphism {
   msource :: CASLSign
msource = CASLSign
ssign,
   mtarget :: CASLSign
mtarget = Sign -> CASLSign
mapSign (Sign -> CASLSign) -> Sign -> CASLSign
forall a b. (a -> b) -> a -> b
$ RSMorphism -> Sign
SRel.codomain RSMorphism
phi,
   sort_map :: Sort_map
sort_map = Sort_map
forall k a. Map k a
Map.empty,
   op_map :: Op_map
op_map = [((RSRawSymbol, OpType), (RSRawSymbol, OpKind))] -> Op_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((RSRawSymbol, OpType), (RSRawSymbol, OpKind))] -> Op_map)
-> [((RSRawSymbol, OpType), (RSRawSymbol, OpKind))] -> Op_map
forall a b. (a -> b) -> a -> b
$
     ((RSRawSymbol, (RSRawSymbol, RSRawSymbol))
 -> ((RSRawSymbol, OpType), (RSRawSymbol, OpKind)))
-> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))]
-> [((RSRawSymbol, OpType), (RSRawSymbol, OpKind))]
forall a b. (a -> b) -> [a] -> [b]
map (\ (tab :: RSRawSymbol
tab, (c1 :: RSRawSymbol
c1, c2 :: RSRawSymbol
c2)) -> let
          t :: RSTable
t : _ = (RSTable -> Bool) -> [RSTable] -> [RSTable]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ tb :: RSTable
tb -> RSTable -> RSRawSymbol
SRel.t_name RSTable
tb RSRawSymbol -> RSRawSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== RSRawSymbol
tab) ([RSTable] -> [RSTable]) -> [RSTable] -> [RSTable]
forall a b. (a -> b) -> a -> b
$
              Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList (Set RSTable -> [RSTable]) -> Set RSTable -> [RSTable]
forall a b. (a -> b) -> a -> b
$ Sign -> Set RSTable
SRel.tables (Sign -> Set RSTable) -> Sign -> Set RSTable
forall a b. (a -> b) -> a -> b
$ RSMorphism -> Sign
SRel.domain RSMorphism
phi
          types :: [RSRawSymbol]
types = RSTable -> [RSRawSymbol]
getTypes RSTable
t
          resType :: RSRawSymbol
resType = String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSDatatype -> String
forall a. Show a => a -> String
show (RSDatatype -> String) -> RSDatatype -> String
forall a b. (a -> b) -> a -> b
$ RSColumn -> RSDatatype
SRel.c_data (RSColumn -> RSDatatype) -> RSColumn -> RSDatatype
forall a b. (a -> b) -> a -> b
$
                    [RSColumn] -> RSColumn
forall a. [a] -> a
head ([RSColumn] -> RSColumn) -> [RSColumn] -> RSColumn
forall a b. (a -> b) -> a -> b
$ (RSColumn -> Bool) -> [RSColumn] -> [RSColumn]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ col :: RSColumn
col -> RSColumn -> RSRawSymbol
SRel.c_name RSColumn
col RSRawSymbol -> RSRawSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== RSRawSymbol
c1) ([RSColumn] -> [RSColumn]) -> [RSColumn] -> [RSColumn]
forall a b. (a -> b) -> a -> b
$
                    RSTable -> [RSColumn]
SRel.columns RSTable
t
          fname :: RSRawSymbol
fname = String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSRawSymbol -> String
forall a. Show a => a -> String
show RSRawSymbol
tab String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: RSRawSymbol -> String
forall a. Show a => a -> String
show RSRawSymbol
c1
          ftype :: OpType
ftype = [RSRawSymbol] -> RSRawSymbol -> OpType
mkTotOpType [RSRawSymbol]
types RSRawSymbol
resType
          rname :: RSRawSymbol
rname = String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$
                  RSRawSymbol -> String
forall a. Show a => a -> String
show (RSMorphism -> Sort_map
SRel.table_map RSMorphism
phi Sort_map -> RSRawSymbol -> RSRawSymbol
forall k a. Ord k => Map k a -> k -> a
Map.! RSRawSymbol
tab) String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: RSRawSymbol -> String
forall a. Show a => a -> String
show RSRawSymbol
c2
                            in
            ((RSRawSymbol
fname, OpType
ftype), (RSRawSymbol
rname, OpKind
Partial))
                               )
     ([(RSRawSymbol, (RSRawSymbol, RSRawSymbol))]
 -> [((RSRawSymbol, OpType), (RSRawSymbol, OpKind))])
-> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))]
-> [((RSRawSymbol, OpType), (RSRawSymbol, OpKind))]
forall a b. (a -> b) -> a -> b
$ ((RSRawSymbol, RSTMap)
 -> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))])
-> [(RSRawSymbol, RSTMap)]
-> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (x :: RSRawSymbol
x, f :: RSTMap
f) -> ((RSRawSymbol, RSRawSymbol)
 -> (RSRawSymbol, (RSRawSymbol, RSRawSymbol)))
-> [(RSRawSymbol, RSRawSymbol)]
-> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))]
forall a b. (a -> b) -> [a] -> [b]
map (\ y :: (RSRawSymbol, RSRawSymbol)
y -> (RSRawSymbol
x, (RSRawSymbol, RSRawSymbol)
y)) ([(RSRawSymbol, RSRawSymbol)]
 -> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))])
-> [(RSRawSymbol, RSRawSymbol)]
-> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))]
forall a b. (a -> b) -> a -> b
$ Sort_map -> [(RSRawSymbol, RSRawSymbol)]
forall k a. Map k a -> [(k, a)]
Map.toList (Sort_map -> [(RSRawSymbol, RSRawSymbol)])
-> Sort_map -> [(RSRawSymbol, RSRawSymbol)]
forall a b. (a -> b) -> a -> b
$ RSTMap -> Sort_map
SRel.col_map RSTMap
f)
       ([(RSRawSymbol, RSTMap)]
 -> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))])
-> [(RSRawSymbol, RSTMap)]
-> [(RSRawSymbol, (RSRawSymbol, RSRawSymbol))]
forall a b. (a -> b) -> a -> b
$ Map RSRawSymbol RSTMap -> [(RSRawSymbol, RSTMap)]
forall k a. Map k a -> [(k, a)]
Map.toList (Map RSRawSymbol RSTMap -> [(RSRawSymbol, RSTMap)])
-> Map RSRawSymbol RSTMap -> [(RSRawSymbol, RSTMap)]
forall a b. (a -> b) -> a -> b
$ RSMorphism -> Map RSRawSymbol RSTMap
SRel.column_map RSMorphism
phi,
   pred_map :: Pred_map
pred_map = [((RSRawSymbol, PredType), RSRawSymbol)] -> Pred_map
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([((RSRawSymbol, PredType), RSRawSymbol)] -> Pred_map)
-> [((RSRawSymbol, PredType), RSRawSymbol)] -> Pred_map
forall a b. (a -> b) -> a -> b
$ ((RSRawSymbol, [PredType])
 -> [((RSRawSymbol, PredType), RSRawSymbol)])
-> [(RSRawSymbol, [PredType])]
-> [((RSRawSymbol, PredType), RSRawSymbol)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap
               (\ (i :: RSRawSymbol
i, pSet :: [PredType]
pSet) ->
                     [((RSRawSymbol
i, PredType
pt), RSMorphism -> Sort_map
SRel.table_map RSMorphism
phi Sort_map -> RSRawSymbol -> RSRawSymbol
forall k a. Ord k => Map k a -> k -> a
Map.! RSRawSymbol
i)
                             | PredType
pt <- [PredType]
pSet]) ([(RSRawSymbol, [PredType])]
 -> [((RSRawSymbol, PredType), RSRawSymbol)])
-> [(RSRawSymbol, [PredType])]
-> [((RSRawSymbol, PredType), RSRawSymbol)]
forall a b. (a -> b) -> a -> b
$
               PredMap -> [(RSRawSymbol, [PredType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (PredMap -> [(RSRawSymbol, [PredType])])
-> PredMap -> [(RSRawSymbol, [PredType])]
forall a b. (a -> b) -> a -> b
$ CASLSign -> PredMap
forall f e. Sign f e -> PredMap
predMap CASLSign
ssign,
   extended_map :: ()
extended_map = ()
}

genCASLSig :: [SRel.RSTable] -> Set.Set SORT -> OpMap -> PredMap
  -> (Set.Set SORT, OpMap, PredMap)
genCASLSig :: [RSTable]
-> Set RSRawSymbol
-> OpMap
-> PredMap
-> (Set RSRawSymbol, OpMap, PredMap)
genCASLSig tabList :: [RSTable]
tabList sorts :: Set RSRawSymbol
sorts ops :: OpMap
ops preds :: PredMap
preds = case [RSTable]
tabList of
  [] -> (Set RSRawSymbol
sorts, OpMap
ops, PredMap
preds)
  t :: RSTable
t : tList :: [RSTable]
tList -> let
   arity :: [RSRawSymbol]
arity = RSTable -> [RSRawSymbol]
getTypes RSTable
t
   sorts' :: Set RSRawSymbol
sorts' = [RSRawSymbol] -> Set RSRawSymbol
forall a. Ord a => [a] -> Set a
Set.fromList [RSRawSymbol]
arity
   ops' :: OpMap
ops' =
    [(RSRawSymbol, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList ([(RSRawSymbol, [OpType])] -> OpMap)
-> [(RSRawSymbol, [OpType])] -> OpMap
forall a b. (a -> b) -> a -> b
$
     (RSColumn -> (RSRawSymbol, [OpType]))
-> [RSColumn] -> [(RSRawSymbol, [OpType])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ c :: RSColumn
c -> (String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSRawSymbol -> String
forall a. Show a => a -> String
show (RSTable -> RSRawSymbol
SRel.t_name RSTable
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_'
                                Char -> ShowS
forall a. a -> [a] -> [a]
: RSRawSymbol -> String
forall a. Show a => a -> String
show (RSColumn -> RSRawSymbol
SRel.c_name RSColumn
c),
                  [OpKind -> [RSRawSymbol] -> RSRawSymbol -> OpType
OpType OpKind
Total [RSRawSymbol]
arity (RSRawSymbol -> OpType) -> RSRawSymbol -> OpType
forall a b. (a -> b) -> a -> b
$ String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSDatatype -> String
forall a. Show a => a -> String
show (RSDatatype -> String) -> RSDatatype -> String
forall a b. (a -> b) -> a -> b
$ RSColumn -> RSDatatype
SRel.c_data RSColumn
c]))
     ([RSColumn] -> [(RSRawSymbol, [OpType])])
-> [RSColumn] -> [(RSRawSymbol, [OpType])]
forall a b. (a -> b) -> a -> b
$ RSTable -> [RSColumn]
SRel.columns RSTable
t
   preds' :: PredMap
preds' = RSRawSymbol -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert (RSTable -> RSRawSymbol
SRel.t_name RSTable
t)
                       ([RSRawSymbol] -> PredType
PredType [RSRawSymbol]
arity) PredMap
preds
             in [RSTable]
-> Set RSRawSymbol
-> OpMap
-> PredMap
-> (Set RSRawSymbol, OpMap, PredMap)
genCASLSig [RSTable]
tList
                           (Set RSRawSymbol -> Set RSRawSymbol -> Set RSRawSymbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set RSRawSymbol
sorts Set RSRawSymbol
sorts')
                           (OpMap -> OpMap -> OpMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union OpMap
ops OpMap
ops')
                           PredMap
preds'

genAxioms :: SRel.RSTable -> Result [Named CASLFORMULA]
genAxioms :: RSTable -> Result [Named CASLFORMULA]
genAxioms tab :: RSTable
tab =
  if Set (RSRawSymbol, RSDatatype) -> Bool
forall a. Set a -> Bool
Set.null (Set (RSRawSymbol, RSDatatype) -> Bool)
-> Set (RSRawSymbol, RSDatatype) -> Bool
forall a b. (a -> b) -> a -> b
$ RSTable -> Set (RSRawSymbol, RSDatatype)
SRel.t_keys RSTable
tab then RSTable -> Result [Named CASLFORMULA]
projections RSTable
tab else do
          [Named CASLFORMULA]
axK <- RSTable -> Result [Named CASLFORMULA]
axiomsForKeys RSTable
tab
          [Named CASLFORMULA]
axP <- RSTable -> Result [Named CASLFORMULA]
projections RSTable
tab
          [Named CASLFORMULA] -> Result [Named CASLFORMULA]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named CASLFORMULA] -> Result [Named CASLFORMULA])
-> [Named CASLFORMULA] -> Result [Named CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [Named CASLFORMULA]
axK [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
axP

genTypedVars :: Char -> [Id] -> [(Token, Id)]
genTypedVars :: Char -> [RSRawSymbol] -> [(Token, RSRawSymbol)]
genTypedVars c :: Char
c = ((RSRawSymbol, Int) -> (Token, RSRawSymbol))
-> [(RSRawSymbol, Int)] -> [(Token, RSRawSymbol)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: RSRawSymbol
t, n :: Int
n) -> (String -> Token
genToken (Char
c Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
n), RSRawSymbol
t)) ([(RSRawSymbol, Int)] -> [(Token, RSRawSymbol)])
-> ([RSRawSymbol] -> [(RSRawSymbol, Int)])
-> [RSRawSymbol]
-> [(Token, RSRawSymbol)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RSRawSymbol] -> [(RSRawSymbol, Int)]
forall a. [a] -> [(a, Int)]
number

axiomsForKeys :: SRel.RSTable -> Result [Named CASLFORMULA]
axiomsForKeys :: RSTable -> Result [Named CASLFORMULA]
axiomsForKeys tab :: RSTable
tab = do
 let
  types :: [RSRawSymbol]
types = RSTable -> [RSRawSymbol]
getTypes RSTable
tab
  vars_x :: [(Token, RSRawSymbol)]
vars_x = Char -> [RSRawSymbol] -> [(Token, RSRawSymbol)]
genTypedVars 'x' [RSRawSymbol]
types
  vars_y :: [(Token, RSRawSymbol)]
vars_y = Char -> [RSRawSymbol] -> [(Token, RSRawSymbol)]
genTypedVars 'y' [RSRawSymbol]
types
  qual_vars :: [(Token, RSRawSymbol)] -> [TERM f]
qual_vars = ((Token, RSRawSymbol) -> TERM f)
-> [(Token, RSRawSymbol)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map ((Token -> RSRawSymbol -> TERM f) -> (Token, RSRawSymbol) -> TERM f
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> RSRawSymbol -> TERM f
forall f. Token -> RSRawSymbol -> TERM f
mkVarTerm)
  qXs :: [TERM f]
qXs = [(Token, RSRawSymbol)] -> [TERM f]
forall f. [(Token, RSRawSymbol)] -> [TERM f]
qual_vars [(Token, RSRawSymbol)]
vars_x
  qYs :: [TERM f]
qYs = [(Token, RSRawSymbol)] -> [TERM f]
forall f. [(Token, RSRawSymbol)] -> [TERM f]
qual_vars [(Token, RSRawSymbol)]
vars_y
  conjuncts :: [FORMULA f]
conjuncts = (TERM f -> TERM f -> FORMULA f)
-> [TERM f] -> [TERM f] -> [FORMULA f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq [TERM f]
forall f. [TERM f]
qXs [TERM f]
forall f. [TERM f]
qYs
  keys :: [(RSRawSymbol, RSDatatype)]
keys = Set (RSRawSymbol, RSDatatype) -> [(RSRawSymbol, RSDatatype)]
forall a. Set a -> [a]
Set.toList (Set (RSRawSymbol, RSDatatype) -> [(RSRawSymbol, RSDatatype)])
-> Set (RSRawSymbol, RSDatatype) -> [(RSRawSymbol, RSDatatype)]
forall a b. (a -> b) -> a -> b
$ RSTable -> Set (RSRawSymbol, RSDatatype)
SRel.t_keys RSTable
tab
  keysEqual :: [FORMULA f]
keysEqual = ((RSRawSymbol, RSDatatype) -> FORMULA f)
-> [(RSRawSymbol, RSDatatype)] -> [FORMULA f]
forall a b. (a -> b) -> [a] -> [b]
map (\ (cid :: RSRawSymbol
cid, ctype :: RSDatatype
ctype) -> let
                  qualOp :: OP_SYMB
qualOp = RSRawSymbol -> OP_TYPE -> OP_SYMB
mkQualOp
                     (String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSRawSymbol -> String
forall a. Show a => a -> String
show (RSTable -> RSRawSymbol
SRel.t_name RSTable
tab) String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: RSRawSymbol -> String
forall a. Show a => a -> String
show RSRawSymbol
cid)
                     (OpKind -> [RSRawSymbol] -> RSRawSymbol -> Range -> OP_TYPE
Op_type OpKind
Total [RSRawSymbol]
types (String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSDatatype -> String
forall a. Show a => a -> String
show RSDatatype
ctype) Range
nullRange)
                  in TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
                         (OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
qualOp [TERM f]
forall f. [TERM f]
qXs)
                         (OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
qualOp [TERM f]
forall f. [TERM f]
qYs)
                  ) [(RSRawSymbol, RSDatatype)]
keys
 [Named CASLFORMULA] -> Result [Named CASLFORMULA]
forall (m :: * -> *) a. Monad m => a -> m a
return [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "" (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall
            (((Token, RSRawSymbol) -> VAR_DECL)
-> [(Token, RSRawSymbol)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map ((Token -> RSRawSymbol -> VAR_DECL)
-> (Token, RSRawSymbol) -> VAR_DECL
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> RSRawSymbol -> VAR_DECL
mkVarDecl) ([(Token, RSRawSymbol)] -> [VAR_DECL])
-> [(Token, RSRawSymbol)] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ [(Token, RSRawSymbol)]
vars_x [(Token, RSRawSymbol)]
-> [(Token, RSRawSymbol)] -> [(Token, RSRawSymbol)]
forall a. [a] -> [a] -> [a]
++ [(Token, RSRawSymbol)]
vars_y)
            (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
              (let qualPred :: PRED_SYMB
qualPred = RSRawSymbol -> PRED_TYPE -> PRED_SYMB
mkQualPred
                     (RSTable -> RSRawSymbol
SRel.t_name RSTable
tab)
                     ([RSRawSymbol] -> Range -> PRED_TYPE
Pred_type [RSRawSymbol]
types Range
nullRange)
               in [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct
                ([ PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
qualPred [TERM ()]
forall f. [TERM f]
qXs
                 , PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication PRED_SYMB
qualPred [TERM ()]
forall f. [TERM f]
qYs ]
                 [CASLFORMULA] -> [CASLFORMULA] -> [CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [CASLFORMULA]
forall f. [FORMULA f]
keysEqual)
              )
              ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct [CASLFORMULA]
forall f. [FORMULA f]
conjuncts)
            )
          ]

getTypes :: SRel.RSTable -> [Id]
getTypes :: RSTable -> [RSRawSymbol]
getTypes = (RSColumn -> RSRawSymbol) -> [RSColumn] -> [RSRawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (String -> RSRawSymbol
stringToId (String -> RSRawSymbol)
-> (RSColumn -> String) -> RSColumn -> RSRawSymbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSDatatype -> String
forall a. Show a => a -> String
show (RSDatatype -> String)
-> (RSColumn -> RSDatatype) -> RSColumn -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSColumn -> RSDatatype
SRel.c_data) ([RSColumn] -> [RSRawSymbol])
-> (RSTable -> [RSColumn]) -> RSTable -> [RSRawSymbol]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSTable -> [RSColumn]
SRel.columns

projections :: SRel.RSTable -> Result [Named CASLFORMULA]
projections :: RSTable -> Result [Named CASLFORMULA]
projections tab :: RSTable
tab = let
  types :: [RSRawSymbol]
types = RSTable -> [RSRawSymbol]
getTypes RSTable
tab
  vars_x :: [(Token, RSRawSymbol)]
vars_x = Char -> [RSRawSymbol] -> [(Token, RSRawSymbol)]
genTypedVars 'x' [RSRawSymbol]
types
  vardecls :: [(Token, RSRawSymbol)] -> [VAR_DECL]
vardecls = ((Token, RSRawSymbol) -> VAR_DECL)
-> [(Token, RSRawSymbol)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map ((Token -> RSRawSymbol -> VAR_DECL)
-> (Token, RSRawSymbol) -> VAR_DECL
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> RSRawSymbol -> VAR_DECL
mkVarDecl)
  qual_vars :: [(Token, RSRawSymbol)] -> [TERM f]
qual_vars = ((Token, RSRawSymbol) -> TERM f)
-> [(Token, RSRawSymbol)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map ((Token -> RSRawSymbol -> TERM f) -> (Token, RSRawSymbol) -> TERM f
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> RSRawSymbol -> TERM f
forall f. Token -> RSRawSymbol -> TERM f
mkVarTerm)
  fields :: [String]
fields = (RSColumn -> String) -> [RSColumn] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map (RSRawSymbol -> String
forall a. Show a => a -> String
show (RSRawSymbol -> String)
-> (RSColumn -> RSRawSymbol) -> RSColumn -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RSColumn -> RSRawSymbol
SRel.c_name) ([RSColumn] -> [String]) -> [RSColumn] -> [String]
forall a b. (a -> b) -> a -> b
$ RSTable -> [RSColumn]
SRel.columns RSTable
tab
  projAx :: String -> (Token, RSRawSymbol) -> SenAttr (FORMULA f) String
projAx c :: String
c (vRes :: Token
vRes, typeRes :: RSRawSymbol
typeRes) = String -> FORMULA f -> SenAttr (FORMULA f) String
forall a s. a -> s -> SenAttr s a
makeNamed "" (FORMULA f -> SenAttr (FORMULA f) String)
-> FORMULA f -> SenAttr (FORMULA f) String
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall
             ([(Token, RSRawSymbol)] -> [VAR_DECL]
vardecls [(Token, RSRawSymbol)]
vars_x)
             (TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
               (OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl
                  (RSRawSymbol -> OP_TYPE -> OP_SYMB
mkQualOp
                     (String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSRawSymbol -> String
forall a. Show a => a -> String
show (RSTable -> RSRawSymbol
SRel.t_name RSTable
tab) String -> ShowS
forall a. [a] -> [a] -> [a]
++ '_' Char -> ShowS
forall a. a -> [a] -> [a]
: String
c)
                     (OpKind -> [RSRawSymbol] -> RSRawSymbol -> Range -> OP_TYPE
Op_type OpKind
Total [RSRawSymbol]
types RSRawSymbol
typeRes Range
nullRange)
                    )
                  ([(Token, RSRawSymbol)] -> [TERM f]
forall f. [(Token, RSRawSymbol)] -> [TERM f]
qual_vars [(Token, RSRawSymbol)]
vars_x)
                  )
                  (Token -> RSRawSymbol -> TERM f
forall f. Token -> RSRawSymbol -> TERM f
mkVarTerm Token
vRes RSRawSymbol
typeRes)
               )
  in [Named CASLFORMULA] -> Result [Named CASLFORMULA]
forall (m :: * -> *) a. Monad m => a -> m a
return ([Named CASLFORMULA] -> Result [Named CASLFORMULA])
-> [Named CASLFORMULA] -> Result [Named CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ (String -> (Token, RSRawSymbol) -> Named CASLFORMULA)
-> [String] -> [(Token, RSRawSymbol)] -> [Named CASLFORMULA]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith String -> (Token, RSRawSymbol) -> Named CASLFORMULA
forall f.
String -> (Token, RSRawSymbol) -> SenAttr (FORMULA f) String
projAx [String]
fields [(Token, RSRawSymbol)]
vars_x


mapNamedSen :: SRel.Sign -> Named Sentence -> Result (Named CASLFORMULA)
mapNamedSen :: Sign -> Named Sentence -> Result (Named CASLFORMULA)
mapNamedSen sign :: Sign
sign n_sens :: Named Sentence
n_sens =
    let
        s :: Sentence
s = Named Sentence -> Sentence
forall s a. SenAttr s a -> s
sentence Named Sentence
n_sens
    in
      do
        CASLFORMULA
ts <- Sign -> Sentence -> Result CASLFORMULA
mapSen Sign
sign Sentence
s
        Named CASLFORMULA -> Result (Named CASLFORMULA)
forall (m :: * -> *) a. Monad m => a -> m a
return (Named CASLFORMULA -> Result (Named CASLFORMULA))
-> Named CASLFORMULA -> Result (Named CASLFORMULA)
forall a b. (a -> b) -> a -> b
$ Named Sentence
n_sens {sentence :: CASLFORMULA
sentence = CASLFORMULA
ts}

mapSen :: SRel.Sign -> Sentence -> Result CASLFORMULA
mapSen :: Sign -> Sentence -> Result CASLFORMULA
mapSen sign :: Sign
sign sen :: Sentence
sen = let
  linkedcols :: [(RSRawSymbol, RSRawSymbol)]
linkedcols = [RSRawSymbol] -> [RSRawSymbol] -> [(RSRawSymbol, RSRawSymbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip ((RSQualId -> RSRawSymbol) -> [RSQualId] -> [RSRawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map RSQualId -> RSRawSymbol
column ([RSQualId] -> [RSRawSymbol]) -> [RSQualId] -> [RSRawSymbol]
forall a b. (a -> b) -> a -> b
$ Sentence -> [RSQualId]
r_lhs Sentence
sen)
                   ((RSQualId -> RSRawSymbol) -> [RSQualId] -> [RSRawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map RSQualId -> RSRawSymbol
column ([RSQualId] -> [RSRawSymbol]) -> [RSQualId] -> [RSRawSymbol]
forall a b. (a -> b) -> a -> b
$ Sentence -> [RSQualId]
r_rhs Sentence
sen)
  rtableName :: RSRawSymbol
rtableName : _ = (RSQualId -> RSRawSymbol) -> [RSQualId] -> [RSRawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map RSQualId -> RSRawSymbol
table ([RSQualId] -> [RSRawSymbol]) -> [RSQualId] -> [RSRawSymbol]
forall a b. (a -> b) -> a -> b
$ Sentence -> [RSQualId]
r_rhs Sentence
sen
  ltableName :: RSRawSymbol
ltableName : _ = (RSQualId -> RSRawSymbol) -> [RSQualId] -> [RSRawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map RSQualId -> RSRawSymbol
table ([RSQualId] -> [RSRawSymbol]) -> [RSQualId] -> [RSRawSymbol]
forall a b. (a -> b) -> a -> b
$ Sentence -> [RSQualId]
r_lhs Sentence
sen
  ltable :: RSTable
ltable : _ = (RSTable -> Bool) -> [RSTable] -> [RSTable]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ t :: RSTable
t -> RSTable -> RSRawSymbol
SRel.t_name RSTable
t RSRawSymbol -> RSRawSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== RSRawSymbol
ltableName) ([RSTable] -> [RSTable]) -> [RSTable] -> [RSTable]
forall a b. (a -> b) -> a -> b
$
           Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList (Set RSTable -> [RSTable]) -> Set RSTable -> [RSTable]
forall a b. (a -> b) -> a -> b
$ Sign -> Set RSTable
SRel.tables Sign
sign
  rtable :: RSTable
rtable : _ = (RSTable -> Bool) -> [RSTable] -> [RSTable]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ t :: RSTable
t -> RSTable -> RSRawSymbol
SRel.t_name RSTable
t RSRawSymbol -> RSRawSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== RSRawSymbol
rtableName) ([RSTable] -> [RSTable]) -> [RSTable] -> [RSTable]
forall a b. (a -> b) -> a -> b
$
           Set RSTable -> [RSTable]
forall a. Set a -> [a]
Set.toList (Set RSTable -> [RSTable]) -> Set RSTable -> [RSTable]
forall a b. (a -> b) -> a -> b
$ Sign -> Set RSTable
SRel.tables Sign
sign
  allRcols :: [(RSColumn, Int)]
allRcols = [RSColumn] -> [(RSColumn, Int)]
forall a. [a] -> [(a, Int)]
number ([RSColumn] -> [(RSColumn, Int)])
-> [RSColumn] -> [(RSColumn, Int)]
forall a b. (a -> b) -> a -> b
$ RSTable -> [RSColumn]
SRel.columns RSTable
rtable
  typesL :: [RSRawSymbol]
typesL = RSTable -> [RSRawSymbol]
getTypes RSTable
ltable
  typesR :: [RSRawSymbol]
typesR = RSTable -> [RSRawSymbol]
getTypes RSTable
rtable
  vars_x :: [(Token, RSRawSymbol)]
vars_x = Char -> [RSRawSymbol] -> [(Token, RSRawSymbol)]
genTypedVars 'x' [RSRawSymbol]
typesL
  vardecls :: [(Token, RSRawSymbol)] -> [VAR_DECL]
vardecls = ((Token, RSRawSymbol) -> VAR_DECL)
-> [(Token, RSRawSymbol)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map ((Token -> RSRawSymbol -> VAR_DECL)
-> (Token, RSRawSymbol) -> VAR_DECL
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> RSRawSymbol -> VAR_DECL
mkVarDecl)
  qual_vars :: [(Token, RSRawSymbol)] -> [TERM f]
qual_vars = ((Token, RSRawSymbol) -> TERM f)
-> [(Token, RSRawSymbol)] -> [TERM f]
forall a b. (a -> b) -> [a] -> [b]
map ((Token -> RSRawSymbol -> TERM f) -> (Token, RSRawSymbol) -> TERM f
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Token -> RSRawSymbol -> TERM f
forall f. Token -> RSRawSymbol -> TERM f
mkVarTerm)
  quantif :: QUANTIFIER
quantif = case Sentence -> RSRelType
r_type Sentence
sen of
             RSone_to_one -> QUANTIFIER
Unique_existential
             _ -> QUANTIFIER
Existential
  (decls :: [VAR_DECL]
decls, terms :: [TERM f]
terms) = (([VAR_DECL], [TERM f])
 -> (RSColumn, Int) -> ([VAR_DECL], [TERM f]))
-> ([VAR_DECL], [TERM f])
-> [(RSColumn, Int)]
-> ([VAR_DECL], [TERM f])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ (dList :: [VAR_DECL]
dList, tList :: [TERM f]
tList) (c :: RSColumn
c, i :: Int
i) ->
                    if RSColumn -> RSRawSymbol
SRel.c_name RSColumn
c RSRawSymbol -> [RSRawSymbol] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` ((RSRawSymbol, RSRawSymbol) -> RSRawSymbol)
-> [(RSRawSymbol, RSRawSymbol)] -> [RSRawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (RSRawSymbol, RSRawSymbol) -> RSRawSymbol
forall a b. (a, b) -> b
snd [(RSRawSymbol, RSRawSymbol)]
linkedcols then let
                       ti :: TERM f
ti = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl
                             (RSRawSymbol -> OP_TYPE -> OP_SYMB
mkQualOp
                               (String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$
                                 RSRawSymbol -> String
forall a. Show a => a -> String
show RSRawSymbol
ltableName String -> ShowS
forall a. [a] -> [a] -> [a]
++ "_" String -> ShowS
forall a. [a] -> [a] -> [a]
++
                                 RSRawSymbol -> String
forall a. Show a => a -> String
show ((RSRawSymbol, RSRawSymbol) -> RSRawSymbol
forall a b. (a, b) -> a
fst ((RSRawSymbol, RSRawSymbol) -> RSRawSymbol)
-> (RSRawSymbol, RSRawSymbol) -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ [(RSRawSymbol, RSRawSymbol)] -> (RSRawSymbol, RSRawSymbol)
forall a. [a] -> a
head ([(RSRawSymbol, RSRawSymbol)] -> (RSRawSymbol, RSRawSymbol))
-> [(RSRawSymbol, RSRawSymbol)] -> (RSRawSymbol, RSRawSymbol)
forall a b. (a -> b) -> a -> b
$
                                  ((RSRawSymbol, RSRawSymbol) -> Bool)
-> [(RSRawSymbol, RSRawSymbol)] -> [(RSRawSymbol, RSRawSymbol)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (_, y :: RSRawSymbol
y) -> RSRawSymbol
y RSRawSymbol -> RSRawSymbol -> Bool
forall a. Eq a => a -> a -> Bool
== RSColumn -> RSRawSymbol
SRel.c_name RSColumn
c)
                                  [(RSRawSymbol, RSRawSymbol)]
linkedcols))
                               (OpKind -> [RSRawSymbol] -> RSRawSymbol -> Range -> OP_TYPE
Op_type
                                 OpKind
Total
                                 [RSRawSymbol]
typesL
                                 (String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSDatatype -> String
forall a. Show a => a -> String
show (RSDatatype -> String) -> RSDatatype -> String
forall a b. (a -> b) -> a -> b
$ RSColumn -> RSDatatype
SRel.c_data RSColumn
c)
                                  Range
nullRange)
                                )
                             ([(Token, RSRawSymbol)] -> [TERM f]
forall f. [(Token, RSRawSymbol)] -> [TERM f]
qual_vars [(Token, RSRawSymbol)]
vars_x)
                             in ([VAR_DECL]
dList, TERM f
forall f. TERM f
ti TERM f -> [TERM f] -> [TERM f]
forall a. a -> [a] -> [a]
: [TERM f]
tList)
                     else let
                       di :: VAR_DECL
di = Token -> RSRawSymbol -> VAR_DECL
mkVarDecl
                             (String -> Token
genToken (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ 'y' Char -> ShowS
forall a. a -> [a] -> [a]
: Int -> String
forall a. Show a => a -> String
show Int
i)
                             (String -> RSRawSymbol
stringToId (String -> RSRawSymbol) -> String -> RSRawSymbol
forall a b. (a -> b) -> a -> b
$ RSDatatype -> String
forall a. Show a => a -> String
show (RSDatatype -> String) -> RSDatatype -> String
forall a b. (a -> b) -> a -> b
$ RSColumn -> RSDatatype
SRel.c_data RSColumn
c)
                       ti :: TERM f
ti = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
di
                             in (VAR_DECL
di VAR_DECL -> [VAR_DECL] -> [VAR_DECL]
forall a. a -> [a] -> [a]
: [VAR_DECL]
dList, TERM f
forall f. TERM f
ti TERM f -> [TERM f] -> [TERM f]
forall a. a -> [a] -> [a]
: [TERM f]
tList)
                           ) ([], []) [(RSColumn, Int)]
allRcols

  in CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall ([(Token, RSRawSymbol)] -> [VAR_DECL]
vardecls [(Token, RSRawSymbol)]
vars_x) (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkImpl
                    (PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication
                       (RSRawSymbol -> PRED_TYPE -> PRED_SYMB
mkQualPred RSRawSymbol
ltableName
                          ([RSRawSymbol] -> Range -> PRED_TYPE
Pred_type [RSRawSymbol]
typesL Range
nullRange)
                          ) ([(Token, RSRawSymbol)] -> [TERM ()]
forall f. [(Token, RSRawSymbol)] -> [TERM f]
qual_vars [(Token, RSRawSymbol)]
vars_x)
                       )

                    (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
quantif ([VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a]
reverse [VAR_DECL]
decls)
                       (PRED_SYMB -> [TERM ()] -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> FORMULA f
mkPredication
                          (RSRawSymbol -> PRED_TYPE -> PRED_SYMB
mkQualPred RSRawSymbol
rtableName
                             ([RSRawSymbol] -> Range -> PRED_TYPE
Pred_type [RSRawSymbol]
typesR Range
nullRange)
                          )
                          ([TERM ()] -> [TERM ()]
forall a. [a] -> [a]
reverse [TERM ()]
forall f. [TERM f]
terms)
                       ) Range
nullRange