{-# 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 $ symbItems reservedWords

parse_symb_map_items VSE = Just $ 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]