{-# LANGUAGE MultiParamTypeClasses #-}
module HasCASL.Logic_HasCASL (HasCASL (HasCASL)) where
import HasCASL.As
import HasCASL.Builtin
import HasCASL.Le
import HasCASL.PrintLe
import HasCASL.AsToLe
import HasCASL.RawSym
import HasCASL.SymbItem
import HasCASL.Symbol
import HasCASL.ParseItem
import HasCASL.Morphism
import HasCASL.ATC_HasCASL ()
import HasCASL.SymbolMapAnalysis
import HasCASL.Sublogic
import HasCASL.SimplifyTerm
import HasCASL.Merge
import HasCASL.ToItem
import Logic.Logic
import Common.Doc
import Common.DocUtils
import Data.Monoid ()
data HasCASL = HasCASL deriving Int -> HasCASL -> ShowS
[HasCASL] -> ShowS
HasCASL -> String
(Int -> HasCASL -> ShowS)
-> (HasCASL -> String) -> ([HasCASL] -> ShowS) -> Show HasCASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [HasCASL] -> ShowS
$cshowList :: [HasCASL] -> ShowS
show :: HasCASL -> String
$cshow :: HasCASL -> String
showsPrec :: Int -> HasCASL -> ShowS
$cshowsPrec :: Int -> HasCASL -> ShowS
Show
instance Language HasCASL where
description :: HasCASL -> String
description _ = [String] -> String
unlines
[ "HasCASL - Algebraic Specification + Functional Programming"
, " = Environment for Formal Software Development"
, "This logic is based on the partial lambda calculus and"
, " features subtyping, overloading and type class polymorphism"
, "See the HasCASL summary and further papers available at"
, " http://www.informatik.uni-bremen.de/cofi/HasCASL"
, ""
, "Abbreviations of sublogic names indicate the following feature:"
, " Sub -> with subtyping"
, " P -> with partial functions"
, " TyCl -> with simple type classes (a la Isabelle)"
, " CoCl -> with constructor classes (a la Haskell)"
, " Poly -> polymorphism without classes"
, " TyCons -> user definable type constructors"
, " HOL -> higher order logic (covers sort generation constraints)"
, " FOL -> first order logic"
, "and others like for CASL"
, ""
, "Examples:"
, " SubCFOL= -> the CASL logic without sort generation constraints"
, " PCoClTyConsHOL -> the Haskell type system fragment" ]
instance Semigroup BasicSpec where
(BasicSpec l1 :: [Annoted BasicItem]
l1) <> :: BasicSpec -> BasicSpec -> BasicSpec
<> (BasicSpec l2 :: [Annoted BasicItem]
l2) = [Annoted BasicItem] -> BasicSpec
BasicSpec ([Annoted BasicItem] -> BasicSpec)
-> [Annoted BasicItem] -> BasicSpec
forall a b. (a -> b) -> a -> b
$ [Annoted BasicItem]
l1 [Annoted BasicItem] -> [Annoted BasicItem] -> [Annoted BasicItem]
forall a. [a] -> [a] -> [a]
++ [Annoted BasicItem]
l2
instance Monoid BasicSpec where
mempty :: BasicSpec
mempty = [Annoted BasicItem] -> BasicSpec
BasicSpec []
instance Syntax HasCASL BasicSpec
Symbol SymbItems SymbMapItems
where
parse_basic_spec :: HasCASL -> Maybe (PrefixMap -> AParser st BasicSpec)
parse_basic_spec HasCASL = (PrefixMap -> AParser st BasicSpec)
-> Maybe (PrefixMap -> AParser st BasicSpec)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st BasicSpec)
-> Maybe (PrefixMap -> AParser st BasicSpec))
-> (PrefixMap -> AParser st BasicSpec)
-> Maybe (PrefixMap -> AParser st BasicSpec)
forall a b. (a -> b) -> a -> b
$ AParser st BasicSpec -> PrefixMap -> AParser st BasicSpec
forall a b. a -> b -> a
const AParser st BasicSpec
forall st. AParser st BasicSpec
basicSpec
parse_symb_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbItems)
parse_symb_items HasCASL = (PrefixMap -> AParser st SymbItems)
-> Maybe (PrefixMap -> AParser st SymbItems)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SymbItems)
-> Maybe (PrefixMap -> AParser st SymbItems))
-> (AParser st SymbItems -> PrefixMap -> AParser st SymbItems)
-> AParser st SymbItems
-> Maybe (PrefixMap -> AParser st SymbItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SymbItems -> PrefixMap -> AParser st SymbItems
forall a b. a -> b -> a
const (AParser st SymbItems -> Maybe (PrefixMap -> AParser st SymbItems))
-> AParser st SymbItems
-> Maybe (PrefixMap -> AParser st SymbItems)
forall a b. (a -> b) -> a -> b
$ AParser st SymbItems
forall st. AParser st SymbItems
symbItems
parse_symb_map_items :: HasCASL -> Maybe (PrefixMap -> AParser st SymbMapItems)
parse_symb_map_items HasCASL = (PrefixMap -> AParser st SymbMapItems)
-> Maybe (PrefixMap -> AParser st SymbMapItems)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SymbMapItems)
-> Maybe (PrefixMap -> AParser st SymbMapItems))
-> (AParser st SymbMapItems
-> PrefixMap -> AParser st SymbMapItems)
-> AParser st SymbMapItems
-> Maybe (PrefixMap -> AParser st SymbMapItems)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SymbMapItems -> PrefixMap -> AParser st SymbMapItems
forall a b. a -> b -> a
const (AParser st SymbMapItems
-> Maybe (PrefixMap -> AParser st SymbMapItems))
-> AParser st SymbMapItems
-> Maybe (PrefixMap -> AParser st SymbMapItems)
forall a b. (a -> b) -> a -> b
$ AParser st SymbMapItems
forall st. AParser st SymbMapItems
symbMapItems
toItem :: HasCASL -> BasicSpec -> Item
toItem HasCASL = BasicSpec -> Item
bsToItem
instance Category Env Morphism where
ide :: Env -> Morphism
ide = Env -> Morphism
ideMor
composeMorphisms :: Morphism -> Morphism -> Result Morphism
composeMorphisms = Morphism -> Morphism -> Result Morphism
compMor
isInclusion :: Morphism -> Bool
isInclusion = Morphism -> Bool
isInclMor
dom :: Morphism -> Env
dom = Morphism -> Env
msource
cod :: Morphism -> Env
cod = Morphism -> Env
mtarget
legal_mor :: Morphism -> Result ()
legal_mor = Morphism -> Result ()
legalMor
instance Sentences HasCASL Sentence Env Morphism Symbol where
map_sen :: HasCASL -> Morphism -> Sentence -> Result Sentence
map_sen HasCASL = Morphism -> Sentence -> Result Sentence
mapSentence
simplify_sen :: HasCASL -> Env -> Sentence -> Sentence
simplify_sen HasCASL = Env -> Sentence -> Sentence
simplifySentence
print_named :: HasCASL -> Named Sentence -> Doc
print_named _ = (Sentence -> Doc) -> Bool -> Annoted Sentence -> Doc
forall a. (a -> Doc) -> Bool -> Annoted a -> Doc
printSemiAnno ((GlobalAnnos -> GlobalAnnos) -> Doc -> Doc
changeGlobalAnnos GlobalAnnos -> GlobalAnnos
addBuiltins (Doc -> Doc) -> (Sentence -> Doc) -> Sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sentence -> Doc
forall a. Pretty a => a -> Doc
pretty) Bool
True
(Annoted Sentence -> Doc)
-> (Named Sentence -> Annoted Sentence) -> Named Sentence -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named Sentence -> Annoted Sentence
forall s. Named s -> Annoted s
fromLabelledSen
sym_name :: HasCASL -> Symbol -> Id
sym_name HasCASL = Symbol -> Id
symName
symKind :: HasCASL -> Symbol -> String
symKind HasCASL = Doc -> String
forall a. Show a => a -> String
show (Doc -> String) -> (Symbol -> Doc) -> Symbol -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbKind -> Doc
forall a. Pretty a => a -> Doc
pretty (SymbKind -> Doc) -> (Symbol -> SymbKind) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbolType -> SymbKind
symbTypeToKind (SymbolType -> SymbKind)
-> (Symbol -> SymbolType) -> Symbol -> SymbKind
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbolType
symType
sym_of :: HasCASL -> Env -> [Set Symbol]
sym_of HasCASL = Env -> [Set Symbol]
symOf
mostSymsOf :: HasCASL -> Env -> [Symbol]
mostSymsOf HasCASL = Env -> [Symbol]
mostSyms
symmap_of :: HasCASL -> Morphism -> EndoMap Symbol
symmap_of HasCASL = Morphism -> EndoMap Symbol
morphismToSymbMap
instance StaticAnalysis HasCASL BasicSpec Sentence
SymbItems SymbMapItems
Env
Morphism
Symbol RawSymbol where
basic_analysis :: HasCASL
-> Maybe
((BasicSpec, Env, GlobalAnnos)
-> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]))
basic_analysis HasCASL = ((BasicSpec, Env, GlobalAnnos)
-> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]))
-> Maybe
((BasicSpec, Env, GlobalAnnos)
-> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence]))
forall a. a -> Maybe a
Just (BasicSpec, Env, GlobalAnnos)
-> Result (BasicSpec, ExtSign Env Symbol, [Named Sentence])
basicAnalysis
signature_union :: HasCASL -> Env -> Env -> Result Env
signature_union HasCASL = Env -> Env -> Result Env
merge
signatureDiff :: HasCASL -> Env -> Env -> Result Env
signatureDiff HasCASL s :: Env
s = Env -> Result Env
forall (m :: * -> *) a. Monad m => a -> m a
return (Env -> Result Env) -> (Env -> Env) -> Env -> Result Env
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Env -> Env
diffEnv Env
s
empty_signature :: HasCASL -> Env
empty_signature HasCASL = Env
initialEnv
induced_from_to_morphism :: HasCASL
-> EndoMap RawSymbol
-> ExtSign Env Symbol
-> ExtSign Env Symbol
-> Result Morphism
induced_from_to_morphism HasCASL = EndoMap RawSymbol
-> ExtSign Env Symbol -> ExtSign Env Symbol -> Result Morphism
inducedFromToMorphism
induced_from_morphism :: HasCASL -> EndoMap RawSymbol -> Env -> Result Morphism
induced_from_morphism HasCASL = EndoMap RawSymbol -> Env -> Result Morphism
inducedFromMorphism
morphism_union :: HasCASL -> Morphism -> Morphism -> Result Morphism
morphism_union HasCASL = Morphism -> Morphism -> Result Morphism
morphismUnion
is_subsig :: HasCASL -> Env -> Env -> Bool
is_subsig HasCASL = Env -> Env -> Bool
isSubEnv
subsig_inclusion :: HasCASL -> Env -> Env -> Result Morphism
subsig_inclusion HasCASL s :: Env
s = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism)
-> (Env -> Morphism) -> Env -> Result Morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Env -> Env -> Morphism
mkMorphism Env
s
cogenerated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism
cogenerated_sign HasCASL = Set Symbol -> Env -> Result Morphism
cogeneratedSign
generated_sign :: HasCASL -> Set Symbol -> Env -> Result Morphism
generated_sign HasCASL = Set Symbol -> Env -> Result Morphism
generatedSign
stat_symb_map_items :: HasCASL
-> Env -> Maybe Env -> [SymbMapItems] -> Result (EndoMap RawSymbol)
stat_symb_map_items HasCASL e :: Env
e _ = Env -> [SymbMapItems] -> Result (EndoMap RawSymbol)
statSymbMapItems Env
e
stat_symb_items :: HasCASL -> Env -> [SymbItems] -> Result [RawSymbol]
stat_symb_items HasCASL = Env -> [SymbItems] -> Result [RawSymbol]
statSymbItems
symbol_to_raw :: HasCASL -> Symbol -> RawSymbol
symbol_to_raw HasCASL = Symbol -> RawSymbol
symbolToRaw
id_to_raw :: HasCASL -> Id -> RawSymbol
id_to_raw HasCASL = Id -> RawSymbol
idToRaw
matches :: HasCASL -> Symbol -> RawSymbol -> Bool
matches HasCASL = Symbol -> RawSymbol -> Bool
matchSymb
final_union :: HasCASL -> Env -> Env -> Result Env
final_union HasCASL = Env -> Env -> Result Env
merge
instance SemiLatticeWithTop Sublogic where
lub :: Sublogic -> Sublogic -> Sublogic
lub s :: Sublogic
s = Sublogic -> Sublogic
sublogicUp (Sublogic -> Sublogic)
-> (Sublogic -> Sublogic) -> Sublogic -> Sublogic
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sublogic -> Sublogic -> Sublogic
sublogic_max Sublogic
s
top :: Sublogic
top = Sublogic
topLogic
instance SublogicName Sublogic where
sublogicName :: Sublogic -> String
sublogicName = Sublogic -> String
sublogic_name
instance MinSublogic Sublogic BasicSpec where
minSublogic :: BasicSpec -> Sublogic
minSublogic = BasicSpec -> Sublogic
sl_basicSpec
instance MinSublogic Sublogic Sentence where
minSublogic :: Sentence -> Sublogic
minSublogic = Sentence -> Sublogic
sl_sentence
instance MinSublogic Sublogic SymbItems where
minSublogic :: SymbItems -> Sublogic
minSublogic = SymbItems -> Sublogic
sl_symbItems
instance MinSublogic Sublogic SymbMapItems where
minSublogic :: SymbMapItems -> Sublogic
minSublogic = SymbMapItems -> Sublogic
sl_symbMapItems
instance MinSublogic Sublogic Env where
minSublogic :: Env -> Sublogic
minSublogic = Env -> Sublogic
sl_env
instance MinSublogic Sublogic Morphism where
minSublogic :: Morphism -> Sublogic
minSublogic = Morphism -> Sublogic
sl_morphism
instance MinSublogic Sublogic Symbol where
minSublogic :: Symbol -> Sublogic
minSublogic = Symbol -> Sublogic
sl_symbol
instance ProjectSublogic Sublogic BasicSpec where
projectSublogic :: Sublogic -> BasicSpec -> BasicSpec
projectSublogic = String -> Sublogic -> BasicSpec -> BasicSpec
forall a. HasCallStack => String -> a
error "ProjectSublogic Sublogic BasicSpec"
instance ProjectSublogicM Sublogic SymbItems where
projectSublogicM :: Sublogic -> SymbItems -> Maybe SymbItems
projectSublogicM = String -> Sublogic -> SymbItems -> Maybe SymbItems
forall a. HasCallStack => String -> a
error " ProjectSublogicM Sublogic SymbItems"
instance ProjectSublogicM Sublogic SymbMapItems where
projectSublogicM :: Sublogic -> SymbMapItems -> Maybe SymbMapItems
projectSublogicM = String -> Sublogic -> SymbMapItems -> Maybe SymbMapItems
forall a. HasCallStack => String -> a
error " ProjectSublogicM Sublogic SymbMapItems"
instance ProjectSublogic Sublogic Env where
projectSublogic :: Sublogic -> Env -> Env
projectSublogic = String -> Sublogic -> Env -> Env
forall a. HasCallStack => String -> a
error "ProjectSublogic Sublogic Env"
instance ProjectSublogic Sublogic Morphism where
projectSublogic :: Sublogic -> Morphism -> Morphism
projectSublogic = String -> Sublogic -> Morphism -> Morphism
forall a. HasCallStack => String -> a
error "ProjectSublogic Sublogic Morphism"
instance ProjectSublogicM Sublogic Symbol where
projectSublogicM :: Sublogic -> Symbol -> Maybe Symbol
projectSublogicM = String -> Sublogic -> Symbol -> Maybe Symbol
forall a. HasCallStack => String -> a
error " ProjectSublogicM Sublogic Symbol"
instance Logic HasCASL Sublogic
BasicSpec Sentence SymbItems SymbMapItems
Env
Morphism
Symbol RawSymbol () where
stability :: HasCASL -> Stability
stability _ = Stability
Stable
all_sublogics :: HasCASL -> [Sublogic]
all_sublogics _ = [Sublogic]
sublogics_all
empty_proof_tree :: HasCASL -> ()
empty_proof_tree _ = ()