d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann{- | Module : $Header$

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Description : Implementation of logic instance Mon

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Copyright : (c) Daniel Hausmann & Georgel Calin & Lutz Schroeder, DFKI Lab Bremen,

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder - Rob Myers & Dirk Pattinson, Department of Computing, ICL

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

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Maintainer : hausmann@dfki.de

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Stability : provisional

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Portability : portable

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann -

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann - Provides the implementation of the matching functions monotonic modal logic.

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann -}

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, FlexibleContexts #-}

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannmodule GMP.Logics.Mon where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.List

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Ratio

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederimport Data.Maybe

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannimport Debug.Trace

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannimport Text.ParserCombinators.Parsec

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannimport GMP.Logics.Generic

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmannimport GMP.Parser

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ------------------------------------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance of feature for Monotonic logic

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------------------------------------------------------------------ -}

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederdata Mon a = Mon [Formula a] deriving (Eq, Show)

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- For any combination of a positive and a negative literal, there is a premise

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedercontaining only one sequent. This sequent contains only one formula over the

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederstripped positive literal and the negated stripped negative literal.

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedere.g. seq = [ (M Mon p), !(M Mon q), (M Mon !p), !(M Mon !r)]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroedermatch seq = [ [[ p, !q]], [[p, r]], [[ !p, !q]], [[ !p, r]] ] -}

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmanninstance (SigFeature b c d, Eq (b (c d)), Eq (c d)) => NonEmptyFeature Mon b c d where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder nefMatch flags seq =

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder let stripnlits = [ Neg (head phi) | Neg (Mod (Mon phi)) <- seq]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder striplits = [ head phi | Mod (Mon phi) <- seq]

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder in [ [[Sequent [Neg (And (Neg neg) (Neg pos))]]] |

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder neg <- stripnlits, pos <- striplits]

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefPretty d = genfPretty d "[Mon]"

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefFeatureFromSignature sig = Mon

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefFeatureFromFormula phi = Mon

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann nefStripFeature (Mon phis) = phis

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder{- ------------------------------------------------------------------------------

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroederinstance of sigFeature for Monotonic logic

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder------------------------------------------------------------------------------ -}

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmann

d1767fe15b7c3960e36996cc02977c0480ab4b17Daniel Hausmanninstance (SigFeature b c d, Eq (c d), Eq (b (c d))) => NonEmptySigFeature Mon b c d where

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder neGoOn = genericPGoOn