copying_gcScript.sml

(*
  Algorithm of a copying garbage collector.
*)
open HolKernel Parse boolLib bossLib; val _ = new_theory "copying_gc";

open pred_setTheory arithmeticTheory pairTheory listTheory combinTheory;
open finite_mapTheory sumTheory relationTheory;

val _ = ParseExtras.temp_loose_equality();

Datatype:
  heap_address = H_ADDR num | H_DATA 'a
End

Datatype:
  heap_element =
    H_EMP | H_REF num | H_BLOCK (('a heap_address) list # (num # 'b))
End

Definition getBLOCK_def:
  (getBLOCK z (H_BLOCK y) = y) /\
  (getBLOCK z _ = z)
End

Definition rel_move_def:
  (rel_move (H_DATA x,j,m,b,e,b2,e2) = (H_DATA x,j,m)) /\
  (rel_move (H_ADDR a,j,m,b,e,b2,e2) =
     case m a of
        H_EMP => (H_ADDR j,j,m)
      | H_REF i => (H_ADDR i,j,m)
      | H_BLOCK (xs,n,d) => let m = (a =+ H_REF j) m in
                            let m = (j =+ H_BLOCK (xs,n,d)) m in
                              (H_ADDR j,j + n + 1,m))
End

Definition rel_move_list_def:
  (rel_move_list ([],j,m,b,e,b2,e2) = ([],j,m)) /\
  (rel_move_list (x::xs,j,m,b,e,b2,e2) =
     let (x,j,m) = rel_move (x,j,m,b,e,b2,e2) in
     let (xs,j,m) = rel_move_list (xs,j,m,b,e,b2,e2) in
       (x::xs,j,m))
End

Definition rel_gc_step_def:
  rel_gc_step z (i,j,m,b,e,b2,e2) =
    let (xs,n,d) = getBLOCK z (m i) in
    let (ys,j,m) = rel_move_list (xs,j,m,b,e,b2,e2) in
    let m = (i =+ H_BLOCK (ys,n,d)) m in
    let i = i + n + 1 in
      (i,j,m)
End

Definition rel_gc_loop_def:
  rel_gc_loop z (i,j,m,b,e,b2,e2) =
    if i = j then (i,m) else
    if ~(i < j /\ j <= e) then (i,m) else
      let (i,j,m) = rel_gc_step z (i,j,m,b,e,b2,e2) in
      let (i,m) = rel_gc_loop z (i,j,m,b,e,b2,e2) in
        (i,m)
Termination
  WF_REL_TAC `measure (\(z,i,j,m,b,e,b2,e2). e - i)`
  THEN SIMP_TAC std_ss [rel_gc_step_def,LET_DEF]
  THEN CONV_TAC (DEPTH_CONV (PairRules.PBETA_CONV))
  THEN ONCE_REWRITE_TAC [EQ_SYM_EQ]
  THEN SIMP_TAC std_ss [] THEN REPEAT STRIP_TAC THEN DECIDE_TAC
End

Definition RANGE_def:
  RANGE(i:num,j) k = i <= k /\ k < j
End
Definition CUT_def:
  CUT (i,j) m = \k. if RANGE (i,j) k then m k else H_EMP
End

Definition rel_gc_def:
  rel_gc z (b:num,e:num,b2:num,e2:num,roots,m) =
    let (b2,e2,b,e) = (b,e,b2,e2) in
    let (roots,j,m) = rel_move_list (roots,b,m,b,e,b2,e2) in
    let (i,m) = rel_gc_loop z (b,j,m,b,e,b2,e2) in
    let m = CUT (b,i) m in
      (b,i,e,b2,e2,roots,m)
End

(*
val res = translate getBLOCK_def
val res = translate combinTheory.UPDATE_def
val res = translate rel_move_def
val res = translate rel_move_list_def
val res = translate rel_gc_step_def
val res = translate rel_gc_loop_def
val res = translate RANGE_def
val res = translate CUT_def
val res = translate rel_gc_def
*)

val _ = export_theory();