{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./CommonLogic/Sublogic.hs
Description :  Sublogics for CommonLogic
Copyright   :  (c) Eugen Kuksa, Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (via Logic.Logic)

Sublogics for CommonLogic
-}

module CommonLogic.Sublogic
    ( sl_basic_spec       -- determine sublogic for basic spec
    , CLTextType (..)     -- types of CommonLogic texts
    , CommonLogicSL (..)  -- sublogics for CommonLogic
    , sublogics_max       -- join of sublogics
    , top                 -- FullCommonLogic
    , bottom              -- Propositional
    , propsl              -- Propositional
    , folsl               -- FirstOrderLogic
    , fullclsl            -- FullCommonLogic
    , sublogics_all       -- all sublogics
    , sublogics_name      -- name of sublogics
    , sl_sig              -- sublogic for a signature
    , sl_sym              -- sublogic for symbols
    , sl_mor              -- sublogic for morphisms
    , sl_symmap           -- sublogic for symbol map items
    , sl_symitems         -- sublogic for symbol items
    , sublogic_text       -- sublogic for a text
    , sublogic_name       -- sublogic for a text
    , prSymbolM
    , prSig
    , prMor
    , prSymMapM
    , prSymItemsM
    , prName
    , prBasicSpec
    )
    where

import CommonLogic.Tools

import Data.Data
import Data.Function
import qualified Data.Set as Set

import CommonLogic.AS_CommonLogic
import Common.AS_Annotation (Annoted (..))
import CommonLogic.Sign
import CommonLogic.Symbol
import CommonLogic.Morphism

{- -----------------------------------------------------------------------------
datatypes                                                                 --
----------------------------------------------------------------------------- -}

-- | types of sublogics
data CLTextType =
    Propositional      -- ^ Text without quantifiers
  | FirstOrder         -- ^ Text in First Order Logic
  | Impredicative
  deriving (Int -> CLTextType -> ShowS
[CLTextType] -> ShowS
CLTextType -> String
(Int -> CLTextType -> ShowS)
-> (CLTextType -> String)
-> ([CLTextType] -> ShowS)
-> Show CLTextType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CLTextType] -> ShowS
$cshowList :: [CLTextType] -> ShowS
show :: CLTextType -> String
$cshow :: CLTextType -> String
showsPrec :: Int -> CLTextType -> ShowS
$cshowsPrec :: Int -> CLTextType -> ShowS
Show, CLTextType -> CLTextType -> Bool
(CLTextType -> CLTextType -> Bool)
-> (CLTextType -> CLTextType -> Bool) -> Eq CLTextType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CLTextType -> CLTextType -> Bool
$c/= :: CLTextType -> CLTextType -> Bool
== :: CLTextType -> CLTextType -> Bool
$c== :: CLTextType -> CLTextType -> Bool
Eq, Eq CLTextType
Eq CLTextType =>
(CLTextType -> CLTextType -> Ordering)
-> (CLTextType -> CLTextType -> Bool)
-> (CLTextType -> CLTextType -> Bool)
-> (CLTextType -> CLTextType -> Bool)
-> (CLTextType -> CLTextType -> Bool)
-> (CLTextType -> CLTextType -> CLTextType)
-> (CLTextType -> CLTextType -> CLTextType)
-> Ord CLTextType
CLTextType -> CLTextType -> Bool
CLTextType -> CLTextType -> Ordering
CLTextType -> CLTextType -> CLTextType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CLTextType -> CLTextType -> CLTextType
$cmin :: CLTextType -> CLTextType -> CLTextType
max :: CLTextType -> CLTextType -> CLTextType
$cmax :: CLTextType -> CLTextType -> CLTextType
>= :: CLTextType -> CLTextType -> Bool
$c>= :: CLTextType -> CLTextType -> Bool
> :: CLTextType -> CLTextType -> Bool
$c> :: CLTextType -> CLTextType -> Bool
<= :: CLTextType -> CLTextType -> Bool
$c<= :: CLTextType -> CLTextType -> Bool
< :: CLTextType -> CLTextType -> Bool
$c< :: CLTextType -> CLTextType -> Bool
compare :: CLTextType -> CLTextType -> Ordering
$ccompare :: CLTextType -> CLTextType -> Ordering
$cp1Ord :: Eq CLTextType
Ord, Int -> CLTextType
CLTextType -> Int
CLTextType -> [CLTextType]
CLTextType -> CLTextType
CLTextType -> CLTextType -> [CLTextType]
CLTextType -> CLTextType -> CLTextType -> [CLTextType]
(CLTextType -> CLTextType)
-> (CLTextType -> CLTextType)
-> (Int -> CLTextType)
-> (CLTextType -> Int)
-> (CLTextType -> [CLTextType])
-> (CLTextType -> CLTextType -> [CLTextType])
-> (CLTextType -> CLTextType -> [CLTextType])
-> (CLTextType -> CLTextType -> CLTextType -> [CLTextType])
-> Enum CLTextType
forall a.
(a -> a)
-> (a -> a)
-> (Int -> a)
-> (a -> Int)
-> (a -> [a])
-> (a -> a -> [a])
-> (a -> a -> [a])
-> (a -> a -> a -> [a])
-> Enum a
enumFromThenTo :: CLTextType -> CLTextType -> CLTextType -> [CLTextType]
$cenumFromThenTo :: CLTextType -> CLTextType -> CLTextType -> [CLTextType]
enumFromTo :: CLTextType -> CLTextType -> [CLTextType]
$cenumFromTo :: CLTextType -> CLTextType -> [CLTextType]
enumFromThen :: CLTextType -> CLTextType -> [CLTextType]
$cenumFromThen :: CLTextType -> CLTextType -> [CLTextType]
enumFrom :: CLTextType -> [CLTextType]
$cenumFrom :: CLTextType -> [CLTextType]
fromEnum :: CLTextType -> Int
$cfromEnum :: CLTextType -> Int
toEnum :: Int -> CLTextType
$ctoEnum :: Int -> CLTextType
pred :: CLTextType -> CLTextType
$cpred :: CLTextType -> CLTextType
succ :: CLTextType -> CLTextType
$csucc :: CLTextType -> CLTextType
Enum, CLTextType
CLTextType -> CLTextType -> Bounded CLTextType
forall a. a -> a -> Bounded a
maxBound :: CLTextType
$cmaxBound :: CLTextType
minBound :: CLTextType
$cminBound :: CLTextType
Bounded, Typeable)

