{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/CASL2VSEImport.hs
Description :  embedding from CASL to VSE, plus wrapping procedures
               with default implementations
Copyright   :  (c) M.Codescu, DFKI Bremen 2008
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Mihai.Codescu@dfki.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

The embedding comorphism from CASL to VSE.
-}

module Comorphisms.CASL2VSEImport (CASL2VSEImport (..)) where

import Logic.Logic
import Logic.Comorphism

import CASL.Logic_CASL
import CASL.Sublogic as SL
import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Morphism

import VSE.Logic_VSE
import VSE.As
import VSE.Ana

import Common.AS_Annotation
import Common.Id
import Common.ProofTree
import Common.Result
import qualified Common.Lib.MapSet as MapSet
import qualified Control.Monad.Fail as Fail

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

-- | The identity of the comorphism
data CASL2VSEImport = CASL2VSEImport deriving (Int -> CASL2VSEImport -> ShowS
[CASL2VSEImport] -> ShowS
CASL2VSEImport -> String
(Int -> CASL2VSEImport -> ShowS)
-> (CASL2VSEImport -> String)
-> ([CASL2VSEImport] -> ShowS)
-> Show CASL2VSEImport
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2VSEImport] -> ShowS
$cshowList :: [CASL2VSEImport] -> ShowS
show :: CASL2VSEImport -> String
$cshow :: CASL2VSEImport -> String
showsPrec :: Int -> CASL2VSEImport -> ShowS
$cshowsPrec :: Int -> CASL2VSEImport -> ShowS
Show)

instance Language CASL2VSEImport -- default definition is okay

instance Comorphism CASL2VSEImport
               CASL CASL_Sublogics
               CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
               CASLSign
               CASLMor
               Symbol RawSymbol ProofTree
               VSE ()
               VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS
               VSESign
               VSEMor
               Symbol RawSymbol () where
    sourceLogic :: CASL2VSEImport -> CASL
sourceLogic CASL2VSEImport = CASL
CASL
    sourceSublogic :: CASL2VSEImport -> CASL_Sublogics
sourceSublogic CASL2VSEImport = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.cFol
    targetLogic :: CASL2VSEImport -> VSE
targetLogic CASL2VSEImport = VSE
VSE
    mapSublogic :: CASL2VSEImport -> CASL_Sublogics -> Maybe ()
mapSublogic CASL2VSEImport _ = () -> Maybe ()
forall a. a -> Maybe a
Just ()
    map_theory :: CASL2VSEImport
-> (CASLSign, [Named CASLFORMULA])
-> Result (VSESign, [Named Sentence])
map_theory CASL2VSEImport = (CASLSign, [Named CASLFORMULA])
-> Result (VSESign, [Named Sentence])
mapCASLTheory
    map_morphism :: CASL2VSEImport -> CASLMor -> Result VSEMor
map_morphism CASL2VSEImport = VSEMor -> Result VSEMor
forall (m :: * -> *) a. Monad m => a -> m a
return (VSEMor -> Result VSEMor)
-> (CASLMor -> VSEMor) -> CASLMor -> Result VSEMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLMor -> VSEMor
mapMor
    map_sentence :: CASL2VSEImport -> CASLSign -> CASLFORMULA -> Result Sentence
map_sentence CASL2VSEImport _ = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (CASLFORMULA -> Sentence) -> CASLFORMULA -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. CASLFORMULA -> Sentence
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA
    map_symbol :: CASL2VSEImport -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2VSEImport = String -> CASLSign -> Symbol -> Set Symbol
forall a. HasCallStack => String -> a
error "nyi"
      -- check these 3, but should be fine
    has_model_expansion :: CASL2VSEImport -> Bool
has_model_expansion CASL2VSEImport = Bool
True
    is_weakly_amalgamable :: CASL2VSEImport -> Bool
is_weakly_amalgamable CASL2VSEImport = Bool
True
    isInclusionComorphism :: CASL2VSEImport -> Bool
isInclusionComorphism CASL2VSEImport = Bool
True


