{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  ./Comorphisms/Prop2CommonLogic.hs
Description :  Coding of Propositional into CommonLogic
Copyright   :  (c) Eugen Kuksa and Uni Bremen 2011
License     :  GPLv2 or higher, see LICENSE.txt

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

The translating comorphism from Propositional to CommonLogic.
-}

module Comorphisms.Prop2CommonLogic
    (
     Prop2CommonLogic (..)
    )
    where

import Common.ProofTree
import Common.Id
import Common.Result
import qualified Common.AS_Annotation as AS_Anno

import Logic.Logic
import Logic.Comorphism

import qualified Data.Set as Set (fromList)

-- Propositional
import qualified Propositional.Logic_Propositional as PLogic
import qualified Propositional.AS_BASIC_Propositional as PBasic
import qualified Propositional.Sublogic as PSL
import qualified Propositional.Sign as PSign
import qualified Propositional.Morphism as PMor
import qualified Propositional.Symbol as PSymbol

-- CommonLogic
import CommonLogic.AS_CommonLogic
import qualified CommonLogic.Logic_CommonLogic as ClLogic
import qualified CommonLogic.Sign as ClSign
import qualified CommonLogic.Symbol as ClSymbol
import qualified CommonLogic.Morphism as ClMor
import qualified CommonLogic.Sublogic as ClSL

-- | lid of the morphism
data Prop2CommonLogic = Prop2CommonLogic deriving Int -> Prop2CommonLogic -> ShowS
[Prop2CommonLogic] -> ShowS
Prop2CommonLogic -> String
(Int -> Prop2CommonLogic -> ShowS)
-> (Prop2CommonLogic -> String)
-> ([Prop2CommonLogic] -> ShowS)
-> Show Prop2CommonLogic
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Prop2CommonLogic] -> ShowS
$cshowList :: [Prop2CommonLogic] -> ShowS
show :: Prop2CommonLogic -> String
$cshow :: Prop2CommonLogic -> String
showsPrec :: Int -> Prop2CommonLogic -> ShowS
$cshowsPrec :: Int -> Prop2CommonLogic -> ShowS
Show

instance Language Prop2CommonLogic where
  language_name :: Prop2CommonLogic -> String
language_name Prop2CommonLogic = "Propositional2CommonLogic"

instance Comorphism Prop2CommonLogic
    PLogic.Propositional
    PSL.PropSL
    PBasic.BASIC_SPEC
    PBasic.FORMULA
    PBasic.SYMB_ITEMS
    PBasic.SYMB_MAP_ITEMS
    PSign.Sign
    PMor.Morphism
    PSymbol.Symbol
    PSymbol.Symbol
    ProofTree
    ClLogic.CommonLogic     -- lid domain
    ClSL.CommonLogicSL      -- sublogics codomain
    BASIC_SPEC              -- Basic spec domain
    TEXT_META               -- sentence domain
    SYMB_ITEMS              -- symb_items
    SYMB_MAP_ITEMS          -- symbol map items domain
    ClSign.Sign             -- signature domain
    ClMor.Morphism          -- morphism domain
    ClSymbol.Symbol         -- symbol domain
    ClSymbol.Symbol         -- rawsymbol domain
    ProofTree               -- proof tree codomain
    where
      sourceLogic :: Prop2CommonLogic -> Propositional
sourceLogic Prop2CommonLogic = Propositional
PLogic.Propositional
      sourceSublogic :: Prop2CommonLogic -> PropSL
sourceSublogic Prop2CommonLogic = PropSL
PSL.top
      targetLogic :: Prop2CommonLogic -> CommonLogic
targetLogic Prop2CommonLogic = CommonLogic
ClLogic.CommonLogic
      mapSublogic :: Prop2CommonLogic -> PropSL -> Maybe CommonLogicSL
mapSublogic Prop2CommonLogic = CommonLogicSL -> Maybe CommonLogicSL
forall a. a -> Maybe a
Just (CommonLogicSL -> Maybe CommonLogicSL)
-> (PropSL -> CommonLogicSL) -> PropSL -> Maybe CommonLogicSL
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PropSL -> CommonLogicSL
mapSub
      map_theory :: Prop2CommonLogic
-> (Sign, [Named FORMULA]) -> Result (Sign, [Named TEXT_META])
map_theory Prop2CommonLogic = (Sign, [Named FORMULA]) -> Result (Sign, [Named TEXT_META])
mapTheory
      map_sentence :: Prop2CommonLogic -> Sign -> FORMULA -> Result TEXT_META
map_sentence Prop2CommonLogic = Sign -> FORMULA -> Result TEXT_META
mapSentence
      map_morphism :: Prop2CommonLogic -> Morphism -> Result Morphism
