{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./ConstraintCASL/Logic_ConstraintCASL.hs
Description :  instance of the class Logic for ConstraintCASL
Copyright   :  (c) Uni Bremen 2002-2007
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

Here is the place where the class Logic is instantiated for Constraint CASL.
   Also the instances for Syntax an Category.
-}

module ConstraintCASL.Logic_ConstraintCASL where

import Logic.Logic

import Common.DocUtils

import ConstraintCASL.AS_ConstraintCASL
import ConstraintCASL.Formula
import ConstraintCASL.StaticAna
import ConstraintCASL.ATC_ConstraintCASL ()
import ConstraintCASL.Print_AS ()

import CASL.AS_Basic_CASL
import CASL.Parse_AS_Basic
import CASL.ToDoc ()
import CASL.SymbolParser
import CASL.MapSentence
import CASL.ATC_CASL ()
import CASL.Sublogic
import CASL.Sign
import CASL.Morphism
import CASL.SymbolMapAnalysis
import CASL.Logic_CASL

data ConstraintCASL = ConstraintCASL deriving Int -> ConstraintCASL -> ShowS
[ConstraintCASL] -> ShowS
ConstraintCASL -> String
(Int -> ConstraintCASL -> ShowS)
-> (ConstraintCASL -> String)
-> ([ConstraintCASL] -> ShowS)
-> Show ConstraintCASL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [ConstraintCASL] -> ShowS
$cshowList :: [ConstraintCASL] -> ShowS
show :: ConstraintCASL -> String
$cshow :: ConstraintCASL -> String
showsPrec :: Int -> ConstraintCASL -> ShowS
$cshowsPrec :: Int -> ConstraintCASL -> ShowS
Show

instance Language ConstraintCASL where
 description :: ConstraintCASL -> String
description _ =
  "ConstraintCASL - a restriction of CASL to constraint "
  String -> ShowS
forall a. [a] -> [a] -> [a]
++ "formulas over predicates"

instance Syntax ConstraintCASL ConstraintCASLBasicSpec
                Symbol SYMB_ITEMS SYMB_MAP_ITEMS
      where
         parse_basic_spec :: ConstraintCASL
-> Maybe (PrefixMap -> AParser st ConstraintCASLBasicSpec)
parse_basic_spec ConstraintCASL = (PrefixMap -> AParser st ConstraintCASLBasicSpec)
-> Maybe (PrefixMap -> AParser st ConstraintCASLBasicSpec)
forall a. a -> Maybe a
Just ((PrefixMap -> AParser st ConstraintCASLBasicSpec)
 -> Maybe (PrefixMap -> AParser st ConstraintCASLBasicSpec))
-> (PrefixMap -> AParser st ConstraintCASLBasicSpec)
-> Maybe (PrefixMap -> AParser st ConstraintCASLBasicSpec)
forall a b. (a -> b) -> a -> b
$ [String] -> PrefixMap -> AParser st ConstraintCASLBasicSpec
forall f s b st.
(TermParser f, AParsable s, AParsable b) =>
[String] -> PrefixMap -> AParser st (BASIC_SPEC b s f)
basicSpec [String]
constraintKeywords
         parse_symb_items :: ConstraintCASL -> Maybe (PrefixMap -> AParser st SYMB_ITEMS)
