include "ERTL/ERTL.ma".
include "ERTL/liveness.ma".

definition vertex ≝ register ⊎ Register.

inductive decision: Type[0] ≝
  | decision_spill: nat → decision
  | decision_colour: Register → decision.

definition is_member ≝
  λvertex.
  λregister_lattice.
  let 〈l, r〉 ≝ register_lattice in
  match vertex with
  [ inl v ⇒ set_member ? (eq_identifier RegisterTag) v l
  | inr v ⇒ set_member ? eq_Register v r
  ].

record coloured_graph (v: valuation): Type[1] ≝
{
  colouring: vertex → decision;
  prop_colouring: ∀l. ∀v1, v2: vertex.
    is_member v1 (v l) → is_member v2 (v l) → colouring v1 ≠ colouring v2
}.

axiom build: ∀valuation. coloured_graph valuation.

(*
(* definition vertex_set ≝ set vertex. *)
definition vertex_priority_set ≝ priority_set vertex.
definition vertex_set_table ≝ set_table vertex (set vertex).
definition vertex_set ≝ set vertex.
definition Register_set_table ≝ set_table vertex (set Register).
definition Register_set ≝ set Register.
*)

(*
record graph: Type[0] ≝
{
  g_regmap     : register_table;
  g_ivv        : vertex_set_table;
  g_ivh        : Register_set_table;
  g_pvv        : vertex_set_table;
  g_pvh        : Register_set_table;
  g_degree     : vertex_priority_set;
  g_nmr        : vertex_priority_set
}.

definition set_ivv ≝
  λgraph.
  λivv: vertex_set_table.
    let regmap ≝ g_regmap graph in
    let ivh    ≝ g_ivh graph in
    let pvv    ≝ g_pvv graph in
    let pvh    ≝ g_pvh graph in
    let degree ≝ g_degree graph in
    let nmr    ≝ g_nmr graph in
      mk_graph
        regmap ivv ivh pvv pvh degree nmr.

definition set_ivh ≝
  λgraph.
  λivh: Register_set_table.
    let regmap ≝ g_regmap graph in
    let ivv    ≝ g_ivv graph in
    let pvv    ≝ g_pvv graph in
    let pvh    ≝ g_pvh graph in
    let degree ≝ g_degree graph in
    let nmr    ≝ g_nmr graph in
      mk_graph
        regmap ivv ivh pvv pvh degree nmr.

definition set_degree ≝
  λgraph.
  λdegree: vertex_priority_set.
    let regmap ≝ g_regmap graph in
    let ivv    ≝ g_ivv graph in
    let ivh    ≝ g_ivh graph in
    let pvv    ≝ g_pvv graph in
    let pvh    ≝ g_pvh graph in
    let nmr    ≝ g_nmr graph in
      mk_graph
        regmap ivv ivh pvv pvh degree nmr.

definition set_nmr ≝
  λgraph.
  λnmr: vertex_priority_set.
    let regmap ≝ g_regmap graph in
    let ivv    ≝ g_ivv graph in
    let ivh    ≝ g_ivh graph in
    let pvv    ≝ g_pvv graph in
    let pvh    ≝ g_pvh graph in
    let degree ≝ g_degree graph in
      mk_graph
        regmap ivv ivh pvv pvh degree nmr.

definition sg_neighboursv ≝
  λgraph: graph.
  λv: vertex.
    set_tbl_find … v (g_ivv graph).

definition sg_existsvv ≝
  λgraph.
  λv1.
  λv2.
  match sg_neighboursv graph v2 with
  [ None       ⇒ false (* XXX: ok? *)
  | Some neigh ⇒ set_member ? eq_nat v1 neigh
  ].

definition sg_neighboursh ≝
  λgraph.
  λv.
    set_tbl_find ? ? v (g_ivh graph). 

definition sg_existsvh ≝
  λgraph.
  λv.
  λh.
  match sg_neighboursh graph v with
  [ None       ⇒ false (* XXX: ok? *)
  | Some neigh ⇒ set_member ? eq_Register h neigh
  ].

definition sg_degree ≝
  λgraph.
  λv.
  match sg_neighboursv graph v with
  [ None ⇒ None ?
  | Some neigh ⇒
    match sg_neighboursh graph v with
    [ None ⇒ None ?
    | Some neigh' ⇒ Some ? ((set_size … neigh) + (set_size … neigh'))
    ]
  ].
    
definition sg_hwregs ≝
  λgraph: graph.
    let union ≝ λkey: vertex. set_union ? in
    set_tbl_fold vertex ? ? union (g_ivh graph) (set_empty Register).