-- for comparison of sublogics use the Ord instance

-- | sublogics for CommonLogic
data CommonLogicSL = CommonLogicSL
    { CommonLogicSL -> CLTextType
format :: CLTextType     -- Structural restrictions
    , CommonLogicSL -> Bool
compact :: Bool
    } deriving (Int -> CommonLogicSL -> ShowS
[CommonLogicSL] -> ShowS
CommonLogicSL -> String
(Int -> CommonLogicSL -> ShowS)
-> (CommonLogicSL -> String)
-> ([CommonLogicSL] -> ShowS)
-> Show CommonLogicSL
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CommonLogicSL] -> ShowS
$cshowList :: [CommonLogicSL] -> ShowS
show :: CommonLogicSL -> String
$cshow :: CommonLogicSL -> String
showsPrec :: Int -> CommonLogicSL -> ShowS
$cshowsPrec :: Int -> CommonLogicSL -> ShowS
Show, CommonLogicSL -> CommonLogicSL -> Bool
(CommonLogicSL -> CommonLogicSL -> Bool)
-> (CommonLogicSL -> CommonLogicSL -> Bool) -> Eq CommonLogicSL
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: CommonLogicSL -> CommonLogicSL -> Bool
$c/= :: CommonLogicSL -> CommonLogicSL -> Bool
== :: CommonLogicSL -> CommonLogicSL -> Bool
$c== :: CommonLogicSL -> CommonLogicSL -> Bool
Eq, Eq CommonLogicSL
Eq CommonLogicSL =>
(CommonLogicSL -> CommonLogicSL -> Ordering)
-> (CommonLogicSL -> CommonLogicSL -> Bool)
-> (CommonLogicSL -> CommonLogicSL -> Bool)
-> (CommonLogicSL -> CommonLogicSL -> Bool)
-> (CommonLogicSL -> CommonLogicSL -> Bool)
-> (CommonLogicSL -> CommonLogicSL -> CommonLogicSL)
-> (CommonLogicSL -> CommonLogicSL -> CommonLogicSL)
-> Ord CommonLogicSL
CommonLogicSL -> CommonLogicSL -> Bool
CommonLogicSL -> CommonLogicSL -> Ordering
CommonLogicSL -> CommonLogicSL -> CommonLogicSL
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
$cmin :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
max :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
$cmax :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
>= :: CommonLogicSL -> CommonLogicSL -> Bool
$c>= :: CommonLogicSL -> CommonLogicSL -> Bool
> :: CommonLogicSL -> CommonLogicSL -> Bool
$c> :: CommonLogicSL -> CommonLogicSL -> Bool
<= :: CommonLogicSL -> CommonLogicSL -> Bool
$c<= :: CommonLogicSL -> CommonLogicSL -> Bool
< :: CommonLogicSL -> CommonLogicSL -> Bool
$c< :: CommonLogicSL -> CommonLogicSL -> Bool
compare :: CommonLogicSL -> CommonLogicSL -> Ordering
$ccompare :: CommonLogicSL -> CommonLogicSL -> Ordering
$cp1Ord :: Eq CommonLogicSL
Ord, Typeable)

-- | all sublogics
sublogics_all :: [CommonLogicSL]
sublogics_all :: [CommonLogicSL]
sublogics_all =
   [ CLTextType -> Bool -> CommonLogicSL
CommonLogicSL CLTextType
t Bool
c
   | CLTextType
t <- [CLTextType
forall a. Bounded a => a
minBound .. CLTextType
forall a. Bounded a => a
maxBound]
   , Bool
c <- [Bool
True, Bool
False]
   ]

{- ----------------------------------------------------------------------------
Special elements in the Lattice of logics                                --
---------------------------------------------------------------------------- -}