mapCASLTheory :: (CASLSign, [Named CASLFORMULA]) ->
                 Result (VSESign, [Named Sentence])
mapCASLTheory :: (CASLSign, [Named CASLFORMULA])
-> Result (VSESign, [Named Sentence])
mapCASLTheory (sig :: CASLSign
sig, n_sens :: [Named CASLFORMULA]
n_sens) =
  let (tsig :: VSESign
tsig, genAx :: [Named Sentence]
genAx) = CASLSign -> (VSESign, [Named Sentence])
mapSig CASLSign
sig
      tsens :: [SenAttr (FORMULA f) String]
tsens = (Named CASLFORMULA -> SenAttr (FORMULA f) String)
-> [Named CASLFORMULA] -> [SenAttr (FORMULA f) String]
forall a b. (a -> b) -> [a] -> [b]
map ((CASLFORMULA -> FORMULA f)
-> Named CASLFORMULA -> SenAttr (FORMULA f) String
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed CASLFORMULA -> FORMULA f
forall f1 f. FORMULA f1 -> FORMULA f
mapFORMULA) [Named CASLFORMULA]
n_sens
  in if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null ([Diagnosis] -> Bool) -> [Diagnosis] -> Bool
forall a b. (a -> b) -> a -> b
$ VSESign -> [Named Sentence] -> [Diagnosis]
forall f e. Sign f e -> [Named Sentence] -> [Diagnosis]
checkCases VSESign
tsig ([Named Sentence]
forall f. [SenAttr (FORMULA f) String]
tsens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
genAx)
     then String -> Result (VSESign, [Named Sentence])
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail "case error in signature"
     else (VSESign, [Named Sentence]) -> Result (VSESign, [Named Sentence])
forall (m :: * -> *) a. Monad m => a -> m a
return (VSESign
tsig, [Named Sentence]
forall f. [SenAttr (FORMULA f) String]
tsens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
genAx)

mkIfProg :: FORMULA () -> Program
mkIfProg :: CASLFORMULA -> Program
mkIfProg f :: CASLFORMULA
f =
  PlainProgram -> Program
forall a. a -> Ranged a
mkRanged (PlainProgram -> Program) -> PlainProgram -> Program
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Program -> Program -> PlainProgram
If CASLFORMULA
f (PlainProgram -> Program
forall a. a -> Ranged a
mkRanged (PlainProgram -> Program) -> PlainProgram -> Program
forall a b. (a -> b) -> a -> b
$ TERM () -> PlainProgram
Return TERM ()
forall f. TERM f
aTrue) (Program -> PlainProgram) -> Program -> PlainProgram
forall a b. (a -> b) -> a -> b
$ PlainProgram -> Program
forall a. a -> Ranged a
mkRanged (PlainProgram -> Program) -> PlainProgram -> Program
forall a b. (a -> b) -> a -> b
$ TERM () -> PlainProgram
Return TERM ()
forall f. TERM f
aFalse

mapSig :: CASLSign -> (VSESign, [Named Sentence])
mapSig :: CASLSign -> (VSESign, [Named Sentence])
mapSig sign :: CASLSign
sign =
 let wrapSort :: ([(Id, Profile)], [Named Sentence])
-> Id -> ([(Id, Profile)], [Named Sentence])
wrapSort (procsym :: [(Id, Profile)]
procsym, axs :: [Named Sentence]
axs) s :: Id
s = let
        restrName :: Id
restrName = Id -> Id
gnRestrName Id
s
        eqName :: Id
eqName = Id -> Id
gnEqName Id
s
        sProcs :: [(Id, Profile)]
sProcs = [(Id
restrName, [Procparam] -> Maybe Id -> Profile
Profile [Paramkind -> Id -> Procparam
Procparam Paramkind
In Id
s] Maybe Id
forall a. Maybe a
Nothing),
                  (Id
eqName,
                     [Procparam] -> Maybe Id -> Profile
Profile [Paramkind -> Id -> Procparam
Procparam Paramkind
In Id
s, Paramkind -> Id -> Procparam
Procparam Paramkind
In Id
s]
                             (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
uBoolean))]
        sSens :: [Named Sentence]
