{- |
Module      :  ./CommonLogic/PredefinedCASLAxioms.hs
Description :  Central datastructures for development graphs
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable(Logic)

Fixed CASL axioms needed for translation of CommonLogic to CASL
-}

module CommonLogic.PredefinedCASLAxioms where


import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.Id

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

import CASL.AS_Basic_CASL
import CASL.Sign

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

list :: Id
list :: Id
list = String -> Id
stringToId "list"

append :: Id
append :: Id
append = String -> Id
stringToId "append"

cons :: Id
cons :: Id
cons = String -> Id
stringToId "cons"

nil :: Id
nil :: Id
nil = String -> Id
stringToId "nil"

individual :: Id
individual :: Id
individual = String -> Id
stringToId "individual"

x1 :: Token
x1 :: Token
x1 = String -> Token
mkSimpleId "X1"

x2 :: Token
x2 :: Token
x2 = String -> Token
mkSimpleId "X2"

y1 :: Token
y1 :: Token
y1 = String -> Token
mkSimpleId "Y1"

y2 :: Token
y2 :: Token
y2 = String -> Token
mkSimpleId "Y2"

nilTypeS :: OpType
nilTypeS :: OpType
nilTypeS = [Id] -> Id -> OpType
mkTotOpType [] Id
list

consTypeS :: OpType
consTypeS :: OpType
consTypeS = [Id] -> Id -> OpType
mkTotOpType [Id
individual, Id
list] Id
list

appendTypeS :: OpType
appendTypeS :: OpType
appendTypeS = [Id] -> Id -> OpType
mkTotOpType [Id
list, Id
list] Id
list

nilType :: OP_TYPE
nilType :: OP_TYPE
nilType = OpType -> OP_TYPE
toOP_TYPE OpType
nilTypeS

consType :: OP_TYPE
consType :: OP_TYPE
consType = OpType -> OP_TYPE
toOP_TYPE OpType
consTypeS

appendType :: OP_TYPE
appendType :: OP_TYPE
appendType = OpType -> OP_TYPE
toOP_TYPE OpType
appendTypeS

baseListAxioms :: [Named CASLFORMULA]
baseListAxioms :: [Named CASLFORMULA]
baseListAxioms =
  [ Named CASLFORMULA
ga_injective_cons
  , Named CASLFORMULA
ga_disjoint_nil_cons
  , Named CASLFORMULA
ga_generated_list
  , Named CASLFORMULA
ga_nil_append
  , Named CASLFORMULA
ga_cons_append ]

-- currently a list annotation is needed in the .dol file %list [__], nil, cons
brId :: Id
brId :: Id
brId = [Token] -> Id
mkId [String -> Token
mkSimpleId "[", Token
placeTok, String -> Token
mkSimpleId "]"]

-- | setting casl sign: sorts, cons, nil, append
listSig :: CASLSign
listSig :: CASLSign
listSig = (() -> CASLSign
forall e f. e -> Sign f e
emptySign ())
               { sortRel :: Rel Id
sortRel = Set Id -> Rel Id
forall a. Ord a => Set a -> Rel a
Rel.fromKeysSet
                   (Set Id -> Rel Id) -> Set Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [Id
list, Id
individual]
               , opMap :: OpMap
opMap = [(Id, [OpType])] -> OpMap
forall a b. (Ord a, Ord b) => [(a, [b])] -> MapSet a b
MapSet.fromList
                         [ (Id
cons, [OpType
consTypeS])
                         , (Id
nil, [OpType
nilTypeS])
                         , (Id
append, [OpType
appendTypeS])
                         ]
               , globAnnos :: GlobalAnnos
globAnnos = GlobalAnnos
emptyGlobalAnnos
                     { literal_annos :: LiteralAnnos
literal_annos = LiteralAnnos
emptyLiteralAnnos
                       { list_lit :: Map Id (Id, Id)
list_lit = Id -> (Id, Id) -> Map Id (Id, Id)
forall k a. k -> a -> Map k a
Map.singleton Id
brId (Id
nil, Id
cons) }
                     , literal_map :: LiteralMap
literal_map = [(Id, LiteralType)] -> LiteralMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList
                          [ (Id
cons, Id -> Id -> LiteralType
ListCons Id
brId Id
nil)
                          , (Id
nil, Id -> LiteralType
ListNull Id
brId)]}
               }

vx2 :: VAR_DECL
vx2 :: VAR_DECL
vx2 = Token -> Id -> VAR_DECL
mkVarDecl Token
x2 Id
list

vy1 :: VAR_DECL
vy1 :: VAR_DECL
vy1 = Token -> Id -> VAR_DECL
mkVarDecl Token
y1 Id
individual

vy2 :: VAR_DECL
vy2 :: VAR_DECL
vy2 = Token -> Id -> VAR_DECL
mkVarDecl Token
y2 Id
list

tx1, tx2, ty1, ty2 :: TERM f

tx1 :: TERM f
tx1 = Token -> Id -> TERM f
forall f. Token -> Id -> TERM f
mkVarTerm Token
x1 Id
individual
tx2 :: TERM f
tx2 = Token -> Id -> TERM f
forall f. Token -> Id -> TERM f
mkVarTerm Token
x2 Id
list

