Logic_CASL.hs revision 8b52f992f2f7a0c4fa6e3692cf868a6baadaa69b
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach{-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances
8267b99c0d7a187abe6f87ad50530dc08f5d1cdcAndy Gimblett , FlexibleInstances #-}
e85b224577b78d08ba5c39fe9dcc2e53995454a2Christian MaederModule : $Header$
97018cf5fa25b494adffd7e9b4e87320dae6bf47Christian MaederDescription : Instance of class Logic for the CASL logic
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachCopyright : (c) Klaus Luettich, Uni Bremen 2002-2005
b4fbc96e05117839ca409f5f20f97b3ac872d1edTill MossakowskiLicense : GPLv2 or higher, see LICENSE.txt
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachMaintainer : till@informatik.uni-bremen.de
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachStability : provisional
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimblettPortability : non-portable (imports Logic.Logic)
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus RoggenbachInstance of class Logic for the CASL logic
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach Also the instances for Syntax and Category.
1538a6e8d77301d6de757616ffc69ee61f1482e4Andy Gimblettimport CASL.ToItem (bsToItem)
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport CASL.CCC.OnePoint () -- currently unused
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettimport qualified CASL.OMDocImport as OMI
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblett#ifdef UNI_PACKAGE
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblettdata CASL = CASL deriving Show
41486a487c9b065d4d9d1a8adf63c00925cd455bAndy Gimblettinstance Language CASL where
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett description _ = unlines
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett [ "CASL - the Common algebraic specification language"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett , "This logic is subsorted partial first-order logic"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett , " with sort generation constraints"
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , "See the CASL User Manual, LNCS 2900, Springer Verlag"
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett , "and the CASL Reference Manual, LNCS 2960, Springer Verlag"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett , "Abbreviations of sublogic names indicate the following feature:"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " Sub -> with subsorting"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett , " Sul -> with a locally filtered subsort relation"
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett , " P -> with partial functions"
eeaf0a8a1dc535d105904a2190f26c0835ecf429Andy Gimblett , " C -> with sort generation constraints"
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , " eC -> C without renamings"
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , " sC -> C with injective constructors"
61051521e4d82769a47f23aecb5fb477de47d534Andy Gimblett , " seC -> sC and eC"
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , " FOL -> first order logic"
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , " FOAlg -> FOL without predicates"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " Horn -> positive conditional logic"
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , " GHorn -> generalized Horn"
e771539425f4a0abef9f94cf4b63690f3603f682Andy Gimblett , " GCond -> GHorn without predicates"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " Cond -> Horn without predicates"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " Atom -> atomic logic"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " Eq -> Atom without predicates"
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , " = -> with equality"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , "Examples:"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " SubPCFOL= -> the CASL logic itself"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " FOAlg= -> first order algebra (without predicates)"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " SubPHorn= -> the positive conditional fragement of CASL"
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett , " SubPAtom -> the atomic subset of CASL"
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett , " SubPCAtom -> SubPAtom with sort generation constraints"
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett , " Eq= -> classical equational logic" ]
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimbletttype CASLBasicSpec = BASIC_SPEC () () ()
90047eafd2de482c67bcd13103c6064e9b0cb254Andy GimbletttrueC :: a -> b -> Bool
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy GimbletttrueC _ _ = True
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettinstance (Ord f, Ord e, Ord m, MorphismExtension e m) =>
90047eafd2de482c67bcd13103c6064e9b0cb254Andy Gimblett Category (Sign f e) (Morphism f e m) where
a79fe3aad8743ea57e473ea5f66a723244cb9c0eMarkus Roggenbach ide sig = idMor (ideMorphismExtension $ extendedInfo sig) sig
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett inverse = inverseMorphism inverseMorphismExtension
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett composeMorphisms m1 =
af745a4a6cb26002e55b69f90d837fe9c6176d4bAndy Gimblett composeM (composeMorphismExtension $ extendedInfo $ msource m1) m1
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett dom = msource
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett cod = mtarget
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett isInclusion = isInclusionMorphism isInclusionMorphismExtension
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett legal_mor = legalMor
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett-- abstract syntax, parsing (and printing)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettinstance Syntax CASL CASLBasicSpec
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett SYMB_ITEMS SYMB_MAP_ITEMS
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett parse_basic_spec CASL = Just $ basicSpec []
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett parse_symb_items CASL = Just $ symbItems []
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett parse_symb_map_items CASL = Just $ symbMapItems []
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett toItem CASL = bsToItem
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett-- lattices (for sublogics)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettinstance Lattice a => SemiLatticeWithTop (CASL_SL a) where
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett join = sublogics_max
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettclass Lattice a => MinSL a f where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett minSL :: f -> CASL_SL a
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance MinSL () () where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett minSL () = bottom
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettclass NameSL a where
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett nameSL :: a -> String
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettinstance NameSL () where
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett nameSL _ = ""
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettclass Lattice a => ProjForm a f where
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett projForm :: CASL_SL a -> f -> Maybe (FORMULA f)
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettinstance Lattice a => ProjForm a () where
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett projForm _ = Just . ExtFORMULA
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettclass (Lattice a, ProjForm a f) => ProjSigItem a s f where
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett projSigItems :: CASL_SL a -> s -> (Maybe (SIG_ITEMS s f), [SORT])
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettinstance (Lattice a, ProjForm a f) => ProjSigItem a () f where
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett projSigItems _ s = (Just $ Ext_SIG_ITEMS s, [])
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettclass (Lattice a, ProjForm a f) => ProjBasic a b s f where
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblett projBasicItems :: CASL_SL a -> b -> (Maybe (BASIC_ITEMS b s f), [SORT])
d326dac41dadbe2b84bb7021cbfd91f4dd4a19bcAndy Gimblettinstance (Lattice a, ProjForm a f, ProjSigItem a s f)
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett => ProjBasic a () s f where
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett projBasicItems _ b = (Just $ Ext_BASIC_ITEMS b, [])
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettinstance (NameSL a) => SublogicName (CASL_SL a) where
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblett sublogicName = sublogics_name nameSL
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance (MinSL a f, MinSL a s, MinSL a b) =>
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett MinSublogic (CASL_SL a) (BASIC_SPEC b s f) where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett minSublogic = sl_basic_spec minSL minSL minSL
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance MinSL a f => MinSublogic (CASL_SL a) (FORMULA f) where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett minSublogic = sl_sentence minSL
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance Lattice a => MinSublogic (CASL_SL a) SYMB_ITEMS where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett minSublogic = sl_symb_items
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance Lattice a => MinSublogic (CASL_SL a) SYMB_MAP_ITEMS where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett minSublogic = sl_symb_map_items
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblettinstance Lattice a => MinSublogic (CASL_SL a) (Sign f e) where
e95030058b77cb83593c85aa4c506caf154f63b7Andy Gimblett minSublogic = sl_sign
e8c03c10d7987b223a9f6bfd5c0c54da21da5b86Andy Gimblettinstance Lattice a => MinSublogic (CASL_SL a) (Morphism f e m) where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett minSublogic = sl_morphism
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance Lattice a => MinSublogic (CASL_SL a) Symbol where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett minSublogic = sl_symbol
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance (MinSL a f, MinSL a s, MinSL a b, ProjForm a f,
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ProjSigItem a s f, ProjBasic a b s f) =>
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ProjectSublogic (CASL_SL a) (BASIC_SPEC b s f) where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett projectSublogic = pr_basic_spec projBasicItems projSigItems projForm
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance Lattice a => ProjectSublogicM (CASL_SL a) SYMB_ITEMS where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett projectSublogicM = pr_symb_items
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance Lattice a => ProjectSublogicM (CASL_SL a) SYMB_MAP_ITEMS where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett projectSublogicM = pr_symb_map_items
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance Lattice a => ProjectSublogic (CASL_SL a) (Sign f e) where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett projectSublogic = pr_sign
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance Lattice a => ProjectSublogic (CASL_SL a) (Morphism f e m) where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett projectSublogic = pr_morphism
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance Lattice a => ProjectSublogicM (CASL_SL a) Symbol where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett projectSublogicM = pr_symbol
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance Sentences CASL CASLFORMULA CASLSign CASLMor Symbol where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett map_sen CASL m = return . mapSen (const id) m
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett negation CASL = negateFormula
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett sym_of CASL = symOf
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett symmap_of CASL = morphismToSymbMap
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett sym_name CASL = symName
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett simplify_sen CASL = simplifyCASLSen
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett print_named CASL = printTheoryFormula
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance StaticAnalysis CASL CASLBasicSpec CASLFORMULA
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett SYMB_ITEMS SYMB_MAP_ITEMS
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett Symbol RawSymbol where
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett basic_analysis CASL = Just basicCASLAnalysis
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett stat_symb_map_items CASL = statSymbMapItems
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett stat_symb_items CASL = statSymbItems
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett signature_colimit CASL diag = return $ signColimit diag extCASLColimit
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett quotient_term_algebra CASL = quotientTermAlgebra
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ensures_amalgamability CASL (opts, diag, sink, desc) =
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett ensuresAmalgamability opts diag sink desc
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett qualify CASL = qualifySig
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett symbol_to_raw CASL = symbolToRaw
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett id_to_raw CASL = idToRaw
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett is_transportable CASL = isSortInjective
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett is_injective CASL = isInjective
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett empty_signature CASL = emptySign ()
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett add_symb_to_sign CASL = addSymbToSign
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett signature_union CASL s = return . addSig const s
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett intersection CASL s = return . interSig const s
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett morphism_union CASL = morphismUnion (const id) const
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett final_union CASL = finalUnion const
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett is_subsig CASL = isSubSig trueC
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett subsig_inclusion CASL = sigInclusion ()
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett cogenerated_sign CASL = cogeneratedSign ()
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett generated_sign CASL = generatedSign ()
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett induced_from_morphism CASL = inducedFromMorphism ()
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett induced_from_to_morphism CASL = inducedFromToMorphism () trueC const
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett theory_to_taxonomy CASL = convTaxo
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett-- convSignOMDoc CASL = someFunctionFromOMDocFolderNowInCASLFolder
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblettinstance Logic CASL CASL_Sublogics
d9e78002fb0bf01a9b72d3d3415fdf9790bdfee8Andy Gimblett CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
omdocToSen CASL = OMI.omdocToSen
omdocToSym CASL = OMI.omdocToSym
addOMadtToTheory CASL = OMI.addOMadtToTheory
addOmdocToTheory CASL = OMI.addOmdocToTheory