sSens = [String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_restriction_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s) (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$
                 VSEforms -> Ranged VSEforms
forall a. a -> Ranged a
mkRanged
                  ([Defproc] -> VSEforms
Defprocs
                   [ProcKind -> Id -> [VAR] -> Program -> Range -> Defproc
Defproc ProcKind
Proc Id
restrName [VAR
xVar]
                   (PlainProgram -> Program
forall a. a -> Ranged a
mkRanged ([VAR_DECL] -> Program -> PlainProgram
Block [] (PlainProgram -> Program
forall a. a -> Ranged a
mkRanged PlainProgram
Skip)))
                           Range
nullRange])
                , String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed ("ga_equality_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
s) (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$
                 VSEforms -> Ranged VSEforms
forall a. a -> Ranged a
mkRanged
                  ([Defproc] -> VSEforms
Defprocs
                   [ProcKind -> Id -> [VAR] -> Program -> Range -> Defproc
Defproc ProcKind
Func Id
eqName ((String -> VAR) -> [String] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map String -> VAR
mkSimpleId ["x", "y"])
                   (PlainProgram -> Program
forall a. a -> Ranged a
mkRanged ([VAR_DECL] -> Program -> PlainProgram
Block [] (CASLFORMULA -> Program
mkIfProg (TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
                        (VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
mkSimpleId "x") Id
s Range
nullRange)
                        (VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var (String -> VAR
mkSimpleId "y") Id
s Range
nullRange)
                        ))))
                           Range
nullRange])
                ]
                                          in
        ([(Id, Profile)]
sProcs [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
procsym, [Named Sentence]
sSens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
axs)
     (sortProcs :: [(Id, Profile)]
sortProcs, sortSens :: [Named Sentence]
sortSens) = (([(Id, Profile)], [Named Sentence])
 -> Id -> ([(Id, Profile)], [Named Sentence]))
-> ([(Id, Profile)], [Named Sentence])
-> [Id]
-> ([(Id, Profile)], [Named Sentence])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([(Id, Profile)], [Named Sentence])
-> Id -> ([(Id, Profile)], [Named Sentence])
wrapSort ([], []) ([Id] -> ([(Id, Profile)], [Named Sentence]))
-> [Id] -> ([(Id, Profile)], [Named Sentence])
forall a b. (a -> b) -> a -> b
$
                                        Set Id -> [Id]
forall a. Set a -> [a]
Set.toList (Set Id -> [Id]) -> Set Id -> [Id]
forall a b. (a -> b) -> a -> b
$ CASLSign -> Set Id
forall f e. Sign f e -> Set Id
sortSet CASLSign
sign
     wrapOp :: ([(Id, Profile)], [Named Sentence])
-> (Id, [OpType]) -> ([(Id, Profile)], [Named Sentence])
wrapOp (procsym :: [(Id, Profile)]
procsym, axs :: [Named Sentence]
axs) (i :: Id
i, opTypes :: [OpType]
opTypes) = let
       funName :: Id
funName = Id -> Id
mkGenName Id
i
       fProcs :: [(Id, Profile)]
fProcs = (OpType -> (Id, Profile)) -> [OpType] -> [(Id, Profile)]
forall a b. (a -> b) -> [a] -> [b]
map (\ profile :: OpType
profile ->
                       (Id
funName,
                        [Procparam] -> Maybe Id -> Profile
Profile
                           ((Id -> Procparam) -> [Id] -> [Procparam]
forall a b. (a -> b) -> [a] -> [b]
map (Paramkind -> Id -> Procparam
Procparam Paramkind
In) ([Id] -> [Procparam]) -> [Id] -> [Procparam]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
profile)
                           (Id -> Maybe Id
forall a. a -> Maybe a
Just (Id -> Maybe Id) -> Id -> Maybe Id
forall a b. (a -> b) -> a -> b
$ OpType -> Id
opRes OpType
profile))) [OpType]
opTypes
       fSens :: [Named Sentence]
fSens = (OpType -> Named Sentence) -> [OpType] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ (OpType fKind :: OpKind
fKind w :: [Id]
w s :: Id
s) -> let vars :: [(VAR, Id)]
vars = [Id] -> [(VAR, Id)]
genVars [Id]
w in
                   String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Range -> Ranged VSEforms
forall a. a -> Range -> Ranged a
Ranged
                     ([Defproc] -> VSEforms
Defprocs
                       [ProcKind -> Id -> [VAR] -> Program -> Range -> Defproc
Defproc
                         ProcKind
Func Id
funName (((VAR, Id) -> VAR) -> [(VAR, Id)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, Id) -> VAR
forall a b. (a, b) -> a
fst [(VAR, Id)]
vars)
                         ( PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged ([VAR_DECL] -> Program -> PlainProgram
Block []
                         (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                            ([VAR_DECL] -> Program -> PlainProgram
Block
                              [[VAR] -> Id -> Range -> VAR_DECL
Var_decl [VAR
yVar] Id
s Range
nullRange]
                              (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                (Program -> Program -> PlainProgram
Seq
                                 (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                   (VAR -> TERM () -> PlainProgram
Assign
                                     VAR
yVar
                                     (OP_SYMB -> [TERM ()] -> Range -> TERM ()
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application
                                      (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
i
                                        (OpKind -> [Id] -> Id -> Range -> OP_TYPE
Op_type OpKind
fKind [Id]
w Id
s Range
nullRange)
                                       Range
nullRange )
                                      (((VAR, Id) -> TERM ()) -> [(VAR, Id)] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map (\ (v :: VAR
v, ss :: Id
ss) ->
                                              VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var VAR
v Id
ss Range
nullRange) [(VAR, Id)]
vars)
                                      Range
nullRange))
                                   Range
nullRange)

                                 (PlainProgram -> Range -> Program
forall a. a -> Range -> Ranged a
Ranged
                                   (TERM () -> PlainProgram
Return
                                    (VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var VAR
yVar Id
s Range
nullRange))
                                   Range
nullRange)

                                ) -- end seq
                               Range
nullRange)
                              ) -- end block
                            Range
nullRange) -- end procedure body
                            ) Range
nullRange)
                         Range
nullRange]
                     )
                     Range
nullRange
                   ) [OpType]