parse_symb_items ConstraintCASL = (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 []
         parse_symb_map_items :: ConstraintCASL -> Maybe (PrefixMap -> AParser st SYMB_MAP_ITEMS)
parse_symb_map_items ConstraintCASL = (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 []

-- lattices (for sublogics) is missing

instance Sentences ConstraintCASL ConstraintCASLFORMULA
                   ConstraintCASLSign ConstraintCASLMor Symbol where
      map_sen :: ConstraintCASL
-> ConstraintCASLMor
-> ConstraintCASLFORMULA
-> Result ConstraintCASLFORMULA
map_sen ConstraintCASL m :: ConstraintCASLMor
m = ConstraintCASLFORMULA -> Result ConstraintCASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstraintCASLFORMULA -> Result ConstraintCASLFORMULA)
-> (ConstraintCASLFORMULA -> ConstraintCASLFORMULA)
-> ConstraintCASLFORMULA
-> Result ConstraintCASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSen ConstraintFORMULA () ()
-> ConstraintCASLMor
-> ConstraintCASLFORMULA
-> ConstraintCASLFORMULA
forall e m f.
MorphismExtension e m =>
MapSen f e m -> Morphism f e m -> FORMULA f -> FORMULA f
mapSen ((ConstraintFORMULA -> ConstraintFORMULA)
-> MapSen ConstraintFORMULA () ()
forall a b. a -> b -> a
const ConstraintFORMULA -> ConstraintFORMULA
forall a. a -> a
id) ConstraintCASLMor
m
      sym_of :: ConstraintCASL -> ConstraintCASLSign -> [Set Symbol]
sym_of ConstraintCASL = ConstraintCASLSign -> [Set Symbol]
forall f e. Sign f e -> [Set Symbol]
symOf
      symKind :: ConstraintCASL -> Symbol -> String
symKind ConstraintCASL = 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
. SYMB_KIND -> Doc
forall a. Pretty a => a -> Doc
pretty (SYMB_KIND -> Doc) -> (Symbol -> SYMB_KIND) -> Symbol -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. SymbType -> SYMB_KIND
symbolKind (SymbType -> SYMB_KIND)
-> (Symbol -> SymbType) -> Symbol -> SYMB_KIND
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbType
symbType
      symmap_of :: ConstraintCASL -> ConstraintCASLMor -> EndoMap Symbol
symmap_of ConstraintCASL = ConstraintCASLMor -> EndoMap Symbol
forall f e m. Morphism f e m -> EndoMap Symbol
morphismToSymbMap
      sym_name :: ConstraintCASL -> Symbol -> Id
sym_name ConstraintCASL = Symbol -> Id
symName

instance StaticAnalysis ConstraintCASL
               ConstraintCASLBasicSpec ConstraintCASLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               ConstraintCASLSign
               ConstraintCASLMor
               Symbol RawSymbol where
         basic_analysis :: ConstraintCASL
-> Maybe
     ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos)
      -> Result
           (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol,
            [Named ConstraintCASLFORMULA]))
basic_analysis ConstraintCASL = ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos)
 -> Result
      (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol,
       [Named ConstraintCASLFORMULA]))
-> Maybe
     ((ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos)
      -> Result
           (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol,
            [Named ConstraintCASLFORMULA]))
forall a. a -> Maybe a
Just (ConstraintCASLBasicSpec, ConstraintCASLSign, GlobalAnnos)
-> Result
     (ConstraintCASLBasicSpec, ExtSign ConstraintCASLSign Symbol,
      [Named ConstraintCASLFORMULA])
basicConstraintCASLAnalysis
         stat_symb_map_items :: ConstraintCASL
