{-# 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 Int -> CASL2NNF -> ShowS
[CASL2NNF] -> ShowS
CASL2NNF -> String
(Int -> CASL2NNF -> ShowS)
-> (CASL2NNF -> String) -> ([CASL2NNF] -> ShowS) -> Show CASL2NNF
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [CASL2NNF] -> ShowS
$cshowList :: [CASL2NNF] -> ShowS
show :: CASL2NNF -> String
$cshow :: CASL2NNF -> String
showsPrec :: Int -> CASL2NNF -> ShowS
$cshowsPrec :: Int -> CASL2NNF -> ShowS
Show

instance Language CASL2NNF where
    language_name :: CASL2NNF -> String
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
sourceLogic CASL2NNF = CASL
CASL
    sourceSublogic :: CASL2NNF -> CASL_Sublogics
sourceSublogic CASL2NNF = CASL_Sublogics
forall a. Lattice a => CASL_SL a
SL.caslTop
    targetLogic :: CASL2NNF -> CASL
targetLogic CASL2NNF = CASL
CASL
    mapSublogic :: CASL2NNF -> CASL_Sublogics -> Maybe CASL_Sublogics
mapSublogic CASL2NNF sl :: CASL_Sublogics
sl = if CASL_Sublogics -> CASL_Formulas
forall a. CASL_SL a -> CASL_Formulas
SL.which_logic CASL_Sublogics
sl CASL_Formulas -> CASL_Formulas -> Bool
forall a. Eq a => a -> a -> Bool
== CASL_Formulas
SL.Horn 
                                then CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just (CASL_Sublogics -> Maybe CASL_Sublogics)
-> CASL_Sublogics -> Maybe CASL_Sublogics
forall a b. (a -> b) -> a -> b
$ CASL_Sublogics
sl {which_logic :: CASL_Formulas
SL.which_logic = CASL_Formulas
SL.FOL}
                                else CASL_Sublogics -> Maybe CASL_Sublogics
forall a. a -> Maybe a
Just CASL_Sublogics
sl
    map_theory :: CASL2NNF
-> (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
map_theory CASL2NNF = (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory
    map_morphism :: CASL2NNF -> CASLMor -> Result CASLMor
map_morphism CASL2NNF = CASLMor -> Result CASLMor
forall (m :: * -> *) a. Monad m => a -> m a
return -- morphisms are mapped identically
    map_sentence :: CASL2NNF -> CASLSign -> CASLFORMULA -> Result CASLFORMULA
map_sentence CASL2NNF _ s :: CASLFORMULA
s = CASLFORMULA -> Result CASLFORMULA
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLFORMULA -> Result CASLFORMULA)
-> CASLFORMULA -> Result CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> CASLFORMULA
negationNormalForm CASLFORMULA
s
    map_symbol :: CASL2NNF -> CASLSign -> Symbol -> Set Symbol
map_symbol CASL2NNF _ = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (Symbol -> Symbol) -> Symbol -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> Symbol
forall a. a -> a
id
    has_model_expansion :: CASL2NNF -> Bool
has_model_expansion CASL2NNF = Bool
True
    is_weakly_amalgamable :: CASL2NNF -> Bool
is_weakly_amalgamable CASL2NNF = Bool
True

mapTheory :: (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA])
mapTheory :: (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
mapTheory (sig :: CASLSign
sig, nsens :: [Named CASLFORMULA]
nsens) = do
 (CASLSign, [Named CASLFORMULA])
-> Result (CASLSign, [Named CASLFORMULA])
forall (m :: * -> *) a. Monad m => a -> m a
return (CASLSign
sig, (Named CASLFORMULA -> Named CASLFORMULA)
-> [Named CASLFORMULA] -> [Named CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (\nsen :: Named CASLFORMULA
nsen -> Named CASLFORMULA
nsen{sentence :: CASLFORMULA
sentence = CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Named CASLFORMULA -> CASLFORMULA
forall s a. SenAttr s a -> s
sentence Named CASLFORMULA
nsen}) [Named CASLFORMULA]
nsens)

-- nnf, implemented recursively

negationNormalForm :: CASLFORMULA -> CASLFORMULA
negationNormalForm :: CASLFORMULA -> CASLFORMULA
negationNormalForm sen :: CASLFORMULA
sen = case CASLFORMULA
sen of
 Quantification q :: QUANTIFIER
q vars :: [VAR_DECL]
vars qsen :: CASLFORMULA
qsen _ ->
   QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
vars (CASLFORMULA -> CASLFORMULA
negationNormalForm CASLFORMULA
qsen) Range
nullRange
 Junction j :: Junctor
j sens :: [CASLFORMULA]
sens _ ->
   Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
j ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map CASLFORMULA -> CASLFORMULA
negationNormalForm [CASLFORMULA]
sens) Range
nullRange
 Relation sen1 :: CASLFORMULA
sen1 Implication sen2 :: CASLFORMULA
sen2 _ ->
   let sen1' :: CASLFORMULA
sen1' = CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$
                CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (CASLFORMULA -> CASLFORMULA
negationNormalForm CASLFORMULA
sen1) Range
nullRange
       sen2' :: CASLFORMULA
sen2' = CASLFORMULA -> CASLFORMULA
negationNormalForm CASLFORMULA
sen2
   in Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis [CASLFORMULA
sen1', CASLFORMULA
sen2'] Range
nullRange
 -- During parsing, "f2 if f1" is saved as "Relation f1 RevImpl f2 _"
 Relation sen1 :: CASLFORMULA
sen1 RevImpl sen2 :: CASLFORMULA
sen2 _ ->
   let sen1' :: CASLFORMULA
sen1' = CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$
                CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (CASLFORMULA -> CASLFORMULA
negationNormalForm CASLFORMULA
sen1) Range
nullRange
       sen2' :: CASLFORMULA
sen2' = CASLFORMULA -> CASLFORMULA
negationNormalForm CASLFORMULA
sen2
   in Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis [CASLFORMULA
sen1', CASLFORMULA
sen2'] Range
nullRange
 Relation sen1 :: CASLFORMULA
sen1 Equivalence sen2 :: CASLFORMULA
sen2 _ ->
   let sen1' :: CASLFORMULA
sen1' = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen1 Relation
Implication CASLFORMULA
sen2 Range
nullRange
       sen2' :: CASLFORMULA
sen2' = CASLFORMULA -> Relation -> CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Relation -> FORMULA f -> Range -> FORMULA f
Relation CASLFORMULA
sen2 Relation
Implication CASLFORMULA
sen1 Range
nullRange
   in CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [CASLFORMULA
sen1', CASLFORMULA
sen2'] Range
nullRange
 Negation (Negation sen' :: CASLFORMULA
sen' _) _ ->
   CASLFORMULA -> CASLFORMULA
negationNormalForm CASLFORMULA
sen'
 Negation (Junction j :: Junctor
j sens :: [CASLFORMULA]
sens _) _ ->
   Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction (Junctor -> Junctor
dualJunctor Junctor
j)
     ((CASLFORMULA -> CASLFORMULA) -> [CASLFORMULA] -> [CASLFORMULA]
forall a b. (a -> b) -> [a] -> [b]
map (\x :: CASLFORMULA
x -> CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
x Range
nullRange) [CASLFORMULA]
sens)
     Range
nullRange
 Negation (Quantification Unique_existential _vars :: [VAR_DECL]
_vars _sen :: CASLFORMULA
_sen _) _->
    String -> CASLFORMULA
forall a. HasCallStack => String -> a
error "negation normal form for unique existentials nyi"
 Negation (Quantification q :: QUANTIFIER
q vars :: [VAR_DECL]
vars qsen :: CASLFORMULA
qsen _) _ ->
   QUANTIFIER -> [VAR_DECL] -> CASLFORMULA -> Range -> CASLFORMULA
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification (QUANTIFIER -> QUANTIFIER
dualQuant QUANTIFIER
q) [VAR_DECL]
vars
     (CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
qsen Range
nullRange)
     Range
nullRange
 Negation (Relation sen1 :: CASLFORMULA
sen1 Implication sen2 :: CASLFORMULA
sen2 _) _ ->  
  CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ 
    CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis [CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
sen1 Range
nullRange, CASLFORMULA
sen2] Range
nullRange) Range
nullRange
 Negation (Relation sen1 :: CASLFORMULA
sen1 RevImpl sen2 :: CASLFORMULA
sen2 _) _ ->  
  CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$ 
    CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis [CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
sen2 Range
nullRange, CASLFORMULA
sen1] Range
nullRange) Range
nullRange
 Negation (Relation sen1 :: CASLFORMULA
sen1 Equivalence sen2 :: CASLFORMULA
sen2 _) _ -> 
  CASLFORMULA -> CASLFORMULA
negationNormalForm (CASLFORMULA -> CASLFORMULA) -> CASLFORMULA -> CASLFORMULA
forall a b. (a -> b) -> a -> b
$
    CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation (Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Con [Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis [CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
sen1 Range
nullRange, CASLFORMULA
sen2] Range
nullRange,
                            Junctor -> [CASLFORMULA] -> Range -> CASLFORMULA
forall f. Junctor -> [FORMULA f] -> Range -> FORMULA f
Junction Junctor
Dis [CASLFORMULA -> Range -> CASLFORMULA
forall f. FORMULA f -> Range -> FORMULA f
Negation CASLFORMULA
sen2 Range
nullRange, CASLFORMULA
sen1] Range
nullRange] 
              Range
nullRange) 
    Range
nullRange
 x :: CASLFORMULA
x -> CASLFORMULA
x