opTypes
                                            in
       ([(Id, Profile)]
procsym [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
fProcs, [Named Sentence]
axs [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
fSens)
     (opProcs :: [(Id, Profile)]
opProcs, opSens :: [Named Sentence]
opSens) = (([(Id, Profile)], [Named Sentence])
 -> (Id, [OpType]) -> ([(Id, Profile)], [Named Sentence]))
-> ([(Id, Profile)], [Named Sentence])
-> [(Id, [OpType])]
-> ([(Id, Profile)], [Named Sentence])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([(Id, Profile)], [Named Sentence])
-> (Id, [OpType]) -> ([(Id, Profile)], [Named Sentence])
wrapOp ([], []) ([(Id, [OpType])] -> ([(Id, Profile)], [Named Sentence]))
-> [(Id, [OpType])] -> ([(Id, Profile)], [Named Sentence])
forall a b. (a -> b) -> a -> b
$
                                        MapSet Id OpType -> [(Id, [OpType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (MapSet Id OpType -> [(Id, [OpType])])
-> MapSet Id OpType -> [(Id, [OpType])]
forall a b. (a -> b) -> a -> b
$ CASLSign -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap CASLSign
sign
     wrapPred :: ([(Id, Profile)], [Named Sentence])
-> (Id, [PredType]) -> ([(Id, Profile)], [Named Sentence])
wrapPred (procsym :: [(Id, Profile)]
procsym, axs :: [Named Sentence]
axs) (i :: Id
i, predTypes :: [PredType]
predTypes) = let
       procName :: Id
procName = Id -> Id
mkGenName Id
i
       pProcs :: [(Id, Profile)]
pProcs = (PredType -> (Id, Profile)) -> [PredType] -> [(Id, Profile)]
forall a b. (a -> b) -> [a] -> [b]
map (\ profile :: PredType
profile -> (Id
procName,
                        [Procparam] -> Maybe Id -> Profile
Profile
                           ((Id -> Procparam) -> [Id] -> [Procparam]
forall a b. (a -> b) -> [a] -> [b]
map (Paramkind -> Id -> Procparam
Procparam Paramkind
In) ([Id] -> [Procparam]) -> [Id] -> [Procparam]
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
profile)
                           (Id -> Maybe Id
forall a. a -> Maybe a
Just Id
uBoolean))) [PredType]
predTypes
       pSens :: [Named Sentence]
pSens = (PredType -> Named Sentence) -> [PredType] -> [Named Sentence]
forall a b. (a -> b) -> [a] -> [b]
map (\ (PredType w :: [Id]
w) -> let vars :: [(VAR, Id)]
vars = [Id] -> [(VAR, Id)]
genVars [Id]
w in
                   String -> Sentence -> Named Sentence
forall a s. a -> s -> SenAttr s a
makeNamed "" (Sentence -> Named Sentence) -> Sentence -> Named Sentence
forall a b. (a -> b) -> a -> b
$ Ranged VSEforms -> Sentence
forall f. f -> FORMULA f
ExtFORMULA (Ranged VSEforms -> Sentence) -> Ranged VSEforms -> Sentence
forall a b. (a -> b) -> a -> b
$ VSEforms -> Ranged VSEforms
forall a. a -> Ranged a
mkRanged
                     ([Defproc] -> VSEforms
Defprocs
                       [ProcKind -> Id -> [VAR] -> Program -> Range -> Defproc
Defproc
                         ProcKind
Func Id
procName (((VAR, Id) -> VAR) -> [(VAR, Id)] -> [VAR]
forall a b. (a -> b) -> [a] -> [b]
map (VAR, Id) -> VAR
forall a b. (a, b) -> a
fst [(VAR, Id)]
vars)
                         (PlainProgram -> Program
forall a. a -> Ranged a
mkRanged ([VAR_DECL] -> Program -> PlainProgram
Block [] (CASLFORMULA -> Program
mkIfProg
                               (PRED_SYMB -> [TERM ()] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
                                        (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name
                                          Id
i
                                         ([Id] -> Range -> PRED_TYPE
Pred_type [Id]
w Range
nullRange)
                                        Range
nullRange)
                                        (((VAR, Id) -> TERM ()) -> [(VAR, Id)] -> [TERM ()]
forall a b. (a -> b) -> [a] -> [b]
map (\ (v :: VAR
v, ss :: Id
ss) ->
                                               VAR -> Id -> Range -> TERM ()
forall f. VAR -> Id -> Range -> TERM f
Qual_var VAR
v Id
ss Range
nullRange) [(VAR, Id)]
vars)
                                       Range
nullRange))))
                          Range
nullRange]
                     )
                   ) [PredType]
predTypes
                                                in
      ([(Id, Profile)]
procsym [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
pProcs, [Named Sentence]
axs [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
pSens)
     (predProcs :: [(Id, Profile)]
predProcs, predSens :: [Named Sentence]
predSens) = (([(Id, Profile)], [Named Sentence])
 -> (Id, [PredType]) -> ([(Id, Profile)], [Named Sentence]))
-> ([(Id, Profile)], [Named Sentence])
-> [(Id, [PredType])]
-> ([(Id, Profile)], [Named Sentence])
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ([(Id, Profile)], [Named Sentence])
-> (Id, [PredType]) -> ([(Id, Profile)], [Named Sentence])
wrapPred ([], []) ([(Id, [PredType])] -> ([(Id, Profile)], [Named Sentence]))
-> [(Id, [PredType])] -> ([(Id, Profile)], [Named Sentence])
forall a b. (a -> b) -> a -> b
$
                                        MapSet Id PredType -> [(Id, [PredType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (MapSet Id PredType -> [(Id, [PredType])])
-> MapSet Id PredType -> [(Id, [PredType])]
forall a b. (a -> b) -> a -> b
$ CASLSign -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap CASLSign
sign
     procs :: Procs
procs = Map Id Profile -> Procs
Procs (Map Id Profile -> Procs) -> Map Id Profile -> Procs
forall a b. (a -> b) -> a -> b
$ [(Id, Profile)] -> Map Id Profile
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Id, Profile)]
sortProcs [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
opProcs [(Id, Profile)] -> [(Id, Profile)] -> [(Id, Profile)]
forall a. [a] -> [a] -> [a]
++ [(Id, Profile)]
predProcs)
     newPreds :: MapSet Id PredType
newPreds = Procs -> MapSet Id PredType
procsToPredMap Procs
procs
     newOps :: MapSet Id OpType
newOps = Procs -> MapSet Id OpType
procsToOpMap Procs
procs
 in (CASLSign
sign { opMap :: MapSet Id OpType
opMap = MapSet Id OpType -> MapSet Id OpType -> MapSet Id OpType
addOpMapSet (CASLSign -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap CASLSign
sign) MapSet Id OpType
newOps,
           predMap :: MapSet Id PredType
predMap = MapSet Id PredType -> MapSet Id PredType -> MapSet Id PredType
addMapSet (CASLSign -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap CASLSign
sign) MapSet Id PredType
newPreds,
           extendedInfo :: Procs
extendedInfo = Procs
procs,
           sentences :: [Named Sentence]
sentences = [] }, [Named Sentence]
sortSens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
opSens [Named Sentence] -> [Named Sentence] -> [Named Sentence]
forall a. [a] -> [a] -> [a]
++ [Named Sentence]
predSens)

mapMor :: CASLMor -> VSEMor
mapMor :: CASLMor -> VSEMor
mapMor m :: CASLMor
m = let
  (om :: Op_map
om, pm :: Pred_map
pm) = CASLMor -> (Op_map, Pred_map)
vseMorExt CASLMor
m
  in CASLMor
m
  { msource :: VSESign
msource = (VSESign, [Named Sentence]) -> VSESign
forall a b. (a, b) -> a
fst ((VSESign, [Named Sentence]) -> VSESign)
-> (VSESign, [Named Sentence]) -> VSESign
forall a b. (a -> b) -> a -> b
$ CASLSign -> (VSESign, [Named Sentence])
mapSig (CASLSign -> (VSESign, [Named Sentence]))
-> CASLSign -> (VSESign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
msource CASLMor
m
  , mtarget :: VSESign
mtarget = (VSESign, [Named Sentence]) -> VSESign
forall a b. (a, b) -> a
fst ((VSESign, [Named Sentence]) -> VSESign)
-> (VSESign, [Named Sentence]) -> VSESign
forall a b. (a -> b) -> a -> b
$ CASLSign -> (VSESign, [Named Sentence])
mapSig (CASLSign -> (VSESign, [Named Sentence]))
-> CASLSign -> (VSESign, [Named Sentence])
forall a b. (a -> b) -> a -> b
$ CASLMor -> CASLSign
forall f e m. Morphism f e m -> Sign f e
mtarget CASLMor
m
  , op_map :: Op_map
op_map = Op_map -> Op_map -> Op_map
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Op_map
om (Op_map -> Op_map) -> Op_map -> Op_map
forall a b. (a -> b) -> a -> b
$ CASLMor -> Op_map
forall f e m. Morphism f e m -> Op_map
op_map CASLMor
m
  , pred_map :: Pred_map
pred_map = Pred_map -> Pred_map -> Pred_map
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Pred_map
pm (Pred_map -> Pred_map) -> Pred_map -> Pred_map
forall a b. (a -> b) -> a -> b
$ CASLMor -> Pred_map
forall f e m. Morphism f e m -> Pred_map
pred_map CASLMor
m
  , extended_map :: VSEMorExt
extended_map = VSEMorExt
forall e. DefMorExt e
emptyMorExt
  }