{- |
Module      :  PredefinedSign.hs
Description :  with inlined axioms
Copyright   :  (c) Uni and DFKI Bremen 2005-2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

-}

module CASL_DL.PredefinedCASLAxioms
  ( predefSign
  , predefinedSign
  , predefSign2
  , datatypeSigns
  , thing
  , nothing
  , conceptPred
  , dataPred
  , dataS
  , predefinedAxioms
  , mkNName
  , mkDigit
  , joinDigits
  , negateInt
  , integer
  , float
  , negateFloat
  , posInt
  , nonPosInt
  , decimal
  , double
  , upcast
  , mkDecimal
  , mkFloat
  , consChar
  , emptyStringTerm
  , trueT
  , falseT
  , nonNegInt
  , negIntS
  , stringS
  ) where

import CASL.AS_Basic_CASL
import CASL.Sign
import OWL2.Keywords

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

import qualified Data.Map as Map

import Data.Char

hetsPrefix :: String
hetsPrefix :: String
hetsPrefix = ""

-- | OWL topsort Thing
thing :: SORT
thing :: SORT
thing = String -> SORT
stringToId String
thingS

n :: Range
n :: Range
n = Range
nullRange

nothing :: SORT
nothing :: SORT
nothing = String -> SORT
stringToId String
nothingS

-- | OWL Data topSort DATA
dataS :: SORT
dataS :: SORT
dataS = String -> SORT
stringToId String
dATAS

integer :: SORT
integer :: SORT
integer = String -> SORT
stringToId String
integerS

float :: SORT
float :: SORT
float = String -> SORT
stringToId String
floatS

decimal :: SORT
decimal :: SORT
decimal = String -> SORT
stringToId String
decimalS

double :: SORT
double :: SORT
double = String -> SORT
stringToId String
doubleS

posInt :: SORT
posInt :: SORT
posInt = String -> SORT
stringToId String
positiveIntegerS

negIntS :: SORT
negIntS :: SORT
negIntS = String -> SORT
stringToId String
negativeIntegerS

nonPosInt :: SORT
nonPosInt :: SORT
nonPosInt = String -> SORT
stringToId String
nonPositiveIntegerS

nonNegInt :: SORT
nonNegInt :: SORT
nonNegInt = String -> SORT
stringToId String
nonNegativeIntegerS

classPredType :: PRED_TYPE
classPredType :: PRED_TYPE
classPredType = [SORT] -> Range -> PRED_TYPE
Pred_type [SORT
thing] Range
n

conceptPred :: PredType
conceptPred :: PredType
conceptPred = PRED_TYPE -> PredType
toPredType PRED_TYPE
classPredType

dataPred :: PredType
dataPred :: PredType
dataPred = [SORT] -> PredType
PredType [SORT
dataS, SORT
dataS]

boolS :: SORT
boolS :: SORT
boolS = String -> SORT
stringToId "boolean"

boolT :: OpType
boolT :: OpType
boolT = [SORT] -> SORT -> OpType
mkTotOpType [] SORT
boolS

trueS :: Id
trueS :: SORT
trueS = String -> SORT
stringToId "True"

falseS :: Id
falseS :: SORT
falseS = String -> SORT
stringToId "False"

mkConst :: Id -> OpType -> TERM ()
mkConst :: SORT -> OpType -> TERM ()
mkConst i :: SORT
i o :: OpType
o = OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
i (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
o) []

trueT :: TERM ()
trueT :: TERM ()
trueT = SORT -> OpType -> TERM ()
mkConst SORT
trueS OpType
boolT

falseT :: TERM ()
falseT :: TERM ()
falseT = SORT -> OpType -> TERM ()
mkConst SORT
falseS OpType
boolT

natT :: OpType
natT :: OpType
natT = [SORT] -> SORT -> OpType
mkTotOpType [] SORT
nonNegInt

-- | create a term of type nonNegativeInteger
mkDigit :: Int -> TERM ()
mkDigit :: Int -> TERM ()
mkDigit i :: Int
i = SORT -> OpType -> TERM ()
mkConst (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
i) OpType
natT

unMinus :: Id
unMinus :: SORT
unMinus = [Token] -> SORT
mkId [String -> Token
mkSimpleId "-", Token
placeTok]