-- | Greates sublogc: FullCommonLogic
top :: CommonLogicSL
top :: CommonLogicSL
top = CLTextType -> Bool -> CommonLogicSL
CommonLogicSL CLTextType
forall a. Bounded a => a
maxBound Bool
False

-- | Smallest sublogic: Propositional
bottom :: CommonLogicSL
bottom :: CommonLogicSL
bottom = CLTextType -> Bool -> CommonLogicSL
CommonLogicSL CLTextType
forall a. Bounded a => a
minBound Bool
True

fullclsl :: CommonLogicSL
fullclsl :: CommonLogicSL
fullclsl = CommonLogicSL
top

-- | Compact as Sublogic
impsl :: CommonLogicSL
impsl :: CommonLogicSL
impsl = CommonLogicSL
top { compact :: Bool
compact = Bool
True }

-- | FirstOrder as Sublogic
folsl :: CommonLogicSL
folsl :: CommonLogicSL
folsl = CommonLogicSL
bottom {format :: CLTextType
format = CLTextType
FirstOrder}

-- | Propositional as Sublogic
propsl :: CommonLogicSL
propsl :: CommonLogicSL
propsl = CommonLogicSL
bottom {format :: CLTextType
format = CLTextType
Propositional}

{- -----------------------------------------------------------------------------
join and max                                                              --
----------------------------------------------------------------------------- -}

-- | Yields the greater sublogic
sublogics_max :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
sublogics_max :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL
sublogics_max s1 :: CommonLogicSL
s1 s2 :: CommonLogicSL
s2 = CLTextType -> Bool -> CommonLogicSL
CommonLogicSL ((CLTextType -> CLTextType -> CLTextType)
-> (CommonLogicSL -> CLTextType)
-> CommonLogicSL
-> CommonLogicSL
-> CLTextType
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on CLTextType -> CLTextType -> CLTextType
forall a. Ord a => a -> a -> a
max CommonLogicSL -> CLTextType
format CommonLogicSL
s1 CommonLogicSL
s2) ((Bool -> Bool -> Bool)
-> (CommonLogicSL -> Bool)
-> CommonLogicSL
-> CommonLogicSL
-> Bool
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
on Bool -> Bool -> Bool
forall a. Ord a => a -> a -> a
min CommonLogicSL -> Bool
compact CommonLogicSL
s1 CommonLogicSL
s2)

{- -----------------------------------------------------------------------------
Helpers                                                                   --
----------------------------------------------------------------------------- -}

-- compute sublogics from a list of sublogics
comp_list :: [CommonLogicSL] -> CommonLogicSL
comp_list :: [CommonLogicSL] -> CommonLogicSL
comp_list = (CommonLogicSL -> CommonLogicSL -> CommonLogicSL)
-> CommonLogicSL -> [CommonLogicSL] -> CommonLogicSL
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CommonLogicSL -> CommonLogicSL -> CommonLogicSL
sublogics_max CommonLogicSL
bottom

{- ----------------------------------------------------------------------------
Functions to compute minimal sublogic for a given element, these work    --
by recursing into all subelements                                        --
---------------------------------------------------------------------------- -}

-- | determines the sublogic for a complete text
sublogic_text :: CommonLogicSL -> TEXT -> CommonLogicSL
sublogic_text :: CommonLogicSL -> TEXT -> CommonLogicSL
sublogic_text cs :: CommonLogicSL
cs t :: TEXT
t = Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL
sl_text (TEXT -> Set NAME
prd_text TEXT
t) CommonLogicSL
cs TEXT
t


-- | determines the sublogic for symbol map items
sl_symmap :: CommonLogicSL -> SYMB_MAP_ITEMS
    -> CommonLogicSL
sl_symmap :: CommonLogicSL -> SYMB_MAP_ITEMS -> CommonLogicSL
sl_symmap cs :: CommonLogicSL
cs _ = CommonLogicSL
cs

-- | determines the sublogic for a morphism
sl_mor :: CommonLogicSL -> Morphism -> CommonLogicSL
sl_mor :: CommonLogicSL -> Morphism -> CommonLogicSL
sl_mor cs :: CommonLogicSL
cs _ = CommonLogicSL
cs

-- | determines the sublogic for a Signature
sl_sig :: CommonLogicSL -> Sign -> CommonLogicSL
sl_sig :: CommonLogicSL -> Sign -> CommonLogicSL
sl_sig cs :: CommonLogicSL
cs _ = CommonLogicSL
cs

-- | determines the sublogic for symbols
sl_sym :: CommonLogicSL -> Symbol -> CommonLogicSL
sl_sym :: CommonLogicSL -> Symbol -> CommonLogicSL
sl_sym cs :: CommonLogicSL
cs _ = CommonLogicSL
cs

-- | determines sublogic for texts, given predicates of the super-text
sl_text :: Set.Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL
sl_text :: Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL
sl_text prds :: Set NAME
prds cs :: CommonLogicSL
cs t :: TEXT
t =
    case TEXT
t of
        Text ps :: [PHRASE]
