{-# 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 Int -> VSE -> ShowS
[VSE] -> ShowS
VSE -> String
(Int -> VSE -> ShowS)
-> (VSE -> String) -> ([VSE] -> ShowS) -> Show VSE
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [VSE] -> ShowS
$cshowList :: [VSE] -> ShowS
show :: VSE -> String
$cshow :: VSE -> String
showsPrec :: Int -> VSE -> ShowS
$cshowsPrec :: Int -> VSE -> ShowS
Show

instance Language VSE where
 description :: VSE -> String
description _ =
  "VSE extends CASL by modal operators and programs."

instance SignExtension Procs where
  isSubSignExtension :: Procs -> Procs -> Bool
isSubSignExtension = Procs -> Procs -> Bool
isSubProcsMap

instance Syntax VSE VSEBasicSpec Symbol SYMB_ITEMS SYMB_MAP_ITEMS where
    parse_basic_spec :: VSE -> Maybe (PrefixMap -> AParser st VSEBasicSpec)
parse_basic_spec VSE = (PrefixMap -> AParser st VSEBasicSpec)
-> Maybe (PrefixMap -> AParser st VSEBasicSpec)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st VSEBasicSpec)
 -> Maybe (PrefixMap -> AParser st VSEBasicSpec))
-> (PrefixMap -> AParser st VSEBasicSpec)
-> Maybe (PrefixMap -> AParser st VSEBasicSpec)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st VSEBasicSpec
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
reservedWords
    parse_symb_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items VSE = (PrefixMap -> AParser st SYMB_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> (AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS)
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_ITEMS -> PrefixMap -> AParser st SYMB_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_ITEMS))
-> AParser st SYMB_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_ITEMS
forall st. [String] -> AParser st SYMB_ITEMS
symbItems [String]
reservedWords
    parse_symb_map_items :: VSE -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items VSE = (PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st SYMB_MAP_ITEMS)
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> (AParser st SYMB_MAP_ITEMS
    -> PrefixMap -> AParser st SYMB_MAP_ITEMS)
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. AParser st SYMB_MAP_ITEMS -> PrefixMap -> AParser st SYMB_MAP_ITEMS
forall a b. a -> b -> a
const (AParser st SYMB_MAP_ITEMS
 -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS))
-> AParser st SYMB_MAP_ITEMS
-> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
forall a b. (a -> b) -> a -> b
$ [String] -> AParser st SYMB_MAP_ITEMS
forall st. [String] -> AParser st SYMB_MAP_ITEMS
symbMapItems [String]
reservedWords

instance Sentences VSE Sentence VSESign VSEMor Symbol where
      map_sen :: VSE -> VSEMor -> Sentence -> Result Sentence
map_sen VSE m :: VSEMor
m = Sentence -> Result Sentence
forall (m :: * -> *) a. Monad m => a -> m a
return (Sentence -> Result Sentence)
-> (Sentence -> Sentence) -> Sentence -> Result Sentence
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen Dlformula Procs VSEMorExt -> VSEMor -> Sentence -> Sentence
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen MapSen Dlformula Procs VSEMorExt
mapDlformula VSEMor
m
      sym_of :: VSE -> VSESign -> [Set Symbol]
sym_of VSE = VSESign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      symmap_of :: VSE -> VSEMor -> EndoMap Symbol
symmap_of VSE = VSEMor -> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: VSE -> Symbol -> Id
sym_name VSE = Symbol -> Id
symName
      simplify_sen :: VSE -> VSESign -> Sentence -> Sentence
simplify_sen VSE = Min Dlformula Procs
-> (VSESign -> Dlformula -> Dlformula)
-> VSESign
-> Sentence
-> Sentence
forall f e.
(FormExtension f, TermExtension f) =>
Min f e
-> (Sign f e -> f -> f) -> Sign f e -> FORMULA f -> FORMULA f
simplifySen Min Dlformula Procs
minExpForm VSESign -> Dlformula -> Dlformula
simpDlformula
      print_named :: VSE -> Named Sentence -> Doc
print_named VSE = Named Sentence -> Doc
forall f. FormExtension f => Named (FORMULA f) -> Doc
printTheoryFormula
      print_sign :: VSE -> VSESign -> Doc
