gistfile1.swift

// Example of how to build a propositional logic 
// reasoner in swift.


typealias VarIndex = Int
typealias TruthValue = Bool
typealias Env = [VarIndex : TruthValue]
typealias Expr = (Env) -> TruthValue


// var builder

func X(i:VarIndex) -> Expr {
  let result = { (env:Env) in
    env[i]!
  }
  
  return result
}

// Operators

func &&(a:Expr, b:Expr) -> Expr {
  return { (env:Env) in
      a(env) && b(env)
  }
}

func ||(a:Expr, b:Expr) -> Expr {
  return { (env:Env) in
    a(env) || b(env)
  }
}

prefix func !(a:Expr) -> Expr {
  return { (env:Env) in
    !a(env)
  }
}

infix operator => { associativity right precedence 100 }
func =>(a:Expr, b:Expr) -> Expr {
  return { (env:Env) in
    !a(env) || b(env)
  }
}

infix operator <=> { associativity right precedence 100 }
func <=>(a:Expr, b:Expr) -> Expr {
  return { (env:Env) in
    ((a => b) && (b => a))(env)
  }
}

// Returns true if the expression evaluated in the given
// environment is true
infix operator |- { associativity left precedence 40 }
func |-(e:Env, a:Expr) -> TruthValue {
  return a(e)
}

// Returns true if every environment built with n variables
// makes true the given expression
infix operator |= { precedence 10 }
func |=(n:Int, expr:Expr) -> Bool {
  let pow2n = 1 << n
  for assignment in 0 ..< pow2n {
    var env:Env = Dictionary<VarIndex, Bool>()
    for bitPos in 0 ..< n {
      let bit = assignment & (1 << bitPos) > 0 ? true : false
      env[bitPos] = bit
    }
    
    if !(env |- expr)  {
      return false
    }
  }
  
  return true
}


// test

let x = X(0)
let y = X(1)

// all the following evaluate to true

2 |= ((x => y) && x) => y
2 |= x && y <=> y && x
2 |= (x => y) <=> (!x || y)