content: {-# LANGUAGE CPP, MultiParamTypeClasses, TypeSynonymInstances
    , FlexibleInstances #-}
  {- |
  Module      :  ./VSE/Logic_VSE.hs
  Description :  the incomplete Logic instance for VSE
  Copyright   :  (c) C. Maeder, DFKI 2008
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (via Logic.Logic)
  
  morphisms and symbols need to be extended, too
  -}
  
  module VSE.Logic_VSE where
  
  import Common.DocUtils
  
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.Morphism
  import CASL.MapSentence
  import CASL.SymbolMapAnalysis
  import CASL.Parse_AS_Basic
  import CASL.Qualify
  import CASL.SymbolParser
  import CASL.SimplifySen
  import CASL.ToDoc
  import CASL.Logic_CASL () -- instance Category VSESign VSEMor
  import CASL.ColimSign
  
  import VSE.As
  import VSE.Parse
  import VSE.Ana
  import VSE.ATC_VSE ()
  import VSE.Prove (vse)
  import Logic.Logic
  
  import qualified Data.Map as Map
  
  data VSE = VSE deriving Show
  
  instance Language VSE where
   description _ =
    "VSE extends CASL by modal operators and programs."
  
  instance SignExtension Procs where
    isSubSignExtension = isSubProcsMap
  
  instance Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
      parse_basic_spec VSE = Just $ basicSpec reservedWords
      parse_symb_items VSE = Just . const $ symbItems reservedWords
      parse_symb_map_items VSE = Just . const $ symbMapItems reservedWords
  
  instance Sentences VSE Sentence VSESign VSEMor Symbol where
        map_sen VSE m = return . mapSen mapDlformula m
        sym_of VSE = symOf
        symmap_of VSE = morphismToSymbMap
        sym_name VSE = symName
        simplify_sen VSE = simplifySen minExpForm simpDlformula
        print_named VSE = printTheoryFormula
        print_sign VSE sig = let e = extendedInfo sig in
          pretty sig { opMap = diffOpMapSet (opMap sig) $ procsToOpMap e
                     , predMap = diffMapSet (predMap sig) $ procsToPredMap e }
  
  interSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
  interSigM f a b = do
    e <- f (extendedInfo a) $ extendedInfo b
    return $ interSig (const $ const e) a b
  
  instance StaticAnalysis VSE VSEBasicSpec Sentence
                 SYMB_ITEMS SYMB_MAP_ITEMS
                 VSESign
                 VSEMor
                 Symbol RawSymbol where
           basic_analysis VSE = Just basicAna
           stat_symb_map_items VSE = statSymbMapItems
           stat_symb_items VSE = statSymbItems
           signature_colimit VSE diag =
             let (sig, mmor) = signColimit diag extVSEColimit
             in return (correctSign sig, Map.map correctTarget mmor)
           qualify VSE = qualifySigExt inducedExt emptyMorExt
           symbol_to_raw VSE = symbolToRaw
           id_to_raw VSE = idToRaw
           matches VSE = CASL.Morphism.matches
  
           empty_signature VSE = emptySign emptyProcs
           signature_union VSE = addSigM unionProcs
           intersection VSE = interSigM interProcs
           morphism_union VSE = morphismUnionM retExtMap unionProcs
           final_union VSE = addSigM unionProcs
           is_subsig VSE = isSubSig isSubProcsMap
           subsig_inclusion VSE = sigInclusion emptyMorExt
           cogenerated_sign VSE s = fmap correctTarget
             . cogeneratedSign emptyMorExt s
           generated_sign VSE s = fmap correctTarget
             . generatedSign emptyMorExt s
           induced_from_morphism VSE rm = fmap correctTarget
             . inducedFromMorphismExt inducedExt (constMorphExt emptyMorExt) rm
           induced_from_to_morphism VSE rm s1 = fmap correctTarget
             . inducedFromToMorphismExt inducedExt (constMorphExt emptyMorExt)
               (\ _ _ -> return emptyMorExt) isSubProcsMap diffProcs rm s1
  
  instance Logic VSE ()
                 VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS
                 VSESign
                 VSEMor
                 Symbol RawSymbol () where
           stability VSE = Testing
           empty_proof_tree VSE = ()
           provers VSE = [vse]
  