minusTy :: OpType
minusTy :: OpType
minusTy = [SORT] -> SORT -> OpType
mkTotOpType [SORT
integer] SORT
integer

minusFloat :: OpType
minusFloat :: OpType
minusFloat = [SORT] -> SORT -> OpType
mkTotOpType [SORT
float] SORT
float

negateTy :: OpType -> TERM () -> TERM ()
negateTy :: OpType -> TERM () -> TERM ()
negateTy o :: OpType
o t :: TERM ()
t = OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
unMinus (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
o) [TERM ()
t]

-- | negate a term of type integer
negateInt :: TERM () -> TERM ()
negateInt :: TERM () -> TERM ()
negateInt = OpType -> TERM () -> TERM ()
negateTy OpType
minusTy

-- | negate a term of type float
negateFloat :: TERM () -> TERM ()
negateFloat :: TERM () -> TERM ()
negateFloat = OpType -> TERM () -> TERM ()
negateTy OpType
minusFloat

atAt :: Id
atAt :: SORT
atAt = String -> SORT
mkInfix "@@"

atAtTy :: OpType
atAtTy :: OpType
atAtTy = [SORT] -> SORT -> OpType
mkTotOpType [SORT
nonNegInt, SORT
nonNegInt] SORT
nonNegInt

mkBinOp :: Id -> OpType -> TERM () -> TERM () -> TERM ()
mkBinOp :: SORT -> OpType -> TERM () -> TERM () -> TERM ()
mkBinOp i :: SORT
i o :: OpType
o t1 :: TERM ()
t1 t2 :: TERM ()
t2 = OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
i (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
o) [TERM ()
t1, TERM ()
t2]

-- | join two terms of type nonNegativeInteger
joinDigits :: TERM () -> TERM () -> TERM ()
joinDigits :: TERM () -> TERM () -> TERM ()
joinDigits = SORT -> OpType -> TERM () -> TERM () -> TERM ()
mkBinOp SORT
atAt OpType
atAtTy

dec :: Id
dec :: SORT
dec = String -> SORT
mkInfix ":::"

decTy :: OpType
decTy :: OpType
decTy = [SORT] -> SORT -> OpType
mkTotOpType [SORT
nonNegInt, SORT
nonNegInt] SORT
float

{- | create the float given by two non-negative integers separated by the
decimal point -}
mkDecimal :: TERM () -> TERM () -> TERM ()
mkDecimal :: TERM () -> TERM () -> TERM ()
mkDecimal = SORT -> OpType -> TERM () -> TERM () -> TERM ()
mkBinOp SORT
dec OpType
decTy

eId :: Id
eId :: SORT
eId = String -> SORT
mkInfix "E"

expTy :: OpType
expTy :: OpType
expTy = [SORT] -> SORT -> OpType
mkTotOpType [SORT
float, SORT
integer] SORT
float

-- | construct the E float, where the second argument is of type integer
mkFloat :: TERM () -> TERM () -> TERM ()
mkFloat :: TERM () -> TERM () -> TERM ()
mkFloat = SORT -> OpType -> TERM () -> TERM () -> TERM ()
mkBinOp SORT
eId OpType
expTy

-- | upcast a term to a matching sort
upcast :: TERM () -> SORT -> TERM ()
upcast :: TERM () -> SORT -> TERM ()
upcast t :: TERM ()
t ty :: SORT
ty = TERM () -> SORT -> Range -> TERM ()
forall f. TERM f -> SORT -> Range -> TERM f
Sorted_term TERM ()
t SORT
ty Range
nullRange

charS :: Id
charS :: SORT
charS = String -> SORT
stringToId "Char"

charT :: OpType
charT :: OpType
charT = [SORT] -> SORT -> OpType
mkTotOpType [] SORT
charS

stringS :: Id
stringS :: SORT
stringS = String -> SORT
stringToId "string"

cons :: Id
cons :: SORT
cons = String -> SORT
mkInfix ":@:"

emptyString :: Id
emptyString :: SORT
emptyString = String -> SORT
stringToId "emptyString"

emptyStringTerm :: TERM ()
emptyStringTerm :: TERM ()
emptyStringTerm = OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
emptyString (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
emptyStringTy) []