ps _ -> Set NAME -> CommonLogicSL -> [PHRASE] -> CommonLogicSL
sl_phrases Set NAME
prds CommonLogicSL
cs [PHRASE]
ps
        Named_text _ nt :: TEXT
nt _ -> Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL
sl_text Set NAME
prds CommonLogicSL
cs TEXT
nt

-- | determines sublogic for phrases, given predicates of the super-text
sl_phrases :: Set.Set NAME -> CommonLogicSL -> [PHRASE] -> CommonLogicSL
sl_phrases :: Set NAME -> CommonLogicSL -> [PHRASE] -> CommonLogicSL
sl_phrases prds :: Set NAME
prds cs :: CommonLogicSL
cs ps :: [PHRASE]
ps = (CommonLogicSL -> CommonLogicSL -> CommonLogicSL)
-> CommonLogicSL -> [CommonLogicSL] -> CommonLogicSL
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl CommonLogicSL -> CommonLogicSL -> CommonLogicSL
sublogics_max CommonLogicSL
cs ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ (PHRASE -> CommonLogicSL) -> [PHRASE] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map (Set NAME -> CommonLogicSL -> PHRASE -> CommonLogicSL
sl_phrase Set NAME
prds CommonLogicSL
cs) [PHRASE]
ps

-- | determines sublogic for a single phrase, given predicates of the super-text
sl_phrase :: Set.Set NAME -> CommonLogicSL -> PHRASE -> CommonLogicSL
sl_phrase :: Set NAME -> CommonLogicSL -> PHRASE -> CommonLogicSL
sl_phrase prds :: Set NAME
prds cs :: CommonLogicSL
cs p :: PHRASE
p =
    case PHRASE
p of
        Module m :: MODULE
m -> Set NAME -> CommonLogicSL -> MODULE -> CommonLogicSL
sl_module Set NAME
prds CommonLogicSL
cs MODULE
m
        Sentence s :: SENTENCE
s -> Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence Set NAME
prds CommonLogicSL
cs SENTENCE
s
        Importation i :: IMPORTATION
i -> Set NAME -> CommonLogicSL -> IMPORTATION -> CommonLogicSL
sl_importation Set NAME
prds CommonLogicSL
cs IMPORTATION
i
        Comment_text _ t :: TEXT
t _ -> Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL
sl_text Set NAME
prds CommonLogicSL
cs TEXT
t

-- | determines sublogic for a module, given predicates of the super-text
sl_module :: Set.Set NAME -> CommonLogicSL -> MODULE -> CommonLogicSL
sl_module :: Set NAME -> CommonLogicSL -> MODULE -> CommonLogicSL
sl_module prds :: Set NAME
prds cs :: CommonLogicSL
cs m :: MODULE
m =
    case MODULE
m of
        Mod _ t :: TEXT
t _ -> Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL
sl_text Set NAME
prds CommonLogicSL
cs TEXT
t
        Mod_ex _ _ t :: TEXT
t _ -> Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL
sl_text Set NAME
prds CommonLogicSL
cs TEXT
t

-- | determines sublogic for a sentence, given predicates of the super-text
sl_sentence :: Set.Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence :: Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence prds :: Set NAME
prds cs :: CommonLogicSL
cs sen :: SENTENCE
sen =
    case SENTENCE
sen of
        Quant_sent q :: QUANT
q vs :: [NAME_OR_SEQMARK]
vs is :: SENTENCE
is _ -> Set NAME
-> CommonLogicSL
-> QUANT
-> [NAME_OR_SEQMARK]
-> SENTENCE
-> CommonLogicSL
sl_quantSent Set NAME
prds CommonLogicSL
cs QUANT
q [NAME_OR_SEQMARK]
vs SENTENCE
is
        Bool_sent b :: BOOL_SENT
b _ -> Set NAME -> CommonLogicSL -> BOOL_SENT -> CommonLogicSL
sl_boolSent Set NAME
prds CommonLogicSL
cs BOOL_SENT
b
        Atom_sent a :: ATOM
a _ -> Set NAME -> CommonLogicSL -> ATOM -> CommonLogicSL
sl_atomSent Set NAME
prds CommonLogicSL
cs ATOM
a
        Comment_sent _ s :: SENTENCE
s _ -> Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence Set NAME
prds CommonLogicSL
cs SENTENCE
s
        Irregular_sent s :: SENTENCE
s _ -> Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence Set NAME
prds CommonLogicSL
cs SENTENCE
s

-- | determines the sublogic for importations (importations are ignored)
sl_importation :: Set.Set NAME -> CommonLogicSL -> IMPORTATION
    -> CommonLogicSL
sl_importation :: Set NAME -> CommonLogicSL -> IMPORTATION -> CommonLogicSL
sl_importation _ cs :: CommonLogicSL
cs _ = CommonLogicSL
cs

{- | determines the sublogic for quantified sentences,
given predicates of the super-text -}
sl_quantSent :: Set.Set NAME -> CommonLogicSL
                -> QUANT -> [NAME_OR_SEQMARK] -> SENTENCE
                -> CommonLogicSL
