{-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances, FlexibleInstances #-}
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
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)
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
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