{- |
Module      :  ./DFOL/Comorphism.hs
Description :  Helper functions for the DFOL -> CASL translation
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module DFOL.Comorphism where

import Common.Id
import Common.AS_Annotation
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

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

import DFOL.Sign
import DFOL.AS_DFOL
import DFOL.Morphism
import DFOL.Symbol

import qualified CASL.Sign as CASL_Sign
import qualified CASL.AS_Basic_CASL as CASL_AS
import qualified CASL.Morphism as CASL_Morphism

-- shorthand notation
nr :: Range
nr :: Range
nr = Range
nullRange

-- the unique sort
sort :: CASL_AS.SORT
sort :: SORT
sort = [Token] -> SORT
mkId [String -> Range -> Token
Token "Sort" Range
nr]

-- the special bot symbol
botTok :: Token
botTok :: Token
botTok = String -> Range -> Token
Token "Bot" Range
nr

bot :: CASL_AS.CASLTERM
bot :: CASLTERM
bot = OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CASL_AS.Application (SORT -> OP_TYPE -> Range -> OP_SYMB
CASL_AS.Qual_op_name ([Token] -> SORT
mkId [Token
botTok])
                          (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
CASL_AS.Op_type OpKind
CASL_AS.Total [] SORT
sort Range
nr) Range
nr) [] Range
nr

-- constructing a FOL type of the specified arity
folType :: Int -> [CASL_AS.SORT]
folType :: Int -> [SORT]
folType n :: Int
n = Int -> SORT -> [SORT]
forall a. Int -> a -> [a]
replicate Int
n SORT
sort

-- signature map
sigMap :: Sign -> CASL_Sign.CASLSign
sigMap :: Sign -> CASLSign
sigMap sig :: Sign
sig =
  (Token -> CASLSign -> CASLSign) -> CASLSign -> [Token] -> CASLSign
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Sign -> Token -> CASLSign -> CASLSign
sigMapH Sign
sig) CASLSign
forall f. Sign f ()
caslSig2 [Token]
symbols
  where caslSig2 :: Sign f ()
caslSig2 = (() -> Sign f ()
forall e f. e -> Sign f e
CASL_Sign.emptySign ())
          { sortRel :: Rel SORT
CASL_Sign.sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
sort Rel SORT
forall a. Rel a
Rel.empty
          , opMap :: OpMap
CASL_Sign.opMap = SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert ([Token] -> SORT
mkId [Token
botTok])
              (SORT -> OpType
CASL_Sign.sortToOpType SORT
sort) OpMap
forall a b. MapSet a b
MapSet.empty }
        symbols :: [Token]
symbols = Set Token -> [Token]
forall a. Set a -> [a]
Set.toList (Set Token -> [Token]) -> Set Token -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> Set Token
getSymbols Sign
sig

sigMapH :: Sign -> NAME -> CASL_Sign.CASLSign -> CASL_Sign.CASLSign
sigMapH :: Sign -> Token -> CASLSign -> CASLSign
sigMapH sig :: Sign
sig sym :: Token
sym csig :: CASLSign
csig = case KIND
kind of
       SortKind -> CASLSign
csig
         { predMap :: PredMap
CASL_Sign.predMap = PredType -> PredMap -> PredMap
insSym (Int -> PredType
predTy (Int -> PredType) -> Int -> PredType
forall a b. (a -> b) -> a -> b
$ Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1) PredMap
predis }
       PredKind -> CASLSign
csig { predMap :: PredMap
CASL_Sign.predMap = PredType -> PredMap -> PredMap
insSym (Int -> PredType
predTy Int
arity) PredMap
predis }
       FuncKind -> CASLSign