sl_quantSent :: Set NAME
-> CommonLogicSL
-> QUANT
-> [NAME_OR_SEQMARK]
-> SENTENCE
-> CommonLogicSL
sl_quantSent prds :: Set NAME
prds cs :: CommonLogicSL
cs _ noss :: [NAME_OR_SEQMARK]
noss s :: SENTENCE
s =
  [CommonLogicSL] -> CommonLogicSL
comp_list ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ CommonLogicSL
folsl CommonLogicSL -> [CommonLogicSL] -> [CommonLogicSL]
forall a. a -> [a] -> [a]
: Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence Set NAME
prds CommonLogicSL
cs SENTENCE
s
  CommonLogicSL -> [CommonLogicSL] -> [CommonLogicSL]
forall a. a -> [a] -> [a]
: (NAME_OR_SEQMARK -> CommonLogicSL)
-> [NAME_OR_SEQMARK] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map (Set NAME -> CommonLogicSL -> NAME_OR_SEQMARK -> CommonLogicSL
sl_nameOrSeqmark Set NAME
prds CommonLogicSL
cs) [NAME_OR_SEQMARK]
noss

{- | determines the sublogic for boolean sentences,
given predicates of the super-text -}
sl_boolSent :: Set.Set NAME -> CommonLogicSL -> BOOL_SENT -> CommonLogicSL
sl_boolSent :: Set NAME -> CommonLogicSL -> BOOL_SENT -> CommonLogicSL
sl_boolSent prds :: Set NAME
prds cs :: CommonLogicSL
cs b :: BOOL_SENT
b =
    case BOOL_SENT
b of
      Junction _ ss :: [SENTENCE]
ss -> [CommonLogicSL] -> CommonLogicSL
comp_list ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ (SENTENCE -> CommonLogicSL) -> [SENTENCE] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map (Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence Set NAME
prds CommonLogicSL
cs) [SENTENCE]
ss
      Negation s :: SENTENCE
s -> Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence Set NAME
prds CommonLogicSL
cs SENTENCE
s
      BinOp _ s1 :: SENTENCE
s1 s2 :: SENTENCE
s2 ->
        CommonLogicSL -> CommonLogicSL -> CommonLogicSL
sublogics_max (Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence Set NAME
prds CommonLogicSL
cs SENTENCE
s1) (Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL
sl_sentence Set NAME
prds CommonLogicSL
cs SENTENCE
s2)

{- | determines the sublogic for atoms,
given predicates of the super-text -}
sl_atomSent :: Set.Set NAME -> CommonLogicSL -> ATOM -> CommonLogicSL
sl_atomSent :: Set NAME -> CommonLogicSL -> ATOM -> CommonLogicSL
sl_atomSent prds :: Set NAME
prds cs :: CommonLogicSL
cs a :: ATOM
a =
    case ATOM
a of
        Equation t1 :: TERM
t1 t2 :: TERM
t2 ->
            [CommonLogicSL] -> CommonLogicSL
comp_list ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ CommonLogicSL
folsl CommonLogicSL -> [CommonLogicSL] -> [CommonLogicSL]
forall a. a -> [a] -> [a]
: (TERM -> CommonLogicSL) -> [TERM] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map (Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_term Set NAME
prds CommonLogicSL
cs) [TERM
t1, TERM
t2]
        Atom t :: TERM
t [] -> Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_term Set NAME
prds CommonLogicSL
cs TERM
t
        Atom t :: TERM
t tseq :: [TERM_SEQ]
tseq -> Set NAME -> CommonLogicSL -> TERM -> [TERM_SEQ] -> CommonLogicSL
slAppl Set NAME
prds CommonLogicSL
cs TERM
t [TERM_SEQ]
tseq

slAppl :: Set.Set NAME -> CommonLogicSL -> TERM -> [TERM_SEQ] -> CommonLogicSL
slAppl :: Set NAME -> CommonLogicSL -> TERM -> [TERM_SEQ] -> CommonLogicSL
slAppl prds :: Set NAME
prds cs :: CommonLogicSL
cs t :: TERM
t tseq :: [TERM_SEQ]
tseq = [CommonLogicSL] -> CommonLogicSL
comp_list
  ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ (if TERM -> Bool
isNameTerm TERM
t then CommonLogicSL
folsl else CommonLogicSL
impsl)
  CommonLogicSL -> [CommonLogicSL] -> [CommonLogicSL]
forall a. a -> [a] -> [a]
: Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_term Set NAME
prds CommonLogicSL
cs TERM
t CommonLogicSL -> [CommonLogicSL] -> [CommonLogicSL]
forall a. a -> [a] -> [a]
: (TERM_SEQ -> CommonLogicSL) -> [TERM_SEQ] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map (Set NAME -> CommonLogicSL -> TERM_SEQ -> CommonLogicSL
sl_termSeq Set NAME
prds CommonLogicSL
cs) [TERM_SEQ]
tseq

-- check for a curried name application
isNameTerm :: TERM -> Bool
isNameTerm :: TERM -> Bool
isNameTerm term :: TERM
term = case TERM
term of
  Name_term _ -> Bool