map_morphism Prop2CommonLogic = Morphism -> Result Morphism
mapMor

mapSub :: PSL.PropSL -> ClSL.CommonLogicSL
mapSub :: PropSL -> CommonLogicSL
mapSub _ = CommonLogicSL
ClSL.folsl

mapMor :: PMor.Morphism -> Result ClMor.Morphism
mapMor :: Morphism -> Result Morphism
mapMor mor :: Morphism
mor =
  let src :: Sign
src = Sign -> Sign
mapSign (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
PMor.source Morphism
mor
      tgt :: Sign
tgt = Sign -> Sign
mapSign (Sign -> Sign) -> Sign -> Sign
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
PMor.target Morphism
mor
      pmp :: Map Id Id
pmp = Morphism -> Map Id Id
PMor.propMap Morphism
mor
  in Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Map Id Id -> Morphism
ClMor.Morphism Sign
src Sign
tgt Map Id Id
pmp

mapSentence :: PSign.Sign -> PBasic.FORMULA -> Result TEXT_META
mapSentence :: Sign -> FORMULA -> Result TEXT_META
mapSentence _ f :: FORMULA
f = TEXT_META -> Result TEXT_META
forall (m :: * -> *) a. Monad m => a -> m a
return (TEXT_META -> Result TEXT_META) -> TEXT_META -> Result TEXT_META
forall a b. (a -> b) -> a -> b
$ FORMULA -> TEXT_META
translate FORMULA
f

mapSign :: PSign.Sign -> ClSign.Sign
mapSign :: Sign -> Sign
mapSign sig :: Sign
sig =
  Sign -> Sign -> Sign
ClSign.unite (Sign
ClSign.emptySig {
      discourseNames :: Set Id
ClSign.discourseNames = Sign -> Set Id
PSign.items Sign
sig
    }) Sign
baseSig

baseSig :: ClSign.Sign
baseSig :: Sign
baseSig = Sign
ClSign.emptySig {
    discourseNames :: Set Id
ClSign.discourseNames = [Id] -> Set Id
forall a. Ord a => [a] -> Set a
Set.fromList [SIMPLE_ID -> Id
simpleIdToId SIMPLE_ID
xName, SIMPLE_ID -> Id
simpleIdToId SIMPLE_ID
yName]
  }

mapTheory :: (PSign.Sign, [AS_Anno.Named PBasic.FORMULA])
             -> Result (ClSign.Sign, [AS_Anno.Named TEXT_META])
mapTheory :: (Sign, [Named FORMULA]) -> Result (Sign, [Named TEXT_META])
mapTheory (srcSign :: Sign
srcSign, srcFormulas :: [Named FORMULA]
srcFormulas) =
  (Sign, [Named TEXT_META]) -> Result (Sign, [Named TEXT_META])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign -> Sign
mapSign Sign
srcSign,
        (Named FORMULA -> Named TEXT_META)
-> [Named FORMULA] -> [Named TEXT_META]
forall a b. (a -> b) -> [a] -> [b]
map ((String -> TEXT_META -> Named TEXT_META)
-> (String, TEXT_META) -> Named TEXT_META
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry String -> TEXT_META -> Named TEXT_META
forall a s. a -> s -> SenAttr s a
AS_Anno.makeNamed ((String, TEXT_META) -> Named TEXT_META)
-> (Named FORMULA -> (String, TEXT_META))
-> Named FORMULA
-> Named TEXT_META
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (String, FORMULA) -> (String, TEXT_META)
transSnd ((String, FORMULA) -> (String, TEXT_META))
-> (Named FORMULA -> (String, FORMULA))
-> Named FORMULA
-> (String, TEXT_META)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named FORMULA -> (String, FORMULA)
senAndName) [Named FORMULA]
srcFormulas)
  where senAndName :: AS_Anno.Named PBasic.FORMULA -> (String, PBasic.FORMULA)
        senAndName :: Named FORMULA -> (String, FORMULA)
senAndName f :: Named FORMULA
f = (Named FORMULA -> String
forall s a. SenAttr s a -> a
AS_Anno.senAttr Named FORMULA
f, Named FORMULA -> FORMULA
forall s a. SenAttr s a -> s
AS_Anno.sentence Named FORMULA
f)
        transSnd :: (String, PBasic.FORMULA) -> (String, TEXT_META)
        transSnd :: (String, FORMULA) -> (String, TEXT_META)
transSnd (s :: String
s, f :: FORMULA
f) = (String
s, FORMULA -> TEXT_META
translate FORMULA
f)

translate :: PBasic.FORMULA -> TEXT_META
translate :: FORMULA -> TEXT_META
translate f :: FORMULA
f =
  TEXT_META
