/**
 * The MIT License (MIT)
 * 
 * Copyright (c) 2015 Camil Staps
 * 
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 * 
 * The above copyright notice and this permission notice shall be included in all
 * copies or substantial portions of the Software.
 * 
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */
definition module Logic

from    StdOverloaded   import class <, class ==
from    StdMaybe        import :: Maybe

// 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

// Possibility for an atom to be true or false
:: AtomOption :== (AtomName,Bool)

:: TruthTable = {exprs :: [Expr], options :: [[AtomOption]]}
:: FilledTruthTable = {table :: TruthTable, values :: [[Maybe Bool]]}

:: OutputOption = Plain | Html | LaTeX
DefaultOutputOption :== Plain
instance == OutputOption

class show a :: OutputOption a -> String
instance show Bool
instance show Char
instance show Op1
instance show Op2
instance show Expr
instance show FilledTruthTable

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 == Op1   
instance < Op1      // Maybe useful later if more unary operators are added
instance == Op2
instance < Op2      // To sort by precedence
instance == Expr
instance < Expr     // To sort by unrigorous 'complexity'; e.g. in truthtables

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

all_atoms :: Expr -> [AtomName]             // All the atomic expressions in an expressions
all_atom_options :: Expr -> [[AtomOption]]  // All AtomOptions for all atomic expressions in an expression

substitute :: AtomOption Expr -> Expr       // Substitute all atomic expressions with some name with some constant
substitute_all :: [AtomOption] Expr -> Expr // Same, for multiple options
eval :: Expr -> [Bool]                      // Evaluate to a simpler form

subexprs :: Expr -> [Expr]                  // Subexpressions of an expression
sorted_subexprs :: (Expr -> [Expr])         // Similar, but roughly sorted by complexity

simple_truthtable :: Expr -> TruthTable     // Simple truthtable: only the atomic expression and the expression itself
simple_truthtable_n :: [Expr] -> TruthTable // Simple truthtable with multiple expressions
truthtable :: Expr -> TruthTable            // Truthtable from an expression
truthtable_n :: [Expr] -> TruthTable        // Truthtable with multiple expressions

compute :: TruthTable -> FilledTruthTable   // Fill in a truthtable

parse :: String -> Expr                     // Parse a string into an expression