charToId :: Char -> Id
charToId :: Char -> SORT
charToId c :: Char
c = let s :: String
s = Int -> String
forall a. Show a => a -> String
show (Char -> Int
ord Char
c) in
  String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ "'\\" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> Char -> String
forall a. Int -> a -> [a]
replicate (3 Int -> Int -> Int
forall a. Num a => a -> a -> a
- String -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length String
s) '0' String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show (Char -> Int
ord Char
c) String -> String -> String
forall a. [a] -> [a] -> [a]
++ "'"

mkChar :: Char -> TERM ()
mkChar :: Char -> TERM ()
mkChar c :: Char
c = OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp (Char -> SORT
charToId Char
c) (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
charT) []

consChar :: Char -> TERM () -> TERM ()
consChar :: Char -> TERM () -> TERM ()
consChar c :: Char
c t :: TERM ()
t = OP_SYMB -> [TERM ()] -> TERM ()
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (SORT -> OP_TYPE -> OP_SYMB
mkQualOp SORT
cons (OP_TYPE -> OP_SYMB) -> OP_TYPE -> OP_SYMB
forall a b. (a -> b) -> a -> b
$ OpType -> OP_TYPE
toOP_TYPE OpType
consTy) [Char -> TERM ()
mkChar Char
c, TERM ()
t]

emptyStringTy :: OpType
emptyStringTy :: OpType
emptyStringTy = [SORT] -> SORT -> OpType
mkTotOpType [] SORT
stringS

consTy :: OpType
consTy :: OpType
consTy = [SORT] -> SORT -> OpType
mkTotOpType [SORT
charS, SORT
stringS] SORT
stringS

-- | OWL bottom
noThing :: PRED_SYMB
noThing :: PRED_SYMB
noThing = SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
nothing PRED_TYPE
classPredType Range
n

intTypes :: [PredType]
intTypes :: [PredType]
intTypes = (SORT -> PredType) -> [SORT] -> [PredType]
forall a b. (a -> b) -> [a] -> [b]
map (\ t :: SORT
t -> [SORT] -> PredType
PredType [SORT
t]) [SORT
integer, SORT
nonNegInt]