emptyTextMeta {
        getText :: TEXT
getText = [PHRASE] -> Range -> TEXT
Text [SENTENCE -> PHRASE
Sentence SENTENCE
singletonUniv, SENTENCE -> PHRASE
Sentence (SENTENCE -> PHRASE) -> SENTENCE -> PHRASE
forall a b. (a -> b) -> a -> b
$ FORMULA -> SENTENCE
toSen FORMULA
f] Range
nullRange
  }
  where singletonUniv :: SENTENCE
singletonUniv = QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal [SIMPLE_ID -> NAME_OR_SEQMARK
Name SIMPLE_ID
xName, SIMPLE_ID -> NAME_OR_SEQMARK
Name SIMPLE_ID
yName]
                        (ATOM -> Range -> SENTENCE
Atom_sent (TERM -> TERM -> ATOM
Equation
                                    (SIMPLE_ID -> TERM
Name_term SIMPLE_ID
xName)
                                    (SIMPLE_ID -> TERM
Name_term SIMPLE_ID
yName)) Range
nullRange) Range
nullRange

toSen :: PBasic.FORMULA -> SENTENCE
toSen :: FORMULA -> SENTENCE
toSen x :: FORMULA
x = case FORMULA
x of
  PBasic.False_atom _ -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (SENTENCE -> BOOL_SENT
Negation SENTENCE
clTrue) Range
nullRange
  PBasic.True_atom _ -> SENTENCE
clTrue
  PBasic.Predication n :: SIMPLE_ID
n -> ATOM -> Range -> SENTENCE
Atom_sent (TERM -> [TERM_SEQ] -> ATOM
Atom (SIMPLE_ID -> TERM
Name_term SIMPLE_ID
n) []) Range
nullRange
  PBasic.Negation f :: FORMULA
f _ -> BOOL_SENT -> Range -> SENTENCE
Bool_sent (SENTENCE -> BOOL_SENT
Negation (SENTENCE -> BOOL_SENT) -> SENTENCE -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$ FORMULA -> SENTENCE
toSen FORMULA
f) Range
nullRange
  PBasic.Conjunction fs :: [FORMULA]
fs _ ->
    BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Conjunction ([SENTENCE] -> BOOL_SENT) -> [SENTENCE] -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$ (FORMULA -> SENTENCE) -> [FORMULA] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> SENTENCE
toSen [FORMULA]
fs) Range
nullRange
  PBasic.Disjunction fs :: [FORMULA]
fs _ ->
    BOOL_SENT -> Range -> SENTENCE
Bool_sent (AndOr -> [SENTENCE] -> BOOL_SENT
Junction AndOr
Disjunction ([SENTENCE] -> BOOL_SENT) -> [SENTENCE] -> BOOL_SENT
forall a b. (a -> b) -> a -> b
$ (FORMULA -> SENTENCE) -> [FORMULA] -> [SENTENCE]
forall a b. (a -> b) -> [a] -> [b]
map FORMULA -> SENTENCE
toSen [FORMULA]
fs) Range
nullRange
  PBasic.Implication f1 :: FORMULA
f1 f2 :: FORMULA
f2 _ ->
    BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Implication (FORMULA -> SENTENCE
toSen FORMULA
f1) (FORMULA -> SENTENCE
toSen FORMULA
f2)) Range
nullRange
  PBasic.Equivalence f1 :: FORMULA
f1 f2 :: FORMULA
f2 _ ->
    BOOL_SENT -> Range -> SENTENCE
Bool_sent (ImplEq -> SENTENCE -> SENTENCE -> BOOL_SENT
BinOp ImplEq
Biconditional (FORMULA -> SENTENCE
toSen FORMULA
f1) (FORMULA -> SENTENCE
toSen FORMULA
f2)) Range
nullRange

clTrue :: SENTENCE -- forall x. x=x
clTrue :: SENTENCE
clTrue = QUANT -> [NAME_OR_SEQMARK] -> SENTENCE -> Range -> SENTENCE
Quant_sent QUANT
Universal [SIMPLE_ID -> NAME_OR_SEQMARK
Name SIMPLE_ID
xName]
         (ATOM -> Range -> SENTENCE
Atom_sent (TERM -> TERM -> ATOM
Equation (SIMPLE_ID -> TERM
Name_term SIMPLE_ID
xName) (SIMPLE_ID -> TERM
Name_term SIMPLE_ID
xName))
          Range
nullRange) Range
nullRange

xName :: NAME
xName :: SIMPLE_ID
xName = String -> SIMPLE_ID
mkSimpleId "x"

yName :: NAME
yName :: SIMPLE_ID
yName = String -> SIMPLE_ID
mkSimpleId "y"