print_sign VSE sig :: VSESign
sig = let e :: Procs
e = VSESign -> Procs
forall f e. Sign f e -> e
extendedInfo VSESign
sig in
        VSESign -> Doc
forall a. Pretty a => a -> Doc
pretty VSESign
sig { opMap :: OpMap
opMap = OpMap -> OpMap -> OpMap
diffOpMapSet (VSESign -> OpMap
forall f e. Sign f e -> OpMap
opMap VSESign
sig) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Procs -> OpMap
procsToOpMap Procs
e
                   , predMap :: PredMap
predMap = PredMap -> PredMap -> PredMap
diffMapSet (VSESign -> PredMap
forall f e. Sign f e -> PredMap
predMap VSESign
sig) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Procs -> PredMap
procsToPredMap Procs
e }

interSigM :: Monad m => (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
interSigM :: (e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
interSigM f :: e -> e -> m e
f a :: Sign f e
a b :: Sign f e
b = do
  e
e <- e -> e -> m e
f (Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
a) (e -> m e) -> e -> m e
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
b
  Sign f e -> m (Sign f e)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign f e -> m (Sign f e)) -> Sign f e -> m (Sign f e)
forall a b. (a -> b) -> a -> b
$ (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
interSig ((e -> e) -> e -> e -> e
forall a b. a -> b -> a
const ((e -> e) -> e -> e -> e) -> (e -> e) -> e -> e -> e
forall a b. (a -> b) -> a -> b
$ e -> e -> e
forall a b. a -> b -> a
const e
e) Sign f e
a Sign f e
b

instance StaticAnalysis VSE VSEBasicSpec Sentence
               SYMB_ITEMS SYMB_MAP_ITEMS
               VSESign
               VSEMor
               Symbol RawSymbol where
         basic_analysis :: VSE
-> Maybe
     ((VSEBasicSpec, VSESign, GlobalAnnos)
      -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]))
basic_analysis VSE = ((VSEBasicSpec, VSESign, GlobalAnnos)
 -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]))
-> Maybe
     ((VSEBasicSpec, VSESign, GlobalAnnos)
      -> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence]))
forall a. a -> Maybe a
Just (VSEBasicSpec, VSESign, GlobalAnnos)
-> Result (VSEBasicSpec, ExtSign VSESign Symbol, [Named Sentence])
basicAna
         stat_symb_map_items :: VSE
-> VSESign
-> Maybe VSESign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items VSE = VSESign
-> Maybe VSESign -> [SYMB_MAP_ITEMS] -> Result (EndoMap RawSymbol)
forall f e.
Sign f e
-> Maybe (Sign f e)
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
statSymbMapItems
         stat_symb_items :: VSE -> VSESign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items VSE = VSESign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems
         signature_colimit :: VSE -> Gr VSESign (Int, VSEMor) -> Result (VSESign, Map Int VSEMor)
signature_colimit VSE diag :: Gr VSESign (Int, VSEMor)
diag =
           let (sig :: VSESign
sig, mmor :: Map Int VSEMor
mmor) = Gr VSESign (Int, VSEMor)
-> (Gr Procs (Int, VSEMorExt)
    -> Map Int VSEMor -> (Procs, Map Int VSEMorExt))
-> (VSESign, Map Int VSEMor)
forall f e m.
Category (Sign f e) (Morphism f e m) =>
Gr (Sign f e) (Int, Morphism f e m)
-> (Gr e (Int, m) -> Map Int (Morphism f e m) -> (e, Map Int m))
-> (Sign f e, Map Int (Morphism f e m))
signColimit Gr VSESign (Int, VSEMor)
diag Gr Procs (Int, VSEMorExt)
-> Map Int VSEMor -> (Procs, Map Int VSEMorExt)
extVSEColimit
           in (VSESign, Map Int VSEMor) -> Result (VSESign, Map Int VSEMor)
forall (m :: * -> *) a. Monad m => a -> m a
return (VSESign -> VSESign
forall f. Sign f Procs -> Sign f Procs
correctSign VSESign
sig, (VSEMor -> VSEMor) -> Map Int VSEMor -> Map Int VSEMor
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map VSEMor -> VSEMor
forall f. Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
correctTarget Map Int VSEMor
mmor)
         qualify :: VSE
