content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
  {- |
  Module      :  $Header$
  Description :  negation normal form
  Copyright   :  (c) Mihai Codescu, 2016
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  codescu@iws.cs.uni-magdeburg.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Comorphism)
  
  -}
  
  module Comorphisms.CASL2NNF where
  
  import Logic.Logic
  import Logic.Comorphism
  
  import CASL.Logic_CASL
  import CASL.AS_Basic_CASL
  import CASL.Sign
  import CASL.Morphism
  import CASL.Sublogic as SL hiding (bottom)
  
  import Common.Result
  import Common.Id
  import qualified Data.Set as Set
  import Common.AS_Annotation
  import Common.ProofTree
  
  data CASL2NNF = CASL2NNF deriving Show
  
  instance Language CASL2NNF where
      language_name CASL2NNF = "CASL2NNF"
  
  instance Comorphism CASL2NNF
                 CASL CASL_Sublogics
                 CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 CASLSign
                 CASLMor
                 Symbol RawSymbol ProofTree
                 CASL CASL_Sublogics
                 CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS
                 CASLSign
                 CASLMor
                 Symbol RawSymbol ProofTree where
      sourceLogic CASL2NNF = CASL
      sourceSublogic CASL2NNF = SL.caslTop
      targetLogic CASL2NNF = CASL
      mapSublogic CASL2NNF sl = if SL.which_logic sl == SL.Horn 
                                  then Just $ sl {SL.which_logic = SL.FOL}
                                  else Just sl
      map_theory CASL2NNF = mapTheory
      map_morphism CASL2NNF = return -- morphisms are mapped identically
      map_sentence CASL2NNF _ s = return $ negationNormalForm s
      map_symbol CASL2NNF _ = Set.singleton . id
      has_model_expansion CASL2NNF = True
      is_weakly_amalgamable CASL2NNF = True
  
  mapTheory :: (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA])
  mapTheory (sig, nsens) = do
   return (sig, map (\nsen -> nsen{sentence = negationNormalForm $ sentence nsen}) nsens)
  
  -- nnf, implemented recursively
  
  negationNormalForm :: CASLFORMULA -> CASLFORMULA
  negationNormalForm sen = case sen of
   Quantification q vars qsen _ ->
     Quantification q vars (negationNormalForm qsen) nullRange
   Junction j sens _ ->
     Junction j (map negationNormalForm sens) nullRange
   Relation sen1 Implication sen2 _ ->
     let sen1' = negationNormalForm $
                  Negation (negationNormalForm sen1) nullRange
         sen2' = negationNormalForm sen2
     in Junction Dis [sen1', sen2'] nullRange
   -- During parsing, "f2 if f1" is saved as "Relation f1 RevImpl f2 _"
   Relation sen1 RevImpl sen2 _ ->
     let sen1' = negationNormalForm $
                  Negation (negationNormalForm sen1) nullRange
         sen2' = negationNormalForm sen2
     in Junction Dis [sen1', sen2'] nullRange
   Relation sen1 Equivalence sen2 _ ->
     let sen1' = Relation sen1 Implication sen2 nullRange
         sen2' = Relation sen2 Implication sen1 nullRange
     in negationNormalForm $ Junction Con [sen1', sen2'] nullRange
   Negation (Negation sen' _) _ ->
     negationNormalForm sen'
   Negation (Junction j sens _) _ ->
     Junction (dualJunctor j)
       (map (\x -> negationNormalForm $ Negation x nullRange) sens)
       nullRange
   Negation (Quantification Unique_existential _vars _sen _) _->
      error "negation normal form for unique existentials nyi"
   Negation (Quantification q vars qsen _) _ ->
     Quantification (dualQuant q) vars
       (negationNormalForm $ Negation qsen nullRange)
       nullRange
   Negation (Relation sen1 Implication sen2 _) _ ->  
    negationNormalForm $ 
      Negation (Junction Dis [Negation sen1 nullRange, sen2] nullRange) nullRange
   Negation (Relation sen1 RevImpl sen2 _) _ ->  
    negationNormalForm $ 
      Negation (Junction Dis [Negation sen2 nullRange, sen1] nullRange) nullRange
   Negation (Relation sen1 Equivalence sen2 _) _ -> 
    negationNormalForm $
      Negation (Junction Con [Junction Dis [Negation sen1 nullRange, sen2] nullRange,
                              Junction Dis [Negation sen2 nullRange, sen1] nullRange] 
                nullRange) 
      nullRange
   x -> x
  