True
  Comment_term t :: TERM
t _ _ -> TERM -> Bool
isNameTerm TERM
t
  Funct_term t :: TERM
t _ _ -> TERM -> Bool
isNameTerm TERM
t
  That_term {} -> Bool
False

{- | determines the sublogic for NAME_OR_SEQMARK,
given predicates of the super-text -}
sl_nameOrSeqmark :: Set.Set NAME -> CommonLogicSL -> NAME_OR_SEQMARK
    -> CommonLogicSL
sl_nameOrSeqmark :: Set NAME -> CommonLogicSL -> NAME_OR_SEQMARK -> CommonLogicSL
sl_nameOrSeqmark prds :: Set NAME
prds cs :: CommonLogicSL
cs nos :: NAME_OR_SEQMARK
nos =
    case NAME_OR_SEQMARK
nos of
        Name n :: NAME
n -> Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_quantName Set NAME
prds CommonLogicSL
cs NAME
n
        SeqMark _ -> CommonLogicSL
cs { compact :: Bool
compact = Bool
False }

{- | determines the sublogic for names which are next to a quantifier,
given predicates of the super-text -}
sl_quantName :: Set.Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_quantName :: Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_quantName prds :: Set NAME
prds _ n :: NAME
n = if NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member NAME
n Set NAME
prds then CommonLogicSL
impsl else CommonLogicSL
folsl

{- | determines the sublogic for names,
given predicates of the super-text -}
sl_name :: Set.Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_name :: Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_name _ = CommonLogicSL -> NAME -> CommonLogicSL
sublogic_name

{- | determines the sublogic for names,
ignoring predicates -}
sublogic_name :: CommonLogicSL -> NAME -> CommonLogicSL
sublogic_name :: CommonLogicSL -> NAME -> CommonLogicSL
sublogic_name _ _ = CommonLogicSL
propsl

{- | determines the sublogic for terms,
given predicates of the super-text -}
sl_term :: Set.Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_term :: Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_term prds :: Set NAME
prds cs :: CommonLogicSL
cs term :: TERM
term =
    case TERM
term of
      Name_term n :: NAME
n -> Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_name Set NAME
prds CommonLogicSL
cs NAME
n
      Funct_term t :: TERM
t tseq :: [TERM_SEQ]
tseq _ -> Set NAME -> CommonLogicSL -> TERM -> [TERM_SEQ] -> CommonLogicSL
slAppl Set NAME
prds CommonLogicSL
cs TERM
t [TERM_SEQ]
tseq
      Comment_term t :: TERM
t _ _ -> Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_term Set NAME
prds CommonLogicSL
cs TERM
t
      That_term {} -> CommonLogicSL
impsl

{- | determines the sublogic for term sequences,
given predicates of the super-text -}
sl_termSeq :: Set.Set NAME -> CommonLogicSL -> TERM_SEQ -> CommonLogicSL
sl_termSeq :: Set NAME -> CommonLogicSL -> TERM_SEQ -> CommonLogicSL
sl_termSeq prds :: Set NAME
prds cs :: CommonLogicSL
cs tseq :: TERM_SEQ
tseq =
    case TERM_SEQ
tseq of
        Term_seq t :: TERM
t -> Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_termInSeq Set NAME
prds CommonLogicSL
cs TERM
t
        Seq_marks _ -> CommonLogicSL
cs { compact :: Bool
compact = Bool
False }

{- | determines the sublogic for names,
given predicates of the super-text -}
sl_nameInTermSeq :: Set.Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_nameInTermSeq :: Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_nameInTermSeq prds :: Set NAME
prds _ n :: NAME
n = if NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member NAME
n Set NAME
prds then CommonLogicSL
impsl else CommonLogicSL
propsl

{- | determines the sublogic for terms inside of a term-sequence,
given predicates of the super-text -}
sl_termInSeq :: Set.Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_termInSeq :: Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_termInSeq prds :: Set NAME
prds cs :: CommonLogicSL
cs term :: TERM
term =
    case TERM
term of
      Name_term n :: NAME
n -> Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL
sl_nameInTermSeq Set NAME
prds CommonLogicSL
cs NAME
n
      Funct_term t :: TERM
t tseq :: [TERM_SEQ]
tseq _ ->
          [CommonLogicSL] -> CommonLogicSL
comp_list ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ CommonLogicSL
folsl CommonLogicSL -> [CommonLogicSL] -> [CommonLogicSL]
forall a. a -> [a] -> [a]
: Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_term Set NAME
prds CommonLogicSL
cs TERM
t CommonLogicSL -> [CommonLogicSL] -> [CommonLogicSL]
forall a. a -> [a] -> [a]
: (TERM_SEQ -> CommonLogicSL) -> [TERM_SEQ] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map (Set NAME -> CommonLogicSL -> TERM_SEQ -> CommonLogicSL
sl_termSeq Set NAME
prds CommonLogicSL
cs) [TERM_SEQ]
tseq
      Comment_term t :: TERM
t _ _ -> Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL
sl_term Set NAME
prds CommonLogicSL
cs TERM
t
      That_term {} -> CommonLogicSL
impsl

