import Base
import ../../lib/logic.bend as L
import ../../lib/nat.bend as N
import ../../lib/list.bend as LL
import ../../../spec/lib/common.bend as SC
import ../../../spec/containers/hash_table.bend as S
import ../../../spec/containers/lru.bend as SP
import ../../../src/math/u64.bend as W
import ../hash_table/keys.bend as K
import ../hash_table/state.bend as HT
import ./state.bend as ST
import ../../lib/nat_list.bend as NL

# List algebra for the recency list and the model's keys: membership,
# duplicate-freedom and the per-slot predicates over appends.


# ---- Bool algebra ----





# not (x or y) and (z and not w)  ==  (not x and z) and not (y or w)


# ---- slot lists ----




# ---- key lists ----


def mem_app_s(+x: String, +a: List<&2, String>, +b: List<&2, String>) -> {S.mem(x, SC.append(String, a, b)) == Bool.or(S.mem(x, a), S.mem(x, b)) : Bool}:
  match a:
    case Nil{}:
      {==}
    case Con{+h, +t}:
      Equal.trans(Bool, Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, b))), Bool.or(S.str_eq(h, x), Bool.or(S.mem(x, t), S.mem(x, b))), Bool.or(Bool.or(S.str_eq(h, x), S.mem(x, t)), S.mem(x, b)), Equal.cong(Bool, Bool, z => Bool.or(S.str_eq(h, x), z), S.mem(x, SC.append(String, t, b)), Bool.or(S.mem(x, t), S.mem(x, b)), mem_app_s(x, t, b)), NL.or_assoc(S.str_eq(h, x), S.mem(x, t), S.mem(x, b)))

def mem_mid_s(+x: String, +a: List<&2, String>, +s: String, +b: List<&2, String>) -> {S.mem(x, SC.append(String, a, Con{s, b})) == Bool.or(S.mem(x, SC.append(String, a, b)), S.str_eq(s, x)) : Bool}:
  match a:
    case Nil{}:
      NL.or_comm(S.str_eq(s, x), S.mem(x, b))
    case Con{+h, +t}:
      Equal.trans(Bool, Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, Con{s, b}))), Bool.or(S.str_eq(h, x), Bool.or(S.mem(x, SC.append(String, t, b)), S.str_eq(s, x))), Bool.or(Bool.or(S.str_eq(h, x), S.mem(x, SC.append(String, t, b))), S.str_eq(s, x)), Equal.cong(Bool, Bool, z => Bool.or(S.str_eq(h, x), z), S.mem(x, SC.append(String, t, Con{s, b})), Bool.or(S.mem(x, SC.append(String, t, b)), S.str_eq(s, x)), mem_mid_s(x, t, s, b)), NL.or_assoc(S.str_eq(h, x), S.mem(x, SC.append(String, t, b)), S.str_eq(s, x)))

def nd_mid_s(+a: List<&2, String>, +s: String, +b: List<&2, String>) -> {S.nodup(SC.append(String, a, Con{s, b})) == Bool.and(S.nodup(SC.append(String, a, b)), Bool.not(S.mem(s, SC.append(String, a, b)))) : Bool}:
  match a:
    case Nil{}:
      NL.and_comm(Bool.not(S.mem(s, b)), S.nodup(b))
    case Con{+h, +t}:
      +X = S.mem(h, SC.append(String, t, b))
      +Z = S.nodup(SC.append(String, t, b))
      +Wm = S.mem(s, SC.append(String, t, b))
      +e1 = Equal.cong(Bool, Bool, z => Bool.and(Bool.not(z), S.nodup(SC.append(String, t, Con{s, b}))), S.mem(h, SC.append(String, t, Con{s, b})), Bool.or(X, S.str_eq(s, h)), mem_mid_s(h, t, s, b))
      +e2 = Equal.cong(Bool, Bool, z => Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), z), S.nodup(SC.append(String, t, Con{s, b})), Bool.and(Z, Bool.not(Wm)), nd_mid_s(t, s, b))
      +e3 = NL.bt_mid(X, S.str_eq(s, h), Z, Wm)
      +e4 = Equal.cong(Bool, Bool, z => Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(z, Wm))), S.str_eq(s, h), S.str_eq(h, s), K.str_sym(s, h))
      Equal.trans(Bool, S.nodup(SC.append(String, Con{h, t}, Con{s, b})), Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), S.nodup(SC.append(String, t, Con{s, b}))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e1, Equal.trans(Bool, Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), S.nodup(SC.append(String, t, Con{s, b}))), Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), Bool.and(Z, Bool.not(Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e2, Equal.trans(Bool, Bool.and(Bool.not(Bool.or(X, S.str_eq(s, h))), Bool.and(Z, Bool.not(Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(s, h), Wm))), Bool.and(Bool.and(Bool.not(X), Z), Bool.not(Bool.or(S.str_eq(h, s), Wm))), e3, e4)))

