PredefinedCASLAxioms.hs revision 0fe5514fdf12b7559c1a470cf22d89737d55b0a0
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
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
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ (cons, [CSign.mkTotOpType
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [individual, list]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa list])
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , (fun, [CSign.mkTotOpType
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [individual, list]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa individual])
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , (nil, [CSign.mkTotOpType [] list])]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CSign.predMap = MapSet.fromList
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [(rel, [CSign.PredType [individual, list]])]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa }
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_injective_cons :: AS_Anno.Named CBasic.CASLFORMULA
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_injective_cons = AS_Anno.makeNamed "ga_injective_cons" $
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa CBasic.Quantification CBasic.Universal
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ CBasic.Var_decl [x1] individual Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.Var_decl [x2] list Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.Var_decl [y1] individual Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.Var_decl [y2] list Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Equivalence
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Strong_equation
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Application
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Qual_op_name cons
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Op_type CBasic.Total [individual,list] list Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa )
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ CBasic.Qual_var (x1) individual Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.Qual_var (x2) list Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ] Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa )
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Application
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Qual_op_name cons
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Op_type CBasic.Total [individual,list] list Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa )
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ CBasic.Qual_var (y1) individual Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.Qual_var (y2) list Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ] Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ) Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Conjunction
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ CBasic.Strong_equation
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Qual_var (x1) individual Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Qual_var (y1) individual Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.Strong_equation
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Qual_var (x2) list Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Qual_var (y2) list Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ] Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ) Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ) Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_disjoint_nil_cons :: AS_Anno.Named CBasic.CASLFORMULA
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksaga_disjoint_nil_cons = AS_Anno.makeNamed "ga_disjoint_nil_cons" $
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa CBasic.Quantification CBasic.Universal
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ CBasic.Var_decl [y1] individual Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.Var_decl [y2] list Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Negation
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Strong_equation
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Application
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Qual_op_name nil
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Op_type CBasic.Total [] list Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ) [] Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa )
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Application
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Qual_op_name cons
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Op_type CBasic.Total [individual,list] list Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa )
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ CBasic.Qual_var (y1) individual Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.Qual_var (y2) list Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ] Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ) Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ) Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ) Id.nullRange
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 =
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa [ (CBasic.Qual_op_name cons
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Op_type CBasic.Total [individual,list] list Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , [-1,0] )
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , (CBasic.Qual_op_name nil
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa (CBasic.Op_type CBasic.Total [] list Id.nullRange)
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa Id.nullRange
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , [])
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ]
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa , CBasic.origSort = list
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa }
64dcce858b74fca0c1c408a249fde7a9db8a8798Eugen Kuksa ] True