-- | determines sublogic for basic items
sl_basic_items :: CommonLogicSL -> BASIC_ITEMS -> CommonLogicSL
sl_basic_items :: CommonLogicSL -> BASIC_ITEMS -> CommonLogicSL
sl_basic_items cs :: CommonLogicSL
cs (Axiom_items axs :: [Annoted TEXT_META]
axs) = [CommonLogicSL] -> CommonLogicSL
comp_list ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ (Annoted TEXT_META -> CommonLogicSL)
-> [Annoted TEXT_META] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map
  (\ Annoted {item :: forall a. Annoted a -> a
item = TEXT_META
tm} ->
    (Set NAME -> TEXT -> CommonLogicSL)
-> (Set NAME, TEXT) -> CommonLogicSL
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry (Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL
`sl_text` CommonLogicSL
cs) ((Set NAME, TEXT) -> CommonLogicSL)
-> (Set NAME, TEXT) -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ TEXT -> (Set NAME, TEXT)
getPreds (TEXT -> (Set NAME, TEXT)) -> TEXT -> (Set NAME, TEXT)
forall a b. (a -> b) -> a -> b
$ TEXT_META -> TEXT
getText TEXT_META
tm
  ) [Annoted TEXT_META]
axs
  where getPreds :: TEXT -> (Set.Set NAME, TEXT)
        getPreds :: TEXT -> (Set NAME, TEXT)
getPreds txt :: TEXT
txt = (TEXT -> Set NAME
prd_text TEXT
txt, TEXT
txt)

-- | determines sublogic for basic spec
sl_basic_spec :: CommonLogicSL -> BASIC_SPEC -> CommonLogicSL
sl_basic_spec :: CommonLogicSL -> BASIC_SPEC -> CommonLogicSL
sl_basic_spec cs :: CommonLogicSL
cs (Basic_spec spec :: [Annoted BASIC_ITEMS]
spec) =
  [CommonLogicSL] -> CommonLogicSL
comp_list ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEMS -> CommonLogicSL)
-> [Annoted BASIC_ITEMS] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map (CommonLogicSL -> BASIC_ITEMS -> CommonLogicSL
sl_basic_items CommonLogicSL
cs (BASIC_ITEMS -> CommonLogicSL)
-> (Annoted BASIC_ITEMS -> BASIC_ITEMS)
-> Annoted BASIC_ITEMS
-> CommonLogicSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Annoted BASIC_ITEMS -> BASIC_ITEMS
forall a. Annoted a -> a
item) [Annoted BASIC_ITEMS]
spec

-- | determines sublogc for symb items
sl_symitems :: CommonLogicSL -> SYMB_ITEMS -> CommonLogicSL
sl_symitems :: CommonLogicSL -> SYMB_ITEMS -> CommonLogicSL
sl_symitems _ (Symb_items noss :: [NAME_OR_SEQMARK]
noss _) =
  [CommonLogicSL] -> CommonLogicSL
comp_list ([CommonLogicSL] -> CommonLogicSL)
-> [CommonLogicSL] -> CommonLogicSL
forall a b. (a -> b) -> a -> b
$ (NAME_OR_SEQMARK -> CommonLogicSL)
-> [NAME_OR_SEQMARK] -> [CommonLogicSL]
forall a b. (a -> b) -> [a] -> [b]
map (Set NAME -> CommonLogicSL -> NAME_OR_SEQMARK -> CommonLogicSL
sl_nameOrSeqmark Set NAME
forall a. Set a
Set.empty CommonLogicSL
bottom) [NAME_OR_SEQMARK]
noss

{- -----------------------------------------------------------------------------
Conversion functions to String                                            --
----------------------------------------------------------------------------- -}

-- | String representation of a Sublogic
sublogics_name :: CommonLogicSL -> String
sublogics_name :: CommonLogicSL -> String
sublogics_name f :: CommonLogicSL
f = CLTextType -> String
forall a. Show a => a -> String
show (CommonLogicSL -> CLTextType
format CommonLogicSL
f) String -> ShowS
forall a. [a] -> [a] -> [a]
++ if CommonLogicSL -> Bool
compact CommonLogicSL
f then "" else "Seq"

{- -----------------------------------------------------------------------------
Projections to sublogics                                                  --
----------------------------------------------------------------------------- -}

-- | projection of a symbol to a sublogic
prSymbolM :: CommonLogicSL -> Symbol -> Maybe Symbol
prSymbolM :: CommonLogicSL -> Symbol -> Maybe Symbol
prSymbolM _ = Symbol -> Maybe Symbol
forall a. a -> Maybe a
Just

prSymItemsM :: CommonLogicSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
prSymItemsM :: CommonLogicSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS
prSymItemsM cs :: CommonLogicSL
cs si :: SYMB_ITEMS
si@(Symb_items noss :: [NAME_OR_SEQMARK]
noss r :: Range
r) = case CommonLogicSL -> CLTextType
format CommonLogicSL
cs of
  Impredicative -> SYMB_ITEMS -> Maybe SYMB_ITEMS
