{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
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 Show

instance Language Prop2CommonLogic where
  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 = PLogic.Propositional
      sourceSublogic Prop2CommonLogic = PSL.top
      targetLogic Prop2CommonLogic = ClLogic.CommonLogic
      mapSublogic Prop2CommonLogic = Just . mapSub
      map_theory Prop2CommonLogic = mapTheory
      map_sentence Prop2CommonLogic = mapSentence
      map_morphism Prop2CommonLogic = mapMor

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

mapMor :: PMor.Morphism -> Result ClMor.Morphism
mapMor mor =
  let src = mapSign $ PMor.source mor
      tgt = mapSign $ PMor.target mor
      pmp = PMor.propMap mor
  in  return $ ClMor.Morphism src tgt pmp

mapSentence :: PSign.Sign -> PBasic.FORMULA -> Result TEXT_META
mapSentence _ f = return $ translate f

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

baseSig :: ClSign.Sign
baseSig = ClSign.emptySig {
    ClSign.discourseNames = Set.fromList [simpleIdToId xName, simpleIdToId yName]
  }

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

translate :: PBasic.FORMULA -> TEXT_META
translate f =
  emptyTextMeta {
        getText = Text [Sentence singletonUniv, Sentence $ toSen f] nullRange
  }
  where singletonUniv = Quant_sent (Universal [Name xName, Name yName]
            $ Atom_sent (Equation (Name_term xName) (Name_term yName)) nullRange
          ) nullRange

toSen :: PBasic.FORMULA -> SENTENCE
toSen x = case x of
  PBasic.False_atom _ -> Bool_sent (Negation clTrue) nullRange
  PBasic.True_atom _ -> clTrue
  PBasic.Predication n -> Atom_sent (Atom (Name_term n) []) nullRange
  PBasic.Negation f _ -> Bool_sent (Negation $ toSen f) nullRange
  PBasic.Conjunction fs _ -> Bool_sent (Conjunction $ map toSen fs) nullRange
  PBasic.Disjunction fs _ -> Bool_sent (Disjunction $ map toSen fs) nullRange
  PBasic.Implication f1 f2 _ ->
    Bool_sent (Implication (toSen f1) (toSen f2)) nullRange
  PBasic.Equivalence f1 f2 _ ->
    Bool_sent (Biconditional (toSen f1) (toSen f2)) nullRange

clTrue :: SENTENCE --forall x. x=x
clTrue = Quant_sent (Universal [Name xName]
            $ Atom_sent (Equation (Name_term xName) (Name_term xName)) nullRange
          ) nullRange

xName :: NAME
xName = mkSimpleId "x"

yName :: NAME
yName = mkSimpleId "y"
