PredefinedCASLAxioms.hs revision 800663e7e87d81818fa8e161c99687540d27f75f
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers{- |
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversModule : $Header$
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversDescription : Central datastructures for development graphs
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversLicense : GPLv2 or higher, see LICENSE.txt
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversMaintainer : till@informatik.uni-bremen.de
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversStability : provisional
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversPortability : non-portable(Logic)
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart PoetteringFixed CASL axioms needed for translation of CommonLogic to CASL
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers-}
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversmodule CommonLogic.PredefinedCASLAxioms where
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poetteringimport qualified Common.AS_Annotation as AS_Anno
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversimport qualified Common.Id as Id
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversimport qualified Common.Lib.MapSet as MapSet
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversimport qualified Common.Lib.Rel as Rel
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversimport qualified CASL.AS_Basic_CASL as CBasic
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversimport qualified CASL.Sign as CSign
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversimport qualified Data.Set as Set
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieverslist :: Id.Id
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieverslist = Id.stringToId "list"
49e942b2bc9fdedba79cd266a076ce9c9d91fc13Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversrel :: Id.Id
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversrel = Id.stringToId "rel"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversfun :: Id.Id
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversfun = Id.stringToId "fun"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieverscons :: Id.Id
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieverscons = Id.stringToId "cons"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversnil :: Id.Id
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversnil = Id.stringToId "nil"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversindividual :: Id.Id
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversindividual = Id.stringToId "individual"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversx1 :: Id.Token
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversx1 = Id.mkSimpleId "X1"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversx2 :: Id.Token
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversx2 = Id.mkSimpleId "X2"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversy1 :: Id.Token
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversy1 = Id.mkSimpleId "Y1"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversy2 :: Id.Token
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversy2 = Id.mkSimpleId "Y2"
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversnilType :: CBasic.OP_TYPE
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversnilType = CBasic.Op_type CBasic.Total [] list Id.nullRange
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversconsType :: CBasic.OP_TYPE
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversconsType = CBasic.Op_type CBasic.Total [individual, list] list Id.nullRange
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversbaseCASLAxioms :: [AS_Anno.Named CBasic.CASLFORMULA]
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieversbaseCASLAxioms = [ga_injective_cons, ga_disjoint_nil_cons, ga_generated_list]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers-- | setting casl sign: sorts, cons, fun, nil, pred
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieverscaslSig :: CSign.CASLSign
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieverscaslSig = (CSign.emptySign ())
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers { CSign.sortRel = Rel.fromKeysSet
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers $ Set.fromList [list, individual]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , CSign.opMap = MapSet.fromList
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [ (cons, [CSign.toOpType consType])
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , (fun, [CSign.mkTotOpType
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [individual, list]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers individual])
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , (nil, [CSign.toOpType nilType])]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , CSign.predMap = MapSet.fromList
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [(rel, [CSign.PredType [individual, list]])]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers }
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers-- | setting casl sign: sorts, cons, nil
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieverslistSig :: CSign.CASLSign
1822350db15b089f094a6dbd2469842ab42c1d87Kay SieverslistSig = (CSign.emptySign ())
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers { CSign.sortRel = Rel.fromKeysSet
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers $ Set.fromList [list, individual]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , CSign.opMap = MapSet.fromList
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [ (cons, [CSign.toOpType consType])
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , (nil, [CSign.toOpType nilType])]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers }
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversvy1 :: CBasic.VAR_DECL
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversvy1 = CBasic.mkVarDecl y1 individual
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversvy2 :: CBasic.VAR_DECL
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversvy2 = CBasic.mkVarDecl y2 list
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieverstx1, tx2, ty1, ty2 :: CBasic.TERM f
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieverstx1 = CBasic.mkVarTerm x1 individual
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieverstx2 = CBasic.mkVarTerm x2 list
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversty1 = CBasic.mkVarTerm y1 individual
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversty2 = CBasic.mkVarTerm y2 list
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversga_injective_cons :: AS_Anno.Named CBasic.CASLFORMULA
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversga_injective_cons = AS_Anno.makeNamed "ga_injective_cons" $
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers CBasic.mkForall
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [ CBasic.mkVarDecl x1 individual
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , CBasic.mkVarDecl x2 list
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , vy1
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , vy2
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers ]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers $ CBasic.mkEqv
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers (CBasic.mkStEq
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers (CBasic.mkAppl
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers (CBasic.mkQualOp cons consType)
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [tx1, tx2]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers )
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers $ CBasic.mkAppl
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers (CBasic.mkQualOp cons consType)
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [ty1, ty2]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers )
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers $ CBasic.conjunct
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [ CBasic.mkStEq tx1 ty1
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , CBasic.mkStEq tx2 ty2
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers ]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversga_disjoint_nil_cons :: AS_Anno.Named CBasic.CASLFORMULA
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversga_disjoint_nil_cons = AS_Anno.makeNamed "ga_disjoint_nil_cons" $
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers CBasic.mkForall [vy1, vy2]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers $ CBasic.mkNeg
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers $ CBasic.mkStEq
d200735e13c52dcfe36c0e066f9f6c2fbfb85a9cMichal Schmidt (CBasic.mkAppl (CBasic.mkQualOp nil nilType) [])
d200735e13c52dcfe36c0e066f9f6c2fbfb85a9cMichal Schmidt $ CBasic.mkAppl
d200735e13c52dcfe36c0e066f9f6c2fbfb85a9cMichal Schmidt (CBasic.mkQualOp cons consType)
d200735e13c52dcfe36c0e066f9f6c2fbfb85a9cMichal Schmidt [ty1, ty2]
d200735e13c52dcfe36c0e066f9f6c2fbfb85a9cMichal Schmidt
d200735e13c52dcfe36c0e066f9f6c2fbfb85a9cMichal Schmidtga_generated_list :: AS_Anno.Named CBasic.CASLFORMULA
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sieversga_generated_list = AS_Anno.makeNamed "ga_generated_list" $
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers CBasic.Sort_gen_ax
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [ CBasic.Constraint
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers { CBasic.newSort = list
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , CBasic.opSymbs =
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers [ (CBasic.mkQualOp cons consType, [-1, 0] )
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , (CBasic.mkQualOp nil nilType, [])
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers ]
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers , CBasic.origSort = list
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers }
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers ] True
1822350db15b089f094a6dbd2469842ab42c1d87Kay Sievers