forall a. a -> Maybe a
Just SYMB_ITEMS
si
  _ -> SYMB_ITEMS -> Maybe SYMB_ITEMS
forall a. a -> Maybe a
Just (SYMB_ITEMS -> Maybe SYMB_ITEMS) -> SYMB_ITEMS -> Maybe SYMB_ITEMS
forall a b. (a -> b) -> a -> b
$ [NAME_OR_SEQMARK] -> Range -> SYMB_ITEMS
Symb_items ((NAME_OR_SEQMARK -> Bool) -> [NAME_OR_SEQMARK] -> [NAME_OR_SEQMARK]
forall a. (a -> Bool) -> [a] -> [a]
filter NAME_OR_SEQMARK -> Bool
isName [NAME_OR_SEQMARK]
noss) Range
r
  where isName :: NAME_OR_SEQMARK -> Bool
isName nos :: NAME_OR_SEQMARK
nos = case NAME_OR_SEQMARK
nos of
          Name _ -> Bool
True
          _ -> Bool
False

-- | projection of a signature to a sublogic
prSig :: CommonLogicSL -> Sign -> Sign
prSig :: CommonLogicSL -> Sign -> Sign
prSig _ = Sign -> Sign
forall a. a -> a
id

-- | projection of a morphism to a sublogic
prMor :: CommonLogicSL -> Morphism -> Morphism
prMor :: CommonLogicSL -> Morphism -> Morphism
prMor _ mor :: Morphism
mor = Morphism
mor

-- | projection of symb map items to a sublogic
prSymMapM :: CommonLogicSL
          -> SYMB_MAP_ITEMS
          -> Maybe SYMB_MAP_ITEMS
prSymMapM :: CommonLogicSL -> SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
prSymMapM _ = SYMB_MAP_ITEMS -> Maybe SYMB_MAP_ITEMS
forall a. a -> Maybe a
Just

-- | projection of a name to a sublogic
prName :: CommonLogicSL -> NAME -> Maybe NAME
prName :: CommonLogicSL -> NAME -> Maybe NAME
prName _ = NAME -> Maybe NAME
forall a. a -> Maybe a
Just

{- | filters all TEXTs inside the BASIC_SPEC of which the sublogic is less than
or equal to @cs@ -}
prBasicSpec :: CommonLogicSL -> BASIC_SPEC -> BASIC_SPEC
prBasicSpec :: CommonLogicSL -> BASIC_SPEC -> BASIC_SPEC
prBasicSpec cs :: CommonLogicSL
cs (Basic_spec items :: [Annoted BASIC_ITEMS]
items) = [Annoted BASIC_ITEMS] -> BASIC_SPEC
Basic_spec ([Annoted BASIC_ITEMS] -> BASIC_SPEC)
-> [Annoted BASIC_ITEMS] -> BASIC_SPEC
forall a b. (a -> b) -> a -> b
$ (Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS)
-> [Annoted BASIC_ITEMS] -> [Annoted BASIC_ITEMS]
forall a b. (a -> b) -> [a] -> [b]
map (CommonLogicSL -> Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS
maybeLE CommonLogicSL
cs) [Annoted BASIC_ITEMS]
items

maybeLE :: CommonLogicSL -> Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS
maybeLE :: CommonLogicSL -> Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS
maybeLE cs :: CommonLogicSL
cs = (BASIC_ITEMS -> BASIC_ITEMS)
-> Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((BASIC_ITEMS -> BASIC_ITEMS)
 -> Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS)
-> (BASIC_ITEMS -> BASIC_ITEMS)
-> Annoted BASIC_ITEMS
-> Annoted BASIC_ITEMS
forall a b. (a -> b) -> a -> b
$ \ (Axiom_items i :: [Annoted TEXT_META]
i) -> [Annoted TEXT_META] -> BASIC_ITEMS
Axiom_items ([Annoted TEXT_META] -> BASIC_ITEMS)
-> [Annoted TEXT_META] -> BASIC_ITEMS
forall a b. (a -> b) -> a -> b
$ (Annoted TEXT_META -> Bool)
-> [Annoted TEXT_META] -> [Annoted TEXT_META]
forall a. (a -> Bool) -> [a] -> [a]
filter (CommonLogicSL -> Annoted TEXT_META -> Bool
isSL_LE CommonLogicSL
cs) [Annoted TEXT_META]
i

isSL_LE :: CommonLogicSL -> Annoted TEXT_META -> Bool
isSL_LE :: CommonLogicSL -> Annoted TEXT_META -> Bool
isSL_LE cs :: CommonLogicSL
cs at :: Annoted TEXT_META
at = CommonLogicSL -> TEXT -> CommonLogicSL
sublogic_text CommonLogicSL
bottom (TEXT_META -> TEXT
getText (TEXT_META -> TEXT) -> TEXT_META -> TEXT
forall a b. (a -> b) -> a -> b
$ Annoted TEXT_META -> TEXT_META
forall a. Annoted a -> a
item Annoted TEXT_META
at) CommonLogicSL -> CommonLogicSL -> Bool
forall a. Ord a => a -> a -> Bool
<= CommonLogicSL
cs