4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder{-# OPTIONS -fallow-undecidable-instances #-}

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder{- |

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederModule : $Header$

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederDescription : Instance of class Logic for propositional logic

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederCopyright : (c) Dominik Luecke, Uni Bremen 2007

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederLicense : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederMaintainer : luecke@tzi.de

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederStability : experimental

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian MaederPortability : portable

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von SchroederDefinition of abstract syntax for propositional logic

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder-}

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder{-

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder Ref.

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder http://en.wikipedia.org/wiki/Propositional_logic

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder-}

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maedermodule Propositional.AS_BASIC_Propositional

8878f7411a09d4dc54bf1941cc7a243e35ddb530Christian Maeder (

8878f7411a09d4dc54bf1941cc7a243e35ddb530Christian Maeder Formula (..) -- datatype for Propositional Formulas

8878f7411a09d4dc54bf1941cc7a243e35ddb530Christian Maeder , pretty -- pretty printing

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder , is_True_atom -- True?

4d3f1471f9fc5ef08b7d49f2e70af7f327292952Christian Maeder , is_False_atom -- False?

) where

import Common.Id

import Common.Doc

import Common.DocUtils

-- DrIFT command

{-! global: UpPos !-}

-- | Datatype for propositional formulas

data Formula = Negation Formula Range

-- pos: not

| Conjunction [Formula] Range

-- pos: "/\"s

| Disjunction [Formula] Range

-- pos: "\/"s

| Implication Formula Formula Bool Range

-- pos: "=>"

| Equivalence Formula Formula Bool Range

-- pos: "<=>"

| True_atom Range

-- pos: "True"

| False_atom Range

-- pos: "False

| Predication Common.Id.Id

-- pos: Propositional Identifiers

deriving (Show, Eq, Ord)

instance Pretty Formula where

pretty = printFormula

-- | Value of the true atom

-- True is always true -P

is_True_atom :: Formula -> Bool

is_True_atom (True_atom _) = True

is_True_atom _ = False

-- | Value of the false atom

-- and False if always false

is_False_atom :: Formula -> Bool

is_False_atom (False_atom _) = False

is_False_atom _ = False

-- Pretty printing for formulas

printFormula :: Formula -> Doc

printFormula (Negation f _) = notDoc

<> lparen <> printFormula f <> rparen

printFormula (Conjunction xs _) = parens $

sepByArbitrary andDoc

$ map printFormula xs

printFormula (Disjunction xs _) = parens $

sepByArbitrary orDoc

$ map printFormula xs

printFormula (Implication x y _ _) = parens $ printFormula x <>

implies <> printFormula y

printFormula (Equivalence x y _ _) = parens $ printFormula x <>

equiv <> printFormula y

printFormula (True_atom _) = text "True"

printFormula (False_atom _) = text "False"

printFormula (Predication x) = idDoc x

-- Extended version of vcat

sepByArbitrary :: Doc -> [Doc] -> Doc

sepByArbitrary _ [] = text ""

sepByArbitrary _ (x:[]) = x

sepByArbitrary separator (x:xs) = x <> separator

<> (sepByArbitrary separator xs)