csig
         { opMap :: OpMap
CASL_Sign.opMap = SORT -> OpType -> OpMap -> OpMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert ([Token] -> SORT
mkId [Token
sym])
             ([SORT] -> SORT -> OpType
CASL_Sign.mkTotOpType (Int -> [SORT]
folType Int
arity) SORT
sort)
             (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ CASLSign -> OpMap
forall f e. Sign f e -> OpMap
CASL_Sign.opMap CASLSign
csig }
  where predis :: PredMap
predis = CASLSign -> PredMap
forall f e. Sign f e -> PredMap
CASL_Sign.predMap CASLSign
csig
        insSym :: PredType -> PredMap -> PredMap
insSym = SORT -> PredType -> PredMap -> PredMap
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert ([Token] -> SORT
mkId [Token
sym])
        predTy :: Int -> PredType
predTy = [SORT] -> PredType
CASL_Sign.PredType ([SORT] -> PredType) -> (Int -> [SORT]) -> Int -> PredType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [SORT]
folType
        Just kind :: KIND
kind = Token -> Sign -> Maybe KIND
getSymbolKind Token
sym Sign
sig
        Just arity :: Int
arity = Token -> Sign -> Maybe Int
getSymbolArity Token
sym Sign
sig

-- generating axioms for a translated signature
generateAxioms :: Sign -> [Named CASL_AS.CASLFORMULA]
generateAxioms :: Sign -> [Named CASLFORMULA]
generateAxioms sig :: Sign
sig = [Named CASLFORMULA]
predAx [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
funcAx [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
sortAx
                     where sorts :: [Token]
sorts = Set Token -> [Token]
forall a. Set a -> [a]
Set.toList (Set Token -> [Token]) -> Set Token -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> KIND -> Set Token
getSymbolsByKind Sign
sig KIND
SortKind
                           funcs :: [Token]
funcs = Set Token -> [Token]
forall a. Set a -> [a]
Set.toList (Set Token -> [Token]) -> Set Token -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> KIND -> Set Token
getSymbolsByKind Sign
sig KIND
FuncKind
                           preds :: [Token]
preds = Set Token -> [Token]
forall a. Set a -> [a]
Set.toList (Set Token -> [Token]) -> Set Token -> [Token]
forall a b. (a -> b) -> a -> b
$ Sign -> KIND -> Set Token
getSymbolsByKind Sign
sig KIND
PredKind
                           sortAx :: [Named CASLFORMULA]
sortAx = Sign -> [Token] -> [Named CASLFORMULA]
generateSortAxioms Sign
sig [Token]
sorts
                           funcAx :: [Named CASLFORMULA]
funcAx = Sign -> [Token] -> [Named CASLFORMULA]
generateFuncAxioms Sign
sig [Token]
funcs
                           predAx :: [Named CASLFORMULA]
predAx = Sign -> [Token] -> [Named CASLFORMULA]
generatePredAxioms Sign
sig [Token]
preds

-- generating axioms for translated predicate symbols
generatePredAxioms :: Sign -> [NAME] -> [Named CASL_AS.CASLFORMULA]
generatePredAxioms :: Sign -> [Token] -> [Named CASLFORMULA]
generatePredAxioms = (Token -> [Named CASLFORMULA]) -> [Token] -> [Named CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Token -> [Named CASLFORMULA]) -> [Token] -> [Named CASLFORMULA])
-> (Sign -> Token -> [Named CASLFORMULA])
-> Sign
-> [Token]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Token -> [Named CASLFORMULA]
generatePredAxiomsH

generatePredAxiomsH :: Sign -> NAME -> [Named CASL_AS.CASLFORMULA]
generatePredAxiomsH :: Sign -> Token -> [Named CASLFORMULA]
generatePredAxiomsH sig :: Sign
sig p :: Token
p =
      [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_pred_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
p) CASLFORMULA
formula | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
argNames]
   where Just argNames :: [Token]
argNames = Token -> Sign -> Maybe [Token]
getArgumentNames Token
p Sign
sig
         Just argTypes :: [TYPE]
argTypes = Token -> Sign -> Maybe [TYPE]
getArgumentTypes Token
p Sign
sig
         args :: [CASLTERM]
args = (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar [Token]
argNames
         formula :: CASLFORMULA
formula = [Token] -> CASLFORMULA -> CASLFORMULA
makeForall
                     [Token]
argNames
                     (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl
                        (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg ([TYPE] -> [CASLTERM] -> Sign -> CASLFORMULA
makeTypeHyps [TYPE]
argTypes [CASLTERM]
args Sign
sig))
                        (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg (Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
p [CASLTERM]
args Sign
sig)))

-- generating axioms for translated function symbols
generateFuncAxioms :: Sign -> [NAME] -> [Named CASL_AS.CASLFORMULA]
generateFuncAxioms :: Sign -> [Token] -> [Named CASLFORMULA]
generateFuncAxioms = (Token -> [Named CASLFORMULA]) -> [Token] -> [Named CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap ((Token -> [Named CASLFORMULA]) -> [Token] -> [Named CASLFORMULA])
-> (Sign -> Token -> [Named CASLFORMULA])
-> Sign
-> [Token]
-> [Named CASLFORMULA]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign -> Token -> [Named CASLFORMULA]
generateFuncAxiomsH

generateFuncAxiomsH :: Sign -> NAME -> [Named CASL_AS.CASLFORMULA]
generateFuncAxiomsH :: Sign -> Token -> [Named CASLFORMULA]
generateFuncAxiomsH sig :: Sign
sig f :: Token
f =
   if [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
argNames
      then [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_func_1_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
f) CASLFORMULA
formula0]
      else [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_func_1_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
f) CASLFORMULA
formula1,
            String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_func_2_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
f) CASLFORMULA
formula2]
   where Just argNames :: [Token]
argNames = Token -> Sign -> Maybe [Token]
getArgumentNames Token
f Sign
sig
         Just argTypes :: [TYPE]
argTypes = Token -> Sign -> Maybe [TYPE]
getArgumentTypes Token
f Sign
sig
         Just resultType :: TYPE
resultType = Token -> Sign -> Maybe TYPE
getReturnType Token
f Sign
sig
         args :: [CASLTERM]
args = (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar [Token]
argNames
         formula1 :: CASLFORMULA
formula1 = [Token] -> CASLFORMULA -> CASLFORMULA
makeForall
                      [Token]
argNames
                      (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl
                         (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg ([TYPE] -> [CASLTERM] -> Sign -> CASLFORMULA
makeTypeHyps [TYPE]
argTypes [CASLTERM]
args Sign
sig))
                         (CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CASL_AS.mkStEq (Token -> [CASLTERM] -> Sign -> CASLTERM
makeApplication Token
f [CASLTERM]
args Sign
sig) CASLTERM
bot))
         formula2 :: CASLFORMULA
formula2 = [Token] -> CASLFORMULA -> CASLFORMULA
makeForall
                      [Token]
argNames
                      (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl
                         ([TYPE] -> [CASLTERM] -> Sign -> CASLFORMULA
makeTypeHyps [TYPE]
argTypes [CASLTERM]
args Sign
sig)
                         (TYPE -> CASLTERM -> Sign -> CASLFORMULA
makeTypeHyp TYPE
resultType
                                      (Token -> [CASLTERM] -> Sign -> CASLTERM
makeApplication Token
f [CASLTERM]
args Sign
sig) Sign
sig))
         formula0 :: CASLFORMULA
formula0 = TYPE -> CASLTERM -> Sign -> CASLFORMULA
makeTypeHyp TYPE
resultType (Token -> [CASLTERM] -> Sign -> CASLTERM
makeApplication Token
f [] Sign
sig) Sign
sig

-- generating axioms for translated sort symbols
generateSortAxioms :: Sign -> [NAME] -> [Named CASL_AS.CASLFORMULA]
generateSortAxioms :: Sign -> [Token] -> [Named CASLFORMULA]
generateSortAxioms sig :: Sign
sig ss :: [Token]
ss =
  [Named CASLFORMULA]
axioms1 [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
axioms2 [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA
axiom3] [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
axioms4
  where axioms1 :: [Named CASLFORMULA]
axioms1 = (Token -> [Named CASLFORMULA]) -> [Token] -> [Named CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Sign -> Token -> [Named CASLFORMULA]
generateSortAxiomsH1 Sign
sig) [Token]
ss
        axioms2 :: [Named CASLFORMULA]
axioms2 = (Token -> [Named CASLFORMULA]) -> [Token] -> [Named CASLFORMULA]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Sign -> Token -> [Named CASLFORMULA]
generateSortAxiomsH2 Sign
sig) [Token]
ss
        axiom3 :: Named CASLFORMULA
axiom3 = Sign -> [Token] -> Named CASLFORMULA
generateSortAxiomsH3 Sign
sig [Token]
ss
        axioms4 :: [Named CASLFORMULA]
axioms4 = Sign -> [Token] -> [Named CASLFORMULA]
generateSortAxiomsH4 Sign
sig [Token]
ss

generateSortAxiomsH1 :: Sign -> NAME -> [Named CASL_AS.CASLFORMULA]
generateSortAxiomsH1 :: Sign -> Token -> [Named CASLFORMULA]
generateSortAxiomsH1 sig :: Sign
sig s :: Token
s =
      [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_sort_1_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s) CASLFORMULA
formula | Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ [Token] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [Token]
argNames]
   where Just argNames :: [Token]
argNames = Token -> Sign -> Maybe [Token]
getArgumentNames Token
s Sign
sig
         Just argTypes :: [TYPE]
argTypes = Token -> Sign -> Maybe [TYPE]
getArgumentTypes Token
s Sign
sig
         args :: [CASLTERM]
args = (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar [Token]
argNames
         elName :: Token
elName = String -> Range -> Token
Token "gen_y" Range
nr
         el :: CASLTERM
el = Token -> CASLTERM
makeVar Token
elName
         formula :: CASLFORMULA
formula = [Token] -> CASLFORMULA -> CASLFORMULA
makeForall
                     [Token]
argNames
                     (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl
                        (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg ([TYPE] -> [CASLTERM] -> Sign -> CASLFORMULA
makeTypeHyps [TYPE]
argTypes [CASLTERM]
args Sign
sig))
                        ([Token] -> CASLFORMULA -> CASLFORMULA
makeForall
                           [Token
elName]
                           (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg
                              (Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s ([CASLTERM]
args [CASLTERM] -> [CASLTERM] -> [CASLTERM]
forall a. [a] -> [a] -> [a]
++ [CASLTERM
el]) Sign
sig))))

generateSortAxiomsH2 :: Sign -> NAME -> [Named CASL_AS.CASLFORMULA]
generateSortAxiomsH2 :: Sign -> Token -> [Named CASLFORMULA]
generateSortAxiomsH2 sig :: Sign
sig s :: Token
s =
   if Int
ar Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0
      then [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_sort_2_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s) CASLFORMULA
formula0]
      else [String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_sort_2_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s) CASLFORMULA
formula1,
            String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_sort_3_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s) CASLFORMULA
formula2]
   where Just ar :: Int
