PredefinedCASLAxioms.hs revision 94e112d16f89130a688db8b03ad3224903f5e97e
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
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified Common.AS_Annotation as AS_Anno
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified Common.Id as Id
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified Common.Lib.MapSet as MapSet
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified Common.Lib.Rel as Rel
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified CASL.AS_Basic_CASL as CBasic
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified CASL.Sign as CSign
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaimport qualified Data.Set as Set
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksalist :: Id.Id
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksalist = Id.stringToId "list"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksarel :: Id.Id
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksarel = Id.stringToId "rel"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksafun :: Id.Id
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksafun = Id.stringToId "fun"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksacons :: Id.Id
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksacons = Id.stringToId "cons"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksanil :: Id.Id
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksanil = Id.stringToId "nil"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaindividual :: Id.Id
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaindividual = Id.stringToId "individual"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksax1 :: Id.Token
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksax1 = Id.mkSimpleId "X1"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksax2 :: Id.Token
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksax2 = Id.mkSimpleId "X2"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksay1 :: Id.Token
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksay1 = Id.mkSimpleId "Y1"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksay2 :: Id.Token
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksay2 = Id.mkSimpleId "Y2"
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedernilType :: CBasic.OP_TYPE
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaedernilType = CBasic.Op_type CBasic.Total [] list Id.nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederconsType :: CBasic.OP_TYPE
94e112d16f89130a688db8b03ad3224903f5e97eChristian MaederconsType = CBasic.Op_type CBasic.Total [individual, list] list Id.nullRange
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen KuksabaseCASLAxioms :: [AS_Anno.Named CBasic.CASLFORMULA]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen KuksabaseCASLAxioms = [ga_injective_cons, ga_disjoint_nil_cons, ga_generated_list]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa-- | setting casl sign: sorts, cons, fun, nil, pred
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen KuksacaslSig :: CSign.CASLSign
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen KuksacaslSig = (CSign.emptySign ())
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa { CSign.sortRel = Rel.fromKeysSet
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa $ Set.fromList [list, individual]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CSign.opMap = MapSet.fromList
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [ (cons, [CSign.toOpType consType])
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , (fun, [CSign.mkTotOpType
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [individual, list]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa individual])
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , (nil, [CSign.toOpType nilType])]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CSign.predMap = MapSet.fromList
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [(rel, [CSign.PredType [individual, list]])]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa }
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedervy1 :: CBasic.VAR_DECL
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedervy1 = CBasic.mkVarDecl y1 individual
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedervy2 :: CBasic.VAR_DECL
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedervy2 = CBasic.mkVarDecl y2 list
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedertx1, tx2, ty1, ty2 :: CBasic.TERM f
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedertx1 = CBasic.mkVarTerm x1 individual
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maedertx2 = CBasic.mkVarTerm x2 list
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederty1 = CBasic.mkVarTerm y1 individual
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maederty2 = CBasic.mkVarTerm y2 list
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_injective_cons :: AS_Anno.Named CBasic.CASLFORMULA
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_injective_cons = AS_Anno.makeNamed "ga_injective_cons" $
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CBasic.mkForall
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [ CBasic.mkVarDecl x1 individual
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , CBasic.mkVarDecl x2 list
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , vy1
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , vy2
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder $ CBasic.mkEqv
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CBasic.mkStEq
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CBasic.mkAppl
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CBasic.mkQualOp cons consType)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [tx1, tx2]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder )
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder $ CBasic.mkAppl
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CBasic.mkQualOp cons consType)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [ty1, ty2]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa )
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder $ CBasic.conjunct
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [ CBasic.mkStEq tx1 ty1
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , CBasic.mkStEq tx2 ty2
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder ]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_disjoint_nil_cons :: AS_Anno.Named CBasic.CASLFORMULA
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_disjoint_nil_cons = AS_Anno.makeNamed "ga_disjoint_nil_cons" $
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder CBasic.mkForall [vy1, vy2]
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder $ CBasic.mkNeg
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder $ CBasic.mkStEq
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CBasic.mkAppl (CBasic.mkQualOp nil nilType) [])
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder $ CBasic.mkAppl
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder (CBasic.mkQualOp cons consType)
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [ty1, ty2]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_generated_list :: AS_Anno.Named CBasic.CASLFORMULA
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_generated_list = AS_Anno.makeNamed "ga_generated_list" $
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa CBasic.Sort_gen_ax
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ CBasic.Constraint
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa { CBasic.newSort = list
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.opSymbs =
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder [ (CBasic.mkQualOp cons consType, [-1, 0] )
94e112d16f89130a688db8b03ad3224903f5e97eChristian Maeder , (CBasic.mkQualOp nil nilType, [])
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.origSort = list
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa }
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ] True