-- -*- coding: raw-text -*-
-- (find-es "lua5" "modal.lua")
-- A library of functions to operate on modal and intuitionistic
-- truth-values.
-- Edrx, 2008aug01

ctrue  = function () return 1 end
cfalse = function () return 0 end
cnot   = function (a) return 1 - a end
cand   = function (a, b) return min(a, b) end
cor    = function (a, b) return max(a, b) end
cimp   = function (a, b) return b >= a and 1 or 0 end

n = 4   -- number of worlds (see "setup", below)
mmap = function (clf, A, B)
    C = {}
    for i=1,n do C[i] = clf(A and A[i], B and B[i]) end
    return C
  end
mtrue  = function () return mmap(ctrue)  end
mfalse = function () return mmap(cfalse) end
mand   = function (A, B) return mmap(cand, A, B) end
mor    = function (A, B) return mmap(cor,  A, B) end
mimp   = function (A, B) return mmap(cimp, A, B) end
mnot   = function (A)    return mmap(cnot, A) end

S = function (A) return table.concat(A) end    -- stringify
M = function (str) return split(str, ".") end  -- modalize (tablify)

-- Reh:  Square:  House:
--  1               1
-- 2 3    1 2      2 3
-- 4	  3 4      4 5
--
Nec_Reh = function (A)
    AI = {}
    AI[4] = A[4]
    AI[3] = A[3]
    AI[2] = A[2] * AI[4]
    AI[1] = A[1] * AI[2] * AI[3]
    return AI
  end
Nec_Square = function (A)
    AI = {}
    AI[4] = A[4]
    AI[3] = A[3]
    AI[2] = A[2] * AI[4]
    AI[1] = A[1] * AI[3]
    return AI
  end
Nec_House = function (A)
    AI = {}
    AI[5] = A[5]
    AI[4] = A[4]
    AI[3] = A[3] * AI[5]
    AI[2] = A[2] * AI[4]
    AI[1] = A[1] * AI[2] * AI[3]
    return AI
  end
Nec = Nec_Reh
Nec = Nec_Square
nec = function (str) return S(Nec(M(str))) end

itrue  = function () return S(mtrue()) end
ifalse = function () return S(mfalse()) end
iand   = function (p, q) return S(mand(M(p), M(q))) end
ior    = function (p, q) return S(mor(M(p), M(q))) end
iimp   = function (p, q) return S(Nec(mimp(M(p), M(q)))) end
inot   = function (p) return S(Nec(mnot(M(p)))) end

addss = function (T, n, prefix)
    prefix = prefix or ""
    if n == 0 then
      tinsert(T, prefix)
    else
      addss(T, n-1, prefix.."0")
      addss(T, n-1, prefix.."1") 
    end
    return T
  end
mtvs_ = function () return addss({}, n) end
itvs_ = function ()
    local itvs = {}
    for _,mtv in ipairs(mtvs_()) do
      if mtv == nec(mtv) then tinsert(itvs, mtv) end
    end
    return itvs
  end

mtvs = mtvs_()    -- modal truth-values
itvs = itvs_()    -- intuitionistic truth-values

star_notnot = function (p) return inot(inot(p)) end
star = star_notnot

-- Other modalities. Usage:
--   star = star_or("001")
--   star = star_imp("011")
star_or  = function (alpha) return function (p) return ior(alpha, p) end end
star_imp = function (beta)  return function (p) return iimp(beta, p) end end
star_force = function (alpha, beta)
    return function (p) return ior(alpha, iimp(beta, p)) end   -- check this
  end

setup = function (n_, Nec_)
    n = n_            -- number of worlds
    Nec = Nec_        -- Nec_Reh or Nec_Square or ...
    mtvs = mtvs_()    -- a table listing all the modal truth-values
    itvs = itvs_()    -- a table listing all the intuitionistic truth-values
    t = itrue()
  end
setup(4, Nec_Square)
setup(5, Nec_House)

-- Reh:  Square:  House:   Vee:  Bighouse:  Two:  Three:
--  1               1      1 2      1        1      1
-- 2 3    1 2      2 3      3      2 3       2      2
-- 4	  3 4      4 5             4 5              3
--                                 6 7
--
Meta_House  = {"23", "4", "5", "", ""}
Meta_Square = {"3", "4", "", ""}
Meta_Vee    = {"3", "3", ""}
Meta_Reh    = {"23", "4", "", ""}
Meta_Bighouse  = {"23", "4", "5", "6", "7", "", ""}
Meta_Two    = {"2", ""}
Meta_Three  = {"2", "3", ""}
Nec_Meta = function (A)
    AI = {}
    for i=n,1,-1 do       -- start from the worlds at the bottom
      AI[i] = A[i]
      for c in string.gmatch(Meta[i], ".") do  -- for each world immediately
        AI[i] = AI[i] * AI[tonumber(c)]        -- below this one: and-ify
      end
    end
    return AI
  end
Setup = function (Meta_)
    n    = #Meta_     -- number of worlds
    Meta = Meta_
    Nec  = Nec_Meta   -- Nec_Reh or Nec_Square or ...
    mtvs = mtvs_()    -- a table listing all the modal truth-values
    itvs = itvs_()    -- a table listing all the intuitionistic truth-values
    t    = itrue()
  end

toset = function (T) local S={}; for i=1,#T do S[T[i]]=T[i] end; return S end
differents = function (T) return #keys(toset(T)) end

eight = function (op, p, q)
    local a, b, c, d = op(p,      q),  op(star(p),      q),
                       op(p, star(q)), op(star(p), star(q))
    return a, b, c, d, star(a), star(b), star(c), star(d)
  end

generatepairs = function (A)
    return coroutine.wrap(function ()
        for _,i in ipairs(A) do
          for _,j in ipairs(A) do
            coroutine.yield(i, j)
          end
        end
      end)
  end
generatetriples = function (A)
    return coroutine.wrap(function ()
        for _,i in ipairs(A) do
          for _,j in ipairs(A) do
            for _,k in ipairs(A) do
              coroutine.yield(i, j, k)
            end
          end
        end
      end)
  end

printeight = function (op, min)
    for p,q in generatepairs(itvs) do
      local d = differents{eight(op, p, q)}
      if d >= (min or 0) then
	print(p, q, eight(op, p, q))
      end
    end
  end

printneight = function (op, min)
    for p,q in generatepairs(itvs) do
      local d = differents{eight(op, p, q)}
      if d >= (min or 0) then
	print(p, q, d)
      end
    end
  end