{- |

Module : $Header$

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.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 (Show, Eq, Ord, Enum, Bounded)

-- for comparison of sublogics use the Ord instance

-- | sublogics for CommonLogic

data CommonLogicSL = CommonLogicSL

{ format :: CLTextType -- Structural restrictions

, compact :: Bool

} deriving (Show, Eq, Ord)

-- | all sublogics

sublogics_all :: [CommonLogicSL]

sublogics_all =

[ CommonLogicSL t c

| t <- [minBound .. maxBound]

, c <- [True, False]

]

{- ----------------------------------------------------------------------------

Special elements in the Lattice of logics --

---------------------------------------------------------------------------- -}

-- | Greates sublogc: FullCommonLogic

top :: CommonLogicSL

top = CommonLogicSL maxBound False

-- | Smallest sublogic: Propositional

bottom :: CommonLogicSL

bottom = CommonLogicSL minBound True

fullclsl :: CommonLogicSL

fullclsl = top

-- | Compact as Sublogic

impsl :: CommonLogicSL

impsl = top { compact = True }

-- | FirstOrder as Sublogic

folsl :: CommonLogicSL

folsl = bottom {format = FirstOrder}

-- | Propositional as Sublogic

propsl :: CommonLogicSL

propsl = bottom {format = Propositional}

{- -----------------------------------------------------------------------------

join and max --

----------------------------------------------------------------------------- -}

-- | Yields the greater sublogic

sublogics_max :: CommonLogicSL -> CommonLogicSL -> CommonLogicSL

sublogics_max s1 s2 = CommonLogicSL (on max format s1 s2) (on min compact s1 s2)

{- -----------------------------------------------------------------------------

Helpers --

----------------------------------------------------------------------------- -}

-- compute sublogics from a list of sublogics

comp_list :: [CommonLogicSL] -> CommonLogicSL

comp_list = foldl sublogics_max 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 cs t = sl_text (prd_text t) cs t

-- | determines the sublogic for symbol map items

sl_symmap :: CommonLogicSL -> SYMB_MAP_ITEMS

-> CommonLogicSL

sl_symmap cs _ = cs

-- | determines the sublogic for a morphism

sl_mor :: CommonLogicSL -> Morphism -> CommonLogicSL

sl_mor cs _ = cs

-- | determines the sublogic for a Signature

sl_sig :: CommonLogicSL -> Sign -> CommonLogicSL

sl_sig cs _ = cs

-- | determines the sublogic for symbols

sl_sym :: CommonLogicSL -> Symbol -> CommonLogicSL

sl_sym cs _ = cs

-- | determines sublogic for texts, given predicates of the super-text

sl_text :: Set.Set NAME -> CommonLogicSL -> TEXT -> CommonLogicSL

sl_text prds cs t =

case t of

Text ps _ -> sl_phrases prds cs ps

Named_text _ nt _ -> sl_text prds cs nt

-- | determines sublogic for phrases, given predicates of the super-text

sl_phrases :: Set.Set NAME -> CommonLogicSL -> [PHRASE] -> CommonLogicSL

sl_phrases prds cs ps = foldl sublogics_max cs $ map (sl_phrase prds cs) ps

-- | determines sublogic for a single phrase, given predicates of the super-text

sl_phrase :: Set.Set NAME -> CommonLogicSL -> PHRASE -> CommonLogicSL

sl_phrase prds cs p =

case p of

Module m -> sl_module prds cs m

Sentence s -> sl_sentence prds cs s

Importation i -> sl_importation prds cs i

Comment_text _ t _ -> sl_text prds cs t

-- | determines sublogic for a module, given predicates of the super-text

sl_module :: Set.Set NAME -> CommonLogicSL -> MODULE -> CommonLogicSL

sl_module prds cs m =

case m of

Mod _ t _ -> sl_text prds cs t

Mod_ex _ _ t _ -> sl_text prds cs t

-- | determines sublogic for a sentence, given predicates of the super-text

sl_sentence :: Set.Set NAME -> CommonLogicSL -> SENTENCE -> CommonLogicSL

sl_sentence prds cs sen =

case sen of

Quant_sent q vs is _ -> sl_quantSent prds cs q vs is

Bool_sent b _ -> sl_boolSent prds cs b

Atom_sent a _ -> sl_atomSent prds cs a

Comment_sent _ s _ -> sl_sentence prds cs s

Irregular_sent s _ -> sl_sentence prds cs s

-- | determines the sublogic for importations (importations are ignored)

sl_importation :: Set.Set NAME -> CommonLogicSL -> IMPORTATION

-> CommonLogicSL

sl_importation _ cs _ = 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 prds cs _ noss s =

comp_list $ folsl : sl_sentence prds cs s

: map (sl_nameOrSeqmark prds cs) noss

{- | determines the sublogic for boolean sentences,

given predicates of the super-text -}

sl_boolSent :: Set.Set NAME -> CommonLogicSL -> BOOL_SENT -> CommonLogicSL

sl_boolSent prds cs b =

case b of

Junction _ ss -> comp_list $ map (sl_sentence prds cs) ss

Negation s -> sl_sentence prds cs s

BinOp _ s1 s2 ->

sublogics_max (sl_sentence prds cs s1) (sl_sentence prds cs s2)

{- | determines the sublogic for atoms,

given predicates of the super-text -}

sl_atomSent :: Set.Set NAME -> CommonLogicSL -> ATOM -> CommonLogicSL

sl_atomSent prds cs a =

case a of

Equation t1 t2 ->

comp_list $ folsl : map (sl_term prds cs) [t1, t2]

Atom t [] -> sl_term prds cs t

Atom t tseq -> slAppl prds cs t tseq

slAppl :: Set.Set NAME -> CommonLogicSL -> TERM -> [TERM_SEQ] -> CommonLogicSL

slAppl prds cs t tseq = comp_list

$ (if isNameTerm t then folsl else impsl)

: sl_term prds cs t : map (sl_termSeq prds cs) tseq

isNameTerm :: TERM -> Bool

isNameTerm term = case term of

Name_term _ -> True

Comment_term t _ _ -> isNameTerm t

_ -> 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 prds cs nos =

case nos of

Name n -> sl_quantName prds cs n

SeqMark _ -> cs { compact = 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 prds _ n = if Set.member n prds then impsl else folsl

{- | determines the sublogic for names,

given predicates of the super-text -}

sl_name :: Set.Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL

sl_name _ = sublogic_name

{- | determines the sublogic for names,

ignoring predicates -}

sublogic_name :: CommonLogicSL -> NAME -> CommonLogicSL

sublogic_name _ _ = propsl

{- | determines the sublogic for terms,

given predicates of the super-text -}

sl_term :: Set.Set NAME -> CommonLogicSL -> TERM -> CommonLogicSL

sl_term prds cs term =

case term of

Name_term n -> sl_name prds cs n

Funct_term t tseq _ -> slAppl prds cs t tseq

Comment_term t _ _ -> sl_term prds cs t

That_term {} -> impsl

{- | determines the sublogic for term sequences,

given predicates of the super-text -}

sl_termSeq :: Set.Set NAME -> CommonLogicSL -> TERM_SEQ -> CommonLogicSL

sl_termSeq prds cs tseq =

case tseq of

Term_seq t -> sl_termInSeq prds cs t

Seq_marks _ -> cs { compact = False }

{- | determines the sublogic for names,

given predicates of the super-text -}

sl_nameInTermSeq :: Set.Set NAME -> CommonLogicSL -> NAME -> CommonLogicSL

sl_nameInTermSeq prds _ n = if Set.member n prds then impsl else 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 prds cs term =

case term of

Name_term n -> sl_nameInTermSeq prds cs n

Funct_term t tseq _ ->

comp_list $ folsl : sl_term prds cs t : map (sl_termSeq prds cs) tseq

Comment_term t _ _ -> sl_term prds cs t

That_term {} -> impsl

-- | determines sublogic for basic items

sl_basic_items :: CommonLogicSL -> BASIC_ITEMS -> CommonLogicSL

sl_basic_items cs (Axiom_items axs) = comp_list $ map

(\ Annoted {item = tm} ->

uncurry (`sl_text` cs) $ getPreds $ getText tm

) axs

where getPreds :: TEXT -> (Set.Set NAME, TEXT)

getPreds txt = (prd_text txt, txt)

-- | determines sublogic for basic spec

sl_basic_spec :: CommonLogicSL -> BASIC_SPEC -> CommonLogicSL

sl_basic_spec cs (Basic_spec spec) =

comp_list $ map (sl_basic_items cs . item) spec

-- | determines sublogc for symb items

sl_symitems :: CommonLogicSL -> SYMB_ITEMS -> CommonLogicSL

sl_symitems _ (Symb_items noss _) =

comp_list $ map (sl_nameOrSeqmark Set.empty bottom) noss

{- -----------------------------------------------------------------------------

Conversion functions to String --

----------------------------------------------------------------------------- -}

-- | String representation of a Sublogic

sublogics_name :: CommonLogicSL -> String

sublogics_name f = show (format f) ++ if compact f then "" else "Seq"

{- -----------------------------------------------------------------------------

Projections to sublogics --

----------------------------------------------------------------------------- -}

-- | projection of a symbol to a sublogic

prSymbolM :: CommonLogicSL -> Symbol -> Maybe Symbol

prSymbolM _ = Just

prSymItemsM :: CommonLogicSL -> SYMB_ITEMS -> Maybe SYMB_ITEMS

prSymItemsM cs si@(Symb_items noss r) = case format cs of

Impredicative -> Just si

_ -> Just $ Symb_items (filter isName noss) r

where isName nos = case nos of

Name _ -> True

_ -> False

-- | projection of a signature to a sublogic

prSig :: CommonLogicSL -> Sign -> Sign

prSig _ = id

-- | projection of a morphism to a sublogic

prMor :: CommonLogicSL -> Morphism -> Morphism

prMor _ mor = mor

-- | projection of symb map items to a sublogic

prSymMapM :: CommonLogicSL

-> SYMB_MAP_ITEMS

-> Maybe SYMB_MAP_ITEMS

prSymMapM _ = Just

-- | projection of a name to a sublogic

prName :: CommonLogicSL -> NAME -> Maybe NAME

prName _ = 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 cs (Basic_spec items) = Basic_spec $ map (maybeLE cs) items

maybeLE :: CommonLogicSL -> Annoted BASIC_ITEMS -> Annoted BASIC_ITEMS

maybeLE cs = fmap $ \ (Axiom_items i) -> Axiom_items $ filter (isSL_LE cs) i

isSL_LE :: CommonLogicSL -> Annoted TEXT_META -> Bool

isSL_LE cs at = sublogic_text bottom (getText $ item at) <= cs