content: {-# 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 (Show, Eq, Ord, Enum, Bounded, Typeable)
  
  -- for comparison of sublogics use the Ord instance
  
  -- | sublogics for CommonLogic
  data CommonLogicSL = CommonLogicSL
      { format :: CLTextType     -- Structural restrictions
      , compact :: Bool
      } deriving (Show, Eq, Ord, Typeable)
  
  -- | 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
  
  -- check for a curried name application
  isNameTerm :: TERM -> Bool
  isNameTerm term = case term of
    Name_term _ -> True
    Comment_term t _ _ -> isNameTerm t
    Funct_term t _ _ -> isNameTerm t
    That_term {} -> 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
  