axiom sg_iter: Type[0]. (* XXX: todo when i can be bothered *)

definition sg_mkvvi ≝
  λgraph.
  λv1.
  λv2.
    set_ivv graph (set_tbl_homo_mkbiedge … v1 v2 (g_ivv graph)).

definition sg_mkvv ≝
  λgraph.
  λv1.
  λv2.
    if eq_nat v1 v2 then
      graph
    else if sg_existsvv graph v1 v2 then
      graph
    else
      sg_mkvvi graph v1 v2.

definition sg_rmvv ≝
  λgraph.
  λv1.
  λv2.
    set_ivv graph (set_tbl_homo_rmbiedge … v1 v2 (g_ivv graph)).

definition sg_rmvvifx ≝
  λgraph.
  λv1.
  λv2.
  if sg_existsvv graph v1 v2 then
    sg_rmvv graph v1 v2
  else
    graph.

definition sg_mkvhi ≝
  λgraph.
  λv.
  λh.
    set_ivh graph (set_tbl_update … v (set_insert … h) (g_ivh graph)). 

definition sg_mkvh ≝
  λgraph.
  λv.
  λh.
  if sg_existsvh graph v h then
    graph
  else
    sg_mkvhi graph v h.

definition sg_rmvh ≝
  λgraph.
  λv.
  λh.
    set_ivh graph (set_tbl_update … v (set_remove … h) (g_ivh graph)).

definition sg_rmvhifx ≝
  λgraph.
  λv.
  λh.
    if sg_existsvh graph v h then
      sg_rmvh graph v h
    else
      graph.

definition sg_coalesce ≝
  λg.
  λx.
  λy.
  match sg_neighboursv g x with
  [ None       ⇒ None ?
  | Some neigh ⇒
    let graph ≝ set_fold ? graph (λw. λg.
      sg_mkvv (sg_rmvv g x w) y w) neigh g
    in
    match sg_neighboursh g x with
    [ None ⇒ None ?
    | Some neigh ⇒
      let graph ≝ set_fold ? ? (λh. λg.
        sg_mkvh (sg_rmvh g x h) y h) neigh g
      in
        Some … graph
    ]
  ].

definition sg_coalesceh ≝
  λg.
  λx.
  λh.
  match sg_neighboursv g x with
  [ None       ⇒ None ?
  | Some neigh ⇒
    let graph ≝ set_fold ? graph (λw. λg.
      sg_mkvh (sg_rmvv g x w) w h) neigh g
    in
    match sg_neighboursh g x with
    [ None ⇒ None ?
    | Some neigh ⇒
      let graph ≝ set_fold ? ? (λk. λg.
        sg_rmvh graph x k) neigh g
      in
        Some … graph
    ]
  ].

definition sg_remove ≝
  λg.
  λx.
  match sg_neighboursv g x with
  [ None ⇒ None ?
  | Some neigh ⇒
    let graph ≝
      set_fold … (λw. λgraph.
        sg_rmvv graph x w) neigh g
    in
    match sg_neighboursh graph x with
    [ None ⇒ None ?
    | Some neigh ⇒
      let graph ≝ set_fold … (λh. λg.
        sg_rmvh g x h) neigh graph
      in
        Some ? graph
    ]
  ].

