File ‹box_id.ML›
signature BOXID =
sig
type box_id
val string_of_box_id: box_id -> string
type box_lattice
val home_id: int
val has_incr_id: box_id -> bool
val add_incr_id: box_id -> box_id
val replace_incr_id: box_id -> box_id
val get_parent_prim: Proof.context -> int -> box_id
val get_ancestors_prim: Proof.context -> box_id -> int list
val reduce_box_id: Proof.context -> int list -> box_id
val get_parent_at_i: Proof.context -> box_id -> int -> box_id
val merge_boxes: Proof.context -> box_id * box_id -> box_id
val get_all_merges: Proof.context -> box_id list list -> box_id list
val get_all_merges_info:
Proof.context -> (box_id * 'a) list list -> (box_id * 'a list) list
val is_eq_ancestor: Proof.context -> box_id -> box_id -> bool
val is_eq_descendent: Proof.context -> box_id -> box_id -> bool
val is_box_resolved: Proof.context -> box_id -> bool
val is_box_unresolved: Proof.context -> box_id -> bool
val id_is_eq_ancestor: Proof.context -> box_id * 'a -> box_id * 'a -> bool
val info_eq_better: Proof.context -> box_id * thm -> box_id * thm -> bool
val merge_box_with_info:
Proof.context -> box_id -> (box_id * 'a) list -> (box_id * 'a) list
val merge_eq_infos: Proof.context -> box_id * thm -> box_id * thm -> box_id * thm
val add_prim_id: box_id -> Proof.context -> int * Proof.context
val add_resolved: box_id -> Proof.context -> Proof.context
end;
structure BoxID : BOXID =
struct
type box_id = int list
fun string_of_box_id id =
if length id = 1 then string_of_int (hd id)
else "(" ^ commas (map string_of_int id) ^ ")"
structure Boxidtab = Table (type key = box_id val ord = list_ord int_ord)
type box_lattice = {
parents: box_id vector,
resolved: box_id list
}
structure Data = Proof_Data
(
type T = box_lattice
fun init _ = {parents = Vector.fromList [[]], resolved = []}
)
val home_id = 1
fun has_incr_id id =
case id of [] => false | x :: _ => x = 0
fun add_incr_id id =
if has_incr_id id then raise Fail "add_incr_id"
else 0 :: id
fun replace_incr_id id =
if has_incr_id id then tl id else id
fun get_parent_prim ctxt prim_id =
let
val {parents, ...} = Data.get ctxt
in
Vector.sub (parents, prim_id)
end
handle Subscript => raise Fail "get_parent_prim: prim_id out of bounds."
fun get_ancestors_prim ctxt id =
let
fun helper all_ids cur_ids =
let
val new_ids =
(maps (get_parent_prim ctxt) cur_ids)
|> distinct (op =) |> subtract (op =) all_ids
in
if null new_ids then all_ids
else helper (all_ids @ new_ids) new_ids
end
in
helper id id
end
handle Option.Option =>
raise Fail "get_ancestors_prim: unexpected prim id."
fun reduce_box_id ctxt prim_lst =
let
fun helper taken rest =
case rest of
[] => taken
| cur :: rest' =>
let val cur_ancestors = get_ancestors_prim ctxt [cur]
in helper (cur :: subtract (op =) cur_ancestors taken) rest' end
in
rev (helper [] prim_lst)
end
fun ordered_merge ms ns =
case (ms, ns) of
([], _) => ns
| (_, []) => ms
| (m :: ms', n :: ns') =>
if m < n then m :: ordered_merge ms' ns
else if n < m then n :: ordered_merge ms ns'
else m :: ordered_merge ms' ns'
fun get_parent_at_i ctxt id i =
reduce_box_id ctxt (ordered_merge (nth_drop i id)
(get_parent_prim ctxt (nth id i)))
fun merge_boxes ctxt (id1, id2) =
let
val merged = ordered_merge id1 id2
val merged_len = length merged
in
if merged_len = length id1 then id1
else if merged_len = length id2 then id2
else reduce_box_id ctxt merged
end
fun get_all_merges ctxt id_lsts =
let
fun merge2 ids1 ids2 =
maps (fn id1 => map (fn id2 => merge_boxes ctxt (id1, id2)) ids2) ids1
|> distinct (op =)
in
fold merge2 id_lsts [[]]
end
fun get_all_merges_info ctxt lsts =
if null lsts then
raise Fail "get_all_merges_info: lsts is empty."
else
let
fun merge ((id1, x), (id2, xs))
= (merge_boxes ctxt (id1, id2), x :: xs)
fun merge2 (lst1, lst2) = map merge (Util.all_pairs (lst1, lst2))
in
Library.foldr merge2 (lsts, [([], [])])
end
fun is_eq_ancestor ctxt id id' = (id' = merge_boxes ctxt (id, id'))
fun is_eq_descendent ctxt id id' = (id = merge_boxes ctxt (id, id'))
fun is_box_resolved ctxt id =
let
val {resolved, ...} = Data.get ctxt
in
exists (is_eq_descendent ctxt id) resolved
end
val is_box_unresolved = not oo is_box_resolved
fun id_is_eq_ancestor ctxt (id, _) (id', _) = is_eq_ancestor ctxt id id'
fun info_eq_better ctxt (id, th) (id', th') =
Thm.prop_of th aconv Thm.prop_of th' andalso is_eq_ancestor ctxt id id'
fun merge_box_with_info ctxt id =
map (apfst (fn id' => merge_boxes ctxt (id, id')))
fun merge_eq_infos ctxt (id, th) (id', th') =
(merge_boxes ctxt (id, id'), Util.transitive_list [th, th'])
fun add_prim_id parent_id ctxt =
let
val {parents, resolved} = Data.get ctxt
val prim_id = Vector.length parents
val parents' = Vector.concat [parents, Vector.fromList [parent_id]]
in
(prim_id, ctxt |> Data.map (K {parents = parents', resolved = resolved}))
end
fun add_resolved id ctxt =
let
val {parents, resolved} = Data.get ctxt
in
if exists (is_eq_descendent ctxt id) resolved then ctxt
else let
val resolved' = id :: filter_out (is_eq_ancestor ctxt id) resolved
in
ctxt |> Data.map (K {parents = parents, resolved = resolved'})
end
end
end
type box_id = BoxID.box_id
type id_inst = box_id * (Type.tyenv * Envir.tenv)
type id_inst_th = id_inst * thm
type id_inst_ths = id_inst * thm list
structure Boxidtab = Table (type key = BoxID.box_id val ord = list_ord int_ord)