# ---- slot predicates ----

def sall_app(~V: Data, +p: ST.SP1<V>, +a: List<&2, Nat>, +b: List<&2, Nat>) -> {ST.sall(~V, p, SC.append(Nat, a, b)) == Bool.and(ST.sall(~V, p, a), ST.sall(~V, p, b)) : Bool}:
  match a:
    case Nil{}:
      {==}
    case Con{+h, +t}:
      Equal.trans(Bool, Bool.and(ST.sev(~V, p, h), ST.sall(~V, p, SC.append(Nat, t, b))), Bool.and(ST.sev(~V, p, h), Bool.and(ST.sall(~V, p, t), ST.sall(~V, p, b))), Bool.and(Bool.and(ST.sev(~V, p, h), ST.sall(~V, p, t)), ST.sall(~V, p, b)), Equal.cong(Bool, Bool, z => Bool.and(ST.sev(~V, p, h), z), ST.sall(~V, p, SC.append(Nat, t, b)), Bool.and(ST.sall(~V, p, t), ST.sall(~V, p, b)), sall_app(~V, p, t, b)), NL.and_assoc(ST.sev(~V, p, h), ST.sall(~V, p, t), ST.sall(~V, p, b)))

def sa_c(~V: Data, +p: ST.SP1<V>, +x: Nat, +s0: Nat, +t: List<&2, Nat>, +h: {Bool.and(ST.sev(~V, p, s0), ST.sall(~V, p, t)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(s0, x) == c : Bool}, +hm: {Bool.or(c, NL.memn(x, t)) == True{} : Bool}, rec: @hs: {ST.sall(~V, p, t) == True{} : Bool} -> @hm2: {NL.memn(x, t) == True{} : Bool} -> {ST.sev(~V, p, x) == True{} : Bool}) -> {ST.sev(~V, p, x) == True{} : Bool}:
  match c:
    case True{}:
      L.subst(Nat, z => {ST.sev(~V, p, z) == True{} : Bool}, s0, x, N.eq_from_is_eq(s0, x, hc), L.and_left(ST.sev(~V, p, s0), ST.sall(~V, p, t), h))
    case False{}:
      rec(L.and_right(ST.sev(~V, p, s0), ST.sall(~V, p, t), h), hm)

# p holds at a member
def sall_mem(~V: Data, +p: ST.SP1<V>, +x: Nat, +xs: List<&2, Nat>, +h: {ST.sall(~V, p, xs) == True{} : Bool}, +hm: {NL.memn(x, xs) == True{} : Bool}) -> {ST.sev(~V, p, x) == True{} : Bool}:
  match xs:
    case Nil{}:
      Empty.absurd({ST.sev(~V, p, x) == True{} : Bool}, L.false_true(hm))
    case Con{+s0, +t}:
      sa_c(~V, p, x, s0, t, h, Nat.is_eq(s0, x), {==}, hm, hs => hm2 => sall_mem(~V, p, x, t, hs, hm2))

# ---- the model's entries ----


def es_app(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +a: List<&2, Nat>, +b: List<&2, Nat>) -> {ST.es(~V, ll, kl, el, SC.append(Nat, a, b)) == SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)) : List<&2, SP.Ent<V>>}:
  match a:
    case Nil{}:
      {==}
    case Con{+h, +t}:
      +x = ST.sent_m(~V, ll, kl, h, HT.nthm(~V, el, h))
      Equal.trans(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, x, ST.es(~V, ll, kl, el, SC.append(Nat, t, b))), SC.append(SP.Ent<V>, x, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b))), SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, x, ST.es(~V, ll, kl, el, t)), ST.es(~V, ll, kl, el, b)), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, x, z), ST.es(~V, ll, kl, el, SC.append(Nat, t, b)), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b)), es_app(~V, ll, kl, el, t, b)), Equal.sym(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, x, ST.es(~V, ll, kl, el, t)), ST.es(~V, ll, kl, el, b)), SC.append(SP.Ent<V>, x, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b))), LL.append_assoc(SP.Ent<V>, x, ST.es(~V, ll, kl, el, t), ST.es(~V, ll, kl, el, b))))

