Logic_HasCASL.hs

{-# 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 Show

instance Language HasCASL where
 description _ = 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) <> (BasicSpec l2) = BasicSpec $ l1 ++ l2
instance Monoid BasicSpec where
    mempty = BasicSpec []

instance Syntax HasCASL BasicSpec
                Symbol SymbItems SymbMapItems
      where
         parse_basic_spec HasCASL = Just $ const basicSpec
         parse_symb_items HasCASL = Just . const $ symbItems
         parse_symb_map_items HasCASL = Just . const $ symbMapItems
         toItem HasCASL = bsToItem

instance Category Env Morphism where
    ide = ideMor
    composeMorphisms = compMor
    isInclusion = isInclMor
    dom = msource
    cod = mtarget
    legal_mor = legalMor

instance Sentences HasCASL Sentence Env Morphism Symbol where
    map_sen HasCASL = mapSentence
    simplify_sen HasCASL = simplifySentence
    print_named _ = printSemiAnno (changeGlobalAnnos addBuiltins . pretty) True
        . fromLabelledSen
    sym_name HasCASL = symName
    symKind HasCASL = show . pretty . symbTypeToKind . symType
    sym_of HasCASL = symOf
    mostSymsOf HasCASL = mostSyms
    symmap_of HasCASL = morphismToSymbMap

instance StaticAnalysis HasCASL BasicSpec Sentence
               SymbItems SymbMapItems
               Env
               Morphism
               Symbol RawSymbol where
    basic_analysis HasCASL = Just basicAnalysis
    signature_union HasCASL = merge
    signatureDiff HasCASL s = return . diffEnv s
    empty_signature HasCASL = initialEnv
    induced_from_to_morphism HasCASL = inducedFromToMorphism
    induced_from_morphism HasCASL = inducedFromMorphism
    morphism_union HasCASL = morphismUnion
    is_subsig HasCASL = isSubEnv
    subsig_inclusion HasCASL s = return . mkMorphism s

    cogenerated_sign HasCASL = cogeneratedSign
    generated_sign HasCASL = generatedSign

    stat_symb_map_items HasCASL e _ = statSymbMapItems e
    stat_symb_items HasCASL = statSymbItems
    symbol_to_raw HasCASL = symbolToRaw
    id_to_raw HasCASL = idToRaw
    matches HasCASL = matchSymb

    final_union HasCASL = merge

instance SemiLatticeWithTop Sublogic where
    lub s = sublogicUp . sublogic_max s
    top = topLogic

instance SublogicName Sublogic where
    sublogicName = sublogic_name

instance MinSublogic Sublogic BasicSpec where
    minSublogic = sl_basicSpec

instance MinSublogic Sublogic Sentence where
    minSublogic = sl_sentence

instance MinSublogic Sublogic SymbItems where
    minSublogic = sl_symbItems

instance MinSublogic Sublogic SymbMapItems where
    minSublogic = sl_symbMapItems

instance MinSublogic Sublogic Env where
    minSublogic = sl_env

instance MinSublogic Sublogic Morphism where
    minSublogic = sl_morphism

instance MinSublogic Sublogic Symbol where
    minSublogic = sl_symbol

instance ProjectSublogic Sublogic BasicSpec where
    projectSublogic = error "ProjectSublogic Sublogic BasicSpec"

instance ProjectSublogicM Sublogic SymbItems where
    projectSublogicM = error " ProjectSublogicM Sublogic SymbItems"

instance ProjectSublogicM Sublogic SymbMapItems where
    projectSublogicM = error " ProjectSublogicM Sublogic SymbMapItems"

instance ProjectSublogic Sublogic Env where
    projectSublogic = error "ProjectSublogic Sublogic Env"

instance ProjectSublogic Sublogic Morphism where
    projectSublogic = error "ProjectSublogic Sublogic Morphism"

instance ProjectSublogicM Sublogic Symbol where
    projectSublogicM = error " ProjectSublogicM Sublogic Symbol"

instance Logic HasCASL Sublogic
               BasicSpec Sentence SymbItems SymbMapItems
               Env
               Morphism
               Symbol RawSymbol () where
         stability _ = Stable
         all_sublogics _ = sublogics_all
         empty_proof_tree _ = ()