{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
{- |
Module      :  $Header$
Description :  Coding of a CASL sublogic to Propositional
Copyright   :  (c) Dominik Luecke and Uni Bremen 2007
License     :  GPLv2 or higher, see LICENSE.txt

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

A comorphism from CASL to Propositional. The CASL sublogic does not precisely
capture the valid domain of the translation. Sorts, ops and preds with
arguments will be ignored. The translation will fail for non-propositional
sentences.
-}

module Comorphisms.CASL2Prop (CASL2Prop (..)) where

import Common.ProofTree

import Logic.Logic
import Logic.Comorphism

-- 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

-- CASL
import CASL.Logic_CASL
import CASL.AS_Basic_CASL
import CASL.Sublogic
import CASL.Sign
import CASL.Morphism

import qualified Data.Set as Set
import qualified Data.Map as Map
import Common.AS_Annotation
import Common.Id
import Common.Result
import Common.DocUtils
import qualified Common.Lib.MapSet as MapSet

-- | lid of the morphism
data CASL2Prop = CASL2Prop deriving Show

instance Language CASL2Prop where
  language_name CASL2Prop = "CASL2Propositional"

instance Comorphism CASL2Prop
    CASL
    CASL_Sublogics
    CASLBasicSpec
    CASLFORMULA
    SYMB_ITEMS
    SYMB_MAP_ITEMS
    CASLSign
    CASLMor
    Symbol
    RawSymbol
    ProofTree
    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
    where
      sourceLogic CASL2Prop = CASL
      sourceSublogic CASL2Prop = sublogics_max need_fol need_pred
      targetLogic CASL2Prop = PLogic.Propositional
      mapSublogic CASL2Prop = Just . mapSub
      map_theory CASL2Prop = mapTheory
      is_model_transportable CASL2Prop = True
      map_symbol CASL2Prop _ = mapSym
      map_sentence CASL2Prop _ = trForm
      map_morphism CASL2Prop = mapMor
      has_model_expansion CASL2Prop = False
      is_weakly_amalgamable CASL2Prop = True
      isInclusionComorphism CASL2Prop = False

-- | Translation of the signature
mapSig :: CASLSign -> PSign.Sign
mapSig = PSign.Sign . MapSet.keysSet
  . MapSet.filter (null . predArgs) . predMap

-- | Which is the target sublogic?
mapSub :: CASL_Sublogics -> PSL.PropSL
mapSub sl = if which_logic sl <= Horn then PSL.bottom else PSL.top

-- | Translation of morphisms
mapMor :: CASLMor -> Result PMor.Morphism
mapMor mor = return PMor.Morphism
  { PMor.source = mapSig (msource mor)
  , PMor.target = mapSig (mtarget mor)
  , PMor.propMap = Map.foldWithKey (\ (i, pt) j ->
      if null (predArgs pt) then Map.insert i j else id) Map.empty
      $ pred_map mor }

-- | Mapping of a theory
mapTheory :: (CASLSign, [Named CASLFORMULA])
  -> Result (PSign.Sign, [Named PBasic.FORMULA])
mapTheory (sig, form) = do
  sens <- mapM trNamedForm form
  return (mapSig sig, sens)

-- | Translation of symbols
mapSym :: Symbol -> Set.Set PSymbol.Symbol
mapSym sym = case symbType sym of
  PredAsItemType pt | null $ predArgs pt ->
    Set.singleton (PSymbol.Symbol $ symName sym)
  _ -> Set.empty

-- | Helper for map theory
trNamedForm :: Named CASLFORMULA -> Result (Named PBasic.FORMULA)
trNamedForm = mapNamedM trForm

-- | Helper for map sentence and map theory
trForm :: CASLFORMULA -> Result PBasic.FORMULA
trForm form = case form of
  Negation fn rn -> do
    t <- trForm fn
    return $ PBasic.Negation t rn
  Junction j fn rn -> do
    ts <- mapM trForm fn
    return $ (case j of
      Con -> PBasic.Conjunction
      Dis -> PBasic.Disjunction) ts rn
  Relation f1 c f2 rn -> do
    t1 <- trForm f1
    t2 <- trForm f2
    return $ (if c == Equivalence then PBasic.Equivalence else
      PBasic.Implication) t1 t2 rn
  Atom b rn -> return $ (if b then PBasic.True_atom else PBasic.False_atom) rn
  Predication (Qual_pred_name pid (Pred_type [] _) _) [] _ ->
    return . PBasic.Predication . mkSimpleId $ show pid
  _ -> fail $ "not a propositional formula: " ++ showDoc form ""