def keys_app(~V: Data, +a: List<&2, SP.Ent<V>>, +b: List<&2, SP.Ent<V>>) -> {SP.keys_of(~V, SC.append(SP.Ent<V>, a, b)) == SC.append(String, SP.keys_of(~V, a), SP.keys_of(~V, b)) : List<&2, String>}:
  match a:
    case Nil{}:
      {==}
    case Con{SP.LE{+k, +v, +t, +d}, +r}:
      LL.cons_cong(String, k, SP.keys_of(~V, SC.append(SP.Ent<V>, r, b)), SC.append(String, SP.keys_of(~V, r), SP.keys_of(~V, b)), keys_app(~V, r, b))

def snoc_app(~V: Data, +a: List<&2, SP.Ent<V>>, +e: SP.Ent<V>) -> {SP.snoc(~V, a, e) == SC.append(SP.Ent<V>, a, Con{e, Nil{}}) : List<&2, SP.Ent<V>>}:
  match a:
    case Nil{}:
      {==}
    case Con{+h, +t}:
      LL.cons_cong(SP.Ent<V>, h, SP.snoc(~V, t, e), SC.append(SP.Ent<V>, t, Con{e, Nil{}}), snoc_app(~V, t, e))

# no entry of a has key
def enk(~V: Data, a: List<&2, SP.Ent<V>>, +key: String) -> Bool:
  match a:
    case Nil{}:
      True{}
    case Con{SP.LE{+k, v, t, d}, r}:
      Bool.and(Bool.not(S.str_eq(k, key)), enk(~V, r, key))

def drop_c(~V: Data, +k: String, +v: V, +t: U32, +d: W.U64, +r: List<&2, SP.Ent<V>>, +b: List<&2, SP.Ent<V>>, +key: String, +c: Bool, +hc: {S.str_eq(k, key) == c : Bool}, +h: {Bool.not(c) == True{} : Bool}, +ih: {SP.drop(~V, SC.append(SP.Ent<V>, r, b), key) == SC.append(SP.Ent<V>, r, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}) -> {SP.drop(~V, SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, b), key) == SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}:
  match c:
    case True{}:
      Empty.absurd({SP.drop(~V, SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, b), key) == SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}, L.false_true(h))
    case False{}:
      L.subst(Bool, z => {Bool.pick(List<&2, SP.Ent<V>>, z, SC.append(SP.Ent<V>, r, b), Con{SP.LE{k, v, t, d}, SP.drop(~V, SC.append(SP.Ent<V>, r, b), key)}) == SC.append(SP.Ent<V>, Con{SP.LE{k, v, t, d}, r}, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}, False{}, S.str_eq(k, key), Equal.sym(Bool, S.str_eq(k, key), False{}, hc), LL.cons_cong(SP.Ent<V>, SP.LE{k, v, t, d}, SP.drop(~V, SC.append(SP.Ent<V>, r, b), key), SC.append(SP.Ent<V>, r, SP.drop(~V, b, key)), ih))

# drop skips a prefix without key
def drop_app(~V: Data, +a: List<&2, SP.Ent<V>>, +b: List<&2, SP.Ent<V>>, +key: String, +h: {enk(~V, a, key) == True{} : Bool}) -> {SP.drop(~V, SC.append(SP.Ent<V>, a, b), key) == SC.append(SP.Ent<V>, a, SP.drop(~V, b, key)) : List<&2, SP.Ent<V>>}:
  match a:
    case Nil{}:
      {==}
    case Con{SP.LE{+k, +v, +t, +d}, +r}:
      drop_c(~V, k, v, t, d, r, b, key, S.str_eq(k, key), {==}, L.and_left(Bool.not(S.str_eq(k, key)), enk(~V, r, key), h), drop_app(~V, r, b, key, L.and_right(Bool.not(S.str_eq(k, key)), enk(~V, r, key), h)))

# ---- splitting a duplicate-free list ----









# a member of x is not in a


# a member of a is not in x