-- Forall and exists in Lua, version 0
-- By Eduardo Ochs, 2011jul26
--[[
* (eepitch-lua51)
* (eepitch-kill)
* (eepitch-lua51)
--]]

get_value = function (var) return _G[var] end
set_value = function (var, value) _G[var] = value end
run = function (f, ...)
    if type(f) == "string" then f = _G[f] end
    return f(...)
  end
prun = function (...) print(run(...)) end

forall_in = function (var, set, f)
    local var_backup = get_value(var)
    local result = true
    for _,value in ipairs(set) do
        set_value(var, value)
        result = result and run(f)
      end
    set_value(var, var_backup)
    return result
  end
exists_in = function (var, set, f)
    local var_backup = get_value(var)
    local result = false
    for _,value in ipairs(set) do
        set_value(var, value)
        result = result or run(f)
      end
    set_value(var, var_backup)
    return result
  end


-- Verbose syntax:

_G["P(a)"] = function () return a < 4 end
_G["Fa a in A.P(a)"] = function ()
    return forall_in("a", get_value("A"), "P(a)")
  end

a = 0;         print(run("P(a)"))              --> true
a = 5;         print(run("P(a)"))              --> false
A = {2, 3, 4}; print(run("Fa a in A.P(a)"))    --> false
A = {2, 3};    print(run("Fa a in A.P(a)"))    --> true


-- Shorter syntax (may be confusing):

_G["P(a)"] = function () return a < 4 end
_G["Fa_a_A.P(a)"] = function ()
    return forall_in("a", A, "P(a)")
  end
a = 0;         prun("P(a)")           --> true
a = 5;         prun("P(a)")           --> false
A = {2, 3, 4}; prun("Fa_a_A.P(a)")    --> false
A = {2, 3};    prun("Fa_a_A.P(a)")    --> true