definition ig_mkvvi ≝
  λgraph.
  λv1.
  λv2.
  let graph ≝ sg_mkvvi graph v1 v2 in
  let graph ≝ sg_rmvvifx graph v1 v2 in
  let degree' ≝ pset_increment ? v1 (repr 1) (pset_increment ? v2 (repr 1) (g_degree graph)) in
  let nmr' ≝ pset_incrementifx ? v1 (repr 1) (pset_incrementifx ? v2 (repr 1) (g_nmr graph)) in
    set_degree (set_nmr graph nmr') degree'.

definition ig_rmvv ≝
  λgraph.
  λv1.
  λv2.
  let graph ≝ sg_rmvv graph v1 v2 in
  let degree' ≝ pset_increment ? v1 (neg (repr 1)) (pset_increment ? v2 (neg (repr 1)) (g_degree graph)) in
  let nmr' ≝ pset_incrementifx ? v1 (neg (repr 1)) (pset_incrementifx ? v2 (neg (repr 1)) (g_nmr graph)) in
    set_degree (set_nmr graph nmr') degree'.

definition ig_mkvhi ≝
  λgraph.
  λv.
  λh.
  let graph ≝ sg_mkvhi graph v h in
  let graph ≝ sg_rmvhifx graph v h in
  let degree ≝ pset_increment ? v (repr 1) (g_degree graph) in
  let nmr ≝ pset_incrementifx ? v (repr 1) (g_nmr graph) in
    set_degree (set_nmr graph nmr) degree.

definition ig_rmvh ≝
  λgraph.
  λv.
  λh.
  let graph ≝ sg_rmvh graph v h in
  let degree ≝ pset_increment ? v (neg (repr 1)) (g_degree graph) in
  let nmr ≝ pset_incrementifx ? v (neg (repr 1)) (g_nmr graph) in
    set_degree (set_nmr graph nmr) degree.

definition pref_nmr ≝
  λgraph.
  λv.
  match sg_neighboursv graph v with
  [ None       ⇒ false (* XXX: ok? *)
  | Some neigh ⇒
    match sg_neighboursh graph v with
    [ None        ⇒ false
    | Some neigh' ⇒
      andb (set_is_empty ? neigh) (set_is_empty ? neigh')
    ]
  ].

definition pref_mkcheck ≝
  λgraph.
  λv.
    if pref_nmr graph v then
      let nmr' ≝ pset_remove ? v (g_nmr graph) in
        set_nmr graph nmr'
    else
      graph.

definition pref_mkvvi ≝
  λgraph.
  λv1.
  λv2.
    if sg_existsvv graph v1 v2 then
      graph
    else
      let graph ≝ pref_mkcheck graph v1 in
      let graph ≝ pref_mkcheck graph v2 in
        sg_mkvvi graph v1 v2.

definition pref_mkvhi ≝
  λgraph.
  λv.
  λh.
  if sg_existsvh graph v h then
    graph
  else
    let graph ≝ pref_mkcheck graph v in
      sg_mkvhi graph v h.

(* XXX: look at this carefully *)
definition pref_rmcheck ≝
  λgraph.
  λv.
  if pref_nmr graph v then
    match pset_lookup ? v (g_degree graph) with
    [ None ⇒ graph (* XXX: ok? *)
    | Some pref ⇒
      let nmr ≝ pset_insert ? v pref (g_nmr graph) in
        set_nmr graph nmr
    ]
  else
    graph.

definition pref_rmvv ≝
  λgraph.
  λv1.
  λv2.
  let graph ≝ sg_rmvv graph v1 v2 in
  let graph ≝ pref_rmcheck graph v1 in
  let graph ≝ pref_rmcheck graph v2 in
    graph.

definition pref_rmvh ≝
  λgraph.
  λv.
  λh.
  let graph ≝ sg_rmvh graph v h in
  let graph ≝ pref_rmcheck graph v in
    graph.
    
definition ig_ipp ≝ sg_neighboursv.
definition ig_iph ≝ sg_neighboursh.
definition ig_ppp ≝ sg_neighboursv.
definition ig_pph ≝ sg_neighboursh.
definition ig_degree ≝ λgraph. λv. pset_lookup ? v (g_degree graph).
definition ig_lowest ≝ λgraph. pset_lowest ? (g_degree graph).
definition ig_lowest_non_move_related ≝ λgraph. pset_lowest ? (g_nmr graph).
definition ig_fold ≝ λA: Type[0]. λf: vertex → A → A. λgraph. λaccu.
  rt_fold … (λv. λ_. λaccu. f v accu) (g_regmap graph) accu.

definition ig_minimum: ∀a: Type[0]. (a → a → order) → (vertex → a) → graph → option vertex ≝
  λa: Type[0].
  λcompare: a → a → order.
  λf: vertex → a.
  λgraph.
  let folded ≝ ig_fold … (λw. λaccu.
    let dw ≝ f w in
      match accu with
      [ None      ⇒ Some … 〈dw, w〉
      | Some dv_v ⇒
        let 〈dv, v〉 ≝ dv_v in
          match compare dw dv with
          [ order_lt ⇒ Some … 〈dw, w〉
          | _        ⇒ accu
          ]
      ]) graph (None …)
  in
    match folded with
    [ None          ⇒ None …
    | Some ignore_v ⇒
      let 〈ignore, v〉 ≝ ignore_v in
        Some … v
    ].
    
definition ig_ppedge ≝ vertex × vertex.

definition ig_pppick ≝ λgraph. λp. set_tbl_pick … (g_pvv graph) p.

definition ig_phedge ≝ vertex × Register.

definition ig_phpick ≝ λgraph. λp. set_tbl_pick … (g_pvh graph) p.

definition ig_create ≝
  λregs.
  let 〈ignore_int, table'', priority''〉 ≝
    foldr … (λr. λv_table_priority'.
      let 〈v, table', priority'〉 ≝ v_table_priority' in
      let table'' ≝ rt_add r v table' in
      let priority'' ≝ pset_insert ? v 0 priority' in
        〈v + 1, table'', priority''〉) 〈0, rt_empty …, pset_empty …〉 regs
  in
      mk_graph table'' (set_tbl_empty …) (set_tbl_empty …) (set_tbl_empty …)
      (set_tbl_empty …) priority'' priority''.
definition ig_lookup ≝ λgraph. λr. rt_backward r (g_regmap graph).
definition ig_registers ≝ λgraph. λv. rt_forward v (g_regmap graph).
definition ig_mkipp ≝
  λgraph.
  λregs1.
  λregs2.
    set_fold … (λr1. λgraph.
      let v1 ≝ ig_lookup graph r1 in
        set_fold … (λr2. λgraph.
          sg_mkvv graph v1 (ig_lookup graph r2)
        ) regs2 graph
    ) regs1 graph.
definition ig_mkiph ≝
  λgraph.
  λregs.
  λhwregs.
    set_fold … (λr. λgraph.
      let v ≝ ig_lookup graph r in
        set_fold … (λh. λgraph.
          sg_mkvh graph v h
        ) hwregs graph
    ) regs graph.
definition ig_mki ≝
  λgraph.
  λregs1_hwregs1.
  λregs2_hwregs2.
  let 〈regs1, hwregs1〉 ≝ regs1_hwregs1 in
  let 〈regs2, hwregs2〉 ≝ regs2_hwregs2 in
  let graph ≝ ig_mkipp graph regs1 regs2 in
  let graph ≝ ig_mkiph graph regs1 hwregs2 in
  let graph ≝ ig_mkiph graph regs2 hwregs1 in
    graph.
definition ig_mkppp ≝
  λgraph.
  λr1.
  λr2.
  let v1 ≝ ig_lookup graph r1 in
  let v2 ≝ ig_lookup graph r2 in
  let graph ≝ sg_mkvv graph v1 v2 in
    graph.
definition ig_mkpph ≝
  λgraph.
  λr.
  λh.
  let v ≝ ig_lookup graph r in
  let graph ≝ sg_mkvh graph v h in
    graph.
(*    
(* XXX: precondition:
  x \not\eq y
  existsvv graph x y == false i.e. coalesce interfering edges *)
definition ig_coalesce ≝
  λgraph.
  λx.
  λy.
  let graph ≝ sg_coalesce graph x y in

let coalesce graph x y =

  assert (x <> y); (* attempt to coalesce one vertex with itself *)
  assert (not (interference#existsvv graph x y)); (* attempt to coalesce two interfering vertices *)

  (* Perform coalescing in the two subgraphs. *)

  let graph = interference#coalesce graph x y in
  let graph = preference#coalesce graph x y in

  (* Remove [x] from all tables. *)

  {
    graph with
    regmap = RegMap.coalesce x y graph.regmap;
    ivh = Vertex.Map.remove x graph.ivh;
    pvh = Vertex.Map.remove x graph.pvh;
    degree = PrioritySet.remove x graph.degree;
    nmr = PrioritySet.remove x graph.nmr;
  }

axiom ig_mkppp: graph → register → register → graph.
axiom ig_mkpph: graph → register → Register → graph.
axiom ig_coalesce: graph → vertex → vertex → graph.
axiom ig_coalesceh: graph → vertex → Register → graph.
axiom ig_remove: graph → vertex → graph.
axiom ig_freeze: graph → vertex → graph.
axiom ig_restrict: graph → (vertex → bool) → graph.
axiom ig_droph: graph → graph.
axiom ig_lookup: graph → register → vertex.
axiom ig_registers: graph → vertex → list register.
axiom ig_degree: graph → vertex → nat.
axiom ig_lowest: graph → option (vertex × nat).
axiom ig_lowest_non_move_related: graph → option (vertex × nat).
axiom ig_minimum: ∀A: Type[0]. ∀ord: A → A → order. (vertex → A) →
  graph → option vertex.
axiom ig_fold: ∀A: Type[0]. (vertex → A → A) → graph → A → A.
axiom ig_ipp: graph → vertex → vertex_set.
axiom ig_iph: graph → vertex → list Register.
axiom ig_ppp: graph → vertex → vertex_set.
axiom ig_pph: graph → vertex → list Register.
definition ig_ppedge ≝ vertex × vertex.
axiom ig_pppick: graph → (ig_ppedge → bool) → option ig_ppedge.
definition ig_phedge ≝ vertex × Register.
axiom ig_phpick: graph → (ig_phedge → bool) → option ig_phedge.
*)
*)