-> SIMPLE_ID
-> LibName
-> VSEMor
-> VSESign
-> Result (VSEMor, [Named Sentence])
qualify VSE = InducedSign Dlformula Procs VSEMorExt Procs
-> VSEMorExt
-> SIMPLE_ID
-> LibName
-> VSEMor
-> VSESign
-> Result (VSEMor, [Named Sentence])
forall f e m.
InducedSign f e m e
-> m
-> SIMPLE_ID
-> LibName
-> Morphism f e m
-> Sign f e
-> Result (Morphism f e m, [Named (FORMULA f)])
qualifySigExt InducedSign Dlformula Procs VSEMorExt Procs
forall f. InducedSign f Procs VSEMorExt Procs
inducedExt VSEMorExt
forall e. DefMorExt e
emptyMorExt
         symbol_to_raw :: VSE -> Symbol -> RawSymbol
symbol_to_raw VSE = Symbol -> RawSymbol
symbolToRaw
         id_to_raw :: VSE -> Id -> RawSymbol
id_to_raw VSE = Id -> RawSymbol
idToRaw
         matches :: VSE -> Symbol -> RawSymbol -> Bool
matches VSE = Symbol -> RawSymbol -> Bool
CASL.Morphism.matches

         empty_signature :: VSE -> VSESign
empty_signature VSE = Procs -> VSESign
forall e f. e -> Sign f e
emptySign Procs
emptyProcs
         signature_union :: VSE -> VSESign -> VSESign -> Result VSESign
