definition module Logic

import StdEnv

// Expressions
:: Expr = B Bool                // A constant
        | Atom AtomName         // An atomic expression
        | App1 Op1 Expr         // Applying an Op1 on an expression
        | App2 Expr Op2 Expr    // Applying an Op2 on two expressions

// Operators with one argument
:: Op1  = Not   // logical not

// Operators with two arguments
:: Op2  = And   // logical and; left-associative
        | Or    // logical or; right-associative
        | Impl  // material implication; right-associative
        | Equiv // equivalence; right-associative

// All Chars may be used, but typically only [a-zA-Z] are used
:: AtomName :== Char

isBool  :: Expr -> Bool
isAtom  :: Expr -> Bool
isApp1  :: Expr -> Bool
isApp2  :: Expr -> Bool
isApp   :: Expr -> Bool

isNot   :: Expr -> Bool
isAnd   :: Expr -> Bool
isOr    :: Expr -> Bool
isImpl  :: Expr -> Bool
isEquiv :: Expr -> Bool

instance toString Op1
instance toString Op2
instance toString Expr

binds_stronger :: Op2 Op2 -> Bool           // True iff arg1 stronger binds than arg2