PredefinedCASLAxioms.hs revision 12ba16b2f63d9fabaf9f49c05d391d28b01788d7
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa{- |
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaModule : $Header$
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaDescription : Central datastructures for development graphs
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaCopyright : (c) Till Mossakowski, Uni Bremen 2002-2006
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaLicense : GPLv2 or higher, see LICENSE.txt
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaMaintainer : till@informatik.uni-bremen.de
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaStability : provisional
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaPortability : non-portable(Logic)
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen KuksaFixed CASL axioms needed for translation of CommonLogic to CASL
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa-}
0fe5514fdf12b7559c1a470cf22d89737d55b0a0Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksamodule CommonLogic.PredefinedCASLAxioms where
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederimport Common.AS_Annotation
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederimport Common.Id
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified Common.Lib.MapSet as MapSet
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified Common.Lib.Rel as Rel
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederimport CASL.AS_Basic_CASL
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederimport CASL.Sign
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified Data.Set as Set
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederlist :: Id
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederlist = stringToId "list"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederappend :: Id
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederappend = stringToId "append"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedercons :: Id
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedercons = stringToId "cons"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedernil :: Id
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedernil = stringToId "nil"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederindividual :: Id
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederindividual = stringToId "individual"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederx1 :: Token
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederx1 = mkSimpleId "X1"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederx2 :: Token
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederx2 = mkSimpleId "X2"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedery1 :: Token
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedery1 = mkSimpleId "Y1"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedery2 :: Token
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedery2 = mkSimpleId "Y2"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedernilTypeS :: OpType
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedernilTypeS = mkTotOpType [] list
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederconsTypeS :: OpType
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederconsTypeS = mkTotOpType [individual, list] list
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederappendTypeS :: OpType
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederappendTypeS = mkTotOpType [list, list] list
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedernilType :: OP_TYPE
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedernilType = toOP_TYPE nilTypeS
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederconsType :: OP_TYPE
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederconsType = toOP_TYPE consTypeS
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederappendType :: OP_TYPE
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederappendType = toOP_TYPE appendTypeS
800663e7e87d81818fa8e161c99687540d27f75fMihai Codescu
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederbaseListAxioms :: [Named CASLFORMULA]
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederbaseListAxioms =
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder [ ga_injective_cons
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , ga_disjoint_nil_cons
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , ga_generated_list
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , ga_nil_append
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , ga_cons_append ]
800663e7e87d81818fa8e161c99687540d27f75fMihai Codescu
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder-- | setting casl sign: sorts, cons, nil, append
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederlistSig :: CASLSign
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederlistSig = (emptySign ())
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder { sortRel = Rel.fromKeysSet
800663e7e87d81818fa8e161c99687540d27f75fMihai Codescu $ Set.fromList [list, individual]
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , opMap = MapSet.fromList
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder [ (cons, [consTypeS])
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , (nil, [nilTypeS])
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , (append, [appendTypeS])
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder ]
800663e7e87d81818fa8e161c99687540d27f75fMihai Codescu }
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedervx2 :: VAR_DECL
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedervx2 = mkVarDecl x2 list
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedervy1 :: VAR_DECL
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedervy1 = mkVarDecl y1 individual
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedervy2 :: VAR_DECL
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedervy2 = mkVarDecl y2 list
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedertx1, tx2, ty1, ty2 :: TERM f
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedertx1 = mkVarTerm x1 individual
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maedertx2 = mkVarTerm x2 list
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederty1 = mkVarTerm y1 individual
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederty2 = mkVarTerm y2 list
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederconsOp :: OP_SYMB
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaederconsOp = mkQualOp cons consType
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedernilOp :: OP_SYMB
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedernilOp = mkQualOp nil nilType
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedermkCons :: TERM f -> TERM f -> TERM f
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedermkCons t1 t2 = mkAppl consOp [t1, t2]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedermkNil :: TERM f
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedermkNil = mkAppl nilOp []
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedermkAppend :: TERM f -> TERM f -> TERM f
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian MaedermkAppend l1 l2 = mkAppl (mkQualOp append appendType) [l1, l2]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_injective_cons :: Named CASLFORMULA
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_injective_cons = makeNamed "ga_injective_cons" $
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder mkForall
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder [ mkVarDecl x1 individual
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , vy1
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , vx2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , vy2
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ]
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder $ mkEqv
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder (mkStEq
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder (mkCons tx1 tx2)
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder $ mkCons ty1 ty2
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder )
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder $ conjunct
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder [ mkStEq tx1 ty1
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , mkStEq tx2 ty2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder ]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_disjoint_nil_cons :: Named CASLFORMULA
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_disjoint_nil_cons = makeNamed "ga_disjoint_nil_cons" $
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder mkForall [vy1, vy2] $ mkNeg $ mkStEq mkNil $ mkCons ty1 ty2
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_nil_append :: Named CASLFORMULA
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_nil_append = makeNamed "ga_nil_append"
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder $ mkForall [vx2]
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder $ mkStEq (mkAppend mkNil tx2) tx2
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_cons_append :: Named CASLFORMULA
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_cons_append = makeNamed "ga_cons_append"
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder $ mkForall [vy1, vy2, vx2]
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder $ mkStEq (mkAppend (mkCons ty1 ty2) tx2)
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder $ mkCons ty1 $ mkAppend ty2 tx2
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_generated_list :: Named CASLFORMULA
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maederga_generated_list = makeNamed "ga_generated_list" $
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder Sort_gen_ax
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder [ Constraint
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder { newSort = list
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , opSymbs =
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder [ (consOp, [-1, 0] )
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , (nilOp, [])
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ]
12ba16b2f63d9fabaf9f49c05d391d28b01788d7Christian Maeder , origSort = list
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa }
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ] True