signature_union VSE = (Procs -> Procs -> Result Procs)
-> VSESign -> VSESign -> Result VSESign
forall (m :: * -> *) e f.
Monad m =>
(e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
addSigM Procs -> Procs -> Result Procs
unionProcs
         intersection :: VSE -> VSESign -> VSESign -> Result VSESign
intersection VSE = (Procs -> Procs -> Result Procs)
-> VSESign -> VSESign -> Result VSESign
forall (m :: * -> *) e f.
Monad m =>
(e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
interSigM Procs -> Procs -> Result Procs
interProcs
         morphism_union :: VSE -> VSEMor -> VSEMor -> Result VSEMor
morphism_union VSE = (VSEMor -> VSEMor -> Result VSEMorExt)
-> (Procs -> Procs -> Result Procs)
-> VSEMor
-> VSEMor
-> Result VSEMor
forall f e m.
(Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Result e)
-> Morphism f e m
-> Morphism f e m
-> Result (Morphism f e m)
morphismUnionM VSEMor -> VSEMor -> Result VSEMorExt
forall b f e m. b -> Morphism f e m -> Result m
retExtMap Procs -> Procs -> Result Procs
unionProcs
         final_union :: VSE -> VSESign -> VSESign -> Result VSESign
final_union VSE = (Procs -> Procs -> Result Procs)
-> VSESign -> VSESign -> Result VSESign
forall (m :: * -> *) e f.
Monad m =>
(e -> e -> m e) -> Sign f e -> Sign f e -> m (Sign f e)
addSigM Procs -> Procs -> Result Procs
unionProcs
         is_subsig :: VSE -> VSESign -> VSESign -> Bool
is_subsig VSE = (Procs -> Procs -> Bool) -> VSESign -> VSESign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig Procs -> Procs -> Bool
isSubProcsMap
         subsig_inclusion :: VSE -> VSESign -> VSESign -> Result VSEMor
subsig_inclusion VSE = VSEMorExt -> VSESign -> VSESign -> Result VSEMor
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion VSEMorExt
forall e. DefMorExt e
emptyMorExt
         cogenerated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor
cogenerated_sign VSE s :: Set Symbol
s = (VSEMor -> VSEMor) -> Result VSEMor -> Result VSEMor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VSEMor -> VSEMor
forall f. Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
correctTarget
           (Result VSEMor -> Result VSEMor)
-> (VSESign -> Result VSEMor) -> VSESign -> Result VSEMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VSEMorExt -> Set Symbol -> VSESign -> Result VSEMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign VSEMorExt
forall e. DefMorExt e
emptyMorExt Set Symbol
s
         generated_sign :: VSE -> Set Symbol -> VSESign -> Result VSEMor
generated_sign VSE s :: Set Symbol
s = (VSEMor -> VSEMor) -> Result VSEMor -> Result VSEMor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VSEMor -> VSEMor
forall f. Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
correctTarget
           (Result VSEMor -> Result VSEMor)
-> (VSESign -> Result VSEMor) -> VSESign -> Result VSEMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VSEMorExt -> Set Symbol -> VSESign -> Result VSEMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign VSEMorExt
forall e. DefMorExt e
emptyMorExt Set Symbol
s
         induced_from_morphism :: VSE -> EndoMap RawSymbol -> VSESign -> Result VSEMor
induced_from_morphism VSE rm :: EndoMap RawSymbol
rm = (VSEMor -> VSEMor) -> Result VSEMor -> Result VSEMor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VSEMor -> VSEMor
forall f. Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
correctTarget
           (Result VSEMor -> Result VSEMor)
-> (VSESign -> Result VSEMor) -> VSESign -> Result VSEMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InducedSign Dlformula Procs VSEMorExt Procs
-> InducedMorphism Procs VSEMorExt
-> EndoMap RawSymbol
-> VSESign
-> Result VSEMor
forall e f m.
(Pretty e, Show f) =>
InducedSign f e m e
-> InducedMorphism e m
-> EndoMap RawSymbol
-> Sign f e
-> Result (Morphism f e m)
inducedFromMorphismExt InducedSign Dlformula Procs VSEMorExt Procs
forall f. InducedSign f Procs VSEMorExt Procs
inducedExt (VSEMorExt -> InducedMorphism Procs VSEMorExt
forall m e. m -> InducedMorphism e m
constMorphExt VSEMorExt
forall e. DefMorExt e
emptyMorExt) EndoMap RawSymbol
rm
         induced_from_to_morphism :: VSE
-> EndoMap RawSymbol
-> ExtSign VSESign Symbol
-> ExtSign VSESign Symbol
-> Result VSEMor
induced_from_to_morphism VSE rm :: EndoMap RawSymbol
rm s1 :: ExtSign VSESign Symbol
s1 = (VSEMor -> VSEMor) -> Result VSEMor -> Result VSEMor
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap VSEMor -> VSEMor
forall f. Morphism f Procs VSEMorExt -> Morphism f Procs VSEMorExt
correctTarget
           (Result VSEMor -> Result VSEMor)
-> (ExtSign VSESign Symbol -> Result VSEMor)
-> ExtSign VSESign Symbol
-> Result VSEMor
forall b c a. (b -> c) -> (a -> b) -> a -> c
. InducedSign Dlformula Procs VSEMorExt Procs
-> InducedMorphism Procs VSEMorExt
-> (VSEMor -> VSEMor -> Result VSEMorExt)
-> (Procs -> Procs -> Bool)
-> (Procs -> Procs -> Procs)
-> EndoMap RawSymbol
-> ExtSign VSESign Symbol
-> ExtSign VSESign Symbol
-> Result VSEMor
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphismExt InducedSign Dlformula Procs VSEMorExt Procs
forall f. InducedSign f Procs VSEMorExt Procs
inducedExt (VSEMorExt -> InducedMorphism Procs VSEMorExt
forall m e. m -> InducedMorphism e m
constMorphExt VSEMorExt
forall e. DefMorExt e
emptyMorExt)
             (\ _ _ -> VSEMorExt -> Result VSEMorExt
forall (m :: * -> *) a. Monad m => a -> m a
return VSEMorExt
forall e. DefMorExt e
emptyMorExt) Procs -> Procs -> Bool
isSubProcsMap Procs -> Procs -> Procs
diffProcs EndoMap RawSymbol
rm ExtSign VSESign Symbol
s1

instance Logic VSE ()
               VSEBasicSpec Sentence SYMB_ITEMS SYMB_MAP_ITEMS
               VSESign
               VSEMor
               Symbol RawSymbol () where
         stability :: VSE -> Stability
stability VSE = Stability
Testing
         empty_proof_tree :: VSE -> ()
empty_proof_tree VSE = ()
         provers :: VSE -> [Prover VSESign Sentence VSEMor () ()]
provers VSE = [Prover VSESign Sentence VSEMor () ()
vse]