ty1 :: TERM f
ty1 = Token -> Id -> TERM f
forall f. Token -> Id -> TERM f
mkVarTerm Token
y1 Id
individual
ty2 :: TERM f
ty2 = Token -> Id -> TERM f
forall f. Token -> Id -> TERM f
mkVarTerm Token
y2 Id
list

consOp :: OP_SYMB
consOp :: OP_SYMB
consOp = Id -> OP_TYPE -> OP_SYMB
mkQualOp Id
cons OP_TYPE
consType

nilOp :: OP_SYMB
nilOp :: OP_SYMB
nilOp = Id -> OP_TYPE -> OP_SYMB
mkQualOp Id
nil OP_TYPE
nilType

mkCons :: TERM f -> TERM f -> TERM f
mkCons :: TERM f -> TERM f -> TERM f
mkCons t1 :: TERM f
t1 t2 :: TERM f
t2 = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
consOp [TERM f
t1, TERM f
t2]

mkNil :: TERM f
mkNil :: TERM f
mkNil = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl OP_SYMB
nilOp []

mkAppend :: TERM f -> TERM f -> TERM f
mkAppend :: TERM f -> TERM f -> TERM f
mkAppend l1 :: TERM f
l1 l2 :: TERM f
l2 = OP_SYMB -> [TERM f] -> TERM f
forall f. OP_SYMB -> [TERM f] -> TERM f
mkAppl (Id -> OP_TYPE -> OP_SYMB
mkQualOp Id
append OP_TYPE
appendType) [TERM f
l1, TERM f
l2]

ga_injective_cons :: Named CASLFORMULA
ga_injective_cons :: Named CASLFORMULA
ga_injective_cons = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "ga_injective_cons" (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$
  [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall
    [ Token -> Id -> VAR_DECL
mkVarDecl Token
x1 Id
individual
    , VAR_DECL
vy1
    , VAR_DECL
vx2
    , VAR_DECL
vy2
    ]
    (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv
        (TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq
          (TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkCons TERM ()
forall f. TERM f
tx1 TERM ()
forall f. TERM f
tx2)
          (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkCons TERM ()
forall f. TERM f
ty1 TERM ()
forall f. TERM f
ty2
        )
        (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [CASLFORMULA] -> CASLFORMULA
forall f. [FORMULA f] -> FORMULA f
conjunct
          [ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
forall f. TERM f
tx1 TERM ()
forall f. TERM f
ty1
          , TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
forall f. TERM f
tx2 TERM ()
forall f. TERM f
ty2
          ]

ga_disjoint_nil_cons :: Named CASLFORMULA
ga_disjoint_nil_cons :: Named CASLFORMULA
ga_disjoint_nil_cons = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "ga_disjoint_nil_cons" (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$
  [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vy1, VAR_DECL
vy2] (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
forall f. FORMULA f -> FORMULA f
mkNeg (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM ()
forall f. TERM f
mkNil (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkCons TERM ()
forall f. TERM f
ty1 TERM ()
forall f. TERM f
ty2

ga_nil_append :: Named CASLFORMULA
ga_nil_append :: Named CASLFORMULA
ga_nil_append = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "ga_nil_append"
  (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vx2]
  (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkAppend TERM ()
forall f. TERM f
mkNil TERM ()
forall f. TERM f
tx2) TERM ()
forall f. TERM f
tx2

ga_cons_append :: Named CASLFORMULA
ga_cons_append :: Named CASLFORMULA
ga_cons_append = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "ga_cons_append"
  (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> CASLFORMULA -> CASLFORMULA
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL
vy1, VAR_DECL
vy2, VAR_DECL
vx2]
  (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> CASLFORMULA
forall f. TERM f -> TERM f -> FORMULA f
mkStEq (TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkAppend (TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkCons TERM ()
forall f. TERM f
ty1 TERM ()
forall f. TERM f
ty2) TERM ()
forall f. TERM f
tx2)
      (TERM () -> CASLFORMULA) -> TERM () -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkCons TERM ()
forall f. TERM f
ty1 (TERM () -> TERM ()) -> TERM () -> TERM ()
forall a b. (a -> b) -> a -> b
$ TERM () -> TERM () -> TERM ()
forall f. TERM f -> TERM f -> TERM f
mkAppend TERM ()
forall f. TERM f
ty2 TERM ()
forall f. TERM f
tx2

ga_generated_list :: Named CASLFORMULA
ga_generated_list :: Named CASLFORMULA
ga_generated_list = String -> CASLFORMULA -> Named CASLFORMULA
forall a s. a -> s -> SenAttr s a
makeNamed "ga_generated_list" (CASLFORMULA -> Named CASLFORMULA)
-> CASLFORMULA -> Named CASLFORMULA
forall a b. (a -> b) -> a -> b
$
  [Constraint] -> Bool -> CASLFORMULA
forall f. [Constraint] -> Bool -> FORMULA f
mkSort_gen_ax
    [ Constraint :: Id -> [(OP_SYMB, [Int])] -> Id -> Constraint
Constraint
      { newSort :: Id
newSort = Id
list
      , opSymbs :: [(OP_SYMB, [Int])]
opSymbs =
          [ (OP_SYMB
consOp, [-1, 0] )
          , (OP_SYMB
nilOp, [])
          ]
      , origSort :: Id
origSort = Id
list
      }
    ] Bool
True