05bf9cbe382548c2665dd01a6a402640c9ec3813Christian Maeder{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder{- |

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederModule : $Header$

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederDescription : negation normal form

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederCopyright : (c) Mihai Codescu, 2016

98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu ProdescuLicense : GPLv2 or higher, see LICENSE.txt

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederMaintainer : codescu@iws.cs.uni-magdeburg.de

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederStability : provisional

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaederPortability : non-portable (imports Logic.Comorphism)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-}

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maedermodule Comorphisms.CASL2NNF where

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Logic.Logic

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Logic.Comorphism

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CASL.Logic_CASL

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CASL.AS_Basic_CASL

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CASL.Sign

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CASL.Morphism

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport CASL.Sublogic as SL hiding (bottom)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport Common.Result

33bdce26495121cdbce30331ef90a1969126a840Liam O'Reillyimport Common.Id

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport qualified Data.Set as Set

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Common.AS_Annotation

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederimport Common.ProofTree

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederdata CASL2NNF = CASL2NNF deriving Show

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederinstance Language CASL2NNF where

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder language_name CASL2NNF = "CASL2NNF"

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maederinstance Comorphism CASL2NNF

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder CASL CASL_Sublogics

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder CASLSign

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder CASLMor

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder Symbol RawSymbol ProofTree

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder CASL CASL_Sublogics

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder CASLSign

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder CASLMor

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder Symbol RawSymbol ProofTree where

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder sourceLogic CASL2NNF = CASL

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder sourceSublogic CASL2NNF = SL.caslTop

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder targetLogic CASL2NNF = CASL

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder mapSublogic CASL2NNF sl = if SL.which_logic sl == SL.Horn

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder then Just $ sl {SL.which_logic = SL.FOL}

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder else Just sl

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder map_theory CASL2NNF = mapTheory

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder map_morphism CASL2NNF = return -- morphisms are mapped identically

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder map_sentence CASL2NNF _ s = return $ negationNormalForm s

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder map_symbol CASL2NNF _ = Set.singleton . id

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder has_model_expansion CASL2NNF = True

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder is_weakly_amalgamable CASL2NNF = True

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaedermapTheory :: (CASLSign, [Named CASLFORMULA]) -> Result (CASLSign, [Named CASLFORMULA])

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaedermapTheory (sig, nsens) = do

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder return (sig, map (\nsen -> nsen{sentence = negationNormalForm $ sentence nsen}) nsens)

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder-- nnf, implemented recursively

400321fd7a25a1c34eb95855ee86daf722734bd4Mihai Codescu

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaedernegationNormalForm :: CASLFORMULA -> CASLFORMULA

286f4deb69d3912337bb09dd7f81284d12912ce8Christian MaedernegationNormalForm sen = case sen of

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder Quantification q vars qsen _ ->

286f4deb69d3912337bb09dd7f81284d12912ce8Christian Maeder 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