{-# LANGUAGE MultiParamTypeClasses #-}
{- |
Module      :  ./HasCASL/Logic_HasCASL.hs
Description :  instance of class Logic
Copyright   :  (c) Christian Maeder and Uni Bremen 2003-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  experimental
Portability :  non-portable (imports Logic.Logic)

Here is the place where the class Logic is instantiated for HasCASL.
   Also the instances for Syntax and Category.
-}

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 _ = ()