-> ConstraintCASLSign
-> Maybe ConstraintCASLSign
-> [SYMB_MAP_ITEMS]
-> Result (EndoMap RawSymbol)
stat_symb_map_items ConstraintCASL = ConstraintCASLSign
-> Maybe ConstraintCASLSign
-> [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 :: ConstraintCASL
-> ConstraintCASLSign -> [SYMB_ITEMS] -> Result [RawSymbol]
stat_symb_items ConstraintCASL = ConstraintCASLSign -> [SYMB_ITEMS] -> Result [RawSymbol]
forall f e. Sign f e -> [SYMB_ITEMS] -> Result [RawSymbol]
statSymbItems

         symbol_to_raw :: ConstraintCASL -> Symbol -> RawSymbol
symbol_to_raw ConstraintCASL = Symbol -> RawSymbol
symbolToRaw
         id_to_raw :: ConstraintCASL -> Id -> RawSymbol
id_to_raw ConstraintCASL = Id -> RawSymbol
idToRaw
         matches :: ConstraintCASL -> Symbol -> RawSymbol -> Bool
matches ConstraintCASL = Symbol -> RawSymbol -> Bool
CASL.Morphism.matches
         is_transportable :: ConstraintCASL -> ConstraintCASLMor -> Bool
is_transportable ConstraintCASL = ConstraintCASLMor -> Bool
forall f e m. Morphism f e m -> Bool
isSortInjective

         empty_signature :: ConstraintCASL -> ConstraintCASLSign
empty_signature ConstraintCASL = () -> ConstraintCASLSign
forall e f. e -> Sign f e
emptySign ()
         signature_union :: ConstraintCASL
-> ConstraintCASLSign
-> ConstraintCASLSign
-> Result ConstraintCASLSign
signature_union ConstraintCASL s :: ConstraintCASLSign
s = ConstraintCASLSign -> Result ConstraintCASLSign
forall (m :: * -> *) a. Monad m => a -> m a
return (ConstraintCASLSign -> Result ConstraintCASLSign)
-> (ConstraintCASLSign -> ConstraintCASLSign)
-> ConstraintCASLSign
-> Result ConstraintCASLSign
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (() -> () -> ())
-> ConstraintCASLSign -> ConstraintCASLSign -> ConstraintCASLSign
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig () -> () -> ()
forall a b. a -> b -> a
const ConstraintCASLSign
s
         morphism_union :: ConstraintCASL
-> ConstraintCASLMor
-> ConstraintCASLMor
-> Result ConstraintCASLMor
morphism_union ConstraintCASL = (() -> () -> ())
-> ConstraintCASLMor
-> ConstraintCASLMor
-> Result ConstraintCASLMor
forall e f m.
(e -> e -> e)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
plainMorphismUnion () -> () -> ()
forall a b. a -> b -> a
const
         final_union :: ConstraintCASL
-> ConstraintCASLSign
-> ConstraintCASLSign
-> Result ConstraintCASLSign
final_union ConstraintCASL = (() -> () -> ())
-> ConstraintCASLSign
-> ConstraintCASLSign
-> Result ConstraintCASLSign
forall e f.
(e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion () -> () -> ()
forall a b. a -> b -> a
const
         is_subsig :: ConstraintCASL -> ConstraintCASLSign -> ConstraintCASLSign -> Bool
is_subsig ConstraintCASL = (() -> () -> Bool)
-> ConstraintCASLSign -> ConstraintCASLSign -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig () -> () -> Bool
forall a b. a -> b -> Bool
trueC
         subsig_inclusion :: ConstraintCASL
-> ConstraintCASLSign
-> ConstraintCASLSign
-> Result ConstraintCASLMor
subsig_inclusion ConstraintCASL = ()
-> ConstraintCASLSign
-> ConstraintCASLSign
-> Result ConstraintCASLMor
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion ()
         cogenerated_sign :: ConstraintCASL
-> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor
cogenerated_sign ConstraintCASL = () -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign ()
         generated_sign :: ConstraintCASL
-> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor
generated_sign ConstraintCASL = () -> Set Symbol -> ConstraintCASLSign -> Result ConstraintCASLMor
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign ()
         induced_from_morphism :: ConstraintCASL
-> EndoMap RawSymbol
-> ConstraintCASLSign
-> Result ConstraintCASLMor
induced_from_morphism ConstraintCASL = ()
-> EndoMap RawSymbol
-> ConstraintCASLSign
-> Result ConstraintCASLMor
forall e f m.
(Pretty e, Show f) =>
m -> EndoMap RawSymbol -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism ()
         induced_from_to_morphism :: ConstraintCASL
-> EndoMap RawSymbol
-> ExtSign ConstraintCASLSign Symbol
-> ExtSign ConstraintCASLSign Symbol
-> Result ConstraintCASLMor
induced_from_to_morphism ConstraintCASL =
             ()
-> (() -> () -> Bool)
-> (() -> () -> ())
-> EndoMap RawSymbol
-> ExtSign ConstraintCASLSign Symbol
-> ExtSign ConstraintCASLSign Symbol
-> Result ConstraintCASLMor
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
m
-> (e -> e -> Bool)
-> (e -> e -> e)
-> EndoMap RawSymbol
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphism () () -> () -> Bool
forall a b. a -> b -> Bool
trueC () -> () -> ()
forall a b. a -> b -> a
const

instance MinSL () ConstraintFORMULA where
    minSL :: ConstraintFORMULA -> CASL_SL ()
minSL _ = CASL_SL ()
forall a. Lattice a => CASL_SL a
bottom

instance ProjForm () ConstraintFORMULA where
    projForm :: CASL_SL () -> ConstraintFORMULA -> Maybe ConstraintCASLFORMULA
projForm _ = ConstraintCASLFORMULA -> Maybe ConstraintCASLFORMULA
forall a. a -> Maybe a
Just (ConstraintCASLFORMULA -> Maybe ConstraintCASLFORMULA)
-> (ConstraintFORMULA -> ConstraintCASLFORMULA)
-> ConstraintFORMULA
-> Maybe ConstraintCASLFORMULA
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ConstraintFORMULA -> ConstraintCASLFORMULA
forall f. f -> FORMULA f
ExtFORMULA

instance Logic ConstraintCASL CASL_Sublogics
               ConstraintCASLBasicSpec ConstraintCASLFORMULA
               SYMB_ITEMS SYMB_MAP_ITEMS
               ConstraintCASLSign
               ConstraintCASLMor
               Symbol RawSymbol () where

         stability :: ConstraintCASL -> Stability
stability _ = Stability
Experimental
         proj_sublogic_epsilon :: ConstraintCASL
-> CASL_SL () -> ConstraintCASLSign -> ConstraintCASLMor
proj_sublogic_epsilon ConstraintCASL = () -> CASL_SL () -> ConstraintCASLSign -> ConstraintCASLMor
forall m a f e. m -> CASL_SL a -> Sign f e -> Morphism f e m
pr_epsilon ()
         all_sublogics :: ConstraintCASL -> [CASL_SL ()]
all_sublogics _ = [()] -> [CASL_SL ()]
forall a. Lattice a => [a] -> [CASL_SL a]
sublogics_all [()]
         empty_proof_tree :: ConstraintCASL -> ()
empty_proof_tree _ = ()