predefinedSign2 :: e -> Sign f e
predefinedSign2 :: e -> Sign f e
predefinedSign2 e :: e
e = (e -> Sign f e
forall e f. e -> Sign f e
emptySign e
e) {
  sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
thing (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
dataS Rel SORT
forall a. Rel a
Rel.empty
  }

predefSign2 :: CASLSign
predefSign2 :: CASLSign
predefSign2 = () -> CASLSign
forall e f. e -> Sign f e
predefinedSign2 ()

-- | instead of one big signature, several small ones

charSign :: CASLSign
charSign :: CASLSign
charSign = (() -> CASLSign
forall e f. e -> Sign f e
emptySign ())
                 { sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey (String -> SORT
stringToId "Char") Rel SORT
forall a. Rel a
Rel.empty
                 , opMap :: OpMap
opMap = [(SORT, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                        ([(SORT, [OpType])] -> OpMap) -> [(SORT, [OpType])] -> OpMap
forall a b. (a -> b) -> a -> b
$  (Char -> (SORT, [OpType])) -> String -> [(SORT, [OpType])]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Char
c -> (Char -> SORT
charToId Char
c, [OpType
charT]))
                          [Int -> Char
chr 0 .. Int -> Char
chr 127]
                 }

integerSign :: CASLSign
integerSign :: CASLSign
integerSign  = (() -> CASLSign
forall e f. e -> Sign f e
emptySign ())
                 { sortRel :: Rel SORT
sortRel =
                      Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> Rel SORT
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList
                       [(SORT
negIntS, SORT
nonPosInt),
                        (SORT
nonNegInt, SORT
integer),
                        (SORT
nonPosInt, SORT
integer),
                        (SORT
posInt, SORT
nonNegInt),
                        (SORT
integer, SORT
dataS)]
                 , predMap :: PredMap
predMap =
                     [(SORT, [PredType])] -> PredMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                      ([(SORT, [PredType])] -> PredMap)
-> [(SORT, [PredType])] -> PredMap
forall a b. (a -> b) -> a -> b
$ 
                      (String -> (SORT, [PredType])) -> [String] -> [(SORT, [PredType])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ o :: String
o -> (String -> SORT
stringToId String
o, [PredType]
intTypes))
                         ["even", "odd"]
                 , opMap :: OpMap
opMap = [(SORT, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                        ([(SORT, [OpType])] -> OpMap) -> [(SORT, [OpType])] -> OpMap
forall a b. (a -> b) -> a -> b
$ (Int -> (SORT, [OpType])) -> [Int] -> [(SORT, [OpType])]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: Int
i -> (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
i, [OpType
natT]))
                          [0 .. 9 :: Int]
                        [(SORT, [OpType])] -> [(SORT, [OpType])] -> [(SORT, [OpType])]
forall a. [a] -> [a] -> [a]
++
                        [ 
                         (SORT
atAt, [OpType
atAtTy])
                        ]
                 , globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
emptyGlobalAnnos
                     { literal_annos :: LiteralAnnos
literal_annos = LiteralAnnos
emptyLiteralAnnos
                       { number_lit :: Maybe SORT
number_lit = SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
atAt
                        }}
                 }



predefinedSign :: e -> Sign f e
predefinedSign :: e -> Sign f e
predefinedSign e :: e
e = (e -> Sign f e
forall e f. e -> Sign f e
emptySign e
e)
                 { sortRel :: Rel SORT
sortRel = SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey (String -> SORT
stringToId "Char")
                      (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ SORT -> Rel SORT -> Rel SORT
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey SORT
thing
                      (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> Rel SORT
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList
                       [(SORT
boolS, SORT
dataS),
                        (SORT
integer, SORT
float),
                        (SORT
float, SORT
dataS),
                        (SORT
negIntS, SORT
nonPosInt),
                        (SORT
nonNegInt, SORT
integer),
                        (SORT
nonPosInt, SORT
integer),
                        (SORT
posInt, SORT
nonNegInt),
                        (SORT
stringS, SORT
dataS) ]
                 , predMap :: PredMap
predMap =
                     [(SORT, [PredType])] -> PredMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                      ([(SORT, [PredType])] -> PredMap)
-> [(SORT, [PredType])] -> PredMap
forall a b. (a -> b) -> a -> b
$ (SORT
nothing, [PredType
conceptPred])
                      (SORT, [PredType]) -> [(SORT, [PredType])] -> [(SORT, [PredType])]
forall a. a -> [a] -> [a]
: (DatatypeFacet -> (SORT, [PredType]))
-> [DatatypeFacet] -> [(SORT, [PredType])]
forall a b. (a -> b) -> [a] -> [b]
map ((\ o :: String
o -> (String -> SORT
mkInfix String
o, [PredType
dataPred])) (String -> (SORT, [PredType]))
-> (DatatypeFacet -> String) -> DatatypeFacet -> (SORT, [PredType])
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                         DatatypeFacet -> String
showFacet) [DatatypeFacet]
facetList
                      [(SORT, [PredType])]
-> [(SORT, [PredType])] -> [(SORT, [PredType])]
forall a. [a] -> [a] -> [a]
++ (String -> (SORT, [PredType])) -> [String] -> [(SORT, [PredType])]
forall a b. (a -> b) -> [a] -> [b]
map ( \ o :: String
o -> (String -> SORT
stringToId String
o, [PredType]
intTypes))
                         ["even", "odd"]
                 , opMap :: OpMap
opMap = [(SORT, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                        ([(SORT, [OpType])] -> OpMap) -> [(SORT, [OpType])] -> OpMap
forall a b. (a -> b) -> a -> b
$ (Int -> (SORT, [OpType])) -> [Int] -> [(SORT, [OpType])]
forall a b. (a -> b) -> [a] -> [b]
map (\ i :: Int
i -> (String -> SORT
stringToId (String -> SORT) -> String -> SORT
forall a b. (a -> b) -> a -> b
$ Int -> String
forall a. Show a => a -> String
show Int
i, [OpType
natT]))
                          [0 .. 9 :: Int]
                        [(SORT, [OpType])] -> [(SORT, [OpType])] -> [(SORT, [OpType])]
forall a. [a] -> [a] -> [a]
++ (Char -> (SORT, [OpType])) -> String -> [(SORT, [OpType])]
forall a b. (a -> b) -> [a] -> [b]
map (\ c :: Char
c -> (Char -> SORT
charToId Char
c, [OpType
charT]))
                          [Int -> Char
chr 0 .. Int -> Char
chr 127]
                        [(SORT, [OpType])] -> [(SORT, [OpType])] -> [(SORT, [OpType])]
forall a. [a] -> [a] -> [a]
++
                        [ (SORT
trueS, [OpType
boolT])
                        , (SORT
falseS, [OpType
boolT])
                        , (SORT
atAt, [OpType
atAtTy])
                        , (SORT
unMinus, [OpType
minusTy, OpType
minusFloat])
                        , (SORT
dec, [OpType
decTy])
                        , (SORT
eId, [OpType
expTy])
                        , (SORT
cons, [OpType
consTy])
                        , (SORT
emptyString, [OpType
emptyStringTy])
                        ]
                 , globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
emptyGlobalAnnos
                     { literal_annos :: LiteralAnnos
literal_annos = LiteralAnnos
emptyLiteralAnnos
                       { number_lit :: Maybe SORT
number_lit = SORT -> Maybe SORT
forall a. a -> Maybe a
Just SORT
atAt
                       , float_lit :: Maybe (SORT, SORT)
float_lit = (SORT, SORT) -> Maybe (SORT, SORT)
forall a. a -> Maybe a
Just (SORT
dec, SORT
eId)
                       , string_lit :: Maybe (SORT, SORT)
string_lit = (SORT, SORT) -> Maybe (SORT, SORT)
forall a. a -> Maybe a
Just (SORT
emptyString, SORT
cons) }}
                 }

floatSign :: CASLSign
floatSign :: CASLSign
floatSign = CASLSign
integerSign
                 { sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a -> Rel a
Rel.union (CASLSign -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel CASLSign
integerSign) 
                      (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> Rel SORT
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList
                       [
                        (SORT
integer, SORT
float),
                        (SORT
float, SORT
dataS)
                        ]
                 
                 , opMap :: OpMap
opMap = OpMap -> OpMap -> OpMap
forall a b.
(Ord a, Ord b) =>
MapSet a b -> MapSet a b -> MapSet a b
MapSet.union (CASLSign -> OpMap
forall f e. Sign f e -> OpMap
opMap CASLSign
integerSign) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ [(SORT, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                        ([(SORT, [OpType])] -> OpMap) -> [(SORT, [OpType])] -> OpMap
forall a b. (a -> b) -> a -> b
$ 
                        [
                          (SORT
unMinus, [OpType
minusTy, OpType
minusFloat])
                        , (SORT
dec, [OpType
decTy])
                        , (SORT
eId, [OpType
expTy])
                        ]
                 , globAnnos :: GlobalAnnos
globAnnos = (CASLSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos CASLSign
integerSign)
                     { literal_annos :: LiteralAnnos
literal_annos = (GlobalAnnos -> LiteralAnnos
literal_annos (GlobalAnnos -> LiteralAnnos) -> GlobalAnnos -> LiteralAnnos
forall a b. (a -> b) -> a -> b
$ CASLSign -> GlobalAnnos
forall f e. Sign f e -> GlobalAnnos
globAnnos CASLSign
integerSign)
                       {  float_lit :: Maybe (SORT, SORT)
float_lit = (SORT, SORT) -> Maybe (SORT, SORT)
forall a. a -> Maybe a
Just (SORT
dec, SORT
eId)
                        }}
                 }

boolSign :: CASLSign
boolSign :: CASLSign
boolSign = (() -> CASLSign
forall e f. e -> Sign f e
emptySign ())
                 { sortRel :: Rel SORT
sortRel =  Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> Rel SORT
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList
                       [(SORT
boolS, SORT
dataS)]
                 , opMap :: OpMap
opMap = [(SORT, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                        ([(SORT, [OpType])] -> OpMap) -> [(SORT, [OpType])] -> OpMap
forall a b. (a -> b) -> a -> b
$ 
                        [ (SORT
trueS, [OpType
boolT])
                        , (SORT
falseS, [OpType
boolT])
                        ]
                 }

stringSignAux :: CASLSign
stringSignAux :: CASLSign
stringSignAux = (() -> CASLSign
forall e f. e -> Sign f e
emptySign ())
                 { sortRel :: Rel SORT
sortRel = 
                      Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.transClosure (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [(SORT, SORT)] -> Rel SORT
forall a. Ord a => [(a, a)] -> Rel a
Rel.fromList
                       [ (SORT
stringS, SORT
dataS) ]
                 , opMap :: OpMap
opMap = [(SORT, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                        ([(SORT, [OpType])] -> OpMap) -> [(SORT, [OpType])] -> OpMap
forall a b. (a -> b) -> a -> b
$ 
                        [
                         (SORT
emptyString, [OpType
emptyStringTy])
                         , (SORT
cons, [OpType
consTy])
                        ]
                 , globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
emptyGlobalAnnos
                     { literal_annos :: LiteralAnnos
literal_annos = LiteralAnnos
emptyLiteralAnnos
                       { 
                       string_lit :: Maybe (SORT, SORT)
string_lit = (SORT, SORT) -> Maybe (SORT, SORT)
forall a. a -> Maybe a
Just (SORT
emptyString, SORT
cons) }}
                 }

stringSign :: CASLSign
stringSign :: CASLSign
stringSign = CASLSign -> CASLSign -> CASLSign
uniteCASLSign CASLSign
stringSignAux CASLSign
charSign

datatypeSigns :: Map.Map SORT CASLSign
datatypeSigns :: Map SORT CASLSign
datatypeSigns = [(SORT, CASLSign)] -> Map SORT CASLSign
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
   [ (SORT
charS, CASLSign
charSign)
   , (SORT
integer, CASLSign
integerSign)
   , (SORT
float, CASLSign
floatSign)
   , (SORT
boolS, CASLSign
boolSign)
   , (SORT
stringS, CASLSign
stringSign)]

predefSign :: CASLSign
predefSign :: CASLSign
predefSign = () -> CASLSign
forall e f. e -> Sign f e
predefinedSign ()

predefinedAxioms :: [Named (FORMULA ())]
predefinedAxioms :: [Named (FORMULA ())]
predefinedAxioms = let
  v1 :: VAR_DECL
v1 = Token -> SORT -> VAR_DECL
mkVarDecl (Int -> Token
mkNName 1) SORT
thing
  t1 :: TERM f
t1 = VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar VAR_DECL
v1
  in [String -> FORMULA () -> Named (FORMULA ())
forall a s. a -> s -> SenAttr s a
makeNamed "nothing in Nothing" (FORMULA () -> Named (FORMULA ()))
-> FORMULA () -> Named (FORMULA ())
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA () -> FORMULA ()
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
v1] (FORMULA () -> FORMULA ()) -> FORMULA () -> FORMULA ()
forall a b. (a -> b) -> a -> b
$ FORMULA () -> Range -> FORMULA ()
forall f. FORMULA f -> Range -> FORMULA f
Negation
            (PRED_SYMB -> [TERM ()] -> Range -> FORMULA ()
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication PRED_SYMB
noThing [TERM ()
forall f. TERM f
t1] Range
n) Range
n,
      String -> FORMULA () -> Named (FORMULA ())
forall a s. a -> s -> SenAttr s a
makeNamed "thing in Thing" (FORMULA () -> Named (FORMULA ()))
-> FORMULA () -> Named (FORMULA ())
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA () -> FORMULA ()
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
v1] (FORMULA () -> FORMULA ()) -> FORMULA () -> FORMULA ()
forall a b. (a -> b) -> a -> b
$ PRED_SYMB -> [TERM ()] -> Range -> FORMULA ()
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication
            (SORT -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name SORT
thing PRED_TYPE
classPredType Range
n) [TERM ()
forall f. TERM f
t1] Range
n]

mkNNameAux :: Int -> String
mkNNameAux :: Int -> String
mkNNameAux k :: Int
k = String
genNamePrefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ "x" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
forall a. Show a => a -> String
show Int
k

-- | Build a name
mkNName :: Int -> Token
mkNName :: Int -> Token
mkNName i :: Int
i = String -> Token
mkSimpleId (String -> Token) -> String -> Token
forall a b. (a -> b) -> a -> b
$ String
hetsPrefix String -> String -> String
forall a. [a] -> [a] -> [a]
++ Int -> String
mkNNameAux Int
i