ar = Token -> Sign -> Maybe Int
getSymbolArity Token
s Sign
sig
         argNames1 :: [Token]
argNames1 = String -> Int -> [Token]
makeArgNames "x" Int
ar
         argNames2 :: [Token]
argNames2 = String -> Int -> [Token]
makeArgNames "y" Int
ar
         elName :: Token
elName = String -> Range -> Token
Token "z" Range
nr
         args1 :: [CASLTERM]
args1 = (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar [Token]
argNames1
         args2 :: [CASLTERM]
args2 = (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar [Token]
argNames2
         el :: CASLTERM
el = Token -> CASLTERM
makeVar Token
elName
         formula1 :: CASLFORMULA
formula1 = [Token] -> CASLFORMULA -> CASLFORMULA
makeForall
                      [Token]
argNames1
                      (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s ([CASLTERM]
args1 [CASLTERM] -> [CASLTERM] -> [CASLTERM]
forall a. [a] -> [a] -> [a]
++ [CASLTERM
bot]) Sign
sig
         formula2 :: CASLFORMULA
formula2 = [Token] -> CASLFORMULA -> CASLFORMULA
makeForall
                      ([Token]
argNames1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
argNames2 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
elName])
                      (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl
                         ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CASL_AS.conjunct
                            [Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s ([CASLTERM]
args1 [CASLTERM] -> [CASLTERM] -> [CASLTERM]
forall a. [a] -> [a] -> [a]
++ [CASLTERM
el]) Sign
sig,
                             Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s ([CASLTERM]
args2 [CASLTERM] -> [CASLTERM] -> [CASLTERM]
forall a. [a] -> [a] -> [a]
++ [CASLTERM
el]) Sign
sig])
                         (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CASL_AS.conjunct
                            ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (CASLTERM -> CASLTERM -> CASLFORMULA)
-> [CASLTERM] -> [CASLTERM] -> [CASLFORMULA]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CASL_AS.mkStEq [CASLTERM]
args1 [CASLTERM]
args2
         formula0 :: CASLFORMULA
formula0 = CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s [CASLTERM
bot] Sign
sig

generateSortAxiomsH3 :: Sign -> [NAME] -> Named CASL_AS.CASLFORMULA
generateSortAxiomsH3 :: Sign -> [Token] -> Named CASLFORMULA
generateSortAxiomsH3 sig :: Sign
sig ss :: [Token]
ss =
   String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "gen_sort_4" CASLFORMULA
formula
   where elName :: Token
elName = String -> Range -> Token
Token "y" Range
nr
         el :: CASLTERM
el = Token -> CASLTERM
makeVar Token
elName
         ar :: Token -> Int
ar s :: Token
s = Maybe Int -> Int
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe Int -> Int) -> Maybe Int -> Int
forall a b. (a -> b) -> a -> b
$ Token -> Sign -> Maybe Int
getSymbolArity Token
s Sign
sig
         argNames :: Token -> [Token]
argNames s :: Token
s = String -> Int -> [Token]
makeArgNames "x" (Token -> Int
ar Token
s)
         args :: Token -> [CASLTERM]
args s :: Token
s = (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar (Token -> [Token]
argNames Token
s)
         formula :: CASLFORMULA
formula = [Token] -> CASLFORMULA -> CASLFORMULA
makeForall
                     [Token
elName]
                     (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl
                        (CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg (CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CASL_AS.mkStEq CASLTERM
el CASLTERM
bot))
                        ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CASL_AS.disjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ (Token -> CASLFORMULA) -> [Token] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLFORMULA
subformula [Token]
ss))
         subformula :: Token -> CASLFORMULA
subformula s :: Token
s = if Token -> Int
ar Token
s Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== 0
                           then Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s [CASLTERM
el] Sign
sig
                           else [Token] -> CASLFORMULA -> CASLFORMULA
makeExists
                                  (Token -> [Token]
argNames Token
s)
                                  (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s (Token -> [CASLTERM]
args Token
s [CASLTERM] -> [CASLTERM] -> [CASLTERM]
forall a. [a] -> [a] -> [a]
++ [CASLTERM
el]) Sign
sig

generateSortAxiomsH4 :: Sign -> [NAME] -> [Named CASL_AS.CASLFORMULA]
generateSortAxiomsH4 :: Sign -> [Token] -> [Named CASLFORMULA]
generateSortAxiomsH4 sig :: Sign
sig ss :: [Token]
ss =
  ((Token, Token) -> Named CASLFORMULA)
-> [(Token, Token)] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> (Token, Token) -> Named CASLFORMULA
generateSortAxiomsH4H Sign
sig) [ (Token
s1, Token
s2) | Token
s1 <- [Token]
ss, Token
s2 <- [Token]
ss, Token
s1 Token -> Token -> Bool
forall a. Ord a => a -> a -> Bool
< Token
s2 ]

generateSortAxiomsH4H :: Sign -> (NAME, NAME) -> Named CASL_AS.CASLFORMULA
generateSortAxiomsH4H :: Sign -> (Token, Token) -> Named CASLFORMULA
generateSortAxiomsH4H sig :: Sign
sig (s1 :: Token
s1, s2 :: Token
s2) =
   String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed ("gen_sort_5_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s1 String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Token -> String
forall a. Show a => a -> String
show Token
s2) CASLFORMULA
formula
   where Just ar1 :: Int
ar1 = Token -> Sign -> Maybe Int
getSymbolArity Token
s1 Sign
sig
         Just ar2 :: Int
ar2 = Token -> Sign -> Maybe Int
getSymbolArity Token
s2 Sign
sig
         argNames1 :: [Token]
argNames1 = String -> Int -> [Token]
makeArgNames "x" Int
ar1
         argNames2 :: [Token]
argNames2 = String -> Int -> [Token]
makeArgNames "y" Int
ar2
         elName :: Token
elName = String -> Range -> Token
Token "z" Range
nr
         args1 :: [CASLTERM]
args1 = (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar [Token]
argNames1
         args2 :: [CASLTERM]
args2 = (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar [Token]
argNames2
         el :: CASLTERM
el = Token -> CASLTERM
makeVar Token
elName
         formula :: CASLFORMULA
formula = [Token] -> CASLFORMULA -> CASLFORMULA
makeForall ([Token]
argNames1 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token]
argNames2 [Token] -> [Token] -> [Token]
forall a. [a] -> [a] -> [a]
++ [Token
elName])
           (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl (Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s1 ([CASLTERM]
args1 [CASLTERM] -> [CASLTERM] -> [CASLTERM]
forall a. [a] -> [a] -> [a]
++ [CASLTERM
el]) Sign
sig)
           (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s2 ([CASLTERM]
args2 [CASLTERM] -> [CASLTERM] -> [CASLTERM]
forall a. [a] -> [a] -> [a]
++ [CASLTERM
el]) Sign
sig
-- make argument names
makeArgNames :: String -> Int -> [NAME]
makeArgNames :: String -> Int -> [Token]
makeArgNames var :: String
var n :: Int
n = (Int -> Token) -> [Int] -> [Token]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: Int
i -> String -> Range -> Token
Token (String
var String -> String -> String
forall a. [a] -> [a] -> [a]
++ "_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
i) Range
nr) [1 .. Int
n]

-- make a variable
makeVar :: NAME -> CASL_AS.CASLTERM
makeVar :: Token -> CASLTERM
makeVar var :: Token
var = Token -> SORT -> Range -> CASLTERM
forall f. Token -> SORT -> Range -> TERM f
CASL_AS.Qual_var Token
var SORT
sort Range
nr

-- make an application
makeApplication :: NAME -> [CASL_AS.CASLTERM] -> Sign -> CASL_AS.CASLTERM
makeApplication :: Token -> [CASLTERM] -> Sign -> CASLTERM
makeApplication f :: Token
f as :: [CASLTERM]
as sig :: Sign
sig =
  OP_SYMB -> [CASLTERM] -> Range -> CASLTERM
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
CASL_AS.Application
    (SORT -> OP_TYPE -> Range -> OP_SYMB
CASL_AS.Qual_op_name
      ([Token] -> SORT
mkId [Token
f])
      (OpKind -> [SORT] -> SORT -> Range -> OP_TYPE
CASL_AS.Op_type OpKind
CASL_AS.Total (Int -> [SORT]
folType Int
arity) SORT
sort Range
nr)
      Range
nr)
    [CASLTERM]
as
    Range
nr
  where Just arity :: Int
arity = Token -> Sign -> Maybe Int
getSymbolArity Token
f Sign
sig

-- make a predication
makePredication :: NAME -> [CASL_AS.CASLTERM] -> Sign -> CASL_AS.CASLFORMULA
makePredication :: Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication p :: Token
p as :: [CASLTERM]
as sig :: Sign
sig =
  PRED_SYMB -> [CASLTERM] -> Range -> CASLFORMULA
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
CASL_AS.Predication
    (SORT -> PRED_TYPE -> Range -> PRED_SYMB
CASL_AS.Qual_pred_name
       ([Token] -> SORT
mkId [Token
p])
       ([SORT] -> Range -> PRED_TYPE
CASL_AS.Pred_type (Int -> [SORT]
folType Int
arity1) Range
nr)
       Range
nr)
    [CASLTERM]
as
    Range
nr
  where Just kind :: KIND
kind = Token -> Sign -> Maybe KIND
getSymbolKind Token
p Sign
sig
        Just arity :: Int
arity = Token -> Sign -> Maybe Int
getSymbolArity Token
p Sign
sig
        arity1 :: Int
arity1 = if KIND
kind KIND -> KIND -> Bool
forall a. Eq a => a -> a -> Bool
== KIND
SortKind then Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1 else Int
arity

-- make a universal quantification
makeForall :: [NAME] -> CASL_AS.CASLFORMULA -> CASL_AS.CASLFORMULA
makeForall :: [Token] -> CASLFORMULA -> CASLFORMULA
makeForall vars :: [Token]
vars = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
CASL_AS.mkForall [[Token] -> SORT -> Range -> VAR_DECL
CASL_AS.Var_decl [Token]
vars SORT
sort Range
nr]

-- make an existential quantification
makeExists :: [NAME] -> CASL_AS.CASLFORMULA -> CASL_AS.CASLFORMULA
makeExists :: [Token] -> CASLFORMULA -> CASLFORMULA
makeExists vars :: [Token]
vars = [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
CASL_AS.mkExist [[Token] -> SORT -> Range -> VAR_DECL
CASL_AS.Var_decl [Token]
vars SORT
sort Range
nr]

-- make a type hypothesis
makeTypeHyp :: TYPE -> CASL_AS.CASLTERM -> Sign -> CASL_AS.CASLFORMULA
makeTypeHyp :: TYPE -> CASLTERM -> Sign -> CASLFORMULA
makeTypeHyp t :: TYPE
t term :: CASLTERM
term sig :: Sign
sig = Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
s ([CASLTERM]
args [CASLTERM] -> [CASLTERM] -> [CASLTERM]
forall a. [a] -> [a] -> [a]
++ [CASLTERM
term]) Sign
sig
                         where Univ sortterm :: TERM
sortterm = TYPE
t
                               (s :: Token
s, as :: [TERM]
as) = TERM -> (Token, [TERM])
termFlatForm TERM
sortterm
                               args :: [CASLTERM]
args = (TERM -> CASLTERM) -> [TERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> TERM -> CASLTERM
termTransl Sign
sig) [TERM]
as

-- make type hypotheses
makeTypeHyps :: [TYPE] -> [CASL_AS.CASLTERM]
                -> Sign -> CASL_AS.CASLFORMULA
makeTypeHyps :: [TYPE] -> [CASLTERM] -> Sign -> CASLFORMULA
makeTypeHyps ts :: [TYPE]
ts terms :: [CASLTERM]
terms sig :: Sign
sig =
  [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CASL_AS.conjunct ([CASLFORMULA] -> CASLFORMULA) -> [CASLFORMULA] -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ ((TYPE, CASLTERM) -> CASLFORMULA)
-> [(TYPE, CASLTERM)] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (\ (t :: TYPE
t, term :: CASLTERM
term) -> TYPE -> CASLTERM -> Sign -> CASLFORMULA
makeTypeHyp TYPE
t CASLTERM
term Sign
sig) ([(TYPE, CASLTERM)] -> [CASLFORMULA])
-> [(TYPE, CASLTERM)] -> [CASLFORMULA]
forall a b. (a -> b) -> a -> b
$ [TYPE] -> [CASLTERM] -> [(TYPE, CASLTERM)]
forall a b. [a] -> [b] -> [(a, b)]
zip [TYPE]
ts [CASLTERM]
terms

-- term translation
termTransl :: Sign -> TERM -> CASL_AS.CASLTERM
termTransl :: Sign -> TERM -> CASLTERM
termTransl sig :: Sign
sig (Identifier x :: Token
x) = if Bool -> Bool
not (Token -> Sign -> Bool
isConstant Token
x Sign
sig)
                                   then Token -> SORT -> Range -> CASLTERM
forall f. Token -> SORT -> Range -> TERM f
CASL_AS.Qual_var Token
x SORT
sort Range
nr
                                else Token -> [CASLTERM] -> Sign -> CASLTERM
makeApplication Token
x [] Sign
sig
termTransl sig :: Sign
sig t :: TERM
t = Token -> [CASLTERM] -> Sign -> CASLTERM
makeApplication Token
f ((TERM -> CASLTERM) -> [TERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> TERM -> CASLTERM
termTransl Sign
sig) [TERM]
as) Sign
sig
                   where (f :: Token
f, as :: [TERM]
as) = TERM -> (Token, [TERM])
termFlatForm TERM
t

-- signature translation
sigTransl :: Sign -> (CASL_Sign.CASLSign, [Named CASL_AS.CASLFORMULA])
sigTransl :: Sign -> (CASLSign, [Named CASLFORMULA])
sigTransl sig :: Sign
sig = (Sign -> CASLSign
sigMap Sign
sig, Sign -> [Named CASLFORMULA]
generateAxioms Sign
sig)

-- theory translation
theoryTransl :: (Sign, [Named FORMULA]) ->
                (CASL_Sign.CASLSign, [Named CASL_AS.CASLFORMULA])
theoryTransl :: (Sign, [Named FORMULA]) -> (CASLSign, [Named CASLFORMULA])
theoryTransl (sig :: Sign
sig, fs :: [Named FORMULA]
fs) = (CASLSign
sigCASL, [Named CASLFORMULA]
axCASL [Named CASLFORMULA] -> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a. [a] -> [a] -> [a]
++ [Named CASLFORMULA]
fsCASL)
                        where (sigCASL :: CASLSign
sigCASL, axCASL :: [Named CASLFORMULA]
axCASL) = Sign -> (CASLSign, [Named CASLFORMULA])
sigTransl Sign
sig
                              fsCASL :: [Named CASLFORMULA]
fsCASL = (Named FORMULA -> Named CASLFORMULA)
-> [Named FORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> Named FORMULA -> Named CASLFORMULA
namedSenTransl Sign
sig) [Named FORMULA]
fs

-- morphism translation
morphTransl :: Morphism -> CASL_Morphism.CASLMor
morphTransl :: Morphism -> CASLMor
morphTransl (Morphism sig1 :: Sign
sig1 sig2 :: Sign
sig2 sym_map :: Map Token Token
sym_map) =
  (CASLMor -> (Token, Token) -> CASLMor)
-> CASLMor -> [(Token, Token)] -> CASLMor
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (Sign -> CASLMor -> (Token, Token) -> CASLMor
addSymbolTransl Sign
sig1) CASLMor
init_morph ([(Token, Token)] -> CASLMor) -> [(Token, Token)] -> CASLMor
forall a b. (a -> b) -> a -> b
$ Map Token Token -> [(Token, Token)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Token Token
sym_map
  where init_morph :: CASLMor
init_morph = Morphism :: forall f e m.
Sign f e
-> Sign f e
-> Sort_map
-> Op_map
-> Pred_map
-> m
-> Morphism f e m
CASL_Morphism.Morphism
                       { msource :: CASLSign
CASL_Morphism.msource = (CASLSign, [Named CASLFORMULA]) -> CASLSign
forall a b. (a, b) -> a
fst ((CASLSign, [Named CASLFORMULA]) -> CASLSign)
-> (CASLSign, [Named CASLFORMULA]) -> CASLSign
forall a b. (a -> b) -> a -> b
$ Sign -> (CASLSign, [Named CASLFORMULA])
sigTransl Sign
sig1
                       , mtarget :: CASLSign
CASL_Morphism.mtarget = (CASLSign, [Named CASLFORMULA]) -> CASLSign
forall a b. (a, b) -> a
fst ((CASLSign, [Named CASLFORMULA]) -> CASLSign)
-> (CASLSign, [Named CASLFORMULA]) -> CASLSign
forall a b. (a -> b) -> a -> b
$ Sign -> (CASLSign, [Named CASLFORMULA])
sigTransl Sign
sig2
                       , sort_map :: Sort_map
CASL_Morphism.sort_map = Sort_map
forall k a. Map k a
Map.empty
                       , op_map :: Op_map
CASL_Morphism.op_map = Op_map
forall k a. Map k a
Map.empty
                       , pred_map :: Pred_map
CASL_Morphism.pred_map = Pred_map
forall k a. Map k a
Map.empty
                       , extended_map :: ()
CASL_Morphism.extended_map = ()
                       }

addSymbolTransl :: Sign -> CASL_Morphism.CASLMor -> (NAME, NAME) ->
                   CASL_Morphism.CASLMor
addSymbolTransl :: Sign -> CASLMor -> (Token, Token) -> CASLMor
addSymbolTransl sig :: Sign
sig m :: CASLMor
m (f :: Token
f, g :: Token
g) = case KIND
kind of
    FuncKind -> let
          f1 :: (SORT, OpType)
f1 = ([Token] -> SORT
mkId [Token
f], OpKind -> [SORT] -> SORT -> OpType
CASL_Sign.OpType OpKind
CASL_AS.Partial (Int -> [SORT]
folType Int
arity) SORT
sort)
          g1 :: (SORT, OpKind)
g1 = ([Token] -> SORT
mkId [Token
g], OpKind
CASL_AS.Total)
          in CASLMor
m {op_map :: Op_map
CASL_Morphism.op_map = (SORT, OpType) -> (SORT, OpKind) -> Op_map -> Op_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT, OpType)
f1 (SORT, OpKind)
g1
                (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
CASL_Morphism.op_map CASLMor
m}
    PredKind -> let
          f1 :: (SORT, PredType)
f1 = ([Token] -> SORT
mkId [Token
f], [SORT] -> PredType
CASL_Sign.PredType (Int -> [SORT]
folType Int
arity))
          g1 :: SORT
g1 = [Token] -> SORT
mkId [Token
g]
          in CASLMor
m {pred_map :: Pred_map
CASL_Morphism.pred_map = (SORT, PredType) -> SORT -> Pred_map -> Pred_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT, PredType)
f1 SORT
g1
                (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
CASL_Morphism.pred_map CASLMor
m}
    SortKind -> let
          f1 :: (SORT, PredType)
f1 = ([Token] -> SORT
mkId [Token
f], [SORT] -> PredType
CASL_Sign.PredType (Int -> [SORT]
folType (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1)))
          g1 :: SORT
g1 = [Token] -> SORT
mkId [Token
g]
          in CASLMor
m {pred_map :: Pred_map
CASL_Morphism.pred_map = (SORT, PredType) -> SORT -> Pred_map -> Pred_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (SORT, PredType)
f1 SORT
g1
                (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
CASL_Morphism.pred_map CASLMor
m}
  where Just kind :: KIND
kind = Token -> Sign -> Maybe KIND
getSymbolKind Token
f Sign
sig
        Just arity :: Int
arity = Token -> Sign -> Maybe Int
getSymbolArity Token
f Sign
sig

makeTypesAndVars :: [DECL] -> ([TYPE], [NAME], [CASL_AS.CASLTERM])
makeTypesAndVars :: [DECL] -> ([TYPE], [Token], [CASLTERM])
makeTypesAndVars ds :: [DECL]
ds = let varNames :: [Token]
varNames = [DECL] -> [Token]
getVarsFromDecls [DECL]
ds in
  ( (DECL -> [TYPE]) -> [DECL] -> [TYPE]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (ns :: [Token]
ns, t1 :: TYPE
t1) -> Int -> TYPE -> [TYPE]
forall a. Int -> a -> [a]
replicate ([Token] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Token]
ns) TYPE
t1) [DECL]
ds
  , [Token]
varNames, (Token -> CASLTERM) -> [Token] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map Token -> CASLTERM
makeVar [Token]
varNames)

-- sentence translation
senTransl :: Sign -> FORMULA -> CASL_AS.CASLFORMULA
senTransl :: Sign -> FORMULA -> CASLFORMULA
senTransl sig :: Sign
sig frm :: FORMULA
frm = case FORMULA
frm of
    T -> CASLFORMULA
forall f. FORMULA f
CASL_AS.trueForm
    F -> CASLFORMULA
forall f. FORMULA f
CASL_AS.falseForm
    Pred t :: TERM
t -> Token -> [CASLTERM] -> Sign -> CASLFORMULA
makePredication Token
p ((TERM -> CASLTERM) -> [TERM] -> [CASLTERM]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> TERM -> CASLTERM
termTransl Sign
sig) [TERM]
as) Sign
sig
      where (p :: Token
p, as :: [TERM]
as) = TERM -> (Token, [TERM])
termFlatForm TERM
t
    Equality t1 :: TERM
t1 t2 :: TERM
t2 -> CASLTERM -> CASLTERM -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
CASL_AS.mkStEq (Sign -> TERM -> CASLTERM
termTransl Sign
sig TERM
t1) (Sign -> TERM -> CASLTERM
termTransl Sign
sig TERM
t2)
    Negation f :: FORMULA
f -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
CASL_AS.mkNeg (Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig FORMULA
f)
    Conjunction fs :: [FORMULA]
fs -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CASL_AS.conjunct ((FORMULA -> CASLFORMULA) -> [FORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig) [FORMULA]
fs)
    Disjunction fs :: [FORMULA]
fs -> [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CASL_AS.disjunct ((FORMULA -> CASLFORMULA) -> [FORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig) [FORMULA]
fs)
    Implication f :: FORMULA
f g :: FORMULA
g -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl (Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig FORMULA
f) (Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig FORMULA
g)
    Equivalence f :: FORMULA
f g :: FORMULA
g -> CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkEqv (Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig FORMULA
f) (Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig FORMULA
g)
    Forall ds :: [DECL]
ds f :: FORMULA
f -> let (types :: [TYPE]
types, varNames :: [Token]
varNames, vars :: [CASLTERM]
vars) = [DECL] -> ([TYPE], [Token], [CASLTERM])
makeTypesAndVars [DECL]
ds in
        [Token] -> CASLFORMULA -> CASLFORMULA
makeForall [Token]
varNames
             (CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
CASL_AS.mkImpl ([TYPE] -> [CASLTERM] -> Sign -> CASLFORMULA
makeTypeHyps [TYPE]
types [CASLTERM]
vars Sign
sig) (Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig FORMULA
f))
    Exists ds :: [DECL]
ds f :: FORMULA
f -> let (types :: [TYPE]
types, varNames :: [Token]
varNames, vars :: [CASLTERM]
vars) = [DECL] -> ([TYPE], [Token], [CASLTERM])
makeTypesAndVars [DECL]
ds in
        [Token] -> CASLFORMULA -> CASLFORMULA
makeExists [Token]
varNames
             ([CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
CASL_AS.conjunct [[TYPE] -> [CASLTERM] -> Sign -> CASLFORMULA
makeTypeHyps [TYPE]
types [CASLTERM]
vars Sign
sig, Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig FORMULA
f])

-- named sentence translation
namedSenTransl :: Sign -> Named FORMULA -> Named CASL_AS.CASLFORMULA
namedSenTransl :: Sign -> Named FORMULA -> Named CASLFORMULA
namedSenTransl sig :: Sign
sig nf :: Named FORMULA
nf = Named FORMULA
nf {sentence :: CASLFORMULA
sentence = Sign -> FORMULA -> CASLFORMULA
senTransl Sign
sig (FORMULA -> CASLFORMULA) -> FORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
sentence Named FORMULA
nf}

-- symbol translation
symbolTransl :: Sign -> Symbol -> Set.Set CASL_Sign.Symbol
symbolTransl :: Sign -> Symbol -> Set Symbol
symbolTransl sig :: Sign
sig sym :: Symbol
sym =
  Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ SORT -> SymbType -> Symbol
CASL_Sign.Symbol ([Token] -> SORT
mkId [Token
n])
    (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ case KIND
kind of
           PredKind -> PredType -> SymbType
CASL_Sign.PredAsItemType
                         (PredType -> SymbType) -> PredType -> SymbType
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
CASL_Sign.PredType (Int -> [SORT]
folType Int
arity)
           FuncKind -> OpType -> SymbType
CASL_Sign.OpAsItemType
                         (OpType -> SymbType) -> OpType -> SymbType
forall a b. (a -> b) -> a -> b
$ [SORT] -> SORT -> OpType
CASL_Sign.mkTotOpType (Int -> [SORT]
folType Int
arity) SORT
sort
           SortKind -> PredType -> SymbType
CASL_Sign.PredAsItemType
                         (PredType -> SymbType) -> PredType -> SymbType
forall a b. (a -> b) -> a -> b
$ [SORT] -> PredType
CASL_Sign.PredType (Int -> [SORT]
folType (Int
arity Int -> Int -> Int
forall a. Num a => a -> a -> a
+ 1))
  where n :: Token
n = Symbol -> Token
name Symbol
sym
        Just kind :: KIND
kind = Token -> Sign -> Maybe KIND
getSymbolKind Token
n Sign
sig
        Just arity :: Int
arity = Token -> Sign -> Maybe Int
getSymbolArity Token
n Sign
sig